JS/Wasm binding linked against c++20 runtime instead of c++17 as expected by libz3

[asteadman]

I was experiencing an issue with heap corruption inside WASM using the javascript api.

While attempting to build the WASM module locally, I observed a linker error. (a missing symbol of _ZNKSt3__220__vector_base_commonILb1EE20__throw_length_errorEv)

It appears that libZ3 is compiled against c++17. This is well defined in scripts/mk_util.py. This seems intentional. Attempting to compile against c++20 does result in new warnings.

However, AFAICT, the last linker step of the WASM code links everything against c++20 (src/api/js/scripts/build-wasm.ts): emcc build/async-fns.cc ${libz3a} --std=c++20

This seems to be because async-fns.cc does use a c++20 extension.

build/async-fns.cc:12:18: warning: initialized lambda pack captures are a C++20 extension [-Wc++20-extensions]
  std::thread t([...args = std::forward<Args>(args)] {

To fix the linker error, I switched the wasm script to use c++17 instead. The version of clang I am using emits the above warning but otherwise compiles the code fine.

The heap corruption I was observing in the official wasm module no longer occurs on my local build. I'm not certain that's related, but it may be.

[asteadman]

(For googling purposes) The errors originally observed (the heap corruption) looked like this:

worker.js onmessage() captured an uncaught exception: RuntimeError: memory access out of bounds
RuntimeError: memory access out of bounds
    at small_object_allocator::allocate(unsigned long) (wasm://wasm/07992eca:wasm-function[5984]:0x3dc411)
    at default_expr_replacer_cfg::get_subst(expr*, expr*&, app*&) (wasm://wasm/07992eca:wasm-function[4083]:0x28fd5d)
    at bool rewriter_tpl<default_expr_replacer_cfg>::visit<false>(expr*, unsigned int) (wasm://wasm/07992eca:wasm-function[4082]:0x28f60c)
    at void rewriter_tpl<default_expr_replacer_cfg>::process_app<false>(app*, rewriter_core::frame&) (wasm://wasm/07992eca:wasm-function[4100]:0x295bbe)
    at void rewriter_tpl<default_expr_replacer_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) (wasm://wasm/07992eca:wasm-function[4095]:0x2921af)
    at void rewriter_tpl<default_expr_replacer_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) (wasm://wasm/07992eca:wasm-function[4092]:0x291011)
    at rewriter_tpl<default_expr_replacer_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) (wasm://wasm/07992eca:wasm-function[4087]:0x2905f6)
    at default_expr_replacer::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (wasm://wasm/07992eca:wasm-function[4107]:0x296aed)
    at invoke_viiiii (eval at importScripts (node_modules/z3-solver/build/z3-built.worker.js:39:16), <anonymous>:13648:29)
    at expr_replacer::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (wasm://wasm/07992eca:wasm-function[4078]:0x28ec02)
Pthread 0x01f9f728 sent an error! undefined:undefined: memory access out of bounds

However, it could manifest in other ways, with other callstacks. I also saw this one:

worker sent an error! undefined:undefined: Aborted(Runtime error: The application has corrupted its heap memory area (address zero)!)

node_modules/z3-solver/build/z3-built.js:4978
      throw ex;
      ^
Error [RuntimeError]: Aborted(Runtime error: The application has corrupted its heap memory area (address zero)!)
    at abort (eval at importScripts (node_modules/z3-solver/build/z3-built.worker.js:39:16), <anonymous>:6378:11)
    at checkStackCookie (eval at importScripts (node_modules/z3-solver/build/z3-built.worker.js:39:16), <anonymous>:6155:47)
    at Object.invokeEntryPoint (eval at importScripts (node_modules/z3-solver/build/z3-built.worker.js:39:16), <anonymous>:7081:7)
    at self.onmessage (node_modules/z3-solver/build/z3-built.worker.js:155:35)
    at MessagePort.<anonymous> (node_modules/z3-solver/build/z3-built.worker.js:25:5)
    at [nodejs.internal.kHybridDispatch] (node:internal/event_target:820:20)
    at MessagePort.<anonymous> (node:internal/per_context/messageport:23:28)

[NikolajBjorner]

Our WASM build has been broken for some time now. I hope this is related. Switching to C++20 may as well be the way to go.

[NikolajBjorner]

help @nunoplopes (to be replaced by AI)

../src/muz/transforms/dl_mk_array_instantiation.cpp:227:16: warning: ISO C++20 considers use of overloaded operator '!=' (with operand types 'expr_equiv_class::iterator' and 'obj_equiv_class<expr, ast_manager>::iterator') to be ambiguous despite there being a unique best viable function with non-reversed arguments [-Wambiguous-reversed-operator] it != eq_classes.end(array); ++it) { ~~ ^ ~~~~~ ../src/ast/rewriter/factor_equivs.h:110:14: note: candidate function with non-reversed arguments bool operator!=(const iterator& o) {return !(this == o);} ^ ../src/ast/rewriter/factor_equivs.h:106:14: note: ambiguous candidate function with reversed arguments bool operator==(const iterator& o) { ^ 1 warning generated. src/muz/transforms/dl_mk_array_blast.cpp src/muz/transforms/dl_mk_subsumption_checker.cpp src/muz/transforms/dl_mk_scale.cpp src/muz/transforms/dl_mk_filter_rules.cpp src/muz/transforms/dl_mk_backwards.cpp src/muz/transforms/dl_mk_array_eq_rewrite.cpp src/muz/transforms/dl_mk_karr_invariants.cpp src/muz/transforms/dl_mk_elim_term_ite.cpp ../src/muz/transforms/dl_mk_array_eq_rewrite.cpp:76:24: warning: ISO C++20 considers use of overloaded operator '!=' (with operand types 'obj_equiv_class<expr, ast_manager>::equiv_iterator' and 'obj_equiv_class<expr, ast_manager>::equiv_iterator') to be ambiguous despite there being a unique best viable function with non-reversed arguments [-Wambiguous-reversed-operator] for (auto c_eq : array_eq_classes) { ^ ../src/ast/rewriter/factor_equivs.h:159:14: note: candidate function with non-reversed arguments bool operator!=(const equiv_iterator& o) {return !(this == o);} ^ ../src/ast/rewriter/factor_equivs.h:155:14: note: ambiguous candidate function with reversed arguments bool operator==(const equiv_iterator& o) { ^ ../src/muz/transforms/dl_mk_array_eq_rewrite.cpp:78:27: warning: ISO C++20 considers use of overloaded operator '!=' (with operand types 'obj_equiv_class<expr, ast_manager>::iterator' and 'obj_equiv_class<expr, ast_manager>::iterator') to be ambiguous despite there being a unique best viable function with non-reversed arguments [-Wambiguous-reversed-operator] for (expr v : c_eq) { ^ ../src/ast/rewriter/factor_equivs.h:110:14: note: candidate function with non-reversed arguments bool operator!=(const iterator& o) {return !(this == o);} ^ ../src/ast/rewriter/factor_equivs.h:106:14: note: ambiguous candidate function with reversed arguments bool operator==(const iterator& o) { ^

[NikolajBjorner]

nope, c++20 did not save us:

Aborted(Cannot enlarge memory arrays to size 1073745920 bytes (OOM). Either (1) compile with -sINITIAL_MEMORY=X with X higher than the current value 1073741824, (2) compile with -sALLOW_MEMORY_GROWTH which allows increasing the size at runtime, or (3) if you want malloc to return NULL (0) instead of this abort, compile with -sABORTING_MALLOC=0)

[NikolajBjorner]

So we revert to c++17 and do:

To fix the linker error, I switched the wasm script to use c++17 instead. The version of clang I am using emits the above warning but otherwise compiles the code fine.

[nunoplopes]

help @nunoplopes (to be replaced by AI)

fixed here: https://github.com/Z3Prover/z3/commit/22d9bfad358eefaa2f7aa490983463f6b0dd022f

The functions were missing a const. While at it, I've removed the unneeded == operators.

AI bot at your service, sir.