Add raw term production #3829
Closed
Add raw term production #3829
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
dwightguth
reviewed
Nov 27, 2023
runtimeverification/llvm-backend#904 is the surrounding context; this isn't quite ready for a review yet. Open to suggestions for alternative implementations! |
|
Closing after discussing with @dwightguth; a better solution is to have the backend insert a symbol automatically as a preprocessing step. |
rv-jenkins
pushed a commit
to runtimeverification/llvm-backend
that referenced
this pull request
Nov 28, 2023
This is an alternative formulation to runtimeverification/k#3829; that PR contains the original context for why this change is necessary. Rather than adding a regular symbol to the K standard library source and using a check in the frontend to ensure that user code doesn't mention it, we directly emit a symbol into each definition with a name that the frontend cannot reference. We also bump the version number for the proof hint format so that this non-standard symbol must be explicitly accepted by the Python client code.
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.
The LLVM backend code that emits binary KORE terms into a proof trace wraps terms that are not represented as symbols at runtime in an injection into
KItemto allow them to be serialized using the code-generated recursion scheme used elsewhere in the backend.However, doing so is not sound (see runtimeverification/llvm-backend#904 for the full context). The additional injection changes the semantics of the serialized terms, and it is ambiguous whether client parser code should strip the injection from terms it reads from the trace.
The solution to this problem that I propose in this PR is to add a symbol to the K standard library whose only purpose is to signal "the term under this symbol is an injection into
KItemthat should be stripped when parsing a trace"; I have also implemented a small check that verifies user code does not attempt to write rules using this symbol.Subsequent follow-up changes will be required to fully implement this solution:
#rawTerminstead of injections, along with a version bump for the format.There may be a better way to implement something equivalent to these changes; I'm open to suggestions!