Propagation of descriptions of rule applications to allow pretty error-traces browsing.

Author: marek-trtik

driver/analyser.py

@@ -224,13 +224,44 @@ def run_search_for_error_traces(
                     if was_trace_saved:
                         trace_id += 1
 
+    if len(traces_list) > 0:
+        loc_info_file = os.path.abspath(os.path.join(results_dir, "..", "program_slicing", "map_from_functions_to_rule_application_sites.json"))
+        loc_descriptions = generate_location_descriptions(loc_info_file)
+        with open(os.path.join(results_dir, "location_descriptions.json"), "w") as descriptions_file:
+            descriptions_file.write(json.dumps(loc_descriptions, sort_keys=True, indent=4))
+        for error_trace in traces_list:
+            if error_trace["file"] in loc_descriptions:
+                file_description = loc_descriptions[error_trace["file"]]
+                if error_trace["line"] in file_description:
+                    file_line_description = file_description[error_trace["line"]]
+                    if file_line_description["function"].startswith(error_trace["function"]):
+                        error_trace["message"] = file_line_description["message"]
+                    else:
+                        error_trace["message"] = ""
+
     with open(os.path.join(results_dir, "error_traces.json"), "w") as traces_file:
         traces_file.write(json.dumps(traces_list, sort_keys=True, indent=4))
 
     prof["duration"] = time.time() - prof_start_time
     return prof
 
 
+def generate_location_descriptions(loc_info_file):
+    result = {}
+    with open(loc_info_file, "r") as ifile:
+        loc_info = json.load(ifile)
+    for rule_id, per_fn_infos in loc_info.items():
+        for fnname, iid_and_description in per_fn_infos.items():
+            for iid, description in iid_and_description.items():
+                if description["file"] not in result:
+                    result[description["file"]] = {}
+                file_result = result[description["file"]]
+                if description["line"] not in file_result:
+                    file_result[description["line"]] = {}
+                file_line_result = file_result[description["line"]]
+                file_line_result["function"] = fnname
+                file_line_result["message"] = " ".join(description["messages"])
+    return result
 
 
 if __name__ == "__main__":

driver/presentation.py

@@ -145,6 +145,14 @@ def build_HTML_interface_to_slicer_instrumentation_props(props,fname):
             ofile.write("    <td>" + str(loc["instruction_id"]) + "</td>\n")
             ofile.write("  </tr>\n")
             ofile.write("  <tr>\n")
+            ofile.write("    <td>Source file</td>\n")
+            ofile.write("    <td>" + escape_text_to_HTML(loc["file"]) + "</td>\n")
+            ofile.write("  </tr>\n")
+            ofile.write("  <tr>\n")
+            ofile.write("    <td>Source line</td>\n")
+            ofile.write("    <td>" + str(loc["line"]) + "</td>\n")
+            ofile.write("  </tr>\n")
+            ofile.write("  <tr>\n")
             ofile.write("    <td>Rule ID</td>\n")
             ofile.write("    <td>" + loc["rule_id"] + "</td>\n")
             ofile.write("  </tr>\n")
@@ -170,6 +178,10 @@ def build_HTML_interface_to_slicer_instrumentation_props(props,fname):
             ofile.write("    <td>Is sink?</td>\n")
             ofile.write("    <td>" + str(state_index in props["sinks"]) + "</td>\n")
             ofile.write("  </tr>\n")
+            ofile.write("  <tr>\n")
+            ofile.write("    <td>Description</td>\n")
+            ofile.write("    <td>" + escape_text_to_HTML(" ".join(loc["messages"])) + "</td>\n")
+            ofile.write("  </tr>\n")
             ofile.write("</table>\n")
             ofile.write("<p></p>\n")
             state_index += 1
@@ -380,14 +392,15 @@ def make_reduction_string(orig_value, reduced_value, add_percentage=True):
     ofile.write("</table>\n")
 
 
-def build_HTML_interface_to_group_of_error_traces(traces,tool_name,tgt_file,tgt_line,ofile):
+def build_HTML_interface_to_group_of_error_traces(traces,tool_name,tgt_file,tgt_line,message,ofile):
     ofile.write(get_html_prefix("Error traces " + tool_name))
 
     ofile.write("<h1>Error traces found by " + tool_name + "</h1>\n")
     ofile.write("<p>Target location:</p>\n")
     ofile.write("<ul>\n")
-    ofile.write("  <li><b>File</b>: " + tgt_file + "</li>\n")
+    ofile.write("  <li><b>File</b>: " + escape_text_to_HTML(tgt_file) + "</li>\n")
     ofile.write("  <li><b>Line</b>: " + str(tgt_line) + "</li>\n")
+    ofile.write("  <li><b>Message</b>: " + escape_text_to_HTML(message) + "</li>\n")
     ofile.write("</ul>\n")
     ofile.write("<table>\n"
                 "<caption>Error traces leading to the traget location.</caption>\n"
@@ -441,6 +454,7 @@ def build_HTML_interface_to_error_traces(root_dir,sub_dir,ofile):
                         "jbmc",
                         traces_group["file"],
                         traces_group["line"],
+                        traces_group["message"],
                         group_ofile)
         else:
             ofile.write("    <td>none</td>\n")
@@ -453,6 +467,7 @@ def build_HTML_interface_to_error_traces(root_dir,sub_dir,ofile):
                         "symex",
                         traces_group["file"],
                         traces_group["line"],
+                        traces_group["message"],
                         group_ofile)
         else:
             ofile.write("    <td>none</td>\n")

