Skip to content

Commit b3a0a62

Browse files
hannes-steffenhagen-diffblueNlightNFotis
hannes-steffenhagen-diffblue
authored 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.
1 parent 8615e3b commit b3a0a62

18 files changed

+554
-33
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: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,21 @@
11
default: tests.log
22

33
GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
4+
CBMC_EXE=../../../src/cbmc/cbmc
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
GOTO_CC_EXE=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
else
10+
GOTO_CC_EXE=../../../src/goto-cc/goto-cc
11+
is_windows=false
12+
endif
413

514
test:
6-
@../test.pl -p -c ${GOTO_HARNESS_EXE}
15+
@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
716

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

1120
show:
1221
@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/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: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
/******************************************************************\
2+
3+
Module: harness generator for functions
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include <util/allocate_objects.h>
10+
#include <util/exception_utils.h>
11+
#include <util/std_code.h>
12+
#include <util/std_expr.h>
13+
14+
#include "function_harness_generator.h"
15+
#include "function_harness_generator_options.h"
16+
#include "goto_harness_parse_options.h"
17+
18+
void function_harness_generatort::handle_option(
19+
const std::string &option,
20+
const cmdlinet &cmdline)
21+
{
22+
if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
23+
{
24+
function = cmdline.get_value(FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT);
25+
}
26+
else
27+
{
28+
throw invalid_command_line_argument_exceptiont{
29+
"function harness generator cannot handle this option", "--" + option};
30+
}
31+
}
32+
33+
void function_harness_generatort::generate(
34+
goto_modelt &goto_model,
35+
const irep_idt &harness_function_name)
36+
{
37+
auto &symbol_table = goto_model.symbol_table;
38+
auto function_found = symbol_table.lookup(function);
39+
auto harness_function_found = symbol_table.lookup(harness_function_name);
40+
41+
if(function_found == nullptr)
42+
{
43+
throw invalid_command_line_argument_exceptiont{
44+
"function that should be harnessed is not found " + id2string(function),
45+
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
46+
}
47+
48+
if(harness_function_found != nullptr)
49+
{
50+
throw invalid_command_line_argument_exceptiont{
51+
"harness function already in the symbol table " +
52+
id2string(harness_function_name),
53+
"--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
54+
}
55+
56+
auto allocate_objects =
57+
allocate_objectst{ID_C, source_locationt{}, "__goto_harness", symbol_table};
58+
59+
// create body for the function
60+
code_blockt function_body{};
61+
62+
const auto &function_type = to_code_type(function_found->type);
63+
const auto &parameters = function_type.parameters();
64+
65+
code_function_callt::operandst arguments{};
66+
67+
for(const auto &parameter : parameters)
68+
{
69+
auto argument = allocate_objects.allocate_automatic_local_object(
70+
parameter.type(), parameter.get_base_name());
71+
arguments.push_back(argument);
72+
}
73+
74+
code_function_callt function_call{function_found->symbol_expr(), arguments};
75+
76+
function_body.add(function_call);
77+
78+
// create the function symbol
79+
symbolt harness_function_symbol{};
80+
harness_function_symbol.name = harness_function_symbol.base_name =
81+
harness_function_symbol.pretty_name = harness_function_name;
82+
83+
harness_function_symbol.is_lvalue = true;
84+
harness_function_symbol.mode = ID_C;
85+
harness_function_symbol.type =
86+
code_typet{code_typet::parameterst{}, void_typet{}};
87+
harness_function_symbol.value = function_body;
88+
89+
symbol_table.insert(harness_function_symbol);
90+
goto_model.goto_functions.update();
91+
}

‎src/goto-harness/function_harness_generator.h

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
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 <string>
13+
14+
#include "goto_harness_generator.h"
15+
16+
/// Function harness generator that for a specified goto-function
17+
/// generates a harness that sets up its arguments and calls it.
18+
class function_harness_generatort : public goto_harness_generatort
19+
{
20+
public:
21+
void
22+
handle_option(const std::string &option, const cmdlinet &cmdline) override;
23+
24+
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
25+
override;
26+
27+
private:
28+
irep_idt function;
29+
};
30+
31+
#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

‎src/goto-harness/goto_harness_generator_factory.cpp

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/******************************************************************\
2+
3+
Module: goto_harness_generator_factory
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include "goto_harness_generator_factory.h"
10+
11+
#include <util/exception_utils.h>
12+
#include <util/invariant.h>
13+
#include <util/make_unique.h>
14+
#include <util/string_utils.h>
15+
16+
#include <algorithm>
17+
#include <functional>
18+
#include <iterator>
19+
#include <sstream>
20+
#include <string>
21+
22+
void goto_harness_generator_factoryt::register_generator(
23+
std::string generator_name,
24+
build_generatort build_generator)
25+
{
26+
PRECONDITION(generators.find(generator_name) == generators.end());
27+
auto res = generators.insert({generator_name, build_generator});
28+
CHECK_RETURN(res.second);
29+
}
30+
31+
std::unique_ptr<goto_harness_generatort>
32+
goto_harness_generator_factoryt::factory(const std::string &generator_name)
33+
{
34+
auto it = generators.find(generator_name);
35+
36+
if(it != generators.end())
37+
{
38+
return it->second();
39+
}
40+
else
41+
{
42+
throw invalid_command_line_argument_exceptiont(
43+
"unknown generator type",
44+
"--" GOTO_HARNESS_GENERATOR_TYPE_OPT,
45+
join_strings(
46+
std::ostringstream(),
47+
generators.begin(),
48+
generators.end(),
49+
", ",
50+
[](const std::pair<std::string, build_generatort> &value) {
51+
return value.first;
52+
})
53+
.str());
54+
}
55+
}

0 commit comments

Comments
 (0)