make it work

VeriFIT · Jan 1, 2025 · ee6dbea · ee6dbea
1 parent cae2540
commit ee6dbea
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 14 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -170,10 +170,8 @@ endif()
 # target_include_directories(libz3 PRIVATE ${PROJECT_SOURCE_DIR}/extern/lib/mata/include)
 # target_link_libraries(libz3 PRIVATE libmata)
 
-if (NOT EMSCRIPTEN)
-  find_library(LIBMATA mata)
-  target_link_libraries(libz3 PRIVATE ${LIBMATA})
-endif()
+find_library(LIBMATA mata)
+target_link_libraries(libz3 PRIVATE ${LIBMATA})
 
 # This is currently only for the OpenMP flags. It needs to be set
 # via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`

diff --git a/src/api/js/README.md b/src/api/js/README.md
@@ -12,12 +12,38 @@ You'll need to have emscripten set up, along with all of its dependencies. The e
 Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeScript wrapper, and `npm run build:wasm` to build the wasm artifact.
 
 Detailed instruction for binding building for Z3-Noodler:
-1. create folder `build-wasm` for the WASM build of libz3.a
-2. inside `build-wasm` run `emcmake cmake -DZ3_BUILD_LIBZ3_SHARED=FALSE -DZ3_SINGLE_THREADED=TRUE ..`
-3. build WASM library using `emmake make libz3` (the static library `libz3.a` should be created after that)
-4. copy the WASM static library of `mata` to `build-wasm` (see instructions in the Mata repository for the WASM build)
-5. run `npm i`, `npm run build:ts`, and `npm run build:wasm` 
-
+1) Get emscripten trough [emsdk](https://github.com/emscripten-core/emsdk) and :
+    ```shell
+    git clone 'https://github.com/emscripten-core/emsdk'
+    cd emdsk
+    ./emsdk install 3.1.73
+    ./emsdk activate 3.1.73
+    source emsdk_env.sh
+    cd ..
+    ```
+2) Get and install [Mata](https://github.com/VeriFIT/mata/) library (it will be installed into `emsdk` environment):
+    ```shell
+    git clone 'https://github.com/VeriFIT/mata.git'
+    cd mata
+    mkdir build && cd build
+    emcmake cmake -DCMAKE_BUILD_TYPE=Release -DMATA_BUILD_EXAMPLES:BOOL=OFF -DBUILD_TESTING:BOOL=OFF ..
+    emmake make install
+    cd ..
+    ```
+3) Find the line on the installation output that contains the path to `libmata.a` and copy this path on line 77 of `scripts/build-wasm.ts`
+4) Create an empty `build` directory in the root of `z3-noodler` directory.
+5) From this directory run following commands to build the binding:
+    ```shell
+    npm install
+    npm run build:ts
+    npm run build:wasm
+    ```
+6) You can add dependency to this binding by adding the following to your `package.json` file:
+```
+"dependencies": {
+    "z3-solver": "file: PATH/TO/THIS/DIRECTORY"
+}
+```
 
 ### Build on your own
 

diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts
@@ -59,12 +59,12 @@ const z3RootDir = path.join(process.cwd(), '../../../');
 
 // TODO(ritave): Detect if it's in the configuration we need
 if (!existsSync(path.join(z3RootDir, 'build/Makefile'))) {
-  spawnSync('emconfigure python scripts/mk_make.py --staticlib --single-threaded --arm64=false', {
-    cwd: z3RootDir,
+  spawnSync('emcmake cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_LIBZ3_SHARED=FALSE -DZ3_SINGLE_THREADED=TRUE ..', {
+    cwd: path.join(z3RootDir, 'build'),
   });
 }
 
-spawnSync(`emmake make -j${os.cpus().length} libz3.a`, { cwd: path.join(z3RootDir, 'build') });
+spawnSync(`emmake make -j${os.cpus().length} libz3`, { cwd: path.join(z3RootDir, 'build') });
 
 const ccWrapperPath = 'build/async-fns.cc';
 console.log(`- Building ${ccWrapperPath}`);
@@ -74,8 +74,9 @@ fs.writeFileSync(ccWrapperPath, makeCCWrapper());
 const fns = JSON.stringify(exportedFuncs());
 const methods = '["PThread","ccall","FS","UTF8ToString","intArrayFromString"]';
 const libz3a = path.normalize('../../../build/libz3.a');
+const libmata = path.normalize('REPLACE THIS TEXT WITH THE PATH TO libmata.a');
 spawnSync(
-  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
+  `emcc build/async-fns.cc ${libz3a} ${libmata} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
 );
 
 fs.rmSync(ccWrapperPath);