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

@@ -126,7 +126,7 @@ void goto_trace_stept::output(
       if(!comment.empty())
         out << "  " << comment << '\n';
 
-      out << "  " << format(pc->get_condition()) << '\n';
+      out << "  " << format(original_condition) << '\n';
       out << '\n';
     }
   }
@@ -398,7 +398,7 @@ void show_compact_goto_trace(
         if(step.pc->is_assert())
         {
           out << "  "
-              << from_expr(ns, step.function_id, step.pc->get_condition())
+              << from_expr(ns, step.function_id, step.original_condition)
               << '\n';
         }
 
@@ -525,7 +525,7 @@ void show_full_goto_trace(
         if(step.pc->is_assert())
         {
           out << "  "
-              << from_expr(ns, step.function_id, step.pc->get_condition())
+              << from_expr(ns, step.function_id, step.original_condition)
               << '\n';
         }
 
@@ -542,7 +542,7 @@ void show_full_goto_trace(
         if(!step.pc->source_location.is_nil())
           out << "  " << step.pc->source_location << '\n';
 
-        out << "  " << from_expr(ns, step.function_id, step.pc->get_condition())
+        out << "  " << from_expr(ns, step.function_id, step.original_condition)
             << '\n';
       }
       break;

src/goto-programs/goto_trace.h

@@ -117,6 +117,7 @@ class goto_trace_stept
   // for assume, assert, goto
   bool cond_value;
   exprt cond_expr;
+  exprt original_condition;
 
   // for assert
   irep_idt property_id;
@@ -161,6 +162,7 @@ class goto_trace_stept
     full_lhs.make_nil();
     full_lhs_value.make_nil();
     cond_expr.make_nil();
+    original_condition.make_nil();
   }
 };
 

src/goto-programs/rewrite_union.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include "rewrite_union.h"
 
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/std_code.h>
 #include <util/byte_operators.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -124,3 +125,63 @@ 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)
+    {
+      const union_typet &union_type = to_union_type(ns.follow(be.op().type()));
+
+      for(const auto &comp : union_type.components())
+      {
+        if(be.offset().is_zero() && be.type() == comp.type())
+        {
+          expr = member_exprt{be.op(), comp.get_name(), be.type()};
+          return false;
+        }
+        else if(
+          comp.type().id() == ID_array || comp.type().id() == ID_struct ||
+          comp.type().id() == ID_struct_tag)
+        {
+          optionalt<exprt> result = get_subexpression_at_offset(
+            member_exprt{be.op(), comp.get_name(), comp.type()},
+            be.offset(),
+            be.type(),
+            ns);
+          if(result.has_value())
+          {
+            expr = *result;
+            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-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())
@@ -410,6 +413,13 @@ void build_goto_trace(
           decision_procedure.get(SSA_step.cond_handle).is_true();
       }
 
+      if(SSA_step.source.pc->is_assert() || SSA_step.source.pc->is_assume())
+      {
+        goto_trace_step.original_condition =
+          SSA_step.source.pc->get_condition();
+        restore_union(goto_trace_step.original_condition, ns);
+      }
+
       if(ssa_step_it == last_step_to_keep)
         return;
     }