Fix for nondet replacement on a direct return (pre-remove returns)

If remove returns hasn't been run and the nondet method call was a direct return - return nondetWithoutNull() - an assertion was hit because it couldn't find the destination assignment to add the nondet value too. This change just adds that particular situation in, saying if we can't find an assignment it's likely to be a return and then attempts to look for that.

The logic is also very slightly modified to replace the code of the target instruction instead of destroying it, creating a new one and inserting that directly afterwards.

Author: JohnDumbell

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 = (<type-of-obj>)return_tmp0;
 ///
 /// We're going to replace all of these lines with
-///   return_tmp0 = NONDET(<type-of-obj>)
+///   obj = NONDET(<type-of-obj>)
+///
+/// In the situation of a direct return, the end result should be:
+///   return NONDET(<type-of-obj>)
 /// \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,60 @@ 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);
+  }
+  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);
+  }
 
   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

jbmc/unit/java_bytecode/java_replace_nondet/Main.class

@@ -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;
+    }
+}

jbmc/unit/java_bytecode/java_replace_nondet/Main.java

@@ -8,7 +8,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <java-testing-utils/load_java_class.h>
+#include <testing-utils/load_java_class.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -29,9 +29,12 @@ void validate_method_removal(
 {
   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(<type>) exists on a rhs somewhere.
     if(inst.is_assign())
     {
       const code_assignt &assignment = to_code_assign(inst.code);
@@ -45,6 +48,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 =
@@ -70,57 +88,151 @@ 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);
+
+  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.
     null_message_handlert null_output;
     goto_functionst functions;
     goto_convert(symbol_table, functions, null_output);
 
-    const std::string function_name = "java::Main.replaceNondet:()V";
-    goto_functionst::goto_functiont &goto_function =
-      functions.function_map.at(function_name);
+    WHEN("A method assigns a local Object variable with nondetWithoutNull.")
+    {
+      load_and_test_method(
+        "replaceNondetAssignment:()V", functions, symbol_table);
+    }
 
-    goto_model_functiont model_function(
-      symbol_table, functions, function_name, goto_function);
+    // Currently causes an abort, needs to be re-enabled when logic is fixed.
 
-    remove_instanceof(goto_function, symbol_table);
+    //    WHEN(
+    //      "A method assigns an int variable with nondetWithoutNull. Causes "
+    //      "unboxing.")
+    //    {
+    //      load_and_test_method("replaceNondetAssignmentUnbox:()V", functions, symbol_table);
+    //    }
 
-    remove_virtual_functions(model_function);
+    WHEN(
+      "A method assigns an Integer variable with nondetWithoutNull. Causes "
+      "implicit cast.")
+    {
+      load_and_test_method(
+        "replaceNondetAssignmentImplicitCast:()V", functions, symbol_table);
+    }
 
-    WHEN("Remove returns is called before java nondet.")
+    WHEN(
+      "A method assigns an Integer variable with nondetWithoutNull. Uses "
+      "explicit cast.")
     {
-      remove_returns(model_function, [](const irep_idt &) { return false; });
+      load_and_test_method(
+        "replaceNondetAssignmentExplicitCast:()V", functions, symbol_table);
+    }
 
-      replace_java_nondet(functions);
+    // Currently causes an abort, needs to be re-enabled when logic is fixed.
 
-      THEN("The nondet method call should have been removed.")
-      {
-        validate_method_removal(goto_function.body.instructions);
-      }
-    }
+    //    WHEN(
+    //      "A method assigns an int variable with nondetWithoutNull +3 with explicit cast.")
+    //    {
+    //      load_and_test_method("replaceNondetAssignmentAddition:()V", functions, symbol_table);
+    //    }
 
-    WHEN("Remove returns is called after java nondet.")
+    //    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);
+    //    }
+
+    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);
     }
+
+    // Currently causes an abort, needs to be re-enabled when logic is fixed.
+
+    //    WHEN(
+    //      "A method directly returns a nonDetWithoutNull +3 with explicit int cast.")
+    //    {
+    //      load_and_test_method("replaceNondetReturnAddition:()Ljava/lang/Integer;", functions, symbol_table);
+    //    }
   }
-}
+}