Merge pull request diffblue#273 from diffblue/vsb-dependence-graph-immediate-deps

Variable sensitivity dependence graph - track only immediate data dependencies

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