From 072e37412eef52f62a6ddcf62d6d7bd3541d4d8d Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Tue, 28 Mar 2017 17:53:51 +0100
Subject: [PATCH] Display dynamic object names as 'data' in JSON traces

Fixes diffblue/test-gen#147
---
 src/util/json_expr.cpp | 70 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 68 insertions(+), 2 deletions(-)

diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
index 77f58eb0e18..3b494ff9543 100644
--- a/src/util/json_expr.cpp
+++ b/src/util/json_expr.cpp
@@ -14,11 +14,67 @@ Author: Peter Schrammel
 #include "fixedbv.h"
 #include "std_expr.h"
 #include "config.h"
+#include "identifier.h"
 
 #include "json_expr.h"
 
 /*******************************************************************\
 
+Function: simplify_json_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt simplify_json_expr(
+  const exprt &src,
+  const namespacet &ns)
+{
+  if(src.id()==ID_constant)
+  {
+    const typet &type=ns.follow(src.type());
+
+    if(type.id()==ID_pointer)
+    {
+      const irep_idt &value=to_constant_expr(src).get_value();
+
+      if(value!=ID_NULL &&
+         (value!=std::string(value.size(), '0') ||
+          !config.ansi_c.NULL_is_zero) &&
+         src.operands().size()==1 &&
+         src.op0().id()!=ID_constant)
+        // try to simplify the constant pointer
+        return simplify_json_expr(src.op0(), ns);
+    }
+  }
+  else if(src.id()==ID_address_of &&
+          src.operands().size()==1 &&
+          src.op0().id()==ID_member &&
+          id2string(to_member_expr(
+            src.op0()).get_component_name()).find("@")!=std::string::npos)
+  {
+    // simplify things of the form  &member_expr(object, @class_identifier)
+    return simplify_json_expr(src.op0(), ns);
+  }
+  else if(src.id()==ID_member &&
+          src.operands().size()==1 &&
+          id2string(
+            to_member_expr(src).get_component_name())
+              .find("@")!=std::string::npos)
+  {
+    // simplify things of the form  member_expr(object, @class_identifier)
+    return simplify_json_expr(src.op0(), ns);
+  }
+
+  return src;
+}
+
+/*******************************************************************\
+
 Function: json
 
   Inputs:
@@ -262,9 +318,19 @@ json_objectt json(
     else if(type.id()==ID_pointer)
     {
       result["name"]=json_stringt("pointer");
-      result["binary"]=json_stringt(expr.get_string(ID_value));
-      if(expr.get(ID_value)==ID_NULL)
+      exprt simpl_expr=simplify_json_expr(expr, ns);
+      if(simpl_expr.get(ID_value)==ID_NULL ||
+         // remove typecast on NULL
+         (simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer &&
+          simpl_expr.op0().get(ID_value)==ID_NULL))
         result["data"]=json_stringt("NULL");
+      else if(simpl_expr.id()==ID_symbol)
+      {
+        const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();
+        identifiert identifier(id2string(ptr_id));
+        assert(!identifier.components.empty());
+        result["data"]=json_stringt(identifier.components.back());
+      }
     }
     else if(type.id()==ID_bool)
     {