Commit 8038cbd9 authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

PmCheck: Formulate as translation between Clause Trees

We used to check `GrdVec`s arising from multiple clauses and guards in
isolation. That resulted in a split between `pmCheck` and
`pmCheckGuards`, the implementations of which were similar, but subtly
different in detail. Also the throttling mechanism described in
`Note [Countering exponential blowup]` ultimately got quite complicated
because it had to cater for both checking functions.

This patch realises that pattern match checking doesn't just consider
single guarded RHSs, but that it's always a whole set of clauses, each
of which can have multiple guarded RHSs in turn. We do so by
translating a list of `Match`es to a `GrdTree`:

```haskell
data GrdTree
  = Rhs !RhsInfo
  | Guard !PmGrd !GrdTree      -- captures lef-to-right  match semantics
  | Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
  | Empty                      -- For -XEmptyCase, neutral element of Sequence
```

Then we have a function `checkGrdTree` that matches a given `GrdTree`
against an incoming set of values, represented by `Deltas`:

```haskell
checkGrdTree :: GrdTree -> Deltas -> CheckResult
...
```

Throttling is isolated to the `Sequence` case and becomes as easy as one
would expect: When the union of uncovered values becomes too big, just
return the original incoming `Deltas` instead (which is always a
superset of the union, thus a sound approximation).

The returned `CheckResult` contains two things:

1. The set of values that were not covered by any of the clauses, for
   exhaustivity warnings.
2. The `AnnotatedTree` that enriches the syntactic structure of the
   input program with divergence and inaccessibility information.

This is `AnnotatedTree`:

```haskell
data AnnotatedTree
  = AccessibleRhs !RhsInfo
  | InaccessibleRhs !RhsInfo
  | MayDiverge !AnnotatedTree
  | SequenceAnn !AnnotatedTree !AnnotatedTree
  | EmptyAnn
```

Crucially, `MayDiverge` asserts that the tree may force diverging
values, so not all of its wrapped clauses can be redundant.

While the set of uncovered values can be used to generate the missing
equations for warning messages, redundant and proper inaccessible
equations can be extracted from `AnnotatedTree` by
`redundantAndInaccessibleRhss`.

For this to work properly, the interface to the Oracle had to change.
There's only `addPmCts` now, which takes a bag of `PmCt`s. There's a
whole bunch of `PmCt` variants to replace the different oracle functions
from before.

The new `AnnotatedTree` structure allows for more accurate warning
reporting (as evidenced by a number of changes spread throughout GHC's
code base), thus we fix #17465.

Fixes #17646 on the go.

Metric Decrease:
    T11822
    T9233
    PmSeriesS
    haddock.compiler
