diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh index 01d447961a6..60aa1b47322 100755 --- a/regression/goto-harness/chain.sh +++ b/regression/goto-harness/chain.sh @@ -24,8 +24,9 @@ if [ -e "${name}-mod.gb" ] ; then fi # `# some comment` is an inline comment - basically, cause bash to execute an empty command - +$cbmc --show-goto-functions "${name}.gb" $goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} +$cbmc --show-goto-functions "${name}-mod.gb" $cbmc --function $entry_point "${name}-mod.gb" \ --pointer-check `# because we want to see out of bounds errors` \ --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \ diff --git a/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-1-snapshot.json b/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-1-snapshot.json new file mode 100644 index 00000000000..6d4258f3a9e --- /dev/null +++ b/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-1-snapshot.json @@ -0,0 +1,62 @@ +{ + "symbolTable": { + "x": { + "baseName": "x", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": {}, + "mode": "C", + "module": "main", + "name": "x", + "prettyName": "x", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": {}, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + } + } +} diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/main.c b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/main.c new file mode 100644 index 00000000000..8f23ee994bd --- /dev/null +++ b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/main.c @@ -0,0 +1,18 @@ +int x; +int flag; + +int main() +{ + x = 0; + + assert(flag != 0 || x == 1); + assert(flag != 1 || x == 0); + + if(flag == 0) + { + flag = 1; + main(); + } + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc new file mode 100644 index 00000000000..d05e4853896 --- /dev/null +++ b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:1 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/main.c b/regression/goto-harness/load-snapshot-static-global-array-01/main.c new file mode 100644 index 00000000000..c17e3aec4a9 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-array-01/main.c @@ -0,0 +1,10 @@ +int x[] = {1, 2, 3}; + +int main() +{ + assert(x[0] == 4); + assert(x[1] == 5); + assert(x[2] == 6); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/snapshot.json b/regression/goto-harness/load-snapshot-static-global-array-01/snapshot.json new file mode 100644 index 00000000000..c0cfc3b5f81 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-array-01/snapshot.json @@ -0,0 +1,181 @@ +{ + "symbolTable": { + "x": { + "baseName": "x", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": {}, + "mode": "C", + "module": "test", + "name": "x", + "prettyName": "x", + "type": { + "id": "array", + "namedSub": { + "#source_location": {}, + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "3" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + }, + "value": { + "id": "array", + "namedSub": { + "#source_location": {}, + "type": { + "id": "array", + "namedSub": { + "#source_location": {}, + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "3" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": {}, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "4" + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": {}, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "5" + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": {}, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "6" + } + } + } + ] + } + } + } +} diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc new file mode 100644 index 00000000000..8092fa6d9f6 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-location main:0 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/main.c b/regression/goto-harness/load-snapshot-static-global-int-01/main.c new file mode 100644 index 00000000000..e9414393722 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-01/main.c @@ -0,0 +1,8 @@ +int x; + +int main() +{ + assert(x == 1); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc new file mode 100644 index 00000000000..1e064294660 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/main.c b/regression/goto-harness/load-snapshot-static-global-int-02/main.c new file mode 100644 index 00000000000..6583b6b1c7e --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-02/main.c @@ -0,0 +1,10 @@ +int x; +int y; // snapshot contains no value for y + +int main() +{ + assert(x == 1); + assert(y == 1); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc new file mode 100644 index 00000000000..db97cfec79c --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion y == 1: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/main.c b/regression/goto-harness/load-snapshot-static-global-int-03/main.c new file mode 100644 index 00000000000..21e3752f42f --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-03/main.c @@ -0,0 +1,14 @@ +int x; + +void func() +{ +} + +int main() +{ + func(); + + assert(x == 1); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc new file mode 100644 index 00000000000..1e064294660 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/main.c b/regression/goto-harness/load-snapshot-static-global-int-04/main.c new file mode 100644 index 00000000000..f4d94b66815 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-04/main.c @@ -0,0 +1,10 @@ +int x; + +int main() +{ + x = 0; // should be skipped + + assert(x == 1); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc new file mode 100644 index 00000000000..d05e4853896 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:1 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/main.c b/regression/goto-harness/load-snapshot-static-global-pointer-01/main.c new file mode 100644 index 00000000000..13762a4a775 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/main.c @@ -0,0 +1,11 @@ +int x; +int *p; // has value &x in the snapshot + +int main() +{ + x = 1; + + assert(*p == 1); + + return 0; +} diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/snapshot.json b/regression/goto-harness/load-snapshot-static-global-pointer-01/snapshot.json new file mode 100644 index 00000000000..bf3df318dda --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/snapshot.json @@ -0,0 +1,102 @@ +{ + "symbolTable": { + "p": { + "baseName": "p", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": {}, + "mode": "C", + "module": "main", + "name": "p", + "prettyName": "p", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": {}, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + }, + "value": { + "id": "address_of", + "namedSub": { + "#source_location": {}, + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": {}, + "identifier": { + "id": "x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + } + } +} diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc new file mode 100644 index 00000000000..8092fa6d9f6 --- /dev/null +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-location main:0 +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/src/goto-harness/CMakeLists.txt b/src/goto-harness/CMakeLists.txt index 9e73873ffa3..00e4e895e03 100644 --- a/src/goto-harness/CMakeLists.txt +++ b/src/goto-harness/CMakeLists.txt @@ -5,4 +5,6 @@ generic_includes(goto-harness) target_link_libraries(goto-harness util goto-programs + json + json-symtab-language ) diff --git a/src/goto-harness/Makefile b/src/goto-harness/Makefile index 1d9edf0ecdd..0b12fb4d95e 100644 --- a/src/goto-harness/Makefile +++ b/src/goto-harness/Makefile @@ -4,6 +4,7 @@ SRC = \ goto_harness_generator_factory.cpp \ goto_harness_main.cpp \ goto_harness_parse_options.cpp \ + memory_snapshot_harness_generator.cpp \ recursive_initialization.cpp \ # Empty last line @@ -13,6 +14,8 @@ OBJ += \ ../big-int/big-int$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../linking/linking$(LIBEXT) \ + ../json/json$(LIBEXT) \ + ../json-symtab-language/json-symtab-language$(LIBEXT) \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index b18b8136431..f36766be7e2 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -272,7 +272,8 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for( recursive_initialization->initialize(lhs, 0, {}, block); } -void function_call_harness_generatort::validate_options() +void function_call_harness_generatort::validate_options( + const goto_modelt &goto_model) { if(p_impl->function == ID_empty) throw invalid_command_line_argument_exceptiont{ diff --git a/src/goto-harness/function_call_harness_generator.h b/src/goto-harness/function_call_harness_generator.h index 354542b757b..56ab474796a 100644 --- a/src/goto-harness/function_call_harness_generator.h +++ b/src/goto-harness/function_call_harness_generator.h @@ -33,7 +33,7 @@ class function_call_harness_generatort : public goto_harness_generatort const std::string &option, const std::list &values) override; - void validate_options() override; + void validate_options(const goto_modelt &goto_model) override; private: std::size_t require_one_size_value( diff --git a/src/goto-harness/goto_harness_generator.h b/src/goto-harness/goto_harness_generator.h index 7869b5d757b..ada7bae4fd3 100644 --- a/src/goto-harness/goto_harness_generator.h +++ b/src/goto-harness/goto_harness_generator.h @@ -35,7 +35,7 @@ class goto_harness_generatort const std::list &values) = 0; /// Check if options are in a sane state, throw otherwise - virtual void validate_options() = 0; + virtual void validate_options(const goto_modelt &goto_model) = 0; /// Returns the only value of a single element list, /// throws an exception if not passed a single element list diff --git a/src/goto-harness/goto_harness_generator_factory.cpp b/src/goto-harness/goto_harness_generator_factory.cpp index 679246f6e62..9a02783bcff 100644 --- a/src/goto-harness/goto_harness_generator_factory.cpp +++ b/src/goto-harness/goto_harness_generator_factory.cpp @@ -31,7 +31,8 @@ void goto_harness_generator_factoryt::register_generator( std::unique_ptr goto_harness_generator_factoryt::factory( const std::string &generator_name, - const generator_optionst &generator_options) + const generator_optionst &generator_options, + const goto_modelt &goto_model) { auto it = generators.find(generator_name); @@ -42,7 +43,7 @@ goto_harness_generator_factoryt::factory( { generator->handle_option(option.first, option.second); } - generator->validate_options(); + generator->validate_options(goto_model); return generator; } diff --git a/src/goto-harness/goto_harness_generator_factory.h b/src/goto-harness/goto_harness_generator_factory.h index fcdf69fe9d8..7e1f75d3c41 100644 --- a/src/goto-harness/goto_harness_generator_factory.h +++ b/src/goto-harness/goto_harness_generator_factory.h @@ -48,7 +48,8 @@ class goto_harness_generator_factoryt /// throws if no generator with the supplied name is registered. std::unique_ptr factory( const std::string &generator_name, - const generator_optionst &generator_options); + const generator_optionst &generator_options, + const goto_modelt &goto_model); private: std::map generators; diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 994004621b5..aa351b926be 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -25,6 +25,7 @@ Author: Diffblue Ltd. #include "function_call_harness_generator.h" #include "goto_harness_generator_factory.h" +#include "memory_snapshot_harness_generator.h" // The basic idea is that this module is handling the following // sequence of events: @@ -49,11 +50,6 @@ int goto_harness_parse_optionst::doit() auto factory_options = collect_generate_factory_options(); - // Initialise harness generator - auto harness_generator = - factory.factory(got_harness_config.harness_type, factory_options); - CHECK_RETURN(harness_generator != nullptr); - // This just sets up the defaults (and would interpret options such as --32). config.set(cmdline); @@ -66,8 +62,28 @@ int goto_harness_parse_optionst::doit() got_harness_config.in_file + "'"}; } auto goto_model = std::move(read_goto_binary_result.value()); + + // This has to be called after the defaults are set up (as per the + // config.set(cmdline) above) otherwise, e.g. the architecture specification + // will be unknown. config.set_from_symbol_table(goto_model.symbol_table); + if(goto_model.symbol_table.has_symbol( + got_harness_config.harness_function_name)) + { + throw invalid_command_line_argument_exceptiont( + "harness function `" + + id2string(got_harness_config.harness_function_name) + + "` already in " + "the symbol table", + "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT); + } + + // Initialise harness generator + auto harness_generator = factory.factory( + got_harness_config.harness_type, factory_options, goto_model); + CHECK_RETURN(harness_generator != nullptr); + harness_generator->generate( goto_model, got_harness_config.harness_function_name); @@ -103,7 +119,8 @@ void goto_harness_parse_optionst::help() "generate\n" << "--harness-type one of the harness types listed below\n" << "\n\n" - << FUNCTION_HARNESS_GENERATOR_HELP << messaget::eom; + << FUNCTION_HARNESS_GENERATOR_HELP << "\n\n" + << MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP << messaget::eom; } goto_harness_parse_optionst::goto_harness_parse_optionst( @@ -162,6 +179,12 @@ goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory() return util_make_unique( ui_message_handler); }); + + factory.register_generator("initialise-with-memory-snapshot", [this]() { + return util_make_unique( + ui_message_handler); + }); + return factory; } diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h index 3cb8dcc0c63..8665574c9da 100644 --- a/src/goto-harness/goto_harness_parse_options.h +++ b/src/goto-harness/goto_harness_parse_options.h @@ -23,6 +23,7 @@ Author: Diffblue Ltd. "(version)" \ GOTO_HARNESS_FACTORY_OPTIONS \ FUNCTION_HARNESS_GENERATOR_OPTIONS \ + MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ // end GOTO_HARNESS_OPTIONS // clang-format on diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp new file mode 100644 index 00000000000..47c23c2a318 --- /dev/null +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -0,0 +1,336 @@ +/******************************************************************\ + +Module: Harness to initialise memory from memory snapshot + +Author: Daniel Poetzl + +\******************************************************************/ + +#include "memory_snapshot_harness_generator.h" + +#include + +#include + +#include + +#include +#include +#include +#include +#include +#include + +#include + +#include "goto_harness_generator_factory.h" + +void memory_snapshot_harness_generatort::handle_option( + const std::string &option, + const std::list &values) +{ + if(option == "memory-snapshot") + { + memory_snapshot_file = require_exactly_one_value(option, values); + } + else if(option == "initial-location") + { + const std::string initial_location = + require_exactly_one_value(option, values); + + std::vector start; + split_string(initial_location, ':', start, true); + + if( + start.empty() || start.front().empty() || + (start.size() == 2 && start.back().empty()) || start.size() > 2) + { + throw invalid_command_line_argument_exceptiont( + "invalid initial location specification", "--initial-location"); + } + + entry_function_name = start.front(); + + if(start.size() == 2) + { + location_number = optionalt(safe_string2unsigned(start.back())); + } + } + else + { + throw invalid_command_line_argument_exceptiont( + "unrecognized option for memory snapshot harness generator", + "--" + option); + } +} + +void memory_snapshot_harness_generatort::validate_options( + const goto_modelt &goto_model) +{ + if(memory_snapshot_file.empty()) + { + throw invalid_command_line_argument_exceptiont( + "option --memory_snapshot is required", + "--harness-type initialise-from-memory-snapshot"); + } + + if(entry_function_name.empty()) + { + INVARIANT( + !location_number.has_value(), + "when `function` is empty then the option --initial-location was not " + "given and thus `location_number` was not set"); + + throw invalid_command_line_argument_exceptiont( + "option --initial-location is required", + "--harness-type initialise-from-memory-snapshot"); + } + + const auto &goto_functions = goto_model.goto_functions; + const auto &goto_function = + goto_functions.function_map.find(entry_function_name); + if(goto_function == goto_functions.function_map.end()) + { + throw invalid_command_line_argument_exceptiont( + "unknown initial location specification", "--initial-location"); + } + + if(!goto_function->second.body_available()) + { + throw invalid_command_line_argument_exceptiont( + "given function `" + id2string(entry_function_name) + + "` does not have a body", + "--initial-location"); + } + + if(location_number.has_value()) + { + const auto &goto_program = goto_function->second.body; + const auto opt_it = goto_program.get_target(*location_number); + + if(!opt_it.has_value()) + { + throw invalid_command_line_argument_exceptiont( + "no instruction with location number " + + std::to_string(*location_number) + " in function " + + id2string(entry_function_name), + "--initial-location"); + } + } + + if(goto_functions.function_map.count(INITIALIZE_FUNCTION) == 0) + { + throw invalid_command_line_argument_exceptiont( + "invalid input program: " + std::string(INITIALIZE_FUNCTION) + + " not found", + ""); + } + + const symbol_tablet &symbol_table = goto_model.symbol_table; + const symbolt *called_function_symbol = + symbol_table.lookup(entry_function_name); + + if(called_function_symbol == nullptr) + { + throw invalid_command_line_argument_exceptiont( + "function `" + id2string(entry_function_name) + + "` not found in the symbol table", + "--initial-location"); + } +} + +void memory_snapshot_harness_generatort::add_init_section( + goto_modelt &goto_model) const +{ + goto_functionst &goto_functions = goto_model.goto_functions; + symbol_tablet &symbol_table = goto_model.symbol_table; + + goto_functiont &goto_function = + goto_functions.function_map[entry_function_name]; + const symbolt &function_symbol = symbol_table.lookup_ref(entry_function_name); + + goto_programt &goto_program = goto_function.body; + + // introduce a symbol for a Boolean variable to indicate the point at which + // the function initialisation is completed + symbolt &func_init_done_symbol = get_fresh_aux_symbol( + bool_typet(), + id2string(entry_function_name), + "func_init_done", + function_symbol.location, + function_symbol.mode, + symbol_table); + func_init_done_symbol.is_static_lifetime = true; + func_init_done_symbol.value = false_exprt(); + + const symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr(); + + // initialise func_init_done_var in __CPROVER_initialize if it is present + // so that it's FALSE value is visible before the harnessed function is called + goto_programt &cprover_initialize = + goto_functions.function_map.find(INITIALIZE_FUNCTION)->second.body; + cprover_initialize.insert_before( + std::prev(cprover_initialize.instructions.end()), + goto_programt::make_assignment( + code_assignt(func_init_done_var, false_exprt()))); + + const goto_programt::const_targett start_it = + goto_program.instructions.begin(); + + auto ins_it1 = goto_program.insert_before( + start_it, + goto_programt::make_goto(goto_program.const_cast_target(start_it))); + ins_it1->guard = func_init_done_var; + + auto ins_it2 = goto_program.insert_after( + ins_it1, + goto_programt::make_assignment( + code_assignt(func_init_done_var, true_exprt()))); + + goto_program.compute_location_numbers(); + goto_program.insert_after( + ins_it2, + goto_programt::make_goto(goto_program.const_cast_target( + location_number.has_value() ? *goto_program.get_target(*location_number) + : start_it))); +} + +code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( + const symbol_tablet &snapshot) const +{ + code_blockt code; + for(const auto &pair : snapshot) + { + const symbolt &symbol = pair.second; + + if(!symbol.is_static_lifetime) + continue; + + code.add(code_assignt{symbol.symbol_expr(), symbol.value}); + } + return code; +} + +void memory_snapshot_harness_generatort::add_call_with_nondet_arguments( + const symbolt &called_function_symbol, + code_blockt &code) const +{ + const code_typet &code_type = to_code_type(called_function_symbol.type); + + code_function_callt::argumentst arguments; + + for(const code_typet::parametert ¶meter : code_type.parameters()) + { + arguments.push_back(side_effect_expr_nondett{ + parameter.type(), called_function_symbol.location}); + } + + code.add(code_function_callt{called_function_symbol.symbol_expr(), + std::move(arguments)}); +} + +void memory_snapshot_harness_generatort:: + insert_harness_function_into_goto_model( + goto_modelt &goto_model, + const symbolt &function) const +{ + const auto r = goto_model.symbol_table.insert(function); + CHECK_RETURN(r.second); + + auto function_iterator_pair = goto_model.goto_functions.function_map.emplace( + function.name, goto_functiont{}); + + CHECK_RETURN(function_iterator_pair.second); + + goto_functiont &harness_function = function_iterator_pair.first->second; + harness_function.type = to_code_type(function.type); + + goto_convert( + to_code_block(to_code(function.value)), + goto_model.symbol_table, + harness_function.body, + message_handler, + function.mode); + + harness_function.body.add(goto_programt::make_end_function()); +} + +void memory_snapshot_harness_generatort::get_memory_snapshot( + const std::string &file, + symbol_tablet &snapshot) const +{ + jsont json; + + const bool r = parse_json(memory_snapshot_file, message_handler, json); + + if(r) + { + throw deserialization_exceptiont("failed to read JSON memory snapshot"); + } + + if(json.is_array()) + { + // since memory-analyzer produces an array JSON we need to search it + // to find the first JSON object that is a symbol table + const auto &jarr = to_json_array(json); + for(auto const &arr_element : jarr) + { + if(!arr_element.is_object()) + continue; + const auto &json_obj = to_json_object(arr_element); + const auto it = json_obj.find("symbolTable"); + if(it != json_obj.end()) + { + symbol_table_from_json(json_obj, snapshot); + return; + } + } + throw deserialization_exceptiont( + "JSON memory snapshot does not contain symbol table"); + } + else + { + // throws a deserialization_exceptiont or an + // incorrect_goto_program_exceptiont + // on failure to read JSON symbol table + symbol_table_from_json(json, snapshot); + } +} + +void memory_snapshot_harness_generatort::generate( + goto_modelt &goto_model, + const irep_idt &harness_function_name) +{ + symbol_tablet snapshot; + get_memory_snapshot(memory_snapshot_file, snapshot); + + symbol_tablet &symbol_table = goto_model.symbol_table; + goto_functionst &goto_functions = goto_model.goto_functions; + + const symbolt *called_function_symbol = + symbol_table.lookup(entry_function_name); + + add_init_section(goto_model); + + code_blockt harness_function_body = add_assignments_to_globals(snapshot); + + add_call_with_nondet_arguments( + *called_function_symbol, harness_function_body); + + // Create harness function symbol + + symbolt harness_function_symbol; + harness_function_symbol.name = harness_function_name; + harness_function_symbol.base_name = harness_function_name; + harness_function_symbol.pretty_name = harness_function_name; + + harness_function_symbol.is_lvalue = true; + harness_function_symbol.mode = called_function_symbol->mode; + harness_function_symbol.type = code_typet({}, empty_typet()); + harness_function_symbol.value = harness_function_body; + + // Add harness function to goto model and symbol table + insert_harness_function_into_goto_model(goto_model, harness_function_symbol); + + goto_functions.update(); +} diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h new file mode 100644 index 00000000000..fac5f6484e9 --- /dev/null +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -0,0 +1,82 @@ +/******************************************************************\ + +Module: Harness to initialise memory from memory snapshot + +Author: Daniel Poetzl + +\******************************************************************/ + +#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H +#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H + +#include +#include + +#include "goto_harness_generator.h" + +#include + +#include +#include + +#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ + "(memory-snapshot):" \ + "(initial-location):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS + +// clang-format off +#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ + "memory snapshot harness generator (--harness-type\n" \ + " initialise-from-memory-snapshot)\n\n" \ + "--memory-snapshot initialise memory from JSON memory snapshot\n"\ + "--initial-location ]>\n" \ + " use given function and location number as " \ + "entry\n point\n" \ + // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP +// clang-format on + +/// Generates a harness which first assigns global variables with values from +/// a given memory snapshot and then calls a specified function. The called +/// function is also modified such that it appears to start executing at the +/// given location number on the first invocation. +class memory_snapshot_harness_generatort : public goto_harness_generatort +{ +public: + explicit memory_snapshot_harness_generatort(message_handlert &message_handler) + : message_handler(message_handler) + { + } + + void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) + override; + +protected: + void handle_option( + const std::string &option, + const std::list &values) override; + + void validate_options(const goto_modelt &goto_model) override; + + void + get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const; + + void add_init_section(goto_modelt &goto_model) const; + + code_blockt add_assignments_to_globals(const symbol_tablet &snapshot) const; + + void add_call_with_nondet_arguments( + const symbolt &called_function_symbol, + code_blockt &code) const; + + void insert_harness_function_into_goto_model( + goto_modelt &goto_model, + const symbolt &function) const; + + std::string memory_snapshot_file; + + irep_idt entry_function_name; + optionalt location_number; + + message_handlert &message_handler; +}; + +#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H diff --git a/src/goto-harness/module_dependencies.txt b/src/goto-harness/module_dependencies.txt index 9507ebf6616..74032eb8b08 100644 --- a/src/goto-harness/module_dependencies.txt +++ b/src/goto-harness/module_dependencies.txt @@ -1,3 +1,6 @@ util goto-harness -goto-programs \ No newline at end of file +goto-programs +json +json-symtab-language +linking diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 432c940c448..7e6abf55afb 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -588,6 +588,28 @@ class goto_programt return t; } + optionalt get_target(const unsigned location_number) const + { + PRECONDITION(!instructions.empty()); + + const unsigned start_location_number = instructions.front().location_number; + + if( + location_number < start_location_number || + location_number > instructions.back().location_number) + { + return nullopt; + } + + auto location_target = + std::next(instructions.begin(), location_number - start_location_number); + + // location numbers are contiguous unless new instructions are inserted + // here we check that nobody inserted any instruction into our function + CHECK_RETURN(location_target->location_number == location_number); + return location_target; + } + template std::list get_successors(Target target) const; diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 3846643e780..fdd72175050 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -117,6 +117,18 @@ class symbol_tablet : public symbol_table_baset return iteratort(internal_symbols.end()); } + typedef symbolst::const_iterator const_iteratort; + + virtual const_iteratort begin() const + { + return internal_symbols.begin(); + } + + virtual const_iteratort end() const + { + return internal_symbols.end(); + } + /// Check that the symbol table is well-formed void validate(const validation_modet vm = validation_modet::INVARIANT) const;