Merge pull request #2204 from diffblue/remove-lhs-object

remove lhs_object from goto_trace_stept

Author: kroening

regression/cbmc/trace-values/trace-values.c

@@ -0,0 +1,38 @@
+int global_var;
+
+struct S
+{
+  int f;
+  int array[3];
+} my_nested[2];
+
+int main()
+{
+  static int static_var;
+  int local_var;
+  int *p=&my_nested[0].array[1];
+  int *q=&my_nested[1].f;
+  int *null=0;
+  int *junk;
+
+  global_var=1;
+  static_var=2;
+  local_var=3;
+  *p=4;
+  *q=5;
+  *null=6;
+  *junk=7;
+
+  // dynamic
+  p=malloc(sizeof(int)*2);
+  p[1]=8;
+  
+  // not even a pointer variable
+  *(int *)0=9;
+
+  // assign entire struct
+  my_nested[1]=my_nested[0];
+
+  // get a trace
+  __CPROVER_assert(0, "");
+}

regression/cbmc/trace-values/trace-values.desc

@@ -0,0 +1,18 @@
+CORE
+trace-values.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^  local_var=0 .*$
+^  global_var=1 .*$
+^  static_var=2 .*$
+^  local_var=3 .*$
+^  my_nested\[0.*\].array\[1.*\]=4 .*$
+^  my_nested\[1.*\].f=5 .*$
+^  null\$object=6 .*$
+^  junk\$object=7 .*$
+^  dynamic_object1\[1.*\]=8 .*$
+^  my_nested\[1.*\]={ .f=0, .array={ 0, 4, 0 } } .*$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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;