Ts/Go bindings

[aestriplex]

@NikolajBjorner I closed the issue #5736 and I moved here the discussion, in order to keep clean the issues board.
Unfortunately I don't know much about WebAssembly, so I cannot contribute to that part of the codebase. Nevertheless, if you think it could be an audience for either Ts or Go bindings, I can start working on it. For what concerns Ts/JS, yes, there is a SWIG interface available for C++, so I would start from that.

[NikolajBjorner]

Thanks for transferring it, I should have done so already.

Coincidentally I learned yesterday that there is a repository with go bindings.
https://github.com/mitchellh/go-z3 by @mitchellh.
The project was around 4 days of active development but seems not in an active state with occasional user requests.

I think the model used for the Julia bindings would be easier to manage:

• It builds on top of C++ so adding another function is one line in a file.
  • the typical issue with evolving the bindings is that the underlying C API changes slightly or gets new functionality that isn't included.
  • examples: optimization API, functions for building regular expression terms.
• It is integrated with Azure pipelines (it could have a separate GitHub Action, but we didn't use them when adding Julia bindings).

We stopped short, very unfortunately, of other steps that would be useful:

• running BVT tests on the bindings.
• generating artifacts (as part of release.yml)

[aestriplex]

I looked at the Go bindings in https://github.com/mitchellh/go-z3. I agree with you; the model used for the Julia bindings it's definitely easier to manage and even to maintain. This week I'll start working on it. From time to time I'll notify here the status of the work.
For now, I'd like to thank you for your helpfulness.

(I also changed the title of the discussion in order to include Go)

[NikolajBjorner]

Thanks! I am not well tuned into what is required for ts over C++ so will definitely love to see whether it works out and it is likely others can benefit. You are invited eventually add a pull request similar to julia bindings if you have an opportunity to. This would allow the bindings to evolve with the API and be easier discoverable (an npm package is likely even more discoverable).

[aestriplex]

One last thing: are there any best practices/ code style guidelines for contributors? I cannot find them on the repository

[NikolajBjorner]

For language bindings we have adapt conventions that are more common to the external language. So I would not worry about this.
At this point we generate doxygen output, with hooks for API bindings for Java, C#, Ocaml. For python it is help strings.

For C++ code it is 4 spaces and one of the C++ conventions where you put space after "if", "for", "while" and "{" on the same line as "for/while/else". Auto-format in VS after you set 4 spaces takes care much of it. There is no style file for details checked in, unfortunately.

[aestriplex]

Hi @NikolajBjorner, happy new year!

I began working on the bindings. In particular, I started considering the tools available for such a task. Here's the result:

• SWIG. Although it's a popular tool, I think it wouldn't be appropriate for maintaining the bindings for such a complex project. Indeed, the official documentation says

  The primary development environment has been Linux (Ubuntu 12.04). Windows and Mac OS X have been tested sporadically. Therefore, the generators might have more issues on those platforms.

  In particular, the code you get with the option "V8" enabled is compatible only with some versions of the V8-lib. Therefore, if SWIG is incompatible with your version of V8 or node-gyp (the node compile for C++), it generates many unsupported types and macros. On macOS, you can use the option "JSC" (Javascript Core), but (apart from the lack of portability) it cannot handle inner classes like optimize::handle, solver::cube_generator, etc.

• We can consider wrapping directly the header z3++.h with the V8 api. It's portable but hard to maintain. For every class and method, you have to write lines and lines of intricate code in order to convert the C++ types into Javascript types. As a partial solution, it could be helpful to use libraries as nan.h or napi.h, for example, by which you can write the bindings from scratch in a less verbose way.

The best solution I have found so far is emscripten, a very powerful and flexible compiler. It's easy to install and pretty straightforward to use for everyone who's familiar with gcc/clang options. I'm going to use it to generate javascript bindings (in order to wrap them into Typescript interfaces), but it can be used for generating wasm output files as well.

I'm going on with emscripten.

[NikolajBjorner]

I tried the quic_example.cpp (on Windows). It generates a WASM file so this route is JS bindings over WASM assemblies, which seems like the current way to go. The SWIG documentation probably predates the wider-spread use of WASM.
We use the python files under src/scripts to generate language specific bindings. This seems to be relevant for the macros that emscripten uses. the scripts are somewhat bulky, but not too many:
https://github.com/Z3Prover/z3/blob/master/scripts/mk_genfile_common.py
https://github.com/Z3Prover/z3/blob/master/scripts/update_api.py

[NikolajBjorner]

To set expectations, there is a comment in update_api.py

# TODO: rewrite this file without using global variables.
# This file is a big HACK.
# It started as small simple script.
# Now, it is too big, and is invoked from mk_make.py

Adding one more target would likely be possible, but benefit from some modularization.

[NikolajBjorner]

Note also that code like this

z3/scripts/update_api.py

Line 804 in d1fb831

def mk_js(js_output_dir):

is orphaned and I would delete it.

[NikolajBjorner]

Note also the activity around #5746. There are a couple of takeaways:
It shows a direct WASM integration with JS and it exposes an issue in WASM that is currently open.

[bakkot]

I've started working on TypeScript bindings here, built on top of wasm. It has auto-generated well-typed native bindings and the beginnings of a wrapper to provide a more user-friendly Python-style library.

The Python library is > 10k lines of code, so it'll be a long while before it reaches parity, but it's a start. @aestriplex (or anyone) if you want to collaborate, pull requests very welcome! This weekend I should have it to a state where there's CI and linting and so on.

It's pretty straightforward to port the Python bindings, there's just a lot to be done.

(The native bindings do technically work without a wrapper, but they're pretty hard to use - I'm not sure they're worth publishing on their own.)

@NikolajBjorner how do tests work? I'd like to port tests if there are existing ones - either tests of the underlying C bindings or (ideally) tests of the Python API.

[NikolajBjorner]

For python bindings we test the doc-strings and there are some samples that get tested in some versions of z3test runs.

You have of course the freedom to maintain auxiliary bindings outside of github.com/z3prover/z3, but a reasonable binding would have the benefit of being rolled into the master branch and tested with every build (using a github Action or alternatively or in addition the Azure pipeline scripts). So I am trying to encourage bindings that can be integrated and are easier to maintain.
I am aware of several other bindings, such as Haskell, Rust, Go, but have no way to follow them. They probably also bitrot relatively quickly and lack features.

[bakkot]

Yeah, once I get these to a state I'm happy with, including tests, I'll submit a PR.

Probably it'll happen in two parts: one PR which just exposes the raw C API with good TypeScript types, and then later another which exposes a more user-friendly wrapper like Python's (which will be incomplete when I PR it, but still useful).

I almost have the first part done, but there's a handful of cases I haven't handled yet (mostly to do with out parameters, which need to be wrapped even for the raw API because they require malloc).

[NikolajBjorner]

I encourage small incremental steps: Even the C API could be a basis. If the second step is abandoned, then the value of the first part does not get lost.

[aestriplex]

I'll start focusing on the Golang bindings then.
@bakkot I will be glad to help with the ts bindings if needed

[NikolajBjorner]

Above I was speculating about what it would take to change update_api.py and didn't find it too appealing to touch.

The script that auto-generates the js bindings https://github.com/bakkot/z3-js-bindings/blob/0fa155fb243015168e4750e25c6fe7713e919855/build/wrapper.ts
is totally independent of the python code in update_api.py.
I see this as a nice advantage: it cuts dependencies and does not suffer from the legacy hacks (that conflates several languages in one place).

[bakkot]

@NikolajBjorner OK, I have the raw TypeScript bindings in a state I'm happy with. I've updated the readme for the project. Specifically:

• Everything in the API (specifically these files) is supported (except Z3_get_lstring, because I wasn't sure how to interpret its return value - I don't know what the difference between Z3_string and Z3_char_ptr is meant to convey)
• There's a reasonable translation layer from C conventions to JS conventions
• The long-running APIs mentioned here are automatically shunted to a different thread and wrapped up in a JS Promise.
• I've ported a couple nontrivial examples and confirmed they work the same in JS as in C.

I'd like to contribute these to this repository. Some questions about that:

• Ideally the TS bindings would be built and be tested as part of CI. Should I just add a new Github Action which does the build "manually"? I'd prefer to avoid touching makefiles, if possible. The build is straightforward.
• What's the current process for releases? If you'd like I can include in my PR a Github Action which publishes on npm whenever you create a release on Github (that's what I do in my own projects, and it works well).
• Under what account would you like the package published? I see someone has the "z3" username, but they don't appear to be using it; I can ask npm if they'd release it to the control of this project, if you'd like; they are sometimes amenable to that.

[philzook58]

Very cool! You mention the SharedBufferArray problem in your readme that requires a coiworker workaround. It is my understanding the the single threaded Z3 build does not have this problem. The previous wasm CI action built the single threaded library although as you say seemed to require using the same compiler (or libc++?) to use it. I don't know if one can setup the npm build to work this way, but it may be desirable to have the option of a single threaded build for browser side and a multi threaded build for server side node.

[bakkot]

It is my understanding the the single threaded Z3 build does not have this problem.

Single threaded (meaning, "no threads") wasm builds of Z3 are entirely broken for anything nontrivial; see #5746, specifically #5746 (comment) and the following comment.

[NikolajBjorner]

A little background: Z3 must always be built using pthreads linking. This is to enable timeouts. Even the "single threaded" mode of building z3 requires pthreads, but it disables some locking around global data-structures. So the name of the build parameter SINGLE_THREADED is somewhat confusing because it still uses threads, just only in a single place. SINGLE_THREADED mode speeds up applications that don't use any of the multi-threaded features (except for timeouts).

[NikolajBjorner]

Very nice!

• Z3_string are 0 terminated strings.

• Z3_char_ptr is a pointer to characters. The character 0 has no specific meaning. The number of valid characters is supplied by an unsigned length.

• Should I just add a new Github Action

  • Yes, I think this is the more agile approach. Touching cmake and other is not as important if there is a self-contained build step. This would be second priority given that what matters is reproducibility (that others can build and that that the builds are continuous to avoid bit-rot).

• The current process for releases is to run an Azure Pipeline.

Azure Pipelines are a little different from GitHub Actions and when I started with Azure Pipelines the GitHub actions did not yet exist. For python (pypi) I have an account and set up secrets appropriately in the build pipeline to be able to upload. For nuget I have something similar, in principle, but it doesn't work so I just upload manually. It is better to have set up an account and keys. You can have your own account and keys and publish under your naming convention and I can replicate it for z3 (we would either need different names for the npm or transfer/share ownership). For the pypi z3-solver I was added as co-owner. Based on what I can see on https://www.npmjs.com/ and other online material on Github Actions and npm the setup looks similar. I created a "z3-solver" package and sent an invitation to your email address. If this works, then we are good.

So I suggest:

• Create a build GitHub Action builds and tests the npm and creates an artifact (locally as a zip).
• Create a release GitHub Action that build (tests) and uploads the to a relevant npm registry.

All these steps can be done in your own repository to start with so don't require round-tripping with the main branch during development.

I currently doubt that integrating the js as part of the main build as a flag makes sense: (1) The integration process for the wasm tools is still heavier than issuing an apt-get or similar. (2) he hosted images seem to have some but still limited support for empscripten (microsoft.net.sdk.emscripten on https://github.com/actions/virtual-environments/blob/main/images/win/Windows2022-Readme.md) and nothing for Ubuntu 20). (3) it seems like extra work and unknown who would need this.

There is going to be some value to having the GitHub actions ported to the Azure pipeline nightly and release scripts because the process for uploading artifacts to GitHub releases is streamlined. But this is much less useful than simply uploading to an npm registry from what I can tell.

[bakkot]

I created a "z3-solver" package and sent an invitation to your email address. If this works, then we are good.

I've joined. I'll get CI set up in my repo and then PR it when I've confirmed it's working as expected.

But, question:

You created an organization, not a package - one organization can have multiple packages. When a package is part of an organization, the format for the name is @org-name/package-name. So if you want to publish it under the organization, we'd still need to pick a package name. Maybe wasm? So it would be available as @z3-solver/wasm.

Alternatively I could publish under the global-scoped package name z3-solver, not as part of the organization, so it would be available as just z3-solver.

Either way I'd have to add your account to the package; organizations can't publish packages in their own right, only user accounts.

• Create a build GitHub Action builds and tests the npm and creates an artifact (locally as a zip).
• Create a release GitHub Action that build (tests) and uploads the to a relevant npm registry.

I can do this, but is there a reason to do it as a two-step process? The thing I usually do is to have the publish job also perform its own build; that allows you to avoid having to coordinate the artifacts between jobs. (Having artifacts on GitHub doesn't really do any good; npm is universally used among JS projects, so having the artifact be on npm is sufficient.)

I ask because the wasm build is ~30MB, and storing a fresh 30MB artifact on every commit will quickly use up a lot of space.

That is, I'm proposing:

• A build/test GitHub Action that runs on every commit, which discards the build after running rather than storing as an artifact
• A separate build/test/publish GitHub Action that runs manually (or is triggered automatically when you create a release on GitHub).

---

Also, the publish job will need to know the version to publish as. I can just read it out of the release.yml file, if that works for you?

---

Also also, the release job will need a token for your npm account to do the release to be stored on Github as a secret. It's straightforward, and I can walk you through it, I just want to confirm you're OK with that.

[NikolajBjorner]

Everything you suggest is very good.
I am unfamiliar with organization/package distinctions so made a mistake. Publishing just z3-solver and dropping the organization layer seems much better.
I also assumed the local artifact would be discarded after every new automatic build. This is already the case for other GitHub actions (or should be).

[bakkot]

Cool, I'll publish under z3-solver then.

I also assumed the local artifact would be discarded after every new automatic build. This is already the case for other GitHub actions (or should be).

I don't think they are discarded on every build? If I look at https://github.com/Z3Prover/z3/actions/workflows/wasm.yml, for example, I see lots of old artifacts. From the docs I guess it's 90 days by default.

Anyway, I'll just have the publish job also do the build; it's simpler that way.

[NikolajBjorner]

I see lots of old artifact

Seems so. This was not my initial understanding, but the artifacts seem to belong to the build not the action.

[aestriplex]

@NikolajBjorner I started the wrapping of the C++ library on my fork. I'm writing a "refactored" version of z3++.h in order to make it compatible with SWIG and Go. Right now, I'm focusing on:

• replacing operator overloads with "Java style" functions (i.e. X add(X other_number) in lieu of X operator+(const X & other_number)), since neither SWIG nor Go support operator overloading;
• replacing Z3 exceptions with Z3 error code, since Go doesn't support exceptions;
• taking out the inner classes (i.e. the iterator classes)

On my fork you can see the complete refactoring of the first three classes. Just as an example, replacing

operator Z3_context() const { return m_ctx; }

with

Z3_context get_Z3_context() const { return m_ctx; }

on line 130, required more than 500 substitutions throughout the code. So, it may take a while, but if we choose to not use the C library, it's the only way to make SWIG compile the code.

[NikolajBjorner]

Have you considered other approaches than SWIG?

I start getting the understanding from your note and other information I can find online
that SWIG isn't ideal and would introduce its own liability.

The bindings in https://github.com/mitchellh/go-z3 directly invoke the C API. They are hand-written and contain a lot of repetitious patterns (there are lots of functions for building expressions and they all have the same format taking a context and arguments and returning an expression.
It uses the "defer" construct just after resources (except expressions) are created to control GC.
With those options go programming experience may end up being low level requiring clients to remember to call "defer" while the C++ class-based discipline binds the resource lifetime to the object and it works nicely with lexical scope for stack allocated classes.
I can't tell what the right option for would be go as I have no experience using go and don't know the Intrinsics. It says somewhere that it was designed to not repeat what was seen as issues with C++ and the style I see in the go bindings departs from OO features (use structs and functions over structs).
If the gc allows callbacks it can be leveraged for resource collection, though it has a big gotcha that, in the GCs I know of, the resource utilization of a native object has to be declared to the GC so it knows how to prioritize efficient collections.
Reference counting is so basic that there must be some best practices for integrating reference counted objects with FFI for reasonable languages.

Maybe the consequential approach is a mixture of scripts that auto-generate most of the API for regular patterns and hand code for the C API for the remaining. This is the pattern we took elsewhere and most recently the TS/JS bindings by Kevin.
The Julia bindings use a Python/Boost inspired approach which is eminently convenient. This appears not available elsewhere.

Note that for expressions, Z3 has two modes.

• expressions are reference counted
• expressions life-time is bound to the context.
  The second mode frees the client from managing reference counts, but of course only allows a bounded set of expressions per context. It allows to serve entry-level use cases.

[aestriplex]

Hi @NikolajBjorner,
I'm sorry if the go bindings aren't available yet, but I've been very busy with my daytime work during the last month. Anyway, I am finishing a script that generates the go interfaces, and I'm waiting for go 1.18 to be released (it should be released this February, according to the official website). They say "Go 1.18 includes an implementation of generic features", which can be very useful for us.