Use inf-llc for codegen
#44
Conversation
There was a problem hiding this comment.
Pull request overview
This PR migrates the WASM code generation from a hand-written encoder-based approach to using LLVM IR and the inf-llc compiler toolchain. The change introduces LLVM-based compilation with custom intrinsics for non-deterministic operations (forall, exists, assume, unique) and Uzumaki expressions.
Key changes:
- Replaced direct WASM encoding with LLVM IR generation using inkwell
- Added build script to copy platform-specific
inf-llcbinaries - Introduced new test files for const and nondet features with execution validation
Reviewed changes
Copilot reviewed 12 out of 17 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| core/wasm-codegen/src/module.rs | Removed entire hand-written WASM encoder implementation |
| core/wasm-codegen/src/lib.rs | Replaced encoder with LLVM-based compiler workflow |
| core/wasm-codegen/src/compiler.rs | New LLVM IR compiler with intrinsics support |
| core/wasm-codegen/src/utils.rs | Added utilities for invoking inf-llc and wasm-ld |
| core/wasm-codegen/Cargo.toml | Replaced wasm-encoder with inkwell and build dependencies |
| core/wasm-codegen/build.rs | Added build script to copy inf-llc binary to target directory |
| core/ast/src/nodes_impl.rs | Added is_non_det and is_void helper methods |
| core/ast/src/builder.rs | Initialize type_info for SimpleType nodes |
| tests/src/codegen/wasm/base.rs | Added new test cases including execution validation |
| tests/Cargo.toml | Added inf-wasmparser and wasmtime dependencies |
| tests/test_data/codegen/wasm/base/const.inf | New test file for const definitions |
| tests/test_data/codegen/wasm/base/nondet.inf | New test file for non-deterministic operations |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> Signed-off-by: Georgii Plotnikov <accembler@gmail.com>
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 13 out of 19 changed files in this pull request and generated 3 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| //TODO: don't forget to remove | ||
| #![allow(dead_code)] |
There was a problem hiding this comment.
The #![allow(dead_code)] lint suppression with the TODO comment suggests this is temporary. Since this is production code being merged, either remove unused code or document why it needs to remain with the dead_code attribute. Temporary lint suppressions can hide real issues and make the codebase harder to maintain.
| //TODO: don't forget to remove | |
| #![allow(dead_code)] |
| }, | ||
| Statement::Expression(expression) => { | ||
| let expr = self.lower_expression(&expression); | ||
| //FIXME: revisit this logic #45 |
There was a problem hiding this comment.
The FIXME comment references issue #45 but doesn't explain what needs to be revisited about this logic. Consider adding a brief description of the problem or expected behavior to make the maintenance need clearer for future developers.
| //FIXME: revisit this logic #45 | |
| //FIXME: revisit this logic (#45): It is unclear if storing the result of the last expression in a non-deterministic, void block is necessary or correct. |
| } | ||
|
|
||
| pub fn infer_expression_types(&self) { | ||
| //FIXME: very hacky way to infer Uzumaki expression types in return statements |
There was a problem hiding this comment.
This comment acknowledges the implementation is hacky. Since type inference is a critical part of the compiler, consider filing an issue to refactor this properly or documenting what a proper solution would look like.
Instead of using hand-written codegen, this PR uses
inf-llc