Skip to content

Commit f73ffcd

Browse files
butterunderflowahuoguo
butterunderflow
and
ahuoguo
authored
staged concolic miniwasm (#89)
* remove unused expressions * let's start from the staged miniwasm interpreter * dup all concrete operations to symbolic * maintain a symbolic stack during the execution * record path conditions * The branch node only needs to remember the positive condition. use the sub-nodes of the branch to classify whether the execution is true or false * symbolic runtime for explore tree * add a to graphviz method, enhancing debug experience * put symbolic expression on the SymStack * `type.symbolic` instruction * test staged concolic compilation in CI * dump graphviz by default * concolic driver * fix: add an unreachable node & use GENSYM_ASSERT * call z3 to solve constraints * remove unused & resize before update environment * use c++20 * branch in brtable * use driver's entrypoint by default * rename package name of staged miniwasm * tweak * Reuse symbolic states (#90) 1. split concrete and symbolic interpreter 2. copy tests from concrete execution 3. some bug fixes * c++17 compatible * fix * revert: don't split concrete/symbolic interpreter & don't support snapshot for now * introduce a SnapshotNode, which currently behaves same as UnexploredNode * fill snapshot into SnapshotNode * snapshot reuse via continuation more tests should be added * remove debug printings * give every branch node an ID * a bitmap to record the branch coverage * a new exploring strategy: exit when all branches are covered * support numeric globals * Explicitly classify the next stage computation and its type Then we can compose/decompose them more easily. * correct behavior for global * make log function returning std::monostate/Unit type * Symbolic memory (#91) * move Memory_t to symbolic * failing cases for load * correct behavior for load/store (concrete) * test offset * test concolic, currently failed * oops * symstack and stack should be consistent * added test for extract(currently failing * extract & concat * some fixes, make btree example runable * tweak --------- Co-authored-by: butterunderflow <azhong.934@gmail.com> * fix: high bits should be concat first * make btree example work with concolic execution * preallocate pages for the memory * remove some unperformant code 1. dont intialize memory twice 2. dont allocate memory for unuse symbolic memory, because we need to copy them 3. profiling utilities * work list algorithm for exploration * config header; fix extract evaluation; capture by value in lambda * replace SymEnv_t's underlying representation * compare the exploration trees (w/ vs. w/o snapshot reuse) * accelerate test by using O0 optimization * add an option to use immutable data structure * a simple test case to show immutable's improvements * add a benchmark testcase * a pool to store symbolic concrete * a example to show when snapshot is highly effective * some infra to support the cost model to decide if we should create snapshot * a cost model to determin if we want to create snapshot * update btree benchmarks * rename * turn wast to wat * use imported api for symbolic operations so they can be run by wat2wasm currently only 2o2u.wat works * replace call to i32.symbolic with external call * a normalize script * replace sym_assume with (call $i32.sym_assume) * remove print_btree, it's a dummy instruction only implemented in wasp * replace (sym_assert) with (call $i32.sym_assert) * replace the usage of get_sym_int32 * remove two files that are not runable by wasp * convert all wat file to a form we can parse via (wasm2wat . wat2wasm) * get_sym_int32 is not useful anymore * take get_sym_int32 back but don't use them * a test entry that compile btree cases * a compile script in python * avoid some usage of fun * remove an unused function * nontermination (if loop termination depends on symbolic value, it will explode the user's stack instead, now it gets out of bounds for the concrete stack in c++) * support sym_assume to prune subtrees * support write profile file * a script for running and cleaning up benchmark executables. * never build an expression twice * update sym_assert and timer * refactor operator to explicit methods * fixed a bug, zero initialize local variables * use z3's api to evaluate a symbolic expression * let z3 decide the value of symbols that are not in the model * tweak tests * update test script * support some f32 * support call_indirect * final call_indirect * misc * up * fix * up btree for wasp * update collection-c benchmark * add import * i32.symbolic * sym_assume is call 1 * sym_assert is call 2 * alloc and free wasp primitive * support some operations * tweak * a script to run wasp on btree benchmarks * data section initialize * revert something * more operations * try not to build symbolic expressions when all operands are concrete * a crafted benchmark * snapshot benchmark * lots cleanup * fix cost ratio related things * fix: extract's index is 1-based * remove debug prints * use a dedicated slot for current continuation (so we can enforce tail call optimizations later) * finally we have tail call optimization enforced To run larger benchmarks, we must have this * a test case for very long execution * fix * little optimize * save current symbolic environment in snapshot * fix a memory issue detected by sanitizer * more guaranteed tail call * a interface to calculate the dag size of symbolic * a unified interface for storing symbolic byte * calculate dag size of symbolic expressions * avoid creating duplicate symbolic operations * avoid creating same symbolic expressions multiple times by factory pattern * reorg snapshot related logic: only calculate cost of a snapshot when it's reachable * update profile * update crafted benchmarks * fix smallbv factory * a cache for query results * independent constraint resolving * remove collection-c benchmark * update benchmark compilation entry * remove unnecessary files * remove pldi2026 benchmarks, add them in another PR * a function to collect path conditions without re-iterating same path * fix ci * support wasp style profiling * mechanism for profiling Z3 solver API calls * tweak * extract node picking logic from the driver * small fix * use a unified path condition to explore new path * fix ci * a bv2bool method * mark a node as unreachable if its condition is concrete * more simplification * more simplification * enrich symbolic encoding, so we can simplify them further * more simplification applied other concolic execution tools * more simplification detected by gpt * tweak * try to reduce the use of not * try build z3_expr less often * update * fix ci * refactor & fix ci --------- Co-authored-by: ahuoguo <ahuoguo@gmail.com>
1 parent d35cad8 commit f73ffcd

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+31721
-1006
lines changed

‎.github/workflows/scala.yml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@ jobs:
1010
build:
1111

1212
runs-on: ubuntu-22.04
13+
env:
14+
Z3_INCLUDE_DIR: /usr/include
15+
Z3_LIB_DIR: /usr/lib/x86_64-linux-gnu
16+
IMMER_INCLUDE_DIR: ${{ github.workspace }}/third-party/immer
1317
defaults:
1418
run:
1519
working-directory: ./
@@ -78,4 +82,4 @@ jobs:
7882
sbt 'testOnly gensym.wasm.TestScriptRun'
7983
sbt 'testOnly gensym.wasm.TestConcolic'
8084
sbt 'testOnly gensym.wasm.TestDriver'
81-
sbt 'testOnly gensym.wasm.TestStagedEval'
85+
sbt 'testOnly gensym.wasm.TestStagedConcolicEval'

‎benchmarks/wasm/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,6 @@
33
clean:
44
find . -type f -name '*.cpp' -delete
55
find . -type f -name '*.cpp.exe' -delete
6-
find . -type d -name '*.dSYM' -exec rm -rf {} +
6+
find . -type d -name '*.dSYM' -exec rm -rf {} +
7+
find . -type f -name '*.dot' -delete
8+

‎benchmarks/wasm/branch-strip-buggy.wat‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@
2929
else
3030
i32.const 0
3131
call 2
32+
i32.const 1 ;; to satisfy the type checker, this line will never be reached
3233
end
3334
end
3435
)

‎benchmarks/wasm/btree/2o1u-unlabeled.wat‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2626,9 +2626,12 @@
26262626
i32.and
26272627
drop)
26282628
(func (;7;) (type 4)
2629-
i32.const 3
26302629
i32.const 2
2630+
i32.symbolic
26312631
i32.const 1
2632+
i32.symbolic
2633+
i32.const 0
2634+
i32.symbolic
26322635
call 6)
26332636
(memory (;0;) 2)
26342637
(export "main" (func 7))

