Closed2024/08/27にクローズ11

ExpoSE起動するぞ

canalun

https://github.com/ExpoSEJS/ExpoSE　これのこと。
ec03edf85f883248612b1d498c6a7d9189d16d6f　から始める。

自分の環境は下記。

canalun

自分の環境は前からnpmがあまりワークしないので、全体的にyarnに直してみる。
ただし./scripts/docker-setupはやったらダメ(dockerにはyarnを入れていないようなので)。

canalun

./Browserのelectornが古すぎるので、^13.1.7にする。とにかくyarn installでエラーが出ないバージョンなら一旦良しとする。

canalun

nodeバージョンを固定する。具体的には

expoSE自体は21.7.2を指定されているので、そうする。
./Analyser配下は21.5.0にする。node-ffi-napiのために。

自分はvoltaを使っているので、コマンドはこれ。

$ pwd
/Users/XXXXXX/ExpoSE
$ volta pin node@21.7.2
success: pinned node@21.7.2 (with npm@10.5.0) in package.json
$ cd ./Analyser
$ volta pin node@21.5.0
success: pinned node@21.5.0 (with npm@10.2.4) in package.json

一応こうなった。
それぞれのpackage.jsonでvoltaで指定している

canalun

./installをすると成功する。

ただ実行してみると、今度はarch関連のエラー。なお、デバッグのためにEXPOSE_PRINT_PATHS=1をつけるといいらしい。

$ EXPOSE_PRINT_PATHS=1 ./expoSE ./tests/numbers/infoflow
[+] ExpoSE /Users/XXXXXX/ExpoSE/tests/numbers/infoflow concurrent: 10 timeout: 7200000 per-test: 2400000
[\] [0 done /0 queued / 1 running / 0 errors / 0% coverage ] ***/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/node_modules/@makeomatic/ffi-napi/lib/dynamic_library.js:75
    throw new Error('Dynamic Linking Error: ' + err);
    ^

Error: Dynamic Linking Error: dlopen(./node_modules/z3javascript/bin/libz3.dylib, 0x0002): tried: './node_modules/z3javascript/bin/libz3.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e' or 'arm64')), '/System/Volumes/Preboot/Cryptexes/OS./node_modules/z3javascript/bin/libz3.dylib' (no such file), '/usr/lib/./node_modules/z3javascript/bin/libz3.dylib' (no such file, not in dyld cache), './node_modules/z3javascript/bin/libz3.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e' or 'arm64')), '/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/bin/libz3.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e' or 'arm64')), '/System/Volumes/Preboot/Cryptexes/OS/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/bin/libz3.dylib' (no such file), '/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/bin/libz3.dylib' (mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e' or 'arm64'))
    at new DynamicLibrary (/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/node_modules/@makeomatic/ffi-napi/lib/dynamic_library.js:75:11)
    at Object.Library (/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/node_modules/@makeomatic/ffi-napi/lib/library.js:47:10)
    at module.exports (/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/bin/package.js:768:14)
    at Object.<anonymous> (/Users/XXXXXX/ExpoSE/Analyser/node_modules/z3javascript/bin/Z3Loader.js:12:37)
    at Module._compile (node:internal/modules/cjs/loader:1368:14)
    at Module._extensions..js (node:internal/modules/cjs/loader:1426:10)
    at Module.load (node:internal/modules/cjs/loader:1205:32)
    at Module._load (node:internal/modules/cjs/loader:1021:12)
    at Module.require (node:internal/modules/cjs/loader:1230:19)
    at require (node:internal/modules/helpers:179:18)

Node.js v21.7.2
[|] [1 done /0 queued / 0 running / 1 errors / 0% coverage ] ***
[+] {"_bound":0} took 0.567s
[!] Exception E: SyntaxError: Unexpected end of JSON input of coverage data on
[!] Exception E: SyntaxError: Unexpected end of JSON input of test data on
[!] Exit code non-zero
[!] Error extracting final output - a fatal error must have occured
[!] expoSE replay /Users/XXXXXX/ExpoSE/tests/numbers/infoflow '{"_bound":0}'
[!] Stats
[!] Done
[+] Total Lines Of Code 0
[+] Total Coverage: NaN%
[+] EXPOSE_PRINT_COVERAGE=1 for line by line breakdown
[+] ExpoSE Finished. 1 paths, 1 errors

canalun

mach-o file, but is an incompatible architecture (have 'x86_64', need 'arm64e' or 'arm64')
について調べると、要はM1チップ問題なので、rosettaをいれる。(入ってなかった👶)

softwareupdate --install-rosetta --agree-to-license

canalun

ビルドしなおそう、ということで、あらためてここに書いてあることを最初からやってみる。

canalun

だめだ。ちゃんと丁寧に、arch -arm64でビルドする専用のz3javascriptのforkを作ってもぜんぜん機能しない。

canalun

ということで、下記からz3のarm64ビルドをありがたく頂戴して入れ替えたら動いた。
https://github.com/Z3Prover/z3/releases
(z3-X.X.X-arm64-osx-X.X.zipみたいなやつ)

canalun

まとめると、下記で動いた

(前提: 私はいまM1 Macを使っています)
下記をやったら動きました
- 全体的にyarnにする
- ./Browserのelectornをエラーが出ない程度に新しくしておく
- nodeバージョンを固定する
  - expoSE自体は21.7.2
  - ./Analyser配下は21.5.0(node-ffi-napi)
- ./installを実行する
- 最後に、z3のarm64ビルドをreleasesから取ってきて、その中のlibz3.dylibを./Analyser/node_modules/z3javascript/bin/libz3.dylibと入れ替える

canalun

というわけで、forkして作っておいた。
これをcloneして、makeすれば動く👶(自分の手元では！！！！！)
ghを使っているよ。あと、オリジナルにはないんだけど、いちおうlockファイルもコミットしてある。

$ git clone git@github.com:canalun/ExpoSE-for-m1mac.git
$ make

このスクラップは2024/08/27にクローズされました