Restore member-of-union expressions in trace output

byte_extract operations precisely capture the semantics, but aren't
meaningful to users.

Author: tautschnig

regression/cbmc/xml-trace/test.desc

@@ -7,7 +7,7 @@ VERIFICATION FAILED
 <assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">
 <location file=".*" function="test" line="\d+" working-directory=".*"/>
 <type>union myunion</type>
-<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
+<full_lhs>u</full_lhs>
 <full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>
 <value>\{ \.i=\d+ll? \}</value>
 <value_expression>

src/goto-programs/goto_trace.cpp

@@ -19,36 +19,25 @@ Author: Daniel Kroening
 #include <util/byte_operators.h>
 #include <util/format_expr.h>
 #include <util/range.h>
+#include <util/std_expr.h>
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
 #include <langapi/language_util.h>
 
 #include "printf_formatter.h"
+#include "rewrite_union.h"
 
-static optionalt<symbol_exprt> get_object_rec(const exprt &src)
+optionalt<symbol_exprt>
+goto_trace_stept::get_lhs_object(const namespacet &ns) const
 {
-  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 if(
-    src.id() == ID_byte_extract_little_endian ||
-    src.id() == ID_byte_extract_big_endian)
-  {
-    return get_object_rec(to_byte_extract_expr(src).op());
-  }
-  else
-    return {}; // give up
-}
+  object_descriptor_exprt ode;
+  ode.build(full_lhs, ns);
 
-optionalt<symbol_exprt> goto_trace_stept::get_lhs_object() const
-{
-  return get_object_rec(full_lhs);
+  if(ode.root_object().id() == ID_symbol)
+    return to_symbol_expr(ode.root_object());
+  else
+    return {};
 }
 
 void goto_tracet::output(
@@ -59,9 +48,7 @@ void goto_tracet::output(
     step.output(ns, out);
 }
 
-void goto_trace_stept::output(
-  const namespacet &,
-  std::ostream &out) const
+void goto_trace_stept::output(const namespacet &ns, std::ostream &out) const
 {
   out << "*** ";
 
@@ -126,7 +113,9 @@ void goto_trace_stept::output(
       if(!comment.empty())
         out << "  " << comment << '\n';
 
-      out << "  " << format(pc->get_condition()) << '\n';
+      exprt condition{pc->get_condition()};
+      restore_union(condition, ns);
+      out << "  " << format(condition) << '\n';
       out << '\n';
     }
   }
@@ -397,9 +386,9 @@ void show_compact_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  "
-              << from_expr(ns, step.function_id, step.pc->get_condition())
-              << '\n';
+          exprt condition{step.pc->get_condition()};
+          restore_union(condition, ns);
+          out << "  " << from_expr(ns, step.function_id, condition) << '\n';
         }
 
         out << '\n';
@@ -425,7 +414,7 @@ void show_compact_goto_trace(
       trace_value(
         out,
         ns,
-        step.get_lhs_object(),
+        step.get_lhs_object(ns),
         step.full_lhs,
         step.full_lhs_value,
         options);
@@ -524,9 +513,9 @@ void show_full_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  "
-              << from_expr(ns, step.function_id, step.pc->get_condition())
-              << '\n';
+          exprt condition{step.pc->get_condition()};
+          restore_union(condition, ns);
+          out << "  " << from_expr(ns, step.function_id, condition) << '\n';
         }
 
         out << '\n';