‎benchmarks/wasm/btree/Makefile‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
# Makefile for building different versions of 2o1u-unlabeled.wat.cpp
2+
3+
CXX := g++
4+
SRC := 2o1u-unlabeled.wat.cpp
5+
HEADERS := ../../headers/
6+
LDFLAGS := -lz3
7+
CXXFLAGS := -g -I $(HEADERS) -std=c++17 -DENABLE_PROFILE -fno-omit-frame-pointer -O3 -DENABLE_PROFILE_TIME
8+
9+
.PHONY: all clean benchmark
10+
11+
all: 2o1u-unlabeled.wat.cpp.imm.no-snap.exe 2o1u-unlabeled.wat.cpp.imm.exe 2o1u-unlabeled.wat.cpp.no-snap.exe 2o1u-unlabeled.wat.cpp.exe \
12+
2o1u-unlabeled.wat.cpp.concolic.imm.no-snap.exe 2o1u-unlabeled.wat.cpp.concolic.imm.exe 2o1u-unlabeled.wat.cpp.concolic.no-snap.exe 2o1u-unlabeled.wat.cpp.concolic.exe 2o1u-unlabeled.wat.cpp.concolic.imm.cost-model.exe
13+
14+
2o1u-unlabeled.wat.cpp.exe: $(SRC)
15+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DRUN_ONCE
16+
17+
2o1u-unlabeled.wat.cpp.no-snap.exe: $(SRC)
18+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DNO_REUSE -DRUN_ONCE
19+
20+
2o1u-unlabeled.wat.cpp.imm.exe: $(SRC)
21+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DUSE_IMM -DRUN_ONCE
22+
23+
2o1u-unlabeled.wat.cpp.imm.no-snap.exe: $(SRC)
24+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DUSE_IMM -DNO_REUSE -DRUN_ONCE
25+
26+
27+
## Concolic execution tests
28+
2o1u-unlabeled.wat.cpp.concolic.exe: $(SRC)
29+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DBY_COVERAGE
30+
31+
2o1u-unlabeled.wat.cpp.concolic.no-snap.exe: $(SRC)
32+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DNO_REUSE -DBY_COVERAGE
33+
34+
2o1u-unlabeled.wat.cpp.concolic.imm.exe: $(SRC)
35+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DUSE_IMM -DBY_COVERAGE
36+
37+
2o1u-unlabeled.wat.cpp.concolic.imm.no-snap.exe: $(SRC)
38+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DUSE_IMM -DNO_REUSE -DBY_COVERAGE
39+
40+
2o1u-unlabeled.wat.cpp.concolic.imm.cost-model.exe: $(SRC)
41+
$(CXX) $< -o $@ $(CXXFLAGS) $(LDFLAGS) -DUSE_IMM -DNO_REUSE -DBY_COVERAGE -DUSE_COST_MODEL
42+
43+
benchmark: all
44+
hyperfine './2o1u-unlabeled.wat.cpp.imm.no-snap.exe' \
45+
'./2o1u-unlabeled.wat.cpp.imm.exe' \
46+
'./2o1u-unlabeled.wat.cpp.no-snap.exe' \
47+
'./2o1u-unlabeled.wat.cpp.exe'
48+
hyperfine './2o1u-unlabeled.wat.cpp.concolic.imm.no-snap.exe' \
49+
'./2o1u-unlabeled.wat.cpp.concolic.imm.exe' \
50+
'./2o1u-unlabeled.wat.cpp.concolic.no-snap.exe' \
51+
'./2o1u-unlabeled.wat.cpp.concolic.exe'
52+
clean:
53+
rm -f *.exe

