Added thunk constructor
#569
Draft
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
`thunk` will be carried through rules unevaluated. Some `KItem` productions were changed to `Evaluation` to be compatible with the change.
ehildenb
reviewed
May 7, 2025
Comment on lines
591
to
594
|
|
||
| rule <k> thunk(#expect(_, _, _MSG)) => .K ... </k> | ||
|
|
||
| rule <k> thunk(#expect(_, _, MSG)) => AssertError(MSG) ... </k> |
There was a problem hiding this comment.
Add some documentation here, before this code-block, indicating why we add these rules. Specifically:
- if one of the more specific rules for
#expectfires, we know that we definitely don't have an assertion failure, or that we definitely do have an assertion failure. - Otherwise, the
thunkwrapper indicates that we don't know, and so instead we non-deterministically explore both branches. This will be sound for our proofs (we won't lose assertion failures, just may have too many).
ehildenb
reviewed
May 7, 2025
Comment on lines
328
to
329
| syntax TypedValue ::= thunk ( Evaluation ) | ||
| rule <k> EV:Evaluation => thunk(EV) ... </k> requires notBool isTypedValue(EV) [owise] |
There was a problem hiding this comment.
Add documentation before this codeblock explaining what the thunk is. Specifically:
- It captures any
Evaluationthat we can't make any further progress on, and turns it into aTypedValueso we can continue execution with it. - In particular, if we have pointer arithmetic with abstract pointers (not able to be resolved to ints/bytes directly), then it will
thunkthat up, and we can continue execution.
ehildenb
reviewed
May 7, 2025
Comment on lines
-883
to
-910
| Error cases for `castKindIntToInt` | ||
| * unknown target type (not in `types`) | ||
| * target type is not an `Int` type | ||
| * value is not a `Integer` | ||
|
|
||
| ```k | ||
| rule <k> #cast(_, castKindIntToInt, TY) => UnknownCastTarget(TY, TYPEMAP) ... </k> | ||
| <types> TYPEMAP </types> | ||
| requires notBool isTypeInfo(TYPEMAP[TY]) | ||
| [preserves-definedness] | ||
|
|
||
| rule <k> #cast(_, castKindIntToInt, TY) => UnexpectedCastTarget(castKindIntToInt, {TYPEMAP[TY]}:>TypeInfo) ... </k> | ||
| <types> TYPEMAP </types> | ||
| requires notBool (#isIntType({TYPEMAP[TY]}:>TypeInfo)) | ||
| [preserves-definedness] | ||
|
|
||
| rule <k> #cast(NONINT, castKindIntToInt, _TY) => UnexpectedCastArgument(NONINT, castKindIntToInt) ... </k> | ||
| [owise] | ||
| ``` | ||
|
|
||
| ### Other type casts | ||
|
|
||
| Other type casts are not implemented yet. | ||
|
|
||
| ```k | ||
| rule <k> #cast(_, CASTKIND, _TY) => CastNotimplemented(CASTKIND)... </k> | ||
| requires CASTKIND =/=K castKindIntToInt | ||
| [owise] |
There was a problem hiding this comment.
I suppose now we can get rid of all the Error constructors we had, like UnknownCastTarget and such. This is probably true that we can get rid of a lot of error constructors now.
ehildenb
reviewed
May 7, 2025
Comment on lines
-1128
to
-1135
| typedValue(Integer(_, WIDTH, SIGNEDNESS), TY, _), | ||
| typedValue(Integer(_, WIDTH, SIGNEDNESS), TY, _), | ||
| false) // unchecked | ||
| => Overflow_U_B | ||
| requires isArithmetic(BOP) | ||
| [priority(60)] | ||
|
|
||
| // These are additional high priority rules to detect/report divbyzero and div/rem overflow/underflow |
There was a problem hiding this comment.
Similarly we can get rid of Overflow_U_B and such now.
ehildenb
reviewed
May 9, 2025
|
|
||
| rule <k> #expect(typedValue(BoolVal(COND), _, _), EXPECTED, _MSG) => .K ... </k> | ||
| requires COND ==Bool EXPECTED | ||
|
|
||
| rule <k> #expect(typedValue(BoolVal(COND), _, _), EXPECTED, MSG) => AssertError(MSG) ... </k> | ||
| requires COND =/=Bool EXPECTED | ||
| ``` | ||
| If the specific assertion rules above for `#expect` are matched, then we definitely know that there is or is not an assertion failure (respective to the matched rule). However if a `thunk` wrapper exists around an `#expect` we want to non-deterministically explore both branches. This does not sacrifice unsoundness as we would not eliminate any assertion failures with `thunk`, but instead will create unnecessary ones in the cases the `thunk(#expect(...))` would evaluate to true. |
There was a problem hiding this comment.
I usually do 1 sentence per file line (so it's easy to remove sentences), or wrap at 120 characters. But this should be formatted a bit. It looks like in other places in the file, it's 1 sentence per line.
Other place where comment is added too.
I would also put one blank line before this (after the code block).
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.
Following the conversation where we decided that we would create a constructor to delay evaluation of currently impossible to implement features (e.g. when an address of a place is required) Everett and I have implemented the
thunk(Evaluation)constructor toTypedValue. We have athunkfirst approach, meaning that the errors are removed and left asthunks. This should stop us getting stuck and allow us to get very far in our executions with unevaluatedthunks that will illustrate features we implement.Things added:
TypedValue ::= thunk(Evalution)Things changed:
Evaluation ::= #castEvaluation ::= #computeEvaluation ::= #expectEvaluation ::= projectedUpdateRemoved rules resulting in: