Add support for rawTerm to Python bindings
#908
Merged
Conversation
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
Baltoli
force-pushed
the
bind-raw-term-strip
branch
from
05c9709 to
23e9e5e
Compare
tothtamas28
reviewed
Nov 30, 2023
Co-authored-by: Tamás Tóth <[email protected]>
tothtamas28
reviewed
Nov 30, 2023
tothtamas28
reviewed
Nov 30, 2023
There was a problem hiding this comment.
Python part looks good.
Test in pyk: runtimeverification/pyk#748
This was referenced Dec 1, 2023
rv-jenkins
pushed a commit
that referenced
this pull request
Dec 1, 2023
Part of: #905 In #905, we are implementing a Python binding for the backend's function evaluator: given a function label and list of argument `Pattern`s, construct runtime terms for the arguments, evaluate the function with the given label, and return the result as an AST pattern. To safely reify the runtime term produced by the function call to an AST pattern, we need to know its sort (so that the machinery in #907, #908 can be used correctly). In some places in the bindings, we have to require that callers provide a sort when reifying terms back to patterns. However, when calling a function, the label of the function determines precisely the correct sort to use. This PR emits a new table of global data into compiled interpreters that maps tags to declared return sorts, along with a function that abstracts away indexing into this table. This change is similar to (but simpler than) an existing table of _argument sorts_ for each symbol that we already emit. Testing is handled by binding the new function to Python.
Robertorosmaninho
approved these changes
Dec 5, 2023
rv-jenkins
pushed a commit
to runtimeverification/pyk
that referenced
this pull request
Dec 6, 2023
~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
rv-jenkins
pushed a commit
that referenced
this pull request
Dec 18, 2023
This PR adds a new feature to the backend's binding API that allows for function symbols to be evaluated on a set of AST pattern arguments, with the result returned as a pattern also. This is motivated by the proof generation project; the execution trace format generated by the backend to summarise a concrete execution can contain the labels and arguments for function call events, but not the functions' return values without breaking tail-call optimisation. Most of the prerequisite work for this PR was done in #908 and #911; the actual changes here are quite small: * Adds a sort-aware term-to-pattern reification method that uses the new `rawTerm{}` wrapper. * Marshals arguments and returns between pattern and term level in the core bindings API. * Adds a test case demonstrating a few simple cases for this feature; as ever the bulk of the testing ought to be performed in Pyk.
Baltoli
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 9, 2024
~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
Baltoli
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 9, 2024
…erification/pyk#748) ~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
Baltoli
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 9, 2024
…erification/pyk#748) ~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
Baltoli
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 10, 2024
…erification/pyk#748) ~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
Baltoli
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 10, 2024
…erification/pyk#748) ~Blocked on runtimeverification/llvm-backend#908 --------- Co-authored-by: devops <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Blocked on #907This PR follows up #907 by having the Python bindings strip patterns of the form
rawTerm{}(inj{...}(...)})when deserializing from binary KORE; this will allow Pyk and subsequently the proof checker's parser to soundly load function arguments from proof traces and pass them to the function evaluator in #905.