remove lhs_object from goto_trace_stept

Author: kroening

src/goto-programs/goto_trace.cpp

@@ -93,11 +93,15 @@ void goto_trace_stept::output(
 
   out << "\n";
 
-  if((pc->is_other() && lhs_object.is_not_nil()) || pc->is_assign())
+  if((pc->is_other() && full_lhs.is_not_nil()) || pc->is_assign())
   {
-    irep_idt identifier=lhs_object.get_object_name();
-    out << "  " << from_expr(ns, identifier, lhs_object.get_original_expr())
-        << " = " << from_expr(ns, identifier, lhs_object_value)
+    auto lhs_object=get_lhs_object();
+
+    const irep_idt identifier=
+      lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
+
+    out << "  " << from_expr(ns, identifier, full_lhs)
+        << " = " << from_expr(ns, identifier, full_lhs_value)
         << "\n";
   }
   else if(pc->is_assert())
@@ -306,7 +310,7 @@ void show_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)
         {
@@ -315,13 +319,8 @@ void show_goto_trace(
           show_state_header(out, step, step.pc->source_location, step.step_nr);
         }
 
-        // 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);
-        else
-          trace_value(
-            out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
+        trace_value(
+          out, ns, step.full_lhs, step.full_lhs_value);
       }
       break;
 
@@ -333,7 +332,7 @@ void show_goto_trace(
         show_state_header(out, step, step.pc->source_location, step.step_nr);
       }
 
-      trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
+      trace_value(out, ns, step.full_lhs, step.full_lhs_value);
       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;
@@ -138,8 +138,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();
@@ -203,8 +201,7 @@ void show_goto_trace(
 void trace_value(
   std::ostream &out,
   const namespacet &,
-  const ssa_exprt &lhs_object,
-  const exprt &full_lhs,
+  const exprt &lhs,
   const exprt &value);
 
 

src/goto-programs/graphml_witness.cpp

@@ -278,7 +278,7 @@ 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() ||

src/goto-programs/interpreter.cpp

@@ -675,15 +675,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

@@ -70,17 +70,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, binary_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);
 
-        if(step.lhs_object_value.is_not_nil())
-          value_string=from_expr(ns, identifier, step.lhs_object_value);
+            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;
+          }
+        }
+
+        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);
@@ -89,43 +105,17 @@ void convert(
           full_lhs_value_string=
             from_expr(ns, identifier, step.full_lhs_value);
 
-        if(step.lhs_object_value.type().is_not_nil())
-          type_string=
-            from_type(ns, identifier, step.lhs_object_value.type());
-
-        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.new_element("value").data=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",
           step.assignment_type==
             goto_trace_stept::assignment_typet::ACTUAL_PARAMETER?
           "actual_parameter":"state");
-
-        if(step.lhs_object_value.is_not_nil())
-          xml_assignment.new_element("value_expression").
-            new_element(xml(step.lhs_object_value, ns));
       }
       break;
 

src/goto-symex/build_goto_trace.cpp

@@ -265,11 +265,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;
@@ -294,9 +289,6 @@ void build_goto_trace(
         build_full_lhs_rec(
           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);