Merge pull request diffblue#256 from danpoe/feature/control-deps-of-function-body-instructions-on-calls

Control dependencies of function body instructions to function calls

Author: chrisr-diffblue

regression/goto-analyzer/dependence-graph13/test.desc

@@ -4,9 +4,11 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+
-Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+
-Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+
+// The function entry points shall have a control dependency on the function call
+Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL\]
+Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL\]
+Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL\]
 --
+// The __CPROVER__start function must not have a control dependency on anything
 Function: __CPROVER__start\n.*\n.*\n.*\nControl dependencies: [0-9]+
 ^warning: ignoring

regression/goto-analyzer/dependence-graph14/main.c

@@ -0,0 +1,13 @@
+
+void main(void)
+{
+  int a;
+
+  if(a)
+  {
+    a = 1;
+  }
+
+  a = 2;
+}
+

regression/goto-analyzer/dependence-graph14/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --dependence-graph
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+a = 1;
+Control dependencies: [0-9]+ \[CALL\]\n.*\n.*\n\s+a = 2;
+
+--
+^warning: ignoring

src/analyses/dependence_graph.cpp

@@ -44,7 +44,8 @@ bool dep_graph_domaint::merge(
 
   changed|=merge_control_dependencies(
     src.control_deps,
-    src.control_dep_candidates);
+    src.control_dep_candidates,
+    src.control_dep_calls);
 
   has_changed=false;
   has_values=tvt::unknown();
@@ -74,7 +75,9 @@ void dep_graph_domaint::control_dependencies(
     control_dep_candidates.insert(from);
   else if(from->is_end_function())
   {
+    control_deps.clear();
     control_dep_candidates.clear();
+    control_dep_calls.clear();
     return;
   }
 
@@ -149,6 +152,7 @@ void dep_graph_domaint::control_dependencies(
       }
 
       control_deps.insert(std::make_pair(cd, branch));
+      control_dep_calls.clear();
     }
   }
 
@@ -259,7 +263,8 @@ void dep_graph_domaint::control_dependencies(
 
 bool dep_graph_domaint::merge_control_dependencies(
   const control_depst &other_control_deps,
-  const control_dep_candidatest &other_control_dep_candidates)
+  const control_dep_candidatest &other_control_dep_candidates,
+  const control_dep_callst &other_control_dep_calls)
 {
   bool changed=false;
 
@@ -308,6 +313,16 @@ bool dep_graph_domaint::merge_control_dependencies(
 
   changed|=n!=control_dep_candidates.size();
 
+  // Merge call control dependencies
+
+  n=control_dep_calls.size();
+
+  control_dep_calls.insert(
+      other_control_dep_calls.begin(),
+      other_control_dep_calls.end());
+
+  changed|=n!=control_dep_calls.size();
+
   return changed;
 }
 
@@ -448,25 +463,6 @@ void dep_graph_domaint::transform(
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
   assert(dep_graph!=nullptr);
 
-  // We do not propagate control dependencies on function calls, i.e., only the
-  // entry point of a function should have a control dependency on the call
-  if(!control_deps.empty())
-  {
-    const goto_programt::const_targett &dep = control_deps.begin()->first;
-    if(dep->is_function_call())
-    {
-      INVARIANT(
-        std::all_of(
-          std::next(control_deps.begin()),
-          control_deps.end(),
-          [](const std::pair<const goto_programt::const_targett, tvt> &d)
-            { return d.first->is_function_call(); }),
-        "All entries must be function calls");
-
-      control_deps.clear();
-    }
-  }
-
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
@@ -492,13 +488,15 @@ void dep_graph_domaint::transform(
       // modify abstract state of return location
       if(s->merge_control_dependencies(
            control_deps,
-           control_dep_candidates))
+           control_dep_candidates,
+           control_dep_calls))
         s->has_changed=true;
 
       control_deps.clear();
-      control_deps.insert(std::make_pair(from, tvt::unknown()));
-
       control_dep_candidates.clear();
+
+      control_dep_calls.clear();
+      control_dep_calls.insert(from);
     }
   }
   else
