Merge pull request #1997 from tautschnig/no-sort-operands

tautschnig · web-flow · commit cf40d223cbb6 · 2021-01-28T10:42:14.000+01:00
Do not sort operands as part of simplification [blocks: #3486]
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <math.h>
+
+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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,42 +116,44 @@ 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;
 
   if(!expr.has_operands())
     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<exprt> bits2expr(
   const std::string &bits,
   const typet &type,
diff --git 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

Original file line number	Diff line number	Diff line change
`@@ -24,8 +24,10 @@ public void trimRight() {`
`24`	`24`	`}`
`25`	`25`
`26`	`26`	`public void noprop(String str) {`
`27`		`- str = str.trim();`
`28`		`- assert str.equals("abc");`
	`27`	`+ if(str != null) {`
	`28`	`+ str = str.trim();`
	`29`	`+ assert str.equals("abc");`
	`30`	`+ }`
`29`	`31`	`}`
`30`	`32`
`31`	`33`	`public void empty() {`