Remove composite object from the constant propagator when a field is updated

Otherwise e.g. in "memset2" we had the whole object being initialised
with "{0, 0}" (which is stored in const prop and then expanded to
individual fields), then later any operation that needed the
whole-struct representation (such as the memset-of-one-field in that
test, which expanded to "whole_struct = byte_update(whole_struct,
offset, int, 0)") would get the whole-struct definition stored in
const-prop, disregarding any intermediate updates that were able to
directly reference a single field.

This avoids having two different versions of a symbol (the
field-of-composite and the indivisible field versions) in the most
direct way possible.

Author: smowton

src/goto-symex/field_sensitivity.cpp

@@ -167,15 +167,17 @@ exprt field_sensitivityt::get_fields(
 void field_sensitivityt::field_assignments(
   const namespacet &ns,
   goto_symex_statet &state,
-  const exprt &lhs,
-  symex_targett &target)
+  const ssa_exprt &lhs,
+  symex_targett &target,
+  bool allow_pointer_unsoundness)
 {
   exprt lhs_fs = lhs;
   apply(ns, state, lhs_fs, false);
 
   bool run_apply_bak = run_apply;
   run_apply = false;
-  field_assignments_rec(ns, state, lhs_fs, lhs, target);
+  field_assignments_rec(
+    ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
   run_apply = run_apply_bak;
 }
 
@@ -188,12 +190,14 @@ void field_sensitivityt::field_assignments(
 /// \param lhs_fs: expanded symbol
 /// \param lhs: non-expanded symbol
 /// \param target: symbolic execution equation store
+/// \param allow_pointer_unsoundness: allow pointer unsoundness
 void field_sensitivityt::field_assignments_rec(
   const namespacet &ns,
   goto_symex_statet &state,
   const exprt &lhs_fs,
   const exprt &lhs,
-  symex_targett &target)
+  symex_targett &target,
+  bool allow_pointer_unsoundness)
 {
   if(lhs == lhs_fs)
     return;
@@ -203,7 +207,8 @@ void field_sensitivityt::field_assignments_rec(
     simplify(ssa_rhs, ns);
 
     ssa_exprt ssa_lhs = to_ssa_expr(lhs_fs);
-    state.assignment(ssa_lhs, ssa_rhs, ns, true, true);
+    state.assignment(
+      ssa_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness);
 
     // do the assignment
     target.assignment(
@@ -230,7 +235,8 @@ void field_sensitivityt::field_assignments_rec(
       const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
       const exprt &member_lhs = *fs_it;
 
-      field_assignments_rec(ns, state, member_lhs, member_rhs, target);
+      field_assignments_rec(
+        ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
       ++fs_it;
     }
   }
@@ -248,7 +254,8 @@ void field_sensitivityt::field_assignments_rec(
       const index_exprt index_rhs(lhs, from_integer(i, index_type()));
       const exprt &index_lhs = *fs_it;
 
-      field_assignments_rec(ns, state, index_lhs, index_rhs, target);
+      field_assignments_rec(
+        ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
       ++fs_it;
     }
   }
@@ -261,7 +268,8 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(const exprt &op : lhs.operands())
     {
-      field_assignments_rec(ns, state, *fs_it, op, target);
+      field_assignments_rec(
+        ns, state, *fs_it, op, target, allow_pointer_unsoundness);
       ++fs_it;
     }
   }

src/goto-symex/field_sensitivity.h

@@ -27,11 +27,13 @@ class field_sensitivityt
   /// \param state: symbolic execution state
   /// \param lhs: non-expanded symbol
   /// \param target: symbolic execution equation store
+  /// \param allow_pointer_unsoundness: allow pointer unsoundness
   void field_assignments(
     const namespacet &ns,
     goto_symex_statet &state,
-    const exprt &lhs,
-    symex_targett &target);
+    const ssa_exprt &lhs,
+    symex_targett &target,
+    bool allow_pointer_unsoundness);
 
   /// Turn an expression \p expr into a field-sensitive SSA expression.
   /// Field-sensitive SSA expressions have individual symbols for each
@@ -81,7 +83,8 @@ class field_sensitivityt
     goto_symex_statet &state,
     const exprt &lhs_fs,
     const exprt &lhs,
-    symex_targett &target);
+    symex_targett &target,
+    bool allow_pointer_unsoundness);
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

