Skip to content

Commit aa84827

Browse files
hannes-steffenhagen-diffblueNlightNFotis
hannes-steffenhagen-diffblue
and
NlightNFotis
committed
Add function harness generator and generator factory
This adds a framework for adding various new harness generator types and adds tests. It also adds a harness generator that calls a given goto function. Co-authored-by: Hannes Steffenhagen <[email protected]> Co-authored-by: Fotis Koutoulakis <[email protected]>
1 parent 178802d commit aa84827

18 files changed

+563
-29
lines changed

‎regression/goto-harness/CMakeLists.txt

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,12 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
17
add_test_pl_tests(
2-
"$<TARGET_FILE:goto-harness>")
8+
"../chain.sh \
9+
$<TARGET_FILE:goto-cc> \
10+
$<TARGET_FILE:goto-harness> \
11+
$<TARGET_FILE:cbmc> \
12+
${is_windows}")

‎regression/goto-harness/Makefile

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,24 @@
11
default: tests.log
22

3+
include ../../src/config.inc
4+
include ../../src/common
5+
36
GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
7+
CBMC_EXE=../../../src/cbmc/cbmc
8+
9+
ifeq ($(BUILD_ENV_),MSVC)
10+
GOTO_CC_EXE=../../../src/goto-cc/goto-cl
11+
is_windows=true
12+
else
13+
GOTO_CC_EXE=../../../src/goto-cc/goto-cc
14+
is_windows=false
15+
endif
416

517
test:
6-
@../test.pl -p -c ${GOTO_HARNESS_EXE}
18+
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
719

820
tests.log: ../test.pl
9-
@../test.pl -p -c ${GOTO_HARNESS_EXE}
21+
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
1022

1123
show:
1224
@for dir in *; do \