@@ -570,7 +559,7 @@ void show_full_goto_trace(
         trace_value(
           out,
           ns,
-          step.get_lhs_object(),
+          step.get_lhs_object(ns),
           step.full_lhs,
           step.full_lhs_value,
           options);
@@ -587,7 +576,12 @@ void show_full_goto_trace(
 
       out << "  ";
       trace_value(
-        out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
+        out,
+        ns,
+        step.get_lhs_object(ns),
+        step.full_lhs,
+        step.full_lhs_value,
+        options);
       break;
 
     case goto_trace_stept::typet::OUTPUT:

src/goto-programs/goto_trace.h

@@ -126,7 +126,7 @@ class goto_trace_stept
   exprt full_lhs;
 
   // the object being assigned
-  optionalt<symbol_exprt> get_lhs_object() const;
+  optionalt<symbol_exprt> get_lhs_object(const namespacet &ns) const;
 
   // A constant with the new value of the lhs
   exprt full_lhs_value;

src/goto-programs/graphml_witness.cpp

@@ -434,7 +434,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         data_t.data = std::to_string(it->thread_nr);
       }
 
-      const auto lhs_object = it->get_lhs_object();
+      const auto lhs_object = it->get_lhs_object(ns);
       if(
         it->type == goto_trace_stept::typet::ASSIGNMENT &&
         lhs_object.has_value())

src/goto-programs/json_goto_trace.cpp

@@ -65,7 +65,7 @@ void convert_decl(
   const jsont &json_location = conversion_dependencies.location;
   const namespacet &ns = conversion_dependencies.ns;
 
-  auto lhs_object=step.get_lhs_object();
+  auto lhs_object = step.get_lhs_object(ns);
 
   irep_idt identifier =
     lhs_object.has_value()?lhs_object->get_identifier():irep_idt();

src/goto-programs/rewrite_union.cpp

@@ -124,3 +124,51 @@ void rewrite_union(goto_modelt &goto_model)
 {
   rewrite_union(goto_model.goto_functions);
 }
+
+/// Undo the union access -> byte_extract replacement that rewrite_union did for
+/// the purpose of displaying expressions to users.
+/// \param expr: expression to inspect and possibly transform
+/// \param ns: namespace
+/// \return True if, and only if, the expression is unmodified
+static bool restore_union_rec(exprt &expr, const namespacet &ns)
+{
+  bool unmodified = true;
+
+  Forall_operands(it, expr)
+    unmodified &= restore_union_rec(*it, ns);
+
+  if(expr.id() == byte_extract_id())
+  {
+    byte_extract_exprt &be = to_byte_extract_expr(expr);
+    if(
+      (be.op().type().id() == ID_union ||
+       be.op().type().id() == ID_union_tag) &&
+      be.offset().is_zero())
+    {
+      const union_typet &union_type = to_union_type(ns.follow(be.op().type()));
+
+      for(const auto &comp : union_type.components())
+      {
+        if(be.type() == comp.type())
+        {
+          expr = member_exprt{be.op(), comp.get_name(), be.type()};
+          return false;
+        }
+      }
+    }
+  }
+
+  return unmodified;
+}
+
+/// Undo the union access -> byte_extract replacement that rewrite_union did for
+/// the purpose of displaying expressions to users.
+/// \param expr: expression to inspect and possibly transform
+/// \param ns: namespace
+void restore_union(exprt &expr, const namespacet &ns)
+{
+  exprt tmp = expr;
+
+  if(!restore_union_rec(tmp, ns))
+    expr.swap(tmp);
+}

src/goto-programs/rewrite_union.h

@@ -24,4 +24,6 @@ void rewrite_union(goto_functionst::goto_functiont &);
 void rewrite_union(goto_functionst &);
 void rewrite_union(goto_modelt &);
 
+void restore_union(exprt &, const namespacet &);
+
 #endif // CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H

src/goto-programs/vcd_goto_trace.cpp

@@ -88,7 +88,7 @@ void output_vcd(
   {
     if(step.is_assignment())
     {
-      auto lhs_object=step.get_lhs_object();
+      auto lhs_object = step.get_lhs_object(ns);
       if(lhs_object.has_value())
       {
         irep_idt identifier=lhs_object->get_identifier();
@@ -115,7 +115,7 @@ void output_vcd(
   {
     if(step.is_assignment())
     {
-      auto lhs_object = step.get_lhs_object();
+      auto lhs_object = step.get_lhs_object(ns);
       if(lhs_object.has_value())
       {
         irep_idt identifier = lhs_object->get_identifier();

src/goto-programs/xml_goto_trace.cpp

@@ -31,7 +31,7 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
   if(value.is_nil())
     return value_xml;
 
-  const auto &lhs_object = step.get_lhs_object();
+  const auto &lhs_object = step.get_lhs_object(ns);
   const irep_idt identifier =
     lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
   value_xml.data = from_expr(ns, identifier, value);
@@ -91,7 +91,7 @@ void convert(
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::DECL:
     {
-      auto lhs_object = step.get_lhs_object();
+      auto lhs_object = step.get_lhs_object(ns);
       irep_idt identifier =
         lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
       xmlt &xml_assignment = dest.new_element("assignment");

src/goto-symex/build_goto_trace.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening
 
 #include <solvers/decision_procedure.h>
 
+#include <goto-programs/rewrite_union.h>
+
 #include "partial_order_concurrency.h"
 
 static exprt build_full_lhs_rec(
@@ -378,6 +380,7 @@ void build_goto_trace(
             SSA_step.ssa_full_lhs),
           ns);
         replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
+        restore_union(goto_trace_step.full_lhs, ns);
       }
 
       if(SSA_step.ssa_full_lhs.is_not_nil())