Merge pull request #6896 from tautschnig/cleanup/output_instruction

tautschnig · web-flow · commit 8bf3ea62ccdd · 2022-05-31T09:36:10.000+02:00
Replace all uses of goto_programt::output_instruction
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
@@ -43,6 +43,8 @@ void ai_baset::output(
   const goto_programt &goto_program,
   std::ostream &out) const
 {
+  (void)function_id; // unused parameter
+
   forall_goto_program_instructions(i_it, goto_program)
   {
     out << "**** " << i_it->location_number << " " << i_it->source_location()
@@ -51,7 +53,7 @@ void ai_baset::output(
     abstract_state_before(i_it)->output(out, *this, ns);
     out << "\n";
     #if 1
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
     out << "\n";
     #endif
   }
@@ -84,13 +86,15 @@ jsont ai_baset::output_json(
   const irep_idt &function_id,
   const goto_programt &goto_program) const
 {
+  (void)function_id; // unused parameter
+
   json_arrayt contents;
 
   forall_goto_program_instructions(i_it, goto_program)
   {
     // Ideally we need output_instruction_json
     std::ostringstream out;
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
 
     json_objectt location{
       {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
@@ -135,6 +139,8 @@ xmlt ai_baset::output_xml(
   const irep_idt &function_id,
   const goto_programt &goto_program) const
 {
+  (void)function_id; // unused parameter
+
   xmlt function_body;
 
   forall_goto_program_instructions(i_it, goto_program)
@@ -147,7 +153,7 @@ xmlt ai_baset::output_xml(
 
     // Ideally we need output_instruction_xml
     std::ostringstream out;
-    goto_program.output_instruction(ns, function_id, out, *i_it);
+    i_it->output(out);
     location.set_attribute("instruction", out.str());
 
     function_body.new_element(location);
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
@@ -173,16 +173,16 @@ bool flow_insensitive_analysis_baset::visit(
 //  if (id2string(l->function).find("debug")!=std::string::npos)
 //    std::cout << l->function << '\n'; //=="messages::debug")
 
-//  {
-//    static unsigned state_cntr=0;
-//    std::string s("pastate"); s += std::to_string(state_cntr);
-//    std::ofstream f(s.c_str());
-//    goto_program.output_instruction(ns, "", f, l);
-//    f << '\n';
-//    get_state().output(ns, f);
-//    f.close();
-//    state_cntr++;
-//  }
+  //  {
+  //    static unsigned state_cntr=0;
+  //    std::string s("pastate"); s += std::to_string(state_cntr);
+  //    std::ofstream f(s.c_str());
+  //    l->output(f);
+  //    f << '\n';
+  //    get_state().output(ns, f);
+  //    f.close();
+  //    state_cntr++;
+  //  }
 
   return new_data;
 }
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
@@ -365,7 +365,7 @@ void local_bitvector_analysist::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << "\n";
 
     l++;
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
@@ -497,7 +497,7 @@ void local_may_aliast::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << "\n";
 
     l++;
diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp
@@ -217,7 +217,7 @@ void local_safe_pointerst::output(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << '\n';
   }
 }
@@ -268,7 +268,7 @@ void local_safe_pointerst::output_safe_dereferences(
     }
 
     out << '\n';
-    goto_program.output_instruction(ns, irep_idt(), out, instruction);
+    instruction.output(out);
     out << '\n';
   }
 }
diff --git a/src/analyses/sese_regions.cpp b/src/analyses/sese_regions.cpp
@@ -221,7 +221,7 @@ static std::string brief_instruction_string(
     &program_relative_instruction_indices)
 {
   std::ostringstream ostr;
-  goto_program.output_instruction(ns, "", ostr, *instruction);
+  instruction->output(ostr);
   return instruction_ordinals(
            instruction, program_relative_instruction_indices) +
          " " + trimmed_last_line(ostr.str());
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
@@ -94,7 +94,7 @@ void static_analysis_baset::output(
     get_state(i_it).output(ns, out);
     out << "\n";
     #if 0
-    goto_program.output_instruction(ns, identifier, out, i_it);
+    i_it->output(out);
     out << "\n";
     #endif
   }
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
@@ -75,7 +75,7 @@ static void output_dead_plain(
   for(dead_mapt::const_iterator it=dead_map.begin();
       it!=dead_map.end();
       ++it)
-    goto_program.output_instruction(ns, function_identifier, os, *it->second);
+    it->second->output(os);
 }
 
 static void add_to_xml(
@@ -136,7 +136,7 @@ static void add_to_json(
       ++it)
   {
     std::ostringstream oss;
-    goto_program.output_instruction(ns, function_identifier, oss, *it->second);
+    it->second->output(oss);
     std::string s=oss.str();
 
     std::string::size_type n=s.find('\n');
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
@@ -284,7 +284,6 @@ class change_impactt
     char prefix,
     const goto_programt &goto_program,
     const namespacet &ns,
-    const irep_idt &function_id,
     goto_programt::const_targett &target) const;
 };
 
@@ -606,7 +605,7 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, ns, function_id, target);
+    output_instruction(prefix, goto_program, ns, target);
   }
 }
 
@@ -644,7 +643,7 @@ void change_impactt::output_change_impact(
 
     if(old_mod_flags&DELETED)
     {
-      output_instruction('-', goto_program, o_ns, function_id, o_target);
+      output_instruction('-', goto_program, o_ns, o_target);
       ++o_target;
       --target;
       continue;
@@ -696,7 +695,7 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, n_ns, function_id, target);
+    output_instruction(prefix, goto_program, n_ns, target);
   }
   for( ;
       o_target!=old_goto_program.instructions.end();
@@ -724,15 +723,14 @@ void change_impactt::output_change_impact(
     else
       UNREACHABLE;
 
-    output_instruction(prefix, goto_program, o_ns, function_id, o_target);
+    output_instruction(prefix, goto_program, o_ns, o_target);
   }
 }
 
 void change_impactt::output_instruction(
   char prefix,
   const goto_programt &goto_program,
   const namespacet &ns,
-  const irep_idt &function_id,
   goto_programt::const_targett &target) const
 {
   if(compact_output)
@@ -748,7 +746,7 @@ void change_impactt::output_instruction(
   else
   {
     std::cout << prefix;
-    goto_program.output_instruction(ns, function_id, std::cout, *target);
+    target->output(std::cout);
   }
 }
 
diff --git a/src/goto-diff/unified_diff.cpp b/src/goto-diff/unified_diff.cpp
@@ -130,15 +130,15 @@ void unified_difft::output_diff(
     {
     case differencet::SAME:
       os << ' ';
-      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      d.first->output(os);
       break;
     case differencet::DELETED:
       os << '-';
-      old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
+      d.first->output(os);
       break;
     case differencet::NEW:
       os << '+';
-      new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
+      d.first->output(os);
       break;
     }
   }
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -51,9 +51,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       ++it)
   {
     if(loop.contains(it))
-    {
-      goto_program.output_instruction(ns, "scratch", std::cout, *it);
-    }
+      it->output(std::cout);
   }
 
   std::cout << "Modified:\n";
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
@@ -32,7 +32,7 @@ bool enumerating_loop_accelerationt::accelerate(
         it!=path.end();
         ++it)
     {
-      goto_program.output_instruction(ns, "OMG", std::cout, *it->loc);
+      it->loc->output(std::cout);
     }
 #endif
 
diff --git a/src/goto-instrument/accelerate/path.cpp b/src/goto-instrument/accelerate/path.cpp
@@ -15,10 +15,8 @@ Author: Matt Lewis
 
 void output_path(
   const patht &path,
-  const goto_programt &program,
-  const namespacet &ns,
   std::ostream &str)
 {
   for(const auto &step : path)
-    program.output_instruction(ns, "path", str, *step.loc);
+    step.loc->output(str);
 }
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -62,7 +62,7 @@ bool polynomial_acceleratort::accelerate(
       it!=body.end();
       ++it)
   {
-    program.output_instruction(ns, "scratch", std::cout, *it);
+    it->output(std::cout);
   }
 
   std::cout << "Modified:\n";
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -947,7 +947,11 @@ void code_contractst::apply_function_contract(
   // Kill return value variable if fresh
   if(call_ret_is_fresh_var)
   {
-    function_body.output_instruction(ns, "", log.warning(), *target);
+    log.conditional_output(
+      log.warning(), [&target](messaget::mstreamt &mstream) {
+        target->output(mstream);
+        mstream << messaget::eom;
+      });
     auto dead_inst =
       goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
     function_body.insert_before_swap(target, dead_inst);
@@ -1120,11 +1124,14 @@ void code_contractst::apply_loop_contract(
     {
       if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0)
       {
-        log.error() << "Computed loop at " << loop_head->source_location()
+        log.conditional_output(
+          log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
+            mstream << "Computed loop at " << loop_head->source_location()
                     << "contains an instruction beyond [loop_head, loop_end]:"
                     << messaget::eom;
-        goto_function.body.output_instruction(
-          ns, function_name, log.error(), *i);
+            i->output(mstream);
+            mstream << messaget::eom;
+          });
         throw 0;
       }
     }
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
@@ -204,16 +204,20 @@ bool is_loop_free(
     auto size = scc_size[scc_id];
     if(size > 1)
     {
-      log.error() << "Found CFG SCC with size " << size << messaget::eom;
-      for(const auto &node_id : node_to_scc)
-      {
-        if(node_to_scc[node_id] == scc_id)
-        {
-          const auto &pc = cfg[node_id].PC;
-          goto_program.output_instruction(ns, "", log.error(), *pc);
-          log.error() << messaget::eom;
-        }
-      }
+      log.conditional_output(
+        log.error(),
+        [&cfg, &node_to_scc, &scc_id, &size](messaget::mstreamt &mstream) {
+          mstream << "Found CFG SCC with size " << size << messaget::eom;
+          for(const auto &node_id : node_to_scc)
+          {
+            if(node_to_scc[node_id] == scc_id)
+            {
+              const auto &pc = cfg[node_id].PC;
+              pc->output(mstream);
+              mstream << messaget::eom;
+            }
+          }
+        });
       return false;
     }
   }
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -273,7 +273,7 @@ int goto_instrument_parse_optionst::doit()
 
         forall_goto_program_instructions(i_it, goto_program)
         {
-          goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
+          i_it->output(std::cout);
           std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
                     << "\n\n";
         }
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
@@ -282,10 +282,8 @@ void goto_unwindt::unwind(
       i_it!=goto_program.instructions.end();)
   {
 #ifdef DEBUG
-    symbol_tablet st;
-    namespacet ns(st);
     std::cout << "Instruction:\n";
-    goto_program.output_instruction(ns, function_id, std::cout, *i_it);
+    i_it->output(std::cout);
 #endif
 
     if(!i_it->is_backwards_goto())
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
@@ -311,7 +311,7 @@ void goto_inlinet::expand_function_call(
 
 #ifdef DEBUG
   std::cout << "Expanding call:\n";
-  dest.output_instruction(ns, irep_idt(), std::cout, *target);
+  target->output(std::cout);
 #endif
 
   exprt lhs;
@@ -691,15 +691,13 @@ void goto_inlinet::output_inline_map(
         goto_function.body_available(),
         "cannot inline function with empty body");
 
-      const goto_programt &goto_program=goto_function.body;
-
       for(const auto &call : call_list)
       {
         const goto_programt::const_targett target=call.first;
         bool transitive=call.second;
 
         out << "  Call:\n";
-        goto_program.output_instruction(ns, id, out, *target);
+        target->output(out);
         out << "  Transitive: " << transitive << "\n";
       }
     }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -120,8 +120,7 @@ void interpretert::show_state()
     output.status() << "End of function '" << function->first << "'\n";
   }
   else
-    function->second.body.output_instruction(
-      ns, function->first, output.status(), *pc);
+    pc->output(output.status());
 
   output.status() << messaget::eom;
 }
diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp
diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp
diff --git a/src/goto-programs/show_goto_functions_json.h b/src/goto-programs/show_goto_functions_json.h
diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp
diff --git a/src/goto-programs/show_goto_functions_xml.h b/src/goto-programs/show_goto_functions_xml.h
diff --git a/src/pointer-analysis/value_set_analysis_fivr.h b/src/pointer-analysis/value_set_analysis_fivr.h
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.h b/src/pointer-analysis/value_set_analysis_fivrns.h

Original file line number	Diff line number	Diff line change
`@@ -365,7 +365,7 @@ void local_bitvector_analysist::output(`
`365`	`365`	`}`
`366`	`366`
`367`	`367`	`out << "\n";`
`368`		`- goto_function.body.output_instruction(ns, irep_idt(), out, instruction);`
	`368`	`+ instruction.output(out);`
`369`	`369`	`out << "\n";`
`370`	`370`
`371`	`371`	`l++;`
Original file line number	Diff line number	Diff line change
`@@ -497,7 +497,7 @@ void local_may_aliast::output(`
`497`	`497`	`}`
`498`	`498`
`499`	`499`	`out << "\n";`
`500`		`- goto_function.body.output_instruction(ns, irep_idt(), out, instruction);`
	`500`	`+ instruction.output(out);`
`501`	`501`	`out << "\n";`
`502`	`502`
`503`	`503`	`l++;`
Original file line number	Diff line number	Diff line change
`@@ -217,7 +217,7 @@ void local_safe_pointerst::output(`
`217`	`217`	`}`
`218`	`218`
`219`	`219`	`out << '\n';`
`220`		`- goto_program.output_instruction(ns, irep_idt(), out, instruction);`
	`220`	`+ instruction.output(out);`
`221`	`221`	`out << '\n';`
`222`	`222`	`}`
`223`	`223`	`}`
`@@ -268,7 +268,7 @@ void local_safe_pointerst::output_safe_dereferences(`
`268`	`268`	`}`
`269`	`269`
`270`	`270`	`out << '\n';`
`271`		`- goto_program.output_instruction(ns, irep_idt(), out, instruction);`
	`271`	`+ instruction.output(out);`
`272`	`272`	`out << '\n';`
`273`	`273`	`}`
`274`	`274`	`}`
Original file line number	Diff line number	Diff line change
`@@ -221,7 +221,7 @@ static std::string brief_instruction_string(`
`221`	`221`	`&program_relative_instruction_indices)`
`222`	`222`	`{`
`223`	`223`	`std::ostringstream ostr;`
`224`		`- goto_program.output_instruction(ns, "", ostr, *instruction);`
	`224`	`+ instruction->output(ostr);`
`225`	`225`	`return instruction_ordinals(`
`226`	`226`	`instruction, program_relative_instruction_indices) +`
`227`	`227`	`" " + trimmed_last_line(ostr.str());`
Original file line number	Diff line number	Diff line change
`@@ -94,7 +94,7 @@ void static_analysis_baset::output(`
`94`	`94`	`get_state(i_it).output(ns, out);`
`95`	`95`	`out << "\n";`
`96`	`96`	`#if 0`
`97`		`- goto_program.output_instruction(ns, identifier, out, i_it);`
	`97`	`+ i_it->output(out);`
`98`	`98`	`out << "\n";`
`99`	`99`	`#endif`
`100`	`100`	`}`
Original file line number	Diff line number	Diff line change
`@@ -284,7 +284,6 @@ class change_impactt`
`284`	`284`	`char prefix,`
`285`	`285`	`const goto_programt &goto_program,`
`286`	`286`	`const namespacet &ns,`
`287`		`- const irep_idt &function_id,`
`288`	`287`	`goto_programt::const_targett &target) const;`
`289`	`288`	`};`
`290`	`289`
`@@ -606,7 +605,7 @@ void change_impactt::output_change_impact(`
`606`	`605`	`else`
`607`	`606`	`UNREACHABLE;`
`608`	`607`
`609`		`- output_instruction(prefix, goto_program, ns, function_id, target);`
	`608`	`+ output_instruction(prefix, goto_program, ns, target);`
`610`	`609`	`}`
`611`	`610`	`}`
`612`	`611`
`@@ -644,7 +643,7 @@ void change_impactt::output_change_impact(`
`644`	`643`
`645`	`644`	`if(old_mod_flags&DELETED)`
`646`	`645`	`{`
`647`		`- output_instruction('-', goto_program, o_ns, function_id, o_target);`
	`646`	`+ output_instruction('-', goto_program, o_ns, o_target);`
`648`	`647`	`++o_target;`
`649`	`648`	`--target;`
`650`	`649`	`continue;`
`@@ -696,7 +695,7 @@ void change_impactt::output_change_impact(`
`696`	`695`	`else`
`697`	`696`	`UNREACHABLE;`
`698`	`697`
`699`		`- output_instruction(prefix, goto_program, n_ns, function_id, target);`
	`698`	`+ output_instruction(prefix, goto_program, n_ns, target);`
`700`	`699`	`}`
`701`	`700`	`for( ;`
`702`	`701`	`o_target!=old_goto_program.instructions.end();`
`@@ -724,15 +723,14 @@ void change_impactt::output_change_impact(`
`724`	`723`	`else`
`725`	`724`	`UNREACHABLE;`
`726`	`725`
`727`		`- output_instruction(prefix, goto_program, o_ns, function_id, o_target);`
	`726`	`+ output_instruction(prefix, goto_program, o_ns, o_target);`
`728`	`727`	`}`
`729`	`728`	`}`
`730`	`729`
`731`	`730`	`void change_impactt::output_instruction(`
`732`	`731`	`char prefix,`
`733`	`732`	`const goto_programt &goto_program,`
`734`	`733`	`const namespacet &ns,`
`735`		`- const irep_idt &function_id,`
`736`	`734`	`goto_programt::const_targett &target) const`
`737`	`735`	`{`
`738`	`736`	`if(compact_output)`
`@@ -748,7 +746,7 @@ void change_impactt::output_instruction(`
`748`	`746`	`else`
`749`	`747`	`{`
`750`	`748`	`std::cout << prefix;`
`751`		`- goto_program.output_instruction(ns, function_id, std::cout, *target);`
	`749`	`+ target->output(std::cout);`
`752`	`750`	`}`
`753`	`751`	`}`
`754`	`752`
Original file line number	Diff line number	Diff line change
`@@ -130,15 +130,15 @@ void unified_difft::output_diff(`
`130`	`130`	`{`
`131`	`131`	`case differencet::SAME:`
`132`	`132`	`os << ' ';`
`133`		`- new_goto_program.output_instruction(ns_new, identifier, os, *d.first);`
	`133`	`+ d.first->output(os);`
`134`	`134`	`break;`
`135`	`135`	`case differencet::DELETED:`
`136`	`136`	`os << '-';`
`137`		`- old_goto_program.output_instruction(ns_old, identifier, os, *d.first);`
	`137`	`+ d.first->output(os);`
`138`	`138`	`break;`
`139`	`139`	`case differencet::NEW:`
`140`	`140`	`os << '+';`
`141`		`- new_goto_program.output_instruction(ns_new, identifier, os, *d.first);`
	`141`	`+ d.first->output(os);`
`142`	`142`	`break;`
`143`	`143`	`}`
`144`	`144`	`}`