diff --git a/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class new file mode 100644 index 00000000000..0fae31a44fb Binary files /dev/null and b/jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class differ 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 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 diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 1cb61aa55f0..874150b26b6 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -166,6 +166,24 @@ class java_object_factoryt code_blockt &assignments, 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, + 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. @@ -1198,55 +1216,113 @@ void java_object_factoryt::allocate_nondet_length_array( assignments.add(assign); } -/// 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 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 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 &expr, - size_t depth, - update_in_placet update_in_place, + const exprt &init_array_expr, + const exprt &length_expr, + const typet &element_type, + const exprt &max_length_expr, 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); + array_typet array_type(element_type, max_length_expr); - 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)); + // 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): +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// 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 &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) +{ const symbol_exprt &array_init_symexpr = allocate_objects.allocate_automatic_local_object( init_array_expr.type(), "array_data_init"); @@ -1322,6 +1398,82 @@ 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)); + + 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 /// for their type: /// int i = nondet(int); 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