Merge pull request #167 from diffblue/goto_location_storing

[TYT-3] Store the original GOTO location in a GOTO binary

Author: Thomas Kiley

regression/goto-instrument/store_goto_locations/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-instrument/store_goto_locations/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --store-goto-locations
+^EXIT=0$
+^SIGNAL=0$
+Original GOTO location
+--
+--

src/analyses/ai.cpp

@@ -169,6 +169,9 @@ jsont ai_baset::output_json(
     location["sourceLocation"]=
       json_stringt(i_it->source_location.as_string());
     location["abstractState"]=find_state(i_it).output_json(*this, ns);
+    auto original_location = i_it->source_location.get_goto_location();
+    if(original_location!="")
+      location["originalGOTOLocation"]=json_stringt(id2string(original_location));
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
@@ -228,6 +231,13 @@ xmlt ai_baset::output_xml(
     location.set_attribute(
       "source_location",
       i_it->source_location.as_string());
+    auto original_location = i_it->source_location.get_goto_location();
+    if(original_location!="")
+    {
+      location.set_attribute(
+        "original_GOTO_Location",
+        id2string(original_location));
+    }
 
     location.new_element(find_state(i_it).output_xml(*this, ns));
 

src/goto-instrument/Makefile

@@ -51,6 +51,7 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
+      store_goto_location.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -95,6 +95,8 @@ Author: Daniel Kroening, [email protected]
 #include "model_argc_argv.h"
 #include "undefined_functions.h"
 #include "remove_function.h"
+#include "store_goto_location.h"
+
 void goto_instrument_parse_optionst::eval_verbosity()
 {
   unsigned int v=8;
@@ -432,6 +434,14 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("store-goto-locations"))
+    {
+      for(auto &function : goto_functions.function_map)
+      {
+        store_goto_locations(function.second.body);
+      }
+    }
+
     if(cmdline.isset("check-call-sequence"))
     {
       do_remove_returns();

src/goto-instrument/goto_instrument_parse_options.h

@@ -78,6 +78,7 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):" \
+  "(store-goto-locations)" \
   "(remove-calls-nobody)"
 
 class goto_instrument_parse_optionst:

src/goto-instrument/show_locations.cpp

@@ -45,6 +45,8 @@ void show_locations(
         l.new_element("file").data=id2string(source_location.get_file());
         l.new_element("function").data=
           id2string(source_location.get_function());
+        l.new_element("original_goto_location").data=
+          id2string(source_location.get_goto_location());
 
         std::cout << xml << '\n';
       }
@@ -53,7 +55,9 @@ void show_locations(
     case ui_message_handlert::uit::PLAIN:
       std::cout << function_id << " "
                 << it->location_number << " "
-                << it->source_location << '\n';
+                << it->source_location << " "
+                << "(Original GOTO Location:" << " "
+                << it->source_location.get_goto_location() << ") \n";
       break;
 
     default:

src/goto-instrument/store_goto_location.cpp

@@ -0,0 +1,17 @@
+#include "store_goto_location.h"
+
+#include <goto-programs/goto_program.h>
+#include <util/source_location.h>
+
+void store_goto_locations(goto_programt &goto_program)
+{
+    for(auto it=goto_program.instructions.begin();
+        it!=goto_program.instructions.end();
+        it++)
+    {
+      auto &source_location=it->source_location;
+      auto location_number=it->location_number;
+
+      source_location.set_goto_location(location_number);
+    }
+}

src/goto-instrument/store_goto_location.h

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Store the location of instructions in the GOTO binary
+
+Author: Diffblue Limited (c) 2017
+
+Date: August 2017
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H
+#define CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H
+
+
+#include <goto-programs/goto_program.h>
+
+void store_goto_locations(goto_programt &goto_program);
+
+#endif // CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H

src/goto-programs/goto_program.cpp

@@ -49,6 +49,11 @@ std::ostream &goto_programt::output_instruction(
   const goto_program_templatet::instructiont &instruction) const
 {
   out << "        // " << instruction.location_number << " ";
+  auto original_location=instruction.source_location.get_goto_location();
+  if(original_location!="")
+  {
+    out << "(Original GOTO location: " << original_location << ") ";
+  }
 
   if(!instruction.source_location.is_nil())
     out << instruction.source_location.as_string();