From cb0f3100f7c8b97612cf406149a489d8cce1ce1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 2 Aug 2018 10:31:13 +0200 Subject: [PATCH 1/5] Add nondet.{h.cpp} --- jbmc/src/java_bytecode/Makefile | 1 + jbmc/src/java_bytecode/nondet.cpp | 131 ++++++++++++++++++++++++++++++ jbmc/src/java_bytecode/nondet.h | 34 ++++++++ 3 files changed, 166 insertions(+) create mode 100644 jbmc/src/java_bytecode/nondet.cpp create mode 100644 jbmc/src/java_bytecode/nondet.h diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 5d4e734a0e5..07d67543380 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -35,6 +35,7 @@ SRC = bytecode_info.cpp \ java_utils.cpp \ load_method_by_regex.cpp \ mz_zip_archive.cpp \ + nondet.cpp \ remove_exceptions.cpp \ remove_instanceof.cpp \ remove_java_new.cpp \ diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp new file mode 100644 index 00000000000..406b2f77201 --- /dev/null +++ b/jbmc/src/java_bytecode/nondet.cpp @@ -0,0 +1,131 @@ +/*******************************************************************\ + +Module: Non-deterministic object init and choice for JBMC + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "nondet.h" + +#include +#include +#include +#include +#include + +/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated +/// resembles: +/// ``` +/// int_type name_prefix::nondet_int = NONDET(int_type) +/// ASSUME(name_prefix::nondet_int >= min_value) +/// ASSUME(name_prefix::nondet_int <= max_value) +/// ``` +/// \param min_value: Minimum value (inclusive) of returned int. +/// \param max_value: Maximum value (inclusive) of returned int. +/// \param name_prefix: Prefix for the fresh symbol name generated. +/// \param int_type: The type of the int used to non-deterministically choose +/// one of the switch cases. +/// \param source_location: The location to mark the generated int with. +/// \param symbol_table: The global symbol table. +/// \param instructions [out]: Output instructions are written to +/// 'instructions'. These declare, nondet-initialise and range-constrain (with +/// assume statements) a fresh integer. +/// \return Returns a symbol expression for the resulting integer. +symbol_exprt generate_nondet_int( + const int64_t min_value, + const int64_t max_value, + const std::string &name_prefix, + const typet &int_type, + const source_locationt &source_location, + symbol_table_baset &symbol_table, + code_blockt &instructions) +{ + PRECONDITION(min_value < max_value); + + // Declare a symbol for the non deterministic integer. + const symbol_exprt &nondet_symbol = get_fresh_aux_symbol( + int_type, + name_prefix + "::nondet_int", + "nondet_int", + source_location, + ID_java, + symbol_table) + .symbol_expr(); + instructions.add(code_declt(nondet_symbol)); + + // Assign the symbol any non deterministic integer value. + // int_type name_prefix::nondet_int = NONDET(int_type) + instructions.add( + code_assignt(nondet_symbol, side_effect_expr_nondett(int_type))); + + // Constrain the non deterministic integer with a lower bound of `min_value`. + // ASSUME(name_prefix::nondet_int >= min_value) + instructions.add( + code_assumet( + binary_predicate_exprt( + nondet_symbol, ID_ge, from_integer(min_value, int_type)))); + + // Constrain the non deterministic integer with an upper bound of `max_value`. + // ASSUME(name_prefix::nondet_int <= max_value) + instructions.add( + code_assumet( + binary_predicate_exprt( + nondet_symbol, ID_le, from_integer(max_value, int_type)))); + + return nondet_symbol; +} + +/// Pick nondeterministically between imperative actions 'switch_cases'. +/// \param name_prefix: Name prefix for fresh symbols +/// \param switch_cases: List of codet objects to execute in each switch case. +/// \param int_type: The type of the int used to non-deterministically choose +/// one of the switch cases. +/// \param source_location: The location to mark the generated int with. +/// \param symbol_table: The global symbol table. +/// \return Returns a nondet-switch choosing between switch_cases. The resulting +/// switch block has no default case. +code_blockt generate_nondet_switch( + const irep_idt &name_prefix, + const alternate_casest &switch_cases, + const typet &int_type, + const source_locationt &source_location, + symbol_table_baset &symbol_table) +{ + PRECONDITION(!switch_cases.empty()); + + if(switch_cases.size() == 1) + return code_blockt({switch_cases[0]}); + + code_switcht result_switch; + code_blockt result_block; + + const symbol_exprt &switch_value = generate_nondet_int( + 0, + switch_cases.size() - 1, + id2string(name_prefix), + int_type, + source_location, + symbol_table, + result_block); + + result_switch.value() = switch_value; + + code_blockt switch_block; + int64_t case_number = 0; + for(const auto &switch_case : switch_cases) + { + code_blockt this_block; + this_block.add(switch_case); + this_block.add(code_breakt()); + code_switch_caset this_case; + this_case.case_op() = from_integer(case_number, switch_value.type()); + this_case.code() = this_block; + switch_block.move(this_case); + ++case_number; + } + + result_switch.body() = switch_block; + result_block.move(result_switch); + return result_block; +} diff --git a/jbmc/src/java_bytecode/nondet.h b/jbmc/src/java_bytecode/nondet.h new file mode 100644 index 00000000000..59264f926ce --- /dev/null +++ b/jbmc/src/java_bytecode/nondet.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + + Module: Non-deterministic object init and choice for JBMC + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_NONDET_H +#define CPROVER_JAVA_BYTECODE_NONDET_H + +#include +#include +#include + +symbol_exprt generate_nondet_int( + int64_t min_value, + int64_t max_value, + const std::string &name_prefix, + const typet &int_type, + const source_locationt &source_location, + symbol_table_baset &symbol_table, + code_blockt &instructions); + +typedef std::vector alternate_casest; + +code_blockt generate_nondet_switch( + const irep_idt &name_prefix, + const alternate_casest &switch_cases, + const typet &int_type, + const source_locationt &source_location, + symbol_table_baset &symbol_table); + +#endif // CPROVER_JAVA_BYTECODE_NONDET_H From d2bc0123b372dfd4173f1c8cc71911d6845f0076 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 23 Jul 2018 09:47:56 +0200 Subject: [PATCH 2/5] Allow multi object type parameter in entry point function call --- jbmc/src/java_bytecode/java_entry_point.cpp | 96 ++++++++++++++++--- .../src/java_bytecode/select_pointer_type.cpp | 9 ++ jbmc/src/java_bytecode/select_pointer_type.h | 5 + 3 files changed, 99 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 73fadb9b697..859b707bef6 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_object_factory.h" #include "java_string_literals.h" #include "java_utils.h" +#include "nondet.h" +#include #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V" @@ -317,17 +319,89 @@ exprt::operandst java_build_arguments( parameters.function_id = goto_functionst::entry_point(); - // generate code to allocate and non-deterministicaly initialize the - // argument - main_arguments[param_number] = object_factory( - p.type(), - base_name, - init_code, - symbol_table, - parameters, - allocation_typet::LOCAL, - function.location, - pointer_type_selector); + namespacet ns(symbol_table); + + // Generate code to allocate and non-deterministicaly initialize the + // argument, if the argument has different possible object types (e.g., from + // casts in the function body), then choose one in a non-deterministic way. + const auto alternatives = + pointer_type_selector.get_parameter_alternative_types( + function.name, p.get_identifier(), ns); + if(!alternatives.has_value()) + { + main_arguments[param_number] = object_factory( + p.type(), + base_name, + init_code, + symbol_table, + parameters, + allocation_typet::LOCAL, + function.location, + pointer_type_selector); + } + else + { + INVARIANT(!is_this, "We cannot have different types for `this` here"); + // create a non-deterministic switch between all possible values for the + // type of the parameter. + const auto alternative_object_types = alternatives.value(); + code_switcht code_switch; + + // the idea is to get a new symbol for the parameter value `tmp` + + // then add a non-deterministic switch over all possible input types, + // construct the object type at hand and assign to `tmp` + + // switch(...) + // { + // case obj1: + // tmp_expr = object_factory(...) + // param = tmp_expr + // break + // ... + // } + // method(..., param, ...) + // + + const symbolt result_symbol = get_fresh_aux_symbol( + p.type(), + "nondet_parameter_" + std::to_string(param_number), + "nondet_parameter_" + std::to_string(param_number), + function.location, + ID_java, + symbol_table); + main_arguments[param_number] = result_symbol.symbol_expr(); + + std::vector cases; + size_t alternative = 0; + for(const auto &type : alternative_object_types) + { + code_blockt init_code_for_type; + exprt init_expr_for_parameter = object_factory( + java_reference_type(type), + id2string(base_name) + "_alt_" + std::to_string(alternative), + init_code_for_type, + symbol_table, + parameters, + allocation_typet::DYNAMIC, + function.location, + pointer_type_selector); + alternative++; + init_code_for_type.add( + code_assignt( + result_symbol.symbol_expr(), + typecast_exprt(init_expr_for_parameter, p.type()))); + cases.push_back(init_code_for_type); + } + + init_code.add( + generate_nondet_switch( + id2string(function.base_name) + "_" + std::to_string(param_number), + cases, + java_int_type(), + function.location, + symbol_table)); + } // record as an input codet input(ID_input); diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index e9b69ba002a..ee548c03bec 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -223,3 +223,12 @@ select_pointer_typet::get_recursively_instantiated_type( visited.erase(parameter_name); return inst_val; } + +optionalt> +select_pointer_typet::get_parameter_alternative_types( + const irep_idt &function_name, + const irep_idt ¶meter_name, + const namespacet &ns) const +{ + return {}; +} diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 64c1127f6c1..7fbb7a7bd9b 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -42,6 +42,11 @@ class select_pointer_typet &generic_parameter_specialization_map, const namespacet &ns) const; + virtual optionalt> get_parameter_alternative_types( + const irep_idt &function_name, + const irep_idt ¶meter_name, + const namespacet &ns) const; + pointer_typet specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt From 6e96333e7a3b281a7364bc64cda919ec41aa1ccf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 14 Aug 2018 15:53:41 +0200 Subject: [PATCH 3/5] Change from optional set to simply set --- jbmc/src/java_bytecode/java_entry_point.cpp | 5 ++--- jbmc/src/java_bytecode/select_pointer_type.cpp | 3 +-- jbmc/src/java_bytecode/select_pointer_type.h | 2 +- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 859b707bef6..fa7d4f48b4b 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -327,7 +327,7 @@ exprt::operandst java_build_arguments( const auto alternatives = pointer_type_selector.get_parameter_alternative_types( function.name, p.get_identifier(), ns); - if(!alternatives.has_value()) + if(alternatives.empty()) { main_arguments[param_number] = object_factory( p.type(), @@ -344,7 +344,6 @@ exprt::operandst java_build_arguments( INVARIANT(!is_this, "We cannot have different types for `this` here"); // create a non-deterministic switch between all possible values for the // type of the parameter. - const auto alternative_object_types = alternatives.value(); code_switcht code_switch; // the idea is to get a new symbol for the parameter value `tmp` @@ -374,7 +373,7 @@ exprt::operandst java_build_arguments( std::vector cases; size_t alternative = 0; - for(const auto &type : alternative_object_types) + for(const auto &type : alternatives) { code_blockt init_code_for_type; exprt init_expr_for_parameter = object_factory( diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index ee548c03bec..5d6731b7c00 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -224,8 +224,7 @@ select_pointer_typet::get_recursively_instantiated_type( return inst_val; } -optionalt> -select_pointer_typet::get_parameter_alternative_types( +std::set select_pointer_typet::get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 7fbb7a7bd9b..482c8fdbbd0 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -42,7 +42,7 @@ class select_pointer_typet &generic_parameter_specialization_map, const namespacet &ns) const; - virtual optionalt> get_parameter_alternative_types( + virtual std::set get_parameter_alternative_types( const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const; From f623c0bd5bf35d6c7b9080cf83f40e91fac0d2c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 14 Aug 2018 18:20:55 +0200 Subject: [PATCH 4/5] Simplify code for alternative parameter types --- jbmc/src/java_bytecode/java_entry_point.cpp | 22 ++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fa7d4f48b4b..e2445570ee5 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -364,34 +364,38 @@ exprt::operandst java_build_arguments( const symbolt result_symbol = get_fresh_aux_symbol( p.type(), - "nondet_parameter_" + std::to_string(param_number), + id2string(function.name), "nondet_parameter_" + std::to_string(param_number), function.location, ID_java, symbol_table); main_arguments[param_number] = result_symbol.symbol_expr(); - std::vector cases; - size_t alternative = 0; - for(const auto &type : alternatives) - { + std::vector cases(alternatives.size()); + const auto initialize_parameter = [&](const symbol_typet &type) { code_blockt init_code_for_type; exprt init_expr_for_parameter = object_factory( java_reference_type(type), - id2string(base_name) + "_alt_" + std::to_string(alternative), + id2string(base_name) + "_alternative_" + + id2string(type.get_identifier()), init_code_for_type, symbol_table, parameters, allocation_typet::DYNAMIC, function.location, pointer_type_selector); - alternative++; init_code_for_type.add( code_assignt( result_symbol.symbol_expr(), typecast_exprt(init_expr_for_parameter, p.type()))); - cases.push_back(init_code_for_type); - } + return init_code_for_type; + }; + + std::transform( + alternatives.begin(), + alternatives.end(), + cases.begin(), + initialize_parameter); init_code.add( generate_nondet_switch( From 4ed36c6e9f1f978ab5fdb819b5b0319c2a893741 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 22 Aug 2018 14:43:55 +0200 Subject: [PATCH 5/5] Fix naming in variables for non-deterministic values --- jbmc/src/java_bytecode/java_entry_point.cpp | 2 +- jbmc/src/java_bytecode/nondet.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index e2445570ee5..85fb83e0a6c 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -399,7 +399,7 @@ exprt::operandst java_build_arguments( init_code.add( generate_nondet_switch( - id2string(function.base_name) + "_" + std::to_string(param_number), + id2string(function.name) + "_" + std::to_string(param_number), cases, java_int_type(), function.location, diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp index 406b2f77201..35fca8ff27f 100644 --- a/jbmc/src/java_bytecode/nondet.cpp +++ b/jbmc/src/java_bytecode/nondet.cpp @@ -46,7 +46,7 @@ symbol_exprt generate_nondet_int( // Declare a symbol for the non deterministic integer. const symbol_exprt &nondet_symbol = get_fresh_aux_symbol( int_type, - name_prefix + "::nondet_int", + name_prefix, "nondet_int", source_location, ID_java,