From 5f018593f0e8dce6ae28523454236bc00796adc0 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 02:00:34 -0400 Subject: [PATCH 1/6] bug fix: remove recalculation of symbolic size --- headers/wasm/sym_rt.hpp | 18 ------------------ headers/wasm/symbolic_decl.hpp | 2 +- 2 files changed, 1 insertion(+), 19 deletions(-) diff --git a/headers/wasm/sym_rt.hpp b/headers/wasm/sym_rt.hpp index efc49ad5..b0d025ef 100644 --- a/headers/wasm/sym_rt.hpp +++ b/headers/wasm/sym_rt.hpp @@ -42,7 +42,6 @@ class SymStack_t { void push(SymVal val) { // Push a symbolic value to the stack stack.push_back(val); - symbolic_size += val->size(); } SymVal pop() { @@ -54,12 +53,10 @@ class SymStack_t { #ifdef USE_IMM auto ret = *(stack.end() - 1); stack.take(stack.size() - 1); - symbolic_size -= ret->size(); return ret; #else auto ret = stack.back(); stack.pop_back(); - symbolic_size -= ret->size(); return ret; #endif } @@ -71,7 +68,6 @@ class SymStack_t { for (size_t i = n - size; i < n; ++i) { assert(i - offset >= 0); #ifdef USE_IMM - symbolic_size -= stack[i - offset]->size(); stack.set(i - offset, stack[i]); #else stack[i - offset] = stack[i]; @@ -149,10 +145,6 @@ class SymFrames_t { auto frame_base = current_frame_base(); assert(frame_base + size == stack.size()); - for (int i = 0; i < size; ++i) { - symbolic_size -= stack[stack.size() - 1 - i]->size(); - } - #ifdef USE_IMM stack.take(stack.size() - size); #else @@ -173,10 +165,6 @@ class SymFrames_t { assert(size >= 0); assert(static_cast(size) <= stack.size()); - for (int i = 0; i < size; ++i) { - symbolic_size -= stack[stack.size() - 1 - i]->size(); - } - #ifdef USE_IMM stack.take(stack.size() - size); #else @@ -203,7 +191,6 @@ class SymFrames_t { auto frame_base = current_frame_base(); assert(index >= 0 && static_cast(frame_base + index) < stack.size()); - symbolic_size += val->size() - stack[frame_base + index]->size(); #ifdef USE_IMM stack.set(frame_base + index, val); #else @@ -451,11 +438,6 @@ class SymMemory_t { exists = (it != memory.end()); #endif auto old_value = loadSymByte(addr); - if (exists) { - // We are overwriting an existing symbolic value - symbolic_size -= old_value->size(); - } - symbolic_size += value->size(); #ifdef USE_IMM memory.set(addr, value); #else diff --git a/headers/wasm/symbolic_decl.hpp b/headers/wasm/symbolic_decl.hpp index 8ce89dd0..0e2b5bd2 100644 --- a/headers/wasm/symbolic_decl.hpp +++ b/headers/wasm/symbolic_decl.hpp @@ -314,7 +314,7 @@ inline std::tuple count_dag_size_aux(Symbolic &val, } else if (auto witness = dynamic_cast(&val)) { assert(false && "Witness should not appear during instruction execution"); } else { - throw std::runtime_error("Unknown symbolic type in dag size counting"); + assert(false && "Unknown symbolic type in dag size counting"); } } From 31a7ca85f8e85575c254a273ed4c0005cdce5702 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 14:43:10 -0400 Subject: [PATCH 2/6] a debug utility --- headers/wasm/utils.hpp | 28 +++++++++++++++---- .../scala/wasm/StagedConcolicMiniWasm.scala | 8 ++++-- 2 files changed, 29 insertions(+), 7 deletions(-) diff --git a/headers/wasm/utils.hpp b/headers/wasm/utils.hpp index 8b7b0471..62c5bb8a 100644 --- a/headers/wasm/utils.hpp +++ b/headers/wasm/utils.hpp @@ -52,18 +52,36 @@ inline bool starts_with(const std::string &str, const std::string &prefix) { } #endif -inline std::monostate info() { -#ifdef DEBUG +inline std::monostate print_infos() { std::cout << std::endl; -#endif + return std::monostate{}; +} + +template +std::monostate print_infos(const T &first, const Args &...args) { + std::cout << first << " "; + print_infos(args...); return std::monostate{}; } template std::monostate info(const T &first, const Args &...args) { #ifdef DEBUG - std::cout << first << " "; - info(args...); + print_infos(first, args...); +#endif + return std::monostate{}; +} + +constexpr const char *DEBUG_OPTS_ENV_VAR = "GENSYM_DEBUG"; + +template +std::monostate infoWhen(const char *dbg_option, const Args &...args) { +#ifdef DEBUGWHEN + const char *env_value = std::getenv(DEBUG_OPTS_ENV_VAR); + if (env_value && std::string(env_value).find(std::string(dbg_option)) != + std::string::npos) { + print_infos(args...); + } #endif return std::monostate{}; } diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index b06eb028..c576a022 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -1112,6 +1112,10 @@ trait DebugInfo extends SAIOps { def info(xs: Rep[_]*): Rep[Unit] = { "info".reflectCtrlWith[Unit](xs: _*) } + + def infoWhen(envVar: Rep[String], xs: Rep[_]*): Rep[Unit] = { + "infoWhen".reflectCtrlWith[Unit](envVar :: xs.toList: _*) + } } @virtualize @@ -1671,7 +1675,7 @@ trait StagedWasmEvaluator extends SAIOps }) val newMKont: Rep[MCont[Unit]] = currentMCont.prependCont(restK) updateCurrentMCont(newMKont) - info(s"Calling function at index ", index.toInt, " with call_indirect, stackSize =", Stack.size) + infoWhen("CALL", s"Calling function at index ", index.toInt, " with call_indirect, stackSize =", Stack.size) val argsC = Stack.takeC(functy.inps) val argsS = Stack.takeS(functy.inps) Frames.pushFrameCallerC(functy.inps) @@ -1718,7 +1722,7 @@ trait StagedWasmEvaluator extends SAIOps val callee = evalFunc(ty, body, funcIndex, ty.inps, bodyLocals) // Predef.println(s"[DEBUG] locals size: ${locals.size}") withBlock { - info("Taking arguments from stack to call function at ", funcIndex) + infoWhen("CALL", s"Taking arguments from stack to call function at ", funcIndex) val newCtx = ctx.take(ty.inps.size) val argsC = Stack.takeC(ty.inps) val argsS = Stack.takeS(ty.inps) From 1b257fd27e85b5e77a116285e3b3f5c81d721753 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 15:05:52 -0400 Subject: [PATCH 3/6] fix: symbol name for combined z3 model --- headers/wasm/smt_solver.hpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp index fdd71dd6..d49117a1 100644 --- a/headers/wasm/smt_solver.hpp +++ b/headers/wasm/smt_solver.hpp @@ -51,8 +51,9 @@ compose_query_results(const std::vector &results) { // build a combined z3 model for (const auto &[id, num] : combined_map) { + // TODO: fix symbol name for other types solver.add( - global_z3_ctx().bv_const(("s_" + std::to_string(id)).c_str(), 32) == + global_z3_ctx().bv_const(("s_int" + std::to_string(id)).c_str(), 32) == global_z3_ctx().bv_val(num.value, 32)); } solver.check(); From 235f74b354cb7d477ac95cf7b9e5678b6225f0cd Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 15:11:11 -0400 Subject: [PATCH 4/6] compute composed model by z3::model directly --- headers/wasm/smt_solver.hpp | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp index d49117a1..562eeecb 100644 --- a/headers/wasm/smt_solver.hpp +++ b/headers/wasm/smt_solver.hpp @@ -36,6 +36,7 @@ static QueryResult compose_query_results(const std::vector &results) { ManagedTimer timer(TimeProfileKind::SPLIT_CONDITIONS); NumMap combined_map; + z3::model combined_model(global_z3_ctx()); for (const auto &res : results) { auto num_map = res.map_box; for (const auto &[id, num] : *num_map) { @@ -44,20 +45,21 @@ compose_query_results(const std::vector &results) { "Conflicting symbolic environment ids when composing query results"); combined_map[id] = num; } + const z3::model &model = res.model; + for (unsigned i = 0; i < model.num_consts(); ++i) { + z3::func_decl decl = model.get_const_decl(i); + std::string name = decl.name().str(); + assert((starts_with(name, "s_int") || starts_with(name, "s_f32") || + starts_with(name, "s_f64")) && + "Unexpected declaration in query result model"); + assert(!combined_model.has_interp(decl) && + "Internal Error: Conflicting constant declarations when composing query results"); + z3::expr value = model.get_const_interp(decl); + combined_model.add_const_interp(decl, value); + } } ImmNumMapBox combined_map_box(combined_map); - - z3::solver solver(global_z3_ctx()); - - // build a combined z3 model - for (const auto &[id, num] : combined_map) { - // TODO: fix symbol name for other types - solver.add( - global_z3_ctx().bv_const(("s_int" + std::to_string(id)).c_str(), 32) == - global_z3_ctx().bv_val(num.value, 32)); - } - solver.check(); - return QueryResult{combined_map_box, solver.get_model()}; + return QueryResult{combined_map_box, combined_model}; } // VectorGroupResult groups a vector. key is the vector index, and value is the From 761276055b770f9744e1194ba46e46671ea34dd3 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 15:23:53 -0400 Subject: [PATCH 5/6] remove a test case for i64.rotr, which is not use in benchmarks --- benchmarks/wasm/i64_ops.wat | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/benchmarks/wasm/i64_ops.wat b/benchmarks/wasm/i64_ops.wat index 75e589fc..673825b4 100644 --- a/benchmarks/wasm/i64_ops.wat +++ b/benchmarks/wasm/i64_ops.wat @@ -87,13 +87,13 @@ i64.eq call 0 - local.get 0 - local.get 2 - i64.extend_i32_u - i64.rotr - i64.const 4611686018427387909 - i64.eq - call 0 + ;; local.get 0 + ;; local.get 2 + ;; i64.extend_i32_u + ;; i64.rotr + ;; i64.const 4611686018427387909 + ;; i64.eq + ;; call 0 ;; comparisons local.get 0 From 6d458b12d170f06ee9ac5a0345ebdf0e912f4b2b Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 23:39:17 -0400 Subject: [PATCH 6/6] more debuggiing infos --- src/main/scala/wasm/StagedConcolicMiniWasm.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index c576a022..5d5b7c4b 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -1579,7 +1579,7 @@ trait StagedWasmEvaluator extends SAIOps } tailCall(thnK, ()) } else { - info(s"Continue") + info(s"Continue rest of the block") withBlock { val control = makeControl(thnK, currentMCont) ExploreTree.moveCursor(false, control) @@ -1690,7 +1690,7 @@ trait StagedWasmEvaluator extends SAIOps compileCache(funcIndex) } else { def retK(ctx: Context): Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => { - info(s"Return from the function at $funcIndex, stackSize =", Stack.size) + infoWhen("CALL", s"Exiting the function at $funcIndex, stackSize =", Stack.size) Frames.popFrameCalleeC(locals.size) Frames.popFrameCalleeS(locals.size) val offset = ctx.stackTypes.size - ty.out.size @@ -1700,7 +1700,7 @@ trait StagedWasmEvaluator extends SAIOps }) val func = topFun((_: Rep[Unit]) => { - info(s"Entered the function at $funcIndex, stackSize =", Stack.size) + infoWhen("CALL", s"Entered the function at $funcIndex, stackSize =", Stack.size) Frames.pushFrameCalleeC(locals.size) Frames.pushFrameCalleeS(locals) // the return instruction is also stack polymorphic @@ -1729,7 +1729,7 @@ trait StagedWasmEvaluator extends SAIOps // We make a new trail by `restK`, since function creates a new block to escape // (more or less like `return`) val restK: Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => { - info(s"Exiting the function at $funcIndex, stackSize =", Stack.size) + infoWhen("CALL", s"Returning from the function at $funcIndex, stackSize =", Stack.size) Frames.popFrameCallerC(ty.inps.size) Frames.popFrameCallerS(ty.inps.size) eval(rest, kont, trail)(newCtx.copy(stackTypes = ty.out.reverse ++ ctx.stackTypes.drop(ty.inps.size)))