From 9d4f8fe89e1e9b8db49c56fc31511da8f6ef3b30 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 19 Nov 2018 11:41:45 +0000 Subject: [PATCH 1/4] Factor out object allocation code from object factories to util/allocate_objects.h/cpp --- jbmc/src/java_bytecode/java_object_factory.h | 2 +- src/util/Makefile | 3 +- src/util/allocate_objects.cpp | 279 +++++++++++++++++++ src/util/allocate_objects.h | 99 +++++++ 4 files changed, 381 insertions(+), 2 deletions(-) create mode 100644 src/util/allocate_objects.cpp create mode 100644 src/util/allocate_objects.h diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index 66f8506ae8f..3b07a20e3ed 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -78,7 +78,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -/// Selects the kind of allocation used by java_object_factory et al. +/// Selects the kind of allocation used by the object factories enum class allocation_typet { /// Allocate global objects diff --git a/src/util/Makefile b/src/util/Makefile index 52ce754b1e5..58a32bf25b7 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,4 +1,5 @@ -SRC = arith_tools.cpp \ +SRC = allocate_objects.cpp \ + arith_tools.cpp \ array_name.cpp \ base_type.cpp \ bv_arithmetic.cpp \ diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp new file mode 100644 index 00000000000..434d4a1bb19 --- /dev/null +++ b/src/util/allocate_objects.cpp @@ -0,0 +1,279 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "allocate_objects.h" + +#include "arith_tools.h" +#include "c_types.h" +#include "fresh_symbol.h" +#include "pointer_offset_size.h" +#include "string_constant.h" + +/// Allocates a new object, either by creating a local variable with automatic +/// lifetime, a global variable with static lifetime, or by dynamically +/// allocating memory via ALLOCATE(). Code is added to `assignments` which +/// assigns a pointer to the allocated memory to `target_expr`. The +/// `allocate_type` may differ from `target_expr.type()`, e.g. for target_expr +/// having type `int*` and `allocate_type` being an `int[10]`. +/// +/// \param assignments: The code block to add code to. +/// \param target_expr: A pointer to the allocated memory will be assigned to +/// this lvalue expression +/// \param allocate_type: Type of the object allocated +/// \param lifetime: Lifetime of the allocated object (AUTOMATIC_LOCAL, +/// STATIC_GLOBAL, or DYNAMIC) +/// \param basename_prefix: prefix of the basename of the new variable +/// \return An lvalue expression denoting the newly allocated object +exprt allocate_objectst::allocate_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const lifetimet lifetime, + const irep_idt &basename_prefix) +{ + switch(lifetime) + { + case lifetimet::AUTOMATIC_LOCAL: + return allocate_automatic_local_object( + assignments, target_expr, allocate_type, basename_prefix); + break; + + case lifetimet::STATIC_GLOBAL: + return allocate_static_global_object( + assignments, target_expr, allocate_type, basename_prefix); + break; + + case lifetimet::DYNAMIC: + return allocate_dynamic_object(assignments, target_expr, allocate_type); + break; + } + + UNREACHABLE; +} + +/// Creates a local variable with automatic lifetime. Code is added to +/// `assignments` which assigns a pointer to the variable to `target_expr`. The +/// `allocate_type` may differ from `target_expr.type()`, e.g. for `target_expr` +/// having type `int*` and `allocate_type` being an `int[10]`.. +/// +/// \param assignments: The code block to add code to. +/// \param target_expr: A pointer to the variable will be assigned to this +/// lvalue expression +/// \param allocate_type: Type of the new variable +/// \param basename_prefix: prefix of the basename of the new variable +/// \return An expression denoting the variable +exprt allocate_objectst::allocate_automatic_local_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const irep_idt &basename_prefix) +{ + return allocate_non_dynamic_object( + assignments, target_expr, allocate_type, false, basename_prefix); +} + +/// Creates a global variable with static lifetime. Code is added to +/// `assignments` which assigns a pointer to the variable to `target_expr`. The +/// `allocate_type` may differ from `target_expr.type()`, e.g. for `target_expr` +/// having type `int*` and `allocate_type` being an `int[10]`. +/// +/// \param assignments: The code block to add code to. +/// \param target_expr: A pointer to the variable will be assigned to this +/// lvalue expression +/// \param allocate_type: Type of the new variable +/// \param basename_prefix: prefix of the basename of the new variable +/// \return An expression denoting the variable +exprt allocate_objectst::allocate_static_global_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const irep_idt &basename_prefix) +{ + return allocate_non_dynamic_object( + assignments, target_expr, allocate_type, true, basename_prefix); +} + +/// Creates a local variable with automatic lifetime and returns it as a symbol +/// expression. +/// +/// \param allocate_type: Type of the new variable +/// \param basename_prefix: prefix of the basename of the new variable +/// \return A symbol expression denoting the variable +symbol_exprt allocate_objectst::allocate_automatic_local_object( + const typet &allocate_type, + const irep_idt &basename_prefix) +{ + symbolt &aux_symbol = get_fresh_aux_symbol( + allocate_type, + id2string(name_prefix), + id2string(basename_prefix), + source_location, + symbol_mode, + symbol_table); + + symbols_created.push_back(&aux_symbol); + + return aux_symbol.symbol_expr(); +} + +/// Generates code for allocating a dynamic object. A new variable with basename +/// prefix `alloc_site` is introduced to which the allocated memory is assigned. +/// Then, the variable is assigned to `target_expr`. For example, with +/// `target_expr` being `*p` the following code is generated: +/// +/// `alloc_site$1 = ALLOCATE(object_size, FALSE);` +/// `*p = alloc_site$1;` +/// +/// The function returns a dereference expressiont that dereferences the +/// allocation site variable (e.g., `*alloc_site$1`) and which can be used to +/// initialize the allocated memory. +/// +/// \param output_code: Code block to which the necessary code is added +/// \param target_expr: A pointer to the allocated memory will be assigned to +/// this (lvalue) expression +/// \param allocate_type: Type of the object allocated +/// \return A dereference_exprt that dereferences the pointer to the allocated +/// memory, or an empty expression when `allocate_type` is void +exprt allocate_objectst::allocate_dynamic_object( + code_blockt &output_code, + const exprt &target_expr, + const typet &allocate_type) +{ + if(allocate_type.id() == ID_empty) + { + // make null + null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type())); + code_assignt code(target_expr, null_pointer_expr); + code.add_source_location() = source_location; + output_code.add(code); + + return exprt(); + } + + // build size expression + exprt object_size = size_of_expr(allocate_type, ns); + INVARIANT(!object_size.is_nil(), "Size of objects should be known"); + + // malloc expression + side_effect_exprt malloc_expr( + ID_allocate, pointer_type(allocate_type), source_location); + malloc_expr.copy_to_operands(object_size); + malloc_expr.copy_to_operands(false_exprt()); + + // create a symbol for the malloc expression so we can initialize + // without having to do it potentially through a double-deref, which + // breaks the to-SSA phase. + symbolt &malloc_sym = get_fresh_aux_symbol( + pointer_type(allocate_type), + id2string(name_prefix), + "malloc_site", + source_location, + symbol_mode, + symbol_table); + + symbols_created.push_back(&malloc_sym); + + code_assignt assign(malloc_sym.symbol_expr(), malloc_expr); + assign.add_source_location() = source_location; + output_code.add(assign); + + exprt malloc_symbol_expr = + ns.follow(malloc_sym.symbol_expr().type()) != ns.follow(target_expr.type()) + ? (exprt)typecast_exprt(malloc_sym.symbol_expr(), target_expr.type()) + : malloc_sym.symbol_expr(); + + code_assignt code(target_expr, malloc_symbol_expr); + code.add_source_location() = source_location; + output_code.add(code); + + return dereference_exprt(malloc_sym.symbol_expr()); +} + +exprt allocate_objectst::allocate_non_dynamic_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const bool static_lifetime, + const irep_idt &basename_prefix) +{ + symbolt &aux_symbol = get_fresh_aux_symbol( + allocate_type, + id2string(name_prefix), + id2string(basename_prefix), + source_location, + symbol_mode, + symbol_table); + + aux_symbol.is_static_lifetime = static_lifetime; + symbols_created.push_back(&aux_symbol); + + exprt aoe = + ns.follow(aux_symbol.symbol_expr().type()) != + ns.follow(target_expr.type().subtype()) + ? (exprt)typecast_exprt( + address_of_exprt(aux_symbol.symbol_expr()), target_expr.type()) + : address_of_exprt(aux_symbol.symbol_expr()); + + code_assignt code(target_expr, aoe); + code.add_source_location() = source_location; + assignments.add(code); + + if(aoe.id() == ID_typecast) + { + return dereference_exprt(aoe); + } + else + { + return aux_symbol.symbol_expr(); + } +} + +/// Add a pointer to a symbol to the list of pointers to symbols created so far +/// +/// \param symbol_ptr pointer to a symbol in the symbol table +void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr) +{ + symbols_created.push_back(symbol_ptr); +} + +/// Adds declarations for all non-static symbols created +/// +/// \param init_code code block to which to add the declarations +void allocate_objectst::declare_created_symbols(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() = source_location; + init_code.add(decl); + } + } +} + +/// Adds code to mark the created symbols as input +/// +/// \param init_code code block to which to add the generated code +void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code) +{ + // Add the following code to init_code for each symbol that's been created: + // INPUT("", ); + for(symbolt const *symbol_ptr : symbols_created) + { + codet input_code(ID_input); + input_code.operands().resize(2); + input_code.op0() = address_of_exprt(index_exprt( + string_constantt(symbol_ptr->base_name), from_integer(0, index_type()))); + input_code.op1() = symbol_ptr->symbol_expr(); + input_code.add_source_location() = source_location; + init_code.add(std::move(input_code)); + } +} diff --git a/src/util/allocate_objects.h b/src/util/allocate_objects.h new file mode 100644 index 00000000000..a0cd9a9d83b --- /dev/null +++ b/src/util/allocate_objects.h @@ -0,0 +1,99 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H +#define CPROVER_UTIL_ALLOCATE_OBJECTS_H + +#include "base_type.h" +#include "expr.h" +#include "namespace.h" +#include "source_location.h" +#include "std_code.h" +#include "symbol_table.h" +#include "type.h" + +/// Selects the kind of objects allocated +enum class lifetimet +{ + /// Allocate local objects with automatic lifetime + AUTOMATIC_LOCAL, + /// Allocate global objects with static lifetime + STATIC_GLOBAL, + /// Allocate dynamic objects (using ALLOCATE) + DYNAMIC +}; + +class allocate_objectst +{ +public: + allocate_objectst( + const irep_idt &symbol_mode, + const source_locationt &source_location, + const irep_idt &name_prefix, + symbol_table_baset &symbol_table) + : symbol_mode(symbol_mode), + source_location(source_location), + name_prefix(name_prefix), + symbol_table(symbol_table), + ns(symbol_table) + { + } + + exprt allocate_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const lifetimet lifetime, + const irep_idt &basename_prefix = "tmp"); + + exprt allocate_automatic_local_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const irep_idt &basename_prefix = "tmp"); + + exprt allocate_static_global_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const irep_idt &basename_prefix = "tmp"); + + exprt allocate_dynamic_object( + code_blockt &output_code, + const exprt &target_expr, + const typet &allocate_type); + + symbol_exprt allocate_automatic_local_object( + const typet &allocate_type, + const irep_idt &basename_prefix = "tmp"); + + void add_created_symbol(const symbolt *symbol_ptr); + + void declare_created_symbols(code_blockt &init_code); + + void mark_created_symbols_as_input(code_blockt &init_code); + +private: + const irep_idt &symbol_mode; + const source_locationt &source_location; + const irep_idt &name_prefix; + + symbol_table_baset &symbol_table; + const namespacet ns; + + std::vector symbols_created; + + exprt allocate_non_dynamic_object( + code_blockt &assignments, + const exprt &target_expr, + const typet &allocate_type, + const bool static_lifetime, + const irep_idt &basename_prefix); +}; + +#endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H From 1adfa5c3d17db9630b293d1232f6ad25779e4bb9 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 19 Nov 2018 14:59:01 +0000 Subject: [PATCH 2/4] Use allocate_objectst in the c nondet object factory --- src/ansi-c/c_nondet_symbol_factory.cpp | 118 ++++++------------------- 1 file changed, 27 insertions(+), 91 deletions(-) diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index bb931f9ed62..eadc2a25927 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -13,6 +13,7 @@ Author: Diffblue Ltd. #include +#include #include #include #include @@ -26,39 +27,48 @@ Author: Diffblue Ltd. class symbol_factoryt { - std::vector &symbols_created; symbol_tablet &symbol_table; const source_locationt &loc; namespacet ns; const c_object_factory_parameterst &object_factory_params; + allocate_objectst allocate_objects; + typedef std::set recursion_sett; public: symbol_factoryt( - std::vector &_symbols_created, symbol_tablet &_symbol_table, const source_locationt &loc, const c_object_factory_parameterst &object_factory_params) - : symbols_created(_symbols_created), - symbol_table(_symbol_table), + : symbol_table(_symbol_table), loc(loc), ns(_symbol_table), - object_factory_params(object_factory_params) + object_factory_params(object_factory_params), + allocate_objects(ID_C, loc, loc.get_function(), symbol_table) {} - exprt allocate_object( - code_blockt &assignments, - const exprt &target_expr, - const typet &allocate_type, - const bool static_lifetime); - void gen_nondet_init( code_blockt &assignments, const exprt &expr, const std::size_t depth = 0, recursion_sett recursion_set = recursion_sett()); + void add_created_symbol(const symbolt *symbol_ptr) + { + allocate_objects.add_created_symbol(symbol_ptr); + } + + void declare_created_symbols(code_blockt &init_code) + { + allocate_objects.declare_created_symbols(init_code); + } + + void mark_created_symbols_as_input(code_blockt &init_code) + { + allocate_objects.mark_created_symbols_as_input(init_code); + } + private: /// Generate initialisation code for each array element /// \param assignments: The code block to add code to @@ -73,49 +83,6 @@ class symbol_factoryt const recursion_sett &recursion_set); }; -/// Create a symbol for a pointer to point to -/// \param assignments: The code block to add code to -/// \param target_expr: The expression which we are allocating a symbol for -/// \param allocate_type: The type to use for the symbol. If this doesn't match -/// target_expr then a cast will be used for the assignment -/// \param static_lifetime: Whether the symbol created should have static -/// lifetime -/// \return Returns the address of the allocated symbol -exprt symbol_factoryt::allocate_object( - code_blockt &assignments, - const exprt &target_expr, - const typet &allocate_type, - const bool static_lifetime) -{ - symbolt &aux_symbol = get_fresh_aux_symbol( - allocate_type, - id2string(loc.get_function()), - "tmp", - loc, - ID_C, - symbol_table); - aux_symbol.is_static_lifetime = static_lifetime; - symbols_created.push_back(&aux_symbol); - - 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; - - exprt aoe=address_of_exprt(aux_symbol.symbol_expr()); - if(cast_needed) - { - aoe=typecast_exprt(aoe, target_expr.type()); - } - - // Add the following code to assignments: - // = &tmp$ - code_assignt assign(target_expr, aoe); - assign.add_source_location()=loc; - assignments.add(std::move(assign)); - - return aoe; -} - /// Creates a nondet for expr, including calling itself recursively to make /// appropriate symbols to point to if expr is a pointer. /// \param assignments: The code block to add code to @@ -155,17 +122,9 @@ void symbol_factoryt::gen_nondet_init( code_blockt non_null_inst; - exprt allocated=allocate_object(non_null_inst, expr, subtype, false); + exprt init_expr = allocate_objects.allocate_automatic_local_object( + non_null_inst, expr, subtype); - exprt init_expr; - if(allocated.id()==ID_address_of) - { - init_expr=allocated.op0(); - } - else - { - init_expr=dereference_exprt(allocated, allocated.type().subtype()); - } gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set); if(depth < object_factory_params.min_null_tree_depth) @@ -288,39 +247,16 @@ symbol_exprt c_nondet_symbol_factory( bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr); CHECK_RETURN(!moving_symbol_failed); - std::vector symbols_created; - symbols_created.push_back(main_symbol_ptr); - - symbol_factoryt state( - symbols_created, symbol_table, loc, object_factory_parameters); + symbol_factoryt state(symbol_table, loc, object_factory_parameters); code_blockt assignments; state.gen_nondet_init(assignments, main_symbol_expr); - // 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(std::move(decl)); - } + state.add_created_symbol(main_symbol_ptr); + state.declare_created_symbols(init_code); init_code.append(assignments); - // Add the following code to init_code for each symbol that's been created: - // INPUT("", ); - for(symbolt const *symbol_ptr : symbols_created) - { - codet input_code(ID_input); - input_code.operands().resize(2); - input_code.op0()= - address_of_exprt(index_exprt( - string_constantt(symbol_ptr->base_name), - from_integer(0, index_type()))); - input_code.op1()=symbol_ptr->symbol_expr(); - input_code.add_source_location()=loc; - init_code.add(std::move(input_code)); - } + state.mark_created_symbols_as_input(init_code); return main_symbol_expr; } From 255c6bd86a30c9b1633917bd8cc54e32d5b6f211 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sat, 15 Dec 2018 18:20:59 +0000 Subject: [PATCH 3/4] Use allocate_objectst in jbmc --- .../src/java_bytecode/convert_java_nondet.cpp | 2 +- jbmc/src/java_bytecode/java_entry_point.cpp | 6 +- .../src/java_bytecode/java_object_factory.cpp | 423 +++++------------- jbmc/src/java_bytecode/java_object_factory.h | 37 +- .../java_static_initializers.cpp | 4 +- .../java_string_library_preprocess.cpp | 26 +- .../java_bytecode/simple_method_stubbing.cpp | 4 +- .../gen_nondet_string_init.cpp | 2 +- 8 files changed, 139 insertions(+), 365 deletions(-) diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp index d945ed6d41d..b535ee8f4df 100644 --- a/jbmc/src/java_bytecode/convert_java_nondet.cpp +++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp @@ -55,7 +55,7 @@ static goto_programt get_gen_nondet_init_instructions( symbol_table, source_loc, skip_classid, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, object_factory_parameters, update_in_placet::NO_UPDATE_IN_PLACE); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 6a099c32764..068df7baed3 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -243,7 +243,7 @@ static void java_static_lifetime_init( symbol_table, source_location, false, - allocation_typet::GLOBAL, + lifetimet::STATIC_GLOBAL, parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); @@ -348,7 +348,7 @@ exprt::operandst java_build_arguments( init_code, symbol_table, parameters, - allocation_typet::LOCAL, + lifetimet::AUTOMATIC_LOCAL, function.location, pointer_type_selector); } @@ -394,7 +394,7 @@ exprt::operandst java_build_arguments( init_code_for_type, symbol_table, parameters, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, function.location, pointer_type_selector); init_code_for_type.add( diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index cbaf8d37d06..7f7015ca431 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -23,11 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com class java_object_factoryt { - /// Every new variable initialized by the code emitted by the methods of this - /// class gets a symbol in the symbol table, and such symbols are also added - /// to this vector. - std::vector &symbols_created; - /// The source location for new statements emitted during the operation of the /// methods in this class. const source_locationt &loc; @@ -61,6 +56,8 @@ class java_object_factoryt /// implementations. const select_pointer_typet &pointer_type_selector; + allocate_objectst allocate_objects; + code_assignt get_null_assignment( const exprt &expr, const pointer_typet &ptr_type); @@ -69,7 +66,7 @@ class java_object_factoryt code_blockt &assignments, const exprt &expr, const typet &target_type, - allocation_typet alloc_type, + lifetimet lifetime, size_t depth, update_in_placet update_in_place, const source_locationt &location); @@ -83,25 +80,22 @@ class java_object_factoryt public: java_object_factoryt( - std::vector &_symbols_created, const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector) - : symbols_created(_symbols_created), - loc(loc), + : loc(loc), object_factory_parameters(_object_factory_parameters), symbol_table(_symbol_table), ns(_symbol_table), - pointer_type_selector(pointer_type_selector) + pointer_type_selector(pointer_type_selector), + allocate_objects( + ID_java, + loc, + object_factory_parameters.function_id, + symbol_table) {} - exprt allocate_object( - code_blockt &assignments, - const exprt &, - const typet &, - allocation_typet alloc_type); - void gen_nondet_array_init( code_blockt &assignments, const exprt &expr, @@ -121,18 +115,22 @@ class java_object_factoryt bool is_sub, irep_idt class_identifier, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, bool override_, const typet &override_type, size_t depth, update_in_placet, const source_locationt &location); + void add_created_symbol(const symbolt *symbol); + + void declare_created_symbols(code_blockt &init_code); + private: void gen_nondet_pointer_init( code_blockt &assignments, const exprt &expr, - allocation_typet alloc_type, + lifetimet lifetime, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, @@ -144,7 +142,7 @@ class java_object_factoryt bool is_sub, irep_idt class_identifier, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place, @@ -152,7 +150,7 @@ class java_object_factoryt symbol_exprt gen_nondet_subtype_pointer_init( code_blockt &assignments, - allocation_typet alloc_type, + lifetimet lifetime, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location); @@ -170,182 +168,6 @@ class java_object_factoryt const irep_idt &method_name); }; -/// Generates code for allocating a dynamic object. This is used in -/// allocate_object() and also in the library preprocessing for allocating -/// strings. -/// \param target_expr: expression to which the necessary memory will be -/// allocated, its type should be pointer to `allocate_type` -/// \param allocate_type: type of the object allocated -/// \param symbol_table: symbol table -/// \param loc: location in the source -/// \param function_id: function ID to associate with auxiliary variables -/// \param output_code: code block to which the necessary code is added -/// \param symbols_created: created symbols to be declared by the caller -/// \param cast_needed: Boolean flags saying where we need to cast the malloc -/// site -/// \return Expression representing the malloc site allocated. -exprt allocate_dynamic_object( - const exprt &target_expr, - const typet &allocate_type, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &output_code, - std::vector &symbols_created, - bool cast_needed) -{ - // build size expression - exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table)); - - if(allocate_type.id()!=ID_empty) - { - INVARIANT(!object_size.is_nil(), "Size of Java objects should be known"); - // malloc expression - side_effect_exprt malloc_expr( - ID_allocate, pointer_type(allocate_type), loc); - malloc_expr.copy_to_operands(object_size); - malloc_expr.copy_to_operands(false_exprt()); - // create a symbol for the malloc expression so we can initialize - // without having to do it potentially through a double-deref, which - // breaks the to-SSA phase. - symbolt &malloc_sym = get_fresh_aux_symbol( - pointer_type(allocate_type), - id2string(function_id), - "malloc_site", - loc, - ID_java, - symbol_table); - symbols_created.push_back(&malloc_sym); - code_assignt assign(malloc_sym.symbol_expr(), malloc_expr); - assign.add_source_location()=loc; - output_code.add(assign); - exprt malloc_symbol_expr=malloc_sym.symbol_expr(); - if(cast_needed) - malloc_symbol_expr=typecast_exprt(malloc_symbol_expr, target_expr.type()); - code_assignt code(target_expr, malloc_symbol_expr); - code.add_source_location()=loc; - output_code.add(code); - return malloc_sym.symbol_expr(); - } - else - { - // make null - null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type())); - code_assignt code(target_expr, null_pointer_expr); - code.add_source_location()=loc; - output_code.add(code); - return exprt(); - } -} - -/// Generates code for allocating a dynamic object. This is a static version of -/// allocate_dynamic_object that can be called from outside java_object_factory -/// and which takes care of creating the associated declarations. -/// \param target_expr: expression to which the necessary memory will be -/// allocated -/// \param symbol_table: symbol table -/// \param loc: location in the source -/// \param function_id: function ID to associate with auxiliary variables -/// \param output_code: code block to which the necessary code is added -/// \return the dynamic object created -exprt allocate_dynamic_object_with_decl( - const exprt &target_expr, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &output_code) -{ - std::vector symbols_created; - code_blockt tmp_block; - const typet &allocate_type=target_expr.type().subtype(); - const exprt dynamic_object = allocate_dynamic_object( - target_expr, - allocate_type, - symbol_table, - loc, - function_id, - tmp_block, - symbols_created, - false); - - // Add the following code to output_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; - output_code.add(decl); - } - - for(const auto &code : tmp_block.statements()) - output_code.add(code); - - return dynamic_object; -} - -/// Installs a new symbol in the symbol table, pushing the corresponding symbolt -/// object to the field `symbols_created` and emits to \p assignments a new -/// assignment of the form ` := address-of(new_object)`. The -/// \p allocate_type may differ from `target_expr.type()`, e.g. for target_expr -/// having type int* and allocate_type being an int[10]. -/// -/// \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 alloc_type: Allocation type (global, local or dynamic) -/// \return An address_of_exprt of the newly allocated object. -exprt java_object_factoryt::allocate_object( - code_blockt &assignments, - const exprt &target_expr, - const typet &allocate_type, - 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; - switch(alloc_type) - { - case allocation_typet::LOCAL: - case allocation_typet::GLOBAL: - { - symbolt &aux_symbol = get_fresh_aux_symbol( - allocate_type, - id2string(object_factory_parameters.function_id), - "tmp_object_factory", - loc, - ID_java, - symbol_table); - 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.add(code); - return aoe; - } - case allocation_typet::DYNAMIC: - { - return allocate_dynamic_object( - target_expr, - allocate_type, - symbol_table, - loc, - object_factory_parameters.function_id, - assignments, - symbols_created, - cast_needed); - } - default: - UNREACHABLE; - return exprt(); - } // End switch -} - /// Returns a codet that assigns \p expr, of type \p ptr_type, a NULL value. code_assignt java_object_factoryt::get_null_assignment( const exprt &expr, @@ -363,19 +185,19 @@ code_assignt java_object_factoryt::get_null_assignment( /// /// When in NO_UPDATE_IN_PLACE mode, the code emitted looks like: /// -/// ``` -/// struct new_object obj; // depends on alloc_type +/// \code +/// struct new_object obj; // depends on lifetime /// := &obj /// // recursive initialization of obj in NO_UPDATE_IN_PLACE mode -/// ``` +/// \endcode /// /// When in MUST_UPDATE_IN_PLACE mode, all code is emitted by a recursive call /// to gen_nondet_init in MUST_UPDATE_IN_PLACE mode, and looks like: /// -/// ``` +/// \code /// (*).some_int := NONDET(int) /// (*).some_char := NONDET(char) -/// ``` +/// \endcode /// It is illegal to call the function with MAY_UPDATE_IN_PLACE. /// /// \param[out] assignments: @@ -387,8 +209,9 @@ code_assignt java_object_factoryt::get_null_assignment( /// Structure type to initialize, which may not match `*expr` (for example, /// `expr` might be have type void*). It cannot be a pointer to a primitive /// type because Java does not allow so. -/// \param alloc_type: -/// Allocation type (global, local or dynamic) +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param depth: /// Number of times that a pointer has been dereferenced from the root of the /// object tree that we are initializing. @@ -402,7 +225,7 @@ void java_object_factoryt::gen_pointer_target_init( code_blockt &assignments, const exprt &expr, const typet &target_type, - allocation_typet alloc_type, + lifetimet lifetime, size_t depth, update_in_placet update_in_place, const source_locationt &location) @@ -432,34 +255,29 @@ void java_object_factoryt::gen_pointer_target_init( // (return value of `allocate_object`), emit a statement of the form // ` := address-of()` and recursively initialize such new // object. - exprt target; + exprt init_expr; if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE) { - target = allocate_object(assignments, expr, target_type, alloc_type); - INVARIANT( - target.type().id() == ID_pointer, "Pointer-typed expression expected"); + init_expr = allocate_objects.allocate_object( + assignments, expr, target_type, lifetime, "tmp_object_factory"); } else { - target = expr; + if(expr.id() == ID_address_of) + init_expr = expr.op0(); + else + { + init_expr = dereference_exprt(expr); + } } - // we dereference the pointer and initialize the resulting object using a - // recursive call - exprt init_expr; - if(target.id() == ID_address_of) - init_expr = target.op0(); - else - { - init_expr = dereference_exprt(target, target.type().subtype()); - } gen_nondet_init( assignments, init_expr, false, // is_sub "", // class_identifier false, // skip_classid - alloc_type, + lifetime, false, // override typet(), // override type immaterial depth + 1, @@ -667,8 +485,9 @@ void initialize_nondet_string_fields( /// The code block we are building with initialization code. /// \param expr: /// Pointer-typed lvalue expression to initialize. -/// \param alloc_type: -/// Allocation type (global, local or dynamic) +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param depth: /// Number of times that a pointer has been dereferenced from the root of the /// object tree that we are initializing. @@ -684,7 +503,7 @@ void initialize_nondet_string_fields( void java_object_factoryt::gen_nondet_pointer_init( code_blockt &assignments, const exprt &expr, - allocation_typet alloc_type, + lifetimet lifetime, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, @@ -710,7 +529,7 @@ void java_object_factoryt::gen_nondet_pointer_init( replacement_pointer_type, ns.follow(replacement_pointer_type.subtype())); const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( - assignments, alloc_type, replacement_pointer_type, depth, location); + assignments, lifetime, replacement_pointer_type, depth, location); // Having created a pointer to object of type replacement_pointer_type // we now assign it back to the original pointer with a cast @@ -798,7 +617,7 @@ void java_object_factoryt::gen_nondet_pointer_init( update_in_place_assignments, expr, subtype, - alloc_type, + lifetime, depth, update_in_placet::MUST_UPDATE_IN_PLACE, location); @@ -821,7 +640,7 @@ void java_object_factoryt::gen_nondet_pointer_init( non_null_inst, expr, subtype, - alloc_type, + lifetime, depth, update_in_placet::NO_UPDATE_IN_PLACE, location); @@ -884,7 +703,7 @@ void java_object_factoryt::gen_nondet_pointer_init( /// Generate codet assignments to initalize the selected concrete type. /// Generated code looks as follows (here A = replacement_pointer.subtype()): /// -/// // allocate memory for a new object, depends on `alloc_type` +/// // allocate memory for a new object, depends on `lifetime` /// A { ... } tmp_object; /// /// // non-det init all the fields of A @@ -896,7 +715,9 @@ void java_object_factoryt::gen_nondet_pointer_init( /// /// \param assignments /// A block of code where we append the generated code. -/// \param alloc_type: Allocation type (global, local or dynamic) +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param replacement_pointer /// The type of the pointer we actually want to to create. /// \param depth: @@ -909,7 +730,7 @@ void java_object_factoryt::gen_nondet_pointer_init( /// pointer to object `tmp_object` (see above). symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( code_blockt &assignments, - allocation_typet alloc_type, + lifetimet lifetime, const pointer_typet &replacement_pointer, size_t depth, const source_locationt &location) @@ -929,7 +750,7 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( false, // is_sub "", // class_identifier false, // skip_classid - alloc_type, + lifetime, false, // override typet(), // override_type depth, @@ -984,8 +805,9 @@ alternate_casest get_string_input_values_code( /// others. /// \param skip_classid: /// If true, skip initializing `@class_identifier`. -/// \param alloc_type: -/// Allocation type (global, local or dynamic) +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param struct_type: /// The type of the struct we are initalizing. /// \param depth: @@ -1003,7 +825,7 @@ void java_object_factoryt::gen_nondet_struct_init( bool is_sub, irep_idt class_identifier, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place, @@ -1142,7 +964,7 @@ void java_object_factoryt::gen_nondet_struct_init( _is_sub, class_identifier, false, // skip_classid - alloc_type, + lifetime, false, // override typet(), // override_type depth, @@ -1179,8 +1001,9 @@ void java_object_factoryt::gen_nondet_struct_init( /// others. /// \param skip_classid: /// If true, skip initializing `@class_identifier`. -/// \param alloc_type: -/// Allocation type (global, local or dynamic) +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param override_: /// If true, initialize with `override_type` instead of `expr.type()`. Used at /// the moment for reference arrays, which are implemented as void* arrays but @@ -1203,7 +1026,7 @@ void java_object_factoryt::gen_nondet_init( bool is_sub, irep_idt class_identifier, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, bool override_, const typet &override_type, size_t depth, @@ -1230,7 +1053,7 @@ void java_object_factoryt::gen_nondet_init( gen_nondet_pointer_init( assignments, expr, - alloc_type, + lifetime, pointer_type, depth, update_in_place, @@ -1260,7 +1083,7 @@ void java_object_factoryt::gen_nondet_init( is_sub, class_identifier, skip_classid, - alloc_type, + lifetime, struct_type, depth, update_in_place, @@ -1279,6 +1102,16 @@ void java_object_factoryt::gen_nondet_init( } } +void java_object_factoryt::add_created_symbol(const symbolt *symbol_ptr) +{ + allocate_objects.add_created_symbol(symbol_ptr); +} + +void java_object_factoryt::declare_created_symbols(code_blockt &init_code) +{ + allocate_objects.declare_created_symbols(init_code); +} + /// Nondeterministically initializes an int i in the range min <= i <= max, /// where min is the integer represented by `min_value_expr` and max is the /// integer represented by `max_value_expr`. @@ -1297,16 +1130,10 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init( const source_locationt &location) { PRECONDITION(min_value_expr.type() == max_value_expr.type()); - // Allocate a new symbol for the int - const symbolt &int_symbol = get_fresh_aux_symbol( - min_value_expr.type(), - id2string(object_factory_parameters.function_id), - basename_prefix, - loc, - ID_java, - symbol_table); - symbols_created.push_back(&int_symbol); - const auto &int_symbol_expr = int_symbol.symbol_expr(); + + const symbol_exprt &int_symbol_expr = + allocate_objects.allocate_automatic_local_object( + min_value_expr.type(), basename_prefix); // Nondet-initialize it gen_nondet_init( @@ -1314,11 +1141,11 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init( int_symbol_expr, false, // is_sub irep_idt(), - false, // skip_classid - allocation_typet::LOCAL, // immaterial, type is primitive - false, // override - typet(), // override type is immaterial - 0, // depth is immaterial, always non-null + false, // skip_classid + lifetimet::AUTOMATIC_LOCAL, // immaterial, type is primitive + false, // override + typet(), // override type is immaterial + 0, // depth is immaterial, always non-null update_in_placet::NO_UPDATE_IN_PLACE, location); @@ -1420,32 +1247,20 @@ void java_object_factoryt::gen_nondet_array_init( init_array_expr= typecast_exprt(init_array_expr, pointer_type(element_type)); - // Interpose a new symbol, as the goto-symex stage can't handle array indexing - // via a cast. - symbolt &array_init_symbol = get_fresh_aux_symbol( - init_array_expr.type(), - id2string(object_factory_parameters.function_id), - "array_data_init", - loc, - ID_java, - symbol_table); - symbols_created.push_back(&array_init_symbol); - const auto &array_init_symexpr=array_init_symbol.symbol_expr(); + const symbol_exprt &array_init_symexpr = + allocate_objects.allocate_automatic_local_object( + init_array_expr.type(), "array_data_init"); + code_assignt data_assign(array_init_symexpr, init_array_expr); data_assign.add_source_location()=loc; assignments.add(data_assign); - // Emit init loop for(array_init_iter=0; array_init_iter!=array.length; - // ++array_init_iter) init(array[array_init_iter]); - symbolt &counter = get_fresh_aux_symbol( - length_expr.type(), - id2string(object_factory_parameters.function_id), - "array_init_iter", - loc, - ID_java, - symbol_table); - symbols_created.push_back(&counter); - exprt counter_expr=counter.symbol_expr(); + const symbol_exprt &counter_expr = + allocate_objects.allocate_automatic_local_object( + length_expr.type(), "array_init_iter"); + + const symbolt &counter = + symbol_table.lookup_ref(counter_expr.get_identifier()); exprt java_zero=from_integer(0, java_int_type()); assignments.add(code_assignt(counter_expr, java_zero)); @@ -1493,7 +1308,7 @@ void java_object_factoryt::gen_nondet_array_init( irep_idt(), // class_identifier false, // skip_classid // These are variable in number, so use dynamic allocator: - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, true, // override element_type, depth, @@ -1553,29 +1368,6 @@ void java_object_factoryt::gen_nondet_enum_init( assignments.add(enum_assign); } -/// 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` below, but instead of allocating and /// non-deterministically initializing the the argument `expr` passed to that /// function, we create a static global object of type \p type and @@ -1593,7 +1385,7 @@ exprt object_factory( code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, - allocation_typet alloc_type, + lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector) { @@ -1615,10 +1407,7 @@ exprt object_factory( bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr); CHECK_RETURN(!moving_symbol_failed); - std::vector symbols_created; - symbols_created.push_back(main_symbol_ptr); java_object_factoryt state( - symbols_created, loc, parameters, symbol_table, @@ -1630,14 +1419,15 @@ exprt object_factory( false, // is_sub "", // class_identifier false, // skip_classid - alloc_type, + lifetime, false, // override typet(), // override_type is immaterial 1, // initial depth update_in_placet::NO_UPDATE_IN_PLACE, loc); - declare_created_symbols(symbols_created, loc, init_code); + state.add_created_symbol(main_symbol_ptr); + state.declare_created_symbols(init_code); init_code.append(assignments); return object; @@ -1662,9 +1452,9 @@ exprt object_factory( /// Source location to which all generated code will be associated to. /// \param skip_classid: /// If true, skip initializing field `@class_identifier`. -/// \param alloc_type: -/// Allocate new objects as global objects (GLOBAL) or as local variables -/// (LOCAL) or using malloc (DYNAMIC). +/// \param lifetime: +/// Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or +/// DYNAMIC) /// \param object_factory_parameters: /// Parameters for the generation of non deterministic objects. /// \param pointer_type_selector: @@ -1684,15 +1474,12 @@ void gen_nondet_init( symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place) { - std::vector symbols_created; - java_object_factoryt state( - symbols_created, loc, object_factory_parameters, symbol_table, @@ -1704,14 +1491,14 @@ void gen_nondet_init( false, // is_sub "", // class_identifier skip_classid, - alloc_type, + lifetime, false, // override typet(), // override_type is immaterial 1, // initial depth update_in_place, loc); - declare_created_symbols(symbols_created, loc, init_code); + state.declare_created_symbols(init_code); init_code.append(assignments); } @@ -1723,7 +1510,7 @@ exprt object_factory( code_blockt &init_code, symbol_tablet &symbol_table, const java_object_factory_parameterst &object_factory_parameters, - allocation_typet alloc_type, + lifetimet lifetime, const source_locationt &location) { select_pointer_typet pointer_type_selector; @@ -1733,7 +1520,7 @@ exprt object_factory( init_code, symbol_table, object_factory_parameters, - alloc_type, + lifetime, location, pointer_type_selector); } @@ -1745,7 +1532,7 @@ void gen_nondet_init( symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place) { @@ -1756,7 +1543,7 @@ void gen_nondet_init( symbol_table, loc, skip_classid, - alloc_type, + lifetime, object_factory_parameters, pointer_type_selector, update_in_place); diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index 3b07a20e3ed..93cfb77d5d4 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -74,28 +74,18 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_language.h" #include "select_pointer_type.h" +#include #include #include #include -/// Selects the kind of allocation used by the object factories -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, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, - allocation_typet alloc_type, + lifetimet lifetime, const source_locationt &location, const select_pointer_typet &pointer_type_selector); @@ -105,7 +95,7 @@ exprt object_factory( code_blockt &init_code, symbol_tablet &symbol_table, const java_object_factory_parameterst &object_factory_parameters, - allocation_typet alloc_type, + lifetimet lifetime, const source_locationt &location); enum class update_in_placet @@ -121,7 +111,7 @@ void gen_nondet_init( symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place); @@ -132,25 +122,8 @@ void gen_nondet_init( symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, - allocation_typet alloc_type, + lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place); -exprt allocate_dynamic_object( - const exprt &target_expr, - const typet &allocate_type, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &output_code, - std::vector &symbols_created, - bool cast_needed = false); - -exprt allocate_dynamic_object_with_decl( - const exprt &target_expr, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &output_code); - #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 89cbe14ab7f..d39905a1190 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -259,7 +259,7 @@ static void clinit_wrapper_do_recursive_calls( symbol_table, source_locationt(), false, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); @@ -870,7 +870,7 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body( symbol_table, location, false, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 57daaa1e6e5..be1c2b589d5 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -16,13 +16,14 @@ Date: April 2017 /// java standard library. In particular methods from java.lang.String, /// java.lang.StringBuilder, java.lang.StringBuffer. +#include #include -#include -#include +#include #include #include +#include +#include #include -#include #include "java_types.h" #include "java_object_factory.h" @@ -575,7 +576,14 @@ exprt java_string_library_preprocesst::allocate_fresh_string( code_blockt &code) { exprt str=fresh_string(type, loc, symbol_table); - allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code); + + allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table); + + code_blockt tmp; + allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype()); + allocate_objects.declare_created_symbols(code); + code.append(tmp); + return str; } @@ -1380,8 +1388,14 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format( ID_java, symbol_table); symbol_exprt arg_i=object_symbol.symbol_expr(); - allocate_dynamic_object_with_decl( - arg_i, symbol_table, loc, function_id, code); + + allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table); + + code_blockt tmp; + allocate_objects.allocate_dynamic_object(tmp, arg_i, arg_i.type().subtype()); + allocate_objects.declare_created_symbols(code); + code.append(tmp); + code.add(code_assignt(arg_i, obj), loc); code.add( code_assumet( diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 7b68aba3d1d..a17e8ab6033 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -123,7 +123,7 @@ void java_simple_method_stubst::create_method_stub_at( symbol_table, loc, is_constructor, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, parameters, update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE : update_in_placet::NO_UPDATE_IN_PLACE); @@ -208,7 +208,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) symbol_table, source_locationt(), false, - allocation_typet::LOCAL, // Irrelevant as type is primitive + lifetimet::AUTOMATIC_LOCAL, // Irrelevant as type is primitive parameters, update_in_placet::NO_UPDATE_IN_PLACE); } diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 3d2b388a965..6ee153fbd19 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -59,7 +59,7 @@ SCENARIO( symbol_table, loc, false, - allocation_typet::DYNAMIC, + lifetimet::DYNAMIC, object_factory_parameters, update_in_placet::NO_UPDATE_IN_PLACE); From 890be45178649726bc038010a4645e999285b751 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 18 Dec 2018 14:19:18 +0000 Subject: [PATCH 4/4] Make nondet function arg regression tests independent of variable output order --- .../cbmc/pointer-function-parameters-2/test.desc | 16 ++++++++++++---- .../cbmc/pointer-function-parameters/test.desc | 6 +++--- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index 5ffe7f3fa78..60a0c1b3785 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-2/test.desc @@ -3,10 +3,18 @@ main.c --function fun --cover branch ^\*\* 7 of 7 covered \(100.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$ -^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ -^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$ -^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ +a=\(\(signed int \*\*\)NULL\) +tmp(\$\d+)?=[^,]* +tmp(\$\d+)?=[^,]* +a=&tmp(\$\d+)?!0 +tmp(\$\d+)?=\(\(signed int \*\)NULL\) +tmp(\$\d+)?=[^,]* +a=&tmp(\$\d+)?!0 +tmp(\$\d+)?=&tmp\$\d+!0 +tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+) +a=&tmp(\$\d+)?!0 +tmp(\$\d+)?=&tmp(\$\d+)?!0 +tmp(\$\d+)?=4 ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index a816cc3039a..8070ac7cbbb 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -3,9 +3,9 @@ main.c --function fun --cover branch ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ -^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ -^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$ +^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$ +^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0)$ +^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0)$ ^EXIT=0$ ^SIGNAL=0$ --