Webassembly backend #153

Signed-off-by: Jerome Simeon <[email protected]>

Signed-off-by: Patrik Keller <[email protected]>

I'm struggling with RuntimeOpRecDot. make -C tests wasm I need debugger access to the generated wasm and provided ejson argument.

This PoC demonstrates how Assemblyscript could be used to implement a runtime for imp_ejson. The next step on this road would be to implement a pair functions that read/write JS Ejson from/to Assemblyscript's managed memory.

This commit adds a pair of functions that read/write JS Ejson from/to Assemblyscript's managed memory. Executing a imp function compiled to wasm is now easy. Next steps: - Test the set op implemented operators. - Hook the new runtime into the compiler pipeline.

The runtime allows to run qcert queries compiled to wasm modules in chrome. DevTools enable stepwise debugging. This predates the recent effort to implement the IMP operators in Assemblyscript.

This commit removes the Imp(Wasm) runtime operators that have been implemented before. Instead we call imported functions. These functions are defined in an Assemblyscript module. As a side effect, we lost support for constants and EjsonRuntimeOperator(s). Next steps: - Unit test the set op implemented operators. - Provide engine that links the compiled module with the runtime. - Compile constants - Support EjsonRuntimeOperator(s).

This commit add a PoC engine that executes a compiled to wasm qcert query on NodeJS. It dynamically links the IMP runtime that we implement in AssemblyScript and compile to a separate wasm module.

We can compile the following OQL queries: 3.14 not (true or false) 3.14 <. 4.5 pi pi <. e greet And execute them on input: { "pi" : 3.14, "e" : 2.72, "greet" : "Hello World!" }

Before, each use of an IMP constant lead to a fresh allocation in the AssemblyScript runtime. Additionally, strings were entirely encoded in the AST (as function that allocate and inititalize the corresponding string in the runtime). Now, constants are serialized into the linear memory of the compiled module. On first use, a corresponding value is allocated in the memory of the AssemblyScript runtime. Repeated use of a constant uses the same value on the runtime side.

We now use the AssemblyScript runtime. The old runtime is not needed anymore.

- Make explicit, that be transfer bytes of an UTF8 string. - Allocate a single, correctly sized buffer on the runtime side.

Avoids headache on Javascript/Wasm interface.

Signed-off-by: Jerome Simeon <[email protected]>

Runtime operators added with this commit: - runtimeArray - runtimeArrayLength - runtimeFloatOfNat

Signed-off-by: Jerome Simeon <[email protected]>

Before, we encoded constants into the linear memory of the compiled module using an ad hoc binary encoding. Now, we reuse the binary EJson encoding introduced with the last few commits.

Before, the new Wasm backend was intertwined with the extracted QCert code. The backend could not be be used with Imp definitions extracted in other projects. Now, we define which type definitions we need from the extraction in `wasm_intf.ml`. We abstract from the exact implementation using a functor (see `wasm_backend.ml`). Instantiation of the functor for local use happens in `wasm_ast.ml`. This way we stay compatible with the previous version without touching the Coq project itself.

This commit adds support for branded values. Both the Q*cert internal Wasm eval (spec interpreter) and the PoC NodeJS engine can run wasm modules with branded values. The commit also removes EjLeft/EjRight from the Assemblyscript runtime.

Signed-off-by: Jerome Simeon <[email protected]>

- fixes incompatibility with node ("invalid block type error" when loading compiled wasm module) - removes dependencies to wat2wasm/wasm2wat

Before, if-then-else became if-then-then Signed-off-by: Patrik Keller <[email protected]>

Q*cert's `EJsonRuntimeCompare a b` returns sign(b - a). Before this fix the Wasm implementation of this operator returned sign(a - b). Signed-off-by: Patrik Keller <[email protected]>

Signed-off-by: Jerome Simeon <[email protected]>

Signed-off-by: Patrik Keller <[email protected]>

Signed-off-by: Jerome Simeon <[email protected]>

- derive the expected output from Imp eval. - avoid bash for loop for iteration

Signed-off-by: Jerome Simeon <[email protected]>

- add a small binary (tools/binary_to_string.(ml|exe) that escapes a binary string to a valid OCaml string using hex codes. - add a dune rule that reads binary runtime.wasm into a generated ml file. - use the resulting OCaml value in for the wasm spec eval.

Signed-off-by: Jerome Simeon <[email protected]>

… array Signed-off-by: Jerome Simeon <[email protected]>

Signed-off-by: Jerome Simeon <[email protected]>

I change the implementation of runtimeArrayAccess such that it throws an error in case of out of bounds instead of returning null. This behaviour seems to be assumed by the For -> ForRange rewrite.

We tracked a text representation before which resulted in polluted git logs. TODO: `dune build -w` is trapped in a loop after editing assembly/index.ts

Signed-off-by: Jerome Simeon <[email protected]>

npm install overrides the package-lock.json and uses newer versions. npm ci doesn't. https://stackoverflow.com/q/45022048

This is good news for #148. However, the opArrayPush clones the Array on each invocation.

Not implemented operators raise an error.

Runtime support might be missing.

Signed-off-by: Jerome Simeon <[email protected]>

…yAccess

Signed-off-by: Jerome Simeon <[email protected]>

…ringJoin) operators

Signed-off-by: Jerome Simeon <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Webassembly backend #153

Webassembly backend #153

Commits on Apr 28, 2022