JS (High-level) - Eventual memory corruption

[AiBobby]

In trying to track down a memory corruption bug that I think might be related to z3, I rebuilt 4.15.2 with the the additional CXXFLAGS -fsanitize=address and -fno-omit-frame-pointer, and with debug and tracing turned on when configuring the make file here. I also included -fsanitize=address in the emcc step here.

Once this was built (with build:wasm and build:ts), I ran this simple test against it:

      const { Context } = await init();
      const ctx = Context('main');

      for (var i = 0; i < 2; i++) {
        const solver = new ctx.Solver();
        const res = await solver.check();

        console.log(`Result ${i + 1}:`, res);
        solver.release();
      }

The first time through the loop, all seems well and it prints 'sat' as a result. However, the second pass is where ASan reports a null-pointer-dereference

The full error and call stack:

z3-built.js:2938 SUMMARY: AddressSanitizer: null-pointer-dereference (this.program+0x101488a) in ptr_hash_entry<char const>::is_used() const+0x101488a
put_char	@	z3-built.js:2938
write	@	z3-built.js:2887
write	@	z3-built.js:4553
doWritev	@	z3-built.js:6146
_fd_write	@	z3-built.js:6167
$__sanitizer::internal_write(int, void const*, unsigned long)	@	z3-built.wasm:0x8e20fdd
$__sanitizer::ReportFile::Write(char const*, unsigned long)	@	z3-built.wasm:0x8e218a3
$__sanitizer::RawWrite(char const*)	@	z3-built.wasm:0x8e1db96
$__sanitizer::SharedPrintfCodeNoBuffer(bool, char*, int, char const*, void*)	@	z3-built.wasm:0x8e22590
$__sanitizer::SharedPrintfCode(bool, char const*, void*)	@	z3-built.wasm:0x8e223ec
$__sanitizer::Printf(char const*, ...)	@	z3-built.wasm:0x8e223bc
$__sanitizer_report_error_summary	@	z3-built.wasm:0x8e1c3e3
$__sanitizer::ReportErrorSummary(char const*, char const*)	@	z3-built.wasm:0x8e1c39c
$__sanitizer::ReportErrorSummary(char const*, __sanitizer::AddressInfo const&, char const*)	@	z3-built.wasm:0x8e28c09
$__sanitizer::ReportErrorSummary(char const*, __sanitizer::StackTrace const*, char const*)	@	z3-built.wasm:0x8e28d9b
$__asan::ErrorGeneric::Print()	@	z3-built.wasm:0x8e0761f
$__asan::ErrorDescription::Print()	@	z3-built.wasm:0x8e0f748
$__asan::ScopedInErrorReport::~ScopedInErrorReport()	@	z3-built.wasm:0x8e0f149
$__asan::ReportGenericError(unsigned long, unsigned long, unsigned long, unsigned long, bool, unsigned long, unsigned int, bool)	@	z3-built.wasm:0x8e11b39
$__asan_report_load4	@	z3-built.wasm:0x8e12136
$ptr_hash_entry<char const>::is_used() const	@	z3-built.wasm:0x101488e
$core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::insert_if_not_there_core(char const*&&, ptr_hash_entry<char const>*&)	@	z3-built.wasm:0x1012996
$core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::insert_if_not_there_core(char const* const&, ptr_hash_entry<char const>*&)	@	z3-built.wasm:0x100d902
$(anonymous namespace)::internal_symbol_table::get_str(char const*)	@	z3-built.wasm:0x100d1fd
$symbol::symbol(char const*)	@	z3-built.wasm:0x100ce20
$solver_params::smtlib2_log() const	@	z3-built.wasm:0x334702
invoke_ii	@	z3-built.js:8188
$init_solver_log(_Z3_context*, _Z3_solver*)	@	z3-built.wasm:0x332d0d
invoke_vii	@	z3-built.js:8210
$Z3_mk_solver	@	z3-built.wasm:0x335f0d
(anonymous)	@	z3-built.js:950
testZ3Crash

Looking at the code for smtlib2_log I see that it contains a call to symbol() with an empty string which raises some suspicion in me but I'm not super familiar with what is happening in the z3 internals in general. Any help would be greatly appreciated.

[bakkot]

Huh. It's pretty easy to instrument the package to trace all the calls from the high level API into the low level API, but after doing so I don't see anything obviously wrong.

like this

edit build/low-level/wrapper.GENERATED.js to replace return { em: Mod, Z3: { ... with let o = { em: Mod, Z3: { ..., and then after that statement add

for (let [k, v] of Object.entries(o.Z3)) {
  o.Z3[k] = function(...args) {
    var out = v.apply(this, args);
    if (out == null) {
      console.log(`${k}(${args.join(', ')})`);
    } else {
      console.log(`${k}(${args.join(', ')}) = ${out}`);
    }
    return out;
  };
}

return o;

Output is

mk_config() = 21496696
mk_context_rc(21496696) = 21496768
set_ast_print_mode(21496768, 2)
del_config(21496696)
mk_solver(21496768) = 21496696
solver_inc_ref(21496768, 21496696)
solver_check_assumptions(21496768, 21496696, ) = [object Promise]
get_error_code(21496768) = 0
Result 1: sat
solver_dec_ref(21496768, 21496696)
mk_solver(21496768) = 51173800
solver_inc_ref(21496768, 51173800)
solver_check_assumptions(21496768, 51173800, ) = [object Promise]
get_error_code(21496768) = 0
Result 2: sat
solver_dec_ref(21496768, 51173800)

which seems basically reasonable - no double-decrements or anything.

I wonder if the same happens when building natively with ASan. Unfortunately I am unlikely to have time to look into further this in the near future.

[NikolajBjorner]

it isn't a problem to pass nullptr to the symbol constructor. Z3_open_log(logfilename.log) before any other z3 calls, rerun crash using z3.exe?