Symex trace: show implicit value associated with composite declarations

Previously when a struct- or other composite-typed variable was declared, symex_decl
would initialize its individual fields, then return an L2-renamed symbol relating to
the whole object. With field-sensitivity enabled, the returned symbol is e.g. my_struct!0@1#0,
while anybody reading from it will read my_struct!0@1#1..field, a different symbol which
to the solver is unrelated. The result was that in the trace, the declaration would show
up with the value of the free symbol my_struct!0@1#0 (most likely zero, since it can't be
referred to), while the rest of the trace may make it obvious that it actually had some other
non-zero value.

With this change we expand the struct into its constituent field symbols before recording an
SSA_stept for the trace. This restores the correspondence between what the trace reads and what
code reading from the struct reads.

Author: smowton

src/goto-symex/symex_decl.cpp

@@ -54,6 +54,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   target.decl(
     state.guard.as_expr(),
     ssa,
+    state.field_sensitivity.apply(ns, state, ssa, false),
     state.source,
     hidden?
       symex_targett::assignment_typet::HIDDEN:

src/goto-symex/symex_target.h

@@ -134,6 +134,7 @@ class symex_targett
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
     assignment_typet assignment_type)=0;
 

src/goto-symex/symex_target_equation.cpp

@@ -128,6 +128,7 @@ void symex_target_equationt::assignment(
 void symex_target_equationt::decl(
   const exprt &guard,
   const ssa_exprt &ssa_lhs,
+  const exprt &initializer,
   const sourcet &source,
   assignment_typet assignment_type)
 {
@@ -138,7 +139,7 @@ void symex_target_equationt::decl(
 
   SSA_step.guard=guard;
   SSA_step.ssa_lhs=ssa_lhs;
-  SSA_step.ssa_full_lhs=ssa_lhs;
+  SSA_step.ssa_full_lhs=initializer;
   SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
   SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
 

src/goto-symex/symex_target_equation.h

@@ -73,6 +73,7 @@ class symex_target_equationt:public symex_targett
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
     assignment_typet assignment_type);