diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index cbb2b2f098a..c2ccbe33dda 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -23,11 +23,10 @@ void collect_deref_expr( const exprt &src, std::set &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( diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index f0001a26da8..7aefc947a8c 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/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(instr.code); - src.visit(test_for_function_address); + src.visit_pre(test_for_function_address); } } } diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index 376f8e3feda..1bf33ce5d08 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/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); + }); } diff --git a/src/solvers/smt2/letify.cpp b/src/solvers/smt2/letify.cpp index bab53dcba72..13166aa1bc6 100644 --- a/src/solvers/smt2/letify.cpp +++ b/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 diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 00f574df85a..94f63125733 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -243,15 +243,16 @@ const source_locationt &exprt::find_source_location() const return static_cast(get_nil_irep()); } -void exprt::visit(std::function visitor) +template +static void visit_pre_template(std::function visitor, T *_expr) { - std::stack stack; + std::stack 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 visitor) } } -void exprt::visit(std::function visitor) const +void exprt::visit_pre(std::function visitor) { - std::stack 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 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() diff --git a/src/util/expr.h b/src/util/expr.h index 078a7dd6fe3..686c2018007 100644 --- a/src/util/expr.h +++ b/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 visit(std::function) const; + void visit_pre(std::function); + void visit_pre(std::function) const; depth_iteratort depth_begin(); depth_iteratort depth_end(); diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index afde421f333..1841bc8464e 100644 --- a/src/util/find_symbols.cpp +++ b/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 &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 &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);