@@ -37,21 +37,36 @@ 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
5065 def testFileConcreteCpp (filename : String , main : Option [String ] = None , expect : Option [List [Float ]] = None ) = {
5166 val moduleInst = ModuleInstance (Parser .parseFile(filename))
5267 val cppFile = s " $filename.cpp "
5368 val exe = s " $cppFile.exe "
54- WasmToCppCompiler .compileToExe(moduleInst, main, cppFile, exe, true , optimizeLevel= 0 , " NO_INFO" , " RUN_ONCE" )
69+ WasmToCppCompiler .compileToExe(moduleInst, main, cppFile, exe, true , optimizeLevel= 0 , " NO_INFO" , " RUN_ONCE" , " USE_IMM " )
5570
5671 import sys .process ._
5772 val result = s " ./ $exe" .!!
@@ -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