Merge pull request #5880 from jezhiggins/vsd-value-sets-and-constants

VSD - Cross-representation expression evaluation

Author: martin-cs

src/analyses/variable-sensitivity/abstract_object_set.cpp

@@ -7,6 +7,8 @@
 \*******************************************************************/
 
 #include <analyses/variable-sensitivity/abstract_object_set.h>
+#include <analyses/variable-sensitivity/interval_abstract_value.h>
+#include <util/interval.h>
 #include <util/string_utils.h>
 
 static bool by_length(const std::string &lhs, const std::string &rhs)
@@ -34,3 +36,19 @@ void abstract_object_sett::output(
 
   join_strings(out, output_values.begin(), output_values.end(), ", ");
 }
+
+abstract_object_pointert abstract_object_sett::to_interval()
+{
+  PRECONDITION(!values.empty());
+
+  exprt lower_expr = first()->to_constant();
+  exprt upper_expr = first()->to_constant();
+  for(const auto &value : values)
+  {
+    const auto &value_expr = value->to_constant();
+    lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
+    upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
+  }
+  return std::make_shared<interval_abstract_valuet>(
+    constant_interval_exprt(lower_expr, upper_expr));
+}

src/analyses/variable-sensitivity/abstract_object_set.h

@@ -38,6 +38,11 @@ class abstract_object_sett
   {
     values.insert(rhs.begin(), rhs.end());
   }
+  void insert(const value_ranget &rhs)
+  {
+    for(auto const &value : rhs)
+      insert(value);
+  }
 
   abstract_object_pointert first() const
   {
@@ -67,9 +72,19 @@ class abstract_object_sett
     return values == rhs.values;
   }
 
+  void clear()
+  {
+    values.clear();
+  }
+
   void
   output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
 
+  /// Cast the set of values \p other_values to an interval.
+  /// \param other_values: the value-set to be abstracted into an interval
+  /// \return the interval-abstract-object containing \p other_values
+  abstract_object_pointert to_interval();
+
 private:
   value_sett values;
 };