‎benchmarks/wasm/call_indirect_test.wat‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
(module
2+
(type (;0;) (func (param i32) (result i32)))
3+
(type (;1;) (func (param i32 i32) (result i32)))
4+
(type (;2;) (func (result i32)))
5+
(func (;0;) (type 0) (param i32) (result i32)
6+
local.get 0
7+
i32.const 1
8+
i32.add)
9+
(func (;1;) (type 0) (param i32) (result i32)
10+
local.get 0
11+
i32.const 2
12+
i32.mul)
13+
(func (;2;) (type 1) (param i32 i32) (result i32)
14+
local.get 1
15+
local.get 0
16+
call_indirect (type 0))
17+
(func (;3;) (type 2) (result i32)
18+
i32.const 0
19+
i32.const 41
20+
call 2)
21+
(table (;0;) 2 funcref)
22+
(export "run" (func 3))
23+
(export "dispatch" (func 2))
24+
(elem (;0;) (i32.const 0) func 0 1)
25+
(start 3))

‎benchmarks/wasm/compare_wasp/Makefile‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
.PHONY: all run clean
2+
3+
all: large-branch.wat.cpp.imm.noreuse.exe large-branch.wat.cpp.imm.exe large-branch.wat.cpp.imm.cost-model.exe
4+
5+
large-branch.wat.cpp.imm.noreuse.exe: large-branch.wat.cpp
6+
g++ large-branch.wat.cpp -o large-branch.wat.cpp.imm.noreuse.exe -DUSE_IMM -I ../../../headers -lz3 -DENABLE_PROFILE_TIME -O3 -DNO_REUSE -DENABLE_PROFILE_STEP
7+
8+
large-branch.wat.cpp.imm.exe: large-branch.wat.cpp
9+
g++ large-branch.wat.cpp -o large-branch.wat.cpp.imm.exe -DUSE_IMM -I ../../../headers -lz3 -DENABLE_PROFILE_TIME -O3 -DENABLE_PROFILE_STEP
10+
11+
large-branch.wat.cpp.imm.cost-model.exe: large-branch.wat.cpp
12+
g++ large-branch.wat.cpp -o large-branch.wat.cpp.imm.cost-model.exe -DUSE_IMM -I ../../../headers -lz3 -DENABLE_PROFILE_TIME -O3 -DUSE_COST_MODEL
13+
14+
15+
run: all
16+
./large-branch.wat.cpp.imm.noreuse.exe
17+
./large-branch.wat.cpp.imm.exe
18+
19+
clean:
20+
rm -f *.exe

0 commit comments

Comments
 (0)