Further typechecker and interpreter cleanup #2165
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
Make it clearer what you might need to fix in your code. (Mostly, typos in type names.) Also note that we haven't found any way to do anything overtly unsound with the incorrect behavior, only trigger panics.
…binds.
This corrects certain weirdnesses that were probably intended as
ease-of-use affordances for the repl but also affect scripts. In
particular:
- monadic actions need to be in TopLevel (or in ProofScript for
the ProofScript repl);
- monadic actions that are polymorphic in their monad are run
in TopLevel or ProofScript instead of being gratuitiously
rejected;
- the interpreter no longer wraps pieces of the bind in a
Decl for typechecking, which is the first step on cleaning
up the interpreter's typechecking notions (#2158).
The downside is that you can no longer directly eval non-monadic
expressions in the repl without prefixing them with "return". This is
not terrible, but we should at least consider adding repl-specific
affordances to allow that again once the code is in shape to be able
to do it reasonably.
Another oddity is that previously if you eval'd a monadic action that
was in some other monad (e.g. LLVMSetup) at the syntactic top level it
would, instead of giving a type error, just not evaluate it and then
print "<monadic>" as the result. If for some reason you really want
to do this you can also get the old behavior by prefixing the lot with
"return".
Note that all this applied to the _syntactic_ top level, and not binds
within do-blocks, whether or not they were within functions, and
regardless of whether they were in the TopLevel monad.
Include some tests and a CHANGES entry. Closes #2162.
sauclovian-g
added
type: bug
In particular the interpreter used to allow "x <- e;" for a pure term e as long as it was at the syntactic top level; this should have been "let x = e;" and now it will be rejected. The failures so far (except for one) have been linked to three specific saw-script builtins: unfold_term, parse_core_mod, and mir_find_adt. I've checked all uses I can find of these. There might be more cases lurking though. Also update the CHANGES entry to specifically mention this behavior, since it's quite conceivable that downstream users will have their own instances of this problem.
…mples. Properly part of the previous commit.
Pass in the position from the original StmtBind instead of tossing it out and then using PosRepl instead.
There is no reason any more (if there ever was) to yoink the type out of the pattern and graft a copy onto the expression as an explicit type annotation. Commit this separately just in case there's something subtle happening and we end up wanting to be able to bisect to it later.
Move it all to a single subsection of processStmtBind. Also, don't print the types of functions when we weren't asked to print.
There's no point finding a position to cons up an LName if the position is then going to just be discarded.
Now it's in interpretStmt and that's the first step to having only one typechecker call in interpretStmt. Which is in turn the first step on typechecking _before_ we start interpreting.
…oup. This should have no effect, but commit it separately anyway in case we ever need to bisect it. This makes the checkDeclGroup entry point to the typechecker no longer used, so remove it.
The position we've been passing to checkStmt is now always just the position _of_ the statement. The typechecker can get this on its own. Leave a note for later that this is not really the right position to use for the purposes the typechecker uses this position for (the monad context the statement appears in) and that should be sorted out better. But it's probably not worth trying to do so until the interfacing to the typechecker is rationalized.
|
For the record, I decided to go ahead and push the further cleanup I'd been doing while deciding what to do about the failure in s2n. The changes coming (to make the new failures warnings for the time being) really want to sit on top of that cleanup: currently the typechecker cannot produce warnings and making it able to do so affects the interpreter -> typechecker interface, which is now a lot less fraught. |
Statements of the forms x <- e; x <- s; s; where e is a non-monadic term and s is a monadic term in the wrong monad are now accepted with a warning instead of causing a fatal type error. Note that statements of the form e; which also used to be accepted will now fail. The chance of this appearing in the wild is low. While I've fixed all the fallout in the saw tree, the amount (and nature) suggests that downstream users will also have cases to fix and we should allow time for this before making it a hard fail. Add tests for all these forms.
1. Don't allow the wrong monad in a bind whose pattern is a tuple pattern. The old saw produces a type error for that so we don't have to allow it now. 2. For binds in the wrong monad, unify the pattern type with the full wrong monadic type of the expression, not just the associated value type. This assigns the variables in the pattern types in the wrong monad, which matches both the historical behavior and also what happens inside the interpreter during execution. It also turns out that binds in the wrong monad with an explicit type signature expecting the bind to work didn't typecheck in the old saw. So we don't need to make that work as part of the workarounds either. Add three more test cases...
RyanGlScott
reviewed
Jan 6, 2025
|
The failures seem to be another manifestation of #2166 or something like it, not anything I did. FWIW |
|
I've reached out internally about the Galois website URL (https://saw.galois.com/builds/nightly/saw_unbounded-0.8.0.99-2021-09-09-Linux-x86_64.tar.gz) that is failing to resolve. |
It now says "This creates the action but does not execute it", which is both more accurate and avoids a confusing unintended alternate reading of the original text.
RyanGlScott
approved these changes
Jan 13, 2025
CHANGES.md
Outdated
Comment on lines
14
to
47
| * Unexpected special-case type behavior of monad binds in the | ||
| syntactic top level has been removed. | ||
| (This was _not_ specifically associated with the TopLevel monad, so | ||
| top-level binds and binds in functions in TopLevel, or in nested | ||
| do-blocks, would behave differently.) | ||
| See issue #2162. | ||
|
|
||
| There are three primary visible consequences. | ||
| The first is that the REPL no longer accepts | ||
| non-monadic expressions. | ||
| These can still be evaluated and printed; just prefix them with | ||
| ```return```. | ||
| (Affordances specifically for the REPL so this is not required there | ||
| may be restored in the future.) | ||
|
|
||
| The second is that statements of the form ```x <- e;``` where ```e``` | ||
| is a pure (non-monadic) term used to be (improperly) accepted at the | ||
| top level of scripts. | ||
| These statements now generate a warning. | ||
| This will become an error in a future release and such statements | ||
| should be rewritten as ```let x = e;```. | ||
| For example, ```t <- unfold_term ["reverse"] {{ reverse 0b01 }};``` | ||
| should be changed to ```let t = unfold_term ["reverse"] {{ reverse 0b01 }};```. | ||
|
|
||
| The third is that statements of the form ```x <- s;``` or just ```s;``` | ||
| where ```s``` is a term in the _wrong_ monad also used to be | ||
| improperly accepted at the top level of scripts. | ||
| These statements silently did nothing. | ||
| They will now generate a warning. | ||
| This will become an error in a future release. | ||
| Such statements should be removed or rewritten. | ||
| For example, it used to be possible to write ```llvm_assert {{ False }};``` | ||
| at the top level (outside any specification) and it would be ignored. | ||
| ```llvm_assert``` is only meaningful within an LLVM specification. |
There was a problem hiding this comment.
Would you be willing to indent each line here (that doesn't begin with a * ) by two spaces? That is:
* Unexpected special-case type behavior of monad binds in the
syntactic top level has been removed.
(This was _not_ specifically associated with the TopLevel monad, so
top-level binds and binds in functions in TopLevel, or in nested
do-blocks, would behave differently.)
See issue #2162.
There are three primary visible consequences.
Otherwise, GitHub-Flavored Markdown will render it strangely (click "View file" in the PR to see what I mean).
There was a problem hiding this comment.
I didn't realize you could check it that way... was basically hoping it would come out ok (the success rate for which is not high)
Will fix.
CHANGES.md
Outdated
Comment on lines
49
to
60
| * A number of SAWScript type checking problems have been fixed, | ||
| including issue #2077. | ||
| Some of these problems were partially mutually compensating; for | ||
| example, in some cases nonexistent typedefs had been mishandled in | ||
| ways that made them mostly work. | ||
| Some previously accepted scripts and specs may be rejected and need | ||
| (generally minor) adjustment. | ||
| Prior to these changes the typechecker allowed unbound type variables | ||
| in a number of places (such as on the right-hand side of typedefs, and | ||
| in function signatures), so for example type names contaning typos | ||
| would not necessarily have been caught and will now fail. | ||
| ```typedef t = nonexistent``` was previously accepted and now is not. | ||
| These problems could trigger panics, but there does not appear to have | ||
| been any way to produce unsoundness in the sense of false | ||
| verifications. |
There was a problem hiding this comment.
A similar comment about indentation here.
Whitespace only.
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.
No description provided.