MMIO instrument: print status

Previously, there was no indication as to whether any transformation had
taken place.

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 reads, 1 writes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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>
@@ -30,6 +31,9 @@ class mm_iot
 
   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";
@@ -117,6 +121,7 @@ void mm_iot::mm_io(goto_functionst::goto_functiont &goto_function)
            typecast_exprt(size_opt.value(), st)},
           source_location);
         goto_function.body.insert_before_swap(it, call);
+        ++reads_replaced;
         it++;
       }
     }
@@ -140,21 +145,33 @@ void mm_iot::mm_io(goto_functionst::goto_functiont &goto_function)
            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)
 {
   mm_iot rewrite{symbol_table};
 
-  for(auto & f : goto_functions.function_map)
+  for(auto &f : goto_functions.function_map)
     rewrite.mm_io(f.second);
+
+  if(rewrite.reads_replaced || rewrite.writes_replaced)
+  {
+    messaget log{message_handler};
+    log.status() << "Replaced MMIO operations: " << rewrite.reads_replaced
+                 << " read(s), " << rewrite.writes_replaced << " write(s)"
+                 << messaget::eom;
+  }
 }
 
-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);