remove lhs_object from goto_trace_stept

Rationale:
 * lhs_object_value may be extremely large (think of large struct or array), but the information is contained in (more compact form) full_lhs_value.
 * lhs_object is contained in full_lhs. A helper function is provided to extract it.

Author: kroening

src/goto-programs/goto_trace.cpp

@@ -24,6 +24,25 @@ Author: Daniel Kroening
 
 #include "printf_formatter.h"
 
+static optionalt<symbol_exprt> get_object_rec(const exprt &src)
+{
+  if(src.id()==ID_symbol)
+    return to_symbol_expr(src);
+  else if(src.id()==ID_member)
+    return get_object_rec(to_member_expr(src).struct_op());
+  else if(src.id()==ID_index)
+    return get_object_rec(to_index_expr(src).array());
+  else if(src.id()==ID_typecast)
+    return get_object_rec(to_typecast_expr(src).op());
+  else
+    return {}; // give up
+}
+
+optionalt<symbol_exprt> goto_trace_stept::get_lhs_object() const
+{
+  return get_object_rec(full_lhs);
+}
+
 void goto_tracet::output(
   const class namespacet &ns,
   std::ostream &out) const
@@ -217,15 +236,15 @@ std::string trace_numeric_value(
 void trace_value(
   std::ostream &out,
   const namespacet &ns,
-  const ssa_exprt &lhs_object,
+  const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,
   const exprt &value,
   const trace_optionst &options)
 {
   irep_idt identifier;
 
-  if(lhs_object.is_not_nil())
-    identifier=lhs_object.get_object_name();
+  if(lhs_object.has_value())
+    identifier=lhs_object->get_identifier();
 
   std::string value_string;
 
@@ -346,7 +365,7 @@ void show_full_goto_trace(
       if(step.pc->is_assign() ||
          step.pc->is_return() || // returns have a lhs!
          step.pc->is_function_call() ||
-         (step.pc->is_other() && step.lhs_object.is_not_nil()))
+         (step.pc->is_other() && step.full_lhs.is_not_nil()))
       {
         if(prev_step_nr!=step.step_nr || first_step)
         {
@@ -356,23 +375,13 @@ void show_full_goto_trace(
             out, ns, step, step.pc->source_location, step.step_nr, options);
         }
 
-        // see if the full lhs is something clean
-        if(is_index_member_symbol(step.full_lhs))
-          trace_value(
-            out,
-            ns,
-            step.lhs_object,
-            step.full_lhs,
-            step.full_lhs_value,
-            options);
-        else
-          trace_value(
-            out,
-            ns,
-            step.lhs_object,
-            step.lhs_object,
-            step.lhs_object_value,
-            options);
+       trace_value(
+         out,
+         ns,
+         step.get_lhs_object(),
+         step.full_lhs,
+         step.full_lhs_value,
+         options);
       }
       break;
 
@@ -386,7 +395,7 @@ void show_full_goto_trace(
       }
 
       trace_value(
-        out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
+        out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
       break;
 
     case goto_trace_stept::typet::OUTPUT:

src/goto-programs/goto_trace.h

@@ -104,14 +104,14 @@ class goto_trace_stept
   // for assert
   std::string comment;
 
-  // the object being assigned
-  ssa_exprt lhs_object;
-
-  // the full, original lhs expression
+  // the full, original lhs expression, after dereferencing
   exprt full_lhs;
 
-  // A constant with the new value
-  exprt lhs_object_value, full_lhs_value;
+  // the object being assigned
+  optionalt<symbol_exprt> get_lhs_object() const;
+
+  // A constant with the new value of the lhs
+  exprt full_lhs_value;
 
   // for INPUT/OUTPUT
   irep_idt format_string, io_id;
@@ -141,8 +141,6 @@ class goto_trace_stept
     cond_value(false),
     formatted(false)
   {
-    lhs_object.make_nil();
-    lhs_object_value.make_nil();
     full_lhs.make_nil();
     full_lhs_value.make_nil();
     cond_expr.make_nil();
@@ -245,9 +243,10 @@ void show_goto_trace(
 void trace_value(
   std::ostream &out,
   const namespacet &,
-  const ssa_exprt &lhs_object,
+  const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,
-  const exprt &value);
+  const exprt &value,
+  const trace_optionst &);
 
 #define OPT_GOTO_TRACE                                                         \
   "(trace-json-extended)"                                                      \

src/goto-programs/graphml_witness.cpp

@@ -278,24 +278,17 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         }
 
         if(it->type==goto_trace_stept::typet::ASSIGNMENT &&
-           it->lhs_object_value.is_not_nil() &&
+           it->full_lhs_value.is_not_nil() &&
            it->full_lhs.is_not_nil())
         {
-          if(!it->lhs_object_value.is_constant() ||
-             !it->lhs_object_value.has_operands() ||
-             !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)),
-                         "INVALID-"))
-          {
-            xmlt &val=edge.new_element("data");
-            val.set_attribute("key", "assumption");
-            code_assignt assign(it->lhs_object, it->lhs_object_value);
-            irep_idt identifier=it->lhs_object.get_identifier();
-            val.data=convert_assign_rec(identifier, assign);
-
-            xmlt &val_s=edge.new_element("data");
-            val_s.set_attribute("key", "assumption.scope");
-            val_s.data=id2string(it->pc->source_location.get_function());
-          }
+          xmlt &val=edge.new_element("data");
+          val.set_attribute("key", "assumption");
+          val.data=from_expr(ns, it->pc->function, it->full_lhs)+" = "+
+                   from_expr(ns, it->pc->function, it->full_lhs_value)+";";
+
+          xmlt &val_s=edge.new_element("data");
+          val_s.set_attribute("key", "assumption.scope");
+          val_s.data=id2string(it->pc->source_location.get_function());
         }
         else if(it->type==goto_trace_stept::typet::GOTO &&
                 it->pc->is_goto())

