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/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/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/benchmarks/wasm/mem-sym-extract.wat b/benchmarks/wasm/mem-sym-extract.wat new file mode 100644 index 00000000..ca7e70eb --- /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 0 + 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/benchmarks/wasm/mem-sym.wat b/benchmarks/wasm/mem-sym.wat new file mode 100644 index 00000000..c7094008 --- /dev/null +++ b/benchmarks/wasm/mem-sym.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 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 (;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/headers/wasm/concrete_rt.hpp b/headers/wasm/concrete_rt.hpp index 179ef245..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,39 +200,4 @@ 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/smt_solver.hpp b/headers/wasm/smt_solver.hpp index 504422f7..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,7 +122,23 @@ 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); + 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 137d071d..d7aa70ed 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, int64_t value) : size(size), value(value) {} + int get_size() const { return size; } + int64_t get_value() const { return value; } + +private: + int size; + int64_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; @@ -59,7 +86,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; @@ -68,12 +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) { @@ -84,7 +118,17 @@ inline SymVal Concrete(Num num) { return SymVal(std::make_shared(num)); } -enum Operation { ADD, SUB, MUL, DIV, EQ, NEQ, LT, LEQ, GT, GEQ }; +// 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; @@ -96,47 +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 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) { @@ -178,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); @@ -723,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); @@ -744,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())) { @@ -798,4 +887,93 @@ inline std::monostate Snapshot_t::resume_execution(SymEnv_t &sym_env, return cont(mcont); } +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) { + // 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; + // 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; + } + + // 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 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; + if (s3.symptr == nullptr) { + s3 = SymVal(std::make_shared(8, 0)); + } + 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; + // 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{}; + } + + 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 + 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{}; + } + + // 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..5b5ae8de 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)) => @@ -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() @@ -767,9 +767,11 @@ trait StagedWasmEvaluator extends SAIOps { } object Memory { - 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 + // TODO: why this is only one function, rather than `storeInC` and `storeInS`? + // 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.s) } def loadIntC(base: Rep[Int], offset: Int): StagedConcreteNum = { @@ -777,7 +779,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 +1407,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("Memory.storeSym("); shallow(base); emit(", "); shallow(offset); emit(", "); shallow(s_value); emit(")") + case Node(_, "sym-load-int", List(base, offset), _) => + emit("Memory.loadSym("); 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), _) => @@ -1464,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(")") @@ -1476,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 851ef55d..03a5df09 100644 --- a/src/test/scala/genwasym/TestStagedConcolicEval.scala +++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala @@ -66,6 +66,16 @@ 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("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))) } @@ -76,10 +86,14 @@ 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("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))) } + // 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))) }