From b497e389c1512f0d36b20d7cccbc7b6c752e641d Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 20 Dec 2018 18:07:09 +0000 Subject: [PATCH 1/5] Move make_allocate_code to java_object_factory Will also be used in java_object_factory --- jbmc/src/java_bytecode/java_object_factory.cpp | 12 ++++++++++++ jbmc/src/java_bytecode/java_object_factory.h | 2 ++ .../java_bytecode/java_string_library_preprocess.cpp | 12 ------------ 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 1cb61aa55f0..efa50fc7c45 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -1198,6 +1198,18 @@ void java_object_factoryt::allocate_nondet_length_array( assignments.add(assign); } +/// Create code allocating object of size `size` and assigning it to `lhs` +/// \param lhs : pointer which will be allocated +/// \param size : size of the object +/// \return code allocation object and assigning `lhs` +codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) +{ + side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); + alloc.add_to_operands(size); + alloc.add_to_operands(false_exprt()); + return code_assignt(lhs, alloc); +} + /// Create code to initialize a Java array whose size will be at most /// `max_nondet_array_length`. The code is emitted to \p assignments does as /// follows: diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index 93cfb77d5d4..db0bca45bc3 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -126,4 +126,6 @@ void gen_nondet_init( const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place); +codet make_allocate_code(const symbol_exprt &lhs, const exprt &size); + #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index be1c2b589d5..2f1c5e980b9 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -627,18 +627,6 @@ codet java_string_library_preprocesst::code_return_function_application( return code_returnt(fun_app); } -/// Create code allocating object of size `size` and assigning it to `lhs` -/// \param lhs : pointer which will be allocated -/// \param size : size of the object -/// \return code allocation object and assigning `lhs` -static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) -{ - side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); - alloc.add_to_operands(size); - alloc.add_to_operands(false_exprt()); - return code_assignt(lhs, alloc); -} - /// Declare a fresh symbol of type array of character with infinite size. /// \param symbol_table: the symbol table /// \param loc: source location From 0fce0baee06d87a8d4b948c04ac4b2ba0dc3daf8 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 21 Dec 2018 12:54:18 +0000 Subject: [PATCH 2/5] Factor loop init out of gen_nondet_array_init Makes gen_nondet_array_init smaller and clarifies process. --- .../src/java_bytecode/java_object_factory.cpp | 155 +++++++++++++----- 1 file changed, 111 insertions(+), 44 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index efa50fc7c45..1c447a48cdc 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -166,6 +166,16 @@ class java_object_factoryt code_blockt &assignments, const exprt &instance_expr, const irep_idt &method_name); + + void array_loop_init_code( + code_blockt &assignments, + const exprt &init_array_expr, + const exprt &length_expr, + const typet &element_type, + const exprt &max_length_expr, + size_t depth, + update_in_placet update_in_place, + const source_locationt &location); }; /// Returns a codet that assigns \p expr, of type \p ptr_type, a NULL value. @@ -1210,55 +1220,51 @@ codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) return code_assignt(lhs, alloc); } -/// Create code to initialize a Java array whose size will be at most -/// `max_nondet_array_length`. The code is emitted to \p assignments does as -/// follows: -/// 1. non-deterministically choose a length for the array -/// 2. assume that such length is >=0 and <= max_length -/// 3. loop through all elements of the array and initialize them -void java_object_factoryt::gen_nondet_array_init( +/// Create code to nondeterministically initialise each element of an array in a +/// loop. +/// The code produced is of the form (supposing an array of type OBJ): +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// struct OBJ **array_data_init; +/// int array_init_iter; +/// array_data_init = (struct OBJ **)init_array_expr; +/// array_init_iter = 0; +/// 2: IF array_init_iter == length_expr THEN GOTO 5 +/// IF array_init_iter == max_length_expr THEN GOTO 5 +/// IF !NONDET(__CPROVER_bool) THEN GOTO 3 +/// array_data_init[array_init_iter] = null; +/// GOTO 4 +/// 3: malloc_site = ALLOCATE(...); +/// array_data_init[array_init_iter] = (struct OBJ *)malloc_site; +/// *malloc_site = {...}; +/// malloc_site->value = NONDET(int); +/// 4: array_init_iter = array_init_iter + 1; +/// GOTO 2 +/// 5: ... +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// \param [out] assignments : Code block to which the initializing assignments +/// will be appended. +/// \param init_array_expr : array data +/// \param length_expr : array length +/// \param element_type: type of array elements +/// \param max_length_expr : max length, as specified by max-nondet-array-length +/// \param depth: Number of times that a pointer has been dereferenced from the +/// root of the object tree that we are initializing. +/// \param update_in_place: +/// NO_UPDATE_IN_PLACE: initialize `expr` from scratch +/// MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ +/// and MUST_ cases. +/// MUST_UPDATE_IN_PLACE: reinitialize an existing object +/// \param location: Source location associated with nondet-initialization. +void java_object_factoryt::array_loop_init_code( code_blockt &assignments, - const exprt &expr, + const exprt &init_array_expr, + const exprt &length_expr, + const typet &element_type, + const exprt &max_length_expr, size_t depth, update_in_placet update_in_place, const source_locationt &location) { - PRECONDITION(expr.type().id()==ID_pointer); - PRECONDITION(expr.type().subtype().id() == ID_struct_tag); - PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); - - const typet &type=ns.follow(expr.type().subtype()); - const struct_typet &struct_type=to_struct_type(type); - const typet &element_type = - static_cast(expr.type().subtype().find(ID_element_type)); - - auto max_length_expr=from_integer( - object_factory_parameters.max_nondet_array_length, java_int_type()); - - // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively - // initialize its elements - if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE) - { - allocate_nondet_length_array( - assignments, expr, max_length_expr, element_type, location); - } - - // Otherwise we're updating the array in place, and use the - // existing array allocation and length. - - INVARIANT( - is_valid_java_array(struct_type), - "Java struct array does not conform to expectations"); - - dereference_exprt deref_expr(expr, expr.type().subtype()); - const auto &comps=struct_type.components(); - const member_exprt length_expr(deref_expr, "length", comps[1].type()); - exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type()); - - if(init_array_expr.type()!=pointer_type(element_type)) - init_array_expr= - typecast_exprt(init_array_expr, pointer_type(element_type)); - const symbol_exprt &array_init_symexpr = allocate_objects.allocate_automatic_local_object( init_array_expr.type(), "array_data_init"); @@ -1334,6 +1340,67 @@ void java_object_factoryt::gen_nondet_array_init( assignments.add(std::move(init_done_label)); } +/// Create code to initialize a Java array whose size will be at most +/// `max_nondet_array_length`. The code is emitted to \p assignments does as +/// follows: +/// 1. non-deterministically choose a length for the array +/// 2. assume that such length is >=0 and <= max_length +/// 3. loop through all elements of the array and initialize them +void java_object_factoryt::gen_nondet_array_init( + code_blockt &assignments, + const exprt &expr, + size_t depth, + update_in_placet update_in_place, + const source_locationt &location) +{ + PRECONDITION(expr.type().id() == ID_pointer); + PRECONDITION(expr.type().subtype().id() == ID_struct_tag); + PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); + + const typet &type = ns.follow(expr.type().subtype()); + const struct_typet &struct_type = to_struct_type(type); + const typet &element_type = + static_cast(expr.type().subtype().find(ID_element_type)); + + auto max_length_expr = from_integer( + object_factory_parameters.max_nondet_array_length, java_int_type()); + + // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively + // initialize its elements + if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE) + { + allocate_nondet_length_array( + assignments, expr, max_length_expr, element_type, location); + } + + // Otherwise we're updating the array in place, and use the + // existing array allocation and length. + + INVARIANT( + is_valid_java_array(struct_type), + "Java struct array does not conform to expectations"); + + dereference_exprt deref_expr(expr, expr.type().subtype()); + const auto &comps = struct_type.components(); + const member_exprt length_expr(deref_expr, "length", comps[1].type()); + exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type()); + + if(init_array_expr.type() != pointer_type(element_type)) + init_array_expr = + typecast_exprt(init_array_expr, pointer_type(element_type)); + + // Nondeterministically initialise each element of the array + array_loop_init_code( + assignments, + init_array_expr, + length_expr, + element_type, + max_length_expr, + depth, + update_in_place, + location); +} + /// We nondet-initialize enums to be equal to one of the constants defined /// for their type: /// int i = nondet(int); From 6f851a9dce7601ef7a1ce3ef4031dd5dd3bc1105 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 21 Dec 2018 17:12:57 +0000 Subject: [PATCH 3/5] Initialize nondet arrays with a single NONDET Get rid of the initilization loop for nondet arrays, so the size of nondeterministic arrays of primitive types no longer depend on the max unwind value. --- .../src/java_bytecode/java_object_factory.cpp | 95 ++++++++++++++++--- 1 file changed, 84 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 1c447a48cdc..874150b26b6 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -167,6 +167,14 @@ class java_object_factoryt const exprt &instance_expr, const irep_idt &method_name); + void array_primitive_init_code( + code_blockt &assignments, + const exprt &init_array_expr, + const exprt &length_expr, + const typet &element_type, + const exprt &max_length_expr, + const source_locationt &location); + void array_loop_init_code( code_blockt &assignments, const exprt &init_array_expr, @@ -1220,7 +1228,57 @@ codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) return code_assignt(lhs, alloc); } -/// Create code to nondeterministically initialise each element of an array in a +/// Create code to nondeterministically initialize arrays of primitive type. +/// The code produced is of the form (for an array of type TYPE): +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// TYPE (*array_data_init)[max_length_expr]; +/// array_data_init = +/// ALLOCATE(TYPE [max_length_expr], max_length_expr, false); +/// *array_data_init = NONDET(TYPE [max_length_expr]); +/// init_array_expr = *array_data_init; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// \param [out] assignments : Code block to which the initializing assignments +/// will be appended. +/// \param init_array_expr : array data +/// \param length_expr : array length +/// \param element_type: type of array elements +/// \param max_length_expr : the (constant) size to which initialise the array +/// \param location: Source location associated with nondet-initialization. +void java_object_factoryt::array_primitive_init_code( + code_blockt &assignments, + const exprt &init_array_expr, + const exprt &length_expr, + const typet &element_type, + const exprt &max_length_expr, + const source_locationt &location) +{ + array_typet array_type(element_type, max_length_expr); + + // TYPE (*array_data_init)[max_length_expr]; + const symbol_exprt &tmp_finite_array_pointer = + allocate_objects.allocate_automatic_local_object( + pointer_type(array_type), "array_data_init"); + + // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false); + assignments.add( + make_allocate_code( + tmp_finite_array_pointer, + max_length_expr)); + + // *array_data_init = NONDET(TYPE [max_length_expr]); + const exprt nondet_data=side_effect_expr_nondett(array_type, loc); + const exprt data_pointer_deref=dereference_exprt( + tmp_finite_array_pointer, + array_type); + assignments.add(code_assignt(data_pointer_deref, nondet_data)); + + // init_array_expr = *array_data_init; + address_of_exprt tmp_nondet_pointer( + index_exprt(data_pointer_deref, from_integer(0, java_int_type()))); + assignments.add(code_assignt(init_array_expr, tmp_nondet_pointer)); +} + +/// Create code to nondeterministically initialize each element of an array in a /// loop. /// The code produced is of the form (supposing an array of type OBJ): /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1389,16 +1447,31 @@ void java_object_factoryt::gen_nondet_array_init( init_array_expr = typecast_exprt(init_array_expr, pointer_type(element_type)); - // Nondeterministically initialise each element of the array - array_loop_init_code( - assignments, - init_array_expr, - length_expr, - element_type, - max_length_expr, - depth, - update_in_place, - location); + if(element_type.id() == ID_pointer) + { + // For arrays of non-primitive types, nondeterministically initialize each + // element of the array + array_loop_init_code( + assignments, + init_array_expr, + length_expr, + element_type, + max_length_expr, + depth, + update_in_place, + location); + } + else + { + // Arrays of primitive types can be initialized with a single instruction + array_primitive_init_code( + assignments, + init_array_expr, + length_expr, + element_type, + max_length_expr, + location); + } } /// We nondet-initialize enums to be equal to one of the constants defined From 9041b6eb0f2a7b88b2225bf82ff740deefe2d27c Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Mon, 31 Dec 2018 10:17:23 +0000 Subject: [PATCH 4/5] Tests for loop-less array init --- .../NondetArrayPrimitive.class | Bin 0 -> 1496 bytes .../NondetArrayPrimitive.java | 69 ++++++++++++++++++ .../jbmc/NondetArrayPrimitive/boolArray.desc | 12 +++ .../jbmc/NondetArrayPrimitive/byteArray.desc | 12 +++ .../jbmc/NondetArrayPrimitive/charArray.desc | 12 +++ .../NondetArrayPrimitive/doubleArray.desc | 12 +++ .../jbmc/NondetArrayPrimitive/floatArray.desc | 12 +++ .../jbmc/NondetArrayPrimitive/intArray.desc | 12 +++ .../NondetArrayPrimitive/intArrayMulti.desc | 12 +++ .../jbmc/NondetArrayPrimitive/longArray.desc | 12 +++ .../jbmc/NondetArrayPrimitive/shortArray.desc | 12 +++ 11 files changed, 177 insertions(+) create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc create mode 100644 jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class new file mode 100644 index 0000000000000000000000000000000000000000..0fae31a44fb9695a12f98425747123378020fddb GIT binary patch literal 1496 zcma)+O-~a+7{~w9b}4-UTByjoLJKV|P$;M|K?4>@G=dlmiE!Gs3oI^Ov)z*LA-tKG zaPmOnSxqF-q~1LE8T>59|Fm1$gUNQA?94v%%y0hB%k=l(?==7`$OREXDu4iH{YVGl zMXGCUlS_P*#(=aRnIPsc@5h3`KtiolG|Se_a%DrWs0BkS35WxMu2sFP+m8jjso8x2 zU*0Tf0)5Z*vbIw_D`?g$=`7H#m+f`SQZEFQ)ZtU<+p}k@#W&mPTgN4MWSDB3)0T7! z6i-yEwJ|Skp^{l8v}N6>dm3i>xMh1LZNbWkX|*Bu>W+mAyKVE6hRrmM*5(6g>uE~f zt{S$^P*aBu;oYl6!-+b$XI8DEwx!D$hj+|!NoyRpYw2gYt)FWPr|P*HMlbrp2%|?} zNE)(+T0YLMHAC|Cf53F+ z7vh;(RQYp-(F})$Nctn9U*Ne!=m)&7ui^VCQJy-gm+dCoY>?0dx)I}-7b3yo7L5(| zOZe*S6xlNldqT1o-^HMOxOBsZG0fnS49meMiNB2@H|Z;pBUkAIR2idm`M!}pj1h;u z>qt*h`m`f`TuNW+Ncjjwj$(#|aOg8UWE5j=^lS|N_pW)FBz=nXL_2*P6K;9A*Fi~B z%*ZUsnI>D7^bR}DrCpXgU}wo*Bsp#uqBEJAa>b%5xmqN5g)vSdxlX$M5i`8bKhu2kj5#*`^v$JP;aT#D j_6NQpcnQDn6MWvU@U(7C^8(7IP~Zu#$!jWG!-M2M4u}9F literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java new file mode 100644 index 00000000000..7abf3d830ee --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java @@ -0,0 +1,69 @@ +class NondetArrayPrimitive +{ + void intArray(int[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42) { + assert false; + } + } + + void floatArray(float[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42.0) { + assert false; + } + } + + void charArray(char[] array) + { + if (array != null && array.length > 1500 && array[1500] == 'f') { + assert false; + } + } + + void doubleArray(double[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42.0) { + assert false; + } + } + + void longArray(long[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42) { + assert false; + } + } + + void shortArray(short[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42) { + assert false; + } + } + + void byteArray(byte[] array) + { + if (array != null && array.length > 1500 && array[1500] == 42) { + assert false; + } + } + + void boolArray(boolean[] array) + { + if (array != null && array.length > 1500 && array[1500] == true) { + assert false; + } + } + + void intArrayMulti(int[][] array) + { + if (array != null && + array.length > 2 && + array[2].length > 50 && + array[2][50] == 42) { + assert false; + } + } + +} diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc new file mode 100644 index 00000000000..ab6596fc47e --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.boolArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 55 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc new file mode 100644 index 00000000000..aa7a57554a1 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.byteArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 48 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc new file mode 100644 index 00000000000..6fcac7b8670 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.charArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 20 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc new file mode 100644 index 00000000000..51a2bbc971a --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.doubleArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 27 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc new file mode 100644 index 00000000000..3374523efe3 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.floatArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 13 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc new file mode 100644 index 00000000000..a286df87a20 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.intArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 6 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc new file mode 100644 index 00000000000..763fa89ce93 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.intArrayMulti --max-nondet-array-length 51 --unwind 4 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 65 assertion.*: FAILURE +-- +^warning: ignoring +-- +Check inner most array of multi-dimensional array is reachable independently of +--unwind value. diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc new file mode 100644 index 00000000000..977daeb96b2 --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.longArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 34 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc b/jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc new file mode 100644 index 00000000000..b34e8e8c14d --- /dev/null +++ b/jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc @@ -0,0 +1,12 @@ +CORE +NondetArrayPrimitive.class +--function NondetArrayPrimitive.shortArray --max-nondet-array-length 2000 --unwind 1 +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +line 41 assertion.*: FAILURE +-- +Unwinding loop __CPROVER__start.0 iteration 2 +^warning: ignoring +-- +Check no unwind needed to reach non-primitive array cell From 2d24bbd3de264994718ee271c0a4a1a2226ab906 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Mon, 31 Dec 2018 10:18:39 +0000 Subject: [PATCH 5/5] Update trace test Array variable name is now of type "dynamic_object" for primitive arrays. "dynamic_N_array" is a name generated by symex_cpp_new when loop-initializing arrays (in remove_java_newt::lower_java_new_array). We no longer loop-initialize primitive arrays. --- jbmc/regression/jbmc/json_trace3/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc/json_trace3/test.desc b/jbmc/regression/jbmc/json_trace3/test.desc index 830295e9eaa..8cedd7690f8 100644 --- a/jbmc/regression/jbmc/json_trace3/test.desc +++ b/jbmc/regression/jbmc/json_trace3/test.desc @@ -4,7 +4,7 @@ Test.class activate-multi-line-match EXIT=10 SIGNAL=0 -"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64 +"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64 -- "name": "unknown" ^warning: ignoring