src/goto-programs/interpreter.cpp

@@ -677,15 +677,7 @@ void interpretert::execute_assign()
       goto_trace_stept &trace_step=steps.get_last_step();
       assign(address, rhs);
       trace_step.full_lhs=code_assign.lhs();
-
-      // TODO: need to look at other cases on ssa_exprt
-      // (dereference should be handled on ssa)
-      if(ssa_exprt::can_build_identifier(trace_step.full_lhs))
-      {
-        trace_step.lhs_object=ssa_exprt(trace_step.full_lhs);
-      }
       trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
-      trace_step.lhs_object_value=trace_step.full_lhs_value;
     }
   }
   else if(code_assign.rhs().id()==ID_side_effect)

src/goto-programs/json_goto_trace.cpp

@@ -77,7 +77,10 @@ void convert_decl(
   const jsont &json_location = conversion_dependencies.location;
   const namespacet &ns = conversion_dependencies.ns;
 
-  irep_idt identifier = step.lhs_object.get_identifier();
+  auto lhs_object=step.get_lhs_object();
+
+  irep_idt identifier =
+    lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
 
   json_assignment["stepType"] = json_stringt("assignment");
 

src/goto-programs/vcd_goto_trace.cpp

@@ -89,16 +89,20 @@ void output_vcd(
   {
     if(step.is_assignment())
     {
-      irep_idt identifier=step.lhs_object.get_identifier();
-      const typet &type=step.lhs_object.type();
+      auto lhs_object=step.get_lhs_object();
+      if(lhs_object.has_value())
+      {
+        irep_idt identifier=lhs_object->get_identifier();
+        const typet &type=lhs_object->type();
 
-      const auto number=n.number(identifier);
+        const auto number=n.number(identifier);
 
-      const mp_integer width = pointer_offset_bits(type, ns);
+        const mp_integer width = pointer_offset_bits(type, ns);
 
-      if(width>=1)
-        out << "$var reg " << width << " V" << number << " "
-            << identifier << " $end" << "\n";
+        if(width>=1)
+          out << "$var reg " << width << " V" << number << " "
+              << identifier << " $end" << "\n";
+      }
     }
   }
 
@@ -113,30 +117,34 @@ void output_vcd(
     {
     case goto_trace_stept::typet::ASSIGNMENT:
       {
-        irep_idt identifier=step.lhs_object.get_identifier();
-        const typet &type=step.lhs_object.type();
-
-        out << '#' << timestamp << "\n";
-        timestamp++;
-
-        const auto number=n.number(identifier);
-
-        // booleans are special in VCD
-        if(type.id()==ID_bool)
+        auto lhs_object=step.get_lhs_object();
+        if(lhs_object.has_value())
         {
-          if(step.lhs_object_value.is_true())
-            out << "1" << "V" << number << "\n";
-          else if(step.lhs_object_value.is_false())
-            out << "0" << "V" << number << "\n";
+          irep_idt identifier=lhs_object->get_identifier();
+          const typet &type=lhs_object->type();
+
+          out << '#' << timestamp << "\n";
+          timestamp++;
+
+          const auto number=n.number(identifier);
+
+          // booleans are special in VCD
+          if(type.id()==ID_bool)
+          {
+            if(step.full_lhs_value.is_true())
+              out << "1" << "V" << number << "\n";
+            else if(step.full_lhs_value.is_false())
+              out << "0" << "V" << number << "\n";
+            else
+              out << "x" << "V" << number << "\n";
+          }
           else
-            out << "x" << "V" << number << "\n";
-        }
-        else
-        {
-          std::string binary=as_vcd_binary(step.lhs_object_value, ns);
+          {
+            std::string binary=as_vcd_binary(step.full_lhs_value, ns);
 
-          if(binary!="")
-            out << "b" << binary << " V" << number << " " << "\n";
+            if(binary!="")
+              out << "b" << binary << " V" << number << " " << "\n";
+          }
         }
       }
       break;

src/goto-programs/xml_goto_trace.cpp

@@ -71,17 +71,33 @@ void convert(
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::DECL:
       {
-        irep_idt identifier=step.lhs_object.get_identifier();
+        auto lhs_object=step.get_lhs_object();
+        irep_idt identifier=
+          lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
         xmlt &xml_assignment=dest.new_element("assignment");
 
         if(xml_location.name!="")
           xml_assignment.new_element().swap(xml_location);
 
-        std::string value_string, type_string,
-                    full_lhs_string, full_lhs_value_string;
+        {
+          auto lhs_object=step.get_lhs_object();
+
+          const symbolt *symbol;
+
+          if(lhs_object.has_value() &&
+             !ns.lookup(lhs_object->get_identifier(), symbol))
+          {
+            std::string type_string=from_type(ns, symbol->name, symbol->type);
+
+            xml_assignment.set_attribute("mode", id2string(symbol->mode));
+            xml_assignment.set_attribute("identifier", id2string(symbol->name));
+            xml_assignment.set_attribute("base_name", id2string(symbol->base_name));
+            xml_assignment.set_attribute("display_name", id2string(symbol->display_name()));
+            xml_assignment.new_element("type").data=type_string;
+          }
+        }
 
-        if(step.lhs_object_value.is_not_nil())
-          value_string=from_expr(ns, identifier, step.lhs_object_value);
+        std::string full_lhs_string, full_lhs_value_string;
 
         if(step.full_lhs.is_not_nil())
           full_lhs_string=from_expr(ns, identifier, step.full_lhs);
@@ -90,28 +106,11 @@ void convert(
           full_lhs_value_string=
             from_expr(ns, identifier, step.full_lhs_value);
 
-        const symbolt *symbol;
-        irep_idt base_name, display_name;
-
-        if(!ns.lookup(identifier, symbol))
-        {
-          base_name=symbol->base_name;
-          display_name=symbol->display_name();
-          if(type_string=="")
-            type_string=from_type(ns, identifier, symbol->type);
-
-          xml_assignment.set_attribute("mode", id2string(symbol->mode));
-        }
-
-        xml_assignment.new_element("type").data=type_string;
         xml_assignment.new_element("full_lhs").data=full_lhs_string;
         xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
 
         xml_assignment.set_attribute_bool("hidden", step.hidden);
         xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
-        xml_assignment.set_attribute("identifier", id2string(identifier));
-        xml_assignment.set_attribute("base_name", id2string(base_name));
-        xml_assignment.set_attribute("display_name", id2string(display_name));
         xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
 
         xml_assignment.set_attribute("assignment_type",

src/goto-symex/build_goto_trace.cpp

@@ -295,16 +295,6 @@ void build_goto_trace(
       goto_trace_step.thread_nr = SSA_step.source.thread_nr;
       goto_trace_step.pc = SSA_step.source.pc;
       goto_trace_step.comment = SSA_step.comment;
-      if(SSA_step.ssa_lhs.is_not_nil())
-      {
-        goto_trace_step.lhs_object =
-          ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
-      }
-      else
-      {
-        goto_trace_step.lhs_object.make_nil();
-      }
-
       goto_trace_step.type = SSA_step.type;
       goto_trace_step.hidden = SSA_step.hidden;
       goto_trace_step.format_string = SSA_step.format_string;
@@ -334,9 +324,6 @@ void build_goto_trace(
           prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
       }
 
-      if(SSA_step.ssa_lhs.is_not_nil())
-        goto_trace_step.lhs_object_value = prop_conv.get(SSA_step.ssa_lhs);
-
       if(SSA_step.ssa_full_lhs.is_not_nil())
       {
         goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);