Merge pull request #4088 from diffblue/goto_programt_code_cleanup

tautschnig · web-flow · commit be879732d846 · 2019-02-05T21:28:29.000Z
use new goto_programt::instructiont API
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -432,7 +432,7 @@ bool remove_exceptionst::instrument_function_call(
   goto_programt::targett next_it=instr_it;
   next_it++;
 
-  code_function_callt &function_call=to_code_function_call(instr_it->code);
+  code_function_callt &function_call = instr_it->get_function_call();
   DATA_INVARIANT(
     function_call.function().id()==ID_symbol,
     "identified expected to be a symbol");
@@ -493,7 +493,7 @@ void remove_exceptionst::instrument_exceptions(
   {
     if(instr_it->is_decl())
     {
-      code_declt decl=to_code_decl(instr_it->code);
+      code_declt decl = instr_it->get_decl();
       locals.push_back(decl.symbol());
     }
     // Is it a handler push/pop or catch landing-pad?
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
@@ -107,9 +107,8 @@ void remove_asmt::gcc_asm_function_call(
 
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
-  goto_programt::targett call = dest.add_instruction(FUNCTION_CALL);
-  call->code = function_call;
-  call->source_location = code.source_location();
+  dest.add(
+    goto_programt::make_function_call(function_call, code.source_location()));
 
   // do we have it?
   if(!symbol_table.has_symbol(function_identifier))
@@ -157,9 +156,8 @@ void remove_asmt::msc_asm_function_call(
 
   code_function_callt function_call(fkt);
 
-  goto_programt::targett call = dest.add_instruction(FUNCTION_CALL);
-  call->code = function_call;
-  call->source_location = code.source_location();
+  dest.add(
+    goto_programt::make_function_call(function_call, code.source_location()));
 
   // do we have it?
   if(!symbol_table.has_symbol(function_identifier))
@@ -194,7 +192,7 @@ void remove_asmt::process_instruction(
   goto_programt::instructiont &instruction,
   goto_programt &dest)
 {
-  const code_asmt &code = to_code_asm(instruction.code);
+  const code_asmt &code = to_code_asm(instruction.get_other());
 
   const irep_idt &flavor = code.get_flavor();
 
@@ -271,14 +269,15 @@ void remove_asmt::process_instruction_gcc(
       goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
       ab->source_location = code.source_location();
 
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
 
     if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
@@ -292,62 +291,67 @@ void remove_asmt::process_instruction_gcc(
     }
     else if(command == ID_sync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
-      t->code.set(ID_WRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+      code_fence.set(ID_WRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == ID_lwsync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == ID_isync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
       // doesn't do anything by itself,
       // needs to be combined with branch
     }
     else if(command == "dmb" || command == "dsb") // ARM
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
-      t->code.set(ID_WRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+      code_fence.set(ID_WRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == "isb") // ARM
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
       // doesn't do anything by itself,
       // needs to be combined with branch
     }
@@ -436,14 +440,15 @@ void remove_asmt::process_instruction_msc(
       goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
       ab->source_location = code.source_location();
 
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
 
     if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
@@ -95,7 +95,7 @@ bool static_simplifier(
       }
       else if(i_it->is_assign())
       {
-        code_assignt &assign=to_code_assign(i_it->code);
+        code_assignt &assign = i_it->get_assign();
 
         // Simplification needs to be aware of which side of the
         // expression it is handling as:
@@ -115,7 +115,7 @@ bool static_simplifier(
       }
       else if(i_it->is_function_call())
       {
-        code_function_callt &fcall=to_code_function_call(i_it->code);
+        code_function_callt &fcall = i_it->get_function_call();
 
         bool unchanged =
           ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
@@ -73,8 +73,8 @@ void taint_analysist::instrument(
     {
     case FUNCTION_CALL:
       {
-        const code_function_callt &function_call=
-          to_code_function_call(instruction.code);
+        const code_function_callt &function_call =
+          instruction.get_function_call();
         const exprt &function=function_call.function();
 
         if(function.id()==ID_symbol)
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
@@ -257,8 +257,8 @@ void acceleratet::make_overflow_loc(
   }
 
   goto_programt::targett t=program.insert_after(loop_header);
-  t->make_assignment();
-  t->code=code_assignt(overflow_var, false_exprt());
+  *t =
+    goto_programt::make_assignment(code_assignt(overflow_var, false_exprt()));
   t->swap(*loop_header);
   loop.insert(t);
   overflow_locs[loop_header].push_back(t);
@@ -360,8 +360,8 @@ void acceleratet::add_dirty_checks()
       it!=dirty_vars_map.end();
       ++it)
   {
-    goto_programt::instructiont assign(ASSIGN);
-    assign.code=code_assignt(it->second, false_exprt());
+    goto_programt::instructiont assign =
+      goto_programt::make_assignment(code_assignt(it->second, false_exprt()));
     program.insert_before_swap(program.instructions.begin(), assign);
   }
 
@@ -384,8 +384,8 @@ void acceleratet::add_dirty_checks()
 
       if(dirty_var!=dirty_vars_map.end())
       {
-        goto_programt::instructiont clear_flag(ASSIGN);
-        clear_flag.code=code_assignt(dirty_var->second, false_exprt());
+        goto_programt::instructiont clear_flag = goto_programt::make_assignment(
+          code_assignt(dirty_var->second, false_exprt()));
         program.insert_before_swap(it, clear_flag);
       }
     }
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
@@ -164,7 +164,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     {
       if(ins.is_assign())
       {
-        const code_assignt &code_assign = to_code_assign(ins.code);
+        const code_assignt &code_assign = ins.get_assign();
         object_descriptor_exprt ode;
         ode.build(code_assign.lhs(), ns);
 
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
@@ -288,8 +288,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
   goto_programt::const_targett next_PC,
   entryt &entry)
 {
-  const exprt &function=
-    to_code_function_call(instruction.code).function();
+  const exprt &function = instruction.get_function_call().function();
 
   if(function.id()!=ID_symbol)
     return;
@@ -339,8 +338,7 @@ void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
   goto_programt::const_targett next_PC,
   typename cfg_baset<T, P, I>::entryt &entry)
 {
-  const exprt &function=
-    to_code_function_call(instruction.code).function();
+  const exprt &function = instruction.get_function_call().function();
 
   if(function.id()!=ID_symbol)
     return;
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -826,9 +826,11 @@ class goto_programt
       static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
   }
 
-  static instructiont make_other(const codet &_code)
+  static instructiont make_other(
+    const codet &_code,
+    const source_locationt &l = source_locationt::nil())
   {
-    return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {});
+    return instructiont(_code, l, OTHER, nil_exprt(), {});
   }
 
   static instructiont make_decl(
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
@@ -21,7 +21,7 @@ void goto_symext::symex_dead(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const code_deadt &code = to_code_dead(instruction.code);
+  const code_deadt &code = instruction.get_dead();
 
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
@@ -23,13 +23,13 @@ void goto_symext::symex_decl(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const codet &code = instruction.code;
+  const auto &code = instruction.get_decl();
 
   // two-operand decl not supported here
   // we handle the decl with only one operand
   PRECONDITION(code.operands().size() == 1);
 
-  symex_decl(state, to_code_decl(code).symbol());
+  symex_decl(state, code.symbol());
 }
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
@@ -447,7 +447,7 @@ void goto_symext::return_assignment(statet &state)
 
   const goto_programt::instructiont &instruction=*state.source.pc;
   PRECONDITION(instruction.is_return());
-  const code_returnt &code=to_code_return(instruction.code);
+  const code_returnt &code = instruction.get_return();
 
   target.location(state.guard.as_expr(), state.source);
 
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -440,16 +440,15 @@ void goto_symext::symex_step(
 
   case ASSIGN:
     if(!state.guard.is_false())
-      symex_assign(state, to_code_assign(instruction.code));
+      symex_assign(state, instruction.get_assign());
 
     symex_transition(state);
     break;
 
   case FUNCTION_CALL:
     if(!state.guard.is_false())
     {
-      code_function_callt deref_code=
-        to_code_function_call(instruction.code);
+      code_function_callt deref_code = instruction.get_function_call();
 
       if(deref_code.lhs().is_not_nil())
         clean_expr(deref_code.lhs(), state, true);
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
@@ -79,7 +79,7 @@ void goto_symext::symex_other(
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const codet &code = instruction.code;
+  const codet &code = instruction.get_other();
 
   const irep_idt &statement=code.get_statement();
 
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp

Original file line number	Diff line number	Diff line change
`@@ -432,7 +432,7 @@ bool remove_exceptionst::instrument_function_call(`
`432`	`432`	`goto_programt::targett next_it=instr_it;`
`433`	`433`	`next_it++;`
`434`	`434`
`435`		`- code_function_callt &function_call=to_code_function_call(instr_it->code);`
	`435`	`+ code_function_callt &function_call = instr_it->get_function_call();`
`436`	`436`	`DATA_INVARIANT(`
`437`	`437`	`function_call.function().id()==ID_symbol,`
`438`	`438`	`"identified expected to be a symbol");`
`@@ -493,7 +493,7 @@ void remove_exceptionst::instrument_exceptions(`
`493`	`493`	`{`
`494`	`494`	`if(instr_it->is_decl())`
`495`	`495`	`{`
`496`		`- code_declt decl=to_code_decl(instr_it->code);`
	`496`	`+ code_declt decl = instr_it->get_decl();`
`497`	`497`	`locals.push_back(decl.symbol());`
`498`	`498`	`}`
`499`	`499`	`// Is it a handler push/pop or catch landing-pad?`
Original file line number	Diff line number	Diff line change
`@@ -95,7 +95,7 @@ bool static_simplifier(`
`95`	`95`	`}`
`96`	`96`	`else if(i_it->is_assign())`
`97`	`97`	`{`
`98`		`- code_assignt &assign=to_code_assign(i_it->code);`
	`98`	`+ code_assignt &assign = i_it->get_assign();`
`99`	`99`
`100`	`100`	`// Simplification needs to be aware of which side of the`
`101`	`101`	`// expression it is handling as:`
`@@ -115,7 +115,7 @@ bool static_simplifier(`
`115`	`115`	`}`
`116`	`116`	`else if(i_it->is_function_call())`
`117`	`117`	`{`
`118`		`- code_function_callt &fcall=to_code_function_call(i_it->code);`
	`118`	`+ code_function_callt &fcall = i_it->get_function_call();`
`119`	`119`
`120`	`120`	`bool unchanged =`
`121`	`121`	`ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);`
Original file line number	Diff line number	Diff line change
`@@ -73,8 +73,8 @@ void taint_analysist::instrument(`
`73`	`73`	`{`
`74`	`74`	`case FUNCTION_CALL:`
`75`	`75`	`{`
`76`		`- const code_function_callt &function_call=`
`77`		`- to_code_function_call(instruction.code);`
	`76`	`+ const code_function_callt &function_call =`
	`77`	`+ instruction.get_function_call();`
`78`	`78`	`const exprt &function=function_call.function();`
`79`	`79`
`80`	`80`	`if(function.id()==ID_symbol)`
Original file line number	Diff line number	Diff line change
`@@ -257,8 +257,8 @@ void acceleratet::make_overflow_loc(`
`257`	`257`	`}`
`258`	`258`
`259`	`259`	`goto_programt::targett t=program.insert_after(loop_header);`
`260`		`- t->make_assignment();`
`261`		`- t->code=code_assignt(overflow_var, false_exprt());`
	`260`	`+ *t =`
	`261`	`+ goto_programt::make_assignment(code_assignt(overflow_var, false_exprt()));`
`262`	`262`	`t->swap(*loop_header);`
`263`	`263`	`loop.insert(t);`
`264`	`264`	`overflow_locs[loop_header].push_back(t);`
`@@ -360,8 +360,8 @@ void acceleratet::add_dirty_checks()`
`360`	`360`	`it!=dirty_vars_map.end();`
`361`	`361`	`++it)`
`362`	`362`	`{`
`363`		`- goto_programt::instructiont assign(ASSIGN);`
`364`		`- assign.code=code_assignt(it->second, false_exprt());`
	`363`	`+ goto_programt::instructiont assign =`
	`364`	`+ goto_programt::make_assignment(code_assignt(it->second, false_exprt()));`
`365`	`365`	`program.insert_before_swap(program.instructions.begin(), assign);`
`366`	`366`	`}`
`367`	`367`
`@@ -384,8 +384,8 @@ void acceleratet::add_dirty_checks()`
`384`	`384`
`385`	`385`	`if(dirty_var!=dirty_vars_map.end())`
`386`	`386`	`{`
`387`		`- goto_programt::instructiont clear_flag(ASSIGN);`
`388`		`- clear_flag.code=code_assignt(dirty_var->second, false_exprt());`
	`387`	`+ goto_programt::instructiont clear_flag = goto_programt::make_assignment(`
	`388`	`+ code_assignt(dirty_var->second, false_exprt()));`
`389`	`389`	`program.insert_before_swap(it, clear_flag);`
`390`	`390`	`}`
`391`	`391`	`}`
Original file line number	Diff line number	Diff line change
`@@ -164,7 +164,7 @@ void print_global_state_size(const goto_modelt &goto_model)`
`164`	`164`	`{`
`165`	`165`	`if(ins.is_assign())`
`166`	`166`	`{`
`167`		`- const code_assignt &code_assign = to_code_assign(ins.code);`
	`167`	`+ const code_assignt &code_assign = ins.get_assign();`
`168`	`168`	`object_descriptor_exprt ode;`
`169`	`169`	`ode.build(code_assign.lhs(), ns);`
`170`	`170`
Original file line number	Diff line number	Diff line change
`@@ -826,9 +826,11 @@ class goto_programt`
`826`	`826`	`static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});`
`827`	`827`	`}`
`828`	`828`
`829`		`- static instructiont make_other(const codet &_code)`
	`829`	`+ static instructiont make_other(`
	`830`	`+ const codet &_code,`
	`831`	`+ const source_locationt &l = source_locationt::nil())`
`830`	`832`	`{`
`831`		`- return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {});`
	`833`	`+ return instructiont(_code, l, OTHER, nil_exprt(), {});`
`832`	`834`	`}`
`833`	`835`
`834`	`836`	`static instructiont make_decl(`
Original file line number	Diff line number	Diff line change
`@@ -21,7 +21,7 @@ void goto_symext::symex_dead(statet &state)`
`21`	`21`	`{`
`22`	`22`	`const goto_programt::instructiont &instruction=*state.source.pc;`
`23`	`23`
`24`		`- const code_deadt &code = to_code_dead(instruction.code);`
	`24`	`+ const code_deadt &code = instruction.get_dead();`
`25`	`25`
`26`	`26`	`// We increase the L2 renaming to make these non-deterministic.`
`27`	`27`	`// We also prevent propagation of old values.`
Original file line number	Diff line number	Diff line change
`@@ -23,13 +23,13 @@ void goto_symext::symex_decl(statet &state)`
`23`	`23`	`{`
`24`	`24`	`const goto_programt::instructiont &instruction=*state.source.pc;`
`25`	`25`
`26`		`- const codet &code = instruction.code;`
	`26`	`+ const auto &code = instruction.get_decl();`
`27`	`27`
`28`	`28`	`// two-operand decl not supported here`
`29`	`29`	`// we handle the decl with only one operand`
`30`	`30`	`PRECONDITION(code.operands().size() == 1);`
`31`	`31`
`32`		`- symex_decl(state, to_code_decl(code).symbol());`
	`32`	`+ symex_decl(state, code.symbol());`
`33`	`33`	`}`
`34`	`34`
`35`	`35`	`void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)`