From 6d9e80547402093f4469ef181b6e8075c41c8340 Mon Sep 17 00:00:00 2001 From: Owen Date: Mon, 2 Jul 2018 16:32:07 +0100 Subject: [PATCH] Make convert_java_nondet more general --- .../src/java_bytecode/convert_java_nondet.cpp | 189 ++++++++++++------ .../java_replace_nondet/replace_nondet.cpp | 74 ++++++- 2 files changed, 192 insertions(+), 71 deletions(-) diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp index acc3d9bff51..5cc4ebc4ee0 100644 --- a/jbmc/src/java_bytecode/convert_java_nondet.cpp +++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp @@ -22,6 +22,49 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include "java_object_factory.h" // gen_nondet_init +/// Returns true if `expr` is a nondet pointer that isn't a function pointer or +/// a void* pointer as these can be meaningfully non-det initalized. +static bool is_nondet_pointer(exprt expr) +{ + // If the expression type doesn't have a subtype then I guess it's primitive + // and we do not want to convert it. If the type is a ptr-to-void or a + // function pointer then we also do not want to convert it. + const typet &type = expr.type(); + const bool non_void_non_function_pointer = type.id() == ID_pointer && + type.subtype().id() != ID_empty && + type.subtype().id() != ID_code; + return can_cast_expr(expr) && + non_void_non_function_pointer; +} + +/// Populate `instructions` with goto instructions to nondet init +/// `aux_symbol_expr` +static goto_programt get_gen_nondet_init_instructions( + const symbol_exprt &aux_symbol_expr, + const source_locationt &source_loc, + symbol_table_baset &symbol_table, + message_handlert &message_handler, + const object_factory_parameterst &object_factory_parameters, + const irep_idt &mode) +{ + code_blockt gen_nondet_init_code; + const bool skip_classid = true; + gen_nondet_init( + aux_symbol_expr, + gen_nondet_init_code, + symbol_table, + source_loc, + skip_classid, + allocation_typet::DYNAMIC, + object_factory_parameters, + update_in_placet::NO_UPDATE_IN_PLACE); + + goto_programt instructions; + goto_convert( + gen_nondet_init_code, symbol_table, instructions, message_handler, mode); + return instructions; +} + /// Checks an instruction to see whether it contains an assignment from /// side_effect_expr_nondet. If so, replaces the instruction with a range of /// instructions to properly nondet-initialize the lhs. @@ -29,9 +72,12 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com /// \param target: One of the steps in that goto program. /// \param symbol_table: The global symbol table. /// \param message_handler: Handles logging. -/// \param max_nondet_array_length: Maximum size of new nondet arrays. -/// \return The next instruction to process with this function. -static goto_programt::targett insert_nondet_init_code( +/// \param object_factory_parameters: Parameters for the generation of nondet +/// objects. +/// \param mode: Language mode +/// \return The next instruction to process with this function and a boolean +/// indicating whether any changes were made to the goto program. +static std::pair insert_nondet_init_code( goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, @@ -39,73 +85,78 @@ static goto_programt::targett insert_nondet_init_code( object_factory_parameterst object_factory_parameters, const irep_idt &mode) { - // Return if the instruction isn't an assignment - const auto next_instr=std::next(target); - if(!target->is_assign()) - { - return next_instr; - } + const auto next_instr = std::next(target); - // Return if the rhs of the assignment isn't a side effect expression - const auto &assign=to_code_assign(target->code); - if(assign.rhs().id()!=ID_side_effect) + // We only expect to find nondets in the rhs of an assignments, and in return + // statements if remove_returns has not been run, but we do a more general + // check on all operands in case this changes + for(exprt &op : target->code.operands()) { - return next_instr; - } + if(!is_nondet_pointer(op)) + { + continue; + } - // Return if the rhs isn't nondet - const auto &side_effect=to_side_effect_expr(assign.rhs()); - if(side_effect.get_statement()!=ID_nondet) - { - return next_instr; - } + const auto &nondet_expr = to_side_effect_expr_nondet(op); - const auto lhs=assign.lhs(); - // If the lhs type doesn't have a subtype then I guess it's primitive and - // we want to bail out now - if(!lhs.type().has_subtype()) - { - return next_instr; - } + if(!nondet_expr.get_nullable()) + object_factory_parameters.max_nonnull_tree_depth = 1; - // Although, if the type is a ptr-to-void then we also want to bail - if(lhs.type().subtype().id()==ID_empty || - lhs.type().subtype().id()==ID_code) - { - return next_instr; - } + const source_locationt &source_loc = target->source_location; - // Check whether the nondet object may be null - if(!to_side_effect_expr_nondet(side_effect).get_nullable()) - object_factory_parameters.max_nonnull_tree_depth = 1; - // Get the symbol to nondet-init - const auto source_loc=target->source_location; + // Currently the code looks like this + // target: instruction containing op + // When we are done it will look like this + // target : declare aux_symbol + // . + // . + // . + // target2: instruction containing op, with op replaced by aux_symbol + // dead aux_symbol - // Erase the nondet assignment - target->make_skip(); + symbolt &aux_symbol = get_fresh_aux_symbol( + op.type(), + id2string(goto_programt::get_function_id(goto_program)), + "nondet_tmp", + source_loc, + ID_java, + symbol_table); - // Generate nondet init code - code_blockt init_code; - gen_nondet_init( - lhs, - init_code, - symbol_table, - source_loc, - true, - allocation_typet::DYNAMIC, - object_factory_parameters, - update_in_placet::NO_UPDATE_IN_PLACE); + const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr(); + op = aux_symbol_expr; - // Convert this code into goto instructions - goto_programt new_instructions; - goto_convert( - init_code, symbol_table, new_instructions, message_handler, mode); + // Insert an instruction declaring `aux_symbol` before `target`, being + // careful to preserve jumps to `target` + goto_programt::instructiont decl_aux_symbol; + decl_aux_symbol.make_decl(code_declt(aux_symbol_expr)); + decl_aux_symbol.source_location = source_loc; + goto_program.insert_before_swap(target, decl_aux_symbol); - // Insert the new instructions into the instruction list - goto_program.destructive_insert(next_instr, new_instructions); - goto_program.update(); + // Keep track of the new location of the instruction containing op. + const goto_programt::targett target2 = std::next(target); - return next_instr; + goto_programt gen_nondet_init_instructions = + get_gen_nondet_init_instructions( + aux_symbol_expr, + source_loc, + symbol_table, + message_handler, + object_factory_parameters, + mode); + goto_program.destructive_insert(target2, gen_nondet_init_instructions); + + goto_programt::targett dead_aux_symbol = goto_program.insert_after(target2); + dead_aux_symbol->make_dead(); + dead_aux_symbol->code = code_deadt(aux_symbol_expr); + dead_aux_symbol->source_location = source_loc; + + // In theory target could have more than one operand which should be + // replaced by convert_nondet, so we return target2 so that it + // will be checked again + return std::make_pair(target2, true); + } + + return std::make_pair(next_instr, false); } /// For each instruction in the goto program, checks if it is an assignment from @@ -114,7 +165,9 @@ static goto_programt::targett insert_nondet_init_code( /// \param goto_program: The goto program to modify. /// \param symbol_table: The global symbol table. /// \param message_handler: Handles logging. -/// \param max_nondet_array_length: Maximum size of new nondet arrays. +/// \param object_factory_parameters: Parameters for the generation of nondet +/// objects. +/// \param mode: Language mode void convert_nondet( goto_programt &goto_program, symbol_table_baset &symbol_table, @@ -122,17 +175,25 @@ void convert_nondet( const object_factory_parameterst &object_factory_parameters, const irep_idt &mode) { - for(auto instruction_iterator=goto_program.instructions.begin(), - end=goto_program.instructions.end(); - instruction_iterator!=end;) + bool changed = false; + auto instruction_iterator = goto_program.instructions.begin(); + + while(instruction_iterator != goto_program.instructions.end()) { - instruction_iterator = insert_nondet_init_code( + auto ret = insert_nondet_init_code( goto_program, instruction_iterator, symbol_table, message_handler, object_factory_parameters, mode); + instruction_iterator = ret.first; + changed |= ret.second; + } + + if(changed) + { + goto_program.update(); } } diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index 777dc8160cc..b5490499e3d 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -15,6 +15,8 @@ #include #include +#include +#include #include #include @@ -26,7 +28,7 @@ #include #include -void validate_method_removal( +void validate_nondet_method_removed( std::list instructions) { bool method_removed = true, replacement_nondet_exists = false; @@ -90,6 +92,40 @@ void validate_method_removal( REQUIRE(replacement_nondet_exists); } +void validate_nondets_converted( + std::list instructions) +{ + bool nondet_exists = false; + bool allocate_exists = false; + for(const auto &inst : instructions) + { + // Check that our NONDET() exists on a rhs somewhere. + exprt target_expression = + (inst.is_assign() + ? to_code_assign(inst.code).rhs() + : inst.is_return() ? to_code_return(inst.code).return_value() + : inst.code); + + if( + const auto side_effect = + expr_try_dynamic_cast(target_expression)) + { + if(side_effect->get_statement() == ID_nondet) + { + nondet_exists = true; + } + + if(side_effect->get_statement() == ID_allocate) + { + allocate_exists = true; + } + } + } + + REQUIRE_FALSE(nondet_exists); + REQUIRE(allocate_exists); +} + void load_and_test_method( const std::string &method_signature, goto_functionst &functions, @@ -110,26 +146,50 @@ void load_and_test_method( remove_virtual_functions(model_function); // Then test both situations. + THEN("Replace nondet should work after remove returns has been called.") + { + remove_returns(model_function, [](const irep_idt &) { return false; }); + + replace_java_nondet(model_function); + + validate_nondet_method_removed(goto_function.body.instructions); + } + + THEN("Replace nondet should work before remove returns has been called.") + { + replace_java_nondet(model_function); + + remove_returns(model_function, [](const irep_idt &) { return false; }); + + validate_nondet_method_removed(goto_function.body.instructions); + } + + object_factory_parameterst params{}; + THEN( - "Code should work when remove returns is called before " - "replace_java_nondet.") + "Replace and convert nondet should work after remove returns has been " + "called.") { remove_returns(model_function, [](const irep_idt &) { return false; }); replace_java_nondet(model_function); - validate_method_removal(goto_function.body.instructions); + convert_nondet(model_function, null_message_handler, params, ID_java); + + validate_nondets_converted(goto_function.body.instructions); } THEN( - "Code should work when remove returns is called after " - "replace_java_nondet.") + "Replace and convert nondet should work before remove returns has been " + "called.") { replace_java_nondet(model_function); + convert_nondet(model_function, null_message_handler, params, ID_java); + remove_returns(model_function, [](const irep_idt &) { return false; }); - validate_method_removal(goto_function.body.instructions); + validate_nondets_converted(goto_function.body.instructions); } }