feat(kframework_ffi): Marshaller for moving rust kore types to the llvm-backend#10
Merged
Conversation
Change signatures to match what bindgen will produce
…ckend Assisted-by: Claude Code
BUG: The fuzzer has a memory leak now
Assisted-by: Claude Code
Assisted-by: Claude Code
paramaters/return values. Remove unsafe blocks and rely on the safe datatypes. Assisted-by: Claude Code
tothtamas28
approved these changes
May 4, 2026
This was referenced May 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR extends the
kframework_fficrate to offer aMarshallerutility that allows converting the rust library's kore representation to the llvm-backend's kore AST.Changes/Additions
kframework_ffi::kllvm::{Sort, Symbol}, which hold pointers to the llvm-backend's respective representations.Symbolconsists of a symbol name and sort arguments for creating production termskframework_ffi::kllvm::{Marshaller, MarshalError, VarHandler}(See section below)examples/fuzzerto use the Marshallercargo clippyformatting changesMarshaller
VarHandlertraitThe
VarHandlercan be implemented by the user to provide the marshaller with a way to substitute any variables it encounters in the kore term during its marshalling.MarshalErrorAn enum of errors that can happen during marshalling
Unsupported: A kore tree node that the llvm-backend's execution engine doesn't support was encountered (ie. anAxiom, or anExists)UnknownVar: A variable that the marshaller wasn't able to substitute with a term, either because it doesn't have aVarHandleror because the one it has doesn't handle it.Cstring: There was an error when creating a C-string from a rust String. The constructors for the rust types should normally protect against this.MarshallerThe marshaller can be constructed with an optional
VarHandler. You can then callmarshalwith akore::Patternto get akllvm::Pattern.It has a
set_handlermethod to change out the variable handler to make repeated calls with different variable substitutions on the term.It will cache any variable-free subtrees in the term to speed up repeated calls with different handlers. See the doc-strings for more details.