diff --git a/CHANGELOG b/CHANGELOG index 4052fe87941..ba9ceda5549 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,96 @@ +5.7 +=== + +* General: All tools now support the same set of --*-check options. +* General: Added --conversion-check to catch type casts that cause loss of + information. Previously --(un)signed-overflow-check would report these. +* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible + statement- and branch coverage report. +* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static, + --java-cp-include-files, --lazy-methods. +* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options + --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops, + --continue-as-loops, --log +* GOTO-INSTRUMENT: New option --slice-global-inits +* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline, + --no-caching +* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv, + --show-threaded +* GOTO-CC: Additional drop-in replacement support for bcc, as, as86 +* GOTO-CC: GCC-style error/warning messages +* GOTO-CC: New options --native-compiler and --native-linker to select the + compiler/linker to be used when building combined native/goto object files. + + +5.6 +=== + +Bugfixes in the C, C++, Java front-ends. + + +5.5 +=== + +This is a major release, with significant changes. The option +--all-properties is now the default; to restore the previous behaviour, +use --stop-on-fail. The primary area of attention was again the Java +front-end. We have furthermore added test-suite generation for branch +coverage, location coverage, condition coverage, decision coverage and +MC/DC. + + +5.4 +=== + +This is a minor release, focused primarily on maintenance. The primary +area of attention was again the Java front-end. We have also updated to +Minisat 2.2.1. + + +5.3 +=== + +This is a minor release, focused primarily on maintenance. The primary +area of attention is the Java front-end. + + +5.2 +=== + +This is a minor release, focused primarily on maintenance. The primary +areas of attention are the full slicer, the Java frontend, test suite +generation and support for the Glucose solver. + + +5.1 +=== + +This is a minor release, focused primarily on maintenance. Support for solving +floating-point problems using for SMT-LIB2 solvers without support for the +floating-point theory has been added. + + +5.0 +=== + +This is a major release, focused primarily on performance improvements. +Furthermore, the support for the floating-point theory for SMT-LIB2 has been +improved substantially. This release breaks compatibility with the goto-binary +format used by earlier releases; i.e., you will need to rebuild your +goto-binaries. + + +4.9 +=== + +This release is primarily for maintenance purposes and does not add any major +new features. The support for SMT-LIB2 solvers has been improved substantially. + + +4.8 +=== + + 4.7 === diff --git a/COMPILING b/COMPILING index 93fc65c2938..cfbb056c2e0 100644 --- a/COMPILING +++ b/COMPILING @@ -36,7 +36,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. On Red Hat/Fedora or derivates, do - yum install gcc gcc-c++ flex bison perl-libwww-perl patch + yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 Note that you need g++ version 5.2 or newer. @@ -44,10 +44,17 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. git clone https://github.com/diffblue/cbmc cbmc-git -2) Do +2) On Debian/Ubuntu, do cd cbmc-git/src make minisat2-download + make CXX=g++-6 + + On Redhat/Fedora etc., do + + cd cbmc-git/src + make minisat2-download + scl enable devtoolset-6 bash make diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class index 09cb7711192..6895eaa962b 100644 Binary files a/regression/cbmc-java/multinewarray/multinewarray.class and b/regression/cbmc-java/multinewarray/multinewarray.class differ diff --git a/regression/cbmc-java/multinewarray/multinewarray.java b/regression/cbmc-java/multinewarray/multinewarray.java index ce3219586e4..62df1740671 100644 --- a/regression/cbmc-java/multinewarray/multinewarray.java +++ b/regression/cbmc-java/multinewarray/multinewarray.java @@ -12,8 +12,8 @@ public static void main(String[] args) assert some_a[0].length==3; assert some_a[0][0].length==2; - int x=10; - int y=20; + int x=3; + int y=5; int[][] int_array = new int[x][y]; for(int i=0; i a\[.*\]: FAILURE$ ^\[main.assertion.4\] forall c\[\]: SUCCESS$ ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$ - ^\*\* 1 of 5 failed \(2 iterations\)$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc index e38af4ddbdb..a3e1bce313f 100644 --- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc +++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc @@ -2,6 +2,5 @@ CORE main.c ^\*\* Results:$ - ^\*\* 0 of 1 failed \(1 iteration\)$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index 51feeae3b08..630e54eb224 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -8,6 +8,5 @@ main.c ^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$ ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$ ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$ - ^\*\* 0 of 6 failed \(1 iteration\)$ ^\VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index b1b6a0d1d60..2e862045758 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] failure 1: FAILURE$ ^\[main.assertion.4\] success 3: SUCCESS$ ^\[main.assertion.5\] failure 2: FAILURE$ - ^\*\* 2 of 5 failed \(2 iterations\)$ ^\VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 2874b9dc0eb..b8501be880e 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$ ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$ - ^\*\* 0 of 5 failed \(1 iteration\)$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index 3bc8a8d2a5f..b0b25cc9903 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -4,6 +4,5 @@ main.c ^\*\* Results:$ ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$ ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$ - ^\*\* 1 of 2 failed \(2 iterations\)$ ^\VERIFICATION FAILED$ diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile index 5701431a37e..2630bf17097 100644 --- a/regression/goto-analyzer/Makefile +++ b/regression/goto-analyzer/Makefile @@ -1,10 +1,16 @@ default: tests.log test: - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer + @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi tests.log: ../test.pl - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer + @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi show: @for dir in *; do \ diff --git a/regression/goto-instrument/slice22/main.c b/regression/goto-instrument/slice22/main.c new file mode 100644 index 00000000000..bac167b63d3 --- /dev/null +++ b/regression/goto-instrument/slice22/main.c @@ -0,0 +1,19 @@ +#include +#include + +int main() +{ + int *ptr=malloc(sizeof(int)); + *ptr=42; + ptr=realloc(ptr, 20); + assert(*ptr==42); + + int *ptr2=malloc(2*sizeof(int)); + *ptr2=42; + *(ptr2+1)=42; + ptr2=realloc(ptr2, 20); + assert(*ptr2==42); + assert(*(ptr2+1)==42); + + return 0; +} diff --git a/regression/goto-instrument/slice22/test.desc b/regression/goto-instrument/slice22/test.desc new file mode 100644 index 00000000000..50181efa86b --- /dev/null +++ b/regression/goto-instrument/slice22/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/goto-instrument/slice23/main.c b/regression/goto-instrument/slice23/main.c new file mode 100644 index 00000000000..d165e2c38b8 --- /dev/null +++ b/regression/goto-instrument/slice23/main.c @@ -0,0 +1,25 @@ +#include +#include + +void foo(int argc) +{ + void* x=0; + + if(argc>3) + x=malloc(4*sizeof(int)); + else + x=malloc(3*sizeof(int)); + *(int*)x=42; + + x=realloc(x, sizeof(int)); + + assert(*(int*)x==42); +} + +int main(int argc, char* argv[]) +{ +//__CPROVER_ASYNC_1: + foo(argc); + + return 0; +} diff --git a/regression/goto-instrument/slice23/test.desc b/regression/goto-instrument/slice23/test.desc new file mode 100644 index 00000000000..50181efa86b --- /dev/null +++ b/regression/goto-instrument/slice23/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/excluded-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc index 2384efe0828..7fa478ad232 100644 --- a/regression/test-script/excluded-line/test.desc +++ b/regression/test-script/excluded-line/test.desc @@ -1,5 +1,5 @@ CORE -program.c +test.txt ^Hello$ -- diff --git a/regression/test-script/excluded-line/test.txt b/regression/test-script/excluded-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/excluded-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/failing-excluded-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc index 36668db5a5f..3c8b8bc9f72 100644 --- a/regression/test-script/failing-excluded-line/test.desc +++ b/regression/test-script/failing-excluded-line/test.desc @@ -1,5 +1,5 @@ KNOWNBUG -program.c +test.txt ^Hello$ -- diff --git a/regression/test-script/failing-excluded-line/test.txt b/regression/test-script/failing-excluded-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/failing-excluded-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/failing-multi-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc index cf4fcf3034b..b3b2f171842 100644 --- a/regression/test-script/failing-multi-line/test.desc +++ b/regression/test-script/failing-multi-line/test.desc @@ -1,5 +1,5 @@ KNOWNBUG -program.c +test.txt activate-multi-line-match Hello\nAnother\nWorld diff --git a/regression/test-script/failing-multi-line/test.txt b/regression/test-script/failing-multi-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/failing-multi-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/failing-single-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc index 604682ecbdb..973b5aa464b 100644 --- a/regression/test-script/failing-single-line/test.desc +++ b/regression/test-script/failing-single-line/test.desc @@ -1,5 +1,5 @@ KNOWNBUG -program.c +test.txt ^Goodbye$ -- diff --git a/regression/test-script/failing-single-line/test.txt b/regression/test-script/failing-single-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/failing-single-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/multi-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc index cf9bb072880..2ef644c2082 100644 --- a/regression/test-script/multi-line/test.desc +++ b/regression/test-script/multi-line/test.desc @@ -1,5 +1,5 @@ CORE -program.c +test.txt activate-multi-line-match Hello\nWorld diff --git a/regression/test-script/multi-line/test.txt b/regression/test-script/multi-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/multi-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh index 8e09b75f0ab..851f1716b12 100755 --- a/regression/test-script/program_runner.sh +++ b/regression/test-script/program_runner.sh @@ -2,5 +2,4 @@ set -e -gcc $1 -o a.out -./a.out +cat $1 diff --git a/regression/test-script/single-line-windows-line-ends/test.desc b/regression/test-script/single-line-windows-line-ends/test.desc new file mode 100644 index 00000000000..d7c83bd851e --- /dev/null +++ b/regression/test-script/single-line-windows-line-ends/test.desc @@ -0,0 +1,5 @@ +CORE +test.txt + +^Hello$ +-- diff --git a/regression/test-script/single-line-windows-line-ends/test.txt b/regression/test-script/single-line-windows-line-ends/test.txt new file mode 100755 index 00000000000..7c9ae46963c --- /dev/null +++ b/regression/test-script/single-line-windows-line-ends/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c deleted file mode 100755 index 882fedcc2fd..00000000000 --- a/regression/test-script/single-line/program.c +++ /dev/null @@ -1,7 +0,0 @@ -#include - -int main(void) { - printf("Hello\n"); - printf("World\n"); - return 0; -} diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc index 2507fd6a412..d7c83bd851e 100644 --- a/regression/test-script/single-line/test.desc +++ b/regression/test-script/single-line/test.desc @@ -1,5 +1,5 @@ CORE -program.c +test.txt ^Hello$ -- diff --git a/regression/test-script/single-line/test.txt b/regression/test-script/single-line/test.txt new file mode 100755 index 00000000000..0ac4c9a8b57 --- /dev/null +++ b/regression/test-script/single-line/test.txt @@ -0,0 +1,3 @@ +Hello +World + diff --git a/regression/test.pl b/regression/test.pl index a2ac088d0e0..d27c663b0aa 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -73,7 +73,7 @@ ($$$$$) $options =~ s/$ign//g if(defined($ign)); my $output = $input; - $output =~ s/\.(c|i|gb|cpp|ii|xml|class|jar)$/.out/; + $output =~ s/\.[^.]*$/.out/; if($output eq $input) { print("Error in test file -- $test\n"); @@ -125,6 +125,7 @@ ($$$$$) local $/ = undef; binmode $fh; my $whole_file = <$fh>; + $whole_file =~ s/\r\n/\n/g; my $is_match = $whole_file =~ /$result/; $r = ($included ? !$is_match : $is_match); } @@ -132,6 +133,7 @@ ($$$$$) { my $found_line = 0; while(my $line = <$fh>) { + $line =~ s/\r$//; if($line =~ /$result/) { # We've found the line, therefore if it is included we set # the result to 0 (OK) If it is excluded, we set the result diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 4494aa33e76..7bba83bd298 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -55,6 +55,7 @@ class goto_checkt retain_trivial=_options.get_bool_option("retain-trivial"); enable_assert_to_assume=_options.get_bool_option("assert-to-assume"); enable_assertions=_options.get_bool_option("assertions"); + enable_built_in_assertions=_options.get_bool_option("built-in-assertions"); enable_assumptions=_options.get_bool_option("assumptions"); error_labels=_options.get_list_option("error-label"); } @@ -125,6 +126,7 @@ class goto_checkt bool retain_trivial; bool enable_assert_to_assume; bool enable_assertions; + bool enable_built_in_assertions; bool enable_assumptions; typedef optionst::value_listt error_labelst; @@ -1730,9 +1732,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function) } else if(i.is_assert()) { - if(i.source_location.get_bool("user-provided") && - i.source_location.get_property_class()!="error label" && - !enable_assertions) + bool is_user_provided=i.source_location.get_bool("user-provided"); + if((is_user_provided && !enable_assertions && + i.source_location.get_property_class()!="error label") || + (!is_user_provided && !enable_built_in_assertions)) i.type=SKIP; } else if(i.is_assume()) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a6975bdab19..86bd4183b91 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3337,7 +3337,7 @@ std::string expr2ct::convert_code_return( std::string dest=indent_str(indent); dest+="return"; - if(src.operands().size()==1) + if(to_code_return(src).has_return_value()) dest+=" "+convert(src.op0()); dest+=';'; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..b69ab532204 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -237,6 +237,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) else options.set_option("assertions", true); + // check built-in assertions + if(cmdline.isset("no-built-in-assertions")) + options.set_option("built-in-assertions", false); + else + options.set_option("built-in-assertions", true); + // use assumptions if(cmdline.isset("no-assumptions")) options.set_option("assumptions", false); @@ -540,19 +546,6 @@ int cbmc_parse_optionst::doit() return 0; // should contemplate EX_OK from sysexits.h } - // may replace --show-properties - if(cmdline.isset("show-reachable-properties")) - { - const namespacet ns(symbol_table); - - // Entry point will have been set before and function pointers removed - status() << "Removing Unused Functions" << eom; - remove_unused_functions(goto_functions, ui_message_handler); - - show_properties(ns, get_ui(), goto_functions); - return 0; // should contemplate EX_OK from sysexits.h - } - if(set_properties(goto_functions)) return 7; // should contemplate EX_USAGE from sysexits.h @@ -952,8 +945,14 @@ bool cbmc_parse_optionst::process_goto_program( // add loop ids goto_functions.compute_loop_numbers(); - // instrument cover goals + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing Unused Functions" << eom; + remove_unused_functions(goto_functions, ui_message_handler); + } + // instrument cover goals if(cmdline.isset("cover")) { std::list criteria_strings= @@ -1099,6 +1098,7 @@ void cbmc_parse_optionst::help() " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) " --trace give a counterexample trace for failed properties\n" //NOLINT(*) + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" @@ -1148,6 +1148,7 @@ void cbmc_parse_optionst::help() "Program instrumentation options:\n" HELP_GOTO_CHECK " --no-assertions ignore user assertions\n" + " --no-built-in-assertions ignore assertions in built-in library\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a3fc5e7e7d3..db987d3c304 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -32,6 +32,7 @@ class optionst; "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ + "(no-built-in-assertions)" \ "(xml-ui)(xml-interface)(json-ui)" \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ "(no-sat-preprocessor)" \ @@ -41,7 +42,8 @@ class optionst; "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ - "(show-claims)(claim):(show-properties)(show-reachable-properties)" \ + "(show-claims)(claim):(show-properties)" \ + "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index 8f64f9900a8..69af02e9e9e 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -318,7 +318,7 @@ void symex_coveraget::compute_overall_coverage( it!=file_records.end(); ++it) { - if(has_prefix(id2string(it->first), "first))) continue; const coverage_recordt &f_cov=it->second; diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 2988b8637d2..96b21195a82 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -44,7 +44,7 @@ static void collect_eloc( const irep_idt &file=it->source_location.get_file(); if(!file.empty() && - !has_prefix(id2string(file), "source_location.is_built_in()) files[file].insert(it->source_location.get_line()); } } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fa92bc27cc7..ede599b6d8b 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1082,9 +1082,7 @@ void instrument_cover_goals( // ignore if built-in library if(!goto_program.instructions.empty() && - has_prefix( - id2string(goto_program.instructions.front().source_location.get_file()), - "code.get_statement(); + if(statement==ID_array_copy) + return true; + if(!target->is_assign()) return false; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 615470b7f9e..8fdcd28ae07 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -851,13 +851,19 @@ void goto_convertt::do_java_new_array( goto_programt tmp; symbol_exprt tmp_i= - new_tmp_symbol(index_type(), "index", tmp, location).symbol_expr(); + new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr(); code_fort for_loop; side_effect_exprt sub_java_new=rhs; sub_java_new.operands().erase(sub_java_new.operands().begin()); + assert(rhs.type().id()==ID_pointer); + typet sub_type= + static_cast(rhs.type().subtype().find("#element_type")); + assert(sub_type.id()==ID_pointer); + sub_java_new.type()=sub_type; + side_effect_exprt inc(ID_assign); inc.operands().resize(2); inc.op0()=tmp_i; @@ -866,11 +872,21 @@ void goto_convertt::do_java_new_array( dereference_exprt deref_expr( plus_exprt(data, tmp_i), data.type().subtype()); + code_blockt for_body; + symbol_exprt init_sym= + new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr(); + + code_assignt init_subarray(init_sym, sub_java_new); + code_assignt assign_subarray( + deref_expr, + typecast_exprt(init_sym, deref_expr.type())); + for_body.move_to_operands(init_subarray); + for_body.move_to_operands(assign_subarray); + for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type())); for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0()); for_loop.iter()=inc; - for_loop.body()=code_skipt(); - for_loop.body()=code_assignt(deref_expr, sub_java_new); + for_loop.body()=for_body; convert(for_loop, tmp); dest.destructive_append(tmp); @@ -1304,7 +1320,9 @@ void goto_convertt::do_function_call_symbol( goto_programt::targett t=dest.add_instruction(ASSERT); t->guard=arguments[0]; t->source_location=function.source_location(); - t->source_location.set("user-provided", true); + t->source_location.set( + "user-provided", + !function.source_location().is_built_in()); t->source_location.set_property_class(ID_assertion); t->source_location.set_comment(description); diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 8e95a03d853..8b0bd6dc46c 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -196,7 +196,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) (it->is_goto() && it->pc->guard.is_true()) || source_location.is_nil() || source_location.get_file().empty() || - source_location.get_file()=="" || + source_location.is_built_in() || source_location.get_line().empty()) { step_to_node[it->step_nr]=sink; @@ -392,7 +392,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || (it->is_goto() && it->source.pc->guard.is_true()) || source_location.is_nil() || - source_location.get_file()=="" || + source_location.is_built_in() || source_location.get_line().empty()) { step_to_node[step_nr]=sink; diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index 5bb7320963e..a496682961e 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -19,7 +19,7 @@ class goto_modelt; "(show-goto-functions)" #define HELP_SHOW_GOTO_FUNCTIONS \ - " --show-goto-functions show goto program\n" + " --show-goto-functions show goto program\n" void show_goto_functions( const namespacet &ns, diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 0e0a6f07dad..6c30ccd09d4 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -132,6 +132,79 @@ exprt adjust_lhs_object( /*******************************************************************\ +Function: hide_dynamic_object + + Inputs: + + Outputs: + + Purpose: hide variable assignments related to dynamic_object[0-9] + and dynamic_[0-9]_array. + +\*******************************************************************/ + +void hide_dynamic_object( + const exprt &expr, + goto_trace_stept &goto_trace_step, + const namespacet &ns) +{ + if(expr.id()==ID_symbol) + { + const irep_idt &id=to_ssa_expr(expr).get_original_name(); + const symbolt *symbol; + if(!ns.lookup(id, symbol)) + { + bool result=symbol->type.get_bool("#dynamic"); + if(result) + goto_trace_step.hidden=true; + } + } + else + { + forall_operands(it, expr) + hide_dynamic_object(*it, goto_trace_step, ns); + } +} + +/*******************************************************************\ + +Function: update_fields_to_hidden + + Inputs: + + Outputs: + + Purpose: hide variables assignments related to dynamic_object + and CPROVER internal functions (e.g., __CPROVER_initialize) + +\*******************************************************************/ + +void update_fields_to_hidden( + const symex_target_equationt::SSA_stept &SSA_step, + goto_trace_stept &goto_trace_step, + const namespacet &ns) +{ + // hide dynamic_object in lhs and rhs expressions + hide_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns); + hide_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, ns); + + // hide internal CPROVER functions (e.g., __CPROVER_initialize) + if(SSA_step.is_function_call()) + { + if(SSA_step.source.pc->source_location.as_string().empty()) + goto_trace_step.hidden=true; + } + + // hide input and output steps + if(goto_trace_step.type==goto_trace_stept::OUTPUT || + goto_trace_step.type==goto_trace_stept::INPUT) + { + goto_trace_step.hidden=true; + } +} + +/*******************************************************************\ + Function: build_goto_trace Inputs: @@ -237,6 +310,9 @@ void build_goto_trace( goto_trace_step.formatted=SSA_step.formatted; goto_trace_step.identifier=SSA_step.identifier; + // hide specific variables in the counterexample trace + update_fields_to_hidden(SSA_step, goto_trace_step, ns); + goto_trace_step.assignment_type= (it->is_assignment()&& (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER || diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 088a25f7038..166be7827c9 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -25,18 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_utils.h" -/*******************************************************************\ - -Function: gen_nondet_init - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - class java_object_factoryt:public messaget { code_blockt &init_code; @@ -75,25 +63,20 @@ class java_object_factoryt:public messaget bool is_sub, irep_idt class_identifier, const source_locationt &loc, - bool skip_classid, bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet()); }; - /*******************************************************************\ -Function: gen_nondet_array_init +Function: java_object_factoryt::allocate_object - Inputs: the target expression, desired object type, source location - and Boolean whether to create a dynamic object + Inputs: - Outputs: the allocated object + Outputs: - Purpose: Returns false if we can't figure out the size of allocate_type. - allocate_type may differ from target_expr, e.g. for target_expr - having type int* and allocate_type being an int[10]. + Purpose: \*******************************************************************/ @@ -165,16 +148,33 @@ exprt java_object_factoryt::allocate_object( } } -// Override type says to ignore the LHS' real type, and init it with the given -// type regardless. Used at the moment for reference arrays, which are -// implemented as void* arrays but should be init'd as their true type with -// appropriate casts. +/*******************************************************************\ + +Function: java_object_factoryt::gen_nondet_init + + Inputs: + expr - + is_sub - + class_identifier - + loc - + create_dynamic_objects - + override - Ignore the LHS' real type. Used at the moment for + reference arrays, which are implemented as void* + arrays but should be init'd as their true type with + appropriate casts. + override_type - Type to use if ignoring the LHS' real type + + Outputs: + + Purpose: + +\*******************************************************************/ + void java_object_factoryt::gen_nondet_init( const exprt &expr, bool is_sub, irep_idt class_identifier, const source_locationt &loc, - bool skip_classid, bool create_dynamic_objects, bool override, const typet &override_type) @@ -250,20 +250,17 @@ void java_object_factoryt::gen_nondet_init( { exprt allocated= allocate_object(expr, subtype, loc, create_dynamic_objects); - { - exprt init_expr; - if(allocated.id()==ID_address_of) - init_expr=allocated.op0(); - else - init_expr=dereference_exprt(allocated, allocated.type().subtype()); - gen_nondet_init( - init_expr, - false, - "", - loc, - false, - create_dynamic_objects); - } + exprt init_expr; + if(allocated.id()==ID_address_of) + init_expr=allocated.op0(); + else + init_expr=dereference_exprt(allocated, allocated.type().subtype()); + gen_nondet_init( + init_expr, + false, + "", + loc, + create_dynamic_objects); } if(!assume_non_null) @@ -297,9 +294,6 @@ void java_object_factoryt::gen_nondet_init( if(name=="@class_identifier") { - if(skip_classid) - continue; - irep_idt qualified_clsid="java::"+as_string(class_identifier); constant_exprt ci(qualified_clsid, string_typet()); code_assignt code(me, ci); @@ -327,7 +321,6 @@ void java_object_factoryt::gen_nondet_init( _is_sub, class_identifier, loc, - false, create_dynamic_objects); } } @@ -345,7 +338,7 @@ void java_object_factoryt::gen_nondet_init( /*******************************************************************\ -Function: gen_nondet_array_init +Function: java_object_factoryt::gen_nondet_array_init Inputs: @@ -379,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init( const auto &length_sym_expr=length_sym.symbol_expr(); // Initialize array with some undetermined length: - gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false, false); + gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false); // Insert assumptions to bound its length: binary_relation_exprt @@ -464,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init( false, irep_idt(), loc, - false, true, true, element_type); @@ -479,44 +471,6 @@ void java_object_factoryt::gen_nondet_array_init( /*******************************************************************\ -Function: gen_nondet_init - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void gen_nondet_init( - const exprt &expr, - code_blockt &init_code, - symbol_tablet &symbol_table, - const source_locationt &loc, - bool skip_classid, - bool create_dyn_objs, - bool assume_non_null, - message_handlert &message_handler, - size_t max_nondet_array_length) -{ - java_object_factoryt state( - init_code, - assume_non_null, - max_nondet_array_length, - symbol_table, - message_handler); - state.gen_nondet_init( - expr, - false, - "", - loc, - skip_classid, - create_dyn_objs); -} - -/*******************************************************************\ - Function: new_tmp_symbol Inputs: @@ -592,17 +546,18 @@ exprt object_factory( exprt object=aux_symbol.symbol_expr(); - const namespacet ns(symbol_table); - gen_nondet_init( - object, + java_object_factoryt state( init_code, + !allow_null, + max_nondet_array_length, symbol_table, - loc, - false, + message_handler); + state.gen_nondet_init( + object, false, - !allow_null, - message_handler, - max_nondet_array_length); + "", + loc, + false); return object; } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 6122d3e2780..37ed40f0ec9 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -22,18 +22,6 @@ exprt object_factory( const source_locationt &, message_handlert &message_handler); -void gen_nondet_init( - const exprt &expr, - code_blockt &init_code, - symbol_tablet &symbol_table, - const source_locationt &, - bool skip_classid, - bool create_dynamic_objects, - bool assume_non_null, - message_handlert &message_handler, - size_t max_nondet_array_length=5); - - exprt get_nondet_bool(const typet &); symbolt &new_tmp_symbol( diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 125a2cae58a..55542296c48 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1729,6 +1729,9 @@ void value_set_fit::apply_code( else if(statement==ID_fence) { } + else if(statement==ID_array_copy) + { + } else if(statement==ID_input || statement==ID_output) { // doesn't do anything diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 54aa9382759..04135b96d9c 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -383,6 +384,13 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // add loop ids goto_model.goto_functions.compute_loop_numbers(); + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing Unused Functions" << eom; + remove_unused_functions(goto_model.goto_functions, ui_message_handler); + } + if(cmdline.isset("cover")) { std::string criterion=cmdline.get_value("cover"); @@ -683,6 +691,7 @@ void symex_parse_optionst::help() " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINTNEXTLINE(whitespace/line_length) " --trace give a counterexample trace for failed properties\n" + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index a67469d71e5..5e178eec14e 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -41,6 +41,7 @@ class optionst; "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(show-locs)(show-vcc)(show-properties)" \ + "(drop-unused-functions)" \ OPT_SHOW_GOTO_FUNCTIONS \ "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ "(no-simplify)(no-unwinding-assertions)(no-propagation)" diff --git a/src/util/source_location.h b/src/util/source_location.h index b24befcb8c4..b9cf434f3b0 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_SOURCE_LOCATION_H #include "irep.h" +#include "prefix.h" class source_locationt:public irept { @@ -138,6 +139,18 @@ class source_locationt:public irept return get_bool(ID_hide); } + static bool is_built_in(const std::string &s) + { + std::string built_in1=""; + std::string built_in2=""; + return has_prefix(s, built_in1) || has_prefix(s, built_in2); + } + + bool is_built_in() const + { + return is_built_in(id2string(get_file())); + } + static const source_locationt &nil() { return static_cast(get_nil_irep());