Dependence graph: ensure grapht representation is consistent with domain

src/analyses/ai.cpp

@@ -280,6 +280,11 @@ void ai_baset::initialize(const goto_functionst &goto_functions)
     initialize(it->second);
 }
 
+void ai_baset::finalize()
+{
+  // Nothing to do per default
+}
+
 ai_baset::locationt ai_baset::get_next(
   working_sett &working_set)
 {

src/analyses/ai.h

@@ -133,6 +133,7 @@ class ai_baset
     initialize(goto_program);
     entry_state(goto_program);
     fixedpoint(goto_program, goto_functions, ns);
+    finalize();
   }
 
   void operator()(
@@ -142,6 +143,7 @@ class ai_baset
     initialize(goto_functions);
     entry_state(goto_functions);
     fixedpoint(goto_functions, ns);
+    finalize();
   }
 
   void operator()(const goto_modelt &goto_model)
@@ -150,6 +152,7 @@ class ai_baset
     initialize(goto_model.goto_functions);
     entry_state(goto_model.goto_functions);
     fixedpoint(goto_model.goto_functions, ns);
+    finalize();
   }
 
   void operator()(
@@ -160,6 +163,7 @@ class ai_baset
     initialize(goto_function);
     entry_state(goto_function.body);
     fixedpoint(goto_function.body, goto_functions, ns);
+    finalize();
   }
 
   /// Returns the abstract state before the given instruction
@@ -264,6 +268,9 @@ class ai_baset
   virtual void initialize(const goto_functionst::goto_functiont &);
   virtual void initialize(const goto_functionst &);
 
+  // override to add a cleanup step after fixedpoint has run
+  virtual void finalize();
+
   void entry_state(const goto_programt &);
   void entry_state(const goto_functionst &);
 

src/analyses/dependence_graph.cpp

@@ -120,10 +120,6 @@ void dep_graph_domaint::control_dependencies(
 
     it=next;
   }
-
-  // add edges to the graph
-  for(const auto &c_dep : control_deps)
-    dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, to);
 }
 
 static bool may_be_def_use_pair(
@@ -185,15 +181,6 @@ void dep_graph_domaint::data_dependencies(
 
     dep_graph.reaching_definitions()[to].clear_cache(it->first);
   }
-
-  // add edges to the graph
-  for(const auto &d_dep : data_deps)
-  {
-    // *it might be handled in a future call call to visit only,
-    // depending on the sequence of successors; make sure it exists
-    dep_graph.get_state(d_dep);
-    dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, to);
-  }
 }
 
 void dep_graph_domaint::transform(
@@ -326,3 +313,13 @@ void dependence_grapht::add_dep(
   nodes[n_from].out[n_to].add(kind);
   nodes[n_to].in[n_from].add(kind);
 }
+
+void dep_graph_domaint::populate_dep_graph(
+  dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const
+{
+  for(const auto &c_dep : control_deps)
+    dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, this_loc);
+
+  for(const auto &d_dep : data_deps)
+    dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, this_loc);
+}

src/analyses/dependence_graph.h

@@ -154,13 +154,21 @@ class dep_graph_domaint:public ai_domain_baset
     return node_id;
   }
 
+  void populate_dep_graph(
+    dependence_grapht &, goto_programt::const_targett) const;
+
 private:
   tvt has_values;
   node_indext node_id;
 
   typedef std::set<goto_programt::const_targett> depst;
   depst control_deps, data_deps;
 
+  friend const depst &
+    dependence_graph_test_get_control_deps(const dep_graph_domaint &);
+  friend const depst &
+    dependence_graph_test_get_data_deps(const dep_graph_domaint &);
+
   void control_dependencies(
     goto_programt::const_targett from,
     goto_programt::const_targett to,
@@ -207,6 +215,14 @@ class dependence_grapht:
     }
   }
 