src/goto-symex/goto_symex_state.cpp

@@ -170,6 +170,7 @@ void goto_symex_statet::assignment(
   {
     DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
   }
+  const ssa_exprt l1_lhs = lhs;
 
 #if 0
   PRECONDITION(l1_identifier != get_original_name(l1_identifier)
@@ -221,11 +222,23 @@ void goto_symex_statet::assignment(
     value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
   }
 
-  #if 0
+  if(field_sensitivityt::is_divisible(l1_lhs))
+  {
+    // Split composite symbol lhs into its components
+    field_sensitivity.field_assignments(
+      ns, *this, l1_lhs, *symex_target, allow_pointer_unsoundness);
+    // Erase the composite symbol from our working state. Note that we need to
+    // have it in the propagation table and the value set while doing the field
+    // assignments, thus we cannot skip putting it in there above.
+    propagation.erase(l1_identifier);
+    value_set.erase_symbol(l1_lhs, ns);
+  }
+
+#if 0
   std::cout << "Assigning " << l1_identifier << '\n';
   value_set.output(ns, std::cout);
   std::cout << "**********************\n";
-  #endif
+#endif
 }
 
 template <levelt level>

src/goto-symex/symex_assign.cpp

@@ -434,8 +434,6 @@ void goto_symext::symex_assign_symbol(
     state.source,
     assignment_type);
 
-  state.field_sensitivity.field_assignments(ns, state, lhs_mod, target);
-
   // Restore the guard
   guard.pop_back();
 }

src/pointer-analysis/value_set.cpp

@@ -1653,3 +1653,46 @@ void value_sett::erase_values_from_entry(
   }
   values.replace(index, std::move(replacement));
 }
+
+void value_sett::erase_struct_union_symbol(
+  const struct_union_typet &struct_union_type,
+  const std::string &erase_prefix,
+  const namespacet &ns)
+{
+  for(const auto &c : struct_union_type.components())
+  {
+    const typet &subtype = c.type();
+    const irep_idt &name = c.get_name();
+
+    // ignore methods and padding
+    if(subtype.id() == ID_code || c.get_is_padding())
+      continue;
+
+    erase_symbol_rec(subtype, erase_prefix + "." + id2string(name), ns);
+  }
+}
+
+void value_sett::erase_symbol_rec(
+  const typet &type,
+  const std::string &erase_prefix,
+  const namespacet &ns)
+{
+  if(type.id() == ID_struct_tag)
+    erase_struct_union_symbol(
+      ns.follow_tag(to_struct_tag_type(type)), erase_prefix, ns);
+  else if(type.id() == ID_union_tag)
+    erase_struct_union_symbol(
+      ns.follow_tag(to_union_tag_type(type)), erase_prefix, ns);
+  else if(type.id() == ID_array)
+    erase_symbol_rec(type.subtype(), erase_prefix + "[]", ns);
+  else if(values.has_key(erase_prefix))
+    values.erase(erase_prefix);
+}
+
+void value_sett::erase_symbol(
+  const symbol_exprt &symbol_expr,
+  const namespacet &ns)
+{
+  erase_symbol_rec(
+    symbol_expr.type(), id2string(symbol_expr.get_identifier()), ns);
+}

src/pointer-analysis/value_set.h

@@ -481,6 +481,8 @@ class value_sett
     const irep_idt &index,
     const std::unordered_set<exprt, irep_hash> &values_to_erase);
 
+  void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
+
 protected:
   /// Reads the set of objects pointed to by `expr`, including making
   /// recursive lookups for dereference operations etc.
@@ -515,6 +517,16 @@ class value_sett
     const exprt &src,
     exprt &dest) const;
 
+  void erase_symbol_rec(
+    const typet &type,
+    const std::string &erase_prefix,
+    const namespacet &ns);
+
+  void erase_struct_union_symbol(
+    const struct_union_typet &struct_union_type,
+    const std::string &erase_prefix,
+    const namespacet &ns);
+
   // Subclass customisation points:
 
 protected: