From e7d28c42ba49d3e724ecf64c408404f9bd33ca24 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 6 Mar 2017 09:46:38 +0000 Subject: [PATCH 1/3] 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 | 60 +++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index ee03e7e0bd8..6dadd40941a 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -109,6 +109,63 @@ 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 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); + } +} + +/// set internal for 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; + } + + // 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; + } + + // set internal field to _start function-return step + if(SSA_step.source.pc->function==goto_functionst::entry_point()) + { + 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 +273,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== From 335d81586e57f6f18f31f8c86a6f6f919628b436 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Tue, 28 Mar 2017 16:00:35 +0100 Subject: [PATCH 2/3] 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 | 24 ++++++++++++------------ 3 files changed, 22 insertions(+), 12 deletions(-) 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 6dadd40941a..5028763d3db 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/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()&& From e906af424f17d76d673fd1ec0c8a97dae409d32b Mon Sep 17 00:00:00 2001 From: Pascal Kesseli Date: Thu, 25 May 2017 11:56:47 +0100 Subject: [PATCH 3/3] Avoid marking main function call / arguments as internal Fixes issue https://github.com/diffblue/test-gen/issues/334. The patch avoids marking any steps in _start whose source is a code_function_callt, which includes the main function call and its argument assignments. Internal function calls in _start (e.g. __CPROVER_initialize) are marked by previous checks. Includes a minimal test case from https://github.com/DiffBlue-benchmarks/java-test which sparked the issue. --- .../nestedobjects/subpackage/Item.class | Bin 0 -> 350 bytes .../nestedobjects/subpackage/Item.java | 5 ++++ .../nestedobjects/subpackage/Order.class | Bin 0 -> 719 bytes .../nestedobjects/subpackage/Order.java | 25 ++++++++++++++++++ .../nestedobjects/subpackage/readme.txt | 2 ++ regression/cbmc-java/internal1/test.desc | 13 +++++++++ src/goto-symex/build_goto_trace.cpp | 6 ++++- 7 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class create mode 100644 regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java create mode 100644 regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class create mode 100644 regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java create mode 100644 regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt create mode 100644 regression/cbmc-java/internal1/test.desc 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 0000000000000000000000000000000000000000..bf9694b3f360ac53622c0a0dea19714768811eb8 GIT binary patch literal 350 zcmbVHJ5Iwu6rAVyLrfr_8_)p-TL2Y^1_>#W1w~N$-SsAHu)WA$b1y0+3J$=b5O1xV zfMzr^Pj5!^^ZWG;;0lWzBTO^QGRz6FcAY2Cl91lo#`-(L==5yOmwQ(l!nClBdF*Rt z+GnXMb{2)xvRcd52E8|9|6)7Bb)j7?O1s&psyAXM-=#O57Y&0co!S}gJJI#(P3l*< zHDc*aeM87su5Yz@u%Tca%!}|lL5hrU`HxV-EF_3ZHe2yD6ypRDZwGiUVkCRU6|4_f hiQxhy=bxYtHX@7}Q?|j6IpbvD2@aWspd-cz$A3YDQJeq( literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..9c810453dec2363c6c121eec0729834933080b60 GIT binary patch literal 719 zcmb7>!Al!K6vn^FX0y#^HK}cCwGs5D5xSSO6x3b{fkIkAC5PT-H)9-4vSD{p`bT*Y zYzrQG75YaNznLuboXeYeZ{GX8@4fl^@8J)C9(F?bcwI*oTOrMMfHwg;0#$9)RN&np z&8G24UtT7Yg^I7`cWG2%;u(z^Wy!TlO%WH1WG>SiIacv!mK_Pyj`d8Nj{@HQ!H~31 z*+>aA2YRNyE~bgfFJv-dWMhz}ax#>;wtg9`nk!uhykE8VX+Bapn+I32usU4#Zvt!Q zhU&h^dC3n7WtQ(B_E+uU<~ty?rhe$cP^O?0o@a|ZRefz|3Z0I(c2^Oep&p@zAVL!@ zf!>PibSQzAg~by&8^@<^=h)+C`TRllw|L$>-q?*cq!+sv!0-NsxMQG#25pUDn;OwZ z?(Sm^>-6|LXwll@K2Mw1=-#992;aM{-qQ6PVx1?L7SOA+_&=&qqMo~4VWn)~Maev) x0$Uh$f5AKH9{xn7W1&l3OK6)Ty&`(kL3fw=CDiJ*g9_#Zc!@SE1+y(-^9j2;l&Sy# literal 0 HcmV?d00001 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-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 5028763d3db..56f9f42763d 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -162,7 +162,11 @@ void update_internal_field( // set internal field to _start function-return step if(SSA_step.source.pc->function==goto_functionst::entry_point()) { - goto_trace_step.internal=true; + // "__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; } }