never executed always true always false
1
2 {-# LANGUAGE DeriveFunctor #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE GADTs #-}
5
6 -- | Coverage checking step of the
7 -- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
8 --
9 -- Coverage check guard trees (like @'PmMatch' 'Pre'@) to get a
10 -- 'CheckResult', containing
11 --
12 -- 1. The set of uncovered values, 'cr_uncov'
13 -- 2. And an annotated tree variant (like @'PmMatch' 'Post'@) that captures
14 -- redundancy and inaccessibility information as 'RedSets' annotations
15 --
16 -- Basically the UA function from Section 5.1, which is an optimised
17 -- interleaving of U and A from Section 3.2 (Figure 5).
18 -- The Normalised Refinement Types 'Nablas' are maintained in
19 -- "GHC.HsToCore.Pmc.Solver".
20 module GHC.HsToCore.Pmc.Check (
21 CheckAction(..),
22 checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
23 ) where
24
25 import GHC.Prelude
26
27 import GHC.Builtin.Names ( hasKey, considerAccessibleIdKey, trueDataConKey )
28 import GHC.HsToCore.Monad ( DsM )
29 import GHC.HsToCore.Pmc.Types
30 import GHC.HsToCore.Pmc.Utils
31 import GHC.HsToCore.Pmc.Solver
32 import GHC.Driver.Session
33 import GHC.Utils.Outputable
34 import GHC.Tc.Utils.TcType (evVarPred)
35 import GHC.Data.OrdList
36
37 import qualified Data.Semigroup as Semi
38 import Data.List.NonEmpty ( NonEmpty(..) )
39 import qualified Data.List.NonEmpty as NE
40 import Data.Coerce
41
42 -- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
43 newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
44 deriving Functor
45
46 -- | Composes 'CheckAction's top-to-bottom:
47 -- If a value falls through the resulting action, then it must fall through the
48 -- first action and then through the second action.
49 -- If a value matches the resulting action, then it either matches the
50 -- first action or matches the second action.
51 -- Basically the semantics of the LYG branching construct.
52 topToBottom :: (top -> bot -> ret)
53 -> CheckAction top
54 -> CheckAction bot
55 -> CheckAction ret
56 topToBottom f (CA top) (CA bot) = CA $ \inc -> do
57 t <- top inc
58 b <- bot (cr_uncov t)
59 pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
60 , cr_uncov = cr_uncov b
61 , cr_approx = cr_approx t Semi.<> cr_approx b }
62
63
64 -- | Composes 'CheckAction's left-to-right:
65 -- If a value falls through the resulting action, then it either falls through the
66 -- first action or through the second action.
67 -- If a value matches the resulting action, then it must match the first action
68 -- and then match the second action.
69 -- Basically the semantics of the LYG guard construct.
70 leftToRight :: (RedSets -> right -> ret)
71 -> CheckAction RedSets
72 -> CheckAction right
73 -> CheckAction ret
74 leftToRight f (CA left) (CA right) = CA $ \inc -> do
75 l <- left inc
76 r <- right (rs_cov (cr_ret l))
77 limit <- maxPmCheckModels <$> getDynFlags
78 let uncov = cr_uncov l Semi.<> cr_uncov r
79 -- See Note [Countering exponential blowup]
80 let (prec', uncov') = throttle limit inc uncov
81 pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
82 , cr_uncov = uncov'
83 , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
84
85 -- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
86 -- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
87 -- See Note [Countering exponential blowup].
88 throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
89 throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
90 --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
91 | length new_ds > max limit (length old_ds) = (Approximate, old)
92 | otherwise = (Precise, new)
93
94 checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
95 -- The implementation is pretty similar to
96 -- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
97 checkSequence act (t :| []) = (:| []) <$> act t
98 checkSequence act (t1 :| (t2:ts)) =
99 topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
100
101 emptyRedSets :: RedSets
102 -- Semigroup instance would be misleading!
103 emptyRedSets = RedSets mempty mempty mempty
104
105 checkGrd :: PmGrd -> CheckAction RedSets
106 checkGrd grd = CA $ \inc -> case grd of
107 -- let x = e: Refine with x ~ e
108 PmLet x e -> do
109 matched <- addPhiCtNablas inc (PhiCoreCt x e)
110 tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
111 pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
112 , cr_uncov = mempty
113 , cr_approx = Precise }
114 -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
115 PmBang x mb_info -> do
116 div <- addPhiCtNablas inc (PhiBotCt x)
117 matched <- addPhiCtNablas inc (PhiNotBotCt x)
118 -- See Note [Dead bang patterns]
119 -- mb_info = Just info <==> PmBang originates from bang pattern in source
120 let bangs | Just info <- mb_info = unitOL (div, info)
121 | otherwise = NilOL
122 tracePm "check:Bang" (ppr x <+> ppr div)
123 pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
124 , cr_uncov = mempty
125 , cr_approx = Precise }
126 -- See point (3) of Note [considerAccessible]
127 PmCon x (PmAltConLike con) _ _ _
128 | x `hasKey` considerAccessibleIdKey
129 , con `hasKey` trueDataConKey
130 -> pure CheckResult { cr_ret = emptyRedSets { rs_cov = initNablas }
131 , cr_uncov = mempty
132 , cr_approx = Precise }
133 -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
134 PmCon x con tvs dicts args -> do
135 !div <- if isPmAltConMatchStrict con
136 then addPhiCtNablas inc (PhiBotCt x)
137 else pure mempty
138 !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
139 !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
140 tracePm "check:Con" $ vcat
141 [ ppr grd
142 , ppr inc
143 , hang (text "div") 2 (ppr div)
144 , hang (text "matched") 2 (ppr matched)
145 , hang (text "uncov") 2 (ppr uncov)
146 ]
147 pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
148 , cr_uncov = uncov
149 , cr_approx = Precise }
150
151 checkGrds :: [PmGrd] -> CheckAction RedSets
152 checkGrds [] = CA $ \inc ->
153 pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
154 , cr_uncov = mempty
155 , cr_approx = Precise }
156 checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
157 where
158 merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
159 RedSets { rs_cov = rs_cov ri_grds
160 , rs_div = rs_div ri_g Semi.<> rs_div ri_grds
161 , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
162
163 checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
164 checkMatchGroup (PmMatchGroup matches) =
165 PmMatchGroup <$> checkSequence checkMatch matches
166
167 checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
168 checkMatch (PmMatch { pm_pats = GrdVec grds, pm_grhss = grhss }) =
169 leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
170
171 checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
172 checkGRHSs (PmGRHSs { pgs_lcls = GrdVec lcls, pgs_grhss = grhss }) =
173 leftToRight PmGRHSs (checkGrds lcls) (checkSequence checkGRHS grhss)
174
175 checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
176 checkGRHS (PmGRHS { pg_grds = GrdVec grds, pg_rhs = rhs_info }) =
177 flip PmGRHS rhs_info <$> checkGrds grds
178
179 checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
180 -- See Note [Checking EmptyCase]
181 checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
182 unc <- addPhiCtNablas inc (PhiNotBotCt var)
183 pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
184
185 checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
186 checkPatBind = coerce checkGRHS
187
188 {- Note [Checking EmptyCase]
189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
190 -XEmptyCase is useful for matching on empty data types like 'Void'. For example,
191 the following is a complete match:
192
193 f :: Void -> ()
194 f x = case x of {}
195
196 Really, -XEmptyCase is the only way to write a program that at the same time is
197 safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
198 (@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
199 exception into divergence (@f x = f x@).
200
201 Semantically, unlike every other case expression, -XEmptyCase is strict in its
202 match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
203 initial Nabla and check if there are any values left to match on.
204
205 Note [Dead bang patterns]
206 ~~~~~~~~~~~~~~~~~~~~~~~~~
207 Consider
208
209 f :: Bool -> Int
210 f True = 1
211 f !x = 2
212
213 Whenever we fall through to the second equation, we will already have evaluated
214 the argument. Thus, the bang pattern serves no purpose and should be warned
215 about. We call this kind of bang patterns "dead". Dead bangs are the ones
216 that under no circumstances can force a thunk that wasn't already forced.
217 Dead bangs are a form of redundant bangs; see below.
218
219 We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
220 where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
221 dead. So for a source bang, we add the refined Nabla and the source info to
222 the 'RedSet's 'rs_bangs'. When collecting stuff to warn, we test that Nabla for
223 inhabitants. If it's empty, we'll warn that it's redundant.
224
225 Note that we don't want to warn for a dead bang that appears on a redundant
226 clause. That is because in that case, we recommend to delete the clause wholly,
227 including its leading pattern match.
228
229 Dead bang patterns are redundant. But there are bang patterns which are
230 redundant that aren't dead, for example
231
232 f !() = 0
233
234 the bang still forces the match variable, before we attempt to match on (). But
235 it is redundant with the forcing done by the () match. We currently don't
236 detect redundant bangs that aren't dead.
237
238 Note [Countering exponential blowup]
239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
240 Precise pattern match exhaustiveness checking is necessarily exponential in
241 the size of some input programs. We implement a counter-measure in the form of
242 the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
243 each pattern by a constant.
244
245 How do we do that? Consider
246
247 f True True = ()
248 f True True = ()
249
250 And imagine we set our limit to 1 for the sake of the example. The first clause
251 will be checked against the initial Nabla, {}. Doing so will produce an
252 Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
253 Also we find the first clause to cover the model {x~True,y~True}.
254
255 But the Uncovered set we get out of the match is too huge! We somehow have to
256 ensure not to make things worse as they are already, so we continue checking
257 with a singleton Uncovered set of the initial Nabla {}. Why is this
258 sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
259 to forgetting that we matched against the first clause. The values represented
260 by {} are a superset of those represented by its two refinements {x≁True} and
261 {x~True,y≁True}.
262
263 This forgetfulness becomes very apparent in the example above: By continuing
264 with {} we don't detect the second clause as redundant, as it again covers the
265 same non-empty subset of {}. So we don't flag everything as redundant anymore,
266 but still will never flag something as redundant that isn't.
267
268 For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
269 and report @f _ _@ as missing, which is a superset of the actual missing
270 matches. But soundness means we will never fail to report a missing match.
271
272 This mechanism is implemented in 'throttle'.
273
274 Guards are an extreme example in this regard, with #11195 being a particularly
275 dreadful example: Since their RHS are often pretty much unique, we split on a
276 variable (the one representing the RHS) that doesn't occur anywhere else in the
277 program, so we don't actually get useful information out of that split!
278
279 Note [considerAccessible]
280 ~~~~~~~~~~~~~~~~~~~~~~~~~
281 Consider (T18610)
282
283 f :: Bool -> Int
284 f x = case (x, x) of
285 (True, True) -> 1
286 (False, False) -> 2
287 (True, False) -> 3 -- Warning: Redundant
288
289 The third case is detected as redundant. But it may be the intent of the
290 programmer to keep the dead code, in order for it not to bitrot or to support
291 debugging scenarios. But there is no way to communicate that to the
292 pattern-match checker! The only way is to deactivate pattern-match checking
293 whole-sale, which is quite annoying. Hence, we define in "GHC.Exts":
294
295 considerAccessible = True
296
297 'considerAccessible' is treated specially by the pattern-match checker in that a
298 guard with it as the scrutinee expression will keep its parent clause alive:
299
300 g :: Bool -> Int
301 g x = case (x, x) of
302 (True, True) -> 1
303 (False, False) -> 2
304 (True, False) | GHC.Exts.considerAccessible -> 3 -- No warning
305
306 The key bits of the implementation are:
307
308 1. Its definition is recognised as known-key (see "GHC.Builtin.Names").
309 2. After "GHC.HsToCore.Pmc.Desugar", the guard will end up as a 'PmCon', where
310 the match var is the known-key 'considerAccessible' and the constructor
311 against which it matches is 'True'.
312 3. We recognise the 'PmCon' in 'GHC.HsToCore.Check.checkGrd' and inflate the
313 incoming set of values for all guards downstream to the unconstrained
314 'initNablas' set, e.g. /all/ values.
315 (The set of values that falls through that particular guard is empty, as
316 matching 'considerAccessible' against 'True' can't fail.)
317
318 Note that 'considerAccessible' breaks the invariant that incoming sets of values
319 reaching syntactic children are subsets of that of the syntactic ancestor:
320 A whole match, like that of the third clause of the example, might have no
321 incoming value, but its single RHS has incoming values because of (3).
322
323 That means the 'is_covered' flag computed in 'GHC.HsToCore.Pmc.cirbsMatch'
324 is irrelevant and should not be used to flag all children as redundant (which is
325 what we used to do).
326
327 We achieve great benefits with a very simple implementation.
328 There are caveats, though:
329
330 (A) Putting potentially failing guards /after/ the
331 'considerAccessible' guard might lead to weird check results, e.g.,
332
333 h :: Bool -> Int
334 h x = case (x, x) of
335 (True, True) -> 1
336 (False, False) -> 2
337 (True, False) | GHC.Exts.considerAccessible, False <- x -> 3
338 -- Warning: Not matched: (_, _)
339
340 That *is* fixable, although we would pay with a much more complicated
341 implementation.
342 (B) If the programmer puts a 'considerAccessible' marker on an accessible
343 clause, the checker doesn't warn about it. E.g.,
344
345 f :: Bool -> Int
346 f True | considerAccessible = 0
347 f False = 1
348
349 will not emit any warning whatsoever. We could implement code that warns
350 here, but it wouldn't be as simple as it is now.
351 -}