Unsound.jp

README.md

@@ -1534,4 +1534,11 @@ Here's the magic diff that we did at some point that we keep bumping up to new G
 
 https://github.com/ucsd-progsys/liquidhaskell/commit/d380018850297b8f1878c33d0e4c586a1fddc2b8#diff-3644b76a8e6b3405f5492d8194da3874R224 
 
+Warnings
+========
+
+Liquid Haskell provides the following warnings:
+
+- `--Wdetect-unsafe` warns if your program includes any unsafe functionality, including `undefined`, `lazy`, or `assume`. Liquid Haskell will admit such functionality even if the implementation is not correct. Disable with `--Wno-detect-unsafe`.
+- `--Werror` makes warnings fatal. 
 

liquidhaskell.cabal

@@ -142,6 +142,7 @@ library
                       Language.Haskell.Liquid.Types.Types
                       Language.Haskell.Liquid.Types.Variance
                       Language.Haskell.Liquid.Types.Visitors
+                      Language.Haskell.Liquid.Types.Warnings
                       Language.Haskell.Liquid.UX.ACSS
                       Language.Haskell.Liquid.UX.Annotate
                       Language.Haskell.Liquid.UX.CTags

src/Language/Haskell/Liquid/Constraint/Monad.hs

@@ -108,6 +108,7 @@ addHole x t γ = do
       env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
       x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
 
+
 --------------------------------------------------------------------------------
 -- | Update annotations for a location, due to (ghost) predicate applications
 --------------------------------------------------------------------------------

src/Language/Haskell/Liquid/GHC/Interface.hs

@@ -433,8 +433,57 @@ processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = d
   bareSpecs  <- makeBareSpecs cfg depGraph specEnv     modSum bareSpec
   let ghcSpec = makeGhcSpec   cfg ghcSrc   logicMap           bareSpecs  
   _          <- liftIO $ saveLiftedSpec ghcSrc ghcSpec 
+  runWarnings cfg $ checkWarnings cfg bareSpec ghcSrc -- JP: Not sure if this is the right spot for this.
   return      $ GI ghcSrc ghcSpec
 
+runWarnings :: Config -> [TWarning Doc] -> Ghc ()
+runWarnings cfg warnings | wError cfg = mapM_ (\w -> throw $ ErrWError (wrnPos w) w) warnings -- JP: Can we show all the warnings?
+runWarnings _   warnings              = liftIO $ mapM_ (putStrLn . showpp) warnings
+
+checkWarnings :: Config -> Ms.BareSpec -> GhcSrc -> [TWarning Doc]
+checkWarnings cfg bareSpec ghcSrc = unsafeWarnings
+  where
+    unsafeWarnings = if detectUnsafe cfg then
+        checkUnsafeWarning bareSpec ghcSrc
+      else
+        mempty
+
+checkUnsafeWarning :: Ms.BareSpec -> GhcSrc -> [TWarning Doc]
+checkUnsafeWarning bareSpec ghcSrc = 
+       checkUnsafeAssume bareSpec
+    <> checkUnsafeLazy bareSpec
+    <> checkUnsafeVar ghcSrc
+  where
+    checkUnsafeAssume bareSpec = 
+        let toWarning (ls, lt) =
+              let span = fSrcSpan ls in
+              WrnUnsafeAssumed span (pprint ls) (pprint lt)
+        in
+        map toWarning $ asmSigs bareSpec
+
+    checkUnsafeLazy bareSpec = 
+        let toWarning ls =
+              let span = fSrcSpan ls in
+              WrnUnsafeLazy span (pprint ls) -- (pprint lt)
+        in
+        map toWarning $ S.toList $ lazy bareSpec
+
+    checkUnsafeVar ghcSrc = 
+        let cbs = giCbs ghcSrc in
+        concatMap checkUnsafeVarCB cbs
+
+    checkUnsafeVarCB (NonRec x e) = checkUnsafeVarCB' x e
+    checkUnsafeVarCB (Rec xes)    = concatMap (uncurry checkUnsafeVarCB') xes
+
+    checkUnsafeVarCB' x e = 
+        let vars = readVars e in
+        let unsafeVars = filter isUnsafeVar vars in
+        map (\unsafeVar -> 
+            let span = Ghc.getSrcSpan x in
+            WrnUnsafeVar span (pprint x) (pprint unsafeVar)
+          ) unsafeVars
+
+
 ---------------------------------------------------------------------------------------
 -- | @makeGhcSrc@ builds all the source-related information needed for consgen 
 ---------------------------------------------------------------------------------------

src/Language/Haskell/Liquid/GHC/Play.hs

@@ -3,15 +3,17 @@
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE PatternSynonyms           #-}
+{-# LANGUAGE TemplateHaskell           #-}
 
 module Language.Haskell.Liquid.GHC.Play where
 
 import Prelude hiding (error)
-import GHC
 import CoreSyn
+import DataCon
+import GHC
+-- import qualified PrelNames as GHC
 import Var
 import TyCoRep hiding (substTysWith)
-import DataCon
 
 import TyCon
 import Type      (tyConAppArgs_maybe, tyConAppTyCon_maybe, binderVar)
@@ -20,14 +22,28 @@ import PrelNames (isStringClassName)
 import           Control.Arrow       ((***))
 import qualified Data.HashMap.Strict as M
 import qualified Data.List           as L
+import qualified Data.Set            as Set
 
 import Language.Haskell.Liquid.GHC.Misc ()
 import Language.Haskell.Liquid.Types.Errors
 
+-- import Debug.Trace
 
 isHoleVar :: Var -> Bool 
 isHoleVar x = L.isPrefixOf "_" (show x)
 
+isUnsafeVar :: Var -> Bool
+isUnsafeVar x = show x `Set.member` unsafeList
+  where
+    unsafeList = Set.fromList ["GHC.Err.undefined"]
+-- isUnsafeVar x = (varUnique $ trace (show (varUnique x) ++ ": " ++ show x) x) `L.elem` traceShowId unsafeList
+--   where
+--     unsafeList = [ GHC.undefinedKey]
+-- TODO: How can we get the `Var` for arbitrary variables? FIXME XXX
+-- isUnsafeVar x = x `Set.member` unsafeList
+--   where
+--     unsafeList = Set.fromList ['undefined]
+
 dataConImplicitIds :: DataCon -> [Id]
 dataConImplicitIds dc = [ x | AnId x <- dataConImplicitTyThings dc]
 

src/Language/Haskell/Liquid/Types/Errors.hs

@@ -64,15 +64,15 @@ import           Data.Aeson                   hiding (Result)
 import qualified Data.HashMap.Strict          as M
 import qualified Data.List                    as L 
 import           System.Directory
-import           System.FilePath
 import           Text.PrettyPrint.HughesPJ 
 import           Text.Parsec.Error            (ParseError)
 import           Text.Parsec.Error            (errorMessages, showErrorMessages)
 
 import           Language.Fixpoint.Types      (pprint, showpp, Tidy (..), PPrint (..), Symbol, Expr)
 import qualified Language.Fixpoint.Misc       as Misc
-import qualified Language.Haskell.Liquid.Misc     as Misc 
+import qualified Language.Haskell.Liquid.Misc as Misc 
 import           Language.Haskell.Liquid.Misc ((<->))
+import           Language.Haskell.Liquid.Types.Warnings
 
 instance PPrint ParseError where
   pprintTidy _ e = vcat $ tail $ text <$> ls
@@ -440,8 +440,62 @@ data TError t =
                 , msg   :: !Doc
                 } -- ^ Sigh. Other.
 
+  | ErrWError   { pos        :: SrcSpan
+                , errWarning :: TWarning t
+                }
+
   deriving (Typeable, Generic , Functor )
 
+
+-- -- | Whether an error should display the position.
+displayPos :: TError t -> Bool
+displayPos ErrSubType{} = True
+displayPos ErrSubTypeModel{} = True
+displayPos ErrFCrash{} = True
+displayPos ErrHole{} = True
+displayPos ErrAssType{} = True
+displayPos ErrParse{} = True
+displayPos ErrTySpec{} = True
+displayPos ErrTermSpec{} = True
+displayPos ErrDupAlias{} = True
+displayPos ErrDupSpecs{} = True
+displayPos ErrDupIMeas{} = True
+displayPos ErrDupMeas{} = True
+displayPos ErrDupField{} = True
+displayPos ErrDupNames{} = True
+displayPos ErrBadData{} = True
+displayPos ErrBadGADT{} = True
+displayPos ErrDataCon{} = True
+displayPos ErrInvt{} = True
+displayPos ErrIAl{} = True
+displayPos ErrIAlMis{} = True
+displayPos ErrMeas{} = True
+displayPos ErrHMeas{} = True
+displayPos ErrUnbound{} = True
+displayPos ErrUnbPred{} = True
+displayPos ErrGhc{} = True
+displayPos ErrResolve{} = True
+displayPos ErrMismatch{} = True
+displayPos ErrPartPred{} = True
+displayPos ErrAliasCycle{} = True
+displayPos ErrIllegalAliasApp{} = True
+displayPos ErrAliasApp{} = True
+displayPos ErrTermin{} = True
+displayPos ErrStTerm{} = True
+displayPos ErrILaw{} = True
+displayPos ErrRClass{} = True
+displayPos ErrMClass{} = True
+displayPos ErrBadQual{} = True
+displayPos ErrSaved{} = True
+displayPos ErrFilePragma{} = True
+displayPos ErrTyCon{} = True
+displayPos ErrLiftExp{} = True
+displayPos ErrParseAnn{} = True
+displayPos ErrNoSpec{} = True
+displayPos ErrOther{} = True
+displayPos ErrWError{} = False
+
+
 errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t
 errDupSpecs d spans@(sp:_) = ErrDupSpecs sp d spans
 errDupSpecs _ _            = impossible Nothing "errDupSpecs with empty spans!"
@@ -482,41 +536,6 @@ dropModel m = case m of
   NoModel t     -> t
   WithModel _ t -> t
 
-instance PPrint SrcSpan where
-  pprintTidy _ = pprSrcSpan
-
-pprSrcSpan :: SrcSpan -> Doc
-pprSrcSpan (UnhelpfulSpan s) = text $ unpackFS s
-pprSrcSpan (RealSrcSpan s)   = pprRealSrcSpan s
-
-pprRealSrcSpan :: RealSrcSpan -> Doc
-pprRealSrcSpan span
-  | sline == eline && scol == ecol =
-    hcat [ pathDoc <-> colon
-         , int sline <-> colon
-         , int scol
-         ]
-  | sline == eline =
-    hcat $ [ pathDoc <-> colon
-           , int sline <-> colon
-           , int scol
-           ] ++ if ecol - scol <= 1 then [] else [char '-' <-> int (ecol - 1)]
-  | otherwise =
-    hcat [ pathDoc <-> colon
-         , parens (int sline <-> comma <-> int scol)
-         , char '-'
-         , parens (int eline <-> comma <-> int ecol')
-         ]
- where
-   path  = srcSpanFile      span
-   sline = srcSpanStartLine span
-   eline = srcSpanEndLine   span
-   scol  = srcSpanStartCol  span
-   ecol  = srcSpanEndCol    span
-
-   pathDoc = text $ normalise $ unpackFS path
-   ecol'   = if ecol == 0 then ecol else ecol - 1
-
 instance Show UserError where
   show = showpp
 
@@ -566,7 +585,10 @@ ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
 --------------------------------------------------------------------------------
 ppError k dCtx e = ppError' k dSp dCtx e
   where
-    dSp          = pprint (pos e) <-> text ": Error:"
+    dSp = if displayPos e then
+        pprint (pos e) <-> text ": Error:"
+      else
+        mempty
 
 nests :: Foldable t => Int -> t Doc -> Doc
 nests n      = foldr (\d acc -> nest n (d $+$ acc)) empty
@@ -713,11 +735,12 @@ totalityType td tE = pprintTidy td tE == text "{VV : Addr# | 5 < 4}"
 hint :: TError a -> Doc 
 hint e = maybe empty (\d -> "" $+$ ("HINT:" <+> d)) (go e) 
   where 
-    go (ErrMismatch {}) = Just "Use the hole '_' instead of the mismatched component (in the Liquid specification)"
-    go (ErrBadGADT {})  = Just "Use the hole '_' to specify the type of the constructor" 
-    go (ErrSubType {})  = Just "Use \"--no-totality\" to deactivate totality checking."
-    go (ErrNoSpec {})   = Just "Run 'liquid' on the source file first."
-    go _                = Nothing 
+    go (ErrMismatch {})       = Just "Use the hole '_' instead of the mismatched component (in the Liquid specification)"
+    go (ErrBadGADT {})        = Just "Use the hole '_' to specify the type of the constructor" 
+    go (ErrSubType {})        = Just "Use \"--no-totality\" to deactivate totality checking."
+    go (ErrNoSpec {})         = Just "Run 'liquid' on the source file first."
+    go (ErrWError {})         = Just "Warning made fatal by \"--Werror\"."
+    go _                      = Nothing 
 
 --------------------------------------------------------------------------------
 ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
@@ -988,6 +1011,10 @@ ppError' _ dSp dCtx (ErrParseAnn _ msg)
   = dSp <+> text "Malformed annotation"
         $+$ dCtx
         $+$ nest 4 msg
+ppError' t dSp dCtx e@(ErrWError _ w)
+  = dSp <+> ppWarning t dCtx w
+        $+$ hint e
+
 
 ppTicks :: PPrint a => a -> Doc
 ppTicks = ticks . pprint 

src/Language/Haskell/Liquid/Types/Types.hs

@@ -182,6 +182,9 @@ module Language.Haskell.Liquid.Types.Types (
   , Error
   , ErrorResult
 
+  -- * Warnings
+  , module Language.Haskell.Liquid.Types.Warnings
+
   -- * Source information (associated with constraints)
   , Cinfo (..)
 
@@ -271,6 +274,7 @@ import qualified Language.Fixpoint.Types as F
 
 import           Language.Haskell.Liquid.GHC.Misc
 import           Language.Haskell.Liquid.Types.Variance
+import           Language.Haskell.Liquid.Types.Warnings
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Misc
 import           Language.Haskell.Liquid.UX.Config
@@ -1850,6 +1854,7 @@ type ErrorResult    = F.FixResult UserError
 type Error          = TError SpecType
 
 
+instance NFData a => NFData (TWarning a)
 instance NFData a => NFData (TError a)
 
 --------------------------------------------------------------------------------