Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WebAssembly Backend #142

Closed
wants to merge 81 commits into from
Closed

WebAssembly Backend #142

wants to merge 81 commits into from

Conversation

jeromesimeon
Copy link
Member

@jeromesimeon jeromesimeon commented Aug 13, 2020

WASM backend

  • Compiles with Coq 8.11 / 8.12
  • Switches to separate extraction
  • WASM PoC, but functional
  • Need to better integrate testing / runtime
  • Left as draft PR for now

@jeromesimeon jeromesimeon requested a review from pkel August 13, 2020 16:02
@jeromesimeon jeromesimeon changed the title Wasm Backend WebAssembly Backend Aug 13, 2020
jeromesimeon and others added 28 commits August 13, 2020 15:00
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.
pkel and others added 24 commits August 14, 2020 17:33
- 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: Jerome Simeon <[email protected]>
- derive the expected output from Imp eval.
- avoid bash for loop for iteration
- 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.
@jeromesimeon
Copy link
Member Author

Replaced by #147

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants