From 65835c249097f2be8905a66df5e117902f418406 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 21 Jul 2017 17:25:02 +0100 Subject: [PATCH 1/2] Object factory: support global allocation This already supported choosing between allocation on the stack and the heap; this adds global object creation as a new possibility. java_static_lifetime_init is switched to use global allocation, as this reflects the true lifetime of static fields. --- src/goto-programs/convert_nondet.cpp | 2 +- .../java_bytecode_instrument.cpp | 1 + src/java_bytecode/java_entry_point.cpp | 2 + src/java_bytecode/java_object_factory.cpp | 168 ++++++++++-------- src/java_bytecode/java_object_factory.h | 13 +- 5 files changed, 107 insertions(+), 79 deletions(-) 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_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..088c046fc8b 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,7 +470,7 @@ 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); // Determine whether the pointer can be null. @@ -531,15 +537,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 +556,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 +576,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 +587,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 +647,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 +664,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 +679,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 +695,7 @@ void java_object_factoryt::gen_nondet_init( assignments, expr, class_identifier, - create_dynamic_objects, + alloc_type, pointer_type, update_in_place); } @@ -705,7 +708,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 +754,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 +886,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 +900,19 @@ 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 +/// 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 +920,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,7 +955,7 @@ exprt object_factory( false, "", false, - false, + alloc_type, false, typet(), update_in_placet::NO_UPDATE_IN_PLACE); @@ -956,9 +964,12 @@ exprt object_factory( // ; for(const symbolt * const symbol_ptr : symbols_created) { - code_declt decl(symbol_ptr->symbol_expr()); - decl.add_source_location()=loc; - init_code.add(decl); + if(!symbol_ptr->is_static_lifetime) + { + code_declt decl(symbol_ptr->symbol_expr()); + decl.add_source_location()=loc; + init_code.add(decl); + } } init_code.append(assignments); @@ -990,7 +1001,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,7 +1021,7 @@ void gen_nondet_init( false, "", skip_classid, - create_dyn_objs, + alloc_type, false, typet(), update_in_place); @@ -1019,9 +1030,12 @@ void gen_nondet_init( // ; for(const symbolt * const symbol_ptr : symbols_created) { - code_declt decl(symbol_ptr->symbol_expr()); - decl.add_source_location()=loc; - init_code.add(decl); + if(!symbol_ptr->is_static_lifetime) + { + code_declt decl(symbol_ptr->symbol_expr()); + decl.add_source_location()=loc; + init_code.add(decl); + } } 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); From f0054270d9a4502882dc032191b1571a8629ad6e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 19 Jul 2017 15:08:34 +0100 Subject: [PATCH 2/2] Fix global variable initialisation External globals (static fields in Java) should have been annotated with the static_lifetime attribute and consequently initialised with either null, or an actual instance of the right type. Instead they were given nondet pointers which could lead to odd results, such as apparently being neither null nor pointing to something of the expected type. This restores proper initialisation, and excludes global void* fields (currently only the #exception_value special returns match this definition) --- .../cbmc-java/external_getstatic1/test.class | Bin 0 -> 569 bytes .../cbmc-java/external_getstatic1/test.desc | 8 +++ .../cbmc-java/external_getstatic1/test.java | 16 +++++ .../java_bytecode_convert_method.cpp | 8 +++ src/java_bytecode/java_object_factory.cpp | 64 +++++++++++------- 5 files changed, 71 insertions(+), 25 deletions(-) create mode 100644 regression/cbmc-java/external_getstatic1/test.class create mode 100644 regression/cbmc-java/external_getstatic1/test.desc create mode 100644 regression/cbmc-java/external_getstatic1/test.java diff --git a/regression/cbmc-java/external_getstatic1/test.class b/regression/cbmc-java/external_getstatic1/test.class new file mode 100644 index 0000000000000000000000000000000000000000..ec38ad6938551538faf41baaf86fb0c522a17d11 GIT binary patch literal 569 zcmYLGO)mpc6g_Wd+Si#5+M?=PvA}{&cSJPBMzJ7*jl8xmGE8S=W-5M5|A2K#G$A2Y z62D2reG_dr@6Mci?m6ea_x=0&4xof(3nua=3{05dC~!=2Oj$@E&oOOb2D2P<45P~; z3}p~Gz8CH~p{TjC!N4vVl3R}FMB5Dd%IX<|QSlp+VWjGK@~G9U$>3CxsnHaU$1rpf ziTdrKxQk)3V@Pe)-G2@1#BT+4x$me6Gm>Gnek1OM4I4u?=CNSILYj=r3add_needed_class( diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 088c046fc8b..5559dfaf714 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -473,6 +473,8 @@ void java_object_factoryt::gen_nondet_pointer_init( 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= @@ -483,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: // = ; @@ -500,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; @@ -900,6 +911,29 @@ void java_object_factoryt::gen_nondet_array_init( assignments.move_to_operands(init_done_label); } +/// 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 @@ -960,17 +994,7 @@ exprt object_factory( 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) - { - if(!symbol_ptr->is_static_lifetime) - { - 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; @@ -1026,17 +1050,7 @@ void gen_nondet_init( 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) - { - if(!symbol_ptr->is_static_lifetime) - { - 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); }