introduce exprt::visit_pre

src/goto-programs/mm_io.cpp

@@ -23,11 +23,10 @@ void collect_deref_expr(
   const exprt &src,
   std::set<dereference_exprt> &dest)
 {
-  if(src.id()==ID_dereference)
-    dest.insert(to_dereference_expr(src));
-
-  for(const auto & op : src.operands())
-    collect_deref_expr(op, dest); // recursive call
+  src.visit_pre([&dest](const exprt &e) {
+    if(e.id() == ID_dereference)
+      dest.insert(to_dereference_expr(e));
+  });
 }
 
 void mm_io(

src/goto-programs/validate_goto_model.cpp

@@ -179,7 +179,7 @@ void validate_goto_modelt::check_called_functions()
 
       // check functions of which the address is taken
       const auto &src = static_cast<const exprt &>(instr.code);
-      src.visit(test_for_function_address);
+      src.visit_pre(test_for_function_address);
     }
   }
 }

src/goto-symex/auto_objects.cpp

@@ -77,31 +77,27 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
 
 void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
 {
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
-  {
-    const ssa_exprt &ssa_expr=to_ssa_expr(expr);
-    const irep_idt &obj_identifier=ssa_expr.get_object_name();
-
-    if(obj_identifier != statet::guard_identifier())
+  expr.visit_pre([&state, this](const exprt &e) {
+    if(e.id() == ID_symbol && e.get_bool(ID_C_SSA_symbol))
     {
-      const symbolt &symbol=
-        ns.lookup(obj_identifier);
+      const ssa_exprt &ssa_expr = to_ssa_expr(e);
+      const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
-      if(has_prefix(id2string(symbol.base_name), "auto_object"))
+      if(obj_identifier != statet::guard_identifier())
       {
-        // done already?
-        if(
-          state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
-          state.get_level2().current_names.end())
+        const symbolt &symbol = ns.lookup(obj_identifier);
+
+        if(has_prefix(id2string(symbol.base_name), "auto_object"))
         {
-          initialize_auto_object(expr, state);
+          // done already?
+          if(
+            state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
+            state.get_level2().current_names.end())
+          {
+            initialize_auto_object(e, state);
+          }
         }
       }
     }
-  }
-
-  // recursive call
-  forall_operands(it, expr)
-    trigger_auto_object(*it, state);
+  });
 }

src/solvers/smt2/letify.cpp

@@ -96,7 +96,7 @@ exprt letifyt::substitute_let(const exprt &expr, const seen_expressionst &map)
 
   for(auto &op : tmp.operands())
   {
-    op.visit([&map](exprt &expr) {
+    op.visit_pre([&map](exprt &expr) {
       seen_expressionst::const_iterator it = map.find(expr);
 
       // replace subexpression by let symbol if used more than once

src/util/expr.cpp

@@ -243,15 +243,16 @@ const source_locationt &exprt::find_source_location() const
   return static_cast<const source_locationt &>(get_nil_irep());
 }
 
-void exprt::visit(std::function<void(exprt &)> visitor)
+template <typename T>
+static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
 {
-  std::stack<exprt *> stack;
+  std::stack<T *> stack;
 
-  stack.push(this);
+  stack.push(_expr);
 
   while(!stack.empty())
   {
-    exprt &expr=*stack.top();
+    T &expr = *stack.top();
     stack.pop();
 
     visitor(expr);
@@ -261,32 +262,24 @@ void exprt::visit(std::function<void(exprt &)> visitor)
   }
 }
 
-void exprt::visit(std::function<void(const exprt &)> visitor) const
+void exprt::visit_pre(std::function<void(exprt &)> visitor)
 {
-  std::stack<const exprt *> stack;
-
-  stack.push(this);
-
-  while(!stack.empty())
-  {
-    const exprt &expr=*stack.top();
-    stack.pop();
-
-    visitor(expr);
+  visit_pre_template(visitor, this);
+}
 
-    for(auto &op : expr.operands())
-      stack.push(&op);
-  }
+void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
+{
+  visit_pre_template(visitor, this);
 }
 
 void exprt::visit(expr_visitort &visitor)
 {
-  visit([&visitor](exprt &e) { visitor(e); });
+  visit_pre([&visitor](exprt &e) { visitor(e); });
 }
 
 void exprt::visit(const_expr_visitort &visitor) const
 {
-  visit([&visitor](const exprt &e) { visitor(e); });
+  visit_pre([&visitor](const exprt &e) { visitor(e); });
 }
 
 depth_iteratort exprt::depth_begin()

src/util/expr.h

@@ -324,10 +324,13 @@ class exprt:public irept
   }
 
 public:
+  /// These are pre-order traversal visitors, i.e.,
+  /// the visitor is executed on a node _before_ its children
+  /// have been visited.
   void visit(class expr_visitort &visitor);
   void visit(class const_expr_visitort &visitor) const;
-  void visit(std::function<void(exprt &)>);
-  void visit(std::function<void(const exprt &)>) const;
+  void visit_pre(std::function<void(exprt &)>);
+  void visit_pre(std::function<void(const exprt &)>) const;
 
   depth_iteratort depth_begin();
   depth_iteratort depth_end();

src/util/find_symbols.cpp

@@ -26,15 +26,12 @@ void find_symbols(
   bool current,
   bool next)
 {
-  if(src.id() == ID_symbol && current)
-    dest.insert(to_symbol_expr(src).get_identifier());
-  else if(src.id() == ID_next_symbol && next)
-    dest.insert(src.get(ID_identifier));
-  else
-  {
-    forall_operands(it, src)
-      find_symbols(*it, dest, current, next);
-  }
+  src.visit_pre([&dest, current, next](const exprt &e) {
+    if(e.id() == ID_symbol && current)
+      dest.insert(to_symbol_expr(e).get_identifier());
+    else if(e.id() == ID_next_symbol && next)
+      dest.insert(e.get(ID_identifier));
+  });
 }
 
 bool has_symbol(
@@ -68,26 +65,20 @@ void find_symbols(
   const exprt &src,
   std::set<exprt> &dest)
 {
-  if(src.id()==ID_symbol || src.id()==ID_next_symbol)
-    dest.insert(src);
-  else
-  {
-    forall_operands(it, src)
-      find_symbols(*it, dest);
-  }
+  src.visit_pre([&dest](const exprt &e) {
+    if(e.id() == ID_symbol || e.id() == ID_next_symbol)
+      dest.insert(e);
+  });
 }
 
 void find_symbols(
   const exprt &src,
   std::set<symbol_exprt> &dest)
 {
-  if(src.id()==ID_symbol)
-    dest.insert(to_symbol_expr(src));
-  else
-  {
-    forall_operands(it, src)
-      find_symbols(*it, dest);
-  }
+  src.visit_pre([&dest](const exprt &e) {
+    if(e.id() == ID_symbol)
+      dest.insert(to_symbol_expr(e));
+  });
 }
 
 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);