Do not sort operands as part of simplification

Author: tautschnig

jbmc/regression/jbmc/throwing-function-return-value/test.desc

@@ -2,7 +2,7 @@ CORE
 Test.class
 --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: 11, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

src/util/simplify_expr.cpp

@@ -2375,7 +2375,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
 
   bool result=true;
 
-  result=sort_and_join(expr) && result;
+  result = sort_and_join(expr, false) && result;
 
   if(expr.id()==ID_typecast)
     result=simplify_typecast(expr) && result;

src/util/simplify_utils.cpp

@@ -119,30 +119,31 @@ static const struct saj_tablet &sort_and_join(
   return saj_table[i];
 }
 
-bool sort_and_join(exprt &expr)
+bool sort_and_join(exprt &expr, bool do_sort)
 {
   bool result=true;
 
   if(!expr.has_operands())
     return true;
 
-  const struct saj_tablet &saj_entry=
-    sort_and_join(expr.id(), expr.type().id());
+  const exprt &expr_const = expr;
+  const struct saj_tablet &saj_entry =
+    sort_and_join(expr_const.id(), expr_const.type().id());
   if(saj_entry.id.empty())
     return true;
 
   // check operand types
 
-  forall_operands(it, expr)
+  forall_operands(it, expr_const)
     if(!sort_and_join(saj_entry, it->type().id()))
       return true;
 
   // join expressions
 
   exprt::operandst new_ops;
-  new_ops.reserve(expr.operands().size());
+  new_ops.reserve(expr_const.operands().size());
 
-  forall_operands(it, expr)
+  forall_operands(it, expr_const)
   {
     if(it->id()==expr.id())
     {
@@ -158,9 +159,11 @@ bool sort_and_join(exprt &expr)
   }
 
   // sort it
+  if(do_sort)
+    result = sort_operands(new_ops) && result;
 
-  result=sort_operands(new_ops) && result;
-  expr.operands().swap(new_ops);
+  if(!result)
+    expr.operands().swap(new_ops);
 
   return result;
 }

src/util/simplify_utils.h

@@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool sort_operands(exprt::operandst &operands);
 
-bool sort_and_join(exprt &expr);
+bool sort_and_join(exprt &expr, bool do_sort = true);
 
 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H