Expose function evaluation to bindings #905
Merged
Conversation
This file contains 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
This was referenced Nov 27, 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.
Baltoli
force-pushed
the
evaluate-2
branch
2 times, most recently
from
44a533f
to
54b1534
Compare
rv-jenkins
pushed a commit
that referenced
this pull request
Dec 5, 2023
~~Blocked on #907 This 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. --------- Co-authored-by: Tamás Tóth <[email protected]>
Baltoli
requested review from
dwightguth,
Robertorosmaninho,
theo25,
tothtamas28 and
gtrepta
tothtamas28
reviewed
Dec 7, 2023
Robertorosmaninho
approved these changes
Dec 13, 2023
tothtamas28
reviewed
Dec 15, 2023
There was a problem hiding this comment.
Python API looks good.
Tests in pyk: runtimeverification/pyk#784
tothtamas28
reviewed
Dec 15, 2023
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.
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:
rawTerm{}wrapper.