Commit 76b1e119 authored by Alexander Vershilov's avatar Alexander Vershilov Committed by Austin Seipp
Browse files

Improve core linter so it catches unsafeCoerce problems (T9122)

Summary:
This is a draft of the patch that is sent for review.

In this patch required changes in linter were introduced
and actual check:

 - new helper function: primRepSizeB
 - primRep check for floating
 - Add access to dynamic flags in linter.
 - Implement additional lint rules.

Reviewers: austin, goldfire, simonpj

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D637

GHC Trac Issues: #9122
parent 504d8a4b
......@@ -89,6 +89,7 @@ We check for
(b) Out-of-scope type variables
(c) Out-of-scope local variables
(d) Ill-kinded types
(e) Incorrect unsafe coercions
If we have done specialisation the we check that there are
(a) No top-level bindings of primitive (unboxed type)
......@@ -122,6 +123,25 @@ For Ids, the type-substituted Id is added to the in_scope set (which
itself is part of the TvSubst we are carrying down), and when we
find an occurrence of an Id, we fetch it from the in-scope set.
Note [Bad unsafe coercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~
For discussion see https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions
Linter introduces additional rules that checks improper coercion between
different types, called bad coercions. Following coercions are forbidden:
(a) coercions between boxed and unboxed values;
(b) coercions between unlifted values of the different sizes, here
active size is checked, i.e. size of the actual value but not
the space allocated for value;
(c) coercions between floating and integral boxed values, this check
is not yet supported for unboxed tuples, as no semantics were
specified for that;
(d) coercions from / to vector type
(e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
(a-e) holds.
************************************************************************
* *
Beginning and ending passes
......@@ -230,7 +250,7 @@ lintPassResult hsc_env pass binds
| not (gopt Opt_DoCoreLinting dflags)
= return ()
| otherwise
= do { let (warns, errs) = lintCoreBindings pass (interactiveInScope hsc_env) binds
= do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
; displayLintResults dflags pass warns errs binds }
where
......@@ -272,7 +292,7 @@ lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr what hsc_env expr
| not (gopt Opt_DoCoreLinting dflags)
= return ()
| Just err <- lintExpr (interactiveInScope hsc_env) expr
| Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
= do { display_lint_err err
; Err.ghcExit dflags 1 }
| otherwise
......@@ -316,12 +336,12 @@ interactiveInScope hsc_env
-- f :: [t] -> [t]
-- where t is a RuntimeUnk (see TcType)
lintCoreBindings :: CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
-- Returns (warnings, errors)
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreBindings pass local_in_scope binds
= initL flags $
lintCoreBindings dflags pass local_in_scope binds
= initL dflags flags $
addLoc TopLevelBindings $
addInScopeVars local_in_scope $
addInScopeVars binders $
......@@ -378,29 +398,31 @@ We use this to check all unfoldings that come in from interfaces
(it is very painful to catch errors otherwise):
-}
lintUnfolding :: SrcLoc
lintUnfolding :: DynFlags
-> SrcLoc
-> [Var] -- Treat these as in scope
-> CoreExpr
-> Maybe MsgDoc -- Nothing => OK
lintUnfolding locn vars expr
lintUnfolding dflags locn vars expr
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
(_warns, errs) = initL defaultLintFlags linter
(_warns, errs) = initL dflags defaultLintFlags linter
linter = addLoc (ImportedUnfolding locn) $
addInScopeVars vars $
lintCoreExpr expr
lintExpr :: [Var] -- Treat these as in scope
lintExpr :: DynFlags
-> [Var] -- Treat these as in scope
-> CoreExpr
-> Maybe MsgDoc -- Nothing => OK
lintExpr vars expr
lintExpr dflags vars expr
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
(_warns, errs) = initL defaultLintFlags linter
(_warns, errs) = initL dflags defaultLintFlags linter
linter = addLoc TopLevelBindings $
addInScopeVars vars $
lintCoreExpr expr
......@@ -1124,13 +1146,48 @@ lintCoercion (CoVarCo cv)
2 (ppr cv)) }
; return (k, s, t, r) }
-- See Note [Bad unsafe coercion]
lintCoercion (UnivCo _prov r ty1 ty2)
= do { k1 <- lintType ty1
; _k2 <- lintType ty2
; k2 <- lintType ty2
-- ; unless (k1 `eqKind` k2) $
-- failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
-- 2 (ppr co))
; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
(checkTypes ty1 ty2)
; return (k1, ty1, ty2, r) }
where
report s = hang (text $ "Unsafe coercion between " ++ s)
2 (vcat [ text "From:" <+> ppr ty1
, text " To:" <+> ppr ty2])
isUnBoxed :: PrimRep -> Bool
isUnBoxed PtrRep = False
isUnBoxed _ = True
checkTypes t1 t2
= case (repType t1, repType t2) of
(UnaryRep _, UnaryRep _) ->
validateCoercion (typePrimRep t1)
(typePrimRep t2)
(UbxTupleRep rep1, UbxTupleRep rep2) -> do
checkWarnL (length rep1 == length rep2)
(report "unboxed tuples of different length")
zipWithM_ checkTypes rep1 rep2
_ -> addWarnL (report "unboxed tuple and ordinary type")
validateCoercion :: PrimRep -> PrimRep -> LintM ()
validateCoercion rep1 rep2
= do { dflags <- getDynFlags
; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
(report "unboxed and boxed value")
; checkWarnL (TyCon.primRepSizeW dflags rep1
== TyCon.primRepSizeW dflags rep2)
(report "unboxed values of different size")
; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
(TyCon.primRepIsFloat rep2)
; case fl of
Nothing -> addWarnL (report "vector types")
Just False -> addWarnL (report "float and integral values")
_ -> return ()
}
lintCoercion (SymCo co)
= do { (k, ty1, ty2, r) <- lintCoercion co
......@@ -1288,8 +1345,10 @@ data LintEnv
= LE { le_flags :: LintFlags -- Linting the result of this pass
, le_loc :: [LintLocInfo] -- Locations
, le_subst :: TvSubst -- Current type substitution; we also use this
} -- to keep track of all the variables in scope,
-- to keep track of all the variables in scope,
-- both Ids and TyVars
, le_dynflags :: DynFlags -- DynamicFlags
}
data LintFlags
= LF { lf_check_global_ids :: Bool -- See Note [Checking for global Ids]
......@@ -1344,6 +1403,9 @@ instance Monad LintM where
Just r -> unLintM (k r) env errs'
Nothing -> (Nothing, errs'))
instance HasDynFlags LintM where
getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
data LintLocInfo
= RhsOf Id -- The variable bound
| LambdaBodyOf Id -- The lambda-binder
......@@ -1356,12 +1418,12 @@ data LintLocInfo
| InType Type -- Inside a type
| InCo Coercion -- Inside a coercion
initL :: LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
initL flags m
initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs -- Errors and warnings
initL dflags flags m
= case unLintM m env (emptyBag, emptyBag) of
(_, errs) -> errs
where
env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [] }
env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
getLintFlags :: LintM LintFlags
getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
......@@ -1370,6 +1432,10 @@ checkL :: Bool -> MsgDoc -> LintM ()
checkL True _ = return ()
checkL False msg = failWithL msg
checkWarnL :: Bool -> MsgDoc -> LintM ()
checkWarnL True _ = return ()
checkWarnL False msg = addWarnL msg
failWithL :: MsgDoc -> LintM a
failWithL msg = LintM $ \ env (warns,errs) ->
(Nothing, (warns, addMsg env errs msg))
......
......@@ -1196,7 +1196,8 @@ tcPragExpr name expr
-- Check for type consistency in the unfolding
whenGOptM Opt_DoCoreLinting $ do
in_scope <- get_in_scope
case lintUnfolding noSrcLoc in_scope core_expr' of
dflags <- getDynFlags
case lintUnfolding dflags noSrcLoc in_scope core_expr' of
Nothing -> return ()
Just fail_msg -> do { mod <- getIfModule
; pprPanic "Iface Lint failure"
......
......@@ -85,6 +85,7 @@ module TyCon(
PrimRep(..), PrimElemRep(..),
tyConPrimRep, isVoidRep, isGcPtrRep,
primRepSizeW, primElemRepSizeB,
primRepIsFloat,
-- * Recursion breaking
RecTcChecker, initRecTc, checkRecTc
......@@ -980,6 +981,14 @@ primElemRepSizeB Word64ElemRep = 8
primElemRepSizeB FloatElemRep = 4
primElemRepSizeB DoubleElemRep = 8
-- | Return if Rep stands for floating type,
-- returns Nothing for vector types.
primRepIsFloat :: PrimRep -> Maybe Bool
primRepIsFloat FloatRep = Just True
primRepIsFloat DoubleRep = Just True
primRepIsFloat (VecRep _ _) = Nothing
primRepIsFloat _ = Just False
{-
************************************************************************
* *
......
......@@ -207,9 +207,11 @@ k /= BOX
----------------------- :: CoVarCoRepr
G |-co z_(s ~R#k t) : s ~Rep k t
G |-ty t1 : k
----------------------------- :: UnivCo
G |-co t1 ==>!_R t2 : t1 ~R k t2
G |-ty t1 : k1
G |-ty t2 : k2
R <= Phant \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
------------------------------------------------------------------------ :: UnivCo
G |-co t1 ==>!_R t2 : t1 ~R k2 t2
G |-co g : t1 ~R k t2
------------------------- :: SymCo
......
......@@ -278,6 +278,7 @@ terminals :: 'terminals_' ::=
| vars_of :: :: vars_of {{ tex \textsf{vars\_of } }}
| not :: :: not {{ tex \neg }}
| isUnLiftedTyCon :: :: isUnLiftenTyCon {{ tex \textsf{isUnLiftedTyCon} }}
| compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
| false :: :: false {{ tex \textsf{false} }}
| true :: :: true {{ tex \textsf{true} }}
| \/ :: :: or {{ tex \vee }}
......@@ -333,6 +334,7 @@ formula :: 'formula_' ::=
| no_duplicates </ bindingi // i /> :: :: no_duplicates_binding
| not formula :: :: not
| isUnLiftedTyCon T :: :: isUnLiftedTyCon
| compatibleUnBoxedTys t1 t2 :: :: compatibleUnBoxedTys
| formula1 /\ formula2 :: :: and
| formula1 \/ formula2 :: :: or
| ( formula ) :: :: parens
......
......@@ -196,6 +196,18 @@ a list of coercions. This is elided in this presentation, as we simply identify
axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
\begin{itemize}
\item both types are unboxed;
\item types should have same size;
\item both types should be either integral or floating;
\item coercion between vector types are not allowed;
\item unboxed tuples should have same length and each element should be coercible to
appropriate element of the target tuple;
\end{itemize}
For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
For futher discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
\subsection{Type constructors}
Type constructors in GHC contain \emph{lots} of information. We leave most of it out
......
......@@ -162,7 +162,7 @@ main = do
getSessionDynFlags >>= setSessionDynFlags . flip gopt_set Opt_SuppressUniques
dflags <- getSessionDynFlags
liftIO $ forM_ exprs $ \(n,e) -> do
case lintExpr [f,scrut] e of
case lintExpr dflags [f,scrut] e of
Just msg -> putMsg dflags (msg $$ text "in" <+> text n)
Nothing -> return ()
putMsg dflags (text n <> char ':')
......
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