From 3716eb2ac823bae50cedb4c55c8dca6bf824565d Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Mon, 15 Sep 2025 18:21:06 -0400 Subject: [PATCH 01/11] move Memory_t to symbolic --- benchmarks/wasm/Makefile | 7 ++++ headers/wasm/concrete_rt.hpp | 34 ----------------- headers/wasm/symbolic_rt.hpp | 38 +++++++++++++++++++ .../scala/wasm/StagedConcolicMiniWasm.scala | 17 +++++++-- .../genwasym/TestStagedConcolicEval.scala | 3 +- 5 files changed, 59 insertions(+), 40 deletions(-) create mode 100644 benchmarks/wasm/Makefile diff --git a/benchmarks/wasm/Makefile b/benchmarks/wasm/Makefile new file mode 100644 index 00000000..bad47a22 --- /dev/null +++ b/benchmarks/wasm/Makefile @@ -0,0 +1,7 @@ +.PHONY: clean + +clean: + find . -type f -name '*.cpp' -delete + find . -type f -name '*.cpp.exe' -delete + find . -type d -name '*.dSYM' -exec rm -rf {} + + find . -type f -name '*.dot' -delete diff --git a/headers/wasm/concrete_rt.hpp b/headers/wasm/concrete_rt.hpp index 179ef245..34160c11 100644 --- a/headers/wasm/concrete_rt.hpp +++ b/headers/wasm/concrete_rt.hpp @@ -195,39 +195,5 @@ static std::monostate unreachable() { static int32_t pagesize = 65536; static int32_t page_count = 0; -struct Memory_t { - std::vector memory; - Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} - - int32_t loadInt(int32_t base, int32_t offset) { - return *reinterpret_cast(static_cast(memory.data()) + - base + offset); - } - - std::monostate storeInt(int32_t base, int32_t offset, int32_t value) { - *reinterpret_cast(static_cast(memory.data()) + base + - offset) = value; - return std::monostate{}; - } - - // grow memory by delta bytes when bytes > 0. return -1 if failed, return old - // size when success - int32_t grow(int32_t delta) { - if (delta <= 0) { - return memory.size(); - } - - try { - memory.resize(memory.size() + delta * pagesize); - auto old_page_count = page_count; - page_count += delta; - return memory.size(); - } catch (const std::bad_alloc &e) { - return -1; - } - } -}; - -static Memory_t Memory(1); // 1 page memory #endif // WASM_CONCRETE_RT_HPP \ No newline at end of file diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index 137d071d..f0aab2f0 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -798,4 +798,42 @@ inline std::monostate Snapshot_t::resume_execution(SymEnv_t &sym_env, return cont(mcont); } +struct Memory_t { + std::vector memory; + // Try to have + // std::vector> memory; + + Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} + + int32_t loadInt(int32_t base, int32_t offset) { + return *reinterpret_cast(static_cast(memory.data()) + + base + offset); + } + + std::monostate storeInt(int32_t base, int32_t offset, int32_t value) { + *reinterpret_cast(static_cast(memory.data()) + base + + offset) = value; + return std::monostate{}; + } + + // grow memory by delta bytes when bytes > 0. return -1 if failed, return old + // size when success + int32_t grow(int32_t delta) { + if (delta <= 0) { + return memory.size(); + } + + try { + memory.resize(memory.size() + delta * pagesize); + auto old_page_count = page_count; + page_count += delta; + return memory.size(); + } catch (const std::bad_alloc &e) { + return -1; + } + } +}; + +static Memory_t Memory(1); // 1 page memory + #endif // WASM_SYMBOLIC_RT_HPP \ No newline at end of file diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 2c41e2eb..895ba250 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -228,9 +228,9 @@ trait StagedWasmEvaluator extends SAIOps { val addr = Stack.popC(ty1) Stack.popS(ty1) val num = Memory.loadIntC(addr.toInt, offset) - val sym = Memory.loadIntS(addr.toInt, offset) + // val sym = Memory.loadIntS(addr.toInt, offset) Stack.pushC(num) - Stack.pushS(sym) + // Stack.pushS(sym) val newCtx2 = newCtx1.push(ty) eval(rest, kont, mkont, trail)(newCtx2) case MemorySize => ??? @@ -767,9 +767,10 @@ trait StagedWasmEvaluator extends SAIOps { } object Memory { + // TODO: why this is only one function, rather than `storeInC` and `storeInS`? def storeInt(base: Rep[Int], offset: Int, value: Rep[Int]): Rep[Unit] = { "memory-store-int".reflectCtrlWith[Unit](base, offset, value) - // todo: store symbolic value to memory via extract/concat operation + // "sym-store-int".reflectCtrlWith[Unit](base, offset, value) } def loadIntC(base: Rep[Int], offset: Int): StagedConcreteNum = { @@ -777,7 +778,7 @@ trait StagedWasmEvaluator extends SAIOps { } def loadIntS(base: Rep[Int], offset: Int): StagedSymbolicNum = { - StagedSymbolicNum(NumType(I32Type), "sym-load-int-todo".reflectCtrlWith[SymVal](base, offset)) + StagedSymbolicNum(NumType(I32Type), "sym-load-int".reflectCtrlWith[SymVal](base, offset)) } // Returns the previous memory size on success, or -1 if the memory cannot be grown. @@ -1405,6 +1406,14 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("Memory.grow("); shallow(delta); emit(")") case Node(_, "stack-size", _, _) => emit("Stack.size()") + // Symbolic Memory + case Node(_, "sym-store-int", List(base, offset, s_value), _) => + emit("SymMemory.storeInt("); shallow(base); emit(", "); shallow(offset); emit(", "); shallow(s_value); emit(")") + case Node(_, "sym-load-int", List(base, offset), _) => + emit("SymMemory.loadInt("); shallow(base); emit(", "); shallow(offset); emit(")") + case Node(_, "sym-memory-grow", List(delta), _) => + emit("SymMemory.grow("); shallow(delta); emit(")") + // Globals case Node(_, "global-get", List(i), _) => emit("Globals.get("); shallow(i); emit(")") case Node(_, "sym-global-get", List(i), _) => diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index 851ef55d..2445d06f 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -76,10 +76,9 @@ class TestStagedConcolicEval extends FunSuite { // TODO: Waiting more symbolic operators' implementations // test("loop - concrete") { testFileConcreteCpp("./benchmarks/wasm/loop.wat", None, expect=Some(List(10))) } test("even-odd - concrete") { testFileConcreteCpp("./benchmarks/wasm/even_odd.wat", None, expect=Some(List(1))) } - // Try global test("global - concrete") { testFileConcreteCpp("./benchmarks/wasm/global-sym.wat", None) } // TODO: Waiting symbolic memory's implementations - // test("load - concrete") { testFileConcreteCpp("./benchmarks/wasm/load.wat", None, expect=Some(List(1))) } + test("load - concrete") { testFileConcreteCpp("./benchmarks/wasm/load.wat", None, expect=Some(List(1))) } // test("btree - concrete") { testFileConcreteCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat") } test("fib - concrete") { testFileConcreteCpp("./benchmarks/wasm/fib.wat", None, expect=Some(List(144))) } test("tribonacci - concrete") { testFileConcreteCpp("./benchmarks/wasm/tribonacci.wat", None, expect=Some(List(504))) } From 6de493f2e59fa1f9b06122dbb65296d018b34c30 Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Mon, 15 Sep 2025 18:44:26 -0400 Subject: [PATCH 02/11] failing cases for load --- benchmarks/wasm/load-overflow1.wat | 19 +++++++++++++++++++ benchmarks/wasm/load-overflow2.wat | 19 +++++++++++++++++++ benchmarks/wasm/load.wat | 2 +- headers/wasm/symbolic_rt.hpp | 8 +++----- .../genwasym/TestStagedConcolicEval.scala | 3 +++ 5 files changed, 45 insertions(+), 6 deletions(-) create mode 100644 benchmarks/wasm/load-overflow1.wat create mode 100644 benchmarks/wasm/load-overflow2.wat diff --git a/benchmarks/wasm/load-overflow1.wat b/benchmarks/wasm/load-overflow1.wat new file mode 100644 index 00000000..9f005ea1 --- /dev/null +++ b/benchmarks/wasm/load-overflow1.wat @@ -0,0 +1,19 @@ +(module + (type (;0;) (func (result i32))) + (type (;1;) (func)) + (func (;0;) (type 0) (result i32) + i32.const 0 + i32.const 256 + i32.store + i32.const 1 + i32.load + ) + (func (;1;) (type 1) + call 0 + ;; should be 1 + ;; drop + ) + (start 1) + (memory (;0;) 2) + (export "main" (func 1)) +) \ No newline at end of file diff --git a/benchmarks/wasm/load-overflow2.wat b/benchmarks/wasm/load-overflow2.wat new file mode 100644 index 00000000..86c1a574 --- /dev/null +++ b/benchmarks/wasm/load-overflow2.wat @@ -0,0 +1,19 @@ +(module + (type (;0;) (func (result i32))) + (type (;1;) (func)) + (func (;0;) (type 0) (result i32) + i32.const 0 + i32.const 65536 + i32.store + i32.const 2 + i32.load + ) + (func (;1;) (type 1) + call 0 + ;; should be 1 + ;; drop + ) + (start 1) + (memory (;0;) 2) + (export "main" (func 1)) +) \ No newline at end of file diff --git a/benchmarks/wasm/load.wat b/benchmarks/wasm/load.wat index 916328aa..6c43d79b 100644 --- a/benchmarks/wasm/load.wat +++ b/benchmarks/wasm/load.wat @@ -10,7 +10,7 @@ ) (func (;1;) (type 1) call 0 - ;; should be 65536 + ;; should be 1 ;; drop ) (start 1) diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index f0aab2f0..9f8b31d2 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -799,19 +799,17 @@ inline std::monostate Snapshot_t::resume_execution(SymEnv_t &sym_env, } struct Memory_t { - std::vector memory; - // Try to have - // std::vector> memory; + std::vector> memory; Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} int32_t loadInt(int32_t base, int32_t offset) { - return *reinterpret_cast(static_cast(memory.data()) + + return *reinterpret_cast(static_cast *>(memory.data()) + base + offset); } std::monostate storeInt(int32_t base, int32_t offset, int32_t value) { - *reinterpret_cast(static_cast(memory.data()) + base + + *reinterpret_cast(static_cast *>(memory.data()) + base + offset) = value; return std::monostate{}; } diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index 2445d06f..0f04f933 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -79,6 +79,9 @@ class TestStagedConcolicEval extends FunSuite { test("global - concrete") { testFileConcreteCpp("./benchmarks/wasm/global-sym.wat", None) } // TODO: Waiting symbolic memory's implementations test("load - concrete") { testFileConcreteCpp("./benchmarks/wasm/load.wat", None, expect=Some(List(1))) } + // TODO: correct the behavior + test("load overflow 1 - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-overflow1.wat", None, expect=Some(List(1))) } + test("load overflow 2 - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-overflow2.wat", None, expect=Some(List(1))) } // test("btree - concrete") { testFileConcreteCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat") } test("fib - concrete") { testFileConcreteCpp("./benchmarks/wasm/fib.wat", None, expect=Some(List(144))) } test("tribonacci - concrete") { testFileConcreteCpp("./benchmarks/wasm/tribonacci.wat", None, expect=Some(List(504))) } From 9c08273f4c1fdf27302b70e9bd2956e0429b00ef Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Tue, 16 Sep 2025 01:48:41 -0400 Subject: [PATCH 03/11] correct behavior for load/store (concrete) --- headers/wasm/symbolic_rt.hpp | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index 9f8b31d2..a0865cb4 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -804,13 +804,25 @@ struct Memory_t { Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} int32_t loadInt(int32_t base, int32_t offset) { - return *reinterpret_cast(static_cast *>(memory.data()) + - base + offset); + int32_t addr = base + offset; + // Ensure we don't read out of bounds + assert(addr + 3 < memory.size()); + int32_t result = 0; + // Little-endian: lowest byte at lowest address + for (int i = 0; i < 4; ++i) { + result |= static_cast(memory[addr + i].first) << (8 * i); + } + return result; } std::monostate storeInt(int32_t base, int32_t offset, int32_t value) { - *reinterpret_cast(static_cast *>(memory.data()) + base + - offset) = value; + int32_t addr = base + offset; + // Ensure we don't write out of bounds + assert(addr + 3 < memory.size()); + for (int i = 0; i < 4; ++i) { + memory[addr + i].first = static_cast((value >> (8 * i)) & 0xFF); + // Optionally, update memory[addr + i].second (SymVal) if needed + } return std::monostate{}; } From e009c129104b5247f07da836090f8bd405603487 Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Mon, 22 Sep 2025 11:49:52 -0400 Subject: [PATCH 04/11] test offset --- benchmarks/wasm/load-offset.wat | 19 +++++++++++ benchmarks/wasm/mem-sym.wat | 25 +++++++++++++++ headers/wasm/symbolic_rt.hpp | 32 ++++++++++++++++++- .../scala/wasm/StagedConcolicMiniWasm.scala | 13 ++++---- .../genwasym/TestStagedConcolicEval.scala | 7 +++- 5 files changed, 88 insertions(+), 8 deletions(-) create mode 100644 benchmarks/wasm/load-offset.wat create mode 100644 benchmarks/wasm/mem-sym.wat diff --git a/benchmarks/wasm/load-offset.wat b/benchmarks/wasm/load-offset.wat new file mode 100644 index 00000000..1c42df1b --- /dev/null +++ b/benchmarks/wasm/load-offset.wat @@ -0,0 +1,19 @@ +(module + (type (;0;) (func (result i32))) + (type (;1;) (func)) + (func (;0;) (type 0) (result i32) + i32.const 0 + i32.const 256 + i32.store + i32.const 0 + i32.load offset=1 + ) + (func (;1;) (type 1) + call 0 + ;; should be 1 + ;; drop + ) + (start 1) + (memory (;0;) 2) + (export "main" (func 1)) +) \ No newline at end of file diff --git a/benchmarks/wasm/mem-sym.wat b/benchmarks/wasm/mem-sym.wat new file mode 100644 index 00000000..cc7266db --- /dev/null +++ b/benchmarks/wasm/mem-sym.wat @@ -0,0 +1,25 @@ +(module + (type (;0;) (func (result i32))) + (type (;1;) (func)) + (type (;2;) (func (param i32) (result i32))) + + (func (;0;) (type 2) (param i32) (result i32) + i32.const 0 + i32.const 1 + i32.store + i32.const 0 + local.get 0 + i32.store + i32.const 0 + i32.load + ) + (func (;1;) (type 1) + i32.const 0 + i32.symbolic + call 0 + ) + (start 1) + (memory (;0;) 2) + (export "main" (func 1)) + (global (;0;) (mut i32) (i32.const 42)) +) \ No newline at end of file diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index a0865cb4..a08d216e 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -799,13 +799,13 @@ inline std::monostate Snapshot_t::resume_execution(SymEnv_t &sym_env, } struct Memory_t { + // TODO: We assign a SymVal to each byte in memory std::vector> memory; Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} int32_t loadInt(int32_t base, int32_t offset) { int32_t addr = base + offset; - // Ensure we don't read out of bounds assert(addr + 3 < memory.size()); int32_t result = 0; // Little-endian: lowest byte at lowest address @@ -815,6 +815,36 @@ struct Memory_t { return result; } + // When loading a symval, we need to concat 4 symbolic values + // This sounds terribly bad for SMT... + SymVal loadSym(int32_t base, int32_t offset) { + int32_t addr = base + offset; + assert(addr + 3 < memory.size()); + SymVal result = Concrete(I32V(0)); + for (int i = 0; i < 4; ++i) { + auto byte_sym = memory[addr + i].second; + auto shift_amount = Concrete(I32V(8 * i)); + auto shift_byte = byte_sym.mul(Concrete(I32V(1 << (8 * i)))); + result = result.add(shift_byte); + } + return result; + } + + std::monostate storeSym(int32_t base, int32_t offset, SymVal value) { + int32_t addr = base + offset; + assert(addr + 3 < memory.size()); + for (int i = 0; i < 4; ++i) { + // Extract the i-th byte from the symbolic value + auto shift_amount = Concrete(I32V(8 * i)); + auto shifted = value.div(Concrete(I32V(1 << (8 * i)))); + auto byte_sym = shifted.minus(shifted.div(Concrete(I32V(256))).mul( + Concrete(I32V(256)))); + memory[addr + i].second = byte_sym; + // Optionally, update memory[addr + i].first (concrete byte) if needed + } + return std::monostate{}; + } + std::monostate storeInt(int32_t base, int32_t offset, int32_t value) { int32_t addr = base + offset; // Ensure we don't write out of bounds diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 895ba250..777060b9 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -220,7 +220,7 @@ trait StagedWasmEvaluator extends SAIOps { val (ty2, newCtx2) = newCtx1.pop() val addr = Stack.popC(ty2) val symAddr = Stack.popS(ty2) - Memory.storeInt(addr.toInt, offset, value.toInt) + Memory.storeInt(addr.toInt, offset, (value.toInt, symValue)) eval(rest, kont, mkont, trail)(newCtx2) case Nop => eval(rest, kont, mkont, trail) case Load(LoadOp(align, offset, ty, None, None)) => @@ -768,9 +768,10 @@ trait StagedWasmEvaluator extends SAIOps { object Memory { // TODO: why this is only one function, rather than `storeInC` and `storeInS`? - def storeInt(base: Rep[Int], offset: Int, value: Rep[Int]): Rep[Unit] = { - "memory-store-int".reflectCtrlWith[Unit](base, offset, value) - // "sym-store-int".reflectCtrlWith[Unit](base, offset, value) + // TODO: what should the type of SymVal be? + def storeInt(base: Rep[Int], offset: Int, value: (Rep[Int], StagedSymbolicNum)): Rep[Unit] = { + "memory-store-int".reflectCtrlWith[Unit](base, offset, value._1) + // "sym-store-int".reflectCtrlWith[Unit](base, offset, value._2) } def loadIntC(base: Rep[Int], offset: Int): StagedConcreteNum = { @@ -1408,9 +1409,9 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("Stack.size()") // Symbolic Memory case Node(_, "sym-store-int", List(base, offset, s_value), _) => - emit("SymMemory.storeInt("); shallow(base); emit(", "); shallow(offset); emit(", "); shallow(s_value); emit(")") + emit("Memory.storeSym("); shallow(base); emit(", "); shallow(offset); emit(", "); shallow(s_value); emit(")") case Node(_, "sym-load-int", List(base, offset), _) => - emit("SymMemory.loadInt("); shallow(base); emit(", "); shallow(offset); emit(")") + emit("Memory.loadSym("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "sym-memory-grow", List(delta), _) => emit("SymMemory.grow("); shallow(delta); emit(")") // Globals diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index 0f04f933..e5292dbe 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -79,9 +79,14 @@ class TestStagedConcolicEval extends FunSuite { test("global - concrete") { testFileConcreteCpp("./benchmarks/wasm/global-sym.wat", None) } // TODO: Waiting symbolic memory's implementations test("load - concrete") { testFileConcreteCpp("./benchmarks/wasm/load.wat", None, expect=Some(List(1))) } - // TODO: correct the behavior test("load overflow 1 - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-overflow1.wat", None, expect=Some(List(1))) } test("load overflow 2 - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-overflow2.wat", None, expect=Some(List(1))) } + + test("load offset - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-offset.wat", None, expect=Some(List(1))) } + + // alex TODO: how to test this? + test("mem-sym") { testFileConcreteCpp("./benchmarks/wasm/mem-sym.wat", None, expect=Some(List(0))) } + // test("btree - concrete") { testFileConcreteCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat") } test("fib - concrete") { testFileConcreteCpp("./benchmarks/wasm/fib.wat", None, expect=Some(List(144))) } test("tribonacci - concrete") { testFileConcreteCpp("./benchmarks/wasm/tribonacci.wat", None, expect=Some(List(504))) } From 73023b6b8a365ca225d19bf3cec364b1e041aa43 Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Mon, 22 Sep 2025 14:33:19 -0400 Subject: [PATCH 05/11] test concolic, currently failed --- headers/wasm/symbolic_rt.hpp | 6 +++--- src/main/scala/wasm/StagedConcolicMiniWasm.scala | 4 ++-- src/test/scala/genwasym/TestStagedConcolicEval.scala | 7 ++++--- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index a08d216e..c21dd526 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -72,6 +72,7 @@ struct SymVal { SymVal gt(const SymVal &other) const; SymVal geq(const SymVal &other) const; SymVal negate() const; + // TODO: add bitwise operations, and use the underlying bitvector theory bool is_concrete() const; }; @@ -815,7 +816,7 @@ struct Memory_t { return result; } - // When loading a symval, we need to concat 4 symbolic values + // TODO: when loading a symval, we need to concat 4 symbolic values // This sounds terribly bad for SMT... SymVal loadSym(int32_t base, int32_t offset) { int32_t addr = base + offset; @@ -823,7 +824,7 @@ struct Memory_t { SymVal result = Concrete(I32V(0)); for (int i = 0; i < 4; ++i) { auto byte_sym = memory[addr + i].second; - auto shift_amount = Concrete(I32V(8 * i)); + // 1 << i === 2^i auto shift_byte = byte_sym.mul(Concrete(I32V(1 << (8 * i)))); result = result.add(shift_byte); } @@ -835,7 +836,6 @@ struct Memory_t { assert(addr + 3 < memory.size()); for (int i = 0; i < 4; ++i) { // Extract the i-th byte from the symbolic value - auto shift_amount = Concrete(I32V(8 * i)); auto shifted = value.div(Concrete(I32V(1 << (8 * i)))); auto byte_sym = shifted.minus(shifted.div(Concrete(I32V(256))).mul( Concrete(I32V(256)))); diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 777060b9..58bdd19b 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -228,7 +228,7 @@ trait StagedWasmEvaluator extends SAIOps { val addr = Stack.popC(ty1) Stack.popS(ty1) val num = Memory.loadIntC(addr.toInt, offset) - // val sym = Memory.loadIntS(addr.toInt, offset) + val sym = Memory.loadIntS(addr.toInt, offset) Stack.pushC(num) // Stack.pushS(sym) val newCtx2 = newCtx1.push(ty) @@ -771,7 +771,7 @@ trait StagedWasmEvaluator extends SAIOps { // TODO: what should the type of SymVal be? def storeInt(base: Rep[Int], offset: Int, value: (Rep[Int], StagedSymbolicNum)): Rep[Unit] = { "memory-store-int".reflectCtrlWith[Unit](base, offset, value._1) - // "sym-store-int".reflectCtrlWith[Unit](base, offset, value._2) + "sym-store-int".reflectCtrlWith[Unit](base, offset, value._2.s) } def loadIntC(base: Rep[Int], offset: Int): StagedConcreteNum = { diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index e5292dbe..adea9e50 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -66,6 +66,10 @@ class TestStagedConcolicEval extends FunSuite { testFileConcolicCpp("./benchmarks/wasm/staged/simple_global.wat", Some("real_main"), exitByCoverage=true) } + test("mem-sym-concolic") { + testFileConcolicCpp("./benchmarks/wasm/mem-sym.wat", None, exitByCoverage=true) + } + test("return-poly - concrete") { testFileConcreteCpp("./benchmarks/wasm/staged/return_poly.wat", Some("$real_main"), expect=Some(List(42))) } @@ -84,9 +88,6 @@ class TestStagedConcolicEval extends FunSuite { test("load offset - concrete") { testFileConcreteCpp("./benchmarks/wasm/load-offset.wat", None, expect=Some(List(1))) } - // alex TODO: how to test this? - test("mem-sym") { testFileConcreteCpp("./benchmarks/wasm/mem-sym.wat", None, expect=Some(List(0))) } - // test("btree - concrete") { testFileConcreteCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat") } test("fib - concrete") { testFileConcreteCpp("./benchmarks/wasm/fib.wat", None, expect=Some(List(144))) } test("tribonacci - concrete") { testFileConcreteCpp("./benchmarks/wasm/tribonacci.wat", None, expect=Some(List(504))) } From e6183dc90b41e23c9a461cbdc7e53d68ff1bb822 Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Mon, 22 Sep 2025 14:34:35 -0400 Subject: [PATCH 06/11] oops --- benchmarks/wasm/mem-sym.wat | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/benchmarks/wasm/mem-sym.wat b/benchmarks/wasm/mem-sym.wat index cc7266db..c7094008 100644 --- a/benchmarks/wasm/mem-sym.wat +++ b/benchmarks/wasm/mem-sym.wat @@ -2,23 +2,30 @@ (type (;0;) (func (result i32))) (type (;1;) (func)) (type (;2;) (func (param i32) (result i32))) - - (func (;0;) (type 2) (param i32) (result i32) - i32.const 0 - i32.const 1 - i32.store + (type (;3;) (func (param i32))) + (import "console" "assert" (func (type 3))) + (func (;1;) (type 2) (param i32) (result i32) i32.const 0 local.get 0 - i32.store + i32.store i32.const 0 i32.load + i32.const 25 + i32.eq + if (result i32) ;; if x == 25 + i32.const 1 ;; return 1 + else + i32.const 0 + call 0 ;; assert false + i32.const 1 ;; to satisfy the type checker, this line will never be reached + end ) - (func (;1;) (type 1) + (func (;2;) (type 1) i32.const 0 - i32.symbolic - call 0 - ) - (start 1) + i32.symbolic ;; call it x + call 1 + ) + (start 2) (memory (;0;) 2) (export "main" (func 1)) (global (;0;) (mut i32) (i32.const 42)) From b4ffb4882cf5094c18317ef00b284f63386faea8 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Mon, 22 Sep 2025 23:00:54 -0400 Subject: [PATCH 07/11] symstack and stack should be consistent --- src/main/scala/wasm/StagedConcolicMiniWasm.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 58bdd19b..9b7ca831 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -230,7 +230,7 @@ trait StagedWasmEvaluator extends SAIOps { val num = Memory.loadIntC(addr.toInt, offset) val sym = Memory.loadIntS(addr.toInt, offset) Stack.pushC(num) - // Stack.pushS(sym) + Stack.pushS(sym) val newCtx2 = newCtx1.push(ty) eval(rest, kont, mkont, trail)(newCtx2) case MemorySize => ??? From 51b140e39c01cfd1d1d8ada544c25f484e99137e Mon Sep 17 00:00:00 2001 From: ahuoguo Date: Tue, 23 Sep 2025 02:00:06 -0400 Subject: [PATCH 08/11] added test for extract(currently failing --- benchmarks/wasm/mem-sym-extract.wat | 32 +++++++++++++++++++ .../genwasym/TestStagedConcolicEval.scala | 4 +++ 2 files changed, 36 insertions(+) create mode 100644 benchmarks/wasm/mem-sym-extract.wat diff --git a/benchmarks/wasm/mem-sym-extract.wat b/benchmarks/wasm/mem-sym-extract.wat new file mode 100644 index 00000000..53bcbb95 --- /dev/null +++ b/benchmarks/wasm/mem-sym-extract.wat @@ -0,0 +1,32 @@ +(module + (type (;0;) (func (result i32))) + (type (;1;) (func)) + (type (;2;) (func (param i32) (result i32))) + (type (;3;) (func (param i32))) + (import "console" "assert" (func (type 3))) + (func (;1;) (type 2) (param i32) (result i32) + i32.const 0 + local.get 0 + i32.store + i32.const 1 + i32.load + i32.const 1 + i32.eq + if (result i32) ;; if x == 256 + i32.const 1 ;; return 1 + else + i32.const 0 + call 0 ;; assert false + i32.const 1 ;; to satisfy the type checker, this line will never be reached + end + ) + (func (;2;) (type 1) + i32.const 0 + i32.symbolic ;; call it x + call 1 + ) + (start 2) + (memory (;0;) 2) + (export "main" (func 1)) + (global (;0;) (mut i32) (i32.const 42)) +) \ No newline at end of file diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index adea9e50..1e95b609 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -70,6 +70,10 @@ class TestStagedConcolicEval extends FunSuite { testFileConcolicCpp("./benchmarks/wasm/mem-sym.wat", None, exitByCoverage=true) } + test("mem-sym-extract-concolic") { + testFileConcolicCpp("./benchmarks/wasm/mem-sym-extract.wat", None, exitByCoverage=true) + } + test("return-poly - concrete") { testFileConcreteCpp("./benchmarks/wasm/staged/return_poly.wat", Some("$real_main"), expect=Some(List(42))) } From 2a622e543c93aa79fd2a14617ff1c906b52540a5 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Tue, 23 Sep 2025 20:58:45 -0400 Subject: [PATCH 09/11] extract & concat --- benchmarks/wasm/mem-sym-extract.wat | 2 +- headers/wasm/smt_solver.hpp | 10 ++++ headers/wasm/symbolic_rt.hpp | 73 +++++++++++++++++++++-------- 3 files changed, 65 insertions(+), 20 deletions(-) diff --git a/benchmarks/wasm/mem-sym-extract.wat b/benchmarks/wasm/mem-sym-extract.wat index 53bcbb95..ca7e70eb 100644 --- a/benchmarks/wasm/mem-sym-extract.wat +++ b/benchmarks/wasm/mem-sym-extract.wat @@ -8,7 +8,7 @@ i32.const 0 local.get 0 i32.store - i32.const 1 + i32.const 0 i32.load i32.const 1 i32.eq diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp index 504422f7..6d4629f2 100644 --- a/headers/wasm/smt_solver.hpp +++ b/headers/wasm/smt_solver.hpp @@ -119,7 +119,17 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) { case DIV: { return left / right; } + case CONCAT: { + return z3::concat(left, right); } + } + } else if (auto extract = dynamic_cast(sym_val.symptr.get())) { + assert(extract); + int high = extract->high * 8 - 1; + int low = extract->low * 8 - 8; + auto s = build_z3_expr(extract->value); + auto res = s.extract(high, low); + return res; } throw std::runtime_error("Unsupported symbolic value type"); } diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index c21dd526..88be896f 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -59,7 +59,7 @@ struct SymVal { // data structure operations SymVal makeSymbolic() const; - // arithmetic operations + // bitvector arithmetic operations SymVal is_zero() const; SymVal add(const SymVal &other) const; SymVal minus(const SymVal &other) const; @@ -72,6 +72,8 @@ struct SymVal { SymVal gt(const SymVal &other) const; SymVal geq(const SymVal &other) const; SymVal negate() const; + SymVal concat(const SymVal &other) const; + SymVal extract(int high, int low) const; // TODO: add bitwise operations, and use the underlying bitvector theory bool is_concrete() const; @@ -85,7 +87,31 @@ inline SymVal Concrete(Num num) { return SymVal(std::make_shared(num)); } -enum Operation { ADD, SUB, MUL, DIV, EQ, NEQ, LT, LEQ, GT, GEQ }; +enum Operation { + ADD, + SUB, + MUL, + DIV, + EQ, + NEQ, + LT, + LEQ, + GT, + GEQ, + CONCAT, +}; + +// Extract is different from other operations, it only has one symbolic operand, +// the other two operands are constants +// Extract from value, both high and low are inclusive byte indexes +struct SymExtract : Symbolic { + SymVal value; + int high; + int low; + + SymExtract(SymVal value, int high, int low) + : value(value), high(high), low(low) {} +}; struct SymBinary : Symbolic { Operation op; @@ -137,6 +163,13 @@ inline SymVal SymVal::is_zero() const { inline SymVal SymVal::negate() const { return SymVal(std::make_shared(EQ, *this, Concrete(I32V(0)))); } +inline SymVal SymVal::concat(const SymVal &other) const { + return SymVal(std::make_shared(CONCAT, *this, other)); +} +inline SymVal SymVal::extract(int high, int low) const { + assert(high >= low && "Invalid extract range"); + return SymVal(std::make_shared(*this, high, low)); +} inline SymVal SymVal::makeSymbolic() const { auto concrete = dynamic_cast(symptr.get()); @@ -806,6 +839,7 @@ struct Memory_t { Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {} int32_t loadInt(int32_t base, int32_t offset) { + // just load a 4-byte integer from memory of the vector int32_t addr = base + offset; assert(addr + 3 < memory.size()); int32_t result = 0; @@ -818,30 +852,31 @@ struct Memory_t { // TODO: when loading a symval, we need to concat 4 symbolic values // This sounds terribly bad for SMT... + // Load a 4-byte symbolic value from memory SymVal loadSym(int32_t base, int32_t offset) { int32_t addr = base + offset; assert(addr + 3 < memory.size()); - SymVal result = Concrete(I32V(0)); - for (int i = 0; i < 4; ++i) { - auto byte_sym = memory[addr + i].second; - // 1 << i === 2^i - auto shift_byte = byte_sym.mul(Concrete(I32V(1 << (8 * i)))); - result = result.add(shift_byte); - } - return result; + SymVal s0 = memory[addr].second; + SymVal s1 = memory[addr + 1].second; + SymVal s2 = memory[addr + 2].second; + SymVal s3 = memory[addr + 3].second; + assert(!s0.symptr && !s1.symptr && !s2.symptr && !s3.symptr && + "Loading symbolic value from uninitialized memory"); + return s0.concat(s1).concat(s2).concat(s3); } + // Store a 4-byte symbolic value to memory std::monostate storeSym(int32_t base, int32_t offset, SymVal value) { int32_t addr = base + offset; - assert(addr + 3 < memory.size()); - for (int i = 0; i < 4; ++i) { - // Extract the i-th byte from the symbolic value - auto shifted = value.div(Concrete(I32V(1 << (8 * i)))); - auto byte_sym = shifted.minus(shifted.div(Concrete(I32V(256))).mul( - Concrete(I32V(256)))); - memory[addr + i].second = byte_sym; - // Optionally, update memory[addr + i].first (concrete byte) if needed - } + // Extract 4 bytes from that symbol + SymVal s0 = value.extract(1, 1); + SymVal s1 = value.extract(2, 2); + SymVal s2 = value.extract(3, 3); + SymVal s3 = value.extract(4, 4); + memory[addr].second = s0; + memory[addr + 1].second = s1; + memory[addr + 2].second = s2; + memory[addr + 3].second = s3; return std::monostate{}; } From 5979e4a317fe9636fcf116baf1886d519c55a7c1 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Tue, 23 Sep 2025 23:01:06 -0400 Subject: [PATCH 10/11] some fixes, make btree example runable --- headers/wasm/concrete_rt.hpp | 6 +- headers/wasm/smt_solver.hpp | 9 ++ headers/wasm/symbolic_rt.hpp | 110 ++++++++++++------ .../scala/wasm/StagedConcolicMiniWasm.scala | 12 +- .../genwasym/TestStagedConcolicEval.scala | 2 + 5 files changed, 102 insertions(+), 37 deletions(-) diff --git a/headers/wasm/concrete_rt.hpp b/headers/wasm/concrete_rt.hpp index 34160c11..78c63c0e 100644 --- a/headers/wasm/concrete_rt.hpp +++ b/headers/wasm/concrete_rt.hpp @@ -74,6 +74,7 @@ class Stack_t { Num pop() { #ifdef DEBUG assert(count > 0 && "Stack underflow"); + printf("[Debug] poping from stack, size of concrete stack is: %d\n", count); #endif Num num = stack_ptr[count - 1]; count--; @@ -99,9 +100,13 @@ class Stack_t { if (size < 0) { throw std::out_of_range("Invalid size: " + std::to_string(size)); } + std::cout << "Shifting stack by offset " << offset << " and size " << size + << std::endl; + std::cout << "Current stack size: " << count << std::endl; #endif // shift last `size` of numbers forward of `offset` for (int32_t i = count - size; i < count; ++i) { + assert(i - offset >= 0); stack_ptr[i - offset] = stack_ptr[i]; } count -= offset; @@ -195,5 +200,4 @@ static std::monostate unreachable() { static int32_t pagesize = 65536; static int32_t page_count = 0; - #endif // WASM_CONCRETE_RT_HPP \ No newline at end of file diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp index 6d4629f2..64952bcc 100644 --- a/headers/wasm/smt_solver.hpp +++ b/headers/wasm/smt_solver.hpp @@ -71,6 +71,9 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) { } else if (auto concrete = std::dynamic_pointer_cast(sym_val.symptr)) { return z3_ctx.bv_val(concrete->value.value, 32); + } else if (auto smallbv = + std::dynamic_pointer_cast(sym_val.symptr)) { + return z3_ctx.bv_val(smallbv->get_value(), smallbv->get_size()); } else if (auto binary = std::dynamic_pointer_cast(sym_val.symptr)) { auto bit_width = 32; @@ -119,9 +122,15 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) { case DIV: { return left / right; } + case B_AND: { + return left & right; + } case CONCAT: { return z3::concat(left, right); } + default: + throw std::runtime_error("Operation not supported: " + + std::to_string(binary->op)); } } else if (auto extract = dynamic_cast(sym_val.symptr.get())) { assert(extract); diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index 88be896f..04ab19b0 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -6,6 +6,7 @@ #include "utils.hpp" #include #include +#include #include #include #include @@ -48,8 +49,34 @@ class SymConcrete : public Symbolic { SymConcrete(Num num) : value(num) {} }; +class SmallBV : public Symbolic { +public: + SmallBV(int size, uint64_t value) : size(size), value(value) {} + int get_size() const { return size; } + uint64_t get_value() const { return value; } + +private: + int size; + uint64_t value; +}; + struct SymBinary; +enum Operation { + ADD, // Addition + SUB, // Subtraction + MUL, // Multiplication + DIV, // Division + EQ, // Equal + NEQ, // Not equal + LT, // Less than + LEQ, // Less than or equal + GT, // Greater than + GEQ, // Greater than or equal + B_AND, // Bitwise AND + CONCAT, // Byte-level concatenation +}; + struct SymVal { std::shared_ptr symptr; @@ -68,15 +95,19 @@ struct SymVal { SymVal eq(const SymVal &other) const; SymVal neq(const SymVal &other) const; SymVal lt(const SymVal &other) const; - SymVal leq(const SymVal &other) const; + SymVal le(const SymVal &other) const; SymVal gt(const SymVal &other) const; - SymVal geq(const SymVal &other) const; + SymVal ge(const SymVal &other) const; SymVal negate() const; + SymVal bitwise_and(const SymVal &other) const; SymVal concat(const SymVal &other) const; SymVal extract(int high, int low) const; // TODO: add bitwise operations, and use the underlying bitvector theory bool is_concrete() const; + +private: + static SymVal make_binary(Operation op, const SymVal &lhs, const SymVal &rhs); }; static SymVal make_symbolic(int index) { @@ -87,20 +118,6 @@ inline SymVal Concrete(Num num) { return SymVal(std::make_shared(num)); } -enum Operation { - ADD, - SUB, - MUL, - DIV, - EQ, - NEQ, - LT, - LEQ, - GT, - GEQ, - CONCAT, -}; - // Extract is different from other operations, it only has one symbolic operand, // the other two operands are constants // Extract from value, both high and low are inclusive byte indexes @@ -123,54 +140,70 @@ struct SymBinary : Symbolic { }; inline SymVal SymVal::add(const SymVal &other) const { - return SymVal(std::make_shared(ADD, *this, other)); + return make_binary(ADD, *this, other); } inline SymVal SymVal::minus(const SymVal &other) const { - return SymVal(std::make_shared(SUB, *this, other)); + return make_binary(SUB, *this, other); } inline SymVal SymVal::mul(const SymVal &other) const { - return SymVal(std::make_shared(MUL, *this, other)); + return make_binary(MUL, *this, other); } inline SymVal SymVal::div(const SymVal &other) const { - return SymVal(std::make_shared(DIV, *this, other)); + return make_binary(DIV, *this, other); } inline SymVal SymVal::eq(const SymVal &other) const { - return SymVal(std::make_shared(EQ, *this, other)); + return make_binary(EQ, *this, other); } inline SymVal SymVal::neq(const SymVal &other) const { - return SymVal(std::make_shared(NEQ, *this, other)); + return make_binary(NEQ, *this, other); } + inline SymVal SymVal::lt(const SymVal &other) const { - return SymVal(std::make_shared(LT, *this, other)); + return make_binary(LT, *this, other); } -inline SymVal SymVal::leq(const SymVal &other) const { - return SymVal(std::make_shared(LEQ, *this, other)); + +inline SymVal SymVal::le(const SymVal &other) const { + return make_binary(LEQ, *this, other); } + inline SymVal SymVal::gt(const SymVal &other) const { - return SymVal(std::make_shared(GT, *this, other)); + return make_binary(GT, *this, other); } -inline SymVal SymVal::geq(const SymVal &other) const { - return SymVal(std::make_shared(GEQ, *this, other)); + +inline SymVal SymVal::ge(const SymVal &other) const { + return make_binary(GEQ, *this, other); } + inline SymVal SymVal::is_zero() const { - return SymVal(std::make_shared(EQ, *this, Concrete(I32V(0)))); + return make_binary(EQ, *this, Concrete(I32V(0))); } + inline SymVal SymVal::negate() const { - return SymVal(std::make_shared(EQ, *this, Concrete(I32V(0)))); + return make_binary(EQ, *this, Concrete(I32V(0))); } + inline SymVal SymVal::concat(const SymVal &other) const { - return SymVal(std::make_shared(CONCAT, *this, other)); + return make_binary(CONCAT, *this, other); } + inline SymVal SymVal::extract(int high, int low) const { assert(high >= low && "Invalid extract range"); return SymVal(std::make_shared(*this, high, low)); } +inline SymVal SymVal::bitwise_and(const SymVal &other) const { + return make_binary(B_AND, *this, other); +} +inline SymVal SymVal::make_binary(Operation op, const SymVal &lhs, + const SymVal &rhs) { + assert(lhs.symptr != nullptr && rhs.symptr != nullptr); + return SymVal(std::make_shared(op, lhs, rhs)); +} inline SymVal SymVal::makeSymbolic() const { auto concrete = dynamic_cast(symptr.get()); if (concrete) { @@ -212,6 +245,7 @@ class SymStack_t { std::monostate shift(int32_t offset, int32_t size) { auto n = stack.size(); for (size_t i = n - size; i < n; ++i) { + assert(i - offset >= 0); stack[i - offset] = stack[i]; } stack.resize(n - offset); @@ -857,11 +891,21 @@ struct Memory_t { int32_t addr = base + offset; assert(addr + 3 < memory.size()); SymVal s0 = memory[addr].second; + if (s0.symptr == nullptr) { + s0 = SymVal(std::make_shared(8, 0)); + } SymVal s1 = memory[addr + 1].second; + if (s1.symptr == nullptr) { + s1 = SymVal(std::make_shared(8, 0)); + } SymVal s2 = memory[addr + 2].second; + if (s2.symptr == nullptr) { + s2 = SymVal(std::make_shared(8, 0)); + } SymVal s3 = memory[addr + 3].second; - assert(!s0.symptr && !s1.symptr && !s2.symptr && !s3.symptr && - "Loading symbolic value from uninitialized memory"); + if (s3.symptr == nullptr) { + s3 = SymVal(std::make_shared(8, 0)); + } return s0.concat(s1).concat(s2).concat(s3); } diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 9b7ca831..5b5ae8de 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -245,7 +245,7 @@ trait StagedWasmEvaluator extends SAIOps { val retSym = "Concrete".reflectCtrlWith[SymVal](retNum) Stack.pushC(StagedConcreteNum(NumType(I32Type), retNum)) Stack.pushS(StagedSymbolicNum(NumType(I32Type), retSym)) - val newCtx2 = ctx.push(NumType(I32Type)) + val newCtx2 = newCtx.push(NumType(I32Type)) eval(rest, kont, mkont, trail)(newCtx2) case MemoryFill => ??? case Unreachable => unreachable() @@ -1474,11 +1474,15 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { shallow(lhs); emit(".mul("); shallow(rhs); emit(")") case Node(_, "sym-binary-div", List(lhs, rhs), _) => shallow(lhs); emit(".div("); shallow(rhs); emit(")") + case Node(_, "sym-binary-and", List(lhs, rhs), _) => + shallow(lhs); emit(".bitwise_and("); shallow(rhs); emit(")") case Node(_, "sym-relation-le", List(lhs, rhs), _) => - shallow(lhs); emit(".leq("); shallow(rhs); emit(")") + shallow(lhs); emit(".le("); shallow(rhs); emit(")") case Node(_, "sym-relation-leu", List(lhs, rhs), _) => shallow(lhs); emit(".leu("); shallow(rhs); emit(")") - case Node(_, "sym-relation-ge", List(lhs, rhs), _) => + case Node(_, "sym-relation-lt", List(lhs, rhs), _) => + shallow(lhs); emit(".lt("); shallow(rhs); emit(")") + case Node(_, "sym-relation-ge", List(lhs, rhs), _) => shallow(lhs); emit(".ge("); shallow(rhs); emit(")") case Node(_, "sym-relation-geu", List(lhs, rhs), _) => shallow(lhs); emit(".geu("); shallow(rhs); emit(")") @@ -1486,6 +1490,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { shallow(lhs); emit(".eq("); shallow(rhs); emit(")") case Node(_, "sym-relation-ne", List(lhs, rhs), _) => shallow(lhs); emit(".neq("); shallow(rhs); emit(")") + case Node(_, "sym-relation-gt", List(lhs, rhs), _) => + shallow(lhs); emit(".gt("); shallow(rhs); emit(")") case Node(_, "num-to-int", List(num), _) => shallow(num); emit(".toInt()") case Node(_, "make-symbolic", List(num), _) => diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala index 1e95b609..03a5df09 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -73,6 +73,8 @@ class TestStagedConcolicEval extends FunSuite { test("mem-sym-extract-concolic") { testFileConcolicCpp("./benchmarks/wasm/mem-sym-extract.wat", None, exitByCoverage=true) } + test("btree-bug-finding-concolic") { testFileConcolicCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat") } + test("return-poly - concrete") { testFileConcreteCpp("./benchmarks/wasm/staged/return_poly.wat", Some("$real_main"), expect=Some(List(42))) From afe188d5a6a3d4a4dccd629daf564ec4fddfe398 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Tue, 23 Sep 2025 23:27:39 -0400 Subject: [PATCH 11/11] tweak --- headers/wasm/symbolic_rt.hpp | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/headers/wasm/symbolic_rt.hpp b/headers/wasm/symbolic_rt.hpp index 04ab19b0..d7aa70ed 100644 --- a/headers/wasm/symbolic_rt.hpp +++ b/headers/wasm/symbolic_rt.hpp @@ -51,13 +51,13 @@ class SymConcrete : public Symbolic { class SmallBV : public Symbolic { public: - SmallBV(int size, uint64_t value) : size(size), value(value) {} + SmallBV(int size, int64_t value) : size(size), value(value) {} int get_size() const { return size; } - uint64_t get_value() const { return value; } + int64_t get_value() const { return value; } private: int size; - uint64_t value; + int64_t value; }; struct SymBinary; @@ -791,6 +791,17 @@ static SymEnv_t SymEnv; static Num eval_sym_expr(const SymVal &sym, SymEnv_t &sym_env) { if (auto concrete = dynamic_cast(sym.symptr.get())) { return concrete->value; + } else if (auto extract = dynamic_cast(sym.symptr.get())) { + auto value = eval_sym_expr(extract->value, sym_env); + int high = extract->high; + int low = extract->low; + assert(high >= low && "Invalid extract range"); + int size = high - low + 1; // size in bytes + int64_t mask = (1LL << (size * 8)) - 1; + int64_t extracted_value = (value.toInt() >> (low * 8)) & mask; + return Num(I64V(extracted_value)); + } else if (auto smallbv = dynamic_cast(sym.symptr.get())) { + return Num(I64V(smallbv->get_value())); } else if (auto operation = dynamic_cast(sym.symptr.get())) { // If it's a operation, we need to evaluate it auto lhs = eval_sym_expr(operation->lhs, sym_env); @@ -812,8 +823,18 @@ static Num eval_sym_expr(const SymVal &sym, SymEnv_t &sym_env) { return lhs > rhs; case GEQ: return lhs >= rhs; + case NEQ: + return lhs != rhs; + case EQ: + return lhs == rhs; + case B_AND: + return Num(I64V(lhs.value & rhs.value)); + case CONCAT: + // we must know the size of lhs and rhs in bytes to support concat + throw std::runtime_error( + "Concatenation operation not supported in evaluation"); default: - throw std::runtime_error("Operation not supported: " + + throw std::runtime_error("Operation not supported in evaluation: " + std::to_string(operation->op)); } } else if (auto symbol = dynamic_cast(sym.symptr.get())) {