From a5f773923a7a9ae3c294e0258fada17f8c5de5a6 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 6 Mar 2017 09:46:38 +0000 Subject: [PATCH 1/2] set internal for specific variables in the counterexample trace for test-gen-support set internal for variable assignments related to dynamic_object[0-9], dynamic_[0-9]_array, _start function-return step, and CPROVER internal functions (e.g., __CPROVER_initialize). This PR fixes diffblue/test-gen#20. --- src/goto-symex/build_goto_trace.cpp | 82 +++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 0e0a6f07dad..1221154d6a3 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -132,6 +132,85 @@ exprt adjust_lhs_object( /*******************************************************************\ +Function: hide_dynamic_object + + Inputs: + + Outputs: + + Purpose: hide variable assignments related to dynamic_object[0-9] + and dynamic_[0-9]_array. + +\*******************************************************************/ + +void hide_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.hidden=true; + } + } + else + { + forall_operands(it, expr) + hide_dynamic_object(*it, goto_trace_step, ns); + } +} + +/*******************************************************************\ + +Function: update_fields_to_hidden + + Inputs: + + Outputs: + + Purpose: hide variables assignments related to dynamic_object + and CPROVER internal functions (e.g., __CPROVER_initialize) + +\*******************************************************************/ + +void update_fields_to_hidden( + 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); + + // hide internal 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; + } + + // hide input and output steps + if(goto_trace_step.type==goto_trace_stept::OUTPUT || + goto_trace_step.type==goto_trace_stept::INPUT) + { + goto_trace_step.hidden=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 +316,9 @@ 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); + goto_trace_step.assignment_type= (it->is_assignment()&& (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER || From 508131009310a717346ea40c1402d60e73fe8b18 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Tue, 28 Mar 2017 16:00:35 +0100 Subject: [PATCH 2/2] 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. --- src/goto-programs/goto_trace.h | 4 +++ src/goto-programs/json_goto_trace.cpp | 6 +++++ src/goto-symex/build_goto_trace.cpp | 39 ++++++++++++++------------- 3 files changed, 30 insertions(+), 19 deletions(-) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index a669fac5e6b..dc270863894 100644 --- a/src/goto-programs/goto_trace.h +++ b/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), diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index da6590fe2de..3dca95bc93b 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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; diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 1221154d6a3..1cbb442497a 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -132,18 +132,18 @@ exprt adjust_lhs_object( /*******************************************************************\ -Function: hide_dynamic_object +Function: set_internal_dynamic_object Inputs: Outputs: - Purpose: hide variable assignments related to dynamic_object[0-9] - and dynamic_[0-9]_array. + Purpose: 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) @@ -156,50 +156,51 @@ 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); } } /*******************************************************************\ -Function: update_fields_to_hidden +Function: update_internal_field Inputs: Outputs: - Purpose: hide variables assignments related to dynamic_object - and CPROVER internal functions (e.g., __CPROVER_initialize) + Purpose: 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; } - // hide input and output steps + // 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.hidden=true; + goto_trace_step.internal=true; } // set internal field to _start function-return step @@ -316,8 +317,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()&&