‎regression/goto-harness/chain.sh

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
goto_cc=$1
6+
goto_harness=$2
7+
cbmc=$3
8+
is_windows=$4
9+
entry_point='generated_entry_function'
10+
11+
name=${*:$#}
12+
name=${name%.c}
13+
args=${*:5:$#-5}
14+
15+
if [[ "${is_windows}" == "true" ]]; then
16+
$goto_cc "${name}.c"
17+
mv "${name}.exe" "${name}.gb"
18+
else
19+
$goto_cc -o "${name}.gb" "${name}.c"
20+
fi
21+
22+
if [ -e "${name}-mod.gb" ] ; then
23+
rm -f "${name}-mod.gb"
24+
fi
25+
26+
script_dir=$(dirname $0)
27+
28+
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
29+
$cbmc $script_dir/dummy.c --function $entry_point "${name}-mod.gb"

‎regression/goto-harness/dummy.c

Whitespace-only changes.

‎regression/goto-harness/goto-harness-can-generate-trivial-harness/main.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <assert.h>
2+
3+
int function_to_test(int some_argument)
4+
{
5+
assert(some_argument == 0);
6+
return some_argument;
7+
}

‎regression/goto-harness/goto-harness-can-generate-trivial-harness/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function function_to_test
4+
^\[function_to_test.assertion.1\] line \d+ assertion some_argument == 0: FAILURE$
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$

‎regression/goto-harness/goto-harness-exists/test.desc

Lines changed: 0 additions & 6 deletions
This file was deleted.

‎src/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ languages: util.dir langapi.dir \
4949

5050
solvers.dir: util.dir
5151

52-
goto-harness.dir: util.dir
52+
goto-harness.dir: util.dir goto-programs.dir
5353

5454
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
5555
goto-symex.dir linking.dir analyses.dir solvers.dir

‎src/goto-harness/CMakeLists.txt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,6 @@ add_executable(goto-harness ${sources})
33
generic_includes(goto-harness)
44

55
target_link_libraries(goto-harness
6-
util
6+
util
7+
goto-programs
78
)

‎src/goto-harness/Makefile

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,16 @@
11
SRC = \
22
goto_harness_main.cpp \
33
goto_harness_parse_options.cpp \
4+
goto_harness_generator_factory.cpp \
5+
function_harness_generator.cpp \
46
# Empty last line
57

68
OBJ += \
79
../util/util$(LIBEXT) \
10+
../goto-programs/goto-programs$(LIBEXT) \
11+
../big-int/big-int$(LIBEXT) \
12+
../langapi/langapi$(LIBEXT) \
13+
../linking/linking$(LIBEXT) \
814
# Empty last line
915

1016
INCLUDES= -I ..

‎src/goto-harness/function_harness_generator.cpp

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
/******************************************************************\
2+
3+
Module: harness generator for functions
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include <goto-programs/goto_convert.h>
10+
#include <util/allocate_objects.h>
11+
#include <util/exception_utils.h>
12+
#include <util/std_code.h>
13+
#include <util/std_expr.h>
14+
#include <util/ui_message.h>
15+
16+
#include "function_harness_generator.h"
17+
#include "function_harness_generator_options.h"
18+
#include "goto_harness_parse_options.h"
19+
20+
struct function_harness_generatort::implt
21+
{
22+
ui_message_handlert *message_handler;
23+
irep_idt function;
24+
};
25+
26+
function_harness_generatort::function_harness_generatort(
27+
ui_message_handlert &message_handler)
28+
: goto_harness_generatort{}, pImpl(util_make_unique<implt>())
29+
{
30+
pImpl->message_handler = &message_handler;
31+
}
32+
33+
function_harness_generatort::~function_harness_generatort() = default;
34+
35+
void function_harness_generatort::handle_option(
36+
const std::string &option,
37+
const cmdlinet &cmdline)
38+
{
39+
if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
40+
{
41+
pImpl->function =
42+
cmdline.get_value(FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT);
43+
}
44+
else
45+
{
46+
throw invalid_command_line_argument_exceptiont{
47+
"function harness generator cannot handle this option", "--" + option};
48+
}
49+
}
50+
51+
void function_harness_generatort::generate(
52+
goto_modelt &goto_model,
53+
const irep_idt &harness_function_name)
54+
{
55+
auto const &function = pImpl->function;
56+
auto &symbol_table = goto_model.symbol_table;
57+
auto function_found = symbol_table.lookup(function);
58+
auto harness_function_found = symbol_table.lookup(harness_function_name);
59+
60+
if(function_found == nullptr)
61+
{
62+
throw invalid_command_line_argument_exceptiont{
63+
"function that should be harnessed is not found " + id2string(function),
64+
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
65+
}
66+
67+
if(harness_function_found != nullptr)
68+
{
69+
throw invalid_command_line_argument_exceptiont{
70+
"harness function already in the symbol table " +
71+
id2string(harness_function_name),
72+
"--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
73+
}
74+
75+
auto allocate_objects =
76+
allocate_objectst{ID_C, source_locationt{}, "__goto_harness", symbol_table};
77+
78+
// create body for the function
79+
code_blockt function_body{};
80+
81+
const auto &function_type = to_code_type(function_found->type);
82+
const auto &parameters = function_type.parameters();
83+
84+
code_function_callt::operandst arguments{};
85+
86+
for(const auto &parameter : parameters)
87+
{
88+
auto argument = allocate_objects.allocate_automatic_local_object(
89+
parameter.type(), parameter.get_base_name());
90+
arguments.push_back(argument);
91+
}
92+
93+
code_function_callt function_call{function_found->symbol_expr(), arguments};
94+
95+
function_body.add(function_call);
96+
97+
// create the function symbol
98+
symbolt harness_function_symbol{};
99+
harness_function_symbol.name = harness_function_symbol.base_name =
100+
harness_function_symbol.pretty_name = harness_function_name;
101+
102+
harness_function_symbol.is_lvalue = true;
103+
harness_function_symbol.mode = ID_C;
104+
harness_function_symbol.type =
105+
code_typet{code_typet::parameterst{}, void_typet{}};
106+
harness_function_symbol.value = function_body;
107+
108+
symbol_table.insert(harness_function_symbol);
109+
110+
auto const &generated_harness =
111+
goto_model.symbol_table.lookup_ref(harness_function_name);
112+
goto_model.goto_functions.function_map[harness_function_name].type =
113+
to_code_type(generated_harness.type);
114+
auto &body =
115+
goto_model.goto_functions.function_map[harness_function_name].body;
116+
goto_convert(
117+
static_cast<const codet &>(generated_harness.value),
118+
goto_model.symbol_table,
119+
body,
120+
*pImpl->message_handler,
121+
ID_C);
122+
body.add_instruction(goto_program_instruction_typet::END_FUNCTION);
123+
}

‎src/goto-harness/function_harness_generator.h

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
/******************************************************************\
2+
3+
Module: harness generator for functions
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_H
10+
#define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_H
11+
12+
#include <memory>
13+
#include <string>
14+
15+
#include <util/ui_message.h>
16+
17+
#include "goto_harness_generator.h"
18+
19+
/// Function harness generator that for a specified goto-function
20+
/// generates a harness that sets up its arguments and calls it.
21+
class function_harness_generatort : public goto_harness_generatort
22+
{
23+
public:
24+
function_harness_generatort(ui_message_handlert &message_handler);
25+
~function_harness_generatort() override;
26+
void
27+
handle_option(const std::string &option, const cmdlinet &cmdline) override;
28+
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
29+
override;
30+
31+
private:
32+
struct implt;
33+
std::unique_ptr<implt> pImpl;
34+
};
35+
36+
#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_H

‎src/goto-harness/function_harness_generator_options.h

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/******************************************************************\
2+
3+
Module: functions_harness_generator_options
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
10+
#define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
11+
12+
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
13+
#define FUNCTION_HARNESS_GENERATOR_OPTIONS \
14+
"(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"
15+
// FUNCTION_HARNESS_GENERATOR_OPTIONS
16+
17+
#define FUNCTION_HARNESS_GENERATOR_HELP \
18+
"function harness generator (--harness-type call-function)\n\n" \
19+
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \
20+
" the function the harness should call\n" // FUNCTION_HARNESS_GENERATOR_HELP
21+
22+
#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H

‎src/goto-harness/goto_harness_generator.h

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
/******************************************************************\
2+
3+
Module: goto_harness_generator
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#ifndef CRPOVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
10+
#define CRPOVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_H
11+
12+
#include <goto-programs/goto_model.h>
13+
#include <util/cmdline.h>
14+
#include <util/irep.h>
15+
16+
class goto_harness_generatort
17+
{
18+
public:
19+
/// Handle a command line argument. Should throw an exception if the option
20+
/// doesn't apply to this generator. Should only set options rather than
21+
/// immediately performing work
22+
virtual void
23+
handle_option(const std::string &option, const cmdlinet &cmdline) = 0;
24+
25+
/// Generate a harness according to the set options
26+
virtual void
27+
generate(goto_modelt &goto_model, const irep_idt &harness_function_name) = 0;
28+
29+
virtual ~goto_harness_generatort() = default;
30+
};
31+
32+
#endif // CRPOVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H

0 commit comments

Comments
 (0)