Change region_contextt to liveness_contextt

Author: jezhiggins

regression/goto-analyzer/region-tracking/main.c renamed to regression/goto-analyzer/liveness/main.c

@@ -1,6 +1,6 @@
 CORE
 main.c
---variable-sensitivity --vsd-values set-of-constants --vsd-region-tracking --show
+--variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show
 ^EXIT=0$
 ^SIGNAL=0$
 ^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\]

regression/goto-analyzer/region-tracking/test-region-tracking.desc renamed to regression/goto-analyzer/liveness/test-liveness.desc

@@ -45,7 +45,7 @@ SRC = ai.cpp \
       variable-sensitivity/full_array_abstract_object.cpp \
       variable-sensitivity/full_struct_abstract_object.cpp \
       variable-sensitivity/interval_abstract_value.cpp \
-      variable-sensitivity/region_context.cpp \
+      variable-sensitivity/liveness_context.cpp \
       variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/two_value_pointer_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \

regression/goto-analyzer/region-tracking/test-write-location.desc renamed to regression/goto-analyzer/liveness/test-write-location.desc

@@ -6,9 +6,9 @@
 
 \*******************************************************************/
 
-#include "region_context.h"
+#include "liveness_context.h"
 
-abstract_objectt::locationt region_contextt::get_location() const
+abstract_objectt::locationt liveness_contextt::get_location() const
 {
   return *assign_location;
 }
@@ -29,7 +29,7 @@ abstract_objectt::locationt region_contextt::get_location() const
  * \return the abstract_objectt representing the result of writing
  * to a specific component.
  */
