hide internal symbols in the goto trace

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java

@@ -0,0 +1,5 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Item {
+  public int cost;
+}

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java

@@ -0,0 +1,25 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Order {
+  public Item item;
+
+  /**
+   * Checks if this order has an item.
+   */
+  public boolean hasItem() {
+    if (item == null) {
+      return false;
+    } else {
+      return true;
+    }
+  }
+
+  /**
+   * Sets the item for this order.
+   */
+  public boolean setItem(Item item) {
+    boolean exists = hasItem();
+    this.item = item;
+    return exists;
+  }
+}

regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt

@@ -0,0 +1,2 @@
+Source of benchmark:
+https://github.com/DiffBlue-benchmarks/java-test

regression/cbmc-java/internal1/test.desc

@@ -0,0 +1,13 @@
+CORE
+com/diffblue/javatest/nestedobjects/subpackage/Order.class
+--json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --cover location --trace
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"identifier": "__CPROVER_initialize",\n *"sourceLocation": [{][}]\n *[}],\n *"hidden": false,\n *"internal": true,\n *"stepType": "function-call",
+"internal": true,\n *"lhs": "tmp_object_factory[$][0-9]+",
+"internal": false,\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",\n *"line": "21"\n *[}],\n *"stepType": "function-call",
+"internal": false,\n *"lhs": "this",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+"internal": false,\n *"lhs": "item",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+--
+^warning: ignoring

src/goto-programs/goto_trace.h

@@ -83,6 +83,9 @@ class goto_trace_stept
   // we may choose to hide a step
   bool hidden;
 
+  // this is related to an internal expression
+  bool internal;
+
   // we categorize
   enum class assignment_typet { STATE, ACTUAL_PARAMETER };
   assignment_typet assignment_type;
@@ -127,6 +130,7 @@ class goto_trace_stept
     step_nr(0),
     type(typet::NONE),
     hidden(false),
+    internal(false),
     assignment_type(assignment_typet::STATE),
     thread_nr(0),
     cond_value(false),

src/goto-programs/json_goto_trace.cpp

@@ -59,6 +59,7 @@ void convert(
 
         json_failure["stepType"]=json_stringt("failure");
         json_failure["hidden"]=jsont::json_boolean(step.hidden);
+        json_failure["internal"]=jsont::json_boolean(step.internal);
         json_failure["thread"]=json_numbert(std::to_string(step.thread_nr));
         json_failure["reason"]=json_stringt(id2string(step.comment));
         json_failure["property"]=json_stringt(id2string(property_id));
@@ -109,6 +110,7 @@ void convert(
         json_assignment["value"]=full_lhs_value;
         json_assignment["lhs"]=json_stringt(full_lhs_string);
         json_assignment["hidden"]=jsont::json_boolean(step.hidden);
+        json_assignment["internal"]=jsont::json_boolean(step.internal);
         json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));
 
         json_assignment["assignmentType"]=
@@ -126,6 +128,7 @@ void convert(
 
         json_output["stepType"]=json_stringt("output");
         json_output["hidden"]=jsont::json_boolean(step.hidden);
+        json_output["internal"]=jsont::json_boolean(step.internal);
         json_output["thread"]=json_numbert(std::to_string(step.thread_nr));
         json_output["outputID"]=json_stringt(id2string(step.io_id));
 
@@ -150,6 +153,7 @@ void convert(
 
         json_input["stepType"]=json_stringt("input");
         json_input["hidden"]=jsont::json_boolean(step.hidden);
+        json_input["internal"]=jsont::json_boolean(step.internal);
         json_input["thread"]=json_numbert(std::to_string(step.thread_nr));
         json_input["inputID"]=json_stringt(id2string(step.io_id));
 
@@ -178,6 +182,7 @@ void convert(
 
         json_call_return["stepType"]=json_stringt(tag);
         json_call_return["hidden"]=jsont::json_boolean(step.hidden);
+        json_call_return["internal"]=jsont::json_boolean(step.internal);
         json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr));
 
         const symbolt &symbol=ns.lookup(step.identifier);
@@ -201,6 +206,7 @@ void convert(
           json_objectt &json_location_only=dest_array.push_back().make_object();
           json_location_only["stepType"]=json_stringt("location-only");
           json_location_only["hidden"]=jsont::json_boolean(step.hidden);
+          json_location_only["internal"]=jsont::json_boolean(step.internal);
           json_location_only["thread"]=
             json_numbert(std::to_string(step.thread_nr));
           json_location_only["sourceLocation"]=json_location;

src/goto-symex/build_goto_trace.cpp

@@ -109,6 +109,67 @@ exprt adjust_lhs_object(
   return nil_exprt();
 }
 
+/// set internal field for variable assignment related to dynamic_object[0-9]
+/// and dynamic_[0-9]_array.
+void set_internal_dynamic_object(
+  const exprt &expr,
+  goto_trace_stept &goto_trace_step,
+  const namespacet &ns)
+{
+  if(expr.id()==ID_symbol)
+  {
+    const irep_idt &id=to_ssa_expr(expr).get_original_name();
+    const symbolt *symbol;
+    if(!ns.lookup(id, symbol))
+    {
+      bool result=symbol->type.get_bool("#dynamic");
+      if(result)
+        goto_trace_step.internal=true;
+    }
+  }
+  else
+  {
+    forall_operands(it, expr)
+      set_internal_dynamic_object(*it, goto_trace_step, ns);
+  }
+}
+
+/// set internal for variables assignments related to dynamic_object and CPROVER
+/// internal functions (e.g., __CPROVER_initialize)
+void update_internal_field(
+  const symex_target_equationt::SSA_stept &SSA_step,
+  goto_trace_stept &goto_trace_step,
+  const namespacet &ns)
+{
+  // set internal for dynamic_object in both lhs and rhs expressions
+  set_internal_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns);
+  set_internal_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, ns);
+
+  // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
+  if(SSA_step.is_function_call())
+  {
+    if(SSA_step.source.pc->source_location.as_string().empty())
+      goto_trace_step.internal=true;
+  }
+
+  // set internal field to input and output steps
+  if(goto_trace_step.type==goto_trace_stept::typet::OUTPUT ||
+      goto_trace_step.type==goto_trace_stept::typet::INPUT)
+  {
+    goto_trace_step.internal=true;
+  }
+
+  // set internal field to _start function-return step
+  if(SSA_step.source.pc->function==goto_functionst::entry_point())
+  {
+    // "__CPROVER_*" function calls in __CPROVER_start are already marked as
+    // internal. Don't mark any other function calls (i.e. "main"), function
+    // arguments or any other parts of a code_function_callt as internal.
+    if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
+      goto_trace_step.internal=true;
+  }
+}
+
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator end_step,
@@ -216,6 +277,9 @@ void build_goto_trace(
     goto_trace_step.formatted=SSA_step.formatted;
     goto_trace_step.identifier=SSA_step.identifier;
 
+    // update internal field for specific variables in the counterexample
+    update_internal_field(SSA_step, goto_trace_step, ns);
+
     goto_trace_step.assignment_type=
       (it->is_assignment()&&
        (SSA_step.assignment_type==