Propagate merge location context down to struct members

Author: jezhiggins

regression/goto-analyzer/liveness-struct/main.c

@@ -0,0 +1,16 @@
+struct S
+{
+  int x;
+  int y;
+};
+
+int main()
+{
+  int non_det;
+  struct S s = {1, 3};
+
+  if(non_det)
+    s.x = 2;
+  else
+    s.x = 3;
+}

regression/goto-analyzer/liveness-struct/test-liveness.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::s .* \{\} @ \[1\]
+^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\]
+^main::1::s .* \{.x=\[2, 3\] @ \[7\], .y=\[3, 3\] @ \[2\]\} @ \[7\]
+--

regression/goto-analyzer/liveness-struct/test-write-location.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::s .* \{\} @ \[1\]
+^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\]
+^main::1::s .* \{.x=\[2, 3\] @ \[7\], .y=\[3, 3\] @ \[2\]\} @ \[7\]
+--

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -110,8 +110,8 @@ abstract_object_pointert context_abstract_objectt::write_location_context(
 {
   auto result = update_location_context_internal({location});
 
-  auto visited_child = child_abstract_object->write_location_context(location);
-  result->set_child(visited_child);
+  auto updated_child = child_abstract_object->write_location_context(location);
+  result->set_child(updated_child);
 
   return result;
 }

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -284,6 +284,12 @@ abstract_object_pointert full_struct_abstract_objectt::write_location_context(
   return visit_sub_elements(location_update_visitort(location));
 }
 
+abstract_object_pointert full_struct_abstract_objectt::merge_location_context(
+  const locationt &location) const
+{
+  return visit_sub_elements(merge_location_update_visitort(location));
+}
+
 abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
   const abstract_object_visitort &visitor) const
 {

src/analyses/variable-sensitivity/full_struct_abstract_object.h

@@ -76,6 +76,8 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
    */
   abstract_object_pointert
   write_location_context(const locationt &location) const override;
+  abstract_object_pointert
+  merge_location_context(const locationt &location) const override;
 
   /**
    * Apply a visitor operation to all sub elements of this abstract_object.

src/analyses/variable-sensitivity/liveness_context.cpp

@@ -213,5 +213,8 @@ liveness_contextt::merge_location_context(const locationt &location) const
 
   auto update = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
   update->assign_location = location;
+  auto updated_child = child_abstract_object->merge_location_context(location);
+  update->set_child(updated_child);
+
   return update;
 }

src/analyses/variable-sensitivity/location_update_visitor.h

@@ -30,4 +30,24 @@ class location_update_visitort
   const abstract_objectt::locationt &location;
 };
 
+class merge_location_update_visitort
+  : public abstract_objectt::abstract_object_visitort
+{
+public:
+  explicit merge_location_update_visitort(
+    const abstract_objectt::locationt &location)
+    : location(location)
+  {
+  }
+
+  abstract_object_pointert
+  visit(const abstract_object_pointert &element) const override
+  {
+    return element->merge_location_context(location);
+  }
+
+private:
+  const abstract_objectt::locationt &location;
+};
+
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LOCATION_UPDATE_VISITOR_H