Merge pull request #8175 from tautschnig/cleanup/mm_io-sequence

MMIO instrumentation cleanup

Author: tautschnig

doc/architectural/goto-program-transformations.md

@@ -62,7 +62,8 @@ See the device behaviour section of `modeling-mmio.md` for details of
 modeling memory-mapped I/O regions of device interfaces. This pass is always
 carried out but will only make changes if one of the modelling functions exist.
 
-The implementation of this pass is called via the \ref mm_io(goto_modelt &)
+The implementation of this pass is called via the
+\ref mm_io(goto_modelt &, message_handlert &)
 "mm_io" function. Further documentation of this pass can be found in \ref
 mm_io.h
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -190,7 +190,7 @@ bool jdiff_parse_optionst::process_goto_program(
   class_hierarchyt class_hierarchy(goto_model.symbol_table);
   remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
-  mm_io(goto_model);
+  mm_io(goto_model, ui_message_handler);
 
   // instrument library preconditions
   instrument_preconditions(goto_model);

regression/cbmc/mm_io1/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --no-standard-checks
+^Replaced MMIO operations: 3 read\(s\), 1 write\(s\)
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/label_function_pointer_call_sites.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
+#include <goto-programs/mm_io.h>
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_calls_no_body.h>
@@ -899,6 +900,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("drop-unused-functions"))
     {
       do_indirect_call_and_rtti_removal();
+      mm_io(goto_model, ui_message_handler);
 
       log.status() << "Removing unused functions" << messaget::eom;
       remove_unused_functions(goto_model.goto_functions, ui_message_handler);

src/goto-programs/mm_io.cpp

@@ -14,6 +14,7 @@ Date:   April 2017
 #include "mm_io.h"
 
 #include <util/fresh_symbol.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -23,6 +24,51 @@ Date:   April 2017
 
 #include <set>
 
+class mm_iot
+{
+public:
+  explicit mm_iot(symbol_table_baset &symbol_table);
+
+  void mm_io(goto_functionst::goto_functiont &goto_function);
+
+  std::size_t reads_replaced = 0;
+  std::size_t writes_replaced = 0;
+
+protected:
+  const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
+  const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
+
+  const namespacet ns;
+  exprt mm_io_r;
+  exprt mm_io_r_value;
+  exprt mm_io_w;
+};
+
+mm_iot::mm_iot(symbol_table_baset &symbol_table)
+  : ns(symbol_table),
+    mm_io_r(nil_exprt{}),
+    mm_io_r_value(nil_exprt{}),
+    mm_io_w(nil_exprt{})
+{
+  if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
+  {
+    mm_io_r = mm_io_r_symbol->symbol_expr();
+
+    const auto &value_symbol = get_fresh_aux_symbol(
+      to_code_type(mm_io_r.type()).return_type(),
+      id2string(id_r) + "$value",
+      id2string(id_r) + "$value",
+      mm_io_r_symbol->location,
+      mm_io_r_symbol->mode,
+      symbol_table);
+
+    mm_io_r_value = value_symbol.symbol_expr();
+  }
+
+  if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
+    mm_io_w = mm_io_w_symbol->symbol_expr();
+}
+
 static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
 {
   std::set<dereference_exprt> collected;
@@ -33,13 +79,12 @@ static std::set<dereference_exprt> collect_deref_expr(const exprt &src)
   return collected;
 }
 
-void mm_io(
-  const exprt &mm_io_r,
-  const exprt &mm_io_r_value,
-  const exprt &mm_io_w,
-  goto_functionst::goto_functiont &goto_function,
-  const namespacet &ns)
+void mm_iot::mm_io(goto_functionst::goto_functiont &goto_function)
 {
+  // return early when there is nothing to be done
+  if(mm_io_r.is_nil() && mm_io_w.is_nil())
+    return;
+
   for(auto it = goto_function.body.instructions.begin();
       it != goto_function.body.instructions.end();
       it++)
@@ -76,6 +121,7 @@ void mm_io(
            typecast_exprt(size_opt.value(), st)},
           source_location);
         goto_function.body.insert_before_swap(it, call);
+        ++reads_replaced;
         it++;
       }
     }
@@ -99,45 +145,33 @@ void mm_io(
            typecast_exprt(a_rhs, vt)});
         goto_function.body.insert_before_swap(it);
         *it = goto_programt::make_function_call(fc, source_location);
+        ++writes_replaced;
         it++;
       }
     }
   }
 }
 
-void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
+void mm_io(
+  symbol_tablet &symbol_table,
+  goto_functionst &goto_functions,
+  message_handlert &message_handler)
 {
-  const namespacet ns(symbol_table);
-  exprt mm_io_r = nil_exprt();
-  exprt mm_io_r_value = nil_exprt();
-  exprt mm_io_w = nil_exprt();
+  mm_iot rewrite{symbol_table};
 
-  const irep_idt id_r = CPROVER_PREFIX "mm_io_r";
-  const irep_idt id_w = CPROVER_PREFIX "mm_io_w";
+  for(auto &f : goto_functions.function_map)
+    rewrite.mm_io(f.second);
 
-  if(const auto mm_io_r_symbol = symbol_table.lookup(id_r))
+  if(rewrite.reads_replaced || rewrite.writes_replaced)
   {
-    mm_io_r = mm_io_r_symbol->symbol_expr();
-
-    const auto &value_symbol = get_fresh_aux_symbol(
-      to_code_type(mm_io_r.type()).return_type(),
-      id2string(id_r) + "$value",
-      id2string(id_r) + "$value",
-      mm_io_r_symbol->location,
-      mm_io_r_symbol->mode,
-      symbol_table);
-
-    mm_io_r_value = value_symbol.symbol_expr();
+    messaget log{message_handler};
+    log.status() << "Replaced MMIO operations: " << rewrite.reads_replaced
+                 << " read(s), " << rewrite.writes_replaced << " write(s)"
+                 << messaget::eom;
   }
-
-  if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))
-    mm_io_w = mm_io_w_symbol->symbol_expr();
-
-  for(auto & f : goto_functions.function_map)
-    mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);
 }
 
-void mm_io(goto_modelt &model)
+void mm_io(goto_modelt &model, message_handlert &message_handler)
 {
-  mm_io(model.symbol_table, model.goto_functions);
+  mm_io(model.symbol_table, model.goto_functions, message_handler);
 }

src/goto-programs/mm_io.h

@@ -31,9 +31,10 @@ Date:   April 2017
 
 class goto_functionst;
 class goto_modelt;
+class message_handlert;
 class symbol_tablet;
 
-void mm_io(const symbol_tablet &, goto_functionst &);
-void mm_io(goto_modelt &);
+void mm_io(const symbol_tablet &, goto_functionst &, message_handlert &);
+void mm_io(goto_modelt &, message_handlert &);
 
 #endif // CPROVER_GOTO_PROGRAMS_MM_IO_H

src/goto-programs/process_goto_program.cpp

@@ -45,7 +45,7 @@ bool process_goto_program(
                << messaget::eom;
   remove_function_pointers(log.get_message_handler(), goto_model, false);
 
-  mm_io(goto_model);
+  mm_io(goto_model, log.get_message_handler());
 
   // instrument library preconditions
   instrument_preconditions(goto_model);