Merge pull request #4690 from romainbrenguier/clean-up/value-set

Clean up in the value set API

Author: tautschnig

src/doxyfile

@@ -2041,7 +2041,7 @@ INCLUDE_FILE_PATTERNS  =
 # recursively expanded use the := operator instead of the = operator.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-PREDEFINED             =
+PREDEFINED             = "DEPRECATED(msg)= /// \deprecated msg"
 
 # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
 # tag can be used to specify a list of macro names that should be expanded. The

src/goto-symex/postcondition.cpp

@@ -160,16 +160,13 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    value_setst::valuest expr_set;
-    value_set.get_value_set(to_dereference_expr(expr).pointer(), expr_set, ns);
+    std::vector<exprt> expr_set =
+      value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
+    for(const exprt &e : expr_set)
     {
-      const exprt tmp = get_original_name(*it);
+      const exprt tmp = get_original_name(e);
       find_symbols(tmp, symbols);
     }
 

src/goto-symex/precondition.cpp

@@ -112,16 +112,12 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    value_setst::valuest expr_set;
-    value_sets.get_values(
-      SSA_step.source.function_id, target, deref_expr.pointer(), expr_set);
+    const std::vector<exprt> expr_set = value_sets.get_values(
+      SSA_step.source.function_id, target, deref_expr.pointer());
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
-      find_symbols(*it, symbols);
+    for(const exprt &e : expr_set)
+      find_symbols(e, symbols);
 
     if(symbols.find(lhs_identifier)!=symbols.end())
     {

src/goto-symex/symex_dereference_state.cpp

@@ -107,3 +107,10 @@ void symex_dereference_statet::get_value_set(
   std::cout << "**************************\n";
 #endif
 }
+
+/// Just forwards a value-set query to `state.value_set`
+std::vector<exprt>
+symex_dereference_statet::get_value_set(const exprt &expr) const
+{
+  return state.value_set.get_value_set(expr, ns);
+}

src/goto-symex/symex_dereference_state.h

@@ -34,9 +34,12 @@ class symex_dereference_statet:
   goto_symext::statet &state;
   const namespacet &ns;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;
 
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
+
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 };
 

src/pointer-analysis/dereference_callback.h

@@ -29,9 +29,12 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt() = default;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   virtual void
   get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
+  virtual std::vector<exprt> get_value_set(const exprt &expr) const = 0;
+
   virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
 };
 

src/pointer-analysis/goto_program_dereference.cpp

@@ -147,6 +147,16 @@ void goto_program_dereferencet::get_value_set(
   value_sets.get_values(current_function, current_target, expr, dest);
 }
 
+/// Gets the value set corresponding to the current target and
+/// expression \p expr.
+/// \param expr: an expression
+/// \return the value set
+std::vector<exprt>
+goto_program_dereferencet::get_value_set(const exprt &expr) const
+{
+  return value_sets.get_values(current_function, current_target, expr);
+}
+
 /// Remove dereference expressions contained in `expr`.
 /// \param expr: an expression
 /// \param checks_only: when true, execute the substitution on a copy of expr

src/pointer-analysis/goto_program_dereference.h

@@ -65,9 +65,12 @@ class goto_program_dereferencet:protected dereference_callbackt
 
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
+
   void dereference_instruction(
     goto_programt::targett target,
     bool checks_only=false);

src/pointer-analysis/value_set.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
+#include <util/range.h>
 
 #ifdef DEBUG
 #include <iostream>
