Fix memory lifetime bug in async array parameter handling for JS API (#8125)

* Initial plan

* Fix async array parameter handling in JS API wrappers

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add test for solver.check() with assumptions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: add null checks and improve readability

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add unsatCore() method to Solver class

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/js/scripts/make-cc-wrapper.ts

@@ -12,30 +12,118 @@ export function makeCCWrapper() {
     if (fn == null) {
       throw new Error(`could not find definition for ${fnName}`);
     }
-    let wrapper;
-    if (fn.cRet === 'Z3_string') {
-      wrapper = `wrapper_str`;
-    } else if (['int', 'unsigned', 'void'].includes(fn.cRet) || fn.cRet.startsWith('Z3_')) {
-      wrapper = `wrapper`;
-    } else {
-      throw new Error(`async function with unknown return type ${fn.cRet}`);
+    
+    // Check if function has array parameters
+    const arrayParams = fn.params.filter(p => p.isArray && p.kind === 'in_array');
+    const hasArrayParams = arrayParams.length > 0;
+    
+    if (hasArrayParams) {
+      // Generate custom wrapper for functions with array parameters
+      const paramList = fn.params.map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`).join(', ');
+      
+      // Find the size parameter for each array and build copy/free code
+      const arrayCopies: string[] = [];
+      const arrayFrees: string[] = [];
+      const arrayCopyNames: string[] = [];
+      
+      for (let p of arrayParams) {
+        const sizeParam = fn.params[p.sizeIndex!];
+        const ptrType = p.cType.endsWith('*') ? p.cType : `${p.cType}*`;
+        const copyName = `${p.name}_copy`;
+        arrayCopyNames.push(copyName);
+        
+        // Allocate and copy with null check
+        arrayCopies.push(`${ptrType} ${copyName} = (${ptrType})malloc(sizeof(${p.cType}) * ${sizeParam.name});`);
+        arrayCopies.push(`if (!${copyName}) {`);
+        arrayCopies.push(`  MAIN_THREAD_ASYNC_EM_ASM({ reject_async(new Error("Memory allocation failed")); });`);
+        arrayCopies.push(`  return;`);
+        arrayCopies.push(`}`);
+        arrayCopies.push(`memcpy(${copyName}, ${p.name}, sizeof(${p.cType}) * ${sizeParam.name});`);
+        
+        arrayFrees.push(`free(${copyName});`);
+      }
+      
+      // Build lambda capture list
+      const nonArrayParams = fn.params.filter(p => !p.isArray || p.kind !== 'in_array');
+      const captureList = [...arrayCopyNames, ...nonArrayParams.map(p => p.name)].join(', ');
+      
+      // Build argument list for the actual function call, using copied arrays
+      const callArgs = fn.params.map(p => {
+        if (p.isArray && p.kind === 'in_array') {
+          return `${p.name}_copy`;
+        }
+        return p.name;
+      }).join(', ');
+      
+      const isString = fn.cRet === 'Z3_string';
+      const returnType = isString ? 'auto' : fn.cRet;
+      
+      wrappers.push(
+        `
+extern "C" void async_${fn.name}(${paramList}) {
+  ${arrayCopies.join('\n  ')}
+  std::thread t([${captureList}] {
+    try {
+      ${returnType} result = ${fn.name}(${callArgs});
+      ${isString ? `
+      MAIN_THREAD_ASYNC_EM_ASM({
+        resolve_async(UTF8ToString($0));
+      }, result);
+      ` : `
+      MAIN_THREAD_ASYNC_EM_ASM({
+        resolve_async($0);
+      }, result);
+      `}
+    } catch (std::exception& e) {
+      MAIN_THREAD_ASYNC_EM_ASM({
+        reject_async(new Error(UTF8ToString($0)));
+      }, e.what());
+    } catch (...) {
+      MAIN_THREAD_ASYNC_EM_ASM({
+        reject_async(new Error('failed with unknown exception'));
+      });
     }
+    ${arrayFrees.join('\n    ')}
+    MAIN_THREAD_ASYNC_EM_ASM({
+      clearTimeout(threadTimeouts.shift());
+    });
+  });
+  t.detach();
+  EM_ASM({
+    threadTimeouts.push(setTimeout(() => {}, 600000));
+  });
+}
+`.trim(),
+      );
+    } else {
+      // Use template wrapper for functions without array parameters
+      let wrapper;
+      if (fn.cRet === 'Z3_string') {
+        wrapper = `wrapper_str`;
+      } else if (['int', 'unsigned', 'void'].includes(fn.cRet) || fn.cRet.startsWith('Z3_')) {
+        wrapper = `wrapper`;
+      } else {
+        throw new Error(`async function with unknown return type ${fn.cRet}`);
+      }
 
-    wrappers.push(
-      `
+      wrappers.push(
+        `
 extern "C" void async_${fn.name}(${fn.params
-        .map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
-        .join(', ')}) {
+          .map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
+          .join(', ')}) {
   ${wrapper}<decltype(&${fn.name}), &${fn.name}>(${fn.params.map(p => `${p.name}`).join(', ')});
 }
 `.trim(),
-    );
+      );
+    }
   }
 
   return `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
 // DO NOT EDIT IT BY HAND
 
 #include <thread>
+#include <cstdlib>
+#include <cstring>
 
 #include <emscripten.h>
 

src/api/js/scripts/make-ts-wrapper.ts

@@ -137,7 +137,7 @@ async function makeTsWrapper() {
 
     // otherwise fall back to ccall
 
-    const ctypes = fn.params.map(p =>
+    let ctypes = fn.params.map(p =>
       p.kind === 'in_array' ? 'array' : p.kind === 'out_array' ? 'number' : p.isPtr ? 'number' : toEmType(p.type),
     );
 
@@ -149,6 +149,8 @@ async function makeTsWrapper() {
     const args: (string | FuncParam)[] = fn.params;
 
     let arrayLengthParams = new Map();
+    let allocatedArrays: string[] = []; // Track allocated arrays for cleanup
+    
     for (let p of inParams) {
       if (p.nullable && !p.isArray) {
         // this would be easy to implement - just map null to 0 - but nothing actually uses nullable non-array input parameters, so we can't ensure we've done it right
@@ -179,6 +181,33 @@ async function makeTsWrapper() {
       }
       args[sizeIndex] = `${p.name}.length`;
       params[sizeIndex] = null;
+      
+      // For async functions, we need to manually manage array memory
+      // because ccall frees it before the async thread uses it
+      if (isAsync && p.kind === 'in_array') {
+        const paramIdx = fn.params.indexOf(p);
+        const ptrName = `${p.name}_ptr`;
+        allocatedArrays.push(ptrName);
+        // Allocate memory for array of pointers (4 bytes per pointer on wasm32)
+        prefix += `
+        const ${ptrName} = Mod._malloc(${p.name}.length * 4);
+        Mod.HEAPU32.set(${p.name} as unknown as number[], ${ptrName} / 4);
+        `.trim();
+        args[paramIdx] = ptrName;
+        ctypes[paramIdx] = 'number'; // Pass as pointer, not array
+      }
+    }
+    
+    // Add try-finally for async functions with allocated arrays
+    if (isAsync && allocatedArrays.length > 0) {
+      prefix += `
+      try {
+      `.trim();
+      suffix = `
+      } finally {
+        ${allocatedArrays.map(arr => `Mod._free(${arr});`).join('\n        ')}
+      }
+      `.trim() + suffix;
     }
 
     let returnType = fn.ret;

src/api/js/src/high-level/high-level.test.ts

@@ -174,6 +174,29 @@ describe('high-level', () => {
       expect(await solver.check()).toStrictEqual('unsat');
     });
 
+    it('can check with assumptions and get unsat core', async () => {
+      const { Bool, Solver } = api.Context('main');
+      const solver = new Solver();
+      solver.set('unsat_core', true);
+      
+      const x = Bool.const('x');
+      const y = Bool.const('y');
+      const z = Bool.const('z');
+
+      // Add conflicting assertions
+      solver.add(x.or(y));
+      solver.add(x.or(z));
+
+      // Check with assumptions that create a conflict
+      // This tests the async array parameter fix
+      const result = await solver.check(x.not(), y.not(), z.not());
+      expect(result).toStrictEqual('unsat');
+      
+      // Verify we can get the unsat core
+      const core = solver.unsatCore();
+      expect(core.length()).toBeGreaterThan(0);
+    });
+
     it("proves De Morgan's Law", async () => {
       const { Bool, Not, And, Eq, Or } = api.Context('main');
       const [x, y] = [Bool.const('x'), Bool.const('y')];

src/api/js/src/high-level/high-level.ts

@@ -1463,6 +1463,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new ModelImpl(check(Z3.solver_get_model(contextPtr, this.ptr)));
       }
 
+      unsatCore(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_unsat_core(contextPtr, this.ptr)));
+      }
+
       toString() {
         return check(Z3.solver_to_string(contextPtr, this.ptr));
       }

src/api/js/src/high-level/types.ts

@@ -713,6 +713,8 @@ export interface Solver<Name extends string = 'main'> {
 
   model(): Model<Name>;
 
+  unsatCore(): AstVector<Name, Bool<Name>>;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,