From fafe838c2dd8b9725ca87f31ae0b1e8ba04dccba Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 26 Nov 2020 15:04:33 +0000
Subject: [PATCH] Restore member-of-union expressions in trace output

byte_extract operations precisely capture the semantics, but aren't
meaningful to users.
---
 regression/cbmc/xml-trace/test.desc |  2 +-
 src/goto-programs/goto_trace.cpp    | 10 +++--
 src/goto-programs/goto_trace.h      |  2 +
 src/goto-programs/rewrite_union.cpp | 63 +++++++++++++++++++++++++++++
 src/goto-programs/rewrite_union.h   |  2 +
 src/goto-symex/build_goto_trace.cpp |  8 ++++
 6 files changed, 82 insertions(+), 5 deletions(-)

diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
index 2ff05d1a71f..5ed215d69a5 100644
--- a/regression/cbmc/xml-trace/test.desc
+++ b/regression/cbmc/xml-trace/test.desc
@@ -7,7 +7,7 @@ activate-multi-line-match
 VERIFICATION FAILED
 <assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
 <value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
-<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
 --
 ^warning: ignoring
 --
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index c4ba7003589..5d779e7aad6 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -128,7 +128,7 @@ void goto_trace_stept::output(
       if(!comment.empty())
         out << "  " << comment << '\n';
 
-      out << "  " << format(pc->condition()) << '\n';
+      out << "  " << format(original_condition) << '\n';
       out << '\n';
     }
   }
@@ -422,7 +422,8 @@ void show_compact_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  " << from_expr(ns, step.function_id, step.pc->condition())
+          out << "  "
+              << from_expr(ns, step.function_id, step.original_condition)
               << '\n';
         }
 
@@ -549,7 +550,8 @@ void show_full_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  " << from_expr(ns, step.function_id, step.pc->condition())
+          out << "  "
+              << from_expr(ns, step.function_id, step.original_condition)
               << '\n';
         }
 
@@ -566,7 +568,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->condition())
+        out << "  " << from_expr(ns, step.function_id, step.original_condition)
             << '\n';
       }
       break;
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index ae8197601b6..6941908ee11 100644
--- a/src/goto-programs/goto_trace.h
+++ b/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();
   }
 
   /// Use \p dest to establish sharing among ireps.
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index 2f109083618..116dfdda6b5 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/std_code.h>
 
 #include <goto-programs/goto_model.h>
@@ -116,3 +117,65 @@ 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() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian)
+  {
+    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);
+}
diff --git a/src/goto-programs/rewrite_union.h b/src/goto-programs/rewrite_union.h
index 590794f7f5e..89e61b2ec46 100644
--- a/src/goto-programs/rewrite_union.h
+++ b/src/goto-programs/rewrite_union.h
@@ -22,4 +22,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
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 7c2a0a93fe6..1f3e3e5741a 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening
 #include <util/symbol.h>
 
 #include <goto-programs/goto_functions.h>
+#include <goto-programs/rewrite_union.h>
 
 #include <solvers/decision_procedure.h>
 
@@ -379,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())
@@ -411,6 +413,12 @@ 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->condition();
+        restore_union(goto_trace_step.original_condition, ns);
+      }
+
       if(ssa_step_it == last_step_to_keep)
         return;
     }