smt2_solver: iterate over operands in expand_function_applications

src/solvers/smt2/smt2_solver.cpp

@@ -73,47 +73,57 @@ void smt2_solvert::define_constants()
 
 void smt2_solvert::expand_function_applications(exprt &expr)
 {
-  for(exprt &op : expr.operands())
-    expand_function_applications(op);
+  // Replace every function application that has a definition by its
+  // (instantiated) body, bottom-up. exprt::visit_post applies the visitor to
+  // each sub-expression after its operands using an explicit stack rather than
+  // recursion, so this does not overflow the call stack on the deeply-nested
+  // expressions the parser can produce (e.g. chains of thousands of bvand /
+  // store operations in SMT-COMP QF_ABV benchmarks).
+  expr.visit_post(
+    [this](exprt &e)
+    {
+      if(e.id() != ID_function_application)
+        return;
 
-  if(expr.id()==ID_function_application)
-  {
-    auto &app=to_function_application_expr(expr);
+      auto &app = to_function_application_expr(e);
+
+      if(app.function().id() != ID_symbol)
+        return;
 
-    if(app.function().id() == ID_symbol)
-    {
       // look up the symbol
       auto identifier = to_symbol_expr(app.function()).identifier();
       auto f_it = id_map.find(identifier);
 
-      if(f_it != id_map.end())
-      {
-        const auto &f = f_it->second;
+      if(f_it == id_map.end())
+        return;
 
-        DATA_INVARIANT(
-          f.type.id() == ID_mathematical_function,
-          "type of function symbol must be mathematical_function_type");
+      const auto &f = f_it->second;
 
-        const auto &domain = to_mathematical_function_type(f.type).domain();
+      DATA_INVARIANT(
+        f.type.id() == ID_mathematical_function,
+        "type of function symbol must be mathematical_function_type");
 
-        DATA_INVARIANT(
-          domain.size() == app.arguments().size(),
-          "number of parameters must match number of arguments");
+      const auto &domain = to_mathematical_function_type(f.type).domain();
 
-        // Does it have a definition? It's otherwise uninterpreted.
-        if(!f.definition.is_nil())
-        {
-          exprt body = f.definition;
+      DATA_INVARIANT(
+        domain.size() == app.arguments().size(),
+        "number of parameters must match number of arguments");
 
-          if(body.id() == ID_lambda)
-            body = to_lambda_expr(body).application(app.arguments());
+      // Does it have a definition? It's otherwise uninterpreted.
+      if(f.definition.is_nil())
+        return;
 
-          expand_function_applications(body); // rec. call
-          expr = body;
-        }
-      }
-    }
-  }
+      exprt body = f.definition;
+
+      if(body.id() == ID_lambda)
+        body = to_lambda_expr(body).application(app.arguments());
+
+      // The freshly inlined body may itself contain function applications. It
+      // was not part of this traversal, so expand it here. Bodies are typically
+      // shallow -- this is the pre-existing behaviour.
+      expand_function_applications(body);
+      e = body;
+    });
 }
 
 void smt2_solvert::setup_commands()

unit/util/expr.cpp

@@ -34,3 +34,38 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
     }
   }
 }
+
+TEST_CASE(
+  "exprt::visit_post handles deeply nested expressions",
+  "[core][util][expr]")
+{
+  // visit_post is an iterative (explicit-stack) post-order traversal. A chain
+  // this deep would overflow the call stack were it implemented recursively --
+  // it is far beyond the depth at which recursion exceeds the default (~8 MiB)
+  // unit-test stack -- yet light enough to stay cheap. Several rewrites rely on
+  // visit_post for exactly this depth-safety (e.g. smt2_solvert's
+  // expand_function_applications).
+  const std::size_t depth = 100000;
+
+  exprt e{ID_symbol};
+  for(std::size_t i = 0; i < depth; ++i)
+  {
+    exprt parent{ID_typecast};
+    parent.add_to_operands(std::move(e));
+    e = std::move(parent);
+  }
+
+  std::size_t visited = 0;
+  e.visit_post([&visited](exprt &) { ++visited; });
+
+  // Dismantle the chain iteratively before it goes out of scope: this branch
+  // does not include the depth-safe irept destructor, so destroying a chain
+  // this deep recursively would overflow the stack.
+  while(!e.operands().empty())
+  {
+    exprt child = std::move(e.operands().front());
+    e = std::move(child);
+  }
+
+  REQUIRE(visited == depth + 1);
+}