added internal field to json output

Added internal field to json output so that we set it to tru
as we find some specific variable that is not supposed to be
shown in the counterexample trace.

Author: lucasccordeiro

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

@@ -111,7 +111,7 @@ exprt adjust_lhs_object(
 
 /// set internal field for variable assignment related to dynamic_object[0-9]
 /// and dynamic_[0-9]_array.
-void hide_dynamic_object(
+void set_internal_dynamic_object(
   const exprt &expr,
   goto_trace_stept &goto_trace_step,
   const namespacet &ns)
@@ -124,39 +124,39 @@ void hide_dynamic_object(
     {
       bool result=symbol->type.get_bool("#dynamic");
       if(result)
-        goto_trace_step.hidden=true;
+        goto_trace_step.internal=true;
     }
   }
   else
   {
     forall_operands(it, expr)
-      hide_dynamic_object(*it, goto_trace_step, ns);
+      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_fields_to_hidden(
+void update_internal_field(
   const symex_target_equationt::SSA_stept &SSA_step,
   goto_trace_stept &goto_trace_step,
   const namespacet &ns)
 {
-  // hide dynamic_object in both lhs and rhs expressions
-  hide_dynamic_object(SSA_step.ssa_lhs, goto_trace_step, ns);
-  hide_dynamic_object(SSA_step.ssa_rhs, goto_trace_step, 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);
 
-  // hide internal CPROVER functions (e.g., __CPROVER_initialize)
+  // 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.hidden=true;
+      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.hidden=true;
+    goto_trace_step.internal=true;
   }
 
   // set internal field to _start function-return step
@@ -273,8 +273,8 @@ void build_goto_trace(
     goto_trace_step.formatted=SSA_step.formatted;
     goto_trace_step.identifier=SSA_step.identifier;
 
-    // hide specific variables in the counterexample trace
-    update_fields_to_hidden(SSA_step, goto_trace_step, ns);
+    // 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()&&