pre_traversal range for expressions

src/goto-symex/goto_symex_state.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/std_expr.h>
@@ -850,7 +851,9 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns)
 
   // L2 renaming
   exprt fields = field_sensitivity.get_fields(ns, *this, ssa, false);
-  fields.visit_pre([this](const exprt &e) {
+
+  for(auto &e : pre_traversal(fields))
+  {
     if(auto l1_symbol = expr_try_dynamic_cast<symbol_exprt>(e))
     {
       const ssa_exprt &field_ssa = to_ssa_expr(*l1_symbol);
@@ -865,7 +868,7 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns)
         ssa.get_identifier(), ssa, fresh_l2_name_provider);
       CHECK_RETURN(field_generation == 1);
     }
-  });
+  };
 
   record_events.push(false);
   exprt expr_l2 = rename(std::move(ssa), ns).get();

src/goto-symex/symex_main.cpp

@@ -758,9 +758,9 @@ static std::optional<symbol_exprt>
 find_unique_pointer_typed_symbol(const exprt &expr)
 {
   std::optional<symbol_exprt> return_value;
-  for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); ++it)
+  for(auto &node : pre_traversal(expr))
   {
-    const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(*it);
+    const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(node);
     if(symbol_expr && can_cast_type<pointer_typet>(symbol_expr->type()))
     {
       // If we already have a potential return value, check if it is the same

src/util/expr_iterator.h

@@ -305,4 +305,33 @@ class const_unique_depth_iteratort final:
   std::set<exprt> m_traversed;
 };
 
+/// An adapter to yield a range (expected to satisfy C++20 std::ranges::range)
+/// of const_depth_iteratort.
+class const_depth_iterator_range_adaptert
+{
+public:
+  explicit const_depth_iterator_range_adaptert(const exprt &_root) : root{_root}
+  {
+  }
+
+  const_depth_iteratort begin() const
+  {
+    return root.depth_cbegin();
+  }
+
+  const_depth_iteratort end() const
+  {
+    return root.depth_cend();
+  }
+
+protected:
+  const exprt &root;
+};
+
+static inline const_depth_iterator_range_adaptert
+pre_traversal(const exprt &root)
+{
+  return const_depth_iterator_range_adaptert{root};
+}
+
 #endif