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

// generates c wrappers with off-thread versions of specified functions

import path from 'path';
import { asyncFuncs } from './async-fns';
import { functions } from './parse-api';

export function makeCCWrapper() {
  let wrappers = [];

  for (let fnName of asyncFuncs) {
    let fn = functions.find(f => f.name === fnName);
    if (fn == null) {
      throw new Error(`could not find definition for ${fnName}`);
    }

    // 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(
        `
extern "C" void async_${fn.name}(${fn.params
          .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>

#include "../../z3.h"

template<typename Fn, Fn fn, typename... Args>
void wrapper(Args&&... args) {
  std::thread t([...args = std::forward<Args>(args)] {
    try {
      auto result = fn(args...);
      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('failed with unknown exception');
      });
    }
    MAIN_THREAD_ASYNC_EM_ASM({
      // this clears the earliest timeout
      // not necessarily the one corresponding to this thread
      // but that's ok
      clearTimeout(threadTimeouts.shift());
    });
  });
  t.detach();
  EM_ASM({
    // https://github.com/emscripten-core/emscripten/issues/23092
    // in Node.js, the process will die if there is no active work
    // which can happen while the thread is spawning
    // or while it is running
    // so we set a timeout here so it stays alive
    // this needs to be longer than it could conceivably take to call the one function
    // it gets cleared as soon as the thread actually finishes
    threadTimeouts.push(setTimeout(() => {}, 600000));
  });
}

template<typename Fn, Fn fn, typename... Args>
void wrapper_str(Args&&... args) {
  std::thread t([...args = std::forward<Args>(args)] {
    try {
      auto result = fn(args...);
      MAIN_THREAD_ASYNC_EM_ASM({
        resolve_async(UTF8ToString($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'));
      });
    }
    MAIN_THREAD_ASYNC_EM_ASM({
      // this clears the earliest timeout
      // not necessarily the one corresponding to this thread
      // but that's ok
      clearTimeout(threadTimeouts.shift());
    });
  });
  t.detach();
  EM_ASM({
    // https://github.com/emscripten-core/emscripten/issues/23092
    // in Node.js, the process will die if there is no active work
    // which can happen while the thread is spawning
    // or while it is running
    // so we set a timeout here so it stays alive
    // this needs to be longer than it could conceivably take to call the one function
    // it gets cleared as soon as the thread actually finishes
    threadTimeouts.push(setTimeout(() => {}, 600000));
  });
}



class Z3Exception : public std::exception {
public:
  const std::string m_msg;
  Z3Exception(const std::string& msg) : m_msg(msg) {}
  virtual const char* what() const throw () {
    return m_msg.c_str();
  }
};

void throwy_error_handler(Z3_context ctx, Z3_error_code c) {
  throw Z3Exception(Z3_get_error_msg(ctx, c));
}

void noop_error_handler(Z3_context ctx, Z3_error_code c) {
  // pass
}

extern "C" void set_throwy_error_handler(Z3_context ctx) {
  Z3_set_error_handler(ctx, throwy_error_handler);
}

extern "C" void set_noop_error_handler(Z3_context ctx) {
  Z3_set_error_handler(ctx, noop_error_handler);
}

${wrappers.join('\n\n')}
`;
}

if (require.main === module) {
  console.log(makeCCWrapper());
}