-abstract_object_pointert region_contextt::write(
+abstract_object_pointert liveness_contextt::write(
   abstract_environmentt &environment,
   const namespacet &ns,
   const std::stack<exprt> &stack,
@@ -47,12 +47,13 @@ abstract_object_pointert region_contextt::write(
   // Need to ensure the result of the write is still wrapped in a dependency
   // context
   const auto &result =
-    std::dynamic_pointer_cast<region_contextt>(mutable_clone());
+    std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
 
   result->set_child(updated_child);
 
   // Update the child and record the updated write locations
-  auto value_context = std::dynamic_pointer_cast<const region_contextt>(value);
+  auto value_context =
+    std::dynamic_pointer_cast<const liveness_contextt>(value);
   if(value_context)
     result->set_location(value_context->get_location());
 
@@ -69,11 +70,11 @@ abstract_object_pointert region_contextt::write(
  * \return the result of the merge, or 'this' if the merge would not change
  * the current abstract object
  */
-abstract_object_pointert region_contextt::merge(
+abstract_object_pointert liveness_contextt::merge(
   const abstract_object_pointert &other,
   const widen_modet &widen_mode) const
 {
-  auto cast_other = std::dynamic_pointer_cast<const region_contextt>(other);
+  auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
 
   if(cast_other)
   {
@@ -97,26 +98,27 @@ abstract_objectt::combine_result object_meet(
 }
 
 abstract_object_pointert
-region_contextt::meet(const abstract_object_pointert &other) const
+liveness_contextt::meet(const abstract_object_pointert &other) const
 {
-  auto cast_other = std::dynamic_pointer_cast<const region_contextt>(other);
+  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);
 }
 
-abstract_object_pointert
-region_contextt::combine(const region_context_ptrt &other, combine_fn fn) const
+abstract_object_pointert liveness_contextt::combine(
+  const region_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();
 
   if(combined_child.modified || location_match)
   {
     const auto &result =
-      std::dynamic_pointer_cast<region_contextt>(mutable_clone());
+      std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
     result->set_child(combined_child.object);
     result->reset_location();
     return result;
@@ -125,21 +127,21 @@ region_contextt::combine(const region_context_ptrt &other, combine_fn fn) const
   return shared_from_this();
 }
 
-void region_contextt::reset_location()
+void liveness_contextt::reset_location()
 {
   assign_location.reset();
 }
 
 context_abstract_objectt::context_abstract_object_ptrt
-region_contextt::update_location_context_internal(
+liveness_contextt::update_location_context_internal(
   const locationst &locations) const
 {
-  auto result = std::dynamic_pointer_cast<region_contextt>(mutable_clone());
+  auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
   result->set_location(*locations.cbegin());
   return result;
 }
 
-void region_contextt::set_location(const locationt &location)
+void liveness_contextt::set_location(const locationt &location)
 {
   assign_location.emplace(location);
 }
@@ -152,7 +154,7 @@ void region_contextt::set_location(const locationt &location)
  * (that contains the object ... )
  * \param ns the current namespace
  */
-void region_contextt::output(
+void liveness_contextt::output(
   std::ostream &out,
   const ai_baset &ai,
   const namespacet &ns) const
@@ -175,14 +177,14 @@ void region_contextt::output(
  * \return true if 'this' is considered to have been modified in comparison
  * to 'before', false otherwise.
  */
-bool region_contextt::has_been_modified(
+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 region_contextt>(before);
+    std::dynamic_pointer_cast<const liveness_contextt>(before);
 
   if(!before_context)
   {
@@ -204,12 +206,12 @@ bool region_contextt::has_been_modified(
 }
 
 abstract_object_pointert
-region_contextt::merge_location_context(const locationt &location) const
+liveness_contextt::merge_location_context(const locationt &location) const
 {
   if(assign_location.has_value())
     return shared_from_this();
 
-  auto update = std::dynamic_pointer_cast<region_contextt>(mutable_clone());
+  auto update = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
   update->assign_location = location;
   return update;
 }

src/analyses/Makefile

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
- Module: analyses variable-sensitivity region_context
+ Module: analyses variable-sensitivity liveness_contextt
 
  Author: Jez Higgins
 
@@ -9,11 +9,11 @@
 /**
  * \file
  *  Maintain a context in the variable sensitvity domain that records
- *  the assignment region for a given abstract_objectt.
+ *  the liveness region for a given abstract_objectt.
  */
 
-#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_REGION_CONTEXT_H
-#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_REGION_CONTEXT_H
+#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 <iostream>
@@ -30,17 +30,17 @@
  * of this, 'context_abstract_objectt<T>' which provides the same
  * constructors as the standard 'abstract_objectt' class.
  */
-class region_contextt : public context_abstract_objectt
+class liveness_contextt : public context_abstract_objectt
 {
 public:
-  explicit region_contextt(
+  explicit liveness_contextt(
     const abstract_object_pointert child,
     const typet &type)
     : context_abstract_objectt(child, type)
   {
   }
 
-  region_contextt(
+  liveness_contextt(
     const abstract_object_pointert child,
     const typet &type,
     bool top,
@@ -49,7 +49,7 @@ class region_contextt : public context_abstract_objectt
   {
   }
 
-  explicit region_contextt(
+  explicit liveness_contextt(
     const abstract_object_pointert child,
     const exprt &expr,
     const abstract_environmentt &environment,
@@ -58,7 +58,7 @@ class region_contextt : public context_abstract_objectt
   {
   }
 
-  virtual ~region_contextt()
+  virtual ~liveness_contextt()
   {
   }
 
@@ -94,7 +94,7 @@ class region_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 region_contextt>;
+  using region_context_ptrt = std::shared_ptr<const liveness_contextt>;
 
   abstract_object_pointert
   combine(const region_context_ptrt &other, combine_fn fn) const;
@@ -107,4 +107,4 @@ class region_contextt : public context_abstract_objectt
   void set_location(const locationt &location);
 };
 
-#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_REGION_CONTEXT_H
+#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H

src/analyses/variable-sensitivity/region_context.cpp renamed to src/analyses/variable-sensitivity/liveness_context.cpp

@@ -35,8 +35,7 @@ vsd_configt vsd_configt::from_options(const optionst &options)
   config.context_tracking.last_write_context = true;
   config.context_tracking.data_dependency_context =
     options.get_bool_option("data-dependencies");
-  config.context_tracking.region_context =
-    options.get_bool_option("region-tracking");
+  config.context_tracking.liveness = options.get_bool_option("liveness");
 
   config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
                               ? flow_sensitivityt::insensitive

src/analyses/variable-sensitivity/region_context.h renamed to src/analyses/variable-sensitivity/liveness_context.h

@@ -53,7 +53,7 @@ struct vsd_configt
 
   struct
   {
-    bool region_context;
+    bool liveness;
     bool data_dependency_context;
     bool last_write_context;
   } context_tracking;

src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp

@@ -79,7 +79,7 @@
   "(vsd-unions):"                                                              \
   "(vsd-flow-insensitive)"                                                     \
   "(vsd-data-dependencies)"                                                    \
-  "(vsd-region-tracking)"
+  "(vsd-liveness)"
 // clang-format off
 #define HELP_VSD \
     " --vsd-values                 value tracking - constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */ \
@@ -89,7 +89,7 @@
     " --vsd-unions                 union sensitive analysis - top-bottom\n" \
     " --vsd-flow-insensitive       disables flow sensitivity\n" \
     " --vsd-data-dependencies      track data dependencies\n" \
-    " --vsd-region-tracking        track SSA regions\n" \
+    " --vsd-liveness               track variable liveness\n" \
 
 // cland-format on
 
@@ -101,7 +101,7 @@
   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("region-tracking", cmdline.isset("vsd-region-tracking")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
   (void)0
 
 class variable_sensitivity_domaint : public ai_domain_baset

src/analyses/variable-sensitivity/variable_sensitivity_configuration.h

@@ -7,7 +7,7 @@
 \*******************************************************************/
 #include "variable_sensitivity_object_factory.h"
 #include "full_array_abstract_object.h"
-#include "region_context.h"
+#include "liveness_context.h"
 #include "value_set_pointer_abstract_object.h"
 
 template <class context_classt>
@@ -38,8 +38,8 @@ abstract_object_pointert wrap_with_context_object(
   const abstract_object_pointert &abstract_object,
   const vsd_configt &configuration)
 {
-  if(configuration.context_tracking.region_context)
-    return create_context_abstract_object<region_contextt>(abstract_object);
+  if(configuration.context_tracking.liveness)
+    return create_context_abstract_object<liveness_contextt>(abstract_object);
 
   if(configuration.context_tracking.data_dependency_context)
     return create_context_abstract_object<data_dependency_contextt>(