An asm.js/WebAssembly build of the CVC4 SMT solver. Try it at https://people.csail.mit.edu/cpitcla/cvc4.js/cvc4.html (Javascript/asm.js) and https://people.csail.mit.edu/cpitcla/cvc4.wasm/cvc4.html (WebAssembly).

Install Vagrant, then clone this repo and run vagrant up in the vm/ directory. This will create a cvc4-js folder, and a cvc4.js file in the CVC4 subfolder. The script shows high-level steps; more detailed output is redirected to provision.log. Building takes roughly 5 hours on the first build (3 hours to compile Clang, 1 hour to compile CVC4 and its dependencies, and 1 hour to transpile). For subsequent builds, you can use vagrant ssh to log into the VM and run individual commands.

See the demo in the html folder.

cd /vagrant/cvc4-js/CVC4/builds/i686-pc-linux-gnu/production-staticbinary-nodebugsymbols-noassertions-notracing/
# Back up the LLVM bitcode
mv src/main/cvc4{,.native}
# Replace `cvc4` with a node.js wrapper
ln -s /vagrant/run-cvc4.js src/main/cvc4
# Make sure that `make` doesn't rebuild `cvc4`
touch src/main/cvc4
# Run the tests
make test

• Installing emsdk builds clang; passing the --build=Release ensures that the build doesn't run out of memory.
• emcc is pretty stack-heavy — it needs ulimit -s unlimited. Since it's a node program, ~/.emscripten also needs to be edited to call node with the appropriate --stack-size.
• GMP doesn't build cleanly on a 64-bits host (it produces a bunch of warnings). To cross-compile you need to build the gen-* programs on their own first (the GMP build process uses C++ programs to generate some of the sources), then recompile with emmake. GMP also uses regparm, which fails on x64, though using -fPIC disables that. That's why we build in a 32-bits VM.
• CVC4 depends on boost. Since boost is header-only that shouldn't be a problem, but when boost gets auto-included it also pulls in all the other system libraries, and everything breaks. See http:https://vclf.blogspot.com/2014/08/emscripten-linking-to-boost-libraries.html. The workaround is to symlink the boost folder into an otherwise empty directory and -L that instead.
• CVC4 uses sigaltstack, which isn't supported in emscripten. Solved by cvc5/cvc5#172.
• CVC4 needs a bunch of specific emcc flags to run properly. See vm/provision.sh.
  • OUTLINING_LIMIT: The problem is that the option parsing routine in CVC4 is huge (53MB of bitcode), which crashes the Javascript/WASM parsers of both Chromium and Firefox. Emscripten can split (“outline”) these, but the threshold needs to be chosen carefully: if it's too low, emcc starts outlining other functions, including a few large recursive ones in CVC4's SMT parser, which causes stack overflows at run time; but if it's too high, loading compiled programs takes forever or causes stack overflows in the parser.
  • BINARYEN_ASYNC_COMPILATION: Async compilation of the WebAssembly code causes Firefox to infloop, repeatedly printing “still waiting on run dependencies: dependency: wasm-instantiate”.
  • NO_EXIT_RUNTIME: Exiting the runtime after the first execution causes “Invalid function pointer called with signature 'vi'.” on subsequent runs.
• There is a bug in the latest release of emscripten (fixed in incoming) that makes it impossible to run the test suite in Node (emscripten-core/emscripten#5239), but the incoming branch has another bug (emscripten-core/emscripten#5323) that makes it unusable without edits to the asm.js output.