From 5a886195ff02df064b354fa5574f9588762d4525 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Jun 2017 17:55:03 +0100 Subject: [PATCH 1/4] Split up gen_nondet_init function Broke up the code handling initilising a pointer into a standalone function. --- src/java_bytecode/java_object_factory.cpp | 128 ++++++++++++++-------- 1 file changed, 81 insertions(+), 47 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 5f97bbfa529..7594a30a7fe 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -110,6 +110,14 @@ class java_object_factoryt bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet()); + +private: + void gen_nondet_pointer_init( + code_blockt &assignments, + const exprt &expr, + const irep_idt &class_identifier, + bool create_dynamic_objects, + const pointer_typet &pointer_type); }; /// \param assignments: The code block to add code to @@ -250,6 +258,74 @@ void java_object_factoryt::gen_pointer_target_init( } } +/// Initialises a primitive or object tree rooted at `expr`, of type pointer. It +/// allocates child objects as necessary and nondet-initialising their members, +/// \param assignments - the code block we are building with +/// initilisation code +/// \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 pointer_type - The type of the pointer we are initalising +void java_object_factoryt::gen_nondet_pointer_init( + code_blockt &assignments, + const exprt &expr, + const irep_idt &class_identifier, + bool create_dynamic_objects, + const pointer_typet &pointer_type) +{ + const typet &subtype=ns.follow(pointer_type.subtype()); + + if(subtype.id()==ID_struct) + { + const struct_typet &struct_type=to_struct_type(subtype); + const irep_idt struct_tag=struct_type.get_tag(); + // set to null if found in recursion set and not a sub-type + if(recursion_set.find(struct_tag)!=recursion_set.end() && + struct_tag==class_identifier) + { + assignments.copy_to_operands( + get_null_assignment(expr, pointer_type)); + return; + } + } + + code_blockt non_null_inst; + gen_pointer_target_init( + non_null_inst, + expr, + subtype, + create_dynamic_objects); + + if(assume_non_null) + { + // Add the following code to assignments: + // = ; + assignments.append(non_null_inst); + } + else + { + // if(NONDET(_Bool) + // { + // = + // } + // else + // { + // > + // } + 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; + null_check.else_case()=non_null_inst; + + assignments.add(null_check); + } +} + /// Creates a nondet for expr, including calling itself recursively to make /// appropriate symbols to point to if expr is a pointer or struct /// \param expr: The expression which we are generating a non-determinate value @@ -277,54 +353,12 @@ void java_object_factoryt::gen_nondet_init( { // dereferenced type const pointer_typet &pointer_type=to_pointer_type(type); - const typet &subtype=ns.follow(pointer_type.subtype()); - - if(subtype.id()==ID_struct) - { - const struct_typet &struct_type=to_struct_type(subtype); - const irep_idt struct_tag=struct_type.get_tag(); - // set to null if found in recursion set and not a sub-type - if(recursion_set.find(struct_tag)!=recursion_set.end() && - struct_tag==class_identifier) - { - assignments.copy_to_operands( - get_null_assignment(expr, pointer_type)); - return; - } - } - - code_blockt non_null_inst; - gen_pointer_target_init( - non_null_inst, + gen_nondet_pointer_init( + assignments, expr, - subtype, - create_dynamic_objects); - - if(assume_non_null) - { - // Add the following code to assignments: - // = ; - assignments.append(non_null_inst); - } - else - { - // Add the following code to assignments: - // IF !NONDET(_Bool) THEN GOTO - // = - // GOTO - // : = &tmp$; - // > - // And the next line is labelled label2 - 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; - null_check.else_case()=non_null_inst; - - assignments.add(null_check); - } + class_identifier, + create_dynamic_objects, + pointer_type); } else if(type.id()==ID_struct) { From f4e8a9ab632c869cb2f7b0658c2e8a1c31a1bc1d Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Jun 2017 18:00:10 +0100 Subject: [PATCH 2/4] Split up gen_nondet_init for structs Split out the logic for initilising a struct into a standalone method --- src/java_bytecode/java_object_factory.cpp | 138 ++++++++++++++-------- 1 file changed, 86 insertions(+), 52 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 7594a30a7fe..7a38c8034fc 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -118,6 +118,14 @@ class java_object_factoryt const irep_idt &class_identifier, bool create_dynamic_objects, const pointer_typet &pointer_type); + + void gen_nondet_struct_init( + code_blockt &assignments, + const exprt &expr, + bool is_sub, + irep_idt class_identifier, + bool create_dynamic_objects, + const struct_typet &struct_type); }; /// \param assignments: The code block to add code to @@ -326,6 +334,77 @@ void java_object_factoryt::gen_nondet_pointer_init( } } +/// Initialises an object tree rooted at `expr`, allocating child objects as +/// necessary and nondet-initialising their members. +/// \param assignments: The code block to append the new +/// instructions to +/// \param expr: pointer-typed lvalue expression to initialise +/// \param is_sub: If true, `expr` is a substructure of a larger object, which +/// in Java necessarily means a base class. not match *expr (for example, expr +/// might be void*) +/// \param class_identifier: clsid to initialise @java.lang.Object. +/// @class_identifier +/// \param create_dynamic_objects: if true, use malloc to allocate objects; +/// otherwise generate fresh static symbols. +/// \param struct_type - The type of the struct we are initalising +void java_object_factoryt::gen_nondet_struct_init( + code_blockt &assignments, + const exprt &expr, + bool is_sub, + irep_idt class_identifier, + bool create_dynamic_objects, + const struct_typet &struct_type) +{ + typedef struct_typet::componentst componentst; + + const irep_idt struct_tag=struct_type.get_tag(); + + const componentst &components=struct_type.components(); + + if(!is_sub) + class_identifier=struct_tag; + + recursion_set.insert(struct_tag); + assert(!recursion_set.empty()); + + for(const auto &component : components) + { + const typet &component_type=component.type(); + irep_idt name=component.get_name(); + + member_exprt me(expr, name, component_type); + + if(name=="@class_identifier") + { + irep_idt qualified_clsid="java::"+as_string(class_identifier); + constant_exprt ci(qualified_clsid, string_typet()); + code_assignt code(me, ci); + code.add_source_location()=loc; + assignments.copy_to_operands(code); + } + else if(name=="@lock") + { + code_assignt code(me, from_integer(0, me.type())); + code.add_source_location()=loc; + assignments.copy_to_operands(code); + } + else + { + assert(!name.empty()); + + bool _is_sub=name[0]=='@'; + + gen_nondet_init( + assignments, + me, + _is_sub, + class_identifier, + create_dynamic_objects); + } + } + recursion_set.erase(struct_tag); +} + /// Creates a nondet for expr, including calling itself recursively to make /// appropriate symbols to point to if expr is a pointer or struct /// \param expr: The expression which we are generating a non-determinate value @@ -362,59 +441,14 @@ void java_object_factoryt::gen_nondet_init( } else if(type.id()==ID_struct) { - typedef struct_typet::componentst componentst; - const struct_typet &struct_type=to_struct_type(type); - const irep_idt struct_tag=struct_type.get_tag(); - - const componentst &components=struct_type.components(); - - if(!is_sub) - class_identifier=struct_tag; - - recursion_set.insert(struct_tag); - assert(!recursion_set.empty()); - - for(const auto &component : components) - { - const typet &component_type=component.type(); - irep_idt name=component.get_name(); - - member_exprt me(expr, name, component_type); - - if(name=="@class_identifier") - { - irep_idt qualified_clsid="java::"+as_string(class_identifier); - constant_exprt ci(qualified_clsid, string_typet()); - code_assignt code(me, ci); - code.add_source_location()=loc; - assignments.copy_to_operands(code); - } - else if(name=="@lock") - { - code_assignt code(me, from_integer(0, me.type())); - code.add_source_location()=loc; - assignments.copy_to_operands(code); - } - else - { - assert(!name.empty()); - - bool _is_sub=name[0]=='@'; -#if 0 - irep_idt _class_identifier= - _is_sub?(class_identifier.empty()?struct_tag:class_identifier):""; -#endif - - gen_nondet_init( - assignments, - me, - _is_sub, - class_identifier, - create_dynamic_objects); - } - } - recursion_set.erase(struct_tag); + gen_nondet_struct_init( + assignments, + expr, + is_sub, + class_identifier, + create_dynamic_objects, + struct_type); } else { From 0547fae072c55c342aa2313ba8511c06e89442b5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Jun 2017 18:00:59 +0100 Subject: [PATCH 3/4] Added missing comment to class_hieracrchyt --- src/goto-programs/class_hierarchy.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index 10a16760b98..77323aa83e4 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -18,6 +18,10 @@ Date: April 2016 #include "class_hierarchy.h" +/// Looks for all the struct types in the symbol table and construct a map from +/// class names to a data structure that contains lists of parent and child +/// classes for each struct type (ie class). +/// \param symbol_table: The symbol table to analyze void class_hierarchyt::operator()(const symbol_tablet &symbol_table) { forall_symbols(it, symbol_table.symbols) From e873e000cab014e1ed9e4b89811bb8a2f1cdd57b Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 19 Jun 2017 10:15:40 +0100 Subject: [PATCH 4/4] Correcting assertions Removing an assertion that validates the STL lib being correct. Changed assert to invariant that all components on a struct have a name. --- src/java_bytecode/java_object_factory.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 7a38c8034fc..987422e2618 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -365,7 +365,6 @@ void java_object_factoryt::gen_nondet_struct_init( class_identifier=struct_tag; recursion_set.insert(struct_tag); - assert(!recursion_set.empty()); for(const auto &component : components) { @@ -390,7 +389,7 @@ void java_object_factoryt::gen_nondet_struct_init( } else { - assert(!name.empty()); + INVARIANT(!name.empty(), "Each component of a struct must have a name"); bool _is_sub=name[0]=='@';