Skip to content

Conversation

@butterunderflow
Copy link
Contributor

@butterunderflow butterunderflow commented Jul 9, 2025

The starting point of this PR is src/main/scala/wasm/StagedMiniWasm.scala, which is a staged interpreter of MiniWasm that generates C++ code.
By extending src/main/scala/wasm/StagedMiniWasm.scala with symbolic semantics, we got src/main/scala/wasm/StagedConcolicMiniWasm.scala, which is a concolic staged interpreter that generates concolic C++ code.
Combine the generated code with the runtime defined in headers/wasm/ we can achieve compiled concolic execution for WebAssembly.
The generated C++ code looks like this:

std::monostate Snippet(std::monostate x0) {
  // the logic of the entry function
  ...
}
int main(int argc, char *argv[]) {
  start_concolic_execution_with(Snippet, 2);
  return 0;
}

where Snippet is the generated concolic function corresponding to the entry
function of the input WebAssembly module, and start_concolic_execution_with a
C++ runtime function defined that manages the concolic execution process.

To test this feature, you can run:

sbt 'testOnly gensym.wasm.TestStagedConcolicEval'

To use this feature to compile a particular WebAssembly module, you can run this sbt test command:

INPUT=<path-to-your-wat-file> sbt 'testOnly gensym.wasm.TestBenchmark -- -z compile-a-single-file'

@butterunderflow butterunderflow force-pushed the zdh/staged-symbolic-miniwasm branch from 41858de to 61215b6 Compare July 9, 2025 15:18
@butterunderflow butterunderflow force-pushed the zdh/staged-symbolic-miniwasm branch from ce6489c to 314ff5f Compare July 16, 2025 15:58
Comment on lines 262 to 271
ExploreTree.fillWithIfElse(cond.s)
if (cond.toInt != 0) {
info(s"Jump to $label")
ExploreTree.moveCursor(true)
trail(label)(newCtx)(mkont)
} else {
info(s"Continue")
ExploreTree.moveCursor(false)
eval(rest, kont, mkont, trail)(newCtx)
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO: if cons.s is SymVal.Concrete, then do not fork on Exploration Tree
A test case will be a straight line for an exploration tree with a bunch of SymVal

Same for If, BrTable, and other control flow constructs

To run larger benchmarks, we must have this
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants