search

bramvdbogaerde / z3-wasm

Scripts and Javascript Glue code to use Z3 in the browser using WASM
13 stars 7 forks source link

Uncaught exception when running solve with non-trivial examples #1

Closed bramvdbogaerde closed 3 years ago

bramvdbogaerde commented 3 years ago

When using non-trivial SMTlib code, the WASM module throws an exception.

Example program

(declare-const x Int)
(assert (= x 5))
(check-sat)

The exception is generated from the compiled C++ code, and must be viewed by following the memory addresses that are intercepted by the Emscripten runtime.

philzook58 commented 3 years ago

I've had some luck adding pthread related options. I'm not exactly sure what combo is important but it is working better than before. 

CXXFLAGS="-pthread -s DISABLE_EXCEPTION_CATCHING=0 -s USE_PTHREADS=1" emconfigure python scripts/mk_make.py --staticlib
...
emcc api/api.c $Z3_BASE_DIR/build/libz3.a -fexceptions -pthread -s EXPORTED_FUNCTIONS='["_init_context", "_destroy_context", "_eval_smt2"]' -s DISABLE_EXCEPTION_CATCHING=0 -s EXCEPTION_DEBUG=1 -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=4 -s TOTAL_MEMORY=1GB -I $Z3_BASE_DIR/src/api/ --post-js api/api.js -o out/z3.js

https://github.com/philzook58/z3-wasm/blob/master/build.sh#L40

bramvdbogaerde commented 3 years ago

Interesting, I will check later today.

bramvdbogaerde commented 3 years ago

It might have something to do with this. I am attempting to build using the pthread option, but would evidently prefer another solution due to the required COP headers.

bramvdbogaerde commented 3 years ago

Indeed, activating pthread seems to resolve the issue.