inspection-testing 0.6 → 0.6.1
raw patch · 4 files changed
+160/−131 lines, 4 files
Files
- ChangeLog.md +4/−0
- inspection-testing.cabal +1/−1
- src/Test/Inspection/Core.hs +151/−126
- src/Test/Inspection/Plugin.hs +4/−4
ChangeLog.md view
@@ -1,5 +1,9 @@ # Revision history for inspection-testing +## 0.6.1 -- 2025-06-11++* Improve presentation of term inequalities (thanks Oleg Grenrus)+ ## 0.6 -- 2025-01-01 * Support GHC 9.10.1 (thanks Andre Van Der Merwe)
inspection-testing.cabal view
@@ -1,5 +1,5 @@ name: inspection-testing-version: 0.6+version: 0.6.1 synopsis: GHC plugin to do inspection testing description: Some carefully crafted libraries make promises to their users beyond functionality and performance.
src/Test/Inspection/Core.hs view
@@ -1,11 +1,12 @@ -- | This module implements some analyses of Core expressions necessary for -- "Test.Inspection". Normally, users of this package can ignore this module.-{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf #-}+{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, MultiWayIf, ViewPatterns #-} module Test.Inspection.Core ( slice , pprSlice , pprSliceDifference , eqSlice+ , eqSlice' , freeOfType , freeOfTerm , doesNotAllocate@@ -61,20 +62,26 @@ #endif import qualified Data.Set as S-import Control.Monad (guard, unless, mzero)-import Control.Monad.Trans.Class (lift)-import Control.Monad.State.Strict (StateT, runStateT, execState, modify, modify', put, get, gets)+import Control.Monad (unless)+import Control.Monad.State.Strict (execState, modify', gets) import Data.List (nub, intercalate)-import Data.Maybe+import Data.Maybe (listToMaybe, fromJust)+import Data.Either (isRight) import Test.Inspection (Equivalence (..)) -- Uncomment to enable debug traces--- import Debug.Trace+-- #define DEBUG_TRACE +#ifdef DEBUG_TRACE+import Debug.Trace+ tracePut :: Monad m => Int -> String -> String -> m ()--- tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg+tracePut lv name msg = traceM $ replicate lv ' ' ++ name ++ ": " ++ msg+#else+tracePut :: Monad m => Int -> String -> String -> m () tracePut _ _ _ = return ()+#endif #if !MIN_VERSION_ghc(9,2,0) pattern Alt :: a -> b -> c -> (a, b, c)@@ -99,7 +106,7 @@ goV v | v `S.member` local = do seen <- gets (v `S.member`) unless seen $ do- modify (S.insert v)+ modify' (S.insert v) let e = fromJust $ lookup v binds go e | otherwise = return ()@@ -180,21 +187,22 @@ 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 :: Equivalence -> Slice -> Slice -> Bool-eqSlice _ [] [] = True-eqSlice _ _ [] = False-eqSlice _ [] _ = False+eqSlice eqv l r = isRight (eqSlice' eqv l r)++-- | Like 'eqSlice' but also returns an explanation of inequality.+eqSlice' :: Equivalence -> Slice -> Slice -> Either SDoc ()+eqSlice' _ [] [] = Right ()+eqSlice' _ ((v,_) : _) [] = Left $ ppr v+eqSlice' _ [] ((v,_) : _) = Left $ ppr v -- Mostly defensive programming (slices should not be empty)-eqSlice eqv slice1@((head1, _) : _) slice2@((head2, _) : _)- -- slices are equal if there exist any result with no "unification" obligations left.- = any (S.null . snd) results+eqSlice' eqv slice1@((head1, def1) : _) slice2@((head2, def2) : _) = do+ let env = mkRnEnv2 emptyInScopeSet+ goSliceVars [] 0 env head1 def1 head2 def2 where -- ignore types and hpc ticks it :: Bool@@ -210,58 +218,27 @@ IgnoreTypesAndTicksEquiv -> False UnorderedLetsEquiv -> True - -- results. If there are no pairs to be equated, all is fine.- results :: [((), VarPairSet)]- results = runStateT (loop' (mkRnEnv2 emptyInScopeSet) S.empty head1 head2) S.empty-- -- while there are obligations left, try to equate them.- loop :: RnEnv2 -> VarPairSet -> StateT VarPairSet [] ()- loop env done = do- vars <- get- case S.minView vars of- Nothing -> return () -- nothing to do, done.- Just ((x, y), vars') -> do- put vars'- if (x, y) `S.member` done- then loop env done- else loop' env done x y-- loop' :: RnEnv2 -> VarPairSet -> Var -> Var -> StateT VarPairSet [] ()- loop' env done x y = do- tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y)- tracePut 0 "DONESET" (showVarPairSet done)+ goSliceVars :: [SDoc] -> Int -> RnEnv2 -> Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc ()+ goSliceVars ctx lv env x e1 y e2 = do+ tracePut lv "SLICEVAR" (varToString x ++ " =?= " ++ varToString y) -- if x or y expressions are essentially a variable x' or y' respectively -- add an obligation to check x' = y (or x = y').- if | Just e1 <- lookup x slice1- , Just x' <- essentiallyVar e1- , x' `elem` map fst slice1- -> do modify' (S.insert (x', y))- loop env done+ if | Just x' <- essentiallyVar e1+ , Just e1' <- lookup x' slice1+ -> goSliceVars ctx lv env x' e1' y e2 - | Just e2 <- lookup y slice2- , Just y' <- essentiallyVar e2- , y' `elem` map fst slice2- -> do modify' (S.insert (x, y'))- loop env done+ | Just y' <- essentiallyVar e2+ , Just e2' <- lookup y' slice2+ -> goSliceVars ctx lv env x e1 y' e2' -- otherwise if neither x and y expressions are variables -- 1. compare the expressions (already assuming that x and y are equal) -- 2. comparison may create new obligations, loop.- | Just e1 <- lookup x slice1- , Just e2 <- lookup y slice2- -> do- let env' = rnBndr2 env x y- done' = S.insert (x, y) done-- go 0 env' e1 e2- loop env' done'-- -- and finally, if x or y are not in the slice, we abort. | otherwise -> do- tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y ++ " NOT IN SLICES")- mzero+ let env' = rnBndr2 env x y+ go ctx lv env' e1 e2 essentiallyVar :: CoreExpr -> Maybe Var essentiallyVar (App e a) | it, isTyCoArg a = essentiallyVar e@@ -275,93 +252,122 @@ essentiallyVar (Tick SourceNote{} e) = essentiallyVar e essentiallyVar _ = Nothing - go :: Int -> RnEnv2 -> CoreExpr -> CoreExpr -> StateT VarPairSet [] ()- go lv env (Var v1) (Var v2) = do+ -- report inequality+ inequality :: [SDoc] -> SDoc -> Either SDoc a+ inequality [] err = Left err+ inequality ctx err = Left $ err $$ hang (text "in") 2 (vcat ctx)++ go :: [SDoc] -> Int -> RnEnv2 -> CoreExpr -> CoreExpr -> Either SDoc ()+ go ctx lv env (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do if | v1 == v2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") return () | rnOccL env v1 == rnOccR env v2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV") return ()- | otherwise -> do+ | Just e1 <- lookup v1 slice1+ , Just e2 <- lookup v2 slice2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " OBLIGATION")- modify (S.insert (v1, v2))+ goSliceVars ctx lv env v1 e1 v2 e2+ | otherwise -> do+ inequality ctx $ hsep [ text "inequal variables", ppr v1, text "and", ppr v2 ] - go lv _ (Lit lit1) (Lit lit2) = do+ go ctx lv _ (Lit lit1) (Lit lit2) = do tracePut lv "LIT" "???" -- no Show for Literal :(- guard $ lit1 == lit2+ unless (lit1 == lit2) $ inequality ctx $ sep [ text "inequal literals", ppr lit1, text "and", ppr lit2 ] - go _ env (Type t1) (Type t2) = guard $ eqTypeX env t1 t2- go _ env (Coercion co1) (Coercion co2) = guard $ eqCoercionX env co1 co2+ go ctx _ env (Type t1) (Type t2) =+ goTypes ctx env t1 t2 - go lv env (Cast e1 _) e2 | it = go lv env e1 e2- go lv env e1 (Cast e2 _) | it = go lv env e1 e2+ go ctx _ env (Coercion co1) (Coercion co2) =+ goCoercions ctx env co1 co2++ go ctx lv env (Cast e1 _) e2 | it = go ctx lv env e1 e2+ go ctx lv env e1 (Cast e2 _) | it = go ctx lv env e1 e2 #if MIN_VERSION_ghc(9,0,0)- go lv env (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go lv env e1 e2- go lv env e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go lv env e1 e2+ go ctx lv env (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2+ go ctx lv env e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2 #endif- go lv env (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do- guard (eqCoercionX env co1 co2)- go lv env e1 e2+ go ctx lv env (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do+ goCoercions ctx env co1 co2+ go ctx lv env e1 e2 - go lv env (App e1 a) e2 | it, isTyCoArg a = go lv env e1 e2- go lv env e1 (App e2 a) | it, isTyCoArg a = go lv env e1 e2- go lv env (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do- go lv env f1 f2- go lv env a1 a2- go lv env (Tick HpcTick{} e1) e2 | it = go lv env e1 e2- go lv env e1 (Tick HpcTick{} e2) | it = go lv env e1 e2- go lv env (Tick SourceNote{} e1) e2 = go lv env e1 e2- go lv env e1 (Tick SourceNote{} e2) = go lv env e1 e2- go lv env (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do- guard (go_tick env n1 n2)- go lv env e1 e2+ go ctx lv env (App e1 a) e2 | it, isTyCoArg a = go ctx lv env e1 e2+ go ctx lv env e1 (App e2 a) | it, isTyCoArg a = go ctx lv env e1 e2+ go ctx lv env (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do+ go ctx lv env f1 f2+ go ctx lv env a1 a2+ go ctx lv env (Tick HpcTick{} e1) e2 | it = go ctx lv env e1 e2+ go ctx lv env e1 (Tick HpcTick{} e2) | it = go ctx lv env e1 e2+ go ctx lv env (Tick SourceNote{} e1) e2 = go ctx lv env e1 e2+ go ctx lv env e1 (Tick SourceNote{} e2) = go ctx lv env e1 e2+ go ctx lv env (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do+ unless (go_tick env n1 n2) $ inequality ctx $ text "inequal ticks"+ go ctx lv env e1 e2 - go lv env (Lam b e1) e2 | it, isTyCoVar b = go lv env e1 e2- go lv env e1 (Lam b e2) | it, isTyCoVar b = go lv env e1 e2- go lv env (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do- guard (it || eqTypeX env (varType b1) (varType b2))- go lv (rnBndr2 env b1 b2) e1 e2+ go ctx lv env (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env e1 e2+ go ctx lv env e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env e1 e2+ go ctx lv env (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do+ -- guard (it || eqTypeX env (varType b1) (varType b2)) -- TODO+ go ctx lv (rnBndr2 env b1 b2) e1 e2 - go lv env e1@(Let _ _) e2@(Let _ _)+ go ctx lv env e1@(Let _ _) e2@(Let _ _) | ul , (ps1, e1') <- peelLets e1 , (ps2, e2') <- peelLets e2 = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do- guard $ equalLength ps1 ps2- env' <- goBinds lv env ps1 ps2- go lv env' e1' e2'+ let ctx' = text "let bindings:" <+> pprVars ps1 <+> pprVars ps2 : ctx+ unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in let"+ env' <- goBinds ctx' lv env ps1 ps2 - go lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2)- = do go lv env r1 r2 -- No need to check binder types, since RHSs match- go lv (rnBndr2 env v1 v2) e1 e2+ go ctx lv env' e1' e2' - go lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2)- = do guard $ equalLength ps1 ps2- sequence_ $ zipWith (go lv env') rs1 rs2- go lv env' e1 e2+ go ctx lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2)+ = do go ctx lv env r1 r2 -- No need to check binder types, since RHSs match+ go ctx lv (rnBndr2 env v1 v2) e1 e2++ go ctx lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2)+ = do+ unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in recursive let"+ sequence_ $ zipWith (go ctx lv env') rs1 rs2+ go ctx lv env' e1 e2 where+ bs1, bs2 :: [CoreBndr]+ rs1, rs2 :: [CoreExpr]+ (bs1,rs1) = unzip ps1 (bs2,rs2) = unzip ps2 env' = rnBndrs2 env bs1 bs2 - go lv env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2)+ go ctx lv 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 lv env e1 e2- guard (it || eqTypeX env t1 t2)+ , null a2+ = do+ go ctx lv env e1 e2+ unless it $ goTypes ctx env t1 t2+ | otherwise- = do guard $ equalLength a1 a2- go lv env e1 e2- sequence_ $ zipWith (go_alt lv (rnBndr2 env b1 b2)) a1 a2+ = do unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case"+ go ctx lv env e1 e2+ sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2)) a1 a2 - go lv _ e1 e2 = do+ go ctx lv _ e1 e2 = do tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2)- mzero+ inequality ctx $ sep [ text "inequal terms:", ppr e1, text "and", ppr e2] + goCoercions ctx env t1 t2+ | eqCoercionX env t1 t2 = return ()+ | otherwise = inequality ctx $ sep [ text "inequal coercions:", ppr t1, text "and", ppr t2 ]++ goTypes ctx env t1 t2+ | eqTypeX env t1 t2 = return ()+ | otherwise = inequality ctx $ sep [ text "inequal types:", ppr t1, text "and", ppr t2 ]+ ------------ go_alt lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2)- = guard (c1 == c2) >> go lv (rnBndrs2 env bs1 bs2) e1 e2+ go_alt :: [SDoc] -> Int -> RnEnv2 -> CoreAlt -> CoreAlt -> Either SDoc ()+ go_alt ctx lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2)+ = do unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ]+ go ctx lv (rnBndrs2 env bs1 bs2) e1 e2 go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool go_tick env Breakpoint{ breakpointId = lid, breakpointFVs = lids } Breakpoint{ breakpointId = rid, breakpointFVs = rids }@@ -372,21 +378,40 @@ peelLets (Let (Rec bs) e) = let (xs, e') = peelLets e in (bs ++ xs, e') peelLets e = ([], e) - goBinds :: Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> StateT VarPairSet [] RnEnv2- goBinds _ env [] [] = return env- goBinds _ _ [] (_:_) = mzero- goBinds lv env ((v1,b1):xs) ys' = do+ goBinds :: [SDoc] -> Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Either SDoc RnEnv2+ goBinds _ _ env [] [] = return env+ goBinds ctx _ _ [] (_:_) = inequality ctx $ text "goBinds: missing binding"+ goBinds ctx _ _ (_:_) [] = inequality ctx $ text "goBinds: missing binding"+ goBinds ctx lv env [(v1,b1)] [(v2, b2)] = do+ -- special case of singleton let bindings:+ -- there is no choice, so we can save ourselves transforming sub-errors.+ go ctx lv env b1 b2+ return (rnBndr2 env v1 v2)++ goBinds ctx lv env ((v1,b1):xs) ys' = findRight (v1 : map fst xs) (map fst ys') $ do -- select a binding- ((v2,b2), ys) <- lift (choices ys')+ ((v2,b2), ys) <- choices ys'+ return $ do+ let ctx' = hsep [text "trying", ppr v1, text "=", ppr v2] : ctx+ traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv ->+ go ctx' lv env b1 b2 - traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv ->- go lv env b1 b2+ -- continue with the rest of bindings, adding a pair as matching one.+ goBinds ctx' lv (rnBndr2 env v1 v2) xs ys - -- if match succeeds, delete it from the obligations- modify (S.delete (v1, v2))- -- continue with the rest of bindings, adding a pair as matching one.- goBinds lv (rnBndr2 env v1 v2) xs ys+--TODO: rename+findRight :: [Var] -> [Var] -> [Either SDoc a] -> Either SDoc a+findRight ls rs = go []+ where+ go errs [] = Left $ hang (text "Cannot align let bindings:" <+> pprVars ls <+> pprVars rs) 2 (vcatBullet errs)+ go _ (x@(Right _) : _) = x+ go errs (Left err : xs) = go (err : errs) xs + pprVars = braces . hsep . map ppr++vcatBullet :: [SDoc] -> SDoc+vcatBullet = vcat . map (text "*" <+>)+ #if !MIN_VERSION_ghc(9,9,0) && MIN_VERSION_ghc(9,0,0) isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr isUnsafeEqualityCase scrut _bndr [Alt _ _ rhs]@@ -407,8 +432,8 @@ showVars :: [(Var, a)] -> String showVars xs = intercalate ", " [ varToString x | (x, _) <- xs ] -showVarPairSet :: VarPairSet -> String-showVarPairSet xs = intercalate ", " [ varToString x ++ " ~ " ++ varToString y | (x, y) <- S.toList xs ]+pprVars :: [(Var, a)] -> SDoc+pprVars = braces . hsep . map (ppr . fst) varToString :: Var -> String varToString v = occNameString (occName (tyVarName v)) ++ "_" ++ show (getUnique v)
src/Test/Inspection/Plugin.hs view
@@ -229,11 +229,11 @@ , 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 pure ResSuccess+ -> case eqSlice' ignore_types slice1 slice2 of+ -- OK if they have the same expression+ Right _ -> pure ResSuccess -- Not ok if the expression differ- else pure . ResFailure $ pprSliceDifference slice1 slice2+ Left err -> pure . ResFailure $ err $$ pprSliceDifference slice1 slice2 -- Not ok if both names are bound externally | Nothing <- p1 , Nothing <- p2