parent 0e57d8a1
This diff is collapsed.
This diff is collapsed.
......@@ -531,7 +531,7 @@ initDelta :: Delta
initDelta = MkDelta initTyState initTmState
instance Outputable Delta where
ppr delta = vcat [
ppr delta = hang (text "Delta") 2 $ vcat [
-- intentionally formatted this way enable the dev to comment in only
-- the info she needs
ppr (delta_tm_st delta),
......
......@@ -700,7 +700,7 @@ cleanEvalProdDmd n = JD { sd = HeadStr, ud = UProd (replicate n useTop) }
{-
************************************************************************
* *
Demand: combining strictness and usage
Demand: Combining Strictness and Usage
* *
************************************************************************
-}
......
......@@ -1139,7 +1139,8 @@ unload_wkr hsc_env keep_linkables pls@PersistentLinkerState{..} = do
-- Code unloading currently disabled due to instability.
-- See #16841.
| False -- otherwise
-- id False, so that the pattern-match checker doesn't complain
| id False -- otherwise
= mapM_ (unloadObj hsc_env) [f | DotO f <- linkableUnlinked lnk]
-- The components of a BCO linkable may contain
-- dot-o files. Which is very confusing.
......
......@@ -1340,12 +1340,15 @@ parseCfgWeights s oldWeights =
= [s1]
| (s1,rest) <- break (== ',') s
= [s1] ++ settings (drop 1 rest)
#if __GLASGOW_HASKELL__ <= 810
| otherwise = panic $ "Invalid cfg parameters." ++ exampleString
#endif
assignment as
| (name, _:val) <- break (== '=') as
= (name,read val)
| otherwise
= panic $ "Invalid cfg parameters." ++ exampleString
exampleString = "Example parameters: uncondWeight=1000," ++
"condBranchWeight=800,switchWeight=0,callWeight=300" ++
",likelyCondWeight=900,unlikelyCondWeight=300" ++
......@@ -1952,7 +1955,7 @@ defaultDynFlags mySettings llvmConfig =
maxRefHoleFits = Just 6,
refLevelHoleFits = Nothing,
maxUncoveredPatterns = 4,
maxPmCheckModels = 100,
maxPmCheckModels = 30,
simplTickFactor = 100,
specConstrThreshold = Just 2000,
specConstrCount = Just 3,
......
......@@ -385,8 +385,10 @@ handleRunStatus step expr bindings final_ids status history
| EvalComplete alloc (EvalException e) <- status
= return (ExecComplete (Left (fromSerializableException e)) alloc)
#if __GLASGOW_HASKELL__ <= 810
| otherwise
= panic "not_tracing" -- actually exhaustive, but GHC can't tell
#endif
resumeExec :: GhcMonad m => (SrcSpan->Bool) -> SingleStep -> m ExecResult
......
......@@ -718,8 +718,10 @@ sequenceChain info weights' blocks@((BasicBlock entry _):_) =
= [masterChain]
| (rest,entry) <- breakChainAt entry masterChain
= [entry,rest]
#if __GLASGOW_HASKELL__ <= 810
| otherwise = pprPanic "Entry point eliminated" $
ppr masterChain
#endif
blockList
= ASSERT(noDups [masterChain])
......
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- | Graph coloring register allocator.
......@@ -376,8 +377,10 @@ graphAddCoalesce (r1, r2) graph
, RegReal _ <- r2
= graph
#if __GLASGOW_HASKELL__ <= 810
| otherwise
= panic "graphAddCoalesce"
#endif
-- | Patch registers in code using the reg -> reg mapping in this graph.
......
{-# LANGUAGE CPP #-}
-- | Clean out unneeded spill\/reload instructions.
--
......@@ -393,9 +394,11 @@ cleanBackward' liveSlotsOnEntry reloadedBy noReloads acc (li : instrs)
cleanBackward liveSlotsOnEntry noReloads' (li : acc) instrs
#if __GLASGOW_HASKELL__ <= 810
-- some other instruction
| otherwise
= cleanBackward liveSlotsOnEntry noReloads (li : acc) instrs
#endif
-- | Combine the associations from all the inward control flow edges.
......@@ -611,4 +614,3 @@ closeAssoc a assoc
intersectAssoc :: Assoc a -> Assoc a -> Assoc a
intersectAssoc a b
= intersectUFM_C (intersectUniqSets) a b
{-# LANGUAGE CPP #-}
-- | Free regs map for SPARC
module RegAlloc.Linear.SPARC.FreeRegs
......@@ -55,7 +56,9 @@ getFreeRegs cls (FreeRegs g f d)
| RcInteger <- cls = map RealRegSingle $ go 1 g 1 0
| RcFloat <- cls = map RealRegSingle $ go 1 f 1 32
| RcDouble <- cls = map (\i -> RealRegPair i (i+1)) $ go 2 d 1 32
#if __GLASGOW_HASKELL__ <= 810
| otherwise = pprPanic "RegAllocLinear.getFreeRegs: Bad register class " (ppr cls)
#endif
where
go _ _ 0 _
= []
......@@ -184,4 +187,3 @@ showFreeRegs regs
++ " integer: " ++ (show $ getFreeRegs RcInteger regs) ++ "\n"
++ " float: " ++ (show $ getFreeRegs RcFloat regs) ++ "\n"
++ " double: " ++ (show $ getFreeRegs RcDouble regs) ++ "\n"
......@@ -743,7 +743,9 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
-- Loop
do_iteration us2 (iteration_no + 1) (counts1:counts_so_far) binds2 rules1
} }
#if __GLASGOW_HASKELL__ <= 810
| otherwise = panic "do_iteration"
#endif
where
(us1, us2) = splitUniqSupply us
......
......@@ -2370,8 +2370,10 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
; return new_ev }
#if __GLASGOW_HASKELL__ <= 810
| otherwise
= panic "rewriteEvidence"
#endif
where
new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
......
......@@ -853,7 +853,9 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name
; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
; return builder_binds } } }
#if __GLASGOW_HASKELL__ <= 810
| otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
#endif
where
mb_match_group
= case dir of
......
......@@ -735,7 +735,9 @@ checkHiBootIface tcg_env boot_info
-- TODO: Maybe setGlobalTypeEnv should be strict.
setGlobalTypeEnv tcg_env_w_binds type_env' }
#if __GLASGOW_HASKELL__ <= 810
| otherwise = panic "checkHiBootIface: unreachable code"
#endif
{- Note [DFun impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -2174,7 +2174,9 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
-- overlap done by dropDominatedAxioms
; return fam_tc } }
#if __GLASGOW_HASKELL__ <= 810
| otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker
#endif
tcFamDecl1 _ (XFamilyDecl nec) = noExtCon nec
-- | Maybe return a list of Bools that say whether a type family was declared
......
......@@ -857,7 +857,7 @@ of ``-W(no-)*``.
:type: dynamic
:category:
:default: 100
:default: 30
The pattern match checker works by assigning symbolic values to each
pattern. We call each such assignment a 'model'. Now, each pattern match
......
T14773b.hs:4:10: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In a pattern binding guards: = ...
T14773b.hs:4:10: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a pattern binding guards:
Guards do not cover entire pattern space
T14773b.hs:4:12: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In a pattern binding guards: | False = ...
T14773b.hs:7:12: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In a pattern binding guards: | False = ...
T2409.hs:6:8: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f _ | () `seq` False = ...
T2409.hs:10:8: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g _ | () `seq` False = ...
......@@ -7,6 +7,22 @@ ds002.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f z = ...
ds002.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
ds002.hs:12:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g x y z = ...
In an equation for ‘g’: g x y z | True = ...
ds002.hs:13:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g x y z | True = ...
ds002.hs:14:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g x y z | True = ...
ds002.hs:15:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g x y z | True = ...
ds002.hs:16:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g x y z | True = ...
ds006.hs:6:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘v’: v | False = ...
ds021.hs:8:11: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f x y z | False = ...
GivenCheck.hs:11:9: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g y | False = ...
GivenCheckSwap.hs:11:9: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g y | False = ...
Running with -XNoAlternativeLayoutRule
layout006.hs:12:4: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f | True = ...
Running with -XAlternativeLayoutRule
layout006.hs:12:2: error: parse error on input ‘|’
......@@ -7,3 +11,7 @@ Running with -XAlternativeLayoutRule -XAlternativeLayoutRuleTransitional
layout006.hs:12:2: warning: [-Walternative-layout-rule-transitional (in -Wdefault)]
transitional layout will not be accepted in the future:
`|' at the same depth as implicit layout block
layout006.hs:12:4: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f | True = ...
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module T12150 where
data Result a = Success a | Error String
......
T11822.hs:33:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=100 limit, so
Pattern match checker ran into -fmax-pmcheck-models=30 limit, so
• Redundant clauses might not be reported at all
• Redundant clauses might be reported as inaccessible
• Patterns reported as unmatched might actually be matched
......@@ -11,15 +11,11 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)]
In an equation for ‘mkTreeNode’:
Patterns not matched:
_ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
(Data.Set.Internal.Bin _ _ _ _) p
where p is not one of {0}
(Data.Set.Internal.Bin _ _ _ _) (Depth _)
_ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
Data.Set.Internal.Tip p
where p is not one of {0}
Data.Set.Internal.Tip (Depth _)
_ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
(Data.Set.Internal.Bin _ _ _ _) p
where p is not one of {0}
(Data.Set.Internal.Bin _ _ _ _) (Depth _)
_ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
Data.Set.Internal.Tip p
where p is not one of {0}
Data.Set.Internal.Tip (Depth _)
...
module Lib where
f :: () -> ()
f _
| False = ()
| otherwise = ()
g :: () -> ()
g ()
| False = ()
| False = ()
| otherwise = ()
h :: () -> ()
h x
| () <- x, False = ()
| False = ()
| otherwise = ()
T17465.hs:5:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f _ | False = ...
T17465.hs:10:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g () | False = ...
T17465.hs:11:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g () | False = ...
T17465.hs:16:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘h’: h x | () <- x, False = ...
T17465.hs:17:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘h’: h x | False = ...
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
module T17646 where
data T a where
A :: T True
B :: T False
g :: ()
g | B <- A = ()
T17646.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘g’: Guards do not cover entire pattern space
T17646.hs:11:5: warning: [-Winaccessible-code (in -Wdefault)]
• Couldn't match type ‘'True’ with ‘'False’
Inaccessible code in
a pattern with constructor: B :: T 'False,
in a pattern binding in
a pattern guard for
an equation for ‘g’
• In the pattern: B
In a stmt of a pattern guard for
an equation for ‘g’:
B <- A
In an equation for ‘g’: g | B <- A = ()
T17646.hs:11:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘g’: g | B <- A = ...
......@@ -3,9 +3,9 @@ T2204.hs:6:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’:
Patterns not matched:
('0':'1':_:_)
['0', p] where p is not one of {'1'}
('0':p:_:_) where p is not one of {'1'}
[]
[p] where p is not one of {'0'}
(p:_:_) where p is not one of {'0'}
['0']
...
......
......@@ -3,8 +3,8 @@ T9951b.hs:7:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’:
Patterns not matched:
('a':'b':_:_)
['a', p] where p is not one of {'b'}
('a':p:_:_) where p is not one of {'b'}
[]
[p] where p is not one of {'a'}
(p:_:_) where p is not one of {'a'}
['a']
...
......@@ -106,6 +106,10 @@ test('T17357', expect_broken(17357), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17376', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17465', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17646', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
......
......@@ -8,18 +8,18 @@ pmc007.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘g’:
Patterns not matched:
('a':'b':_:_)
('a':'c':_:_)
['a', p] where p is not one of {'b', 'c'}
('a':p:_:_) where p is not one of {'b', 'c'}
[]
[p] where p is not one of {'a'}
(p:_:_) where p is not one of {'a'}
['a']
...
pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In a case alternative:
Patterns not matched:
('a':'b':_:_)
('a':'c':_:_)
['a', p] where p is not one of {'b', 'c'}
('a':p:_:_) where p is not one of {'b', 'c'}
[]
[p] where p is not one of {'a'}
(p:_:_) where p is not one of {'a'}
['a']
...
tc017.hs:4:5: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘v’: v | False = ...
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment