Merge pull request #4702 from romainbrenguier/refactor/value-set

Refactor in value_set

Author: romainbrenguier

src/goto-symex/symex_dereference_state.cpp

@@ -13,6 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/symbol_table.h>
 
+#ifdef DEBUG
+#  include <iostream>
+#endif
+
 /// Get or create a failed symbol for the given pointer-typed expression. These
 /// are used as placeholders when dereferencing expressions that are illegal to
 /// dereference, such as null pointers. The \ref add_failed_symbols pass must
@@ -84,10 +88,10 @@ void symex_dereference_statet::get_value_set(
 {
   state.value_set.get_value_set(expr, value_set, ns);
 
-#if 0
-  std::cout << "**************************\n";
-  state.value_set.output(goto_symex.ns, std::cout);
-  std::cout << "**************************\n";
+#ifdef DEBUG
+  std::cout << "symex_dereference_statet state.value_set={\n";
+  state.value_set.output(ns, std::cout, "  - ");
+  std::cout << "}" << std::endl;
 #endif
 
 #if 0

src/pointer-analysis/value_set.cpp

@@ -131,7 +131,10 @@ bool value_sett::insert(
   return true;
 }
 
-void value_sett::output(const namespacet &ns, std::ostream &out) const
+void value_sett::output(
+  const namespacet &ns,
+  std::ostream &out,
+  const std::string &indent) const
 {
   values.iterate([&](const irep_idt &, const entryt &e) {
     irep_idt identifier, display_name;
@@ -158,9 +161,7 @@ void value_sett::output(const namespacet &ns, std::ostream &out) const
 #endif
     }
 
-    out << display_name;
-
-    out << " = { ";
+    out << indent << display_name << " = { ";
 
     const object_map_dt &object_map = e.object_map.read();
 
@@ -204,7 +205,7 @@ void value_sett::output(const namespacet &ns, std::ostream &out) const
       {
         out << ", ";
         if(width >= 40)
-          out << "\n      ";
+          out << "\n" << std::string(' ', indent.size()) << "      ";
       }
     }
 

src/pointer-analysis/value_set.h

@@ -305,9 +305,11 @@ class value_sett
   /// Pretty-print this value-set
   /// \param ns: global namespace
   /// \param [out] out: stream to write to
+  /// \param indent: string to use for indentation of the output
   void output(
     const namespacet &ns,
-    std::ostream &out) const;
+    std::ostream &out,
+    const std::string &indent = "") const;
 
   /// Stores the LHS ID -> RHS expression set map. See `valuest` documentation
   /// for more detail.

src/pointer-analysis/value_set_dereference.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
@@ -97,33 +98,28 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   // type of the object
   const typet &type=pointer.type().subtype();
 
-#if 0
-  std::cout << "DEREF: " << format(pointer) << '\n';
+#ifdef DEBUG
+  std::cout << "value_set_dereferencet::dereference pointer=" << format(pointer)
+            << '\n';
 #endif
 
   // collect objects the pointer may point to
   value_setst::valuest points_to_set;
 
   dereference_callback.get_value_set(pointer, points_to_set);
 
-#if 0
-  for(value_setst::valuest::const_iterator
-      it=points_to_set.begin();
-      it!=points_to_set.end();
-      it++)
-    std::cout << "P: " << format(*it) << '\n';
+#ifdef DEBUG
+  std::cout << "value_set_dereferencet::dereference points_to_set={";
+  for(auto p : points_to_set)
+    std::cout << format(p) << "; ";
+  std::cout << "}\n" << std::flush;
 #endif
 
   // get the values of these
-
-  std::vector<exprt> retained_values;
-  for(const auto &value : points_to_set)
-  {
-    if(!should_ignore_value(value, exclude_null_derefs, language_mode))
-      retained_values.push_back(value);
-  }
-
-  std::list<valuet> values;
+  const std::vector<exprt> retained_values =
+    make_range(points_to_set).filter([&](const exprt &value) {
+      return !should_ignore_value(value, exclude_null_derefs, language_mode);
+    });
 
   exprt compare_against_pointer = pointer;
 
@@ -140,15 +136,17 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     compare_against_pointer = fresh_binder.symbol_expr();
   }
 
+#ifdef DEBUG
+  std::cout << "value_set_dereferencet::dereference retained_values={";
   for(const auto &value : retained_values)
-  {
-    values.push_back(build_reference_to(value, compare_against_pointer, ns));
-#if 0
-    std::cout << "V: " << format(value.pointer_guard) << " --> ";
-    std::cout << format(value.value);
-    std::cout << '\n';
+    std::cout << format(value) << "; ";
+  std::cout << "}\n" << std::flush;
 #endif
-  }
+
+  std::list<valuet> values =
+    make_range(retained_values).map([&](const exprt &value) {
+      return build_reference_to(value, compare_against_pointer, ns);
+    });
 
   // can this fail?
   bool may_fail;
@@ -227,8 +225,10 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   if(compare_against_pointer != pointer)
     value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value);
 
-#if 0
-  std::cout << "R: " << format(value) << "\n\n";
+#ifdef DEBUG
+  std::cout << "value_set_derefencet::dereference value=" << format(value)
+            << '\n'
+            << std::flush;
 #endif
 
   return value;