packages feed

inspection-testing 0.4 → 0.4.1

raw patch · 10 files changed

+921/−826 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Test.Inspection: NoUseOf :: [Name] -> Property
+ Test.Inspection: doesNotUse :: Name -> Name -> Obligation
+ Test.Inspection.Core: freeOfTerm :: Slice -> Name -> Maybe (Var, CoreExpr)

Files

ChangeLog.md view
@@ -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
README.md view
@@ -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.
− Test/Inspection.hs 
@@ -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--@-{&#45;\# LANGUAGE TemplateHaskell \#&#45;}-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:-@-{&#45;\# LANGUAGE TemplateHaskell \#&#45;}-@--}---- 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-        -- @{&#45;\# LANGUAGE TemplateHaskell \#&#45;}@.-    , 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
− Test/Inspection/Core.hs 
@@ -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
− Test/Inspection/Plugin.hs 
@@ -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)-      ]
+ examples/DoesNotUse.hs view
@@ -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 ()
inspection-testing.cabal view
@@ -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
+ src/Test/Inspection.hs view
@@ -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++@+{&#45;\# LANGUAGE TemplateHaskell \#&#45;}+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:+@+{&#45;\# LANGUAGE TemplateHaskell \#&#45;}+@+-}++-- 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+        -- @{&#45;\# LANGUAGE TemplateHaskell \#&#45;}@.+    , 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
+ src/Test/Inspection/Core.hs view
@@ -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
+ src/Test/Inspection/Plugin.hs view
@@ -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)+      ]