never build an expression twice

Author: butterunderflow

benchmarks/pldi2026/btree/compile.py

@@ -17,7 +17,7 @@
 DEFAULT_FLAGS = [
     "-std=c++17",
     "-g",
-    "-O0",
+    "-O3",
     "-Wall",
     "-Wextra",
     "-DUSE_IMM",

benchmarks/pldi2026/btree/run.py

@@ -23,6 +23,8 @@ def run_all(targets: list[Path], action):
             continue
         file_name = file_path.name.removesuffix(".exe")
         output_path = f"{file_name}.output"
+        if Path(output_path).exists():
+            continue
         if action == "run":
             env = os.environ.copy()
             env.update({"OUTPUT_DIR": output_path})

headers/wasm/smt_solver.hpp

@@ -7,6 +7,7 @@
 #include "wasm/profile.hpp"
 #include "z3++.h"
 #include <array>
+#include <memory>
 #include <set>
 #include <string>
 #include <tuple>
@@ -15,15 +16,16 @@
 class Solver {
 public:
   Solver() {}
-  std::optional<NumMap> solve(const std::vector<SymVal> &conditions) {
+  std::optional<NumMap> solve(std::vector<SymVal> &conditions) {
     z3::solver z3_solver(z3_ctx);
     z3::check_result solver_result;
     {
+      auto timer = ManagedTimer(TimeProfileKind::SOLVER);
       // make an conjunction of all conditions
       auto conjunction = to_z3_conjunction(conditions);
       // call z3 to solve the condition
-      auto timer = ManagedTimer(TimeProfileKind::SOLVER);
-      z3_solver.add(conjunction); // NOTE: half of the solver time is spent in solver.add
+      // NOTE: half of the solver time is spent in solver.add
+      z3_solver.add(conjunction);
       solver_result = z3_solver.check();
     }
     switch (solver_result) {
@@ -56,9 +58,9 @@ class Solver {
   }
 
 private:
-  z3::expr to_z3_conjunction(const std::vector<SymVal> &conditions) {
+  z3::expr to_z3_conjunction(std::vector<SymVal> &conditions) {
     z3::expr conjunction = z3_ctx.bool_val(true);
-    for (const auto &cond : conditions) {
+    for (auto &cond : conditions) {
       auto z3_cond = build_z3_expr(cond);
       conjunction = conjunction && z3_cond != z3_ctx.bv_val(0, 32);
     }
@@ -70,10 +72,13 @@ class Solver {
   }
 
   z3::context z3_ctx;
-  z3::expr build_z3_expr(const SymVal &sym_val);
+  z3::expr build_z3_expr(SymVal &sym_val);
+
+private:
+  z3::expr build_z3_expr_aux(SymVal &sym_val);
 };
 
-inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) {
+inline z3::expr Solver::build_z3_expr_aux(SymVal &sym_val) {
   if (auto sym = std::dynamic_pointer_cast<Symbol>(sym_val.symptr)) {
     return z3_ctx.bv_const(("s_" + std::to_string(sym->get_id())).c_str(), 32);
   } else if (auto concrete =
@@ -150,4 +155,13 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) {
   }
   throw std::runtime_error("Unsupported symbolic value type");
 }
+
+inline z3::expr Solver::build_z3_expr(SymVal &sym_val) {
+  if (sym_val.z3_expr) {
+    return *sym_val.z3_expr;
+  }
+  auto e = build_z3_expr_aux(sym_val);
+  sym_val.z3_expr = std::make_shared<z3::expr>(e);
+  return e;
+}
 #endif // SMT_SOLVER_HPP

headers/wasm/symbolic_rt.hpp

@@ -10,6 +10,7 @@
 #include "immer/vector_transient.hpp"
 #include "profile.hpp"
 #include "utils.hpp"
+#include "z3++.h"
 #include <cassert>
 #include <cstddef>
 #include <cstdint>
@@ -90,6 +91,7 @@ static std::shared_ptr<SmallBV> ZeroByte =
 
 struct SymVal {
   std::shared_ptr<Symbolic> symptr;
+  std::shared_ptr<z3::expr> z3_expr;
 
   SymVal() : symptr(ZERO) {}
   SymVal(std::shared_ptr<Symbolic> symptr) : symptr(symptr) {}
@@ -226,11 +228,21 @@ inline SymVal SymVal::make_binary(Operation op, const SymVal &lhs,
   assert(lhs.symptr != nullptr && rhs.symptr != nullptr);
   return SymVal(SymBookKeeper.allocate<SymBinary>(op, lhs, rhs));
 }
+static std::unordered_map<int, SymVal> SymbolCache;
+
 inline SymVal SymVal::makeSymbolic() const {
   auto concrete = dynamic_cast<SymConcrete *>(symptr.get());
   if (concrete) {
     // If the symbolic value is a concrete value, use it to create a symbol
-    return SymVal(SymBookKeeper.allocate<Symbol>(concrete->value.toInt()));
+    auto id = concrete->value.toInt();
+    auto it = SymbolCache.find(id);
+    if (it != SymbolCache.end()) {
+      return it->second;
+    }
+    auto sym = Symbol(id);
+    auto ptr = SymBookKeeper.allocate<Symbol>(sym);
+    return SymVal(ptr);
+
   } else {
     throw std::runtime_error(
         "Cannot make symbolic a non-concrete symbolic value");