From 76b1e11943d794da61d342c072a783862a9e2a1a Mon Sep 17 00:00:00 2001 From: Alexander Vershilov Date: Sat, 7 Mar 2015 11:13:12 -0600 Subject: 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 --- docs/core-spec/CoreLint.ott | 8 +++++--- docs/core-spec/CoreSyn.ott | 2 ++ docs/core-spec/core-spec.mng | 12 ++++++++++++ docs/core-spec/core-spec.pdf | Bin 339243 -> 340768 bytes 4 files changed, 19 insertions(+), 3 deletions(-) (limited to 'docs/core-spec') diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 56b4b99151..6015731257 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -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 diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index 0c5b30483e..d64667af18 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -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 :: :: no_duplicates_binding | not formula :: :: not | isUnLiftedTyCon T :: :: isUnLiftedTyCon + | compatibleUnBoxedTys t1 t2 :: :: compatibleUnBoxedTys | formula1 /\ formula2 :: :: and | formula1 \/ formula2 :: :: or | ( formula ) :: :: parens diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 28540ac8e9..ddbc6147d4 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -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 diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf index 52f2e39f83..8d2e5cbb13 100644 Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ -- cgit v1.2.1