Try 4

Respond to review comments

Author: Owen Jones

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -22,6 +22,45 @@ Author: Reuben Thomas, [email protected]
 
 #include "java_object_factory.h" // gen_nondet_init
 
+/// Return whether `expr` is a nondet pointer that we should convert
+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;
+}
+
+static void get_gen_nondet_init_instructions(
+  goto_programt &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_convert(
+    gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
+}
+
 /// 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.
@@ -44,94 +83,70 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
 {
   const auto next_instr = std::next(target);
 
-  // We only expect to find nondets in the rhs of an assignments or in return
-  // statements
+  // 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())
   {
-    if(!can_cast_expr<side_effect_expr_nondett>(op))
+    if(!is_nondet_pointer(op))
     {
       continue;
     }
 
-    const auto &nondet_expr = to_side_effect_expr_nondet(op);
-
-    // If the lhs type doesn't have a subtype then I guess it's primitive and
-    // we want to bail out now. If the type is a ptr-to-void or a function
-    // pointer then we also want to bail.
-    const typet &type = nondet_expr.type();
-    if(
-      type.id() != ID_pointer || type.subtype().id() == ID_empty ||
-      type.subtype().id() == ID_code)
-    {
-      continue;
-    }
+   const auto &nondet_expr = to_side_effect_expr_nondet(op);
 
     if(!nondet_expr.get_nullable())
       object_factory_parameters.max_nonnull_tree_depth = 1;
 
-    const auto source_loc = target->source_location;
+    const source_locationt &source_loc = target->source_location;
 
     // Currently the code looks like this
-    //   target: original instruction
+    //   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: orig instruction with op replaced by aux_symbol
+    //   target2: instruction containing op, with op replaced by aux_symbol
     //            dead aux_symbol
 
     symbolt &aux_symbol = get_fresh_aux_symbol(
-      type,
+      op.type(),
       id2string(goto_programt::get_function_id(goto_program)),
       "nondet_tmp",
       source_loc,
       ID_java,
       symbol_table);
-    aux_symbol.is_static_lifetime = false;
 
     const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
     op = aux_symbol_expr;
 
-    // It is simplest to insert the final instruction first, before everything
-    // gets moved around
-    goto_programt::targett dead_aux_symbol = goto_program.insert_after(target);
-    dead_aux_symbol->type = DEAD;
-    dead_aux_symbol->code = code_deadt(aux_symbol_expr);
-    dead_aux_symbol->source_location = source_loc;
-
     // Insert an instruction declaring `aux_symbol` before `target`, being
     // careful to preserve jumps to `target`
-    goto_programt::instructiont decl_aux_symbol(DECL);
-    decl_aux_symbol.code = code_declt(aux_symbol_expr);
+    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);
 
-    // Keep track of the new location of the original instruction.
+    // Keep track of the new location of the instruction containing op.
     const goto_programt::targett target2 = std::next(target);
 
-    code_blockt gen_nondet_init_code;
-    const bool skip_classid = true;
-    gen_nondet_init(
+    goto_programt gen_nondet_init_instructions;
+    get_gen_nondet_init_instructions(
+      gen_nondet_init_instructions,
       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 gen_nondet_init_instructions;
-    goto_convert(
-      gen_nondet_init_code,
       symbol_table,
-      gen_nondet_init_instructions,
       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
@@ -159,9 +174,8 @@ void convert_nondet(
 {
   bool changed = false;
   auto instruction_iterator = goto_program.instructions.begin();
-  auto end = goto_program.instructions.end();
 
-  while(instruction_iterator != end)
+  while(instruction_iterator != goto_program.instructions.end())
   {
     auto ret = insert_nondet_init_code(
       goto_program,

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -106,15 +106,16 @@ void validate_nondets_converted(
          : inst.is_return() ? to_code_return(inst.code).return_value()
                             : inst.code);
 
-    if(target_expression.id() == ID_side_effect)
+    if(
+      const auto side_effect =
+        expr_try_dynamic_cast<side_effect_exprt>(target_expression))
     {
-      auto side_effect = to_side_effect_expr(target_expression);
-      if(side_effect.get_statement() == ID_nondet)
+      if(side_effect->get_statement() == ID_nondet)
       {
         nondet_exists = true;
       }
 
-      if(side_effect.get_statement() == ID_allocate)
+      if(side_effect->get_statement() == ID_allocate)
       {
         allocate_exists = true;
       }
@@ -124,8 +125,7 @@ void validate_nondets_converted(
   REQUIRE_FALSE(nondet_exists);
   REQUIRE(allocate_exists);
 }
-#include<iostream>
-#include<cout_message.h>
+
 void load_and_test_method(
   const std::string &method_signature,
   goto_functionst &functions,