diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class index 5c80d03b77f..2810fb6a468 100644 Binary files a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class and b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class differ 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$ 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/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/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_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()); 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