From ba49ce83e41c4ea5bf9c1eecca356563576a74d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 10 Mar 2017 15:43:40 +0100 Subject: [PATCH] Factor nondet choices in object factory This splits the nondet-if-then-else concept into a utility. It only has one user here, but downstream branches already have several users. This reduces the diff between branches for easier future merges. --- src/java_bytecode/java_object_factory.cpp | 177 ++++++++++++++-------- src/util/Makefile | 1 + src/util/nondet_bool.h | 34 +++++ src/util/nondet_ifthenelse.cpp | 134 ++++++++++++++++ src/util/nondet_ifthenelse.h | 44 ++++++ 5 files changed, 323 insertions(+), 67 deletions(-) create mode 100644 src/util/nondet_bool.h create mode 100644 src/util/nondet_ifthenelse.cpp create mode 100644 src/util/nondet_ifthenelse.h diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 34f5495bb85..036a29933aa 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include @@ -51,25 +53,6 @@ static symbolt &new_tmp_symbol( symbol_table); } -/*******************************************************************\ - -Function: get_nondet_bool - - Inputs: Desired type (C_bool or plain bool) - - Outputs: nondet expr of that type - - Purpose: - -\*******************************************************************/ - -static exprt get_nondet_bool(const typet &type) -{ - // We force this to 0 and 1 and won't consider - // other values. - return typecast_exprt(side_effect_expr_nondett(bool_typet()), type); -} - class java_object_factoryt { code_blockt &init_code; @@ -79,6 +62,17 @@ class java_object_factoryt symbol_tablet &symbol_table; namespacet ns; + void set_null( + const exprt &expr, + const pointer_typet &ptr_type, + const source_locationt &); + + void gen_pointer_target_init( + const exprt &expr, + const typet &target_type, + bool create_dynamic_objects, + const source_locationt &); + public: java_object_factoryt( code_blockt &_init_code, @@ -192,6 +186,87 @@ exprt java_object_factoryt::allocate_object( /*******************************************************************\ +Function: java_object_factoryt::set_null + + Inputs: `expr`: pointer-typed lvalue expression to initialise + `ptr_type`: pointer type to write + + Outputs: + + Purpose: Adds an instruction to `init_code` null-initialising + `expr`. + +\*******************************************************************/ + +void java_object_factoryt::set_null( + const exprt &expr, + const pointer_typet &ptr_type, + const source_locationt &loc) +{ + null_pointer_exprt null_pointer_expr(ptr_type); + code_assignt code(expr, null_pointer_expr); + code.add_source_location()=loc; + init_code.move_to_operands(code); +} + +/*******************************************************************\ + +Function: java_object_factoryt::gen_pointer_target_init + + Inputs: `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. + + Outputs: + + Purpose: Initialises an object tree rooted at `expr`, allocating + child objects as necessary and nondet-initialising their + members. + +\*******************************************************************/ + +void java_object_factoryt::gen_pointer_target_init( + const exprt &expr, + const typet &target_type, + bool create_dynamic_objects, + const source_locationt &loc) +{ + if(target_type.id()==ID_struct && + has_prefix( + id2string(to_struct_type(target_type).get_tag()), + "java::array[")) + { + gen_nondet_array_init(expr, loc); + } + else + { + exprt target= + allocate_object( + expr, + target_type, + loc, + create_dynamic_objects); + 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( + init_expr, + false, + "", + loc, + create_dynamic_objects, + false, + typet()); + } +} + +/*******************************************************************\ + Function: java_object_factoryt::gen_nondet_init Inputs: @@ -238,65 +313,33 @@ void java_object_factoryt::gen_nondet_init( if(recursion_set.find(struct_tag)!=recursion_set.end() && struct_tag==class_identifier) { - // make null - null_pointer_exprt null_pointer_expr(pointer_type); - code_assignt code(expr, null_pointer_expr); - code.add_source_location()=loc; - init_code.copy_to_operands(code); - + set_null(expr, pointer_type, loc); return; } } - code_labelt set_null_label; - code_labelt init_done_label; + nondet_ifthenelset init_null_diamond( + init_code, + symbol_table, + loc, + ID_java, + "nondet_ptr_is_null"); if(!assume_non_null) { - auto set_null_inst= - code_assignt(expr, null_pointer_exprt(pointer_type)); - set_null_inst.add_source_location()=loc; - - static size_t synthetic_constructor_count=0; - std::string fresh_label= - "post_synthetic_malloc_"+std::to_string(++synthetic_constructor_count); - set_null_label=code_labelt(fresh_label, set_null_inst); - - init_done_label=code_labelt(fresh_label+"_init_done", code_skipt()); - - code_ifthenelset null_check; - exprt null_return=from_integer(0, c_bool_typet(1)); - null_check.cond()= - notequal_exprt(get_nondet_bool(c_bool_typet(1)), null_return); - null_check.then_case()=code_gotot(fresh_label); - init_code.move_to_operands(null_check); + init_null_diamond.begin_if(); + set_null(expr, pointer_type, loc); + init_null_diamond.begin_else(); } - if(java_is_array_type(subtype)) - gen_nondet_array_init(expr, loc); - else - { - exprt allocated= - allocate_object(expr, subtype, loc, create_dynamic_objects); - 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( - init_expr, - false, - "", - loc, - create_dynamic_objects); - } + gen_pointer_target_init( + expr, + subtype, + create_dynamic_objects, + loc); if(!assume_non_null) - { - init_code.copy_to_operands(code_gotot(init_done_label.get_label())); - init_code.move_to_operands(set_null_label); - init_code.move_to_operands(init_done_label); - } + init_null_diamond.finish(); } else if(type.id()==ID_struct) { diff --git a/src/util/Makefile b/src/util/Makefile index 154792d1331..7c16c9d5bf9 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -40,6 +40,7 @@ SRC = arith_tools.cpp \ message.cpp \ mp_arith.cpp \ namespace.cpp \ + nondet_ifthenelse.cpp \ options.cpp \ parse_options.cpp \ parser.cpp \ diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h new file mode 100644 index 00000000000..6aee700b889 --- /dev/null +++ b/src/util/nondet_bool.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Nondeterministic boolean helper + +Author: Chris Smowton, chris@smowton.net + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_NONDET_BOOL_H +#define CPROVER_UTIL_NONDET_BOOL_H + +#include +#include + +/*******************************************************************\ + +Function: get_nondet_bool + + Inputs: Desired type (C_bool or plain bool) + + Outputs: nondet expr of that type + + Purpose: + +\*******************************************************************/ + +inline exprt get_nondet_bool(const typet &type) +{ + // We force this to 0 and 1 and won't consider + // other values. + return typecast_exprt(side_effect_expr_nondett(bool_typet()), type); +} + +#endif // CPROVER_UTIL_NONDET_BOOL_H diff --git a/src/util/nondet_ifthenelse.cpp b/src/util/nondet_ifthenelse.cpp new file mode 100644 index 00000000000..ae2f9040977 --- /dev/null +++ b/src/util/nondet_ifthenelse.cpp @@ -0,0 +1,134 @@ +/*******************************************************************\ + +Module: Nondeterministic if-then-else + +Author: Chris Smowton, chris@smowton.net + +\*******************************************************************/ + +#include "nondet_ifthenelse.h" + +#include + +#include +#include +#include +#include +#include +#include + +// This will be unified with other similar fresh-symbol routines shortly +static symbolt &new_tmp_symbol( + symbol_tablet &symbol_table, + const std::string &prefix, + const irep_idt &mode) +{ + static size_t temporary_counter=0; + + auxiliary_symbolt new_symbol; + symbolt *symbol_ptr; + + do + { + new_symbol.name="tmp_object_factory$"+std::to_string(++temporary_counter); + new_symbol.base_name=new_symbol.name; + new_symbol.mode=mode; + } + while(symbol_table.move(new_symbol, symbol_ptr)); + + return *symbol_ptr; +} + +/*******************************************************************\ + +Function: nondet_ifthenelset::begin_if + + Inputs: + + Outputs: + + Purpose: Emits instructions and defines labels for the beginning of + a nondeterministic if-else diamond. Code is emitted to the + `result_code` member of this object's associated + `java_object_factoryt` instance `state`. + The caller should use the following pattern (where *this + is an instance of java_object_factoryt): + ``` + nondet_ifthenelset diamond(*this, "name"); + diamond.begin_if(); + result_code.copy_to_operands(Some if-branch code) + diamond.begin_else(); + result_code.copy_to_operands(Some else-branch code) + diamond.finish(); + ``` + +\*******************************************************************/ + +void nondet_ifthenelset::begin_if() +{ + static size_t nondet_ifthenelse_count=0; + + auto choice_sym= + new_tmp_symbol(symbol_table, choice_symname, fresh_symbol_mode); + choice_sym.type=c_bool_typet(1); + auto choice=choice_sym.symbol_expr(); + auto assign_choice= + code_assignt(choice, get_nondet_bool(choice_sym.type)); + assign_choice.add_source_location()=loc; + result_code.move_to_operands(assign_choice); + + std::ostringstream fresh_label_oss; + fresh_label_oss << choice_symname << "_else_" + << (++nondet_ifthenelse_count); + std::string fresh_label=fresh_label_oss.str(); + else_label=code_labelt(fresh_label, code_skipt()); + + std::ostringstream done_label_oss; + done_label_oss << choice_symname << "_done_" + << nondet_ifthenelse_count; + join_label=code_labelt(done_label_oss.str(), code_skipt()); + + code_ifthenelset test; + test.cond()=equal_exprt( + choice, + constant_exprt("0", choice_sym.type)); + test.then_case()=code_gotot(fresh_label); + result_code.move_to_operands(test); +} + +/*******************************************************************\ + +Function: nondet_ifthenelset::begin_else + + Inputs: + + Outputs: + + Purpose: Terminates the if-block and begins the else-block of a + nondet if-then-else diamond. See ::begin_if for detail. + +\*******************************************************************/ + +void nondet_ifthenelset::begin_else() +{ + result_code.copy_to_operands(code_gotot(join_label.get_label())); + result_code.copy_to_operands(else_label); +} + +/*******************************************************************\ + +Function: nondet_ifthenelset::finish + + Inputs: + + Outputs: + + Purpose: Concludes a nondet if-then-else diamond. + See ::begin_if for detail. + +\*******************************************************************/ + +void nondet_ifthenelset::finish() +{ + result_code.move_to_operands(join_label); +} diff --git a/src/util/nondet_ifthenelse.h b/src/util/nondet_ifthenelse.h new file mode 100644 index 00000000000..c6ee25afcab --- /dev/null +++ b/src/util/nondet_ifthenelse.h @@ -0,0 +1,44 @@ +/*******************************************************************\ + +Module: Nondeterministic if-then-else + +Author: Chris Smowton, chris@smowton.net + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_NONDET_IFTHENELSE_H +#define CPROVER_UTIL_NONDET_IFTHENELSE_H + +#include + +class symbol_tablet; +class source_locationt; + +class nondet_ifthenelset +{ + code_blockt &result_code; + symbol_tablet &symbol_table; + const source_locationt &loc; + irep_idt fresh_symbol_mode; + code_labelt else_label; + code_labelt join_label; + const std::string choice_symname; + public: + nondet_ifthenelset( + code_blockt &_result_code, + symbol_tablet &_symbol_table, + const source_locationt &_loc, + const irep_idt &_fresh_symbol_mode, + const std::string &name) : + result_code(_result_code), + symbol_table(_symbol_table), + loc(_loc), + fresh_symbol_mode(_fresh_symbol_mode), + choice_symname(name) + {} + void begin_if(); + void begin_else(); + void finish(); +}; + +#endif // CPROVER_UTIL_NONDET_IFTHENELSE_H