Constant propagation: Support non-symbol left-hand sides, soundness

1. Properly handle index, member, or dereference expressions on the left-hand
side of assignments.
2. If we find something on the left-hand side that we don't support (maybe byte
extracts, if-expressions, type casts, or maybe something else), set the entire
value set to top to ensure soundness.

Author: tautschnig

regression/goto-analyzer/constant_propagation_09/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --constants --verify
 ^EXIT=0$

regression/goto-analyzer/constant_propagation_11/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --constants --verify
 ^EXIT=0$

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --constants --verify
 ^EXIT=0$

src/analyses/constant_propagator.cpp

@@ -36,26 +36,50 @@ void constant_propagator_domaint::assign_rec(
   const namespacet &ns,
   const constant_propagator_ait *cp)
 {
-  if(lhs.id()!=ID_symbol)
-    return;
+  if(lhs.id() == ID_dereference)
+  {
+    const bool have_dirty = (cp != nullptr);
 
-  if(cp && !cp->should_track_value(lhs, ns))
-    return;
+    if(have_dirty)
+      dest_values.set_dirty_to_top(cp->dirty, ns);
+    else
+      dest_values.set_to_top();
+  }
+  else if(lhs.id() == ID_index)
+  {
+    const index_exprt &index_expr = to_index_expr(lhs);
+    with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs);
+    assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp);
+  }
+  else if(lhs.id() == ID_member)
+  {
+    const member_exprt &member_expr = to_member_expr(lhs);
+    with_exprt new_rhs(member_expr.compound(), exprt(ID_member_name), rhs);
+    new_rhs.where().set(ID_component_name, member_expr.get_component_name());
+    assign_rec(dest_values, member_expr.compound(), new_rhs, ns, cp);
+  }
+  else if(lhs.id() == ID_symbol)
+  {
+    if(cp && !cp->should_track_value(lhs, ns))
+      return;
 
-  const symbol_exprt &s=to_symbol_expr(lhs);
+    const symbol_exprt &s = to_symbol_expr(lhs);
 
-  exprt tmp=rhs;
-  partial_evaluate(dest_values, tmp, ns);
+    exprt tmp = rhs;
+    partial_evaluate(dest_values, tmp, ns);
 
-  if(dest_values.is_constant(tmp))
-  {
-    DATA_INVARIANT(
-      base_type_eq(ns.lookup(s).type, tmp.type(), ns),
-      "type of constant to be replaced should match");
-    dest_values.set_to(s, tmp);
+    if(dest_values.is_constant(tmp))
+    {
+      DATA_INVARIANT(
+        base_type_eq(ns.lookup(s).type, tmp.type(), ns),
+        "type of constant to be replaced should match");
+      dest_values.set_to(s, tmp);
+    }
+    else
+      dest_values.set_to_top(s);
   }
   else
-    dest_values.set_to_top(s);
+    dest_values.set_to_top();
 }
 
 void constant_propagator_domaint::transform(