Merge pull request #709 from lucasccordeiro/fixing-issue-20

set internal field in specific variables in the counterexample trace for test-gen-support

Author: peterschrammel

src/goto-programs/goto_trace.h

@@ -63,6 +63,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
   typedef enum { STATE, ACTUAL_PARAMETER } assignment_typet;
   assignment_typet assignment_type;
@@ -107,6 +110,7 @@ class goto_trace_stept
     step_nr(0),
     type(NONE),
     hidden(false),
+    internal(false),
     assignment_type(STATE),
     thread_nr(0),
     cond_value(false),

src/goto-programs/json_goto_trace.cpp

@@ -68,6 +68,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));
@@ -118,6 +119,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"]=
@@ -132,6 +134,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));
 
@@ -156,6 +159,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));
 
@@ -184,6 +188,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);
@@ -207,6 +212,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

@@ -132,6 +132,86 @@ exprt adjust_lhs_object(
 
 /*******************************************************************\
 
+Function: set_internal_dynamic_object
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 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);
+  }
+}
+
+/*******************************************************************\
+
+Function: update_internal_field
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 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::OUTPUT ||
+      goto_trace_step.type==goto_trace_stept::INPUT)
+  {
+    goto_trace_step.internal=true;
+  }
+
+  // set internal field to _start function-return step
+  if(SSA_step.source.pc->function==goto_functionst::entry_point())
+  {
+    goto_trace_step.internal=true;
+  }
+}
+
+/*******************************************************************\
+
 Function: build_goto_trace
 
   Inputs:
@@ -237,6 +317,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==symex_targett::VISIBLE_ACTUAL_PARAMETER ||