+  void finalize()
+  {
+    for(const auto &location_state : state_map)
+    {
+      location_state.second.populate_dep_graph(*this, location_state.first);
+    }
+  }
+
   void add_dep(
     dep_edget::kindt kind,
     goto_programt::const_targett from,

unit/analyses/dependence_graph.cpp

@@ -0,0 +1,158 @@
+/*******************************************************************\
+
+Module: Unit test for dependence_graph.h
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#include <iostream>
+
+#include <testing-utils/catch.hpp>
+#include <analyses/dependence_graph.h>
+#include <util/symbol_table.h>
+#include <util/std_code.h>
+#include <util/c_types.h>
+#include <util/arith_tools.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <langapi/mode.h>
+#include <java_bytecode/java_bytecode_language.h>
+
+static symbolt create_void_function_symbol(
+  const irep_idt &name,
+  const codet &code)
+{
+  code_typet void_function_type;
+  symbolt function;
+  function.name = name;
+  function.type = void_function_type;
+  function.mode = ID_java;
+  function.value = code;
+  return function;
+}
+
+const std::set<goto_programt::const_targett>&
+    dependence_graph_test_get_control_deps(const dep_graph_domaint &domain)
+{
+  return domain.control_deps;
+}
+
+const std::set<goto_programt::const_targett>&
+    dependence_graph_test_get_data_deps(const dep_graph_domaint &domain)
+{
+  return domain.data_deps;
+}
+
+SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
+{
+  GIVEN("A call under a control dependency")
+  {
+    // Create code like:
+    // void __CPROVER__start() {
+    //   int x;
+    //   if(NONDET(int) == 0) {
+    //     b();
+    //     x = 1;
+    //   }
+    // }
+    // void b() { }
+
+    register_language(new_java_bytecode_language);
+
+    goto_modelt goto_model;
+    namespacet ns(goto_model.symbol_table);
+
+    typet int_type = signed_int_type();
+
+    symbolt x_symbol;
+    x_symbol.name = id2string(goto_functionst::entry_point()) + "::x";
+    x_symbol.base_name = "x";
+    x_symbol.type = int_type;
+    x_symbol.is_lvalue = true;
+    x_symbol.is_state_var = true;
+    x_symbol.is_thread_local = true;
+    x_symbol.is_file_local = true;
+    goto_model.symbol_table.add(x_symbol);
+
+    code_typet void_function_type;
+
+    code_blockt a_body;
+    code_declt declare_x(x_symbol.symbol_expr());
+    a_body.move_to_operands(declare_x);
+
+    code_ifthenelset if_block;
+
+    if_block.cond() =
+      equal_exprt(
+        side_effect_expr_nondett(int_type),
+        from_integer(0, int_type));
+
+    code_blockt then_block;
+    code_function_callt call;
+    call.function() = symbol_exprt("b", void_function_type);
+    then_block.move_to_operands(call);
+    code_assignt assign_x(
+      x_symbol.symbol_expr(), from_integer(1, int_type));
+    then_block.move_to_operands(assign_x);
+
+    if_block.then_case() = then_block;
+
+    a_body.move_to_operands(if_block);
+
+    goto_model.symbol_table.add(
+      create_void_function_symbol(goto_functionst::entry_point(), a_body));
+    goto_model.symbol_table.add(
+      create_void_function_symbol("b", code_skipt()));
+
+    stream_message_handlert msg(std::cerr);
+    goto_convert(goto_model, msg);
+
+    WHEN("Constructing a dependence graph")
+    {
+      dependence_grapht dep_graph(ns);
+      dep_graph(goto_model.goto_functions, ns);
+
+      THEN("The function call and assignment instructions "
+           "should have a control dependency")
+      {
+        for(std::size_t node_idx = 0; node_idx < dep_graph.size(); ++node_idx)
+        {
+          const dep_nodet &node = dep_graph[node_idx];
+          const dep_graph_domaint &node_domain = dep_graph[node.PC];
+          if(node.PC->is_assign() || node.PC->is_function_call())
+          {
+            REQUIRE(
+              dependence_graph_test_get_control_deps(node_domain).size() == 1);
+          }
+        }
+      }
+
+      THEN("The graph's domain and its grapht representation "
+           "should be consistent")
+      {
+        for(std::size_t node_idx = 0; node_idx < dep_graph.size(); ++node_idx)
+        {
+          const dep_nodet &node = dep_graph[node_idx];
+          const dep_graph_domaint &node_domain = dep_graph[node.PC];
+          const std::set<goto_programt::const_targett> &control_deps =
+            dependence_graph_test_get_control_deps(node_domain);
+          const std::set<goto_programt::const_targett> &data_deps =
+            dependence_graph_test_get_data_deps(node_domain);
+
+          std::size_t domain_dep_count =
+            control_deps.size() + data_deps.size();
+
+          REQUIRE(domain_dep_count == node.in.size());
+
+          for(const auto &dep_edge : node.in)
+          {
+            if(dep_edge.second.get() == dep_edget::kindt::CTRL)
+              REQUIRE(control_deps.count(dep_graph[dep_edge.first].PC));
+            else if(dep_edge.second.get() == dep_edget::kindt::DATA)
+              REQUIRE(data_deps.count(dep_graph[dep_edge.first].PC));
+          }
+        }
+      }
+    }
+  }
+}