Skip to content

Commit 57f5eeb

Browse files
a simple test case to show immutable's improvements
1 parent e4ac385 commit 57f5eeb

File tree

2 files changed

+73
-0
lines changed

2 files changed

+73
-0
lines changed
Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
(module
2+
(type (;0;) (func))
3+
(type (;1;) (func (param i32)))
4+
(import "console" "assert" (func (type 1)))
5+
(func (;1;) (type 0)
6+
(local i32 i32)
7+
i32.const 1
8+
local.set 0
9+
i32.const 0
10+
local.set 1
11+
block
12+
loop
13+
local.get 0
14+
i32.const 10000
15+
i32.ge_s
16+
br_if 1
17+
local.get 1
18+
i32.const 0
19+
i32.add
20+
local.set 1
21+
local.get 0
22+
i32.const 1
23+
i32.add
24+
local.set 0
25+
br 0
26+
end
27+
end
28+
i32.const 10000
29+
local.set 0
30+
i32.const 0
31+
local.set 1
32+
block
33+
loop
34+
local.get 0
35+
i32.eqz
36+
br_if 1 ;; break if counter == 0
37+
local.get 1
38+
i32.const 0
39+
i32.sub ;; acc - 0 (no change)
40+
local.set 1
41+
local.get 0
42+
i32.const 1
43+
i32.sub
44+
local.set 0 ;; counter--
45+
br 0 ;; repeat loop
46+
end
47+
end
48+
local.get 1
49+
if
50+
i32.const 0
51+
call 0
52+
end
53+
)
54+
(start 1))

src/test/scala/genwasym/TestStagedConcolicEval.scala

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,13 +37,28 @@ class TestStagedConcolicEval extends FunSuite {
3737
println(result)
3838
exploreTreeFile
3939
}
40+
val exploreTreeFileImm = {
41+
// Do concolic execution with immutable data structure and snapshot reuse
42+
val exe = s"$cppFile.imm.exe"
43+
val exploreTreeFile = s"$filename.imm.tree.dot"
44+
WasmToCppCompiler.compileToExe(moduleInst, main, cppFile, exe, true, optimizeLevel=0, if (exitByCoverage) "BY_COVERAGE" else "EARLY_EXIT", "USE_IMM")
45+
println(s"Running compiled concolic execution with immutable data structure and snapshot reuse: $exe")
46+
val result = Process(s"./$exe", None, "TREE_FILE" -> exploreTreeFile).!!
47+
println(result)
48+
exploreTreeFile
49+
}
4050
// The explore tree generated by two executions should be same
4151
import java.nio.file.Files
4252
assert(
4353
Files.readAllBytes(java.nio.file.Paths.get(exploreTreeFile))
4454
sameElements Files.readAllBytes(java.nio.file.Paths.get(exploreTreeFileNoReuse)),
4555
s"Explore trees $exploreTreeFile and $exploreTreeFileNoReuse are different!"
4656
)
57+
assert(
58+
Files.readAllBytes(java.nio.file.Paths.get(exploreTreeFile))
59+
sameElements Files.readAllBytes(java.nio.file.Paths.get(exploreTreeFileImm)),
60+
s"Explore trees $exploreTreeFile and $exploreTreeFileImm are different!"
61+
)
4762
}
4863

4964
// only test concrete execution and its result
@@ -98,6 +113,10 @@ class TestStagedConcolicEval extends FunSuite {
98113
}
99114
test("btree-bug-finding-concolic") { testFileConcolicCpp("./benchmarks/wasm/btree/2o1u-unlabeled.wat", exitByCoverage = true) }
100115

116+
test("long-trivial-execution-concrete") {
117+
// This is a example to show how much performance improvement we can get by immutable data structure
118+
testFileConcreteCpp("./benchmarks/wasm/staged/long-trivial-execution.wat", None)
119+
}
101120

102121
test("return-poly - concrete") {
103122
testFileConcreteCpp("./benchmarks/wasm/staged/return_poly.wat", Some("$real_main"), expect=Some(List(42)))

0 commit comments

Comments
 (0)