Constant propagation of nondet-symbol [blocks: #35]

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

jbmc/regression/jbmc-strings/nondet_propagation/Test.java

@@ -0,0 +1,8 @@
+public class Test {
+  public String foo() {
+    final int i = 10;
+    final String retval = Integer.toHexString(i);
+    assert(false);
+    return retval;
+  }
+}

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

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.foo --trace
+^EXIT=10$
+^SIGNAL=0$
+dynamic_object1=\{ 'a' \}
+--
+--
+Nondet propagation would previously cause an output like
+dynamic_object1=dynamic_object1#2, because the mapping between dynamic_object1#2
+and a nondet-symbol, which was otherwise being used by the string solver, was
+not established.

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/solvers/flattening/arrays.cpp

@@ -67,9 +67,20 @@ literalt arrayst::record_array_equality(
   collect_arrays(op0);
   collect_arrays(op1);
 
+  lhs_rhs_map.emplace(op0, op1);
+
   return array_equalities.back().l;
 }
 
+exprt arrayst::get(const exprt &expr) const
+{
+  auto it = lhs_rhs_map.find(expr);
+  if(it != lhs_rhs_map.end() && it->first != it->second)
+    return get(it->second);
+  else
+    return SUB::get(expr);
+}
+
 void arrayst::collect_indices()
 {
   for(std::size_t i=0; i<arrays.size(); i++)

src/solvers/flattening/arrays.h

@@ -46,6 +46,8 @@ class arrayst:public equalityt
   literalt record_array_equality(const equal_exprt &expr);
   void record_array_index(const index_exprt &expr);
 
+  exprt get(const exprt &expr) const override;
+
 protected:
   const namespacet &ns;
 
@@ -65,6 +67,7 @@ class arrayst:public equalityt
   // elements are added while references are held
   typedef std::list<array_equalityt> array_equalitiest;
   array_equalitiest array_equalities;
+  std::unordered_map<exprt, exprt, irep_hash> lhs_rhs_map;
 
   // this is used to find the clusters of arrays being compared
   union_find<exprt> arrays;

src/solvers/strings/string_refinement.cpp

@@ -977,6 +977,8 @@ static optionalt<exprt> get_array(
 {
   const exprt &size = arr.length();
   exprt arr_val = simplify_expr(adjust_if_recursive(super_get(arr), ns), ns);
+  if(arr_val.id() == ID_array)
+    return std::move(arr_val);
   exprt size_val = super_get(size);
   size_val = simplify_expr(size_val, ns);
   const typet char_type = arr.type().subtype();

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;
 }