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/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$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

src/util/expr.h

@@ -9,17 +9,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_EXPR_H
 #define CPROVER_UTIL_EXPR_H
 
+#include "as_const.h"
 #include "deprecate.h"
 #include "type.h"
 #include "validate_expressions.h"
 #include "validate_types.h"
 #include "validation_mode.h"
 
-#define forall_operands(it, expr) \
-  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
-    for(exprt::operandst::const_iterator it=(expr).operands().begin(), \
-        it##_end=(expr).operands().end(); \
-        it!=it##_end; ++it)
+#define forall_operands(it, expr)                                              \
+  if(as_const(expr).has_operands())                                            \
+    for(exprt::operandst::const_iterator                                       \
+          it = as_const(expr).operands().begin(),                              \
+          it##_end = as_const(expr).operands().end();                          \
+        it != it##_end;                                                        \
+        ++it)
 
 #define Forall_operands(it, expr) \
   if((expr).has_operands()) /* NOLINT(readability/braces) */ \

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

@@ -7,7 +7,6 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "simplify_utils.h"
-#include "as_const.h"
 
 #include <algorithm>
 
@@ -95,7 +94,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 +105,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 +160,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

src/util/std_expr.h

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 /// \file util/std_expr.h
 /// API to expression classes
 
-#include "as_const.h"
 #include "expr_cast.h"
 #include "invariant.h"
 #include "narrow.h"