@@ -308,8 +309,7 @@ bool value_sett::eval_pointer_offset(
   {
     assert(expr.operands().size()==1);
 
-    object_mapt reference_set;
-    get_value_set(expr.op0(), reference_set, ns, true);
+    const object_mapt reference_set = get_value_set(expr.op0(), ns, true);
 
     exprt new_expr;
     mp_integer previous_offset=0;
@@ -352,12 +352,11 @@ bool value_sett::eval_pointer_offset(
 }
 
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
 {
-  object_mapt object_map;
-  get_value_set(expr, object_map, ns, false);
+  object_mapt object_map = get_value_set(std::move(expr), ns, false);
 
   for(object_map_dt::const_iterator
       it=object_map.read().begin();
@@ -372,17 +371,37 @@ void value_sett::get_value_set(
   #endif
 }
 
+std::vector<exprt>
+value_sett::get_value_set(exprt expr, const namespacet &ns) const
+{
+  const object_mapt object_map = get_value_set(std::move(expr), ns, false);
+  return make_range(object_map.read())
+    .map([&](const object_map_dt::value_type &pair) { return to_expr(pair); });
+}
+
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   object_mapt &dest,
   const namespacet &ns,
   bool is_simplified) const
 {
-  exprt tmp(expr);
   if(!is_simplified)
-    simplify(tmp, ns);
+    simplify(expr, ns);
+
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+}
+
+value_sett::object_mapt value_sett::get_value_set(
+  exprt expr,
+  const namespacet &ns,
+  bool is_simplified) const
+{
+  if(!is_simplified)
+    simplify(expr, ns);
 
-  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
+  object_mapt dest;
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+  return dest;
 }
 
 /// Check if 'suffix' starts with 'field'.
@@ -1304,8 +1323,7 @@ void value_sett::assign(
   else
   {
     // basic type
-    object_mapt values_rhs;
-    get_value_set(rhs, values_rhs, ns, is_simplified);
+    object_mapt values_rhs = get_value_set(rhs, ns, is_simplified);
 
     // Permit custom subclass to alter the read values prior to write:
     adjust_assign_rhs_values(rhs, ns, values_rhs);

src/pointer-analysis/value_set.h

@@ -80,6 +80,7 @@ class value_sett
   /// Represents the offset into an object: either a unique integer offset,
   /// or an unknown value, represented by `!offset`.
   typedef optionalt<mp_integer> offsett;
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   bool offset_is_zero(const offsett &offset) const
   {
     return offset && offset->is_zero();
@@ -236,11 +237,13 @@ class value_sett
 
   /// Set of expressions; only used for the `get` API, not for internal
   /// data representation.
+  DEPRECATED(SINCE(2019, 05, 22, "Only used in deprecated function"))
   typedef std::set<exprt> expr_sett;
 
   /// Set of dynamic object numbers, equivalent to a set of
   /// `dynamic_object_exprt`s with corresponding IDs. Used only in internal
   /// implementation details.
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   typedef std::set<unsigned int> dynamic_object_id_sett;
 
   /// Map representing the entire value set, mapping from string LHS IDs
@@ -258,17 +261,24 @@ class value_sett
   /// `entryt` fields.
   typedef sharing_mapt<irep_idt, entryt> valuest;
 
-  /// Gets values pointed to by `expr`, including following dereference
+  /// Gets values pointed to by \p expr, including following dereference
   /// operators (i.e. this is not a simple lookup in `valuest`).
-  /// \param expr: query expression
-  /// \param [out] dest: assigned a set of expressions that `expr` may point to
-  /// \param ns: global namespace
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use get_value_set(exprt, const namespacet &) instead"))
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
 
+  /// Gets values pointed to by `expr`, including following dereference
+  /// operators (i.e. this is not a simple lookup in `valuest`).
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \return list of expressions that `expr` may point to
+  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
+
   /// Appears to be unimplemented.
+  DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
   expr_sett &get(const irep_idt &identifier, const std::string &suffix);
 
   void clear()
@@ -454,18 +464,25 @@ class value_sett
   void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
 
 protected:
-  /// Reads the set of objects pointed to by `expr`, including making
+  /// Reads the set of objects pointed to by \p expr, including making
   /// recursive lookups for dereference operations etc.
-  /// \param expr: query expression
-  /// \param [out] dest: overwritten by the set of object numbers pointed to
-  /// \param ns: global namespace
-  /// \param is_simplified: if false, simplify `expr` before reading.
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;
 
+  /// Reads the set of objects pointed to by `expr`, including making
+  /// recursive lookups for dereference operations etc.
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \param is_simplified: if false, simplify `expr` before reading.
+  /// \return the set of object numbers pointed to
+  object_mapt
+  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
+
   /// See the other overload of `get_reference_set`. This one returns object
   /// numbers and offsets instead of expressions.
   void get_reference_set(

src/pointer-analysis/value_set_analysis.h

@@ -65,6 +65,7 @@ class value_set_analysis_templatet:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   void get_values(
     const irep_idt &,
     locationt l,
@@ -73,6 +74,13 @@ class value_set_analysis_templatet:
   {
     (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
   }
+
+  // interface value_sets
+  std::vector<exprt>
+  get_values(const irep_idt &, locationt l, const exprt &expr) override
+  {
+    return (*this)[l].value_set.get_value_set(expr, baset::ns);
+  }
 };
 
 typedef

src/pointer-analysis/value_set_analysis_fi.cpp

@@ -195,3 +195,17 @@ bool value_set_analysis_fit::check_type(const typet &type)
 
   return false;
 }
+
+std::vector<exprt> value_set_analysis_fit::get_values(
+  const irep_idt &function_id,
+  flow_insensitive_analysis_baset::locationt l,
+  const exprt &expr)
+{
+  state.value_set.from_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.to_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.from_target_index = l->location_number;
+  state.value_set.to_target_index = l->location_number;
+  return state.value_set.get_value_set(expr, ns);
+}

src/pointer-analysis/value_set_analysis_fi.h

@@ -58,6 +58,7 @@ class value_set_analysis_fit:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning list instead"))
   void get_values(
     const irep_idt &function_id,
     locationt l,
@@ -72,6 +73,11 @@ class value_set_analysis_fit:
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
   }
+
+  std::vector<exprt> get_values(
+    const irep_idt &function_id,
+    locationt l,
+    const exprt &expr) override;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H