Allow post-processing functions to run on a function-by-function basis

Author: NathanJPhillips

src/goto-diff/goto_diff_parse_options.cpp

@@ -396,7 +396,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(symbol_table, goto_functions);
+    remove_asm(goto_model);
 
     // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);

src/goto-programs/remove_asm.cpp

@@ -25,27 +25,20 @@ Date:   December 2014
 class remove_asmt
 {
 public:
-  inline remove_asmt(
-    symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions):
-    symbol_table(_symbol_table),
-    goto_functions(_goto_functions)
+  explicit remove_asmt(symbol_tablet &_symbol_table)
+    : symbol_table(_symbol_table)
   {
   }
 
-  void operator()();
+  void process_function(goto_functionst::goto_functiont &);
 
 protected:
   symbol_tablet &symbol_table;
-  goto_functionst &goto_functions;
 
   void process_instruction(
     goto_programt::instructiont &instruction,
     goto_programt &dest);
 
-  void process_function(
-    goto_functionst::goto_functiont &);
-
   void gcc_asm_function_call(
     const irep_idt &function_base_name,
     const codet &code,
@@ -305,24 +298,24 @@ void remove_asmt::process_function(
 }
 
 /// removes assembler
-void remove_asmt::operator()()
+void remove_asm(
+  goto_functionst::goto_functiont &goto_function,
+  symbol_tablet &symbol_table)
 {
-  Forall_goto_functions(it, goto_functions)
-  {
-    process_function(it->second);
-  }
+  remove_asmt rem(symbol_table);
+  rem.process_function(goto_function);
 }
 
 /// removes assembler
-void remove_asm(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
 {
-  remove_asmt(symbol_table, goto_functions)();
+  remove_asmt rem(symbol_table);
+  for(auto &f : goto_functions.function_map)
+    rem.process_function(f.second);
 }
 
 /// removes assembler
 void remove_asm(goto_modelt &goto_model)
 {
-  remove_asmt(goto_model.symbol_table, goto_model.goto_functions)();
+  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
 }

src/goto-programs/remove_asm.h

@@ -17,8 +17,12 @@ Date:   December 2014
 
 #include <goto-programs/goto_model.h>
 
-void remove_asm(symbol_tablet &, goto_functionst &);
+void remove_asm(
+  goto_functionst::goto_functiont &goto_function,
+  symbol_tablet &symbol_table);
 
-void remove_asm(goto_modelt &);
+void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table);
+
+void remove_asm(goto_modelt &goto_model);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H

src/goto-programs/remove_instanceof.cpp

@@ -22,26 +22,19 @@ Author: Chris Smowton, [email protected]
 class remove_instanceoft
 {
 public:
-  remove_instanceoft(
-    symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions):
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
-    goto_functions(_goto_functions)
+  explicit remove_instanceoft(symbol_tablet &symbol_table)
+  : symbol_table(symbol_table), ns(symbol_table)
   {
-    class_hierarchy(_symbol_table);
+    class_hierarchy(symbol_table);
   }
 
-  // Lower instanceof for all functions:
-  void lower_instanceof();
+  // Lower instanceof for a single functions
+  bool lower_instanceof(goto_programt &);
 
 protected:
   symbol_tablet &symbol_table;
   namespacet ns;
   class_hierarchyt class_hierarchy;
-  goto_functionst &goto_functions;
-
-  bool lower_instanceof(goto_programt &);
 
   bool lower_instanceof(goto_programt &, goto_programt::targett);
 
@@ -174,33 +167,38 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
   return true;
 }
 
-/// See function above
-/// \return Side-effects on this->goto_functions, replacing every instanceof in
-///   every function with an explicit test.
-void remove_instanceoft::lower_instanceof()
+
+/// Replace every instanceof in the passed function with an explicit
+/// class-identifier test.
+/// Extra auxiliary variables may be introduced into symbol_table.
+/// \param function: The function to work on.
+/// \param symbol_table: The symbol table to add symbols to.
+void remove_instanceof(
+  goto_functionst::goto_functiont &function,
+  symbol_tablet &symbol_table)
 {
-  bool changed=false;
-  for(auto &f : goto_functions.function_map)
-    changed=(lower_instanceof(f.second.body) || changed);
-  if(changed)
-    goto_functions.compute_location_numbers();
+  remove_instanceoft rem(symbol_table);
+  rem.lower_instanceof(function.body);
 }
 
-/// See function above
-/// \par parameters: `goto_functions`, a function map, and the corresponding
-/// `symbol_table`.
-/// \return Side-effects on goto_functions, replacing every instanceof in every
-///   function with an explicit test. Extra auxiliary variables may be
-///   introduced into `symbol_table`.
+/// Replace every instanceof in every function with an explicit
+/// class-identifier test.
+/// Extra auxiliary variables may be introduced into symbol_table.
+/// \param goto_functions: The functions to work on.
+/// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table)
 {
-  remove_instanceoft rem(symbol_table, goto_functions);
-  rem.lower_instanceof();
+  remove_instanceoft rem(symbol_table);
+  bool changed=false;
+  for(auto &f : goto_functions.function_map)
+    changed=rem.lower_instanceof(f.second.body) || changed;
+  if(changed)
+    goto_functions.compute_location_numbers();
 }
 
 void remove_instanceof(goto_modelt &goto_model)
 {
-  remove_instanceof(goto_model.symbol_table, goto_model.goto_functions);
+  remove_instanceof(goto_model.goto_functions, goto_model.symbol_table);
 }

src/goto-programs/remove_instanceof.h

@@ -17,8 +17,12 @@ Author: Chris Smowton, [email protected]
 #include "goto_model.h"
 
 void remove_instanceof(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions);
+  goto_functionst::goto_functiont &function,
+  symbol_tablet &symbol_table);
+
+void remove_instanceof(
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table);
 
 void remove_instanceof(goto_modelt &model);
 

src/goto-symex/adjust_float_expressions.cpp

@@ -179,7 +179,7 @@ void adjust_float_expressions(
   }
 }
 
-static void adjust_float_expressions(
+void adjust_float_expressions(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
 {

src/goto-symex/adjust_float_expressions.h

@@ -12,15 +12,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 
+#include <goto-programs/goto_functions.h>
+
 class exprt;
 class namespacet;
-class goto_functionst;
 class goto_modelt;
 
 void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns);
 
+void adjust_float_expressions(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns);
+
 void adjust_float_expressions(
   goto_functionst &goto_functions,
   const namespacet &ns);

src/goto-symex/rewrite_union.cpp

@@ -107,7 +107,7 @@ void rewrite_union(
   }
 }
 
-static void rewrite_union(
+void rewrite_union(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
 {

src/goto-symex/rewrite_union.h

@@ -23,6 +23,10 @@ void rewrite_union(
   exprt &expr,
   const namespacet &ns);
 
+void rewrite_union(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns);
+
 void rewrite_union(
   goto_functionst &goto_functions,
   const namespacet &ns);