Basic changes required to store the original goto-location into the goto binary.

Author: NlightNFotis

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,11 @@ 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(
+        "originalGOTOLocation",
+        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,15 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("store-goto-locations"))
+    {
+      Forall_goto_functions(it, goto_functions)
+      {
+        auto &function_body = it->second.body;
+        store_goto_locations(function_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 STORE_GOTO_LOCATION_H
+#define STORE_GOTO_LOCATION_H
+
+
+#include <goto-programs/goto_program.h>
+
+void store_goto_locations(goto_programt &goto_program);
+
+#endif // STORE_GOTO_LOCATION_H

src/goto-programs/goto_program.cpp

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

src/goto-programs/show_goto_functions_json.cpp

@@ -67,6 +67,10 @@ json_objectt show_goto_functions_jsont::convert(
         {
           instruction_entry["sourceLocation"]=
             json(instruction.code.source_location());
+
+          if(instruction.code.source_location().get_goto_location()!="")
+            instruction_entry["originalGOTOLocation"]=
+              json_stringt(id2string(instruction.code.source_location().get_goto_location()));
         }
 
         std::ostringstream instruction_builder;

src/util/source_location.h

@@ -140,6 +140,16 @@ class source_locationt:public irept
     return get_bool(ID_hide);
   }
 
+  void set_goto_location(unsigned location)
+  {
+    set("GOTO_location", location);
+  }
+
+  const irep_idt get_goto_location() const
+  {
+    return get("GOTO_location");
+  }
+
   static bool is_built_in(const std::string &s)
   {
     std::string built_in1="<built-in-"; // "<built-in-additions>";