From 714de0de54b225a8a363239a37303cad34a2a613 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 1 Aug 2018 12:35:00 +0100 Subject: [PATCH 1/6] Symex: expose call stack to unwinding decision making This enables unwind handlers to use the calling context to decide when to unwind a particular loop, the first use case being generic array clone methods called from enumeration type methods with known bounds. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 ++-- src/cbmc/symex_bmc.cpp | 3 ++- src/cbmc/symex_bmc.h | 16 +++++++++------- src/goto-symex/goto_symex.h | 1 + src/goto-symex/symex_goto.cpp | 3 ++- 5 files changed, 16 insertions(+), 11 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 787d47579f3..e6f4242de56 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -479,12 +479,12 @@ int jbmc_parse_optionst::doit() configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) { bmc.add_loop_unwind_handler( [&symbol_table]( - const irep_idt &function_id, + const goto_symex_statet::call_stackt &context, unsigned loop_number, unsigned unwind, unsigned &max_unwind) { return java_enum_static_init_unwind_handler( - function_id, + context, loop_number, unwind, max_unwind, diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 8a6424c0e5d..09de639997e 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -106,6 +106,7 @@ void symex_bmct::merge_goto( bool symex_bmct::get_unwind( const symex_targett::sourcet &source, + const goto_symex_statet::call_stackt &context, unsigned unwind) { const irep_idt id=goto_programt::loop_id(*source.pc); @@ -117,7 +118,7 @@ bool symex_bmct::get_unwind( { abort_unwind_decision = handler( - source.pc->function, + context, source.pc->loop_number, unwind, this_loop_limit); diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index 07e7b5fca63..9b6e9b5fd77 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -35,14 +35,15 @@ class symex_bmct: public goto_symext // To show progress source_locationt last_source_location; - /// Loop unwind handlers take the function ID and loop number, the unwind - /// count so far, and an out-parameter specifying an advisory maximum, which - /// they may set. If set the advisory maximum is set it is *only* used to - /// print useful information for the user (e.g. "unwinding iteration N, max - /// M"), and is not enforced. They return true to halt unwinding, false to - /// authorise unwinding, or Unknown to indicate they have no opinion. + /// Loop unwind handlers take the call stack, loop number, the unwind count so + /// far, and an out-parameter specifying an advisory maximum, which they may + /// set. If set the advisory maximum is set it is *only* used to print useful + /// information for the user (e.g. "unwinding iteration N, max M"), and is not + /// enforced. They return true to halt unwinding, false to authorise + /// unwinding, or Unknown to indicate they have no opinion. typedef - std::function + std::function loop_unwind_handlert; /// Recursion unwind handlers take the function ID, the unwind count so far, @@ -105,6 +106,7 @@ class symex_bmct: public goto_symext // for loop unwinding virtual bool get_unwind( const symex_targett::sourcet &source, + const goto_symex_statet::call_stackt &context, unsigned unwind); virtual bool get_unwind_recursion( diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 8f27a3c0e02..0e253b28eb7 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -328,6 +328,7 @@ class goto_symext // with false we continue. virtual bool get_unwind( const symex_targett::sourcet &source, + const goto_symex_statet::call_stackt &context, unsigned unwind); virtual void loop_bound_exceeded(statet &, const exprt &guard); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 0fed1309ce1..ca7008f7385 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -86,7 +86,7 @@ void goto_symext::symex_goto(statet &state) unwind++; // continue unwinding? - if(get_unwind(state.source, unwind)) + if(get_unwind(state.source, state.call_stack(), unwind)) { // no! loop_bound_exceeded(state, new_guard); @@ -540,6 +540,7 @@ void goto_symext::loop_bound_exceeded( bool goto_symext::get_unwind( const symex_targett::sourcet &source, + const goto_symex_statet::call_stackt &context, unsigned unwind) { // by default, we keep going From 627096804af3610763d0b31938fa12d26d7db432 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 1 Aug 2018 12:36:03 +0100 Subject: [PATCH 2/6] java-unwind-enum-static: also unwind clone loop in Enum.values() If an enumeration type's values() method clones an array, we assume it is cloning the array of enumeration values and therefore is bounded by the enumeration's size, similar to the existing handling of enumeration static initializers. --- .../java_enum_static_init_unwind_handler.cpp | 49 ++++++++++++++++--- .../java_enum_static_init_unwind_handler.h | 4 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 6 +-- src/cbmc/symex_bmc.cpp | 6 +-- 4 files changed, 47 insertions(+), 18 deletions(-) diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp index d9d48bbf9e7..9c69e5eb056 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp @@ -14,12 +14,47 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +/// Check if we may be in a function that loops over the cases of an +/// enumeration (note we return a candidate function that matches a pattern; +/// our caller must verify it really belongs to an enumeration). +/// At the moment we know of two cases that definitely do so: +/// * An enumeration type's static initialiser +/// * The array[reference].clone() method when called from an enumeration type's +/// 'values()' method +/// \param context: the current call stack +/// \return the name of an enclosing function that may be defined on the +/// relevant enum type, or an empty string if we don't find one. +static irep_idt +find_enum_function_on_stack(const goto_symex_statet::call_stackt &context) +{ + static irep_idt reference_array_clone_id = + "java::array[reference].clone:()Ljava/lang/Object;"; + + PRECONDITION(!context.empty()); + const irep_idt ¤t_function = context.back().function_identifier; + + if(context.size() >= 2 && current_function == reference_array_clone_id) + { + const irep_idt &clone_caller = + context.at(context.size() - 2).function_identifier; + if(id2string(clone_caller).find(".values:()[L") != std::string::npos) + return clone_caller; + else + return irep_idt(); + } + else if(has_suffix(id2string(current_function), ".:()V")) + return current_function; + else + return irep_idt(); +} + /// Unwind handler that special-cases the clinit (static initializer) functions -/// of enumeration classes. When java_bytecode_convert_classt has annotated them +/// of enumeration classes, and VALUES array cloning in their values() methods. +/// When java_bytecode_convert_classt has annotated them /// with a size of the enumeration type, this forces unwinding of any loop in /// the static initializer to at least that many iterations, with intent to -/// permit population of the enumeration's value array. -/// \param function_id: function the loop is in +/// permit population / copying of the enumeration's value array. +/// \param context: call stack when the loop back-edge was taken /// \param loop_number: ordinal number of the loop (ignored) /// \param unwind_count: iteration count that is about to begin /// \param [out] unwind_max: may be set to an advisory (unenforced) maximum when @@ -29,17 +64,17 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// unwind_count is <= the enumeration size, or unknown (defer / no decision) /// otherwise. tvt java_enum_static_init_unwind_handler( - const irep_idt &function_id, + const goto_symex_statet::call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table) { - const std::string &function_str = id2string(function_id); - if(!has_suffix(function_str, ".:()V")) + const irep_idt enum_function_id = find_enum_function_on_stack(context); + if(enum_function_id.empty()) return tvt::unknown(); - const symbolt &function_symbol = symbol_table.lookup_ref(function_str); + const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id); irep_idt class_id = function_symbol.type.get(ID_C_class); INVARIANT( !class_id.empty(), "functions should have their defining class annotated"); diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h index 489a638526f..586fbf98c25 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h @@ -12,11 +12,13 @@ Author: Chris Smowton, chris.smowton@diffblue.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H #define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H +#include + #include #include tvt java_enum_static_init_unwind_handler( - const irep_idt &function_id, + const goto_symex_statet::call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index e6f4242de56..cdcb16b6062 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -484,11 +484,7 @@ int jbmc_parse_optionst::doit() unsigned unwind, unsigned &max_unwind) { return java_enum_static_init_unwind_handler( - context, - loop_number, - unwind, - max_unwind, - symbol_table); + context, loop_number, unwind, max_unwind, symbol_table); }); }; } diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 09de639997e..e455dfa2913 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -117,11 +117,7 @@ bool symex_bmct::get_unwind( for(auto handler : loop_unwind_handlers) { abort_unwind_decision = - handler( - context, - source.pc->loop_number, - unwind, - this_loop_limit); + handler(context, source.pc->loop_number, unwind, this_loop_limit); if(abort_unwind_decision.is_known()) break; } From 361469b8b8982a3bf046c48999dd0c5f7a0f6990 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 6 Jul 2018 07:46:52 +0200 Subject: [PATCH 3/6] Change source location of jump target in {table|lookup}switch Before we considered the `code_switch_caset` to belong to the target instruction which lead to uncoverable goals of the form: IF condition 1 then GOTO 1 ... 1: GOTO 2 ASSERT false // uncoverable block ... 2: --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 651ab62c0ce..1b976187797 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1959,9 +1959,12 @@ codet java_bytecode_convert_methodt::convert_switch( mp_integer number; bool ret = to_integer(to_constant_expr(*a_it), number); DATA_INVARIANT(!ret, "case label expected to be integer"); + // The switch case does not contain any code, it just branches via a GOTO + // to the jump target of the tableswitch/lookupswitch case at + // hand. Therefore we consider this code to belong to the source bytecode + // instruction and not the target instruction. code_case.code() = code_gotot(label(integer2string(number))); - code_case.code().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + code_case.code().add_source_location() = location; if(a_it == args.begin()) code_case.set_default(); From a985eae854779e145ba1e80514f0dc1a200cd78d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 11 Jul 2018 10:37:33 +0100 Subject: [PATCH 4/6] Interpreter: deal with member-of-constant-struct expressions It could already do index-of-constant-array -- by replacing its custom code with simplify_expr we can expand that to also support member-of-constant-struct, as occurs when symex's deref'ing and then the interpreter's environment translate a variable-length array type like int[obj->length] into int[particular_object.length] and then int[{.length = 1, .data = &xyz}.length]. --- src/goto-programs/interpreter_evaluate.cpp | 69 +++++++++------------- 1 file changed, 28 insertions(+), 41 deletions(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 8a1941af60f..b53af16a95f 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -894,52 +895,38 @@ void interpretert::evaluate( mp_integer address=evaluate_address( expr, true); // fail quietly - if(address.is_zero() && expr.id()==ID_index) + if(address.is_zero()) { - // Try reading from a constant array: - mp_vectort idx; - evaluate(expr.op1(), idx); - if(idx.size()==1) + exprt simplified; + // In case of being an indexed access, try to evaluate the index, then + // simplify. + if(expr.id() == ID_index) { - mp_integer read_from_index=idx[0]; - if(expr.op0().id()==ID_array) + exprt evaluated_index = expr; + mp_vectort idx; + evaluate(expr.op1(), idx); + if(idx.size() == 1) { - const auto &ops=expr.op0().operands(); - DATA_INVARIANT(read_from_index.is_long(), "index is too large"); - if(read_from_index>=0 && read_from_index Date: Tue, 17 Jul 2018 12:27:20 +0200 Subject: [PATCH 5/6] Add regression tests for changes to JBMC enumeration support Update regression tests --- .../com/diffblue/regression/Foo$1.class | Bin 0 -> 730 bytes .../com/diffblue/regression/Foo.class | Bin 0 -> 715 bytes .../com/diffblue/regression/Foo.java | 16 ++++++++++++++++ .../com/diffblue/regression/MyEnum.class | Bin 0 -> 1070 bytes .../com/diffblue/regression/MyEnum.java | 5 +++++ jbmc/regression/jbmc/enum_switch/test.desc | 10 ++++++++++ .../com/diffblue/regression/EnumIter.class | Bin 0 -> 574 bytes .../com/diffblue/regression/EnumIter.java | 8 ++++++++ .../com/diffblue/regression/MyEnum.class | Bin 0 -> 1070 bytes .../com/diffblue/regression/MyEnum.java | 5 +++++ .../regression/jbmc/enum_values_clone/test.desc | 7 +++++++ .../com/diffblue/regression/EnumIter.class | Bin 0 -> 699 bytes .../com/diffblue/regression/EnumIter.java | 7 +++++++ .../com/diffblue/regression/MyEnum.class | Bin 0 -> 1070 bytes .../com/diffblue/regression/MyEnum.java | 5 +++++ .../jbmc/enum_values_clone_name/test.desc | 7 +++++++ 16 files changed, 70 insertions(+) create mode 100644 jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class create mode 100644 jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class create mode 100644 jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java create mode 100644 jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class create mode 100644 jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java create mode 100644 jbmc/regression/jbmc/enum_switch/test.desc create mode 100644 jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class create mode 100644 jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java create mode 100644 jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class create mode 100644 jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java create mode 100644 jbmc/regression/jbmc/enum_values_clone/test.desc create mode 100644 jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class create mode 100644 jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java create mode 100644 jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.class create mode 100644 jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java create mode 100644 jbmc/regression/jbmc/enum_values_clone_name/test.desc diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class new file mode 100644 index 0000000000000000000000000000000000000000..56f0ef4b05aa42166704353dff4f4d8b10d096fe GIT binary patch literal 730 zcmah{&2G~`5dJoCY{$6NlmelpZ6Kye0AYbZ96(4AB~nGw9)ilDr;WW$wsm%qe~Nek zUWGFtA%svLfQLeiElN%l$@BBg&V1{c*`L3@p8|M7(2#o(;PV9{bgxB3ql+#RJv(u;YTij=`yuIn%7YThpl|10dH?Y$m&KFcZ7hm-&3}f#jj8`Qz3Dy?SB50QI6P4GoO0TJg23oX@ z8rpb>$7HKmCStRsH{p?AA-PnF`NqNuMt>D0UoI0?afPgbtE8JG4wc(v;n}|d+Qy|^ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class new file mode 100644 index 0000000000000000000000000000000000000000..c7dfc05289a441e993bc6fcfff4dd5432d7c8953 GIT binary patch literal 715 zcmah{O>fgc5PfUMb`o3&1q!5X+JFy9Tg4!8E8>jushvTfy#jyD}g%$ov1gn=}4s~aun0EIxvxpPi3l0d+Ds? z=b9LsgUC$7v7Ssu@l1uOI!jfSX_JJ9#_SV%VvNAk&b47jpI#@k>3+8_Ajq}-zd(VN zVJ@S0NAmr$lKRlh(nuZZveqhTdl&M9^if64$0k}HwtQ@(EwFw=tpbfQEsSMy79Ni- zRFt#38xn%&0^MNvQRmS)iwPJST+Jc)H-})+pn&z3Ew-)$yo&NnI@XDd=S%6MjS9C} zeiqmqYLs}0TS_+=W1E{e_fvuCx=p4gkYy8RVuJ2NCkgRW=?Zo!ttqg?|4Lcn zj7GE1{!zyJ9>lR|WUuMFx$mBP?z#89pTEBT08qr!I3yG_Y~X={IRy_jq_D|1L&cOv zL4zZA1Np@umgsrsvWeA6SvuHcs<7momS{{I&R<_uRa|5y>^LU z&*-nv|C~Wts~uF|9GVQvZ^viKXBLrm7*=!n8^EPXaN;l|tFG_7?zJ0Ecx*L1I#C4A zQInyVtDahCmf=}`%P_m4>$ghz@j}woz_z@a6}p^o$SV0(o5<6DGcw3!*LS;n472|z z_%dH(khMU-$E#K<)LSl;Mct9=N-Y|J*gqjbtJWlBzjaxH=UT8ZnT;6$Na0{Ef zX&tlts^@g<;xWVG|1VBQ7Eg36V@1al(mJO3mf_nB(hQSVbL7$(Vzw9fR5FvxkH|i1 zoH}-wWbKX)qT*SdPH6=8=PItVmiD*kwWa9E#`fpA41g>t5thUVOL~CR0&kCy65_ap zc`z)Hw?dXLtq=AYkxN8BlE-kHc3H%tgwNv65MM+@oN8&Q@CC6;NE{!zhF_!;eSpGU zEQvVHiBP=aHlp+aN?{{=0r`^%kCwYiSFp;ZV@+Vzq2eCaheF;{BYYiygH%r|(F>^O zhzm!Pgp&}C9uv-la3*EpB$e-!6z$XNs!M$&%zCVk39~Nuku=Z2xTe7fG!o56RwT)h Mp^p2=(OCrf-~YJZF8}}l literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc new file mode 100644 index 00000000000..388c92dc1d4 --- /dev/null +++ b/jbmc/regression/jbmc/enum_switch/test.desc @@ -0,0 +1,10 @@ +CORE +com/diffblue/regression/Foo.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static +line 8.*SATISFIED +line 10.*SATISFIED +line 12.*SATISFIED +line 14.*SATISFIED +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class new file mode 100644 index 0000000000000000000000000000000000000000..e977adcf00c9274a706a504a980af2dbb92f6807 GIT binary patch literal 574 zcma)3%TB^T6g^W4)mk1Rz7at;Ac;+kJ0BaP2}#w3hJ|jNmH~&9HYt?Ee{$nSjSD}( zk22mVxFkBwoO|c?o-=1=zP>*`0UTo6L>kK`R>U7spNC-k`A=8;tEX;B|N$|1v!PmC{Q;s%$qQdJaHkFlkBhPexHxIg$xV>n-4R6Kni+); oC*^0VYfxIbq(@H-6iHcWRwulvrj7#gH0gzjvzQ>mQle1$0XQmmx&QzG literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java new file mode 100644 index 00000000000..bc5d1f617b6 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java @@ -0,0 +1,8 @@ +package com.diffblue.regression; +public class EnumIter { + int f() { + MyEnum[] a = MyEnum.values(); + int num = a[2].ordinal() + a[3].ordinal(); + return num ; + } +} diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class new file mode 100644 index 0000000000000000000000000000000000000000..c513fb41e02a38725d4c3cf7711ac015bfbe6e9d GIT binary patch literal 1070 zcma)4?{Csj6g>}0TS_+=W1E{e_fvuCx=p4gkYy8RVuJ2NCkgRW=?Zo!ttqg?|4Lcn zj7GE1{!zyJ9>lR|WUuMFx$mBP?z#89pTEBT08qr!I3yG_Y~X={IRy_jq_D|1L&cOv zL4zZA1Np@umgsrsvWeA6SvuHcs<7momS{{I&R<_uRa|5y>^LU z&*-nv|C~Wts~uF|9GVQvZ^viKXBLrm7*=!n8^EPXaN;l|tFG_7?zJ0Ecx*L1I#C4A zQInyVtDahCmf=}`%P_m4>$ghz@j}woz_z@a6}p^o$SV0(o5<6DGcw3!*LS;n472|z z_%dH(khMU-$E#K<)LSl;Mct9=N-Y|J*gqjbtJWlBzjaxH=UT8ZnT;6$Na0{Ef zX&tlts^@g<;xWVG|1VBQ7Eg36V@1al(mJO3mf_nB(hQSVbL7$(Vzw9fR5FvxkH|i1 zoH}-wWbKX)qT*SdPH6=8=PItVmiD*kwWa9E#`fpA41g>t5thUVOL~CR0&kCy65_ap zc`z)Hw?dXLtq=AYkxN8BlE-kHc3H%tgwNv65MM+@oN8&Q@CC6;NE{!zhF_!;eSpGU zEQvVHiBP=aHlp+aN?{{=0r`^%kCwYiSFp;ZV@+Vzq2eCaheF;{BYYiygH%r|(F>^O zhzm!Pgp&}C9uv-la3*EpB$e-!6z$XNs!M$&%zCVk39~Nuku=Z2xTe7fG!o56RwT)h Mp^p2=(OCrf-~YJZF8}}l literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc new file mode 100644 index 00000000000..3a6767f173e --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/test.desc @@ -0,0 +1,7 @@ +CORE +com/diffblue/regression/EnumIter.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static +\d+ of \d+ covered \(100\.0%\) +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class new file mode 100644 index 0000000000000000000000000000000000000000..3c7ca188bc99aa4392d2c79d5c4b9a1cf147c53e GIT binary patch literal 699 zcma))+fLg+5QhJ892<<&&=3wi1QIBafT*RacSXHu)k>Az_97J$;%bv@!Xn2;jva}& zf}4Pf!~^h9sIzveN{vwKi#hGi=b7KWfB1O^;4O9?%wyHT8lKsB?x2t-FLd-$o0^Sv z8yf`cP=zXaPbf57M+Ea@)RTm=uR{4P9d=~=Lv#YJRQ#wbf+G7?}0TS_+=W1E{e_fvuCx=p4gkYy8RVuJ2NCkgRW=?Zo!ttqg?|4Lcn zj7GE1{!zyJ9>lR|WUuMFx$mBP?z#89pTEBT08qr!I3yG_Y~X={IRy_jq_D|1L&cOv zL4zZA1Np@umgsrsvWeA6SvuHcs<7momS{{I&R<_uRa|5y>^LU z&*-nv|C~Wts~uF|9GVQvZ^viKXBLrm7*=!n8^EPXaN;l|tFG_7?zJ0Ecx*L1I#C4A zQInyVtDahCmf=}`%P_m4>$ghz@j}woz_z@a6}p^o$SV0(o5<6DGcw3!*LS;n472|z z_%dH(khMU-$E#K<)LSl;Mct9=N-Y|J*gqjbtJWlBzjaxH=UT8ZnT;6$Na0{Ef zX&tlts^@g<;xWVG|1VBQ7Eg36V@1al(mJO3mf_nB(hQSVbL7$(Vzw9fR5FvxkH|i1 zoH}-wWbKX)qT*SdPH6=8=PItVmiD*kwWa9E#`fpA41g>t5thUVOL~CR0&kCy65_ap zc`z)Hw?dXLtq=AYkxN8BlE-kHc3H%tgwNv65MM+@oN8&Q@CC6;NE{!zhF_!;eSpGU zEQvVHiBP=aHlp+aN?{{=0r`^%kCwYiSFp;ZV@+Vzq2eCaheF;{BYYiygH%r|(F>^O zhzm!Pgp&}C9uv-la3*EpB$e-!6z$XNs!M$&%zCVk39~Nuku=Z2xTe7fG!o56RwT)h Mp^p2=(OCrf-~YJZF8}}l literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_values_clone_name/test.desc b/jbmc/regression/jbmc/enum_values_clone_name/test.desc new file mode 100644 index 00000000000..b3641395f6a --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone_name/test.desc @@ -0,0 +1,7 @@ +CORE +com/diffblue/regression/EnumIter.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static +\d+ of \d+ covered \(100\.0%\) +^EXIT=0$ +^SIGNAL=0$ +-- From 4f158a3c59a0a06429e6fdd423a3ed0b10778334 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 31 Jul 2018 17:28:50 +0200 Subject: [PATCH 6/6] Mark regression tests as expecting failure for symex driven loading Currently the regression tests fail with symex driven lazy loading due to a difference in generated properties. --- jbmc/regression/jbmc/enum_switch/test.desc | 2 +- jbmc/regression/jbmc/enum_values_clone/test.desc | 2 +- jbmc/regression/jbmc/enum_values_clone_name/test.desc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc index 388c92dc1d4..f525e3e15d4 100644 --- a/jbmc/regression/jbmc/enum_switch/test.desc +++ b/jbmc/regression/jbmc/enum_switch/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure com/diffblue/regression/Foo.class --trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static line 8.*SATISFIED diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc index 3a6767f173e..7009afb0ed1 100644 --- a/jbmc/regression/jbmc/enum_values_clone/test.desc +++ b/jbmc/regression/jbmc/enum_values_clone/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure com/diffblue/regression/EnumIter.class --trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static \d+ of \d+ covered \(100\.0%\) diff --git a/jbmc/regression/jbmc/enum_values_clone_name/test.desc b/jbmc/regression/jbmc/enum_values_clone_name/test.desc index b3641395f6a..66031ef1e9d 100644 --- a/jbmc/regression/jbmc/enum_values_clone_name/test.desc +++ b/jbmc/regression/jbmc/enum_values_clone_name/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure com/diffblue/regression/EnumIter.class --trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static \d+ of \d+ covered \(100\.0%\)