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).

Author: tautschnig

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$

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\]

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$

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$
 --

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$

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 =

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 =

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

src/util/simplify_expr.cpp

@@ -2380,7 +2380,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);
 
@@ -2581,7 +2581,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

src/util/simplify_utils.cpp

@@ -95,7 +95,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)
 {
@@ -106,42 +106,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)
   {
@@ -159,9 +161,21 @@ 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);
+}

src/util/simplify_utils.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 bool sort_operands(exprt::operandst &operands);
 
+bool join_operands(exprt &expr);
+
 bool sort_and_join(exprt &expr);
 
 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H