src/taint-instrumenter/instrumentation_props.cpp

@@ -159,12 +159,12 @@ taint_instrumentation_propst::taint_instrumentation_propst(
       assumption,
       turn_on,
       turn_off);
-    for(const auto &fn_vec : rid_and_map.second)
+    for(const auto &fn_map : rid_and_map.second)
     {
-      for(const auto &iit : fn_vec.second)
+      for(const auto &iit_and_descriptions : fn_map.second)
       {
         INVARIANT(
-          iit->type == FUNCTION_CALL,
+          iit_and_descriptions.first->type == FUNCTION_CALL,
           "An application rule must be associated with a function call "
           "instruction");
         if(
@@ -188,15 +188,16 @@ taint_instrumentation_propst::taint_instrumentation_propst(
           program.get_symbol_table().lookup(fn_vec.first);
         location_props.push_back(
           {rid_and_map.first,
-           fn_vec.first,
+           fn_map.first,
            id2string(function_symbol->pretty_name),
-           iit,
+           iit_and_descriptions.first,
+           iit_and_descriptions.second,
            assumption,
            turn_on,
            turn_off});
       }
       if(use_data_flow_insensitive_instrumentation)
-        suppressed.insert(fn_vec.first);
+        suppressed.insert(fn_map.first);
     }
   }
 
@@ -383,6 +384,16 @@ void dump_as_json(const taint_instrumentation_propst &props, json_objectt &out)
       out_loc_props["function_id"] = json_stringt(loc.get_function_id());
       out_loc_props["instruction_id"] =
         json_numbert(msgstream() << loc.get_instruction_id()->location_number);
+      out_loc_props["file"] =
+        json_stringt(loc.get_description().get_source_file());
+      out_loc_props["line"] =
+        json_numbert(loc.get_description().get_source_line());
+      json_arrayt out_messages;
+      {
+        for(const auto &msg : loc.get_description().get_messages())
+          out_messages.push_back(json_stringt(msg));
+      }
+      out_loc_props["messages"] = out_messages;
       json_arrayt out_assumption;
       {
         for(const auto &assumption : loc.get_assumption())

src/taint-instrumenter/instrumentation_props.h

@@ -67,13 +67,15 @@ class taint_instrumentation_propst
       const taint_function_idt &_function_id,
       const taint_pretty_function_idt &_pretty_function_name,
       const taint_instruction_idt &_instruction_id,
+      const description_of_rule_applicationt &description,
       const std::vector<argidx_and_tokennamet> &_assumption,
       const std::vector<argidx_and_tokennamet> &_turn_on,
       const std::vector<argidx_and_tokennamet> &_turn_off)
       : rule_id(_rule_id),
         function_id(_function_id),
         pretty_function_name(_pretty_function_name),
         instruction_id(_instruction_id),
+        description(description),
         assumption(_assumption),
         turn_on(_turn_on),
         turn_off(_turn_off)
@@ -109,11 +111,17 @@ class taint_instrumentation_propst
       return turn_off;
     }
 
