diff --git a/regression/cbmc-java/external_getstatic1/test.class b/regression/cbmc-java/external_getstatic1/test.class new file mode 100644 index 00000000000..ec38ad69385 Binary files /dev/null and b/regression/cbmc-java/external_getstatic1/test.class differ diff --git a/regression/cbmc-java/external_getstatic1/test.desc b/regression/cbmc-java/external_getstatic1/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/cbmc-java/external_getstatic1/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/external_getstatic1/test.java b/regression/cbmc-java/external_getstatic1/test.java new file mode 100644 index 00000000000..5b3f3bdb9b2 --- /dev/null +++ b/regression/cbmc-java/external_getstatic1/test.java @@ -0,0 +1,16 @@ +class A +{ + public static A external_global; + public int i; +}; + +public class test +{ + public static void main() + { + if(A.external_global == null) + return; + A local = A.external_global; + assert(local instanceof A); + } +} diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index bd878d4cc4c..5b7935470ef 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -85,7 +85,7 @@ static goto_programt::targett insert_nondet_init_code( symbol_table, source_loc, true, - true, + allocation_typet::DYNAMIC, !nullable, max_nondet_array_length, update_in_placet::NO_UPDATE_IN_PLACE); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9494fd2539b..3cb2cc2861d 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2014,6 +2014,10 @@ codet java_bytecode_convert_methodt::convert_instructions( const bool is_assertions_disabled_field= field_name.find("$assertionsDisabled")!=std::string::npos; symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + + // If external, create a symbol table entry for this static field: + check_static_field_stub(symbol_expr, field_name); + if(lazy_methods) { if(arg0.type().id()==ID_symbol) @@ -2056,6 +2060,10 @@ codet java_bytecode_convert_methodt::convert_instructions( symbol_exprt symbol_expr(arg0.type()); const auto &field_name=arg0.get_string(ID_component_name); symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + + // If external, create a symbol table entry for this static field: + check_static_field_stub(symbol_expr, field_name); + if(lazy_methods && arg0.type().id()==ID_symbol) { lazy_methods->add_needed_class( diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index b41e1e73baf..79b89eebe60 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -113,6 +113,7 @@ codet java_bytecode_instrumentt::throw_exception( false, symbol_table, max_array_length, + allocation_typet::LOCAL, original_loc); } else diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 6f6ebd5f149..adb48d98444 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -118,6 +118,7 @@ void java_static_lifetime_init( allow_null, symbol_table, max_nondet_array_length, + allocation_typet::GLOBAL, source_location); code_assignt assignment(sym.symbol_expr(), newsym); code_block.add(assignment); @@ -180,6 +181,7 @@ exprt::operandst java_build_arguments( allow_null, symbol_table, max_nondet_array_length, + allocation_typet::LOCAL, function.location); // record as an input diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index e8b6e92308f..5559dfaf714 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -70,7 +70,7 @@ class java_object_factoryt code_blockt &assignments, const exprt &expr, const typet &target_type, - bool create_dynamic_objects, + allocation_typet alloc_type, update_in_placet update_in_place); void allocate_nondet_length_array( @@ -98,7 +98,7 @@ class java_object_factoryt code_blockt &assignments, const exprt &, const typet &, - bool create_dynamic_objects); + allocation_typet alloc_type); void gen_nondet_array_init( code_blockt &assignments, @@ -111,7 +111,7 @@ class java_object_factoryt bool is_sub, irep_idt class_identifier, bool skip_classid, - bool create_dynamic_objects, + allocation_typet alloc_type, bool override, const typet &override_type, update_in_placet); @@ -121,7 +121,7 @@ class java_object_factoryt code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, - bool create_dynamic_objects, + allocation_typet alloc_type, const pointer_typet &pointer_type, const update_in_placet &update_in_place); @@ -131,13 +131,13 @@ class java_object_factoryt bool is_sub, irep_idt class_identifier, bool skip_classid, - bool create_dynamic_objects, + allocation_typet alloc_type, const struct_typet &struct_type, const update_in_placet &update_in_place); symbol_exprt gen_nondet_subtype_pointer_init( code_blockt &assignments, - bool create_dynamic_objects, + allocation_typet alloc_type, const pointer_typet &substitute_pointer_type); }; @@ -257,43 +257,51 @@ exprt allocate_dynamic_object_with_decl( /// \param assignments: The code block to add code to /// \param target_expr: The expression which we are allocating a symbol for /// \param allocate_type: -/// \param create_dynamic_objects: Whether to create a symbol with static -/// lifetime or +/// \param alloc_type: Allocation type (global, local or dynamic) /// \return the allocated object exprt java_object_factoryt::allocate_object( code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, - bool create_dynamic_objects) + allocation_typet alloc_type) { const typet &allocate_type_resolved=ns.follow(allocate_type); const typet &target_type=ns.follow(target_expr.type().subtype()); bool cast_needed=allocate_type_resolved!=target_type; - if(!create_dynamic_objects) + switch(alloc_type) { - symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type); - symbols_created.push_back(&aux_symbol); - - exprt object=aux_symbol.symbol_expr(); - exprt aoe=address_of_exprt(object); - if(cast_needed) - aoe=typecast_exprt(aoe, target_expr.type()); - code_assignt code(target_expr, aoe); - code.add_source_location()=loc; - assignments.copy_to_operands(code); - return aoe; - } - else - { - return allocate_dynamic_object( - target_expr, - allocate_type, - symbol_table, - loc, - assignments, - symbols_created, - cast_needed); - } + case allocation_typet::LOCAL: + case allocation_typet::GLOBAL: + { + symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type); + if(alloc_type==allocation_typet::GLOBAL) + aux_symbol.is_static_lifetime=true; + symbols_created.push_back(&aux_symbol); + + exprt object=aux_symbol.symbol_expr(); + exprt aoe=address_of_exprt(object); + if(cast_needed) + aoe=typecast_exprt(aoe, target_expr.type()); + code_assignt code(target_expr, aoe); + code.add_source_location()=loc; + assignments.copy_to_operands(code); + return aoe; + } + case allocation_typet::DYNAMIC: + { + return allocate_dynamic_object( + target_expr, + allocate_type, + symbol_table, + loc, + assignments, + symbols_created, + cast_needed); + } + default: + UNREACHABLE; + return exprt(); + } // End switch } /// Adds an instruction to `init_code` null-initialising `expr`. @@ -315,8 +323,7 @@ code_assignt java_object_factoryt::get_null_assignment( /// \par parameters: `expr`: pointer-typed lvalue expression to initialise /// `target_type`: structure type to initialise, which may not match *expr (for /// example, expr might be void*) -/// `create_dynamic_objects`: if true, use malloc to allocate objects; otherwise -/// generate fresh static symbols. +/// `alloc_type`: Allocation type (global, local or dynamic) /// `update_in_place`: NO_UPDATE_IN_PLACE: initialise `expr` from scratch /// MUST_UPDATE_IN_PLACE: reinitialise an existing object MAY_UPDATE_IN_PLACE: /// invalid input @@ -324,7 +331,7 @@ void java_object_factoryt::gen_pointer_target_init( code_blockt &assignments, const exprt &expr, const typet &target_type, - bool create_dynamic_objects, + allocation_typet alloc_type, update_in_placet update_in_place) { assert(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); @@ -348,7 +355,7 @@ void java_object_factoryt::gen_pointer_target_init( assignments, expr, target_type, - create_dynamic_objects); + alloc_type); } else { @@ -368,7 +375,7 @@ void java_object_factoryt::gen_pointer_target_init( false, "", false, - create_dynamic_objects, + alloc_type, false, typet(), update_in_place); @@ -384,8 +391,7 @@ void java_object_factoryt::gen_pointer_target_init( /// \param expr: lvalue expression to initialise /// \param class_identifier - the name of the class so we can identify /// special cases where a null pointer is not applicable. -/// \param create_dynamic_objects: if true, use malloc to allocate objects; -/// otherwise generate fresh static symbols. +/// \param alloc_type: Allocation type (global, local or dynamic) /// \param pointer_type - The type of the pointer we are initalising /// `update_in_place`: NO_UPDATE_IN_PLACE: initialise `expr` from scratch /// MUST_UPDATE_IN_PLACE: reinitialise an existing object MAY_UPDATE_IN_PLACE: @@ -394,7 +400,7 @@ void java_object_factoryt::gen_nondet_pointer_init( code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, - bool create_dynamic_objects, + allocation_typet alloc_type, const pointer_typet &pointer_type, const update_in_placet &update_in_place) { @@ -408,7 +414,7 @@ void java_object_factoryt::gen_nondet_pointer_init( { const symbol_exprt real_pointer_symbol=gen_nondet_subtype_pointer_init( assignments, - create_dynamic_objects, + alloc_type, replacement_pointer_type); // Having created a pointer to object of type replacement_pointer_type @@ -447,7 +453,7 @@ void java_object_factoryt::gen_nondet_pointer_init( update_in_place_assignments, expr, subtype, - create_dynamic_objects, + alloc_type, update_in_placet::MUST_UPDATE_IN_PLACE); } @@ -464,9 +470,11 @@ void java_object_factoryt::gen_nondet_pointer_init( non_null_inst, expr, subtype, - create_dynamic_objects, + alloc_type, update_in_placet::NO_UPDATE_IN_PLACE); + auto set_null_inst=get_null_assignment(expr, pointer_type); + // Determine whether the pointer can be null. // In particular the array field of a String should not be null. bool not_null= @@ -477,7 +485,18 @@ void java_object_factoryt::gen_nondet_pointer_init( class_identifier=="java.lang.CharSequence") && subtype.id()==ID_array); - if(not_null) + // Alternatively, if this is a void* we *must* initialise with null: + // (This can currently happen for some cases of #exception_value) + bool must_be_null= + subtype==empty_typet(); + + if(must_be_null) + { + // Add the following code to assignments: + // = nullptr; + new_object_assignments.add(set_null_inst); + } + else if(not_null) { // Add the following code to assignments: // = ; @@ -494,8 +513,6 @@ void java_object_factoryt::gen_nondet_pointer_init( // > // } - auto set_null_inst=get_null_assignment(expr, pointer_type); - code_ifthenelset null_check; null_check.cond()=side_effect_expr_nondett(bool_typet()); null_check.then_case()=set_null_inst; @@ -531,15 +548,14 @@ void java_object_factoryt::gen_nondet_pointer_init( /// A * p = &tmp_object /// expr = (I *)p /// \param assignments: the code to append to -/// \param create_dynamic_objects: if true, use malloc to allocate objects; -/// otherwise generate fresh static symbols. +/// \param alloc_type: Allocation type (global, local or dynamic) /// \param replacement_pointer: The type of the pointer we actually want to /// to create. /// \return The symbol expression that corresponds to the pointer to object /// created of the required type. symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( code_blockt &assignments, - bool create_dynamic_objects, + allocation_typet alloc_type, const pointer_typet &replacement_pointer) { symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer); @@ -551,7 +567,7 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( false, "", false, - create_dynamic_objects, + alloc_type, false, typet(), update_in_placet::NO_UPDATE_IN_PLACE); @@ -571,8 +587,7 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( /// \param class_identifier: clsid to initialise @java.lang.Object. /// @class_identifier /// \param skip_classid: if true, skip initialising @class_identifier -/// \param create_dynamic_objects: if true, use malloc to allocate objects; -/// otherwise generate fresh static symbols. +/// \param alloc_type: Allocation type (global, local or dynamic) /// \param struct_type - The type of the struct we are initalising /// \param update_in_place: NO_UPDATE_IN_PLACE: initialise `expr` from scratch /// MUST_UPDATE_IN_PLACE: reinitialise an existing object MAY_UPDATE_IN_PLACE: @@ -583,7 +598,7 @@ void java_object_factoryt::gen_nondet_struct_init( bool is_sub, irep_idt class_identifier, bool skip_classid, - bool create_dynamic_objects, + allocation_typet alloc_type, const struct_typet &struct_type, const update_in_placet &update_in_place) { @@ -643,7 +658,7 @@ void java_object_factoryt::gen_nondet_struct_init( _is_sub, class_identifier, false, - create_dynamic_objects, + alloc_type, false, typet(), substruct_in_place); @@ -660,8 +675,7 @@ void java_object_factoryt::gen_nondet_struct_init( /// might be void*) /// `class_identifier`: clsid to initialise @java.lang.Object. @class_identifier /// `skip_classid`: if true, skip initialising @class_identifier -/// `create_dynamic_objects`: if true, use malloc to allocate objects; otherwise -/// generate fresh static symbols. +/// `alloc_type`: Allocation type (global, local or dynamic) /// `override`: If true, initialise with `override_type` instead of /// `expr.type()`. Used at the moment for reference arrays, which are /// implemented as void* arrays but should be init'd as their true type with @@ -676,7 +690,7 @@ void java_object_factoryt::gen_nondet_init( bool is_sub, irep_idt class_identifier, bool skip_classid, - bool create_dynamic_objects, + allocation_typet alloc_type, bool override, const typet &override_type, update_in_placet update_in_place) @@ -692,7 +706,7 @@ void java_object_factoryt::gen_nondet_init( assignments, expr, class_identifier, - create_dynamic_objects, + alloc_type, pointer_type, update_in_place); } @@ -705,7 +719,7 @@ void java_object_factoryt::gen_nondet_init( is_sub, class_identifier, skip_classid, - create_dynamic_objects, + alloc_type, struct_type, update_in_place); } @@ -751,7 +765,7 @@ void java_object_factoryt::allocate_nondet_length_array( false, irep_idt(), false, - false, + allocation_typet::LOCAL, // Doesn't matter, as type is primitive false, typet(), update_in_placet::NO_UPDATE_IN_PLACE); @@ -883,7 +897,8 @@ void java_object_factoryt::gen_nondet_array_init( false, irep_idt(), false, - true, + // These are variable in number, so use dynamic allocator: + allocation_typet::DYNAMIC, true, element_type, child_update_in_place); @@ -896,16 +911,42 @@ void java_object_factoryt::gen_nondet_array_init( assignments.move_to_operands(init_done_label); } -/// Similar to `gen_nondet_init` above, but always creates a fresh static global -/// object or primitive nondet expression. -/// \par parameters: `type`: type of new object to create -/// `allow_null`: if true, may return null; otherwise always allocates an object -/// `max_nondet_array_length`: upper bound on size of initialised arrays. -/// `loc`: source location for all generated code -/// `message_handler`: logging -/// \return `symbol_table` gains any new symbols created, as per gen_nondet_init -/// above. `init_code` gains any instructions requried to initialise either +/// Add code_declt instructions to `init_code` for every non-static symbol +/// in `symbols_created` +/// \param symbols_created: list of symbols +/// \param loc: source location for new code_declt instances +/// \param [out] init_code: gets code_declt for each symbol +static void declare_created_symbols( + const std::vector &symbols_created, + const source_locationt &loc, + code_blockt &init_code) +{ + // Add the following code to init_code for each symbol that's been created: + // ; + for(const symbolt * const symbol_ptr : symbols_created) + { + if(!symbol_ptr->is_static_lifetime) + { + code_declt decl(symbol_ptr->symbol_expr()); + decl.add_source_location()=loc; + init_code.add(decl); + } + } +} + +/// Similar to `gen_nondet_init`, but returns an object expression +/// rather than assigning to one. +/// \param type: type of new object to create +/// \param base_name: base name of top-level constructed object +/// \param [out] init_code: gains any instructions requried to initialise either /// the returned value or its child objects +/// \param allow_null: if true, may return null; otherwise always +/// allocates an object +/// \param max_nondet_array_length: upper bound on size of initialised arrays +/// \param alloc_type: allocation method (global, local or dynamic objects) +/// \param loc: source location for all generated code +/// \return `symbol_table` gains any new symbols created, as per gen_nondet_init +/// above. `init_code` exprt object_factory( const typet &type, const irep_idt base_name, @@ -913,6 +954,7 @@ exprt object_factory( bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, + allocation_typet alloc_type, const source_locationt &loc) { irep_idt identifier=id2string(goto_functionst::entry_point())+ @@ -947,19 +989,12 @@ exprt object_factory( false, "", false, - false, + alloc_type, false, typet(), update_in_placet::NO_UPDATE_IN_PLACE); - // Add the following code to init_code for each symbol that's been created: - // ; - for(const symbolt * const symbol_ptr : symbols_created) - { - code_declt decl(symbol_ptr->symbol_expr()); - decl.add_source_location()=loc; - init_code.add(decl); - } + declare_created_symbols(symbols_created, loc, init_code); init_code.append(assignments); return object; @@ -990,7 +1025,7 @@ void gen_nondet_init( symbol_tablet &symbol_table, const source_locationt &loc, bool skip_classid, - bool create_dyn_objs, + allocation_typet alloc_type, bool assume_non_null, size_t max_nondet_array_length, update_in_placet update_in_place) @@ -1010,19 +1045,12 @@ void gen_nondet_init( false, "", skip_classid, - create_dyn_objs, + alloc_type, false, typet(), update_in_place); - // Add the following code to init_code for each symbol that's been created: - // ; - for(const symbolt * const symbol_ptr : symbols_created) - { - code_declt decl(symbol_ptr->symbol_expr()); - decl.add_source_location()=loc; - init_code.add(decl); - } + declare_created_symbols(symbols_created, loc, init_code); init_code.append(assignments); } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 05f58de4e82..a56f0f14e31 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -14,6 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +/// Selects the kind of allocation used by java_object_factory et al. +enum class allocation_typet { + /// Allocate global objects + GLOBAL, + /// Allocate local stacked objects + LOCAL, + /// Allocate dynamic objects (using MALLOC) + DYNAMIC +}; + exprt object_factory( const typet &type, const irep_idt base_name, @@ -21,6 +31,7 @@ exprt object_factory( bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, + allocation_typet alloc_type, const source_locationt &); enum class update_in_placet @@ -36,7 +47,7 @@ void gen_nondet_init( symbol_tablet &symbol_table, const source_locationt &loc, bool skip_classid, - bool create_dyn_objs, + allocation_typet alloc_type, bool assume_non_null, size_t max_nondet_array_length, update_in_placet update_in_place);