Merge pull request #6267 from jezhiggins/vsd-to-predicate

VSD - to predicate

Author: martin-cs

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -408,22 +408,41 @@ void abstract_environmentt::output(
 {
   out << "{\n";
 
-  decltype(map)::viewt view;
-  map.get_view(view);
-  for(const auto &entry : view)
+  for(const auto &entry : map.get_view())
   {
     out << entry.first << " () -> ";
     entry.second->output(out, ai, ns);
     out << "\n";
   }
+
   out << "}\n";
 }
 
+exprt abstract_environmentt::to_predicate() const
+{
+  if(is_bottom())
+    return false_exprt();
+  if(is_top())
+    return true_exprt();
+
+  auto predicates = std::vector<exprt>{};
+  for(const auto &entry : map.get_view())
+  {
+    auto sym = entry.first;
+    auto val = entry.second;
+    auto pred = val->to_predicate(symbol_exprt(sym, val->type()));
+
+    predicates.push_back(pred);
+  }
+
+  if(predicates.size() == 1)
+    return predicates.front();
+  return and_exprt(predicates);
+}
+
 bool abstract_environmentt::verify() const
 {
-  decltype(map)::viewt view;
-  map.get_view(view);
-  for(const auto &entry : view)
+  for(const auto &entry : map.get_view())
   {
     if(entry.second == nullptr)
     {
@@ -460,9 +479,7 @@ abstract_environmentt::modified_symbols(
 {
   // Find all symbols who have different write locations in each map
   std::vector<abstract_environmentt::map_keyt> symbols_diff;
-  decltype(first.map)::viewt view;
-  first.map.get_view(view);
-  for(const auto &entry : view)
+  for(const auto &entry : first.map.get_view())
   {
     const auto &second_entry = second.map.find(entry.first);
     if(second_entry.has_value())
@@ -505,10 +522,8 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const
 {
   abstract_object_statisticst statistics = {};
   statistics.number_of_globals = count_globals(ns);
-  decltype(map)::viewt view;
-  map.get_view(view);
   abstract_object_visitedt visited;
-  for(auto const &object : view)
+  for(auto const &object : map.get_view())
   {
     if(visited.find(object.second) == visited.end())
     {

src/analyses/variable-sensitivity/abstract_environment.h

@@ -224,6 +224,12 @@ class abstract_environmentt
   void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
     const;
 
+  /// Gives a boolean condition that is true for all values represented by the
+  /// environment.
+  ///
+  /// \return An exprt describing the environment
+  exprt to_predicate() const;
+
   /// Check the structural invariants are maintained.
   /// In this case this is checking there aren't any null pointer mapped values
   bool verify() const;

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -172,6 +172,21 @@ exprt abstract_objectt::to_constant() const
   return nil_exprt();
 }
 
+exprt abstract_objectt::to_predicate(const exprt &name) const
+{
+  if(is_top())
+    return true_exprt();
+  if(is_bottom())
+    return false_exprt();
+  return to_predicate_internal(name);
+}
+
+exprt abstract_objectt::to_predicate_internal(const exprt &name) const
+{
+  UNREACHABLE;
+  return nil_exprt();
+}
+
 void abstract_objectt::output(
   std::ostream &out,
   const ai_baset &ai,

src/analyses/variable-sensitivity/abstract_object.h

@@ -171,6 +171,17 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   /// that allows an object to be built from a value.
   virtual exprt to_constant() const;
 
+  /// Converts to an invariant expression
+  ///
+  /// \param name - the variable name to substitute into the expression
+  /// \return Returns an exprt representing the object as an invariant.
+  ///
+  /// The the abstract element represents a single value the expression will
+  /// have the form _name = value_, if the value is an interval it will have the
+  /// the form _lower <= name <= upper_, etc.
+  /// If the value is bottom returns false, if top returns true.
+  exprt to_predicate(const exprt &name) const;
+
   /**
    * A helper function to evaluate writing to a component of an
    * abstract object. More precise abstractions may override this to
@@ -352,6 +363,11 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
     return shared_from_this() == other;
   }
 
+  /// to_predicate implementation - derived classes will override
+  /// \param name - the variable name to substitute into the expression
+  /// \return Returns an exprt representing the object as an invariant.
+  virtual exprt to_predicate_internal(const exprt &name) const;
+
 private:
   /// To enforce copy-on-write these are private and have read-only accessors
   typet t;

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -144,6 +144,11 @@ abstract_value_pointert constant_abstract_valuet::constrain(
   return as_value(mutable_clone());
 }
 
+exprt constant_abstract_valuet::to_predicate_internal(const exprt &name) const
+{
+  return equal_exprt(name, value);
+}
+
 void constant_abstract_valuet::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -81,6 +81,8 @@ class constant_abstract_valuet : public abstract_value_objectt
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   exprt value;
 };

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -388,3 +388,9 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr(
     return true_exprt();
   return nil_exprt();
 }
+
+exprt constant_pointer_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  return equal_exprt(name, value_stack.to_expression());
+}

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -145,6 +145,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
 
   CLONE
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   bool same_target(abstract_object_pointert other) const;
   exprt offset() const;

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -160,6 +160,11 @@ abstract_object_pointert context_abstract_objectt::unwrap_context() const
   return child_abstract_object->unwrap_context();
 }
 
+exprt context_abstract_objectt::to_predicate_internal(const exprt &name) const
+{
+  return child_abstract_object->to_predicate(name);
+}
+
 void context_abstract_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/context_abstract_object.h

@@ -117,6 +117,8 @@ class context_abstract_objectt : public abstract_objectt
     bool merging_write) const override;
 
   bool has_been_modified(const abstract_object_pointert &before) const override;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -10,6 +10,7 @@
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <util/arith_tools.h>
+#include <util/mathematical_types.h>
 #include <util/std_expr.h>
 
 #include "abstract_value_object.h"
@@ -401,6 +402,28 @@ abstract_object_pointert full_array_abstract_objectt::visit_sub_elements(
   }
 }
 
+exprt full_array_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  auto all_predicates = exprt::operandst{};
+
+  for(auto field : map.get_sorted_view())
+  {
+    auto ii = from_integer(field.first.to_long(), integer_typet());
+    auto index = index_exprt(name, ii);
+    auto field_expr = field.second->to_predicate(index);
+
+    if(!field_expr.is_true())
+      all_predicates.push_back(field_expr);
+  }
+
+  if(all_predicates.empty())
+    return true_exprt();
+  if(all_predicates.size() == 1)
+    return all_predicates.front();
+  return and_exprt(all_predicates);
+}
+
 void full_array_abstract_objectt::statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/full_array_abstract_object.h

@@ -212,6 +212,8 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
   abstract_object_pointert full_array_merge(
     const full_array_pointert &other,
     const widen_modet &widen_mode) const;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -307,6 +307,27 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
   }
 }
 
+exprt full_struct_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  auto all_predicates = exprt::operandst{};
+
+  for(auto field : map.get_sorted_view())
+  {
+    auto field_name = member_exprt(name, field.first, name.type());
+    auto field_expr = field.second->to_predicate(field_name);
+
+    if(!field_expr.is_true())
+      all_predicates.push_back(field_expr);
+  }
+
+  if(all_predicates.empty())
+    return true_exprt();
+  if(all_predicates.size() == 1)
+    return all_predicates.front();
+  return and_exprt(all_predicates);
+}
+
 void full_struct_abstract_objectt::statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/full_struct_abstract_object.h

@@ -169,6 +169,8 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
   abstract_object_pointert merge(
     const abstract_object_pointert &other,
     const widen_modet &widen_mode) const override;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -463,6 +463,17 @@ abstract_value_pointert interval_abstract_valuet::constrain(
     make_interval(constant_interval_exprt(lower_bound, upper_bound)));
 }
 
+exprt interval_abstract_valuet::to_predicate_internal(const exprt &name) const
+{
+  if(interval.is_single_value_interval())
+    return equal_exprt(name, interval.get_lower());
+
+  auto lower_bound = binary_relation_exprt(interval.get_lower(), ID_le, name);
+  auto upper_bound = binary_relation_exprt(name, ID_le, interval.get_upper());
+
+  return and_exprt(lower_bound, upper_bound);
+}
+
 void interval_abstract_valuet::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -94,6 +94,8 @@ class interval_abstract_valuet : public abstract_value_objectt
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   constant_interval_exprt interval;
 

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -119,6 +119,8 @@ static bool are_any_top(const abstract_object_sett &set);
 static bool is_set_extreme(const typet &type, const abstract_object_sett &set);
 
 static abstract_object_sett compact_values(const abstract_object_sett &values);
+static abstract_object_sett
+non_destructive_compact(const abstract_object_sett &values);
 static abstract_object_sett widen_value_set(
   const abstract_object_sett &values,
   const constant_interval_exprt &lhs,
@@ -334,6 +336,25 @@ abstract_value_pointert value_set_abstract_objectt::constrain(
   return as_value(resolve_values(constrained_values));
 }
 
+exprt value_set_abstract_objectt::to_predicate_internal(const exprt &name) const
+{
+  auto compacted = non_destructive_compact(values);
+  if(compacted.size() == 1)
+    return compacted.first()->to_predicate(name);
+
+  auto all_predicates = exprt::operandst{};
+  std::transform(
+    compacted.begin(),
+    compacted.end(),
+    std::back_inserter(all_predicates),
+    [&name](const abstract_object_pointert &value) {
+      return value->to_predicate(name);
+    });
+  std::sort(all_predicates.begin(), all_predicates.end());
+
+  return or_exprt(all_predicates);
+}
+
 void value_set_abstract_objectt::output(
   std::ostream &out,
   const ai_baset &ai,

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -69,6 +69,8 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   /// Setter for updating the stored values
   /// \param other_values: the new (non-empty) set of values
@@ -82,10 +84,10 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   abstract_object_pointert
   resolve_values(const abstract_object_sett &new_values) const;
 
+  void set_top_internal() override;
+
   // data
   abstract_object_sett values;
-
-  void set_top_internal() override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -229,6 +229,25 @@ abstract_object_pointert value_set_pointer_abstract_objectt::merge(
   return abstract_objectt::merge(other, widen_mode);
 }
 
+exprt value_set_pointer_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  if(values.size() == 1)
+    return values.first()->to_predicate(name);
+
+  auto all_predicates = exprt::operandst{};
+  std::transform(
+    values.begin(),
+    values.end(),
+    std::back_inserter(all_predicates),
+    [&name](const abstract_object_pointert &value) {
+      return value->to_predicate(name);
+    });
+  std::sort(all_predicates.begin(), all_predicates.end());
+
+  return or_exprt(all_predicates);
+}
+
 void value_set_pointer_abstract_objectt::set_values(
   const abstract_object_sett &other_values)
 {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -98,6 +98,8 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const abstract_object_pointert &other,
     const widen_modet &widen_mode) const override;
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   /// Update the set of stored values to \p new_values. Build a new abstract
   ///   object of the right type if necessary.