diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index 01ae988493e..c02ae91bdd8 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -152,6 +152,25 @@ static bool is_assignment_from( is_typecast_with_id(rhs, identifier); } +/// Return whether the instruction is a return, and the rhs is a symbol or +/// typecast expression with the specified identifier. +/// \param instr: A goto program instruction. +/// \param identifier: Some identifier. +/// \return True if the expression is a typecast with one operand, and the +/// typecast's identifier matches the specified identifier. +static bool is_return_with_variable( + const goto_programt::instructiont &instr, + const irep_idt &identifier) +{ + if(!instr.is_return()) + { + return false; + } + const auto &rhs = to_code_return(instr.code).return_value(); + return is_symbol_with_id(rhs, identifier) || + is_typecast_with_id(rhs, identifier); +} + /// Given an iterator into a list of instructions, modify the list to replace /// 'nondet' library functions with CBMC-native nondet expressions, and return /// an iterator to the next instruction to check. It's important to note that @@ -166,7 +185,10 @@ static bool is_assignment_from( /// obj = ()return_tmp0; /// /// We're going to replace all of these lines with -/// return_tmp0 = NONDET() +/// obj = NONDET() +/// +/// In the situation of a direct return, the end result should be: +/// return NONDET() /// \param goto_program: The goto program to modify. /// \param target: A single step of the goto program which may be erased and /// replaced. @@ -225,47 +247,64 @@ static goto_programt::targett check_and_replace_target( // Look for the assignment of the temporary return variable into our target // variable. const auto end = goto_program.instructions.end(); - auto assignment_instruction = std::find_if( + auto target_instruction = std::find_if( next_instr, end, [&return_identifier](const goto_programt::instructiont &instr) { return is_assignment_from(instr, return_identifier); }); - INVARIANT( - assignment_instruction != end, - "failed to find assignment of the temporary return variable into our " - "target variable"); - - // Assume that the LHS of *this* assignment is the actual nondet variable - const auto &code_assign = to_code_assign(assignment_instruction->code); - const auto nondet_var = code_assign.lhs(); - const auto source_loc = target->source_location; + // If we can't find an assign, it might be a direct return. + if(target_instruction == end) + { + target_instruction = std::find_if( + next_instr, + end, + [&return_identifier](const goto_programt::instructiont &instr) { + return is_return_with_variable(instr, return_identifier); + }); + } - // Erase from the nondet function call to the assignment - const auto after_matching_assignment = std::next(assignment_instruction); INVARIANT( - after_matching_assignment != end, - "goto_program missing END_FUNCTION instruction"); + target_instruction != end, + "failed to find return of the temporary return variable or assignment of " + "the temporary return variable into a target variable"); std::for_each( - target, after_matching_assignment, [](goto_programt::instructiont &instr) { + target, target_instruction, [](goto_programt::instructiont &instr) { instr.make_skip(); }); - const auto inserted = goto_program.insert_before(after_matching_assignment); - inserted->make_assignment(); - side_effect_expr_nondett inserted_expr(nondet_var.type()); - inserted_expr.set_nullable( - instr_info.get_nullable_type() == - nondet_instruction_infot::is_nullablet::TRUE); - inserted->code = code_assignt(nondet_var, inserted_expr); - inserted->code.add_source_location() = source_loc; - inserted->source_location = source_loc; + if(target_instruction->is_return()) + { + const auto &nondet_var = + to_code_return(target_instruction->code).return_value(); + + side_effect_expr_nondett inserted_expr(nondet_var.type()); + inserted_expr.set_nullable( + instr_info.get_nullable_type() == + nondet_instruction_infot::is_nullablet::TRUE); + target_instruction->code = code_returnt(inserted_expr); + target_instruction->code.add_source_location() = + target_instruction->source_location; + } + else if(target_instruction->is_assign()) + { + // Assume that the LHS of *this* assignment is the actual nondet variable + const auto &nondet_var = to_code_assign(target_instruction->code).lhs(); + + side_effect_expr_nondett inserted_expr(nondet_var.type()); + inserted_expr.set_nullable( + instr_info.get_nullable_type() == + nondet_instruction_infot::is_nullablet::TRUE); + target_instruction->code = code_assignt(nondet_var, inserted_expr); + target_instruction->code.add_source_location() = + target_instruction->source_location; + } goto_program.update(); - return after_matching_assignment; + return std::next(target_instruction); } /// Checks each instruction in the goto program to see whether it is a method diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/Main.class b/jbmc/unit/java_bytecode/java_replace_nondet/Main.class index 068fdf03f68..ebb90572885 100644 Binary files a/jbmc/unit/java_bytecode/java_replace_nondet/Main.class and b/jbmc/unit/java_bytecode/java_replace_nondet/Main.class differ diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/Main.java b/jbmc/unit/java_bytecode/java_replace_nondet/Main.java new file mode 100644 index 00000000000..d7dff2e8e84 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_replace_nondet/Main.java @@ -0,0 +1,45 @@ +public class Main { + public void replaceNondetAssignment() { + Object temp = org.cprover.CProver.nondetWithoutNull(); + } + + public void replaceNondetAssignmentUnbox() { + int temp = org.cprover.CProver.nondetWithoutNull(); + } + + public void replaceNondetAssignmentImplicitCast() { + Integer temp = org.cprover.CProver.nondetWithoutNull(); + } + + public void replaceNondetAssignmentExplicitCast() { + Integer temp = (Integer)org.cprover.CProver.nondetWithoutNull(); + } + + public void replaceNondetAssignmentAddition() { + int temp = ((int)org.cprover.CProver.nondetWithoutNull()) + 3; + } + + public void replaceNondetUnused() { + org.cprover.CProver.nondetWithoutNull(); + } + + public int replaceNondetReturnUnboxed() { + return org.cprover.CProver.nondetWithoutNull(); + } + + public Object replaceNondetReturn() { + return org.cprover.CProver.nondetWithoutNull(); + } + + public Integer replaceNondetReturnWithImplicitCast() { + return org.cprover.CProver.nondetWithoutNull(); + } + + public Integer replaceNondetReturnWithExplicitCast() { + return (Integer)org.cprover.CProver.nondetWithoutNull(); + } + + public Integer replaceNondetReturnAddition() { + return ((int)org.cprover.CProver.nondetWithoutNull()) + 3; + } +} 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 5249bacba73..777dc8160cc 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -24,15 +24,19 @@ #include #include +#include void validate_method_removal( std::list instructions) { bool method_removed = true, replacement_nondet_exists = false; - // Quick loop to check that our method call has been replaced. + // Loop over our instructions to make sure the nondet java method call has + // been removed and that we can find an assignment/return with a nondet + // as it's right-hand side. for(const auto &inst : instructions) { + // Check that our NONDET() exists on a rhs somewhere. if(inst.is_assign()) { const code_assignt &assignment = to_code_assign(inst.code); @@ -46,6 +50,21 @@ void validate_method_removal( } } + if(inst.is_return()) + { + const code_returnt &ret_expr = to_code_return(inst.code); + if(ret_expr.return_value().id() == ID_side_effect) + { + const side_effect_exprt &see = + to_side_effect_expr(ret_expr.return_value()); + if(see.get_statement() == ID_nondet) + { + replacement_nondet_exists = true; + } + } + } + + // And check to see that our nondet method call has been removed. if(inst.is_function_call()) { const code_function_callt &function_call = @@ -71,56 +90,146 @@ void validate_method_removal( REQUIRE(replacement_nondet_exists); } -TEST_CASE( - "Load class with a generated java nondet method call, run remove returns " - "both before and after the nondet statements have been removed, check " - "results are as expected.", +void load_and_test_method( + const std::string &method_signature, + goto_functionst &functions, + journalling_symbol_tablet &symbol_table) +{ + // Find the method under test. + const std::string function_name = "java::Main." + method_signature; + goto_functionst::goto_functiont &goto_function = + functions.function_map.at(function_name); + + goto_model_functiont model_function( + symbol_table, functions, function_name, goto_function); + + // Emulate some of the passes that we'd normally do before replace_java_nondet + // is called. + remove_instanceof(goto_function, symbol_table, null_message_handler); + + remove_virtual_functions(model_function); + + // Then test both situations. + THEN( + "Code should work when remove returns is called before " + "replace_java_nondet.") + { + remove_returns(model_function, [](const irep_idt &) { return false; }); + + replace_java_nondet(model_function); + + validate_method_removal(goto_function.body.instructions); + } + + THEN( + "Code should work when remove returns is called after " + "replace_java_nondet.") + { + replace_java_nondet(model_function); + + remove_returns(model_function, [](const irep_idt &) { return false; }); + + validate_method_removal(goto_function.body.instructions); + } +} + +SCENARIO( + "Testing replace_java_nondet correctly replaces CProver.nondet method calls.", "[core][java_bytecode][replace_nondet]") { - GIVEN("A class with a call to CProver.nondetWithoutNull()") + GIVEN("A class that holds nondet calls.") { - symbol_tablet raw_symbol_table = load_java_class( - "Main", "./java_bytecode/java_replace_nondet", "Main.replaceNondet"); + // Load our main class. + symbol_tablet raw_symbol_table = + load_java_class("Main", "./java_bytecode/java_replace_nondet"); journalling_symbol_tablet symbol_table = journalling_symbol_tablet::wrap(raw_symbol_table); + // Convert bytecode into goto. goto_functionst functions; goto_convert(symbol_table, functions, null_message_handler); - const std::string function_name = "java::Main.replaceNondet:()V"; - goto_functionst::goto_functiont &goto_function = - functions.function_map.at(function_name); - - goto_model_functiont model_function( - symbol_table, functions, function_name, goto_function); - - remove_instanceof(goto_function, symbol_table, null_message_handler); - - remove_virtual_functions(model_function); - - WHEN("Remove returns is called before java nondet.") + WHEN("A method assigns a local Object variable with nondetWithoutNull.") { - remove_returns(model_function, [](const irep_idt &) { return false; }); + load_and_test_method( + "replaceNondetAssignment:()V", functions, symbol_table); + } - replace_java_nondet(functions); + WHEN( + "A method assigns an Integer variable with nondetWithoutNull. Causes " + "implicit cast.") + { + load_and_test_method( + "replaceNondetAssignmentImplicitCast:()V", functions, symbol_table); + } - THEN("The nondet method call should have been removed.") - { - validate_method_removal(goto_function.body.instructions); - } + WHEN( + "A method assigns an Integer variable with nondetWithoutNull. Uses " + "explicit cast.") + { + load_and_test_method( + "replaceNondetAssignmentExplicitCast:()V", functions, symbol_table); } - WHEN("Remove returns is called after java nondet.") + WHEN("A method directly returns a nonDetWithoutNull of type Object.") { - replace_java_nondet(functions); + load_and_test_method( + "replaceNondetReturn:()Ljava/lang/Object;", functions, symbol_table); + } - remove_returns(model_function, [](const irep_idt &) { return false; }); + WHEN( + "A method directly returns a nonDetWithoutNull of type Integer. Causes " + "implicit cast.") + { + load_and_test_method( + "replaceNondetReturnWithImplicitCast:()Ljava/lang/Integer;", + functions, + symbol_table); + } - THEN("The nondet method call should have been removed.") - { - validate_method_removal(goto_function.body.instructions); - } + WHEN( + "A method directly returns a nonDetWithoutNull of type Integer. Uses " + "explicit cast.") + { + load_and_test_method( + "replaceNondetReturnWithExplicitCast:()Ljava/lang/Integer;", + functions, + symbol_table); } + + // These currently cause an abort, issue detailed in https://github.com/diffblue/cbmc/issues/2281. + + // WHEN( + // "A method directly returns a nonDetWithoutNull +3 with explicit int cast.") + // { + // load_and_test_method("replaceNondetReturnAddition:()Ljava/lang/Integer;", functions, symbol_table); + // } + + // WHEN( + // "A method assigns an int variable with nondetWithoutNull. Causes " + // "unboxing.") + // { + // load_and_test_method("replaceNondetAssignmentUnbox:()V", functions, symbol_table); + // } + + // WHEN( + // "A method assigns an int variable with nondetWithoutNull +3 with explicit cast.") + // { + // load_and_test_method("replaceNondetAssignmentAddition:()V", functions, symbol_table); + // } + + // WHEN( + // "A method that calls nondetWithoutNull() without assigning the return value.") + // { + // load_and_test_method("replaceNondetUnused:()V", functions, symbol_table); + // } + + // WHEN( + // "A method directly returns a nonDetWithoutNull of type int. Causes " + // "unboxing.") + // { + // load_and_test_method("replaceNondetReturnUnboxed:()I", functions, symbol_table); + // } } -} +} \ No newline at end of file diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/test.java b/jbmc/unit/java_bytecode/java_replace_nondet/test.java deleted file mode 100644 index 8a2a1a6d14b..00000000000 --- a/jbmc/unit/java_bytecode/java_replace_nondet/test.java +++ /dev/null @@ -1,5 +0,0 @@ -public class Main { - public void replaceNondet() { - Object test = org.cprover.CProver.nondetWithoutNull(); - } -}