Track only immediate dependencies in variable sensitivity dependence graph.

Previously the variable sensitivity dependence graph would track both immediate
and transitive dependencies. Transitive dependencies are not needed and can be
calculated by other means. This change brings variable sensitivity dependence
graph into line with the behaviour of the old dependence graph code.

Author: chrisr-diffblue

regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc

@@ -7,6 +7,6 @@ EXIT=0
 SIGNAL=0
 st \(\) -> \{.a=.* @ \[2, 47\]\[Data dependencies: 47, 2\]\[Data dominators: \], .b=.* @ \[5, 47\]\[Data dependencies: 47, 5\]\[Data dominators: \]\} @ \[2, 5, 47\]\[Data dependencies: 47, 5, 2\]\[Data dominators: 47\]
 ar \(\) -> \{\[0\] = .* @ \[11, 42\]\[Data dependencies: 42, 11\]\[Data dominators: \]\n\[1\] = .* @ \[14, 42\]\[Data dependencies: 42, 14\]\[Data dominators: \]\n\} @ \[11, 14, 42\]\[Data dependencies: 42, 14, 11\]\[Data dominators: 42\]
-arr \(\) -> \{\[0\] = .* @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = .* @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = .* @ \[21, 23\]\[Data dependencies: 23, 21, 20\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 43, 23, 21, 20, 19\]\[Data dominators: 43\]
+arr \(\) -> \{\[0\] = .* @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = .* @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = .* @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 43\]
 --
 ^warning: ignoring

regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc

@@ -16,7 +16,7 @@ Data dependencies: 10 \[ar\[\(signed long int\)0\]\], 13 \[ar\[\(signed long int
 Data dependencies: 19 \[arr\[\(signed long int\)1\]\]
 Data dependencies: 18 \[arr\[\(signed long int\)0\]\]
 Data dependencies: 19 \[arr\[\(signed long int\)1\]\]
-Data dependencies: 19 \[arr\[\(signed long int\)2\]\], 20 \[arr\[\(signed long int\)2\]\], 22 \[arr\[\(signed long int\)2\]\]
+Data dependencies: 20 \[arr\[\(signed long int\)2\]\], 22 \[arr\[\(signed long int\)2\]\]
 Data dependencies: 1 \[st.a\], 53 \[st.a\], 57 \[st.a\]
 Data dependencies: 4 \[st.b\], 53 \[st.b\], 60 \[st.b\]
 Data dependencies: 1 \[st.a\], 4 \[st.b\], 53 \[st.a, st.b\], 57 \[st.a\], 60 \[st.b\]

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

@@ -9,15 +9,15 @@ SIGNAL=0
 ^Data dependencies: 4 \[st.b\], 53 \[st.b\]$
 ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 53 \[st.a, st.b\]$
 ^Data dependencies: 48 \[ar\[\(signed long int\)0\]\]$
-^Data dependencies: 1 \[out1\], 6 \[out1\], 53 \[out1\]$
+^Data dependencies: 6 \[out1\]$
 ^Data dependencies: 48 \[ar\[\(signed long int\)1\]\]$
 ^Data dependencies: 10 \[ar\[\(signed long int\)0\]\], 48 \[ar\[\(signed long int\)0\]\]$
 ^Data dependencies: 13 \[ar\[\(signed long int\)1\]\], 48 \[ar\[\(signed long int\)1\]\]$
 ^Data dependencies: 10 \[ar\[\(signed long int\)0\]\], 13 \[ar\[\(signed long int\)1\]\], 48 \[ar\[\(signed long int\)0\], ar\[\(signed long int\)1\]\]$
 ^Data dependencies: 19 \[arr\[\(signed long int\)1\]\]$
 ^Data dependencies: 18 \[arr\[\(signed long int\)0\]\]$
 ^Data dependencies: 19 \[arr\[\(signed long int\)1\]\]$
-^Data dependencies: 19 \[arr\[\(signed long int\)2\]\], 20 \[arr\[\(signed long int\)2\]\], 22 \[arr\[\(signed long int\)2\]\]$
+^Data dependencies: 20 \[arr\[\(signed long int\)2\]\], 22 \[arr\[\(signed long int\)2\]\]$
 ^Data dependencies: 1 \[st.a\], 53 \[st.a\], 57 \[st.a\]$
 ^Data dependencies: 4 \[st.b\], 53 \[st.b\], 60 \[st.b\]$
 ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 53 \[st.a, st.b\], 57 \[st.a\], 60 \[st.b\]$

src/analyses/variable-sensitivity/data_dependency_context.cpp

@@ -129,6 +129,35 @@ abstract_object_pointert data_dependency_contextt::insert_data_deps(
   return result;
 }
 
+/**
+ * Set the given set of data dependencies for this data_dependency_context
+ * object.
+ *
+ * \param dependencies the set of dependencies to set
+ * \return a new data_dependency_context if new dependencies were set,
+ * or 'this' if the dependencies were not changed.
+ */
+abstract_object_pointert data_dependency_contextt::set_data_deps(
+  const dependencest &dependencies) const
+{
+  // If the dependencies will not change, just return 'this'
+  if(data_deps == dependencies)
+    return shared_from_this();
+
+  const auto &result=
+    std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
+
+  result->data_deps = dependencies;
+
+  // If this is the first write to the context then it is also used as
+  // the initial set of data dependency dominators as well.
+  if(data_deps.empty())
+  {
+    result->data_dominators = dependencies;
+  }
+  return result;
+}
+
 /**
  * A helper function to evaluate writing to a component of an
  * abstract object. More precise abstractions may override this to
@@ -161,7 +190,7 @@ abstract_object_pointert data_dependency_contextt::write(
   const auto cast_value=
     std::dynamic_pointer_cast<const data_dependency_contextt>(value);
 
-  return updated_parent->insert_data_deps(cast_value->data_deps);
+  return updated_parent->set_data_deps(cast_value->data_deps);
 }
 
 /**
@@ -185,7 +214,7 @@ data_dependency_contextt::update_location_context(
       this->write_location_contextt::update_location_context(
         locations, update_sub_elements));
 
-  return updated_parent->insert_data_deps(locations);
+  return updated_parent->set_data_deps(locations);
 }
 
 /**

src/analyses/variable-sensitivity/data_dependency_context.h

@@ -97,17 +97,25 @@ class data_dependency_contextt:
   abstract_object_pointert insert_data_deps(
     const dependencest &dependencies) const;
 
+  abstract_object_pointert set_data_deps(
+    const dependencest &dependencies) const;
+
   abstract_object_pointert insert_data_deps(const locationst &locations) const
   {
     // `locationst` is unsorted, so convert this to a sorted `dependenciest`
-    dependencest dependencies;
-
-    for(const auto l : locations)
-      dependencies.insert(l);
+    dependencest dependencies(locations.begin(), locations.end());
 
     return insert_data_deps(dependencies);
   }
 
+  abstract_object_pointert set_data_deps(const locationst &locations) const
+  {
+    // `locationst` is unsorted, so convert this to a sorted `dependenciest`
+    dependencest dependencies(locations.begin(), locations.end());
+
+    return set_data_deps(dependencies);
+  }
+
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H