Skip to content

Commit c7b962f

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #4014 from NlightNFotis/new_chain_sh
Add function harness generator and generator factory
2 parents 85a2a6a + 7b55287 commit c7b962f

20 files changed

+678
-35
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,8 @@ src/goto-cc/goto-cc
102102
src/goto-cc/goto-gcc
103103
src/goto-cc/goto-cc.exe
104104
src/goto-cc/goto-cl.exe
105+
src/goto-harness/goto-harness
106+
src/goto-harness/goto-harness.exe
105107
src/goto-instrument/goto-instrument
106108
src/goto-instrument/goto-instrument.exe
107109
src/solvers/smt2_solver

‎regression/goto-harness/CMakeLists.txt

+11-1
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

+14-2
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

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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+
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
27+
$cbmc --function $entry_point "${name}-mod.gb"

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

+7
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

+7
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

-6
This file was deleted.

‎src/Makefile

+1-1
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

+2-1
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

+7
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,17 @@
11
SRC = \
2+
function_call_harness_generator.cpp \
3+
goto_harness_generator.cpp \
4+
goto_harness_generator_factory.cpp \
25
goto_harness_main.cpp \
36
goto_harness_parse_options.cpp \
47
# Empty last line
58

69
OBJ += \
710
../util/util$(LIBEXT) \
11+
../goto-programs/goto-programs$(LIBEXT) \
12+
../big-int/big-int$(LIBEXT) \
13+
../langapi/langapi$(LIBEXT) \
14+
../linking/linking$(LIBEXT) \
815
# Empty last line
916

1017
INCLUDES= -I ..

‎src/goto-harness/function_call_harness_generator.cpp

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

‎src/goto-harness/function_call_harness_generator.h

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

‎src/goto-harness/function_harness_generator_options.h

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
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+
// clang-format off
18+
#define FUNCTION_HARNESS_GENERATOR_HELP \
19+
"function harness generator (--harness-type call-function)\n\n" \
20+
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \
21+
" the function the harness should call\n" \
22+
// FUNCTION_HARNESS_GENERATOR_HELP
23+
// clang-format on
24+
25+
#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H

‎src/goto-harness/goto_harness_generator.cpp

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/******************************************************************\
2+
3+
Module: goto_harness_generator
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include "goto_harness_generator.h"
10+
11+
#include <list>
12+
#include <string>
13+
14+
#include <util/exception_utils.h>
15+
#include <util/invariant.h>
16+
17+
std::string goto_harness_generatort::require_exactly_one_value(
18+
const std::string &option,
19+
const std::list<std::string> &values)
20+
{
21+
if(values.size() != 1)
22+
{
23+
throw invalid_command_line_argument_exceptiont{"expected exactly one value",
24+
"--" + option};
25+
}
26+
27+
return values.front();
28+
}
29+
30+
void goto_harness_generatort::assert_no_values(
31+
const std::string &option,
32+
const std::list<std::string> &values)
33+
{
34+
PRECONDITION_WITH_DIAGNOSTICS(values.empty(), option);
35+
}

0 commit comments

Comments
 (0)