Merge pull request #991 from karkhaz/pretty-print

Add --print-internal-representation to goto-instrument

Author: kroening

regression/goto-instrument/print-internal-representation/main.c

@@ -0,0 +1,6 @@
+char stage2_start[100];
+
+int main(){
+  int x = 3;
+  unsigned y = 4;
+}

regression/goto-instrument/print-internal-representation/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--print-internal-representation
+^EXIT=0$
+^SIGNAL=0$
+^  \* identifier: __CPROVER_initialize$
+^      \* identifier: main::1::x$
+^      \* identifier: main::1::y$
+--
+--
+Ensures that the output from pretty() is printed when
+--print-internal-representation is passed to goto-instrument.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -578,6 +578,19 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("print-internal-representation"))
+    {
+      for(auto const &pair : goto_functions.function_map)
+        for(auto const &ins : pair.second.body.instructions)
+        {
+          if(ins.code.is_not_nil())
+            status() << ins.code.pretty() << eom;
+          if(ins.guard.is_not_nil())
+            status() << "[guard] " << ins.guard.pretty() << eom;
+        }
+      return 0;
+    }
+
     if(cmdline.isset("show-goto-functions"))
     {
       namespacet ns(symbol_table);
@@ -770,6 +783,7 @@ int goto_instrument_parse_optionst::doit()
     error() << "Out of memory" << eom;
     return 11;
   }
+// NOLINTNEXTLINE(readability/fn_size)
 }
 
 void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
@@ -1451,6 +1465,8 @@ void goto_instrument_parse_optionst::help()
     " --show-symbol-table          show symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --print-internal-representation\n" // NOLINTNEXTLINE(*)
+    "                              show verbose internal representation of the program\n"
     " --list-undefined-functions   list functions without body\n"
     " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
     " --show-natural-loops         show natural loop heads\n"
@@ -1478,7 +1494,8 @@ void goto_instrument_parse_optionst::help()
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
     " --check-invariant function   instruments invariant checking function\n"
     " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
-    " --undefined-function-is-assume-false\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length)
     "                              convert each call to an undefined function to assume(false)\n"
     "\n"
     "Loop transformations:\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -60,6 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
+  "(print-internal-representation)" \
   "(remove-function-pointers)" \
   "(show-claims)(show-properties)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \