Merge pull request diffblue#265 from danpoe/feature/cyclic-dependency-analysis-vs

Cyclic variable sensitivity dependency analysis

Author: chrisr-diffblue

regression/goto-analyzer/variable-sensitivity-dependence-graph-periodic-task-01/main.c

@@ -0,0 +1,8 @@
+int x;
+int y;
+
+void main(void)
+{
+  x = y;
+  y = 1;
+}

regression/goto-analyzer/variable-sensitivity-dependence-graph-periodic-task-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--show --dependence-graph-vs --periodic-task --json -
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"task": "first"
+"task": "later"
+"expression": "y"
+--
+^warning: ignoring
+"expression": "x"
+--

regression/goto-analyzer/variable-sensitivity-dependence-graph-periodic-task-02/main.c

@@ -0,0 +1,14 @@
+int g_x;
+int g_y;
+
+int x;
+int y;
+
+void main(void)
+{
+  g_x = g_y;
+  x = y;
+
+  g_y = 1;
+  y = 1;
+}

regression/goto-analyzer/variable-sensitivity-dependence-graph-periodic-task-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--show --dependence-graph-vs --periodic-task --json -
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"line": "2",\n.*\n.*\n\s*"task": "first"
+"line": "12",\n.*\n.*\n\s*"task": "later"
+"line": "5",\n.*\n.*\n\s*"task": "first"
+"line": "13",\n.*\n.*\n\s*"task": "later"
+--
+^warning: ignoring
+--

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

@@ -520,6 +520,85 @@ jsont variable_sensitivity_dependence_domaint::output_json(
   return graph;
 }
 
+jsont variable_sensitivity_dependence_domaint::output_json_additional(
+  const namespacet &ns,
+  const variable_sensitivity_dependence_domaint &base_state) const
+{
+  json_arrayt graph;
+
+  for(const auto &cd : control_deps)
+  {
+    const goto_programt::const_targett target=cd.first;
+    const tvt branch=cd.second;
+
+    json_objectt &link=graph.push_back().make_object();
+
+    link["locationNumber"]=
+      json_numbert(std::to_string(target->location_number));
+    link["sourceLocation"]=json(target->source_location);
+    link["type"]=json_stringt("control");
+    link["branch"]=json_stringt(branch.to_string());
+  }
+
+  for(const auto &target : control_dep_calls)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["locationNumber"]=
+      json_numbert(std::to_string(target->location_number));
+    link["sourceLocation"]=json(target->source_location);
+    link["type"]=json_stringt("control");
+    link["branch"]=json_stringt("UNCONDITIONAL");
+  }
+
+  for(const auto &dep : base_state.domain_data_deps)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["locationNumber"]=
+      json_numbert(std::to_string(dep.first->location_number));
+    link["sourceLocation"]=json(dep.first->source_location);
+    json_stringt(dep.first->source_location.as_string());
+    link["type"]=json_stringt("data");
+    link["task"]=json_stringt("first");
+
+    const std::set<exprt> &expr_set=dep.second;
+    json_arrayt &expressions=link["expressions"].make_array();
+
+    for(const exprt &e : expr_set)
+    {
+      json_objectt &object=expressions.push_back().make_object();
+      object["expression"]=json_stringt(from_expr(ns, "", e));
+      object["certainty"]=json_stringt("maybe");
+    }
+  }
+
+  for(const auto &dep : domain_data_deps)
+  {
+    if(base_state.domain_data_deps.find(dep.first) !=
+       base_state.domain_data_deps.end())
+      continue;
+
+    json_objectt &link=graph.push_back().make_object();
+    link["locationNumber"]=
+      json_numbert(std::to_string(dep.first->location_number));
+    link["sourceLocation"]=json(dep.first->source_location);
+    json_stringt(dep.first->source_location.as_string());
+    link["type"]=json_stringt("data");
+    link["task"]=json_stringt("later");
+
+    const std::set<exprt> &expr_set=dep.second;
+    json_arrayt &expressions=link["expressions"].make_array();
+
+    for(const exprt &e : expr_set)
+    {
+      json_objectt &object=expressions.push_back().make_object();
+      object["expression"]=json_stringt(from_expr(ns, "", e));
+      object["certainty"]=json_stringt("maybe");
+    }
+  }
+
+  return graph;
+}
+
 void variable_sensitivity_dependence_domaint::populate_dep_graph(
   variable_sensitivity_dependence_grapht &dep_graph,
   goto_programt::const_targett this_loc) const

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h

@@ -132,6 +132,10 @@ class variable_sensitivity_dependence_domaint:
     const ai_baset &ai,
     const namespacet &ns) const override;
 
+  jsont output_json_additional(
+    const namespacet &ns,
+    const variable_sensitivity_dependence_domaint &base_state) const;
+
   void populate_dep_graph(
     variable_sensitivity_dependence_grapht &,
     goto_programt::const_targett) const;
@@ -259,6 +263,73 @@ class variable_sensitivity_dependence_grapht:
     return entry.first->second;
   }
 
+  // output json, and mark additional data dependencies in this dependence graph
+  // compared to the given `base`
+  jsont output_json_additional(
+    const goto_modelt &goto_model,
+    const variable_sensitivity_dependence_grapht &base) const
+  {
+    const namespacet ns(goto_model.symbol_table);
+
+    json_objectt result;
+
+    forall_goto_functions(f_it, goto_model.goto_functions)
+    {
+      if(f_it->second.body_available())
+      {
+        result[id2string(f_it->first)]=
+          output_json_additional(ns, f_it->second.body, f_it->first, base);
+      }
+      else
+      {
+        result[id2string(f_it->first)]=json_arrayt();
+      }
+    }
+
+    return result;
+  }
+
+  jsont output_json_additional(
+    const namespacet &ns,
+    const goto_programt &goto_program,
+    const irep_idt &identifier,
+    const variable_sensitivity_dependence_grapht &base) const
+  {
+    json_arrayt contents;
+
+    forall_goto_program_instructions(i_it, goto_program)
+    {
+      json_objectt location;
+      location["locationNumber"]=
+        json_numbert(std::to_string(i_it->location_number));
+      location["sourceLocation"]=
+        json_stringt(i_it->source_location.as_string());
+
+      // state of this
+      const statet &state = find_state(i_it);
+      const variable_sensitivity_dependence_domaint &dep_graph_state =
+        static_cast<const variable_sensitivity_dependence_domaint &>(state);
+
+      // state of base
+      const statet &base_state = base.find_state(i_it);
+      const variable_sensitivity_dependence_domaint &base_dep_graph_state =
+        static_cast<const variable_sensitivity_dependence_domaint &>(base_state);
+
+      location["abstractState"]=dep_graph_state.output_json_additional(
+        ns,
+        base_dep_graph_state);
+
+      // Ideally we need output_instruction_json
+      std::ostringstream out;
+      goto_program.output_instruction(ns, identifier, out, *i_it);
+      location["instruction"]=json_stringt(out.str());
+
+      contents.push_back(location);
+    }
+
+    return contents;
+  }
+
   post_dominators_mapt &cfg_post_dominators()
   {
     return post_dominators;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -344,6 +344,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     {
       options.set_option("dependence-graph-vs", true);
       options.set_option("domain set", true);
+      options.set_option("periodic-task", cmdline.isset("periodic-task"));
 
       // Configuration of variable sensitivity domain
       options.set_option("pointers", cmdline.isset("pointers"));
@@ -777,6 +778,13 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     if(options.get_bool_option("dependence-graph") &&
        options.get_bool_option("periodic-task"))
     {
+      if(!options.get_bool_option("json"))
+      {
+        error() << "Must use json output via --json with --periodic-task"
+          << eom;
+        return CPROVER_EXIT_INTERNAL_ERROR;
+      }
+
       namespacet ns(goto_model.symbol_table);
 
       dependence_grapht dg_base(goto_model.goto_functions, ns, false);
@@ -785,16 +793,39 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       dependence_grapht dg_periodic(goto_model.goto_functions, ns, true);
       dg_periodic(goto_model);
 
-      if(options.get_bool_option("json"))
-      {
-        out << dg_periodic.output_json_additional(goto_model, dg_base);
-      }
-      else
+      out << dg_periodic.output_json_additional(goto_model, dg_base);
+
+      return CPROVER_EXIT_SUCCESS;
+    }
+
+    // special case for variable sensitivity dependence graph with the
+    // assumption of periodic tasks for now
+    if(options.get_bool_option("dependence-graph-vs") &&
+       options.get_bool_option("periodic-task"))
+    {
+      if(!options.get_bool_option("json"))
       {
-        error() << "Must use json output via --json with --periodic-task" << eom;
+        error() << "Must use json output via --json with --periodic-task"
+          << eom;
         return CPROVER_EXIT_INTERNAL_ERROR;
       }
 
+      namespacet ns(goto_model.symbol_table);
+
+      variable_sensitivity_dependence_grapht dg_vs_base(
+        goto_model.goto_functions,
+        ns,
+        ai_configt::from_options(options).with_periodic_task(false));
+      dg_vs_base(goto_model);
+
+      variable_sensitivity_dependence_grapht dg_vs_periodic(
+        goto_model.goto_functions,
+        ns,
+        ai_configt::from_options(options).with_periodic_task(true));
+      dg_vs_periodic(goto_model);
+
+      out << dg_vs_periodic.output_json_additional(goto_model, dg_vs_base);
+
       return CPROVER_EXIT_SUCCESS;
     }