liveness fixes for three-way-merge

jezhiggins · jezhiggins · commit 1354ef328c20 · 2021-08-10T11:31:24.000+01:00
diff --git a/regression/goto-analyzer/liveness-function-call/main.c b/regression/goto-analyzer/liveness-function-call/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int globalX;
+
+void f00()
+{
+}
+
+int main()
+{
+  globalX = 1;
+
+  f00();
+
+  assert(globalX == 1);
+
+  globalX = 2;
+
+  f00();
+
+  assert(globalX == 2);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[30\]
+globalX .* 1 @ \[0\]
+globalX .* TOP @ \[33\]
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --three-way-merge --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[30\]
+globalX .* 1 @ \[0\]
+globalX .* TOP @ \[33\]
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --three-way-merge --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: UNKNOWN
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness.desc b/regression/goto-analyzer/liveness-function-call/test-liveness.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-liveness --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: UNKNOWN
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[30\]
+globalX .* 1 @ \[0\]
+globalX .* TOP @ \[0, 4\]
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --three-way-merge --show
+^EXIT=0$
+^SIGNAL=0$
+globalX .* 0 @ \[30\]
+globalX .* 1 @ \[0\]
+globalX .* 2 @ \[4\]
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --three-way-merge --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: SUCCESS
+--
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location.desc b/regression/goto-analyzer/liveness-function-call/test-write-location.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .* globalX == 1: SUCCESS
+\[main.assertion.2\] .* globalX == 2: UNKNOWN
+--
diff --git a/regression/goto-analyzer/liveness-struct/test-write-location.desc b/regression/goto-analyzer/liveness-struct/test-write-location.desc
@@ -1,9 +1,9 @@
 CORE
 main.c
---variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show
+--variable-sensitivity --vsd-structs every-field --vsd-values intervals --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\]
+^main::1::s .* \{.x=\[2, 3\] @ \[4, 6\], .y=\[3, 3\] @ \[2\]\} @ \[4, 6\]
 --
diff --git a/src/analyses/variable-sensitivity/liveness_context.cpp b/src/analyses/variable-sensitivity/liveness_context.cpp
@@ -8,9 +8,14 @@
 
 #include "liveness_context.h"
 
+bool liveness_contextt::has_location() const
+{
+  return assign_location.has_value();
+}
+
 abstract_objectt::locationt liveness_contextt::get_location() const
 {
-  return assign_location.has_value() ? assign_location.value() : locationt();
+  return assign_location.value();
 }
 
 /**
@@ -108,14 +113,21 @@ liveness_contextt::meet(const abstract_object_pointert &other) const
   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 region_context_ptrt &other,
+  const liveness_context_ptrt &other,
   combine_fn fn) const
 {
   auto combined_child = fn(child_abstract_object, other->child_abstract_object);
-  auto location_match = get_location() == other->get_location();
+  auto location_match = at_same_location(other);
 
-  if(combined_child.modified || location_match)
+  if(combined_child.modified || !location_match)
   {
     const auto &result =
       std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
@@ -127,6 +139,25 @@ abstract_object_pointert liveness_contextt::combine(
   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();
+}
+
 void liveness_contextt::reset_location()
 {
   assign_location.reset();
@@ -161,8 +192,8 @@ void liveness_contextt::output(
 {
   context_abstract_objectt::output(out, ai, ns);
 
-  if(assign_location.has_value())
-    out << " @ [" << assign_location.value()->location_number << "]";
+  if(has_location())
+    out << " @ [" << get_location()->location_number << "]";
   else
     out << " @ [undefined]";
 }
@@ -202,7 +233,7 @@ bool liveness_contextt::has_been_modified(
   // 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 before_context->get_location() != get_location();
+  return !at_same_location(before_context);
 }
 
 abstract_object_pointert
diff --git a/src/analyses/variable-sensitivity/liveness_context.h b/src/analyses/variable-sensitivity/liveness_context.h
@@ -79,6 +79,9 @@ class liveness_contextt : public context_abstract_objectt
   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;
+
   abstract_object_pointert write(
     abstract_environmentt &environment,
     const namespacet &ns,
@@ -94,16 +97,19 @@ class liveness_contextt : public context_abstract_objectt
   using combine_fn = std::function<abstract_objectt::combine_result(
     const abstract_object_pointert &op1,
     const abstract_object_pointert &op2)>;
-  using region_context_ptrt = std::shared_ptr<const liveness_contextt>;
+  using liveness_context_ptrt = std::shared_ptr<const liveness_contextt>;
 
   abstract_object_pointert
-  combine(const region_context_ptrt &other, combine_fn fn) const;
+  combine(const liveness_context_ptrt &other, combine_fn fn) 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);
 };
 
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h
@@ -79,26 +79,31 @@
   "(vsd-unions):"                                                              \
   "(vsd-flow-insensitive)"                                                     \
   "(vsd-data-dependencies)"                                                    \
-  "(vsd-liveness)"
-// clang-format off
-#define HELP_VSD \
-    " --vsd-values                 value tracking - constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */ \
-    " --vsd-structs                struct field sensitive analysis - top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */ \
-    " --vsd-arrays                 array entry sensitive analysis - top-bottom|every-element\n" /* NOLINT(whitespace/line_length) */ \
-    " --vsd-pointers               pointer sensitive analysis - top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */ \
-    " --vsd-unions                 union sensitive analysis - top-bottom\n" \
-    " --vsd-flow-insensitive       disables flow sensitivity\n" \
-    " --vsd-data-dependencies      track data dependencies\n" \
-    " --vsd-liveness               track variable liveness\n" \
+  "(vsd-liveness)"                                                             \
+                                                                               \
+    // clang-format off
+#define HELP_VSD                                                               \
+  " --vsd-values                 value tracking - "                            \
+  "constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */ \
+  " --vsd-structs                struct field sensitive analysis - "           \
+  "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */              \
+  " --vsd-arrays                 array entry sensitive analysis - "            \
+  "top-bottom|every-element\n" /* NOLINT(whitespace/line_length) */            \
+  " --vsd-pointers               pointer sensitive analysis - "                \
+  "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */      \
+  " --vsd-unions                 union sensitive analysis - top-bottom\n"      \
+  " --vsd-flow-insensitive       disables flow sensitivity\n"                  \
+  " --vsd-data-dependencies      track data dependencies\n"                    \
+  " --vsd-liveness               track variable liveness\n"                    \
 
 // cland-format on
 
-#define PARSE_OPTIONS_VSD(cmdline, options) \
-  options.set_option("values", cmdline.get_value("vsd-values")); \
-  options.set_option("pointers", cmdline.get_value("vsd-pointers")); \
-  options.set_option("arrays", cmdline.get_value("vsd-arrays")); \
-  options.set_option("structs", cmdline.get_value("vsd-structs")); \
-  options.set_option("unions", cmdline.get_value("vsd-unions")); \
+#define PARSE_OPTIONS_VSD(cmdline, options)                                    \
+  options.set_option("values", cmdline.get_value("vsd-values"));               \
+  options.set_option("pointers", cmdline.get_value("vsd-pointers"));           \
+  options.set_option("arrays", cmdline.get_value("vsd-arrays"));               \
+  options.set_option("structs", cmdline.get_value("vsd-structs"));             \
+  options.set_option("unions", cmdline.get_value("vsd-unions"));               \
   options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
