@@ -117,51 +117,57 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
117117 override string toString ( ) { result = "boolean(" + value + ")" }
118118}
119119
120- /** Holds if `pat` is guaranteed to match at the point in the AST where it occurs. */
121- pragma [ nomagic]
122- private predicate isExhaustiveMatch ( Pat pat ) {
123- (
124- pat instanceof WildcardPat
125- or
126- pat = any ( IdentPat ip | not ip .hasPat ( ) and ip = any ( Variable v ) .getPat ( ) )
127- or
128- pat instanceof RestPat
129- or
130- // `let` statements without an `else` branch must be exhaustive
131- pat = any ( LetStmt let | not let .hasLetElse ( ) ) .getPat ( )
132- or
133- // `match` expressions must be exhaustive, so last arm cannot fail
134- pat = any ( MatchExpr me ) .getLastArm ( ) .getPat ( )
135- or
136- // macro invocations are exhaustive if their expansion is
137- pat = any ( MacroPat mp | isExhaustiveMatch ( mp .getMacroCall ( ) .getExpanded ( ) ) )
138- or
139- // parameter patterns must be exhaustive
140- pat = any ( Param p ) .getPat ( )
141- ) and
142- not pat = any ( ForExpr for ) .getPat ( ) // workaround until `for` loops are desugared
120+ /**
121+ * Holds if `pat` can not _itself_ be the cause of a pattern match failure. This
122+ * does not mean that `pat` is irrefutable, as its children might be the cause
123+ * of a failure.
124+ */
125+ private predicate cannotCauseMatchFailure ( Pat pat ) {
126+ pat instanceof RangePat or
127+ // Identifier patterns that are in fact path patterns can cause failures. For
128+ // instance `None`. Only if an `@ ...` part is present can we be sure that
129+ // it's an actual identifier pattern.
130+ pat = any ( IdentPat p | p .hasPat ( ) ) or
131+ pat instanceof WildcardPat or
132+ pat instanceof RestPat or
133+ pat instanceof RefPat or
134+ pat instanceof TuplePat or
135+ pat instanceof MacroPat
136+ }
137+
138+ /**
139+ * Holds if `pat` is guaranteed to match at the point in the AST where it occurs
140+ * due to Rust's exhaustiveness checks.
141+ */
142+ private predicate guaranteedMatchPosition ( Pat pat ) {
143+ // `let` statements without an `else` branch must match
144+ pat = any ( LetStmt let | not let .hasLetElse ( ) ) .getPat ( )
143145 or
144- exists ( Pat parent | isExhaustiveMatch ( parent ) |
145- pat = parent .( BoxPat ) .getPat ( )
146- or
147- pat = parent .( IdentPat ) .getPat ( )
148- or
149- pat = parent .( MacroPat ) .getMacroCall ( ) .getExpanded ( )
150- or
151- pat = parent .( ParenPat ) .getPat ( )
152- or
153- pat = parent .( RecordPat ) .getRecordPatFieldList ( ) .getField ( _) .getPat ( )
154- or
155- pat = parent .( RefPat ) .getPat ( )
156- or
157- pat = parent .( TuplePat ) .getAField ( )
146+ // `match` expressions must be exhaustive, so last arm must match
147+ pat = any ( MatchExpr me ) .getLastArm ( ) .getPat ( )
148+ or
149+ // parameter patterns must match
150+ pat = any ( Param p ) .getPat ( )
151+ or
152+ exists ( Pat parent | guaranteedMatchPosition ( parent ) |
153+ // propagate to all children except for or patterns
154+ parent = pat .getParentPat ( ) and not parent instanceof OrPat
158155 or
159- pat = parent .( TupleStructPat ) .getAField ( )
156+ // for or patterns only the last child inherits the property
157+ parent .( OrPat ) .getLastPat ( ) = pat
160158 or
161- pat = parent .( OrPat ) .getLastPat ( )
159+ // for macro patterns we propagate to the expanded pattern
160+ parent .( MacroPat ) .getMacroCall ( ) .getExpanded ( ) = pat
162161 )
163162}
164163
164+ private predicate guaranteedMatch ( Pat pat ) {
165+ ( cannotCauseMatchFailure ( pat ) or guaranteedMatchPosition ( pat ) ) and
166+ // In `for` loops we use a no-match edge from the pattern to terminate the
167+ // loop, hence we special case and always allow the no-match edge.
168+ not pat = any ( ForExpr for ) .getPat ( )
169+ }
170+
165171/**
166172 * A completion that represents the result of a pattern match.
167173 */
@@ -170,7 +176,7 @@ class MatchCompletion extends TMatchCompletion, ConditionalCompletion {
170176
171177 override predicate isValidForSpecific ( AstNode e ) {
172178 e instanceof Pat and
173- if isExhaustiveMatch ( e ) then value = true else any ( )
179+ if guaranteedMatch ( e ) then value = true else any ( )
174180 or
175181 e instanceof TryExpr and value = true
176182 }
0 commit comments