More constant propagation

1) Within goto-symex, propagation of nondet_symbol_exprt is actually safe, as
they are instantiations of side_effect_expr_nondett and the value of these
instantiations cannot change.
2) This highlights that we also need to consider further expressions as possibly
being constant in is_constantt which we would otherwise simplify away when they
are constant (but cannot any longer do so when nondet_symbol_exprt are contained
in there).
3) Constant propagation now yields different right-hand sides in a test, and
makes another test trivial.
4) goto-symex applies filters on what is considered "constant" to keep the size
of expressions contained as (repeated) simplification of large expressions is
expensive. We may revisit this in future as we improve the simplifier.

Author: tautschnig

jbmc/regression/jbmc-strings/ClassName/test.desc

@@ -4,5 +4,3 @@ test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[java::test\.main:\(\)V\.assertion\.1\] line 5 assertion at file test\.java line 5 function java::test\.main:\(\)V bytecode-index 8: SUCCESS$
-\[java::test\.main:\(\)V\.assertion\.2\] line 6 assertion at file test\.java line 6 function java::test\.main:\(\)V bytecode-index 19: SUCCESS$

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test.class
 --function Test.checkAbort --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object[0-9]*=.*\?.*
 --
 --
 This tests that the object does not appear in the trace, because concretizing

regression/cbmc/constant_folding3/main.c

@@ -0,0 +1,18 @@
+typedef struct _pair
+{
+  int x;
+  int y;
+} pair;
+
+int __VERIFIER_nondet_int();
+
+int main(void)
+{
+  pair p1 = {.x = 0, .y = __VERIFIER_nondet_int()};
+  pair p2 = {};
+  p2.x = __VERIFIER_nondet_int();
+
+  __CPROVER_assert(p1.x == p2.y, "true by constant propagation");
+
+  return 0;
+}

regression/cbmc/constant_folding3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring

src/goto-symex/goto_symex_is_constant.h

@@ -45,6 +45,20 @@ class goto_symex_is_constantt : public is_constantt
       */
       return false;
     }
+    else if(expr.id() == ID_if)
+    {
+      // don't treat nested if_exprt as constant (even when they are!) as this
+      // may give rise to large expressions that we repeatedly pass to the
+      // simplifier; this is observable on regression/cbmc-library/memmove-01
+      const if_exprt &if_expr = to_if_expr(expr);
+      if(
+        if_expr.true_case().id() == ID_if || if_expr.false_case().id() == ID_if)
+      {
+        return false;
+      }
+    }
+    else if(expr.id() == ID_nondet_symbol)
+      return true;
 
     return is_constantt::is_constant(expr);
   }

src/util/expr_util.cpp

@@ -241,7 +241,9 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
     // byte_update works, byte_extract may be out-of-bounds
     expr.id() == ID_byte_update_big_endian ||
-    expr.id() == ID_byte_update_little_endian)
+    expr.id() == ID_byte_update_little_endian ||
+    // member works, index may be out-of-bounds
+    expr.id() == ID_member || expr.id() == ID_if)
   {
     return std::all_of(
       expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
@@ -276,8 +278,12 @@ bool is_constantt::is_constant_address_of(const exprt &expr) const
 
     return is_constant(deref.pointer());
   }
-  else if(expr.id() == ID_string_constant)
+  else if(
+    expr.id() == ID_string_constant || expr.id() == ID_array ||
+    expr.id() == ID_struct || expr.id() == ID_union)
+  {
     return true;
+  }
 
   return false;
 }