Make convert_java_nondet more general

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -22,90 +22,141 @@ Author: Reuben Thomas, [email protected]
 
 #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<side_effect_expr_nondett>(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.
 /// \param goto_program: The goto program to modify.
 /// \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<goto_programt::targett, bool> insert_nondet_init_code(
   goto_programt &goto_program,
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   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
+    //      .     <gen_nondet_init_instructions - many lines>
+    //      .     <gen_nondet_init_instructions - many lines>
+    //      .     <gen_nondet_init_instructions - many lines>
+    //   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,25 +165,35 @@ 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,
   message_handlert &message_handler,
   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();
   }
 }
 

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -15,6 +15,8 @@
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
 
+#include <java_bytecode/convert_java_nondet.h>
+#include <java_bytecode/object_factory_parameters.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/replace_java_nondet.h>
 
@@ -26,7 +28,7 @@
 #include <iostream>
 #include <java-testing-utils/load_java_class.h>
 
-void validate_method_removal(
+void validate_nondet_method_removed(
   std::list<goto_programt::instructiont> 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<goto_programt::instructiont> instructions)
+{
+  bool nondet_exists = false;
+  bool allocate_exists = false;
+  for(const auto &inst : instructions)
+  {
+    // Check that our NONDET(<type>) 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<side_effect_exprt>(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);
   }
 }