From 62df88030cc4c907a6d07dcaf69cea2200a78c74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 Jan 2021 21:53:23 +0000 Subject: [PATCH 1/3] jbmc-strings/ConstantEvaluationTrim: avoid null dereference String refinement may or may not be successful (resulting in "ERROR" results rather than "FAILURE") when working on an unconstrained string (which the null dereference yields), depending on the models returned by the SAT solver. --- .../ConstantEvaluationTrim/Main.class | Bin 1578 -> 1583 bytes .../ConstantEvaluationTrim/Main.java | 6 ++++-- .../ConstantEvaluationTrim/noprop.desc | 2 ++ 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class index 5c80d03b77f85ebd481d8cd2d47af4d83cbc52fe..2810fb6a468f3830a4e1bea1ea64afc86bc5b298 100644 GIT binary patch delta 231 zcmWm7yG{a86oujc3HRE9Ajz9<7wJ%Ek zJxDeRgnDV&qD+Z`whX51XW_u^kYiWFp8pI-c3*X%s`z4dWD`|g)$lV_OVw6&{7?4& EAAC6>{{R30 delta 215 zcmWm2y=nqM7=__?bl2Hg1|g^*xltv5556lltM<&NIcT#H(wwrl!J(-rkZvD=Cg(NJ{be*M=o1)?9% diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java index 922bb6da298..2a5e4c7371a 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java @@ -24,8 +24,10 @@ public void trimRight() { } public void noprop(String str) { - str = str.trim(); - assert str.equals("abc"); + if(str != null) { + str = str.trim(); + assert str.equals("abc"); + } } public void empty() { diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc index bdddbfaed8f..50cb86ad126 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc @@ -2,6 +2,8 @@ CORE Main --function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +line 29 assertion at file Main.java line 29 .*: FAILURE$ +^\*\* 1 of \d+ failed ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From 9e5434b583e9aa67fb39e7e8c29939e089ad8134 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 Nov 2020 13:29:26 +0000 Subject: [PATCH 2/3] Do not sort operands as part of simplification Data for ReachSafety-BitVectors, the smallest of SV-COMP's categories, running for at most 600s per benchmark: 163M sort_operands calls, contributing to 1B irept::operator< calls, resulting in 4.5B irept::compare calls. None of these calls are actually necessary. As part of this work, also clean up naming of "sort_and_join" functions (as most of them don't actually sort or join, but instead just prepare for doing so). --- .../throwing-function-return-value/test.desc | 2 +- .../cbmc-library/float-nan-check/test.desc | 27 ++++++------- .../cbmc/array-cell-sensitivity2/test.desc | 2 +- regression/cbmc/field-sensitivity1/test.desc | 2 +- regression/cbmc/field-sensitivity11/test.desc | 2 +- regression/cbmc/field-sensitivity12/test.desc | 2 +- regression/cbmc/field-sensitivity13/test.desc | 2 +- .../constant_propagation_07/test.desc | 4 +- src/util/simplify_expr.cpp | 4 +- src/util/simplify_utils.cpp | 38 +++++++++++++------ src/util/simplify_utils.h | 2 + 11 files changed, 52 insertions(+), 35 deletions(-) diff --git a/jbmc/regression/jbmc/throwing-function-return-value/test.desc b/jbmc/regression/jbmc/throwing-function-return-value/test.desc index bc00301fca1..8ce2dcd6bb2 100644 --- a/jbmc/regression/jbmc/throwing-function-return-value/test.desc +++ b/jbmc/regression/jbmc/throwing-function-return-value/test.desc @@ -2,7 +2,7 @@ CORE Test --function Test.main --show-vcc java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\) -java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+ +java::Test\.main:\(Z\)V::9::x!0@1#\d+ = java::Test\.main:\(Z\)V::9::x!0@1#\d+ \+ 5 java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/float-nan-check/test.desc b/regression/cbmc-library/float-nan-check/test.desc index f90dd750bf5..4217f58c852 100644 --- a/regression/cbmc-library/float-nan-check/test.desc +++ b/regression/cbmc-library/float-nan-check/test.desc @@ -6,20 +6,21 @@ main.c \[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE \[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE -\[main.NaN.6\] line \d+ NaN on - in myinf - myinf: FAILURE -\[main.NaN.7\] line \d+ NaN on - in -myinf - -myinf: FAILURE -\[main.NaN.8\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS -\[main.NaN.9\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS -\[main.NaN.10\] line \d+ NaN on \* in mynan \* mynan: SUCCESS -\[main.NaN.11\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS -\[main.NaN.12\] line \d+ NaN on - in mynan - mynan: SUCCESS -\[main.NaN.13\] line \d+ NaN on / in mynan / mynan: SUCCESS -\[main.NaN.14\] line \d+ NaN on \+ in mynan \+ \(float\)n: SUCCESS -\[main.NaN.15\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS -\[main.NaN.16\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS -\[main.NaN.17\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS +\[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE +\[main.NaN.7\] line \d+ NaN on - in myinf - myinf: FAILURE +\[main.NaN.8\] line \d+ NaN on - in -myinf - -myinf: FAILURE +\[main.NaN.9\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS +\[main.NaN.10\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS +\[main.NaN.11\] line \d+ NaN on \* in mynan \* mynan: SUCCESS +\[main.NaN.12\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS +\[main.NaN.13\] line \d+ NaN on - in mynan - mynan: SUCCESS +\[main.NaN.14\] line \d+ NaN on / in mynan / mynan: SUCCESS +\[main.NaN.15\] line \d+ NaN on \+ in mynan \+ \(float\)n: SUCCESS +\[main.NaN.16\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS +\[main.NaN.17\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS +\[main.NaN.18\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -\[main.NaN.18\] +\[main.NaN.19\] diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc index 92a0b40af63..65b734796e9 100644 --- a/regression/cbmc/array-cell-sensitivity2/test.desc +++ b/regression/cbmc/array-cell-sensitivity2/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-vcc -main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(-1 \+ main::argc!0@1#1, signedbv\[64\]\), 1\) +main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\), 1\) main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\) ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/field-sensitivity1/test.desc b/regression/cbmc/field-sensitivity1/test.desc index 1f475162f69..b341617e533 100644 --- a/regression/cbmc/field-sensitivity1/test.desc +++ b/regression/cbmc/field-sensitivity1/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-vcc main::1::a!0@1#2\.\.x = main::argc!0@1#1 -main::1::a!0@1#2\.\.y = 1 \+ main::argc!0@1#1 +main::1::a!0@1#2\.\.y = main::argc!0@1#1 \+ 1 ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/field-sensitivity11/test.desc b/regression/cbmc/field-sensitivity11/test.desc index ece83e62801..b92bd687845 100644 --- a/regression/cbmc/field-sensitivity11/test.desc +++ b/regression/cbmc/field-sensitivity11/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-vcc main::1::a1!0@1#2\.\.x = main::argc!0@1#1 -main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1 +main::1::a1!0@1#2\.\.y = main::argc!0@1#1 \+ 1 main::1::a2!0@1#2\.\.x = main::1::a1!0@1#2\.\.x main::1::a2!0@1#2\.\.y = main::1::a1!0@1#2\.\.y ^EXIT=0$ diff --git a/regression/cbmc/field-sensitivity12/test.desc b/regression/cbmc/field-sensitivity12/test.desc index 357b6b7df6c..077f112784c 100644 --- a/regression/cbmc/field-sensitivity12/test.desc +++ b/regression/cbmc/field-sensitivity12/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-vcc main::1::a1!0@1#2\.\.x = main::argc!0@1#1 -main::1::a1!0@1#2\.\.y = 1 \+ main::argc!0@1#1 +main::1::a1!0@1#2\.\.y = main::argc!0@1#1 \+ 1 main::1::a1!0@1#3\.\.x = main::1::a1!0@1#2\.\.x main::1::a1!0@1#3\.\.y = main::1::a1!0@1#2\.\.y main::1::a2!0@1#2\.\.x = diff --git a/regression/cbmc/field-sensitivity13/test.desc b/regression/cbmc/field-sensitivity13/test.desc index 4b3898ea24a..6b069745129 100644 --- a/regression/cbmc/field-sensitivity13/test.desc +++ b/regression/cbmc/field-sensitivity13/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-vcc main::1::b1!0@1#2\.\.a\.\.x = main::argc!0@1#1 -main::1::b1!0@1#2\.\.a\.\.y = 1 \+ main::argc!0@1#1 +main::1::b1!0@1#2\.\.a\.\.y = main::argc!0@1#1 \+ 1 main::1::b1!0@1#3\.\.a\.\.x = main::1::b1!0@1#2\.\.a\.\.x main::1::b1!0@1#3\.\.a\.\.y = main::1::b1!0@1#2\.\.a\.\.y main::1::b2!0@1#2\.\.a\.\.x = diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 71416697fd4..5c4fd2f28e7 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 18, function calls: 2$ -- ^warning: ignoring diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 608f0592b9b..dbb4ec89d49 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2090,7 +2090,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) #endif exprt expr = node; - bool no_change_sort_and_join = sort_and_join(expr); + bool no_change_join_operands = join_operands(expr); resultt<> r = unchanged(expr); @@ -2291,7 +2291,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) r = simplify_complex(to_unary_expr(expr)); } - if(!no_change_sort_and_join) + if(!no_change_join_operands) r = changed(r); #ifdef DEBUGX diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 9ed4c4d3a25..74d618c32de 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -105,7 +105,7 @@ struct saj_tablet { irep_idt(), { irep_idt() }} }; -static bool sort_and_join( +static bool is_associative_and_commutative_for_type( const struct saj_tablet &saj_entry, const irep_idt &type_id) { @@ -116,21 +116,23 @@ static bool sort_and_join( return false; } -static const struct saj_tablet &sort_and_join( - const irep_idt &id, - const irep_idt &type_id) +static const struct saj_tablet & +get_sort_and_join_table_entry(const irep_idt &id, const irep_idt &type_id) { unsigned i=0; for( ; !saj_table[i].id.empty(); i++) - if(id==saj_table[i].id && - sort_and_join(saj_table[i], type_id)) + { + if( + id == saj_table[i].id && + is_associative_and_commutative_for_type(saj_table[i], type_id)) return saj_table[i]; + } return saj_table[i]; } -bool sort_and_join(exprt &expr) +static bool sort_and_join(exprt &expr, bool do_sort) { bool no_change = true; @@ -138,20 +140,20 @@ bool sort_and_join(exprt &expr) return true; const struct saj_tablet &saj_entry = - sort_and_join(expr.id(), as_const(expr).type().id()); + get_sort_and_join_table_entry(expr.id(), as_const(expr).type().id()); if(saj_entry.id.empty()) return true; // check operand types forall_operands(it, expr) - if(!sort_and_join(saj_entry, it->type().id())) + if(!is_associative_and_commutative_for_type(saj_entry, it->type().id())) return true; // join expressions exprt::operandst new_ops; - new_ops.reserve(expr.operands().size()); + new_ops.reserve(as_const(expr).operands().size()); forall_operands(it, expr) { @@ -169,13 +171,25 @@ bool sort_and_join(exprt &expr) } // sort it + if(do_sort) + no_change = sort_operands(new_ops) && no_change; - no_change = sort_operands(new_ops) && no_change; - expr.operands().swap(new_ops); + if(!no_change) + expr.operands().swap(new_ops); return no_change; } +bool sort_and_join(exprt &expr) +{ + return sort_and_join(expr, true); +} + +bool join_operands(exprt &expr) +{ + return sort_and_join(expr, false); +} + optionalt bits2expr( const std::string &bits, const typet &type, diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h index a0ad7abc57d..c65011a2129 100644 --- a/src/util/simplify_utils.h +++ b/src/util/simplify_utils.h @@ -20,6 +20,8 @@ class namespacet; bool sort_operands(exprt::operandst &operands); +bool join_operands(exprt &expr); + bool sort_and_join(exprt &expr); // bit-level conversions From 375f20857e5e43c4e7e324070ac62ce701a7277d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 Jan 2021 22:28:38 +0000 Subject: [PATCH 3/3] Simplify: sort operands for commutative, but not associative operations Testing floating-point equality is expensive, and thus warrants handling special cases (even if they might be rare) in the simplifier. This (simplistic) test would take 5 seconds with CaDiCaL as SAT back-end when not performing simplification. --- regression/cbmc/Float-equality2/main.c | 13 +++++++++++++ regression/cbmc/Float-equality2/test.desc | 11 +++++++++++ src/util/simplify_expr_floatbv.cpp | 11 ++++++++++- 3 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/Float-equality2/main.c create mode 100644 regression/cbmc/Float-equality2/test.desc diff --git a/regression/cbmc/Float-equality2/main.c b/regression/cbmc/Float-equality2/main.c new file mode 100644 index 00000000000..3cd42cd8a3f --- /dev/null +++ b/regression/cbmc/Float-equality2/main.c @@ -0,0 +1,13 @@ +#include +#include + +int main() +{ + float a; + float b; + // We could do "if (isnormal(a) && isnormal(b))", but __CPROVER_isnanf(a+b) + // will permit solving this entirely via the simplifier, if, and only if, the + // equality is successfully simplified (despite the different order of + // operands). + assert(__CPROVER_isnanf(a + b) || a + b == b + a); +} diff --git a/regression/cbmc/Float-equality2/test.desc b/regression/cbmc/Float-equality2/test.desc new file mode 100644 index 00000000000..17fba7951a0 --- /dev/null +++ b/regression/cbmc/Float-equality2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$) +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This requires simplification of commutative, but not associative operations. diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index fbbb796b2ed..394ad55a58a 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "namespace.h" #include "simplify_expr.h" +#include "simplify_utils.h" #include "std_expr.h" simplify_exprt::resultt<> @@ -361,7 +362,15 @@ simplify_exprt::simplify_ieee_float_relation(const binary_relation_exprt &expr) UNREACHABLE; } - if(expr.lhs() == expr.rhs()) + // addition and multiplication are commutative, but not associative + exprt lhs_sorted = expr.lhs(); + if(lhs_sorted.id() == ID_floatbv_plus || lhs_sorted.id() == ID_floatbv_mult) + sort_operands(lhs_sorted.operands()); + exprt rhs_sorted = expr.rhs(); + if(rhs_sorted.id() == ID_floatbv_plus || rhs_sorted.id() == ID_floatbv_mult) + sort_operands(rhs_sorted.operands()); + + if(lhs_sorted == rhs_sorted) { // x!=x is the same as saying isnan(op) exprt isnan = isnan_exprt(expr.lhs());