Try 3

Owen Jones · Owen · commit 1b7cfe99bb53 · 2018-07-07T08:42:57.000+01:00
Restructure code to be easier to understand, and fix some correctness
issues
diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -43,46 +43,44 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
   const irep_idt &mode)
 {
   const auto next_instr = std::next(target);
-  bool changed = false;
 
   // We only expect to find nondets in the rhs of an assignments or in return
   // statements
   for(exprt &op : target->code.operands())
   {
-    if(op.id() != ID_side_effect)
+    if(!can_cast_expr<side_effect_expr_nondett>(op))
     {
       continue;
     }
 
-    const auto &side_effect = to_side_effect_expr(op);
-    if(side_effect.get_statement() != ID_nondet)
-    {
-      continue;
-    }
+    const auto &nondet_expr = to_side_effect_expr_nondet(op);
 
-    const typet &type = side_effect.type();
     // If the lhs type doesn't have a subtype then I guess it's primitive and
-    // we want to bail out now
-    if(type.id() != ID_pointer)
-    {
-      continue;
-    }
-
-    // Although, if the type is a ptr-to-void or a function pointer then we also
-    // want to bail
-    if(type.subtype().id() == ID_empty || type.subtype().id() == ID_code)
+    // 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;
     }
 
-    if(!to_side_effect_expr_nondet(side_effect).get_nullable())
+    if(!nondet_expr.get_nullable())
       object_factory_parameters.max_nonnull_tree_depth = 1;
 
-    // Get the symbol to nondet-init
     const auto source_loc = target->source_location;
 
-    // Create symbol for storing nondet object. We will replace `op` with this
-    // symbol.
+    // Currently the code looks like this
+    //   target: original instruction
+    // 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
+    //            dead aux_symbol
+
     symbolt &aux_symbol = get_fresh_aux_symbol(
       type,
       id2string(goto_programt::get_function_id(goto_program)),
@@ -93,54 +91,54 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     aux_symbol.is_static_lifetime = false;
 
     const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
-    code_declt decl(aux_symbol_expr);
-    decl.add_source_location() = source_loc;
+    op = aux_symbol_expr;
 
-    // Create goto instructions for declaring and deading aux_symbol
-    goto_programt aux_instructions;
-    code_blockt aux_block;
-    aux_block.move(decl);
-    goto_convert(
-      aux_block, symbol_table, aux_instructions, message_handler, mode);
-    CHECK_RETURN(aux_instructions.instructions.size() == 2);
+    // 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);
+    decl_aux_symbol.source_location = source_loc;
+    goto_program.insert_before_swap(target, decl_aux_symbol);
 
-    code_blockt init_code;
+    // Keep track of the new location of the original instruction.
+    const goto_programt::targett target2 = std::next(target);
 
+    code_blockt gen_nondet_init_code;
     const bool skip_classid = true;
     gen_nondet_init(
       aux_symbol_expr,
-      init_code,
+      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 nondet_init_instructions;
+    goto_programt gen_nondet_init_instructions;
     goto_convert(
-      init_code, symbol_table, nondet_init_instructions, message_handler, mode);
-
-    // First insert the declaration of aux_symbol at the front of
-    // nondet_init_instructions
-    nondet_init_instructions.insert_before_swap(
-      nondet_init_instructions.instructions.begin(),
-      aux_instructions.instructions.front());
-
-    // Insert nondet_init_instructions into the instruction list before target
-    goto_program.destructive_insert(target, nondet_init_instructions);
-
-    // Replace op with aux symbol in target
-    op = aux_symbol_expr;
+      gen_nondet_init_code,
+      symbol_table,
+      gen_nondet_init_instructions,
+      message_handler,
+      mode);
 
-    // Finally insert the dead instruction for aux_symbol after target
-    goto_program.insert_after(target)->swap(
-      aux_instructions.instructions.back());
+    goto_program.destructive_insert(target2, gen_nondet_init_instructions);
 
-    changed = true;
+    // 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, changed);
+  return std::make_pair(next_instr, false);
 }
 
 /// For each instruction in the goto program, checks if it is an assignment from
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -124,7 +124,8 @@ 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,
