Merge pull request #2263 from JohnDumbell/bugfix/nondet_direct_return

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

Author: smowton

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,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

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

@@ -24,15 +24,19 @@
 #include <goto-instrument/cover.h>
 
 #include <iostream>
+#include <java-testing-utils/load_java_class.h>
 
 void validate_method_removal(
   std::list<goto_programt::instructiont> 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(<type>) 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);
+    //    }
   }
-}
+}