Add versions of get_value_set returning a value

These return the computed value, which makes the information flow
clearer in the program.
We deprecate at the same time the functions from the previous version.

Author: romainbrenguier

src/goto-symex/postcondition.cpp

@@ -160,8 +160,8 @@ 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);
+    value_setst::valuest 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

src/goto-symex/precondition.cpp

@@ -112,9 +112,8 @@ 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);
+    value_setst::valuest 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

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`
+value_setst::valuest
+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 list returning version instead"))
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;
 
+  value_setst::valuest 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 list returning version instead"))
   virtual void
   get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
+  virtual value_setst::valuest 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::list<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 list returning version instead"))
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
+  std::list<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;
@@ -356,8 +356,7 @@ void value_sett::get_value_set(
   value_setst::valuest &dest,
   const namespacet &ns) const
 {
-  object_mapt object_map;
-  get_value_set(std::move(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,6 +371,14 @@ void value_sett::get_value_set(
   #endif
 }
 
+std::list<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(
   exprt expr,
   object_mapt &dest,
@@ -384,6 +391,19 @@ void value_sett::get_value_set(
   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);
+
+  object_mapt dest;
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+  return dest;
+}
+
 /// Check if 'suffix' starts with 'field'.
 /// Suffix is delimited by periods and '[]' (array access) tokens, so we're
 /// looking for ".field($|[]|.)"
@@ -1303,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

@@ -261,16 +261,22 @@ 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(
     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::list<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);
@@ -458,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(
     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::list<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::list<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::list<exprt> get_values(
+    const irep_idt &function_id,
+    locationt l,
+    const exprt &expr) override;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H

src/pointer-analysis/value_set_fi.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "value_set_fi.h"
 
 #include <cassert>
+#include <iterator>
 #include <ostream>
 
 #include <util/symbol_table.h>
@@ -296,6 +297,12 @@ void value_set_fit::get_value_set(
   const exprt &expr,
   std::list<exprt> &value_set,
   const namespacet &ns) const
+{
+  value_set = get_value_set(expr, ns);
+}
+
+std::list<exprt>
+value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
 {
   object_mapt object_map;
   get_value_set(expr, object_map, ns);
@@ -336,21 +343,24 @@ void value_set_fit::get_value_set(
       flat_map.write()[it->first]=it->second;
   }
 
+  std::list<exprt> result;
   forall_objects(fit, flat_map.read())
-    value_set.push_back(to_expr(*fit));
+    result.push_back(to_expr(*fit));
 
-  #if 0
+#if 0
   // Sanity check!
   for(std::list<exprt>::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
     assert(it->type().id()!="#REF");
-  #endif
+#endif
 
-  #if 0
+#if 0
   for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
     std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
-  #endif
+#endif
+
+  return result;
 }
 
 void value_set_fit::get_value_set(

src/pointer-analysis/value_set_fi.h

@@ -205,11 +205,14 @@ class value_set_fit
   typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
   #endif
 
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
   void get_value_set(
     const exprt &expr,
     std::list<exprt> &dest,
     const namespacet &ns) const;
 
+  std::list<exprt> get_value_set(const exprt &expr, const namespacet &ns) const;
+
   expr_sett &get(
     const idt &identifier,
     const std::string &suffix);

src/pointer-analysis/value_sets.h

@@ -28,12 +28,19 @@ class value_setst
   typedef std::list<exprt> valuest;
 
   // this is not const to allow a lazy evaluation
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   virtual void get_values(
     const irep_idt &function_id,
     goto_programt::const_targett l,
     const exprt &expr,
     valuest &dest) = 0;
 
+  // this is not const to allow a lazy evaluation
+  virtual valuest get_values(
+    const irep_idt &function_id,
+    goto_programt::const_targett l,
+    const exprt &expr) = 0;
+
   virtual ~value_setst()
   {
   }