From 9ccdd32348867b91cc5c5ed73260fe0c2c468c6e Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 6 Jun 2017 13:45:30 +0100 Subject: [PATCH 1/4] Split up gen_nondet_init function Broke up the code handling initilising a pointer into a standalone funciton. --- src/java_bytecode/java_object_factory.cpp | 239 +++++++++++++--------- 1 file changed, 140 insertions(+), 99 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index ff00c5b1ef7..bb982e05168 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -117,6 +117,15 @@ class java_object_factoryt bool override, const typet &override_type, update_in_placet); + +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, + const update_in_placet &update_in_place); }; /// Generates code for allocating a dynamic object. This is used in @@ -347,6 +356,132 @@ 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, +/// or if MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated +/// objects. +/// \param assignemnts - 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 +/// `update_in_place`: NO_UPDATE_IN_PLACE: initialise `expr` from scratch +/// MUST_UPDATE_IN_PLACE: reinitialise an existing object MAY_UPDATE_IN_PLACE: +/// generate a runtime nondet branch between the NO_ and MUST_ cases. +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 update_in_placet &update_in_place) +{ + 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(); + // If this is a recursive type of some kind, set null. + if(!recursion_set.insert(struct_tag).second) + { + if(update_in_place==NO_UPDATE_IN_PLACE) + { + assignments.copy_to_operands( + get_null_assignment(expr, pointer_type)); + } + // Otherwise leave it as it is. + return; + } + } + + code_blockt new_object_assignments; + code_blockt update_in_place_assignments; + + if(update_in_place!=NO_UPDATE_IN_PLACE) + { + gen_pointer_target_init( + update_in_place_assignments, + expr, + subtype, + create_dynamic_objects, + MUST_UPDATE_IN_PLACE); + } + + if(update_in_place==MUST_UPDATE_IN_PLACE) + { + assignments.append(update_in_place_assignments); + return; + } + + // Otherwise we need code for the allocate-new-object case: + + code_blockt non_null_inst; + gen_pointer_target_init( + non_null_inst, + expr, + subtype, + create_dynamic_objects, + NO_UPDATE_IN_PLACE); + + // Determine whether the pointer can be null. + // In particular the array field of a String should not be null. + bool not_null= + assume_non_null || + ((class_identifier=="java.lang.String" || + class_identifier=="java.lang.StringBuilder" || + class_identifier=="java.lang.StringBuffer" || + class_identifier=="java.lang.CharSequence") && + subtype.id()==ID_array); + + if(not_null) + { + // Add the following code to assignments: + // = ; + new_object_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; + + new_object_assignments.add(null_check); + } + + // Similarly to above, maybe use a conditional if both the + // allocate-fresh and update-in-place cases are allowed: + if(update_in_place==NO_UPDATE_IN_PLACE) + { + assignments.append(new_object_assignments); + } + else + { + assert(update_in_place==MAY_UPDATE_IN_PLACE); + + code_ifthenelset update_check; + update_check.cond()=side_effect_expr_nondett(bool_typet()); + update_check.then_case()=update_in_place_assignments; + update_check.else_case()=new_object_assignments; + + assignments.add(update_check); + } +} + /// Initialises a primitive or object tree rooted at `expr`, allocating child /// objects as necessary and nondet-initialising their members, or if /// MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated objects. @@ -384,107 +519,13 @@ 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(); - // If this is a recursive type of some kind, set null. - if(!recursion_set.insert(struct_tag).second) - { - if(update_in_place==NO_UPDATE_IN_PLACE) - { - assignments.copy_to_operands( - get_null_assignment(expr, pointer_type)); - } - // Otherwise leave it as it is. - return; - } - } - - code_blockt new_object_assignments; - code_blockt update_in_place_assignments; - - if(update_in_place!=NO_UPDATE_IN_PLACE) - { - gen_pointer_target_init( - update_in_place_assignments, - expr, - subtype, - create_dynamic_objects, - MUST_UPDATE_IN_PLACE); - } - - if(update_in_place==MUST_UPDATE_IN_PLACE) - { - assignments.append(update_in_place_assignments); - return; - } - - // Otherwise we need code for the allocate-new-object case: - - code_blockt non_null_inst; - gen_pointer_target_init( - non_null_inst, + gen_nondet_pointer_init( + assignments, expr, - subtype, + class_identifier, create_dynamic_objects, - NO_UPDATE_IN_PLACE); - - // Determine whether the pointer can be null. - // In particular the array field of a String should not be null. - bool not_null= - assume_non_null || - ((class_identifier=="java.lang.String" || - class_identifier=="java.lang.StringBuilder" || - class_identifier=="java.lang.StringBuffer" || - class_identifier=="java.lang.CharSequence") && - subtype.id()==ID_array); - - if(not_null) - { - // Add the following code to assignments: - // = ; - new_object_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; - - new_object_assignments.add(null_check); - } - - // Similarly to above, maybe use a conditional if both the - // allocate-fresh and update-in-place cases are allowed: - if(update_in_place==NO_UPDATE_IN_PLACE) - { - assignments.append(new_object_assignments); - } - else - { - assert(update_in_place==MAY_UPDATE_IN_PLACE); - - code_ifthenelset update_check; - update_check.cond()=side_effect_expr_nondett(bool_typet()); - update_check.then_case()=update_in_place_assignments; - update_check.else_case()=new_object_assignments; - - assignments.add(update_check); - } + pointer_type, + update_in_place); } else if(type.id()==ID_struct) { From 6770e74f86b519fa1a54339acd78815125638479 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 7 Jun 2017 14:17:50 +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 | 180 ++++++++++++++-------- 1 file changed, 112 insertions(+), 68 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index bb982e05168..6af5ba30a32 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -126,6 +126,16 @@ class java_object_factoryt bool create_dynamic_objects, const pointer_typet &pointer_type, const update_in_placet &update_in_place); + + void gen_nondet_struct_init( + code_blockt &assignments, + const exprt &expr, + bool is_sub, + irep_idt class_identifier, + bool skip_classid, + bool create_dynamic_objects, + const struct_typet &struct_type, + const update_in_placet &update_in_place); }; /// Generates code for allocating a dynamic object. This is used in @@ -482,6 +492,98 @@ 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, or if MUST_UPDATE_IN_PLACE +/// is set, re-initialising already-allocated objects. +/// \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 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 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: +/// invalid input +void java_object_factoryt::gen_nondet_struct_init( + code_blockt &assignments, + const exprt &expr, + bool is_sub, + irep_idt class_identifier, + bool skip_classid, + bool create_dynamic_objects, + const struct_typet &struct_type, + const update_in_placet &update_in_place) +{ + 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; + + 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") + { + if(update_in_place==MUST_UPDATE_IN_PLACE) + continue; + + if(skip_classid) + continue; + + 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") + { + if(update_in_place==MUST_UPDATE_IN_PLACE) + continue; + 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]=='@'; + + // MUST_UPDATE_IN_PLACE only applies to this object. + // If this is a pointer to another object, offer the chance + // to leave it alone by setting MAY_UPDATE_IN_PLACE instead. + update_in_placet substruct_in_place= + update_in_place==MUST_UPDATE_IN_PLACE && !_is_sub ? + MAY_UPDATE_IN_PLACE : + update_in_place; + gen_nondet_init( + assignments, + me, + _is_sub, + class_identifier, + false, + create_dynamic_objects, + false, + typet(), + substruct_in_place); + } + } +} + /// Initialises a primitive or object tree rooted at `expr`, allocating child /// objects as necessary and nondet-initialising their members, or if /// MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated objects. @@ -529,74 +631,16 @@ 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; - - 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") - { - if(update_in_place==MUST_UPDATE_IN_PLACE) - continue; - - if(skip_classid) - continue; - - 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") - { - if(update_in_place==MUST_UPDATE_IN_PLACE) - continue; - 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 - - // MUST_UPDATE_IN_PLACE only applies to this object. - // If this is a pointer to another object, offer the chance - // to leave it alone by setting MAY_UPDATE_IN_PLACE instead. - update_in_placet substruct_in_place= - update_in_place==MUST_UPDATE_IN_PLACE && !_is_sub ? - MAY_UPDATE_IN_PLACE : - update_in_place; - gen_nondet_init( - assignments, - me, - _is_sub, - class_identifier, - false, - create_dynamic_objects, - false, - typet(), - substruct_in_place); - } - } + const struct_typet struct_type=to_struct_type(type); + gen_nondet_struct_init( + assignments, + expr, + is_sub, + class_identifier, + skip_classid, + create_dynamic_objects, + struct_type, + update_in_place); } else { From 90c8198fca0678e3bb1d706eefd14bc9b4a42302 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 5 Jun 2017 11:07:37 +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 fde9c7659c1b0c6c2d6288d093ba6ce24bdb0b9f Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 19 Jun 2017 10:51:09 +0100 Subject: [PATCH 4/4] Correcting assertions. Changed assert to invariant that all components on a struct have a name. Changed assert to invariant that must and no update in places cases have been correctly dealt with. --- src/java_bytecode/java_object_factory.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 6af5ba30a32..efcd97f335e 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -481,7 +482,8 @@ void java_object_factoryt::gen_nondet_pointer_init( } else { - assert(update_in_place==MAY_UPDATE_IN_PLACE); + INVARIANT(update_in_place==MAY_UPDATE_IN_PLACE, + "No update and must update should have already been resolved"); code_ifthenelset update_check; update_check.cond()=side_effect_expr_nondett(bool_typet()); @@ -559,7 +561,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]=='@';