+    const description_of_rule_applicationt &get_description() const
+    {
+      return description;
+    }
+
   private:
     taint_rule_idt rule_id;
     taint_function_idt function_id;
     taint_pretty_function_idt pretty_function_name;
     taint_instruction_idt instruction_id;
+    description_of_rule_applicationt description;
     std::vector<argidx_and_tokennamet> assumption;
     std::vector<argidx_and_tokennamet> turn_on;
     std::vector<argidx_and_tokennamet> turn_off;

src/taint-instrumenter/search_for_rule_applications.cpp

@@ -43,8 +43,16 @@ void taint_search_for_rule_applications(
               target->type == FUNCTION_CALL,
               "A transition property must be associated with a function call "
               "instruction");
-            result[props.get_rule_id()][as_string(summary.first)].push_back(
-              target);
+            {
+              auto &location_descriptions =
+                  result[props.get_rule_id()][as_string(summary.first)];
+              if(location_descriptions.count(target) == 0UL)
+                location_descriptions.insert(
+                  {target, {target, props.get_description()}});
+              else
+                location_descriptions.at(target).add_message(
+                  props.get_description());
+            }
             break;
           default:
             break;
@@ -64,12 +72,27 @@ void to_json(
   for(const auto &rid_map : map_from_functions_to_rule_application_sites)
   {
     json_objectt rid;
-    for(const auto &fn_vec : rid_map.second)
+    for(const auto &fn_map : rid_map.second)
     {
-      json_arrayt locs;
-      for(const auto &iit : fn_vec.second)
-        locs.push_back(json_numbert(std::to_string(iit->location_number)));
-      rid[fn_vec.first] = locs;
+      json_objectt locs;
+      for(const auto &iit_and_description : fn_map.second)
+      {
+        json_objectt loc;
+        {
+          loc["file"] =
+            json_stringt(iit_and_description.second.get_source_file());
+          loc["line"] =
+            json_numbert(iit_and_description.second.get_source_line());
+          json_arrayt out_messages;
+          {
+            for(const auto &msg : iit_and_description.second.get_messages())
+              out_messages.push_back(json_stringt(msg));
+          }
+          loc["messages"] = out_messages;
+        }
+        locs[std::to_string(iit_and_description.first->location_number)] = loc;
+      }
+      rid[fn_map.first] = locs;
     }
     result[rid_map.first] = rid;
   }

src/taint-instrumenter/search_for_rule_applications.h

@@ -15,12 +15,49 @@
 #include <util/json.h>
 #include <vector>
 
+class description_of_rule_applicationt
+{
+public:
+
+  description_of_rule_applicationt(
+    const goto_programt::instructionst::const_iterator iit,
+    const std::string &message)
+    : source_file(as_string(iit->source_location.get_file())),
+      source_line(as_string(iit->source_location.get_line())),
+      messages({message})
+  {}
+
+  const std::string &get_source_file() const
+  {
+    return source_file;
+  }
+
+  const std::string &get_source_line() const
+  {
+    return source_line;
+  }
+
+  const std::set<std::string> &get_messages() const
+  {
+    return messages;
+  }
+
+  void add_message(const std::string &new_message)
+  {
+    messages.insert(new_message);
+  }
+
+private:
+  std::string source_file;
+  std::string source_line;
+  std::set<std::string> messages;
+};
+
 typedef std::map<
   taint_rule_idt,
   std::map<std::string, // Name of a function
-           std::vector<goto_programt::instructionst::const_iterator>
-           // Locations inside the function
-           >>
+           std::map<goto_programt::instructionst::const_iterator,
+                    description_of_rule_applicationt>>>
   rule_application_sitest;
 
 /// The function computes a map from transition rules to locations in GOTO