diff --git a/doc/architectural/goto-harness.md b/doc/architectural/goto-harness.md index dad14a5cf0f..35c496273ad 100644 --- a/doc/architectural/goto-harness.md +++ b/doc/architectural/goto-harness.md @@ -20,7 +20,7 @@ $ goto-cc program.c -o program.gb # Run goto-harness to produce harness file $ goto-harness --harness-type call-function --harness-function-name generated_harness_test_function --function test_function program.gb harness.c # Run the checks targetting the generated harness -$ cbmc --pointer-check harness.c --function generated_harness_test_function +$ cbmc --pointer-check harness.c program.c --function generated_harness_test_function ``` ## Detailed Usage @@ -32,11 +32,9 @@ without having any information about the program state. * The `memory-snapshot` harness, which loads an existing program state (in form of a JSON file) and selectively _havoc-ing_ some variables. -**NOTE**: Due to a [bug](https://github.com/diffblue/cbmc/issues/5351), the -`memory-snapshot` harness is currently inoperable. We are working to fix this. - -It is used similarly to how `goto-instrument` is used by modifying an existing -GOTO binary, as produced by `goto-cc`. +The harness generator can either produce the harness (i.e., the function +environment) as C code, or a full GOTO binary. C code is generated when the +output file name ends in ".c". ### The function call harness generator @@ -364,12 +362,6 @@ VERIFICATION SUCCESSFUL ## The memory snapshot harness -***NOTE:*** The memory snapshot harness is temporarily inoperable because of -a bug that occured when we changed the implementation of `goto-harness` to -produce C files instead of `goto` binaries. The bug is being tracked -[here](https://github.com/diffblue/cbmc/issues/5351). We are sorry for the -inconvenience, and hope to get it back to working properly soon. - The `function-call` harness is used in situations in which we want to analyze a function in an arbitrary environment. If we want to analyze a function starting from a _real_ program state, we can use the `memory-snapshot` harness instead. diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh index 84706ecb4b3..6a56a35da95 100755 --- a/regression/goto-harness/chain.sh +++ b/regression/goto-harness/chain.sh @@ -8,13 +8,20 @@ cbmc=$3 is_windows=$4 entry_point='generated_entry_function' +shift 4 name=${*:$#} name=${name%.c} -args=${*:5:$#-5} input_c_file="${name}.c" input_goto_binary="${name}.gb" -harness_c_file="${name}-harness.c" +if [[ "$1" == "harness.gb" ]]; then + harness_file=$1 + shift +else + harness_file="${name}-harness.c" +fi + +args=${*:1:$#-1} @@ -25,16 +32,24 @@ else $goto_cc -o "$input_goto_binary" "$input_c_file" fi -if [ -e "$harness_c_file" ] ; then - rm -f "$harness_c_file" +if [ -e "$harness_file" ] ; then + rm -f "$harness_file" fi # `# some comment` is an inline comment - basically, cause bash to execute an empty command $cbmc --show-goto-functions "$input_goto_binary" -$goto_harness "$input_goto_binary" "$harness_c_file" --harness-function-name $entry_point ${args} -$cbmc --show-goto-functions "$harness_c_file" -$cbmc --function $entry_point "$input_c_file" "$harness_c_file" \ +$goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entry_point ${args} +$cbmc --show-goto-functions "$harness_file" +if [[ "${harness_file}" == "harness.gb" ]];then + $cbmc --function $entry_point "$harness_file" \ + --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` \ + --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ + # cbmc args end +else +$cbmc --function $entry_point "$input_c_file" "$harness_file" \ --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` \ --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ # cbmc args end +fi diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc index 2c70d1c3d6b..d1bf5c6601a 100644 --- a/regression/goto-harness/havoc-global-int-02/test.desc +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -1,11 +1,9 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring --- -More information can be found in github#5351. diff --git a/regression/goto-harness/havoc-global-int-03/test.desc b/regression/goto-harness/havoc-global-int-03/test.desc index d85b23abccc..5c9eb104a84 100644 --- a/regression/goto-harness/havoc-global-int-03/test.desc +++ b/regression/goto-harness/havoc-global-int-03/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS @@ -8,5 +8,3 @@ main.c \[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE -- ^warning: ignoring --- -More information can be found in github#5351. diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc index 1b6d388dc80..12ebe2d7452 100644 --- a/regression/goto-harness/havoc-global-struct/test.desc +++ b/regression/goto-harness/havoc-global-struct/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$ 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 index 1443968cc38..ada15063c50 100644 --- 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 @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL 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 index ce6a542ce7d..ebe62c653c7 100644 --- a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL 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 index 7b183285859..5d8f5f01966 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc @@ -1,10 +1,8 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL -- ^warning: ignoring --- -More information can be found in github#5351. 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 index e6e4c74dbb3..50e01a8e8ca 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc @@ -1,11 +1,9 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-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 --- -More information can be found in github#5351. 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 index 7b183285859..5d8f5f01966 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc @@ -1,10 +1,8 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL -- ^warning: ignoring --- -More information can be found in github#5351. 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 index ee99f2284da..ada15063c50 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc @@ -1,10 +1,8 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL -- ^warning: ignoring --- -More information can be found in github#5351. 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 index ce6a542ce7d..ebe62c653c7 100644 --- a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 334c89e6af0..0b24f13d9ad 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -15,20 +15,21 @@ Author: Diffblue Ltd. #include #include -#include -#include -#include -#include -#include -#include -#include #include #include #include #include #include +#include #include +#include +#include +#include +#include +#include +#include + #include "function_call_harness_generator.h" #include "goto_harness_generator_factory.h" #include "memory_snapshot_harness_generator.h" @@ -145,15 +146,23 @@ int goto_harness_parse_optionst::doit() harness_generator->generate( goto_model, got_harness_config.harness_function_name); - filter_goto_model(goto_model, goto_model_without_harness_symbols); - auto harness_out = std::ofstream{got_harness_config.out_file}; - dump_c( - goto_model.goto_functions, - true, - true, - false, - namespacet{goto_model.get_symbol_table()}, - harness_out); + if(has_suffix(got_harness_config.out_file, ".c")) + { + filter_goto_model(goto_model, goto_model_without_harness_symbols); + auto harness_out = std::ofstream{got_harness_config.out_file}; + dump_c( + goto_model.goto_functions, + true, + true, + false, + namespacet{goto_model.get_symbol_table()}, + harness_out); + } + else + { + write_goto_binary( + got_harness_config.out_file, goto_model, log.get_message_handler()); + } return CPROVER_EXIT_SUCCESS; } @@ -174,8 +183,12 @@ void goto_harness_parse_optionst::help() << " goto-harness --harness-function-name --harness-type " " [harness options]\n" << "\n" - << " goto binaries to read from\n" - << " C file to write the harness to\n" + << " goto binary to read from\n" + << " file to write the harness to\n" + << " the harness is printed as C code, if " + "has a .c suffix,\n" + " else a goto binary including the harness is " + "generated\n" << "--harness-function-name the name of the harness function to " "generate\n" << "--harness-type one of the harness types listed below\n" @@ -205,9 +218,9 @@ goto_harness_parse_optionst::handle_common_options() { help(); throw invalid_command_line_argument_exceptiont{ - "need to specify both input and output goto binary file names (may be " + "need to specify both input and output file names (may be " "the same)", - " "}; + " "}; } goto_harness_config.in_file = cmdline.args[0];