-
Notifications
You must be signed in to change notification settings - Fork 30
Fix unsound Ok() switch guard by demoting all-residual conditional discriminants #271
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -229,3 +229,99 @@ struct ConditionalOnFlag: | |
| 0 [+1] Flag enabled | ||
| if enabled: | ||
| 1 [+1] UInt value | ||
|
|
||
|
|
||
| struct ResidualConditionalDiscriminant: | ||
| # `tag` is itself conditional, and is the switch discriminant for `a`/`b` | ||
| # (it is the first conjunct of their existence conditions). Every arm | ||
| # carries a residual (`outer == 1`), so when `outer != 1` the message is | ||
| # valid even though `tag` is absent -- and on a buffer too short to hold | ||
| # `tag`, reading the discriminant is Unknown. The optimized Ok() must not | ||
|
AaronWebster marked this conversation as resolved.
Outdated
|
||
| # reject such a message. | ||
| 0 [+1] UInt outer | ||
| if outer == 1: | ||
| 1 [+1] UInt tag | ||
|
|
||
| if tag == 0 && outer == 1: | ||
| 2 [+1] UInt a | ||
|
|
||
| if tag == 1 && outer == 1: | ||
| 2 [+1] UInt b | ||
|
|
||
|
|
||
| struct BareConditionalDiscriminant: | ||
| # Like above, but `a`/`b` reference the conditional discriminant `tag` | ||
|
AaronWebster marked this conversation as resolved.
Outdated
|
||
| # without re-guarding `outer == 1`, so the switch arms are bare. Here the | ||
| # discriminant Known() guard is sound: an Unknown `tag` leaves has_a()/ | ||
| # has_b() Unknown, so Ok() correctly reports the message as invalid. | ||
| 0 [+1] UInt outer | ||
| if outer == 1: | ||
| 1 [+1] UInt tag | ||
|
|
||
| if tag == 0: | ||
| 2 [+1] UInt a | ||
|
|
||
| if tag == 1: | ||
| 2 [+1] UInt b | ||
|
|
||
|
|
||
| struct DominatedBareDiscriminant: | ||
| # Bare arms on a conditional discriminant, plus an always-present `tail` | ||
| # field that dominates the structure size. When `outer != 1`, `tag` is | ||
| # absent and has_a()/has_b() are Unknown, but `tail` keeps the size Known so | ||
| # IsComplete() is true. Ok() must still be false: a/b's existence is | ||
| # indeterminate, and the discriminant Known() guard -- not IsComplete() -- | ||
| # is what enforces that. (A `if (has_tag().ValueOrDefault())` wrapper would | ||
| # wrongly accept this message.) | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This last phrase is unclear Does that reflect the state before this PR or after? Is that intended behaviour? Some of the explanations in the comments for these tests might be helpful in the language docs (either as clarifications or examples). |
||
| 0 [+1] UInt outer | ||
| if outer == 1: | ||
| 1 [+1] UInt tag | ||
|
|
||
| if tag == 0: | ||
| 2 [+1] UInt a | ||
|
|
||
| if tag == 1: | ||
| 2 [+1] UInt b | ||
|
|
||
| 3 [+1] UInt tail | ||
|
|
||
|
|
||
| struct DisjunctionConditionalDiscriminant: | ||
| # Disjunction arms (`tag == 0 || tag == 1`) on a conditional discriminant, | ||
| # each carrying a residual. Exercises the disjunction matcher and case-label | ||
| # coalescing together with the residual-only guarded switch. | ||
| 0 [+1] UInt outer | ||
| if outer == 1: | ||
| 1 [+1] UInt tag | ||
|
|
||
| if (tag == 0 || tag == 1) && outer == 1: | ||
| 2 [+1] UInt a | ||
|
|
||
| if (tag == 2 || tag == 3) && outer == 1: | ||
| 2 [+1] UInt b | ||
|
|
||
|
|
||
| struct SingleEntryConditionalDiscriminant: | ||
| # A single residual arm on a conditional discriminant. The switch group has | ||
|
AaronWebster marked this conversation as resolved.
Outdated
|
||
| # one entry, so it is demoted to a has_X() check instead of a switch; no | ||
| # discriminant guard is emitted, so the bug cannot arise here. | ||
| 0 [+1] UInt outer | ||
| if outer == 1: | ||
| 1 [+1] UInt tag | ||
|
|
||
| if tag == 0 && outer == 1: | ||
| 2 [+1] UInt a | ||
|
|
||
|
|
||
| struct EnumConditionalDiscriminant: | ||
| # Conditional discriminant of enum type, with residual arms. Exercises the | ||
| # enum-typed case labels in the guarded switch. | ||
| 0 [+1] OnOff outer | ||
| if outer == OnOff.ON: | ||
| 1 [+1] OnOff tag | ||
|
|
||
| if tag == OnOff.OFF && outer == OnOff.ON: | ||
| 2 [+1] UInt a | ||
|
|
||
| if tag == OnOff.ON && outer == OnOff.ON: | ||
| 2 [+1] UInt b | ||
Uh oh!
There was an error while loading. Please reload this page.