diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,11 @@ # Revision history for inspection-testing +## 0.4.1 -- 2018-11-17 + +* New obligation `doesNotUse` +* Use the Obligation’s testName in the plugin output. +* In `inspect`, do not override `srcLoc` if already present. + ## 0.4 -- 2018-10-12 * Support GHC-8.6 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -78,7 +78,9 @@ programming) * checking the absence of a certain type (useful in the context of list or stream fusion) + * checking the absence of a a use of certian functions * checking the absence of allocation (generally useful) + * checking the absence of typeclass-overloaded code In general, the checks need to be placed in the same module as the checked-definition. diff --git a/Test/Inspection.hs b/Test/Inspection.hs deleted file mode 100644 --- a/Test/Inspection.hs +++ /dev/null @@ -1,257 +0,0 @@ --- | --- Description : Inspection Testing for Haskell --- Copyright : (c) Joachim Breitner, 2017 --- License : MIT --- Maintainer : mail@joachim-breitner.de --- Portability : GHC specifc --- --- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds --- to GHC the ability to do inspection testing. - -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE CPP #-} -module Test.Inspection ( - -- * Synopsis - -- $synposis - - -- * Registering obligations - inspect, - inspectTest, - Result(..), - -- * Defining obligations - Obligation(..), mkObligation, Property(..), - -- * Convenience functions - -- $convenience - (===), (==-), (=/=), hasNoType, hasNoGenerics, - hasNoTypeClasses, hasNoTypeClassesExcept, -) where - -import Language.Haskell.TH -import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls) -#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) -import Language.Haskell.TH.Syntax (addCorePlugin) -#endif -import Data.Data -import GHC.Exts (lazy) -import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1) - -{- $synposis - -To use inspection testing, you need to - - 1. enable the @TemplateHaskell@ language extension - 2. declare your proof obligations using 'inspect' or 'inspectTest' - -An example module is - -@ -{-\# LANGUAGE TemplateHaskell \#-} -module Simple where - -import Test.Inspection -import Data.Maybe - -lhs, rhs :: (a -> b) -> Maybe a -> Bool -lhs f x = isNothing (fmap f x) -rhs f Nothing = True -rhs f (Just _) = False - -inspect $ 'lhs === 'rhs -@ - -On GHC < 8.4, you have to explicitly load the plugin: -@ -{-\# LANGUAGE TemplateHaskell \#-} -@ --} - --- Description of test obligations - --- | This data type describes an inspection testing obligation. --- --- It is recommended to build it using 'mkObligation', for backwards --- compatibility when new fields are added. You can also use the more --- mnemonic convenience functions like '(===)' or 'hasNoType'. --- --- The obligation needs to be passed to 'inspect'. -data Obligation = Obligation - { target :: Name - -- ^ The target of a test obligation; invariably the name of a local - -- definition. To get the name of a function @foo@, write @'foo@. This requires - -- @{-\# LANGUAGE TemplateHaskell \#-}@. - , property :: Property - -- ^ The property of the target to be checked. - , testName :: Maybe String - -- ^ An optional name for the test - , expectFail :: Bool - -- ^ Do we expect this property to fail? - -- (Only used by 'inspect', not by 'inspectTest') - , srcLoc :: Maybe Loc - -- ^ The source location where this obligation is defined. - -- This is filled in by 'inspect'. - , storeResult :: Maybe String - -- ^ If this is 'Nothing', then report errors during compilation. - -- Otherwise, update the top-level definition with this name. - } - deriving Data - --- | Properties of the obligation target to be checked. -data Property - -- | Are the two functions equal? - -- - -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is - -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are - -- @f = e@ and @g = e@. - -- - -- In general @f@ and @g@ need to be defined in this module, so that their - -- actual defintions can be inspected. - -- - -- If the boolean flag is true, then ignore types during the comparison. - = EqualTo Name Bool - - -- | Do none of these types appear anywhere in the definition of the function - -- (neither locally bound nor passed as arguments) - | NoTypes [Name] - - -- | Does this function perform no heap allocations. - | NoAllocation - - -- | Does this value contain dictionaries (/except/ of the listed classes). - | NoTypeClasses [Name] - deriving Data - --- | Creates an inspection obligation for the given function name --- with default values for the optional fields. -mkObligation :: Name -> Property -> Obligation -mkObligation target prop = Obligation - { target = target - , property = prop - , testName = Nothing - , srcLoc = Nothing - , expectFail = False - , storeResult = Nothing - } - -{- $convenience - -These convenience functions create common test obligations directly. --} - --- | Declare two functions to be equal (see 'EqualTo') -(===) :: Name -> Name -> Obligation -(===) = mkEquality False False -infix 9 === - --- | Declare two functions to be equal, but ignoring --- type lambdas, type arguments and type casts (see 'EqualTo') -(==-) :: Name -> Name -> Obligation -(==-) = mkEquality False True -infix 9 ==- - --- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail') --- (This is useful for documentation purposes, or as a TODO list.) -(=/=) :: Name -> Name -> Obligation -(=/=) = mkEquality True False -infix 9 =/= - -mkEquality :: Bool -> Bool -> Name -> Name -> Obligation -mkEquality expectFail ignore_types n1 n2 = - (mkObligation n1 (EqualTo n2 ignore_types)) - { expectFail = expectFail } - --- | Declare that in a function’s implementation, the given type does not occur. --- --- More precisely: No locally bound variable (let-bound, lambda-bound or --- pattern-bound) has a type that contains the given type constructor. --- --- @'inspect' $ fusedFunction ``hasNoType`` ''[]@ -hasNoType :: Name -> Name -> Obligation -hasNoType n tn = mkObligation n (NoTypes [tn]) - --- | Declare that a function’s implementation does not contain any generic types. --- This is just 'asNoType' applied to the usual type constructors used in --- "GHC.Generics". --- --- @inspect $ hasNoGenerics genericFunction@ -hasNoGenerics :: Name -> Obligation -hasNoGenerics n = - mkObligation n - (NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1 - , ''Par1 - ]) - --- | Declare that a function's implementation does not include dictionaries. --- --- More precisely: No locally bound variable (let-bound, lambda-bound or --- pattern-bound) has a type that contains a type that mentions a type class. --- --- @'inspect' $ 'hasNoTypeClasses' specializedFunction@ -hasNoTypeClasses :: Name -> Obligation -hasNoTypeClasses n = hasNoTypeClassesExcept n [] - --- | A variant of 'hasNoTypeClasses', which white-lists some type-classes. --- --- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@ -hasNoTypeClassesExcept :: Name -> [Name] -> Obligation -hasNoTypeClassesExcept n tns = mkObligation n (NoTypeClasses tns) - --- The exported TH functions - -inspectCommon :: AnnTarget -> Obligation -> Q [Dec] -inspectCommon annTarget obl = do -#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) - addCorePlugin "Test.Inspection.Plugin" -#endif - loc <- location - annExpr <- liftData (obl { srcLoc = Just loc }) - pure $ [PragmaD (AnnP annTarget annExpr)] - --- | As seen in the example above, the entry point to inspection testing is the --- 'inspect' function, to which you pass an 'Obligation'. --- It will report test failures at compile time. -inspect :: Obligation -> Q [Dec] -inspect = inspectCommon ModuleAnnotation - --- | The result of 'inspectTest', which has a more or less helpful text message -data Result = Failure String | Success String - deriving Show - -didNotRunPluginError :: Result -didNotRunPluginError = lazy (error "Test.Inspection.Plugin did not run") -{-# NOINLINE didNotRunPluginError #-} - --- | This is a variant that allows compilation to succeed in any case, --- and instead indicates the result as a value of type 'Result', --- which allows seamless integration into test frameworks. --- --- This variant ignores the 'expectFail' field of the obligation. Instead, --- it is expected that you use the corresponding functionality in your test --- framework (e.g. tasty-expected-failure) -inspectTest :: Obligation -> Q Exp -inspectTest obl = do - nameS <- genName - name <- newUniqueName nameS - anns <- inspectCommon (ValueAnnotation name) obl - addTopDecls $ - [ SigD name (ConT ''Result) - , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) [] - , PragmaD (InlineP name NoInline FunLike AllPhases) - ] ++ anns - return $ VarE name - where - genName = do - (r,c) <- loc_start <$> location - return $ "inspect_" ++ show r ++ "_" ++ show c - --- | Like newName, but even more unique (unique across different splices), --- and with unique @nameBase@s. Precondition: the string is a valid Haskell --- alphanumeric identifier (could be upper- or lower-case). -newUniqueName :: Quasi q => String -> q Name -newUniqueName str = do - n <- qNewName str - qNewName $ show n --- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1 diff --git a/Test/Inspection/Core.hs b/Test/Inspection/Core.hs deleted file mode 100644 --- a/Test/Inspection/Core.hs +++ /dev/null @@ -1,279 +0,0 @@ --- | This module implements some analyses of Core expressions necessary for --- "Test.Inspection". Normally, users of this package can ignore this module. -{-# LANGUAGE CPP, FlexibleContexts #-} -module Test.Inspection.Core - ( slice - , pprSlice - , pprSliceDifference - , eqSlice - , freeOfType - , doesNotAllocate - , doesNotContainTypeClasses - ) where - -import CoreSyn -import CoreUtils -import TyCoRep -import Type -import Var -import Id -import Name -import VarEnv -import Outputable -import PprCore -import Coercion -import Util -import TyCon (TyCon, isClassTyCon) - -import qualified Data.Set as S -import Control.Monad.State.Strict -import Control.Monad.Trans.Maybe -import Data.Maybe - -type Slice = [(Var, CoreExpr)] - --- | Selects those bindings that define the given variable -slice :: [(Var, CoreExpr)] -> Var -> Slice -slice binds v = [(v,e) | (v,e) <- binds, v `S.member` used ] - where - used = execState (goV v) S.empty - - local = S.fromList (map fst binds) - goV v | v `S.member` local = do - seen <- gets (v `S.member`) - unless seen $ do - modify (S.insert v) - let Just e = lookup v binds - go e - | otherwise = return () - - go (Var v) = goV v - go (Lit _ ) = pure () - go (App e arg) | isTyCoArg arg = go e - go (App e arg) = go e >> go arg - go (Lam b e) | isTyVar b = go e - go (Lam _ e) = go e - go (Let bind body) = mapM_ go (rhssOfBind bind) >> go body - go (Case s _ _ alts) = go s >> mapM_ goA alts - go (Cast e _) = go e - go (Tick _ e) = go e - go (Type _) = pure () - go (Coercion _) = pure () - - goA (_, _, e) = go e - --- | Pretty-print a slice -pprSlice :: Slice -> SDoc -pprSlice slice = withLessDetail $ pprCoreBindings [ NonRec v e | (v,e) <- slice ] - --- | Pretty-print two slices, after removing variables occurring in both -pprSliceDifference :: Slice -> Slice -> SDoc -pprSliceDifference slice1 slice2 = - nest 4 (hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1')) $$ - nest 4 (hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2')) - where - both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2)) - slice1' = filter (\(v,_) -> v `S.notMember` both) slice1 - slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 - -withLessDetail :: SDoc -> SDoc -#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) -withLessDetail sdoc = sdocWithDynFlags $ \dflags -> - withPprStyle (defaultUserStyle dflags) sdoc -#else -withLessDetail sdoc = withPprStyle defaultUserStyle sdoc -#endif - -type VarPair = (Var, Var) -type VarPairSet = S.Set VarPair - --- | This is a heuristic, which only works if both slices --- have auxiliary variables in the right order. --- (This is mostly to work-around the buggy CSE in GHC-8.0) --- It also breaks if there is shadowing. -eqSlice :: Bool {- ^ ignore types -} -> Slice -> Slice -> Bool -eqSlice _ slice1 slice2 | null slice1 || null slice2 = null slice1 == null slice2 - -- Mostly defensive programming (slices should not be empty) -eqSlice it slice1 slice2 - = step (S.singleton (fst (last slice1), fst (last slice2))) S.empty - where - step :: VarPairSet -> VarPairSet -> Bool - step wanted done - | wanted `S.isSubsetOf` done - = True -- done - | (x,y) : _ <- S.toList (wanted `S.difference` done) - , (Just _, wanted') <- runState (runMaybeT (equate x y)) wanted - = step wanted' (S.insert (x,y) done) - | otherwise - = False - - - equate :: Var -> Var -> MaybeT (State VarPairSet) () - equate x y - | it - , Just e1 <- lookup x slice1 - , Just x' <- essentiallyVar e1 - = equated x' y - | it - , Just e2 <- lookup y slice2 - , Just y' <- essentiallyVar e2 - = equated x y' - | Just e1 <- lookup x slice1 - , Just e2 <- lookup y slice2 - = go (mkRnEnv2 emptyInScopeSet) e1 e2 - equate _ _ = mzero - - equated :: Var -> Var -> MaybeT (State VarPairSet) () - equated x y | x == y = return () - equated x y = lift $ modify (S.insert (x,y)) - - essentiallyVar :: CoreExpr -> Maybe Var - essentiallyVar (App e a) | isTyCoArg a = essentiallyVar e - essentiallyVar (Lam v e) | isTyCoVar v = essentiallyVar e - essentiallyVar (Cast e _) = essentiallyVar e - essentiallyVar (Var v) = Just v - essentiallyVar _ = Nothing - - go :: RnEnv2 -> CoreExpr -> CoreExpr -> MaybeT (State (S.Set (Var,Var))) () - go env (Var v1) (Var v2) | rnOccL env v1 == rnOccR env v2 = pure () - | otherwise = equated v1 v2 - go _ (Lit lit1) (Lit lit2) = guard $ lit1 == lit2 - go env (Type t1) (Type t2) = guard $ eqTypeX env t1 t2 - go env (Coercion co1) (Coercion co2) = guard $ eqCoercionX env co1 co2 - - go env (Cast e1 _) e2 | it = go env e1 e2 - go env e1 (Cast e2 _) | it = go env e1 e2 - go env (Cast e1 co1) (Cast e2 co2) = do guard (eqCoercionX env co1 co2) - go env e1 e2 - - go env (App e1 a) e2 | it, isTyCoArg a = go env e1 e2 - go env e1 (App e2 a) | it, isTyCoArg a = go env e1 e2 - go env (App f1 a1) (App f2 a2) = go env f1 f2 >> go env a1 a2 - go env (Tick n1 e1) (Tick n2 e2) = guard (go_tick env n1 n2) >> go env e1 e2 - - go env (Lam b e1) e2 | it, isTyCoVar b = go env e1 e2 - go env e1 (Lam b e2) | it, isTyCoVar b = go env e1 e2 - go env (Lam b1 e1) (Lam b2 e2) - = do guard (it || eqTypeX env (varType b1) (varType b2)) - -- False for Id/TyVar combination - go (rnBndr2 env b1 b2) e1 e2 - - go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) - = do go env r1 r2 -- No need to check binder types, since RHSs match - go (rnBndr2 env v1 v2) e1 e2 - - go env (Let (Rec ps1) e1) (Let (Rec ps2) e2) - = do guard $ equalLength ps1 ps2 - sequence_ $ zipWith (go env') rs1 rs2 - go env' e1 e2 - where - (bs1,rs1) = unzip ps1 - (bs2,rs2) = unzip ps2 - env' = rnBndrs2 env bs1 bs2 - - go env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) - | null a1 -- See Note [Empty case alternatives] in TrieMap - = do guard (null a2) - go env e1 e2 - guard (it || eqTypeX env t1 t2) - | otherwise - = do guard $ equalLength a1 a2 - go env e1 e2 - sequence_ $ zipWith (go_alt (rnBndr2 env b1 b2)) a1 a2 - - go _ _ _ = guard False - - ----------- - go_alt env (c1, bs1, e1) (c2, bs2, e2) - = guard (c1 == c2) >> go (rnBndrs2 env bs1 bs2) e1 e2 - - go_tick :: RnEnv2 -> Tickish Id -> Tickish Id -> Bool - go_tick env (Breakpoint lid lids) (Breakpoint rid rids) - = lid == rid && map (rnOccL env) lids == map (rnOccR env) rids - go_tick _ l r = l == r - - - --- | Returns @True@ if the given core expression mentions no type constructor --- anywhere that has the given name. -freeOfType :: Slice -> Name -> Maybe (Var, CoreExpr) -freeOfType slice tcN = allTyCons (\tc -> getName tc /= tcN) slice - -allTyCons :: (TyCon -> Bool) -> Slice -> Maybe (Var, CoreExpr) -allTyCons predicate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ] - where - goV v = goT (varType v) - - go (Var v) = goV v - go (Lit _ ) = True - go (App e a) = go e && go a - go (Lam b e) = goV b && go e - go (Let bind body) = all goB (flattenBinds [bind]) && go body - go (Case s b _ alts) = go s && goV b && all goA alts - go (Cast e _) = go e - go (Tick _ e) = go e - go (Type t) = (goT t) - go (Coercion _) = True - - goB (b, e) = goV b && go e - - goA (_,pats, e) = all goV pats && go e - - goT (TyVarTy _) = True - goT (AppTy t1 t2) = goT t1 && goT t2 - goT (TyConApp tc ts) = predicate tc && all goT ts - -- ↑ This is the crucial bit - goT (ForAllTy _ t) = goT t -#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) - goT (FunTy t1 t2) = goT t1 && goT t2 -#endif - goT (LitTy _) = True - goT (CastTy t _) = goT t - goT (CoercionTy _) = True - --- | True if the given variable binding does not allocate, if called fully --- satisfied. --- --- It currently does not look through function calls, which of course could --- allocate. It should probably at least look through local function calls. --- --- The variable is important to know the arity of the function. -doesNotAllocate :: Slice -> Maybe (Var, CoreExpr) -doesNotAllocate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go (idArity v) e) ] - where - go _ (Var v) - | isDataConWorkId v, idArity v > 0 = False - go a (Var v) = (a >= idArity v) - go _ (Lit _ ) = True - go a (App e arg) | isTypeArg arg = go a e - go a (App e arg) = go (a+1) e && goArg arg - go a (Lam b e) | isTyVar b = go a e - go 0 (Lam _ _) = False - go a (Lam _ e) = go (a-1) e - go a (Let bind body) = all goB (flattenBinds [bind]) && go a body - go a (Case s _ _ alts) = go 0 s && all (goA a) alts - go a (Cast e _) = go a e - go a (Tick _ e) = go a e - go _ (Type _) = True - go _ (Coercion _) = True - - goArg e | exprIsTrivial e = go 0 e - | isUnliftedType (exprType e) = go 0 e - | otherwise = False - - goB (b, e) -#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) - | isJoinId b = go (idArity b) e -#endif - -- Not sure when a local function definition allocates… - | isFunTy (idType b) = go (idArity b) e - | isUnliftedType (idType b) = go (idArity b) e - | otherwise = False - -- A let binding allocates if any variable is not a join point and not - -- unlifted - - goA a (_,_, e) = go a e - -doesNotContainTypeClasses :: Slice -> [Name] -> Maybe (Var, CoreExpr) -doesNotContainTypeClasses slice tcNs - = allTyCons (\tc -> not (isClassTyCon tc) || any (getName tc ==) tcNs) slice diff --git a/Test/Inspection/Plugin.hs b/Test/Inspection/Plugin.hs deleted file mode 100644 --- a/Test/Inspection/Plugin.hs +++ /dev/null @@ -1,289 +0,0 @@ --- | See "Test.Inspection". --- -{-# LANGUAGE CPP #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE LambdaCase #-} -module Test.Inspection.Plugin (plugin) where - -import Control.Monad -import System.Exit -import Data.Either -import Data.Maybe -import Data.Bifunctor -import Data.List -import qualified Data.Map.Strict as M -import qualified Language.Haskell.TH.Syntax as TH - -import GhcPlugins hiding (SrcLoc) -import Outputable - -import Test.Inspection (Obligation(..), Property(..), Result(..)) -import Test.Inspection.Core - --- | The plugin. It supports the option @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to --- ignore a failing build. -plugin :: Plugin -plugin = defaultPlugin { installCoreToDos = install } - -data UponFailure = AbortCompilation | KeepGoing deriving Eq - -data ResultTarget = PrintAndAbort | StoreAt Name - -install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] -install args passes = return $ passes ++ [pass] - where - pass = CoreDoPluginPass "Test.Inspection.Plugin" (proofPass upon_failure) - upon_failure | "keep-going" `elem` args = KeepGoing - | otherwise = AbortCompilation - - -extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)]) -extractObligations guts = (guts', obligations) - where - (anns_clean, obligations) = partitionMaybe findObligationAnn (mg_anns guts) - guts' = guts { mg_anns = anns_clean } - -findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation) -findObligationAnn (Annotation (ModuleTarget _) payload) - | Just obl <- fromSerialized deserializeWithData payload - = Just (PrintAndAbort, obl) -findObligationAnn (Annotation (NamedTarget n) payload) - | Just obl <- fromSerialized deserializeWithData payload - = Just (StoreAt n, obl) -findObligationAnn _ - = Nothing - -prettyObligation :: Module -> Obligation -> String -> String -prettyObligation mod (Obligation {..}) result = - maybe "" myPrettySrcLoc srcLoc ++ ": " ++ - prettyProperty mod target property ++ - " " ++ result - -prettyProperty :: Module -> TH.Name -> Property -> String -prettyProperty mod target (EqualTo n2 False) = showTHName mod target ++ " === " ++ showTHName mod n2 -prettyProperty mod target (EqualTo n2 True) = showTHName mod target ++ " ==- " ++ showTHName mod n2 -prettyProperty mod target (NoTypes [t]) = showTHName mod target ++ " `hasNoType` " ++ showTHName mod t -prettyProperty mod target (NoTypes ts) = showTHName mod target ++ " mentions none of " ++ intercalate ", " (map (showTHName mod) ts) -prettyProperty mod target NoAllocation = showTHName mod target ++ " does not allocate" -prettyProperty mod target (NoTypeClasses []) = showTHName mod target ++ " does not contain dictionary values" -prettyProperty mod target (NoTypeClasses ts) = showTHName mod target ++ " does not contain dictionary values except of " ++ intercalate ", " (map (showTHName mod) ts) - --- | Like show, but omit the module name if it is he current module -showTHName :: Module -> TH.Name -> String -showTHName mod (TH.Name occ (TH.NameQ m)) - | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ -showTHName mod (TH.Name occ (TH.NameG _ _ m)) - | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ -showTHName _ n = show n - -data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult - deriving (Enum, Eq, Ord, Bounded) -type Stats = M.Map Stat Int - -type Updates = [(Name, Result)] - -tick :: Stat -> Stats -tick s = M.singleton s 1 - -checkObligation :: ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats) -checkObligation guts (reportTarget, obl) = do - - res <- checkProperty guts (target obl) (property obl) - case reportTarget of - PrintAndAbort -> do - category <- case (res, expectFail obl) of - -- Property holds - (Nothing, False) -> do - putMsgS $ prettyObligation (mg_module guts) obl expSuccess - return ExpSuccess - (Nothing, True) -> do - putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess - return UnexpSuccess - -- Property does not hold - (Just reportDoc, False) -> do - putMsgS $ prettyObligation (mg_module guts) obl unexpFailure - putMsg $ reportDoc - return UnexpFailure - (Just _, True) -> do - putMsgS $ prettyObligation (mg_module guts) obl expFailure - return ExpFailure - return ([], tick category) - StoreAt name -> do - dflags <- getDynFlags - let result = case res of - Nothing -> Success $ showSDoc dflags $ - text (prettyObligation (mg_module guts) obl expSuccess) - Just reportMsg -> Failure $ showSDoc dflags $ - text (prettyObligation (mg_module guts) obl unexpFailure) $$ - reportMsg - pure ([(name, result)], tick StoredResult) - - where - expSuccess = "passed." - unexpSuccess = "passed unexpectedly!" - unexpFailure = "failed:" - expFailure = "failed expectedly." - - -type CheckResult = Maybe SDoc - -lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr) -lookupNameInGuts guts n = listToMaybe - [ (v,e) - | (v,e) <- flattenBinds (mg_binds guts) - , getName v == n - ] - -updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts -updateNameInGuts n expr guts = - guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) } - -updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind -updateNameInGut n e (NonRec v _) | getName v == n = NonRec v e -updateNameInGut _ _ bind = bind - -checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult -checkProperty guts thn1 (EqualTo thn2 ignore_types) = do - n1 <- fromTHName thn1 - n2 <- fromTHName thn2 - - let p1 = lookupNameInGuts guts n1 - let p2 = lookupNameInGuts guts n2 - - if | n1 == n2 - -> return Nothing - -- Ok if one points to another - | Just (_, Var other) <- p1, getName other == n2 - -> return Nothing - | Just (_, Var other) <- p2, getName other == n1 - -> return Nothing - | Just (v1, _) <- p1 - , Just (v2, _) <- p2 - , let slice1 = slice binds v1 - , let slice2 = slice binds v2 - -> if eqSlice ignore_types slice1 slice2 - -- OK if they have the same expression - then return Nothing - -- Not ok if the expression differ - else pure . Just $ pprSliceDifference slice1 slice2 - -- Not ok if both names are bound externally - | Nothing <- p1 - , Nothing <- p2 - -> pure . Just $ ppr n1 <+> text " and " <+> ppr n2 <+> - text "are different external names" - | Nothing <- p1 - -> pure . Just $ ppr n1 <+> text "is an external name" - | Nothing <- p2 - -> pure . Just $ ppr n2 <+> text "is an external name" - where - binds = flattenBinds (mg_binds guts) - -checkProperty guts thn (NoTypes thts) = do - n <- fromTHName thn - ts <- mapM fromTHName thts - case lookupNameInGuts guts n of - Nothing -> pure . Just $ ppr n <+> text "is not a local name" - Just (v, _) -> case msum $ map (freeOfType (slice binds v)) ts of - Just _ -> pure . Just $ pprSlice (slice binds v) - Nothing -> pure Nothing - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn NoAllocation = do - n <- fromTHName thn - case lookupNameInGuts guts n of - Nothing -> pure . Just $ ppr n <+> text "is not a local name" - Just (v, _) -> case doesNotAllocate (slice binds v) of - Just (v',e') -> pure . Just $ nest 4 (ppr v' <+> text "=" <+> ppr e') - Nothing -> pure Nothing - where binds = flattenBinds (mg_binds guts) - -checkProperty guts thn (NoTypeClasses thts) = do - n <- fromTHName thn - ts <- mapM fromTHName thts - case lookupNameInGuts guts n of - Nothing -> pure . Just $ ppr n <+> text "is not a local name" - Just (v, _) -> case doesNotContainTypeClasses (slice binds v) ts of - Just (v',e') -> pure . Just $ nest 4 (ppr v' <+> text "=" <+> ppr e') - Nothing -> pure Nothing - where binds = flattenBinds (mg_binds guts) - - -fromTHName :: TH.Name -> CoreM Name -fromTHName thn = thNameToGhcName thn >>= \case - Nothing -> do - errorMsg $ text "Could not resolve TH name" <+> text (show thn) - liftIO $ exitFailure -- kill the compiler. Is there a nicer way? - Just n -> return n - -storeResults :: Updates -> ModGuts -> CoreM ModGuts -storeResults = flip (foldM (flip (uncurry go))) - where - go :: Name -> Result -> ModGuts -> CoreM ModGuts - go name res guts = do - e <- resultToExpr res - pure $ updateNameInGuts name e guts - -dcExpr :: TH.Name -> CoreM CoreExpr -dcExpr thn = do - name <- fromTHName thn - dc <- lookupDataCon name - pure $ Var (dataConWrapId dc) - -resultToExpr :: Result -> CoreM CoreExpr -resultToExpr (Success s) = App <$> dcExpr 'Success <*> mkStringExpr s -resultToExpr (Failure s) = App <$> dcExpr 'Failure <*> mkStringExpr s - -proofPass :: UponFailure -> ModGuts -> CoreM ModGuts -proofPass upon_failure guts = do - dflags <- getDynFlags - when (optLevel dflags < 1) $ - warnMsg $ fsep $ map text $ words "Test.Inspection: Compilation without -O detected. Expect optimizations to fail." - - let (guts', obligations) = extractObligations guts - (toStore, stats) <- (concat `bimap` M.unionsWith (+)) . unzip <$> - mapM (checkObligation guts') obligations - let n = sum stats :: Int - - guts'' <- storeResults toStore guts' - - let q :: Stat -> Int - q s = fromMaybe 0 $ M.lookup s stats - - let summary_message = nest 2 $ - vcat [ nest 2 (desc s) Outputable.<> colon <+> ppr (q s) - | s <- [minBound..maxBound], q s > 0 ] - - -- Only print a message if there are some compile-time results to report - unless (q StoredResult == n) $ do - if q ExpSuccess + q ExpFailure + q StoredResult == n - then putMsg $ text "inspection testing successful" $$ summary_message - else case upon_failure of - AbortCompilation -> do - errorMsg $ text "inspection testing unsuccessful" $$ summary_message - liftIO $ exitFailure -- kill the compiler. Is there a nicer way? - KeepGoing -> do - warnMsg $ text "inspection testing unsuccessful" $$ summary_message - - return guts'' - - -desc :: Stat -> SDoc -desc ExpSuccess = text " expected successes" -desc UnexpSuccess = text "unexpected successes" -desc ExpFailure = text " expected failures" -desc UnexpFailure = text " unexpected failures" -desc StoredResult = text " results stored" - -partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b]) -partitionMaybe f = partitionEithers . map (\x -> maybe (Left x) Right (f x)) - --- | like prettySrcLoc, but omits the module name -myPrettySrcLoc :: TH.Loc -> String -myPrettySrcLoc TH.Loc {..} - = foldr (++) "" - [ loc_filename, ":" - , show (fst loc_start), ":" - , show (snd loc_start) - ] diff --git a/examples/DoesNotUse.hs b/examples/DoesNotUse.hs new file mode 100644 --- /dev/null +++ b/examples/DoesNotUse.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE TemplateHaskell #-} +module DoesNotUse where + +import Test.Inspection +import Control.Exception.Base (patError) + +matches (Just _) = True +matches Nothing = False + +partial (Just _) = Nothing + + +inspect $ ('matches `doesNotUse` 'Just) { expectFail = True } +inspect $ 'matches `doesNotUse` 'patError +inspect $ ('partial `doesNotUse` 'patError) { expectFail = True } +inspect $ ('partial `doesNotUse` 'Nothing) { expectFail = True } + +main :: IO () +main = return () diff --git a/inspection-testing.cabal b/inspection-testing.cabal --- a/inspection-testing.cabal +++ b/inspection-testing.cabal @@ -1,5 +1,5 @@ name: inspection-testing -version: 0.4 +version: 0.4.1 synopsis: GHC plugin to do inspection testing description: Some carefully crafted libraries make promises to their users beyond functionality and performance. @@ -44,6 +44,7 @@ exposed-modules: Test.Inspection Test.Inspection.Plugin Test.Inspection.Core + hs-source-dirs: src build-depends: base >=4.9 && <4.13 build-depends: ghc >= 8.0.2 && <8.7 build-depends: template-haskell @@ -82,6 +83,17 @@ build-depends: inspection-testing build-depends: base >=4.9 && <4.13 default-language: Haskell2010 + if impl(ghc < 8.4) + ghc-options: -fplugin=Test.Inspection.Plugin + +test-suite doesnotuse + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: DoesNotUse.hs + build-depends: inspection-testing + build-depends: base >=4.9 && <4.13 + default-language: Haskell2010 + ghc-options: -main-is DoesNotUse if impl(ghc < 8.4) ghc-options: -fplugin=Test.Inspection.Plugin diff --git a/src/Test/Inspection.hs b/src/Test/Inspection.hs new file mode 100644 --- /dev/null +++ b/src/Test/Inspection.hs @@ -0,0 +1,270 @@ +-- | +-- Description : Inspection Testing for Haskell +-- Copyright : (c) Joachim Breitner, 2017 +-- License : MIT +-- Maintainer : mail@joachim-breitner.de +-- Portability : GHC specifc +-- +-- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds +-- to GHC the ability to do inspection testing. + +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE CPP #-} +module Test.Inspection ( + -- * Synopsis + -- $synposis + + -- * Registering obligations + inspect, + inspectTest, + Result(..), + -- * Defining obligations + Obligation(..), mkObligation, Property(..), + -- * Convenience functions + -- $convenience + (===), (==-), (=/=), hasNoType, hasNoGenerics, + hasNoTypeClasses, hasNoTypeClassesExcept, + doesNotUse, +) where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls) +#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) +import Language.Haskell.TH.Syntax (addCorePlugin) +#endif +import Data.Data +import Data.Maybe +import GHC.Exts (lazy) +import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1) + +{- $synposis + +To use inspection testing, you need to + + 1. enable the @TemplateHaskell@ language extension + 2. declare your proof obligations using 'inspect' or 'inspectTest' + +An example module is + +@ +{-\# LANGUAGE TemplateHaskell \#-} +module Simple where + +import Test.Inspection +import Data.Maybe + +lhs, rhs :: (a -> b) -> Maybe a -> Bool +lhs f x = isNothing (fmap f x) +rhs f Nothing = True +rhs f (Just _) = False + +inspect $ 'lhs === 'rhs +@ + +On GHC < 8.4, you have to explicitly load the plugin: +@ +{-\# LANGUAGE TemplateHaskell \#-} +@ +-} + +-- Description of test obligations + +-- | This data type describes an inspection testing obligation. +-- +-- It is recommended to build it using 'mkObligation', for backwards +-- compatibility when new fields are added. You can also use the more +-- mnemonic convenience functions like '(===)' or 'hasNoType'. +-- +-- The obligation needs to be passed to 'inspect'. +data Obligation = Obligation + { target :: Name + -- ^ The target of a test obligation; invariably the name of a local + -- definition. To get the name of a function @foo@, write @'foo@. This requires + -- @{-\# LANGUAGE TemplateHaskell \#-}@. + , property :: Property + -- ^ The property of the target to be checked. + , testName :: Maybe String + -- ^ An optional name for the test + , expectFail :: Bool + -- ^ Do we expect this property to fail? + -- (Only used by 'inspect', not by 'inspectTest') + , srcLoc :: Maybe Loc + -- ^ The source location where this obligation is defined. + -- This is filled in by 'inspect'. + , storeResult :: Maybe String + -- ^ If this is 'Nothing', then report errors during compilation. + -- Otherwise, update the top-level definition with this name. + } + deriving Data + +-- | Properties of the obligation target to be checked. +data Property + -- | Are the two functions equal? + -- + -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is + -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are + -- @f = e@ and @g = e@. + -- + -- In general @f@ and @g@ need to be defined in this module, so that their + -- actual defintions can be inspected. + -- + -- If the boolean flag is true, then ignore types during the comparison. + = EqualTo Name Bool + + -- | Do none of these types appear anywhere in the definition of the function + -- (neither locally bound nor passed as arguments) + | NoTypes [Name] + + -- | Does this function perform no heap allocations. + | NoAllocation + + -- | Does this value contain dictionaries (/except/ of the listed classes). + | NoTypeClasses [Name] + + -- | Does not contain this value (in terms or patterns) + | NoUseOf [Name] + deriving Data + +-- | Creates an inspection obligation for the given function name +-- with default values for the optional fields. +mkObligation :: Name -> Property -> Obligation +mkObligation target prop = Obligation + { target = target + , property = prop + , testName = Nothing + , srcLoc = Nothing + , expectFail = False + , storeResult = Nothing + } + +{- $convenience + +These convenience functions create common test obligations directly. +-} + +-- | Declare two functions to be equal (see 'EqualTo') +(===) :: Name -> Name -> Obligation +(===) = mkEquality False False +infix 9 === + +-- | Declare two functions to be equal, but ignoring +-- type lambdas, type arguments and type casts (see 'EqualTo') +(==-) :: Name -> Name -> Obligation +(==-) = mkEquality False True +infix 9 ==- + +-- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail') +-- (This is useful for documentation purposes, or as a TODO list.) +(=/=) :: Name -> Name -> Obligation +(=/=) = mkEquality True False +infix 9 =/= + +mkEquality :: Bool -> Bool -> Name -> Name -> Obligation +mkEquality expectFail ignore_types n1 n2 = + (mkObligation n1 (EqualTo n2 ignore_types)) + { expectFail = expectFail } + +-- | Declare that in a function’s implementation, the given type does not occur. +-- +-- More precisely: No locally bound variable (let-bound, lambda-bound or +-- pattern-bound) has a type that contains the given type constructor. +-- +-- @'inspect' $ fusedFunction ``hasNoType`` ''[]@ +hasNoType :: Name -> Name -> Obligation +hasNoType n tn = mkObligation n (NoTypes [tn]) + +-- | Declare that a function’s implementation does not contain any generic types. +-- This is just 'asNoType' applied to the usual type constructors used in +-- "GHC.Generics". +-- +-- @inspect $ hasNoGenerics genericFunction@ +hasNoGenerics :: Name -> Obligation +hasNoGenerics n = + mkObligation n + (NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1 + , ''Par1 + ]) + +-- | Declare that a function's implementation does not include dictionaries. +-- +-- More precisely: No locally bound variable (let-bound, lambda-bound or +-- pattern-bound) has a type that contains a type that mentions a type class. +-- +-- @'inspect' $ 'hasNoTypeClasses' specializedFunction@ +hasNoTypeClasses :: Name -> Obligation +hasNoTypeClasses n = hasNoTypeClassesExcept n [] + +-- | A variant of 'hasNoTypeClasses', which white-lists some type-classes. +-- +-- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@ +hasNoTypeClassesExcept :: Name -> [Name] -> Obligation +hasNoTypeClassesExcept n tns = mkObligation n (NoTypeClasses tns) + +-- | Declare that a function's implementation does not use the given +-- variable (either in terms or -- if it is a constructor -- in patterns). +-- +-- @'inspect' $ foo ``doesNotUse`` 'error@ +doesNotUse :: Name -> Name -> Obligation +doesNotUse n ns = mkObligation n (NoUseOf [ns]) + + +-- The exported TH functions + +inspectCommon :: AnnTarget -> Obligation -> Q [Dec] +inspectCommon annTarget obl = do +#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0) + addCorePlugin "Test.Inspection.Plugin" +#endif + loc <- location + annExpr <- liftData (obl { srcLoc = Just $ fromMaybe loc $ srcLoc obl }) + pure [PragmaD (AnnP annTarget annExpr)] + +-- | As seen in the example above, the entry point to inspection testing is the +-- 'inspect' function, to which you pass an 'Obligation'. +-- It will report test failures at compile time. +inspect :: Obligation -> Q [Dec] +inspect = inspectCommon ModuleAnnotation + +-- | The result of 'inspectTest', which has a more or less helpful text message +data Result = Failure String | Success String + deriving Show + +didNotRunPluginError :: Result +didNotRunPluginError = lazy (error "Test.Inspection.Plugin did not run") +{-# NOINLINE didNotRunPluginError #-} + +-- | This is a variant that allows compilation to succeed in any case, +-- and instead indicates the result as a value of type 'Result', +-- which allows seamless integration into test frameworks. +-- +-- This variant ignores the 'expectFail' field of the obligation. Instead, +-- it is expected that you use the corresponding functionality in your test +-- framework (e.g. tasty-expected-failure) +inspectTest :: Obligation -> Q Exp +inspectTest obl = do + nameS <- genName + name <- newUniqueName nameS + anns <- inspectCommon (ValueAnnotation name) obl + addTopDecls $ + [ SigD name (ConT ''Result) + , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) [] + , PragmaD (InlineP name NoInline FunLike AllPhases) + ] ++ anns + return $ VarE name + where + genName = do + (r,c) <- loc_start <$> location + return $ "inspect_" ++ show r ++ "_" ++ show c + +-- | Like newName, but even more unique (unique across different splices), +-- and with unique @nameBase@s. Precondition: the string is a valid Haskell +-- alphanumeric identifier (could be upper- or lower-case). +newUniqueName :: Quasi q => String -> q Name +newUniqueName str = do + n <- qNewName str + qNewName $ show n +-- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1 diff --git a/src/Test/Inspection/Core.hs b/src/Test/Inspection/Core.hs new file mode 100644 --- /dev/null +++ b/src/Test/Inspection/Core.hs @@ -0,0 +1,309 @@ +-- | This module implements some analyses of Core expressions necessary for +-- "Test.Inspection". Normally, users of this package can ignore this module. +{-# LANGUAGE CPP, FlexibleContexts #-} +module Test.Inspection.Core + ( slice + , pprSlice + , pprSliceDifference + , eqSlice + , freeOfType + , freeOfTerm + , doesNotAllocate + , doesNotContainTypeClasses + ) where + +import CoreSyn +import CoreUtils +import TyCoRep +import Type +import Var +import Id +import Name +import VarEnv +import Outputable +import PprCore +import Coercion +import Util +import DataCon +import TyCon (TyCon, isClassTyCon) + +import qualified Data.Set as S +import Control.Monad.State.Strict +import Control.Monad.Trans.Maybe +import Data.Maybe + +type Slice = [(Var, CoreExpr)] + +-- | Selects those bindings that define the given variable +slice :: [(Var, CoreExpr)] -> Var -> Slice +slice binds v = [(v,e) | (v,e) <- binds, v `S.member` used ] + where + used = execState (goV v) S.empty + + local = S.fromList (map fst binds) + goV v | v `S.member` local = do + seen <- gets (v `S.member`) + unless seen $ do + modify (S.insert v) + let Just e = lookup v binds + go e + | otherwise = return () + + go (Var v) = goV v + go (Lit _ ) = pure () + go (App e arg) | isTyCoArg arg = go e + go (App e arg) = go e >> go arg + go (Lam b e) | isTyVar b = go e + go (Lam _ e) = go e + go (Let bind body) = mapM_ go (rhssOfBind bind) >> go body + go (Case s _ _ alts) = go s >> mapM_ goA alts + go (Cast e _) = go e + go (Tick _ e) = go e + go (Type _) = pure () + go (Coercion _) = pure () + + goA (_, _, e) = go e + +-- | Pretty-print a slice +pprSlice :: Slice -> SDoc +pprSlice slice = withLessDetail $ pprCoreBindings [ NonRec v e | (v,e) <- slice ] + +-- | Pretty-print two slices, after removing variables occurring in both +pprSliceDifference :: Slice -> Slice -> SDoc +pprSliceDifference slice1 slice2 = + nest 4 (hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1')) $$ + nest 4 (hang (text "RHS" Outputable.<> colon) 4 (pprSlice slice2')) + where + both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2)) + slice1' = filter (\(v,_) -> v `S.notMember` both) slice1 + slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 + +withLessDetail :: SDoc -> SDoc +#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) +withLessDetail sdoc = sdocWithDynFlags $ \dflags -> + withPprStyle (defaultUserStyle dflags) sdoc +#else +withLessDetail sdoc = withPprStyle defaultUserStyle sdoc +#endif + +type VarPair = (Var, Var) +type VarPairSet = S.Set VarPair + +-- | This is a heuristic, which only works if both slices +-- have auxiliary variables in the right order. +-- (This is mostly to work-around the buggy CSE in GHC-8.0) +-- It also breaks if there is shadowing. +eqSlice :: Bool {- ^ ignore types -} -> Slice -> Slice -> Bool +eqSlice _ slice1 slice2 | null slice1 || null slice2 = null slice1 == null slice2 + -- Mostly defensive programming (slices should not be empty) +eqSlice it slice1 slice2 + = step (S.singleton (fst (last slice1), fst (last slice2))) S.empty + where + step :: VarPairSet -> VarPairSet -> Bool + step wanted done + | wanted `S.isSubsetOf` done + = True -- done + | (x,y) : _ <- S.toList (wanted `S.difference` done) + , (Just _, wanted') <- runState (runMaybeT (equate x y)) wanted + = step wanted' (S.insert (x,y) done) + | otherwise + = False + + + equate :: Var -> Var -> MaybeT (State VarPairSet) () + equate x y + | it + , Just e1 <- lookup x slice1 + , Just x' <- essentiallyVar e1 + = equated x' y + | it + , Just e2 <- lookup y slice2 + , Just y' <- essentiallyVar e2 + = equated x y' + | Just e1 <- lookup x slice1 + , Just e2 <- lookup y slice2 + = go (mkRnEnv2 emptyInScopeSet) e1 e2 + equate _ _ = mzero + + equated :: Var -> Var -> MaybeT (State VarPairSet) () + equated x y | x == y = return () + equated x y = lift $ modify (S.insert (x,y)) + + essentiallyVar :: CoreExpr -> Maybe Var + essentiallyVar (App e a) | isTyCoArg a = essentiallyVar e + essentiallyVar (Lam v e) | isTyCoVar v = essentiallyVar e + essentiallyVar (Cast e _) = essentiallyVar e + essentiallyVar (Var v) = Just v + essentiallyVar _ = Nothing + + go :: RnEnv2 -> CoreExpr -> CoreExpr -> MaybeT (State (S.Set (Var,Var))) () + go env (Var v1) (Var v2) | rnOccL env v1 == rnOccR env v2 = pure () + | otherwise = equated v1 v2 + go _ (Lit lit1) (Lit lit2) = guard $ lit1 == lit2 + go env (Type t1) (Type t2) = guard $ eqTypeX env t1 t2 + go env (Coercion co1) (Coercion co2) = guard $ eqCoercionX env co1 co2 + + go env (Cast e1 _) e2 | it = go env e1 e2 + go env e1 (Cast e2 _) | it = go env e1 e2 + go env (Cast e1 co1) (Cast e2 co2) = do guard (eqCoercionX env co1 co2) + go env e1 e2 + + go env (App e1 a) e2 | it, isTyCoArg a = go env e1 e2 + go env e1 (App e2 a) | it, isTyCoArg a = go env e1 e2 + go env (App f1 a1) (App f2 a2) = go env f1 f2 >> go env a1 a2 + go env (Tick n1 e1) (Tick n2 e2) = guard (go_tick env n1 n2) >> go env e1 e2 + + go env (Lam b e1) e2 | it, isTyCoVar b = go env e1 e2 + go env e1 (Lam b e2) | it, isTyCoVar b = go env e1 e2 + go env (Lam b1 e1) (Lam b2 e2) + = do guard (it || eqTypeX env (varType b1) (varType b2)) + -- False for Id/TyVar combination + go (rnBndr2 env b1 b2) e1 e2 + + go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) + = do go env r1 r2 -- No need to check binder types, since RHSs match + go (rnBndr2 env v1 v2) e1 e2 + + go env (Let (Rec ps1) e1) (Let (Rec ps2) e2) + = do guard $ equalLength ps1 ps2 + sequence_ $ zipWith (go env') rs1 rs2 + go env' e1 e2 + where + (bs1,rs1) = unzip ps1 + (bs2,rs2) = unzip ps2 + env' = rnBndrs2 env bs1 bs2 + + go env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) + | null a1 -- See Note [Empty case alternatives] in TrieMap + = do guard (null a2) + go env e1 e2 + guard (it || eqTypeX env t1 t2) + | otherwise + = do guard $ equalLength a1 a2 + go env e1 e2 + sequence_ $ zipWith (go_alt (rnBndr2 env b1 b2)) a1 a2 + + go _ _ _ = guard False + + ----------- + go_alt env (c1, bs1, e1) (c2, bs2, e2) + = guard (c1 == c2) >> go (rnBndrs2 env bs1 bs2) e1 e2 + + go_tick :: RnEnv2 -> Tickish Id -> Tickish Id -> Bool + go_tick env (Breakpoint lid lids) (Breakpoint rid rids) + = lid == rid && map (rnOccL env) lids == map (rnOccR env) rids + go_tick _ l r = l == r + + + +-- | Returns @True@ if the given core expression mentions no type constructor +-- anywhere that has the given name. +freeOfType :: Slice -> Name -> Maybe (Var, CoreExpr) +freeOfType slice tcN = allTyCons (\tc -> getName tc /= tcN) slice + +allTyCons :: (TyCon -> Bool) -> Slice -> Maybe (Var, CoreExpr) +allTyCons predicate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ] + where + goV v = goT (varType v) + + go (Var v) = goV v + go (Lit _ ) = True + go (App e a) = go e && go a + go (Lam b e) = goV b && go e + go (Let bind body) = all goB (flattenBinds [bind]) && go body + go (Case s b _ alts) = go s && goV b && all goA alts + go (Cast e _) = go e + go (Tick _ e) = go e + go (Type t) = (goT t) + go (Coercion _) = True + + goB (b, e) = goV b && go e + + goA (_,pats, e) = all goV pats && go e + + goT (TyVarTy _) = True + goT (AppTy t1 t2) = goT t1 && goT t2 + goT (TyConApp tc ts) = predicate tc && all goT ts + -- ↑ This is the crucial bit + goT (ForAllTy _ t) = goT t +#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) + goT (FunTy t1 t2) = goT t1 && goT t2 +#endif + goT (LitTy _) = True + goT (CastTy t _) = goT t + goT (CoercionTy _) = True +-- +-- | Returns @True@ if the given core expression mentions no term variable +-- anywhere that has the given name. +freeOfTerm :: Slice -> Name -> Maybe (Var, CoreExpr) +freeOfTerm slice needle = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ] + where + goV v | Var.varName v == needle = False + | otherwise = True + + go (Var v) = goV v + go (Lit _ ) = True + go (App e a) = go e && go a + go (Lam b e) = goV b && go e + go (Let bind body) = all goB (flattenBinds [bind]) && go body + go (Case s b _ alts) = go s && goV b && all goA alts + go (Cast e _) = go e + go (Tick _ e) = go e + go (Type _) = True + go (Coercion _) = True + + goB (b, e) = goV b && go e + + goA (ac,pats, e) = goAltCon ac && all goV pats && go e + + goAltCon (DataAlt dc) | dataConName dc == needle = False + | otherwise = True + goAltCon _ = True + + +-- | True if the given variable binding does not allocate, if called fully +-- satisfied. +-- +-- It currently does not look through function calls, which of course could +-- allocate. It should probably at least look through local function calls. +-- +-- The variable is important to know the arity of the function. +doesNotAllocate :: Slice -> Maybe (Var, CoreExpr) +doesNotAllocate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go (idArity v) e) ] + where + go _ (Var v) + | isDataConWorkId v, idArity v > 0 = False + go a (Var v) = (a >= idArity v) + go _ (Lit _ ) = True + go a (App e arg) | isTypeArg arg = go a e + go a (App e arg) = go (a+1) e && goArg arg + go a (Lam b e) | isTyVar b = go a e + go 0 (Lam _ _) = False + go a (Lam _ e) = go (a-1) e + go a (Let bind body) = all goB (flattenBinds [bind]) && go a body + go a (Case s _ _ alts) = go 0 s && all (goA a) alts + go a (Cast e _) = go a e + go a (Tick _ e) = go a e + go _ (Type _) = True + go _ (Coercion _) = True + + goArg e | exprIsTrivial e = go 0 e + | isUnliftedType (exprType e) = go 0 e + | otherwise = False + + goB (b, e) +#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0) + | isJoinId b = go (idArity b) e +#endif + -- Not sure when a local function definition allocates… + | isFunTy (idType b) = go (idArity b) e + | isUnliftedType (idType b) = go (idArity b) e + | otherwise = False + -- A let binding allocates if any variable is not a join point and not + -- unlifted + + goA a (_,_, e) = go a e + +doesNotContainTypeClasses :: Slice -> [Name] -> Maybe (Var, CoreExpr) +doesNotContainTypeClasses slice tcNs + = allTyCons (\tc -> not (isClassTyCon tc) || any (getName tc ==) tcNs) slice diff --git a/src/Test/Inspection/Plugin.hs b/src/Test/Inspection/Plugin.hs new file mode 100644 --- /dev/null +++ b/src/Test/Inspection/Plugin.hs @@ -0,0 +1,302 @@ +-- | See "Test.Inspection". +-- +{-# LANGUAGE CPP #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE LambdaCase #-} +module Test.Inspection.Plugin (plugin) where + +import Control.Monad +import System.Exit +import Data.Either +import Data.Maybe +import Data.Bifunctor +import Data.List +import qualified Data.Map.Strict as M +import qualified Language.Haskell.TH.Syntax as TH + +import GhcPlugins hiding (SrcLoc) +import Outputable + +import Test.Inspection (Obligation(..), Property(..), Result(..)) +import Test.Inspection.Core + +-- | The plugin. It supports the option @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to +-- ignore a failing build. +plugin :: Plugin +plugin = defaultPlugin { installCoreToDos = install } + +data UponFailure = AbortCompilation | KeepGoing deriving Eq + +data ResultTarget = PrintAndAbort | StoreAt Name + +install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] +install args passes = return $ passes ++ [pass] + where + pass = CoreDoPluginPass "Test.Inspection.Plugin" (proofPass upon_failure) + upon_failure | "keep-going" `elem` args = KeepGoing + | otherwise = AbortCompilation + + +extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)]) +extractObligations guts = (guts', obligations) + where + (anns_clean, obligations) = partitionMaybe findObligationAnn (mg_anns guts) + guts' = guts { mg_anns = anns_clean } + +findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation) +findObligationAnn (Annotation (ModuleTarget _) payload) + | Just obl <- fromSerialized deserializeWithData payload + = Just (PrintAndAbort, obl) +findObligationAnn (Annotation (NamedTarget n) payload) + | Just obl <- fromSerialized deserializeWithData payload + = Just (StoreAt n, obl) +findObligationAnn _ + = Nothing + +prettyObligation :: Module -> Obligation -> String -> String +prettyObligation mod (Obligation {..}) result = + maybe "" myPrettySrcLoc srcLoc ++ ": " ++ name ++ " " ++ result + where + name = case testName of + Just n -> n + Nothing -> prettyProperty mod target property + +prettyProperty :: Module -> TH.Name -> Property -> String +prettyProperty mod target (EqualTo n2 False) = showTHName mod target ++ " === " ++ showTHName mod n2 +prettyProperty mod target (EqualTo n2 True) = showTHName mod target ++ " ==- " ++ showTHName mod n2 +prettyProperty mod target (NoTypes [t]) = showTHName mod target ++ " `hasNoType` " ++ showTHName mod t +prettyProperty mod target (NoTypes ts) = showTHName mod target ++ " mentions none of " ++ intercalate ", " (map (showTHName mod) ts) +prettyProperty mod target NoAllocation = showTHName mod target ++ " does not allocate" +prettyProperty mod target (NoTypeClasses []) = showTHName mod target ++ " does not contain dictionary values" +prettyProperty mod target (NoTypeClasses ts) = showTHName mod target ++ " does not contain dictionary values except of " ++ intercalate ", " (map (showTHName mod) ts) +prettyProperty mod target (NoUseOf ns) = showTHName mod target ++ " uses none of " ++ intercalate ", " (map (showTHName mod) ns) + +-- | Like show, but omit the module name if it is he current module +showTHName :: Module -> TH.Name -> String +showTHName mod (TH.Name occ (TH.NameQ m)) + | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ +showTHName mod (TH.Name occ (TH.NameG _ _ m)) + | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ +showTHName _ n = show n + +data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult + deriving (Enum, Eq, Ord, Bounded) +type Stats = M.Map Stat Int + +type Updates = [(Name, Result)] + +tick :: Stat -> Stats +tick s = M.singleton s 1 + +checkObligation :: ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats) +checkObligation guts (reportTarget, obl) = do + + res <- checkProperty guts (target obl) (property obl) + case reportTarget of + PrintAndAbort -> do + category <- case (res, expectFail obl) of + -- Property holds + (Nothing, False) -> do + putMsgS $ prettyObligation (mg_module guts) obl expSuccess + return ExpSuccess + (Nothing, True) -> do + putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess + return UnexpSuccess + -- Property does not hold + (Just reportDoc, False) -> do + putMsgS $ prettyObligation (mg_module guts) obl unexpFailure + putMsg $ reportDoc + return UnexpFailure + (Just _, True) -> do + putMsgS $ prettyObligation (mg_module guts) obl expFailure + return ExpFailure + return ([], tick category) + StoreAt name -> do + dflags <- getDynFlags + let result = case res of + Nothing -> Success $ showSDoc dflags $ + text (prettyObligation (mg_module guts) obl expSuccess) + Just reportMsg -> Failure $ showSDoc dflags $ + text (prettyObligation (mg_module guts) obl unexpFailure) $$ + reportMsg + pure ([(name, result)], tick StoredResult) + + where + expSuccess = "passed." + unexpSuccess = "passed unexpectedly!" + unexpFailure = "failed:" + expFailure = "failed expectedly." + + +type CheckResult = Maybe SDoc + +lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr) +lookupNameInGuts guts n = listToMaybe + [ (v,e) + | (v,e) <- flattenBinds (mg_binds guts) + , getName v == n + ] + +updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts +updateNameInGuts n expr guts = + guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) } + +updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind +updateNameInGut n e (NonRec v _) | getName v == n = NonRec v e +updateNameInGut _ _ bind = bind + +checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult +checkProperty guts thn1 (EqualTo thn2 ignore_types) = do + n1 <- fromTHName thn1 + n2 <- fromTHName thn2 + + let p1 = lookupNameInGuts guts n1 + let p2 = lookupNameInGuts guts n2 + + if | n1 == n2 + -> return Nothing + -- Ok if one points to another + | Just (_, Var other) <- p1, getName other == n2 + -> return Nothing + | Just (_, Var other) <- p2, getName other == n1 + -> return Nothing + | Just (v1, _) <- p1 + , Just (v2, _) <- p2 + , let slice1 = slice binds v1 + , let slice2 = slice binds v2 + -> if eqSlice ignore_types slice1 slice2 + -- OK if they have the same expression + then return Nothing + -- Not ok if the expression differ + else pure . Just $ pprSliceDifference slice1 slice2 + -- Not ok if both names are bound externally + | Nothing <- p1 + , Nothing <- p2 + -> pure . Just $ ppr n1 <+> text " and " <+> ppr n2 <+> + text "are different external names" + | Nothing <- p1 + -> pure . Just $ ppr n1 <+> text "is an external name" + | Nothing <- p2 + -> pure . Just $ ppr n2 <+> text "is an external name" + where + binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoUseOf thns) = do + n <- fromTHName thn + ns <- mapM fromTHName thns + case lookupNameInGuts guts n of + Nothing -> pure . Just $ ppr n <+> text "is not a local name" + Just (v, _) -> case msum $ map (freeOfTerm (slice binds v)) ns of + Just _ -> pure . Just $ pprSlice (slice binds v) + Nothing -> pure Nothing + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoTypes thts) = do + n <- fromTHName thn + ts <- mapM fromTHName thts + case lookupNameInGuts guts n of + Nothing -> pure . Just $ ppr n <+> text "is not a local name" + Just (v, _) -> case msum $ map (freeOfType (slice binds v)) ts of + Just _ -> pure . Just $ pprSlice (slice binds v) + Nothing -> pure Nothing + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn NoAllocation = do + n <- fromTHName thn + case lookupNameInGuts guts n of + Nothing -> pure . Just $ ppr n <+> text "is not a local name" + Just (v, _) -> case doesNotAllocate (slice binds v) of + Just (v',e') -> pure . Just $ nest 4 (ppr v' <+> text "=" <+> ppr e') + Nothing -> pure Nothing + where binds = flattenBinds (mg_binds guts) + +checkProperty guts thn (NoTypeClasses thts) = do + n <- fromTHName thn + ts <- mapM fromTHName thts + case lookupNameInGuts guts n of + Nothing -> pure . Just $ ppr n <+> text "is not a local name" + Just (v, _) -> case doesNotContainTypeClasses (slice binds v) ts of + Just (v',e') -> pure . Just $ nest 4 (ppr v' <+> text "=" <+> ppr e') + Nothing -> pure Nothing + where binds = flattenBinds (mg_binds guts) + + +fromTHName :: TH.Name -> CoreM Name +fromTHName thn = thNameToGhcName thn >>= \case + Nothing -> do + errorMsg $ text "Could not resolve TH name" <+> text (show thn) + liftIO $ exitFailure -- kill the compiler. Is there a nicer way? + Just n -> return n + +storeResults :: Updates -> ModGuts -> CoreM ModGuts +storeResults = flip (foldM (flip (uncurry go))) + where + go :: Name -> Result -> ModGuts -> CoreM ModGuts + go name res guts = do + e <- resultToExpr res + pure $ updateNameInGuts name e guts + +dcExpr :: TH.Name -> CoreM CoreExpr +dcExpr thn = do + name <- fromTHName thn + dc <- lookupDataCon name + pure $ Var (dataConWrapId dc) + +resultToExpr :: Result -> CoreM CoreExpr +resultToExpr (Success s) = App <$> dcExpr 'Success <*> mkStringExpr s +resultToExpr (Failure s) = App <$> dcExpr 'Failure <*> mkStringExpr s + +proofPass :: UponFailure -> ModGuts -> CoreM ModGuts +proofPass upon_failure guts = do + dflags <- getDynFlags + when (optLevel dflags < 1) $ + warnMsg $ fsep $ map text $ words "Test.Inspection: Compilation without -O detected. Expect optimizations to fail." + + let (guts', obligations) = extractObligations guts + (toStore, stats) <- (concat `bimap` M.unionsWith (+)) . unzip <$> + mapM (checkObligation guts') obligations + let n = sum stats :: Int + + guts'' <- storeResults toStore guts' + + let q :: Stat -> Int + q s = fromMaybe 0 $ M.lookup s stats + + let summary_message = nest 2 $ + vcat [ nest 2 (desc s) Outputable.<> colon <+> ppr (q s) + | s <- [minBound..maxBound], q s > 0 ] + + -- Only print a message if there are some compile-time results to report + unless (q StoredResult == n) $ do + if q ExpSuccess + q ExpFailure + q StoredResult == n + then putMsg $ text "inspection testing successful" $$ summary_message + else case upon_failure of + AbortCompilation -> do + errorMsg $ text "inspection testing unsuccessful" $$ summary_message + liftIO $ exitFailure -- kill the compiler. Is there a nicer way? + KeepGoing -> do + warnMsg $ text "inspection testing unsuccessful" $$ summary_message + + return guts'' + + +desc :: Stat -> SDoc +desc ExpSuccess = text " expected successes" +desc UnexpSuccess = text "unexpected successes" +desc ExpFailure = text " expected failures" +desc UnexpFailure = text " unexpected failures" +desc StoredResult = text " results stored" + +partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b]) +partitionMaybe f = partitionEithers . map (\x -> maybe (Left x) Right (f x)) + +-- | like prettySrcLoc, but omits the module name +myPrettySrcLoc :: TH.Loc -> String +myPrettySrcLoc TH.Loc {..} + = foldr (++) "" + [ loc_filename, ":" + , show (fst loc_start), ":" + , show (snd loc_start) + ]