From 0662dd0ab93efbe54e1fa2eea6bfd4ceb985a810 Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Wed, 8 Mar 2017 20:26:38 +0000 Subject: [PATCH 01/21] Fix several test problems on Windows - strip from end of lines in test.pl - tests for test-script do not depend on gcc - Makefile in regression/goto-analyser has the same structure as other test Makefiles - remove tests for empty lines --- regression/cbmc/Quantifiers-assertion/test.desc | 1 - regression/cbmc/Quantifiers-assignment/test.desc | 1 - regression/cbmc/Quantifiers-copy/test.desc | 1 - regression/cbmc/Quantifiers-if/test.desc | 1 - regression/cbmc/Quantifiers-initialisation/test.desc | 1 - regression/cbmc/Quantifiers-initialisation2/test.desc | 1 - .../cbmc/Quantifiers-invalid-var-range/test.desc | 1 - regression/cbmc/Quantifiers-not-exists/test.desc | 1 - regression/cbmc/Quantifiers-not/test.desc | 1 - .../cbmc/Quantifiers-two-dimension-array/test.desc | 1 - regression/cbmc/Quantifiers-type/test.desc | 1 - regression/goto-analyzer/Makefile | 10 ++++++++-- regression/test-script/excluded-line/program.c | 7 ------- regression/test-script/excluded-line/test.desc | 2 +- regression/test-script/excluded-line/test.txt | 3 +++ regression/test-script/failing-excluded-line/program.c | 7 ------- regression/test-script/failing-excluded-line/test.desc | 2 +- regression/test-script/failing-excluded-line/test.txt | 3 +++ regression/test-script/failing-multi-line/program.c | 7 ------- regression/test-script/failing-multi-line/test.desc | 2 +- regression/test-script/failing-multi-line/test.txt | 3 +++ regression/test-script/failing-single-line/program.c | 7 ------- regression/test-script/failing-single-line/test.desc | 2 +- regression/test-script/failing-single-line/test.txt | 3 +++ regression/test-script/multi-line/program.c | 7 ------- regression/test-script/multi-line/test.desc | 2 +- regression/test-script/multi-line/test.txt | 3 +++ regression/test-script/program_runner.sh | 3 +-- .../single-line-windows-line-ends/test.desc | 5 +++++ .../test-script/single-line-windows-line-ends/test.txt | 3 +++ regression/test-script/single-line/program.c | 7 ------- regression/test-script/single-line/test.desc | 2 +- regression/test-script/single-line/test.txt | 3 +++ regression/test.pl | 4 +++- 34 files changed, 44 insertions(+), 64 deletions(-) delete mode 100755 regression/test-script/excluded-line/program.c create mode 100755 regression/test-script/excluded-line/test.txt delete mode 100755 regression/test-script/failing-excluded-line/program.c create mode 100755 regression/test-script/failing-excluded-line/test.txt delete mode 100755 regression/test-script/failing-multi-line/program.c create mode 100755 regression/test-script/failing-multi-line/test.txt delete mode 100755 regression/test-script/failing-single-line/program.c create mode 100755 regression/test-script/failing-single-line/test.txt delete mode 100755 regression/test-script/multi-line/program.c create mode 100755 regression/test-script/multi-line/test.txt create mode 100644 regression/test-script/single-line-windows-line-ends/test.desc create mode 100755 regression/test-script/single-line-windows-line-ends/test.txt delete mode 100755 regression/test-script/single-line/program.c create mode 100755 regression/test-script/single-line/test.txt diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 5b4797b9b00..555f7b0e61f 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -8,6 +8,5 @@ main.c ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$ ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$ ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$ - ^\*\* 2 of 6 failed \(2 iterations\)$ ^\VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index cfc835ce948..289e8a47efc 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -6,6 +6,5 @@ main.c ^\[main.assertion.2\] assertion y: FAILURE$ ^\[main.assertion.3\] assertion z1: SUCCESS$ ^\[main.assertion.4\] assertion z2: SUCCESS$ - ^\*\* 1 of 4 failed \(2 iterations\)$ ^\VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc index 5682d588b9c..993061a5b3a 100644 --- a/regression/cbmc/Quantifiers-copy/test.desc +++ b/regression/cbmc/Quantifiers-copy/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$ ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$ ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$ - ^\*\* 0 of 5 failed \(1 iteration\)$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index e121e2e1955..be4945b25ef 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] success 1: SUCCESS$ ^\[main.assertion.4\] failure 3: FAILURE$ ^\[main.assertion.5\] success 2: SUCCESS$ - ^\*\* 3 of 5 failed \(2 iterations\)$ ^\VERIFICATION FAILED$ diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc index b10b600c308..d0e4c279e1f 100644 --- a/regression/cbmc/Quantifiers-initialisation/test.desc +++ b/regression/cbmc/Quantifiers-initialisation/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$ ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$ ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$ - ^\*\* 0 of 5 failed \(1 iteration\)$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index ad5913e4d92..0f309d9332d 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -7,6 +7,5 @@ main.c ^\[main.assertion.3\] assertion a\[.*\] > 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/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 From 72052c7eef45dd56cd014a7c21ae4f6629b44217 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 20:49:10 +0000 Subject: [PATCH 02/21] Auxiliary function to check whether source location is in built-in --- src/util/source_location.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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()); From 32fcbbcdb95399eff80d4deeaf72992b3e9f9b14 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 21:01:02 +0000 Subject: [PATCH 03/21] Replace built-in checks by is_built_in --- src/cbmc/symex_coverage.cpp | 2 +- src/goto-instrument/count_eloc.cpp | 2 +- src/goto-instrument/cover.cpp | 4 +--- src/goto-programs/graphml_witness.cpp | 4 ++-- 4 files changed, 5 insertions(+), 7 deletions(-) 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()), - "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; From c21d3ed4426a7b5d42e9f1a37f1e29af72c62877 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 23 Mar 2017 08:50:03 +0000 Subject: [PATCH 04/21] update instructions for g++ 6 --- COMPILING | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/COMPILING b/COMPILING index 93fc65c2938..8fe38eeea7e 100644 --- a/COMPILING +++ b/COMPILING @@ -44,12 +44,18 @@ 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 + On Redhat/Fedora etc., do + + cd cbmc-git/src + make minisat2-download + make CXX=g++-6 + COMPILATION ON SOLARIS 11 ------------------------- From 903d243eac50eb8172ab4e25343f4048aa30c4b8 Mon Sep 17 00:00:00 2001 From: jgwilson42 Date: Thu, 23 Mar 2017 10:31:24 +0000 Subject: [PATCH 05/21] Updates for GCC 6 --- COMPILING | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/COMPILING b/COMPILING index 8fe38eeea7e..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. @@ -48,13 +48,14 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. cd cbmc-git/src make minisat2-download - make + make CXX=g++-6 On Redhat/Fedora etc., do cd cbmc-git/src make minisat2-download - make CXX=g++-6 + scl enable devtoolset-6 bash + make COMPILATION ON SOLARIS 11 From e843b724ec4c155e576a6551b24c0dc6e41c865e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 20 Mar 2017 16:09:49 +0000 Subject: [PATCH 06/21] Correct pretty-printing of code_returnt --- src/ansi-c/expr2c.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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+=';'; From 4473f0692f89d28fc2def116aed180c0006efbac Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 23 Mar 2017 12:36:17 +0000 Subject: [PATCH 07/21] Fix Java multinewarray Simply assigning to a temporary symbol of the correct type and amending the type passed to the elaboration of the sub-array seems to suffice to properly initialise a multi-dimensional array. --- src/goto-programs/builtin_functions.cpp | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 615470b7f9e..1f9e790b9d9 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); From 0a53fbbb74ce7dfbb8177e159dc7520906fcba0b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 23 Mar 2017 12:41:35 +0000 Subject: [PATCH 08/21] Amend test-case to complete in acceptable time --- .../cbmc-java/multinewarray/multinewarray.class | Bin 773 -> 771 bytes .../cbmc-java/multinewarray/multinewarray.java | 4 ++-- regression/cbmc-java/multinewarray/test.desc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class index 09cb7711192f8203faf62662cb4b7ed4025996ce..6895eaa962b3d52d89596646be14ff9b8bebc37e 100644 GIT binary patch delta 84 zcmZo=Yi8T9pON!B0}BH?0|P_Tdb82lIn8NwKZ8R8j47%~_{ k8A^e4HIU!PAjKdA)S=G6{)a(^oqYh~N8pONz?0}BH?0|P_L Date: Wed, 22 Mar 2017 09:54:11 +0000 Subject: [PATCH 09/21] Add --drop-unused-functions option The default behaviour of CBMC for the options --show-goto-functions, --show-properties and --cover is to consider all functions. This is particularly annoying for --cover where coverage goals are reported from functions that are trivially unreachable from the entry point. Also, --show-reachable-properties has been introduced in the past to hide such properties. We could change the default behaviour to slicing away everything that is trivially unreachable from the entry point. However, this would require an extra option to be able to view all functions and properties. This commit preserves the default behaviour and enables focussing the output of --show-goto-functions --show-properties and --cover on functions that are not trivially unreachable using --drop-unused-functions. --- src/cbmc/cbmc_parse_options.cpp | 9 ++++++++- src/cbmc/cbmc_parse_options.h | 1 + src/symex/symex_parse_options.cpp | 9 +++++++++ src/symex/symex_parse_options.h | 1 + 4 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..f5241ed48b1 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -952,8 +952,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 +1105,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" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a3fc5e7e7d3..bcc3b8ac749 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -42,6 +42,7 @@ class optionst; "(show-goto-functions)(show-loops)" \ "(show-symbol-table)(show-parse-tree)(show-vcc)" \ "(show-claims)(claim):(show-properties)(show-reachable-properties)" \ + "(drop-unused-functions)" \ "(property):(stop-on-fail)(trace)" \ "(error-label):(verbosity):(no-library)" \ "(nondet-static)" \ 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)" From a35731baa6e38343d75ece15a78acc5846e73875 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 23 Mar 2017 18:44:09 +0000 Subject: [PATCH 10/21] Remove -show-reachable-properties The same effect can now be achieved by --show-properties --drop-unused-functions --- src/cbmc/cbmc_parse_options.cpp | 13 ------------- src/cbmc/cbmc_parse_options.h | 2 +- 2 files changed, 1 insertion(+), 14 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f5241ed48b1..657e4531429 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -540,19 +540,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 diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index bcc3b8ac749..5fe9cdd9bf8 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -41,7 +41,7 @@ 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)" \ From 5e5bbca1d2f1ddf044c4e8d440bfe61ce64f864c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 10:42:04 +0000 Subject: [PATCH 11/21] Correctly align description of option --- src/goto-programs/show_goto_functions.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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, From 85a7566aa8e91be3348bc72bc800239e9dc02f99 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 22 Mar 2017 21:21:15 +0000 Subject: [PATCH 12/21] Option --no-built-in-assertions This commit changes the behahaviour of --no-assertions so that only user assertions are ignored. Built-in assertions can be hidden by the new option --no-built-in-assertions. --- src/analyses/goto_check.cpp | 9 ++++++--- src/cbmc/cbmc_parse_options.cpp | 7 +++++++ src/cbmc/cbmc_parse_options.h | 1 + src/goto-programs/builtin_functions.cpp | 4 +++- 4 files changed, 17 insertions(+), 4 deletions(-) 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/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..a8081e7c8a2 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); @@ -1148,6 +1154,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..fc2c578b69f 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)" \ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 615470b7f9e..1216f9891a9 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -1304,7 +1304,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); From 2b09c0b0b4d611937c48b00f7be74e3128dcf34d Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 11:04:21 +0000 Subject: [PATCH 13/21] Remove unused variable and braces --- src/java_bytecode/java_object_factory.cpp | 27 ++++++++++------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 088a25f7038..ea102a52996 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -250,20 +250,18 @@ 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, + false, + create_dynamic_objects); } if(!assume_non_null) @@ -592,7 +590,6 @@ exprt object_factory( exprt object=aux_symbol.symbol_expr(); - const namespacet ns(symbol_table); gen_nondet_init( object, init_code, From a3f49a341b5e43a104e74feac28c33c574f68545 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 11:19:20 +0000 Subject: [PATCH 14/21] Move function comments to the right place --- src/java_bytecode/java_object_factory.cpp | 53 ++++++++++++----------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index ea102a52996..2c22d71e4ac 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; @@ -81,19 +69,15 @@ class java_object_factoryt:public messaget 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,10 +149,29 @@ 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 - + skip_classid - + 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, @@ -343,7 +346,7 @@ void java_object_factoryt::gen_nondet_init( /*******************************************************************\ -Function: gen_nondet_array_init +Function: java_object_factoryt::gen_nondet_array_init Inputs: From 4c4ccc032919a94753e824c892155a8ca9d55f4a Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 12:04:19 +0000 Subject: [PATCH 15/21] Remove variable that is always false skip_classid was always false, so there wasn't any point having it. --- src/java_bytecode/java_object_factory.cpp | 14 +------------- src/java_bytecode/java_object_factory.h | 1 - 2 files changed, 1 insertion(+), 14 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 2c22d71e4ac..602bc4bb497 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -63,7 +63,6 @@ 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()); @@ -158,7 +157,6 @@ Function: java_object_factoryt::gen_nondet_init is_sub - class_identifier - loc - - skip_classid - create_dynamic_objects - override - Ignore the LHS' real type. Used at the moment for reference arrays, which are implemented as void* @@ -177,7 +175,6 @@ void java_object_factoryt::gen_nondet_init( bool is_sub, irep_idt class_identifier, const source_locationt &loc, - bool skip_classid, bool create_dynamic_objects, bool override, const typet &override_type) @@ -263,7 +260,6 @@ void java_object_factoryt::gen_nondet_init( false, "", loc, - false, create_dynamic_objects); } @@ -298,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); @@ -328,7 +321,6 @@ void java_object_factoryt::gen_nondet_init( _is_sub, class_identifier, loc, - false, create_dynamic_objects); } } @@ -380,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 @@ -465,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init( false, irep_idt(), loc, - false, true, true, element_type); @@ -495,7 +486,6 @@ void gen_nondet_init( 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, @@ -512,7 +502,6 @@ void gen_nondet_init( false, "", loc, - skip_classid, create_dyn_objs); } @@ -599,7 +588,6 @@ exprt object_factory( symbol_table, loc, false, - false, !allow_null, message_handler, max_nondet_array_length); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 6122d3e2780..5141ca45f42 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -27,7 +27,6 @@ void gen_nondet_init( 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, From 9a1dae0323dad1f71ca7a946e4ee8c41596982b6 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 15:05:50 +0000 Subject: [PATCH 16/21] Remove function that's only used once gen_nondet_init() is only used once, and is only two lines long, so get rid of it and just put those two lines. This also avoids confusion with java_object_factory::gen_nondet_init(). --- src/java_bytecode/java_object_factory.cpp | 51 ++++------------------- src/java_bytecode/java_object_factory.h | 11 ----- 2 files changed, 9 insertions(+), 53 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 602bc4bb497..166be7827c9 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -471,42 +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 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, - create_dyn_objs); -} - -/*******************************************************************\ - Function: new_tmp_symbol Inputs: @@ -582,15 +546,18 @@ exprt object_factory( exprt object=aux_symbol.symbol_expr(); - gen_nondet_init( - object, + java_object_factoryt state( init_code, + !allow_null, + max_nondet_array_length, symbol_table, - loc, + 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 5141ca45f42..37ed40f0ec9 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -22,17 +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 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( From 27227ccd96e9318c0b35f5c3049a7f75f6db2096 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 24 Mar 2017 12:58:06 +0000 Subject: [PATCH 17/21] added support for array_copy in the full-slice option Do not slice away array_copy expressions during the implicit call in the full-slicert class. We do not process array_copy in value_set_fit. --- src/goto-instrument/full_slicer.cpp | 4 ++++ src/pointer-analysis/value_set_fi.cpp | 3 +++ 2 files changed, 7 insertions(+) diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 59bda7f0af0..f7b42a0af3c 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -337,6 +337,10 @@ static bool implicit(goto_programt::const_targett target) { // some variables are used during symbolic execution only + const irep_idt &statement=target->code.get_statement(); + if(statement==ID_array_copy) + return true; + if(!target->is_assign()) return false; 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 From e70aa7d261f3b721d1844c5f4f498bb82b59ebc3 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Fri, 24 Mar 2017 12:55:12 +0000 Subject: [PATCH 18/21] added two test cases into goto-instrument regression for checking array_copy added two test cases related to array copy in the goto-instrument regression suite to further test the full-slice option --- regression/goto-instrument/slice22/main.c | 19 +++++++++++++++ regression/goto-instrument/slice22/test.desc | 6 +++++ regression/goto-instrument/slice23/main.c | 25 ++++++++++++++++++++ regression/goto-instrument/slice23/test.desc | 6 +++++ 4 files changed, 56 insertions(+) create mode 100644 regression/goto-instrument/slice22/main.c create mode 100644 regression/goto-instrument/slice22/test.desc create mode 100644 regression/goto-instrument/slice23/main.c create mode 100644 regression/goto-instrument/slice23/test.desc 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$ From 83874c3624713ad5babd2238e06f9b7ada52864b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Mar 2017 19:16:52 +0000 Subject: [PATCH 19/21] Release notes up to 5.6 from CProver Google group messages --- CHANGELOG | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/CHANGELOG b/CHANGELOG index 4052fe87941..d0f6a04a558 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,72 @@ +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 === From 81470f46b6aa1dd9e82b40226b44e3484db62968 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Mar 2017 19:19:36 +0000 Subject: [PATCH 20/21] Initial version of release notes for 5.7 --- CHANGELOG | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/CHANGELOG b/CHANGELOG index d0f6a04a558..ba9ceda5549 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,27 @@ +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 === From 0feaaefa26034f4f80622b729834fc034f3b84c1 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 6 Mar 2017 09:46:38 +0000 Subject: [PATCH 21/21] hide specific variables in the counterexample trace for test-gen-support hide variable assignments related to dynamic_object[0-9], dynamic_[0-9]_array, and CPROVER internal functions (e.g., __CPROVER_initialize). This PR is related to test-gen-support issue #20 --- src/goto-symex/build_goto_trace.cpp | 76 +++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) 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 ||