@@ -512,7 +510,7 @@ void dep_graph_domaint::output(
   const ai_baset &ai,
   const namespacet &ns) const
 {
-  if(!control_deps.empty())
+  if(!control_deps.empty() || !control_dep_calls.empty())
   {
     out << "Control dependencies: ";
     for(control_depst::const_iterator
@@ -528,6 +526,18 @@ void dep_graph_domaint::output(
 
       out << cd->location_number << " [" << branch << "]";
     }
+
+    for(control_dep_callst::const_iterator
+        it=control_dep_calls.begin();
+        it!=control_dep_calls.end();
+        ++it)
+    {
+      if(!control_deps.empty() || it!=control_dep_calls.begin())
+        out << ",";
+
+      out << (*it)->location_number << " [CALL]";
+    }
+
     out << "\n";
   }
 
@@ -584,6 +594,17 @@ jsont dep_graph_domaint::output_json(
     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("CALL");
+  }
+
   for(const auto &dd : data_deps)
   {
     goto_programt::const_targett target=dd.first;
@@ -628,6 +649,17 @@ jsont dep_graph_domaint::output_json_additional(
     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("CALL");
+  }
+
   for(const auto &dd : base_state.data_deps)
   {
     goto_programt::const_targett target=dd.first;
@@ -704,6 +736,9 @@ void dep_graph_domaint::populate_dep_graph(
   for(const auto &c_dep : control_deps)
     dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep.first, this_loc);
 
+  for(const auto &c_dep : control_dep_calls)
+    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.first, this_loc);
 }

src/analyses/dependence_graph.h

@@ -121,6 +121,7 @@ class dep_graph_domaint:public ai_domain_baset
     has_changed=false;
     control_deps.clear();
     control_dep_candidates.clear();
+    control_dep_calls.clear();
     data_deps.clear();
   }
 
@@ -133,6 +134,7 @@ class dep_graph_domaint:public ai_domain_baset
     has_changed=false;
     control_deps.clear();
     control_dep_candidates.clear();
+    control_dep_calls.clear();
     data_deps.clear();
   }
 
@@ -147,7 +149,9 @@ class dep_graph_domaint:public ai_domain_baset
                    "node_id must be valid");
 
     DATA_INVARIANT(!has_values.is_true() ||
-                   (control_deps.empty() && data_deps.empty()),
+                   (control_deps.empty() &&
+                    control_dep_calls.empty() &&
+                    data_deps.empty()),
                    "If the domain is top, it must have no dependencies");
 
     return has_values.is_true();
@@ -159,7 +163,9 @@ class dep_graph_domaint:public ai_domain_baset
                    "node_id must be valid");
 
     DATA_INVARIANT(!has_values.is_false() ||
-                   (control_deps.empty() && data_deps.empty()),
+                   (control_deps.empty() &&
+                    control_dep_calls.empty() &&
+                    data_deps.empty()),
                    "If the domain is bottom, it must have no dependencies");
 
     return has_values.is_false();
@@ -190,6 +196,9 @@ class dep_graph_domaint:public ai_domain_baset
   typedef std::set<goto_programt::const_targett> control_dep_candidatest;
   control_dep_candidatest control_dep_candidates;
 
+  typedef std::set<goto_programt::const_targett> control_dep_callst;
+  control_dep_callst control_dep_calls;
+
   typedef std::map<goto_programt::const_targett, std::set<exprt>> data_depst;
   data_depst data_deps;
 
@@ -211,7 +220,8 @@ class dep_graph_domaint:public ai_domain_baset
 
   bool merge_control_dependencies(
     const control_depst &other_control_deps,
-    const control_dep_candidatest &other_control_dep_candidates);
+    const control_dep_candidatest &other_control_dep_candidates,
+    const control_dep_callst &other_control_dep_calls);
 };
 
 class dependence_grapht: