More constant propagation

Constant propagation now yields different right-hand sides in a test.

Author: tautschnig

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_state.cpp

@@ -153,6 +153,20 @@ class goto_symex_is_constantt : public is_constantt
       */
       return false;
     }
+    else if(expr.id() == ID_if)
+    {
+      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;
+    else if(expr.id() == ID_symbol)
+    {
+      const irep_idt &obj_identifier = to_ssa_expr(expr).get_object_name();
+      return obj_identifier == "goto_symex::\\guard";
+    }
 
     return is_constantt::is_constant(expr);
   }

src/util/expr_util.cpp

@@ -240,7 +240,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) {
@@ -275,8 +277,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;
 }