diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class new file mode 100644 index 00000000000..bf9694b3f36 Binary files /dev/null and b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class differ diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java new file mode 100644 index 00000000000..6e04c6f345a --- /dev/null +++ b/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; +} diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class new file mode 100644 index 00000000000..9c810453dec Binary files /dev/null and b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class differ diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java new file mode 100644 index 00000000000..012c3c7a355 --- /dev/null +++ b/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; + } +} diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt new file mode 100644 index 00000000000..2a237709812 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/regression/cbmc-java/internal1/test.desc b/regression/cbmc-java/internal1/test.desc new file mode 100644 index 00000000000..09047367ca9 --- /dev/null +++ b/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 diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 4c8a3accc8a..67601851ff8 100644 --- a/src/goto-programs/goto_trace.h +++ b/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), diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 744e26500db..c15786900fe 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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; diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index ee03e7e0bd8..56f9f42763d 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/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==