Merge pull request #4579 from diffblue/instructiont-construction

instructiont construction

Author: tautschnig

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -124,9 +124,6 @@ SCENARIO(
   symbol_table.insert(test_program_symbol);
   namespacet ns(symbol_table);
 
-  goto_programt test_program;
-  auto virtual_call_inst = test_program.add_instruction(FUNCTION_CALL);
-
   const symbolt &callee_symbol =
     symbol_table.lookup_ref("java::VirtualFunctionsTestParent.f:()V");
 
@@ -141,9 +138,12 @@ SCENARIO(
     // null pointer:
     {null_pointer_exprt(
       to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))});
-  virtual_call_inst->code = call;
 
-  test_program.add_instruction(END_FUNCTION);
+  goto_programt test_program;
+  auto virtual_call_inst =
+    test_program.add(goto_programt::make_function_call(call));
+
+  test_program.add(goto_programt::make_end_function());
 
   WHEN("Resolving virtual callsite to a single callee")
   {

src/analyses/goto_check.cpp

@@ -1438,13 +1438,16 @@ void goto_checkt::add_guarded_claim(
     goto_program_instruction_typet type=
       enable_assert_to_assume?ASSUME:ASSERT;
 
-    goto_programt::targett t=new_code.add_instruction(type);
+    goto_programt::targett t = new_code.add(goto_programt::instructiont(
+      static_cast<const codet &>(get_nil_irep()),
+      source_location,
+      type,
+      std::move(new_expr),
+      {}));
 
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->set_condition(std::move(new_expr));
-    t->source_location=source_location;
     t->source_location.set_comment(comment+" in "+source_expr_string);
     t->source_location.set_property_class(property_class);
   }
@@ -1739,10 +1742,13 @@ void goto_checkt::goto_check(
         goto_program_instruction_typet type=
           enable_assert_to_assume?ASSUME:ASSERT;
 
-        goto_programt::targett t=new_code.add_instruction(type);
+        goto_programt::targett t = new_code.add(goto_programt::instructiont(
+          static_cast<const codet &>(get_nil_irep()),
+          i.source_location,
+          type,
+          false_exprt(),
+          {}));
 
-        t->set_condition(false_exprt());
-        t->source_location=i.source_location;
         t->source_location.set_property_class("error label");
         t->source_location.set_comment("error label "+label);
         t->source_location.set("user-provided", true);

src/goto-instrument/unwind.cpp

@@ -48,8 +48,9 @@ void goto_unwindt::copy_segment(
 
   for(goto_programt::const_targett t=start; t!=end; t++)
   {
-    goto_programt::targett t_new=goto_program.add_instruction();
-    *t_new=*t;
+    // copy the instruction
+    goto_programt::targett t_new =
+      goto_program.add(goto_programt::instructiont(*t));
     unwind_log.insert(t_new, t->location_number);
     target_vector.push_back(t_new); // store copied instruction
   }

src/goto-instrument/wmm/goto2graph.cpp

@@ -1245,9 +1245,7 @@ void inline instrumentert::add_instr_to_interleaving(
   }
 
   /* add this instruction to the interleaving */
-  goto_programt::targett current_instruction=interleaving.add_instruction();
-  goto_programt::instructiont new_instruction(*it);
-  current_instruction->swap(new_instruction);
+  interleaving.add(goto_programt::instructiont(*it));
 }
 
 bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)

src/goto-programs/goto_convert.cpp

@@ -298,9 +298,8 @@ void goto_convertt::copy(
   goto_program_instruction_typet type,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction(type);
-  t->code=code;
-  t->source_location=code.source_location();
+  dest.add(goto_programt::instructiont(
+    code, code.source_location(), type, nil_exprt(), {}));
 }
 
 void goto_convertt::convert_label(
@@ -827,9 +826,8 @@ void goto_convertt::convert_skip(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction(SKIP);
-  t->source_location=code.source_location();
-  t->code=code;
+  dest.add(goto_programt::instructiont(
+    code, code.source_location(), SKIP, nil_exprt(), {}));
 }
 
 void goto_convertt::convert_assume(
@@ -900,7 +898,7 @@ void goto_convertt::convert_for(
 
   // do the v label
   goto_programt tmp_v;
-  goto_programt::targett v=tmp_v.add_instruction();
+  goto_programt::targett v = tmp_v.add(goto_programt::instructiont());
 
   // do the z label
   goto_programt tmp_z;
@@ -990,9 +988,10 @@ void goto_convertt::convert_while(
   // do the v label
   goto_programt::targett v=tmp_branch.instructions.begin();
 
-  // do the y label
+  // y: goto v;
   goto_programt tmp_y;
-  goto_programt::targett y=tmp_y.add_instruction();
+  goto_programt::targett y = tmp_y.add(
+    goto_programt::make_goto(v, true_exprt(), code.source_location()));
 
   // set the targets
   targets.set_break(z);
@@ -1002,9 +1001,6 @@ void goto_convertt::convert_while(
   goto_programt tmp_x;
   convert(code.body(), tmp_x, mode);
 
-  // y: if(c) goto v;
-  *y = goto_programt::make_goto(v, true_exprt(), code.source_location());
-
   // loop invariant
   convert_loop_invariant(code, y, mode);
 
@@ -1047,7 +1043,8 @@ void goto_convertt::convert_dowhile(
 
   // do the y label
   goto_programt tmp_y;
-  goto_programt::targett y=tmp_y.add_instruction();
+  goto_programt::targett y =
+    tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location));
 
   // do the z label
   goto_programt tmp_z;
@@ -1071,7 +1068,7 @@ void goto_convertt::convert_dowhile(
   goto_programt::targett w=tmp_w.instructions.begin();
 
   // y: if(c) goto w;
-  *y = goto_programt::make_goto(w, cond, condition_location);
+  y->complete_goto(w);
 
   // loop invariant
   convert_loop_invariant(code, y, mode);
@@ -1315,9 +1312,8 @@ void goto_convertt::convert_gcc_computed_goto(
   goto_programt &dest)
 {
   // this instruction will turn into OTHER during post-processing
-  goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
-  t->source_location=code.source_location();
-  t->code=code;
+  goto_programt::targett t = dest.add(goto_programt::instructiont(
+    code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
 
   // remember it to do this later
   targets.computed_gotos.push_back(t);
@@ -1327,10 +1323,8 @@ void goto_convertt::convert_start_thread(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett start_thread=
-    dest.add_instruction(START_THREAD);
-  start_thread->source_location=code.source_location();
-  start_thread->code=code;
+  goto_programt::targett start_thread = dest.add(goto_programt::instructiont(
+    code, code.source_location(), START_THREAD, nil_exprt(), {}));
 
   // remember it to do target later
   targets.gotos.emplace_back(
@@ -1543,7 +1537,8 @@ void goto_convertt::generate_ifthenelse(
 
   // do the x label
   goto_programt tmp_x;
-  goto_programt::targett x=tmp_x.add_instruction();
+  goto_programt::targett x =
+    tmp_x.add(goto_programt::make_incomplete_goto(true_exprt()));
 
   // do the z label
   goto_programt tmp_z;
@@ -1571,8 +1566,8 @@ void goto_convertt::generate_ifthenelse(
 
   // x: goto z;
   CHECK_RETURN(!tmp_w.instructions.empty());
-  *x = goto_programt::make_goto(
-    z, true_exprt(), tmp_w.instructions.back().source_location);
+  x->complete_goto(z);
+  x->source_location = tmp_w.instructions.back().source_location;
 
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);
@@ -1894,13 +1889,21 @@ void goto_convertt::generate_thread_block(
   goto_programt::targett c = body.add(goto_programt::make_skip());
   convert(thread_body, body, mode);
 
-  goto_programt::targett e=postamble.add_instruction(END_THREAD);
+  goto_programt::targett e = postamble.add(goto_programt::instructiont(
+    static_cast<const codet &>(get_nil_irep()),
+    thread_body.source_location(),
+    END_THREAD,
+    nil_exprt(),
+    {}));
   e->source_location=thread_body.source_location();
   goto_programt::targett z = postamble.add(goto_programt::make_skip());
 
-  goto_programt::targett a=preamble.add_instruction(START_THREAD);
-  a->source_location=thread_body.source_location();
-  a->targets.push_back(c);
+  preamble.add(goto_programt::instructiont(
+    static_cast<const codet &>(get_nil_irep()),
+    thread_body.source_location(),
+    START_THREAD,
+    nil_exprt(),
+    {c}));
   preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
 
   dest.destructive_append(preamble);

src/goto-programs/goto_convert_function_call.cpp

@@ -112,11 +112,13 @@ void goto_convertt::do_function_call_if(
 
   // do the v label
   goto_programt tmp_v;
-  goto_programt::targett v=tmp_v.add_instruction();
+  goto_programt::targett v = tmp_v.add(goto_programt::make_incomplete_goto(
+    boolean_negate(function.cond()), function.cond().source_location()));
 
   // do the x label
   goto_programt tmp_x;
-  goto_programt::targett x=tmp_x.add_instruction();
+  goto_programt::targett x =
+    tmp_x.add(goto_programt::make_incomplete_goto(true_exprt()));
 
   // do the z label
   goto_programt tmp_z;
@@ -134,8 +136,7 @@ void goto_convertt::do_function_call_if(
     y=tmp_y.instructions.begin();
 
   // v: if(!c) goto y;
-  *v = goto_programt::make_goto(
-    y, boolean_negate(function.cond()), function.cond().source_location());
+  v->complete_goto(y);
 
   // w: f();
   goto_programt tmp_w;
@@ -146,7 +147,7 @@ void goto_convertt::do_function_call_if(
     tmp_w.add(goto_programt::make_skip());
 
   // x: goto z;
-  *x = goto_programt::make_goto(z, true_exprt());
+  x->complete_goto(z);
 
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);

src/goto-programs/goto_convert_functions.cpp

@@ -182,9 +182,8 @@ void goto_convert_functionst::convert_function(
     end_location.make_nil();
 
   goto_programt tmp_end_function;
-  goto_programt::targett end_function=tmp_end_function.add_instruction();
-  end_function->type=END_FUNCTION;
-  end_function->source_location=end_location;
+  goto_programt::targett end_function =
+    tmp_end_function.add(goto_programt::make_end_function(end_location));
 
   targets=targetst();
   targets.set_return(end_function);

src/goto-programs/goto_convert_side_effect.cpp

@@ -594,13 +594,12 @@ void goto_convertt::remove_side_effect(
   }
   else if(statement==ID_throw)
   {
-    goto_programt::targett t=dest.add_instruction(THROW);
-    t->code = code_expressiont(
-      side_effect_expr_throwt(
-        expr.find(ID_exception_list), expr.type(), expr.source_location()));
-    t->code.op0().operands().swap(expr.operands());
-    t->code.add_source_location()=expr.source_location();
-    t->source_location=expr.source_location();
+    codet code = code_expressiont(side_effect_expr_throwt(
+      expr.find(ID_exception_list), expr.type(), expr.source_location()));
+    code.op0().operands().swap(expr.operands());
+    code.add_source_location() = expr.source_location();
+    dest.add(goto_programt::instructiont(
+      std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
 
     // the result can't be used, these are void
     expr.make_nil();

src/goto-programs/string_abstraction.cpp

@@ -993,7 +993,8 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol,
 
   if(symbol.is_static_lifetime)
   {
-    goto_programt::targett dummy_loc=initialization.add_instruction();
+    goto_programt::targett dummy_loc =
+      initialization.add(goto_programt::instructiont());
     dummy_loc->source_location=symbol.location;
     make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
     initialization.instructions.erase(dummy_loc);
@@ -1249,20 +1250,18 @@ goto_programt::targett string_abstractiont::value_assignments_if(
 {
   goto_programt tmp;
 
-  goto_programt::targett goto_else=tmp.add_instruction(GOTO);
-  goto_programt::targett goto_out=tmp.add_instruction(GOTO);
-  goto_programt::targett else_target=tmp.add_instruction(SKIP);
-  goto_programt::targett out_target=tmp.add_instruction(SKIP);
-
-  *goto_else = goto_programt::make_goto(
-    else_target, boolean_negate(rhs.cond()), target->source_location);
-
-  *goto_out =
-    goto_programt::make_goto(out_target, true_exprt(), target->source_location);
-
-  else_target->source_location=target->source_location;
-
-  out_target->source_location=target->source_location;
+  goto_programt::targett goto_else =
+    tmp.add(goto_programt::make_incomplete_goto(
+      boolean_negate(rhs.cond()), target->source_location));
+  goto_programt::targett goto_out = tmp.add(
+    goto_programt::make_incomplete_goto(true_exprt(), target->source_location));
+  goto_programt::targett else_target =
+    tmp.add(goto_programt::make_skip(target->source_location));
+  goto_programt::targett out_target =
+    tmp.add(goto_programt::make_skip(target->source_location));
+
+  goto_else->complete_goto(else_target);
+  goto_out->complete_goto(out_target);
 
   value_assignments(tmp, goto_out, lhs, rhs.true_case());
   value_assignments(tmp, else_target, lhs, rhs.false_case());