Rework liveness_contextt on top of write_location_contextt

Maintains existing three-way-merge behaviour, which otherwise was lost
because we'd discarded too much context information to be able to merge
precisely.

Author: jezhiggins

regression/goto-analyzer/liveness-function-call/main.c

@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int globalX;
 
 void f00()
@@ -21,4 +19,4 @@ int main()
   assert(globalX == 2);
 
   return 0;
-}
+}

regression/goto-analyzer/liveness-function-call/test-liveness-show.desc

@@ -3,7 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[30\]
+globalX .* 0 @ \[28\]
 globalX .* 1 @ \[0\]
-globalX .* TOP @ \[33\]
+globalX .* 2 @ \[3\]
+globalX .* TOP @ \[31\]
 --

regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc

@@ -3,7 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[30\]
+globalX .* 0 @ \[28\]
 globalX .* 1 @ \[0\]
-globalX .* TOP @ \[33\]
+globalX .* 2 @ \[3\]
+globalX .* TOP @ \[31\]
 --

regression/goto-analyzer/liveness-function-call/test-liveness-three-way.desc

@@ -4,5 +4,5 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] .* globalX == 1: SUCCESS
-\[main.assertion.2\] .* globalX == 2: UNKNOWN
+\[main.assertion.2\] .* globalX == 2: SUCCESS
 --

regression/goto-analyzer/liveness-function-call/test-write-location-show.desc

@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[30\]
+globalX .* 0 @ \[28\]
 globalX .* 1 @ \[0\]
-globalX .* TOP @ \[0, 4\]
+globalX .* TOP @ \[0, 3\]
 --

regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc

@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[30\]
+globalX .* 0 @ \[28\]
 globalX .* 1 @ \[0\]
-globalX .* 2 @ \[4\]
+globalX .* 2 @ \[3\]
 --

src/analyses/variable-sensitivity/liveness_context.cpp

@@ -42,21 +42,15 @@ abstract_object_pointert liveness_contextt::write(
   const abstract_object_pointert &value,
   bool merging_write) const
 {
-  abstract_object_pointert updated_child = child_abstract_object->write(
-    environment, ns, stack, specifier, value, merging_write);
-
-  // Only perform an update if the write to the child has in fact changed it...
-  if(updated_child == child_abstract_object)
+  auto updated = std::dynamic_pointer_cast<const liveness_contextt>(
+    write_location_contextt::write(
+      environment, ns, stack, specifier, value, merging_write));
+  if(updated == shared_from_this())
     return shared_from_this();
 
-  // Need to ensure the result of the write is still wrapped in a dependency
-  // context
-  const auto &result =
-    std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
-
-  result->set_child(updated_child);
-
-  // Update the child and record the updated write locations
+  // record the updated write locations
+  auto result =
+    std::dynamic_pointer_cast<liveness_contextt>(updated->mutable_clone());
   auto value_context =
     std::dynamic_pointer_cast<const liveness_contextt>(value);
   if(value_context)
@@ -83,91 +77,40 @@ abstract_object_pointert liveness_contextt::merge(
 
   if(cast_other)
   {
-    auto merge_fn = [&widen_mode](
-                      const abstract_object_pointert &op1,
-                      const abstract_object_pointert &op2) {
-      return abstract_objectt::merge(op1, op2, widen_mode);
-    };
-    return combine(cast_other, merge_fn);
+    auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
+      write_location_contextt::merge(other, widen_mode));
+    return reset_location_on_merge(merged);
   }
 
   return abstract_objectt::merge(other, widen_mode);
 }
 
-// need wrapper function here to disambiguate meet overload
-abstract_objectt::combine_result object_meet(
-  const abstract_object_pointert &op1,
-  const abstract_object_pointert &op2)
-{
-  return abstract_objectt::meet(op1, op2);
-}
-
-abstract_object_pointert
-liveness_contextt::meet(const abstract_object_pointert &other) const
-{
-  auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
-
-  if(cast_other)
-    return combine(cast_other, object_meet);
-
-  return abstract_objectt::meet(other);
-}
-
-bool liveness_contextt::at_same_location(const liveness_context_ptrt &rhs) const
-{
-  return has_location() && rhs->has_location() &&
-         (get_location()->location_number ==
-          rhs->get_location()->location_number);
-}
-
-abstract_object_pointert liveness_contextt::combine(
-  const liveness_context_ptrt &other,
-  combine_fn fn) const
-{
-  auto combined_child = fn(child_abstract_object, other->child_abstract_object);
-  auto location_match = at_same_location(other);
-
-  if(combined_child.modified || !location_match)
-  {
-    const auto &result =
-      std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
-    result->set_child(combined_child.object);
-    result->reset_location();
-    return result;
-  }
-
-  return shared_from_this();
-}
-
 abstract_object_pointert liveness_contextt::abstract_object_merge_internal(
   const abstract_object_pointert &other) const
 {
-  auto other_context =
-    std::dynamic_pointer_cast<const liveness_contextt>(other);
-
-  if(!other_context)
-    return shared_from_this();
-
-  if(other_context && !at_same_location(other_context))
-  {
-    auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
-    result->reset_location();
-    return result;
-  }
-
-  return shared_from_this();
+  auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
+    write_location_contextt::abstract_object_merge_internal(other));
+  return reset_location_on_merge(merged);
 }
 
-void liveness_contextt::reset_location()
+abstract_object_pointert liveness_contextt::reset_location_on_merge(
+  const liveness_context_ptrt &merged) const
 {
-  assign_location.reset();
+  if(merged == shared_from_this())
+    return shared_from_this();
+
+  auto updated =
+    std::dynamic_pointer_cast<liveness_contextt>(merged->mutable_clone());
+  updated->assign_location.reset();
+  return updated;
 }
 
 context_abstract_objectt::context_abstract_object_ptrt
 liveness_contextt::update_location_context_internal(
   const locationst &locations) const
 {
   auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
+  result->set_last_written_locations(locations);
   result->set_location(*locations.cbegin());
   return result;
 }
@@ -198,44 +141,6 @@ void liveness_contextt::output(
     out << " @ [undefined]";
 }
 
-/**
- * Determine whether 'this' abstract_object has been modified in comparison
- * to a previous 'before' state.
- *
- * \param before the abstract_object_pointert to use as a reference to
- * compare against
- *
- * \return true if 'this' is considered to have been modified in comparison
- * to 'before', false otherwise.
- */
-bool liveness_contextt::has_been_modified(
-  const abstract_object_pointert &before) const
-{
-  if(this == before.get())
-    return false;
-
-  auto before_context =
-    std::dynamic_pointer_cast<const liveness_contextt>(before);
-
-  if(!before_context)
-  {
-    // The other context is not something we understand, so must assume
-    // that the abstract_object has been modified
-    return true;
-  }
-
-  // Even if the pointers are different, it maybe that it has changed only
-  // because of a merge operation, rather than an actual write. Given that
-  // this class has knowledge of where writes have occured, use that
-  // information to determine if any writes have happened and use that as the
-  // proxy for whether the value has changed or not.
-  //
-  // For two sets of last written locations to match,
-  // each location in one set must be equal to precisely one location
-  // in the other, since a set can assume at most one match
-  return !at_same_location(before_context);
-}
-
 abstract_object_pointert
 liveness_contextt::merge_location_context(const locationt &location) const
 {

src/analyses/variable-sensitivity/liveness_context.h

@@ -15,7 +15,7 @@
 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
 
-#include <analyses/variable-sensitivity/context_abstract_object.h>
+#include <analyses/variable-sensitivity/write_location_context.h>
 #include <iostream>
 #include <stack>
 
@@ -30,13 +30,13 @@
  * of this, 'context_abstract_objectt<T>' which provides the same
  * constructors as the standard 'abstract_objectt' class.
  */
-class liveness_contextt : public context_abstract_objectt
+class liveness_contextt : public write_location_contextt
 {
 public:
   explicit liveness_contextt(
     const abstract_object_pointert child,
     const typet &type)
-    : context_abstract_objectt(child, type)
+    : write_location_contextt(child, type)
   {
   }
 
@@ -45,7 +45,7 @@ class liveness_contextt : public context_abstract_objectt
     const typet &type,
     bool top,
     bool bottom)
-    : context_abstract_objectt(child, type, top, bottom)
+    : write_location_contextt(child, type, top, bottom)
   {
   }
 
@@ -54,16 +54,10 @@ class liveness_contextt : public context_abstract_objectt
     const exprt &expr,
     const abstract_environmentt &environment,
     const namespacet &ns)
-    : context_abstract_objectt(child, expr, environment, ns)
+    : write_location_contextt(child, expr, environment, ns)
   {
   }
 
-  virtual ~liveness_contextt()
-  {
-  }
-
-  bool has_been_modified(const abstract_object_pointert &before) const override;
-
   abstract_object_pointert
   merge_location_context(const locationt &location) const override;
 
@@ -76,8 +70,6 @@ class liveness_contextt : public context_abstract_objectt
   abstract_object_pointert merge(
     const abstract_object_pointert &other,
     const widen_modet &widen_mode) const override;
-  abstract_object_pointert
-  meet(const abstract_object_pointert &other) const override;
 
   abstract_object_pointert abstract_object_merge_internal(
     const abstract_object_pointert &other) const override;
@@ -91,24 +83,19 @@ class liveness_contextt : public context_abstract_objectt
     bool merging_write) const override;
 
   locationt get_location() const;
-  void reset_location();
 
 private:
-  using combine_fn = std::function<abstract_objectt::combine_result(
-    const abstract_object_pointert &op1,
-    const abstract_object_pointert &op2)>;
   using liveness_context_ptrt = std::shared_ptr<const liveness_contextt>;
 
   abstract_object_pointert
-  combine(const liveness_context_ptrt &other, combine_fn fn) const;
+  reset_location_on_merge(const liveness_context_ptrt &merged) const;
 
   optionalt<locationt> assign_location;
 
   context_abstract_object_ptrt
   update_location_context_internal(const locationst &locations) const override;
 
   bool has_location() const;
-  bool at_same_location(const liveness_context_ptrt &rhs) const;
 
   void set_location(const locationt &location);
 };