diff --git a/src/Reopt/TypeInference/Constraints.hs b/src/Reopt/TypeInference/Constraints.hs index 1e22f90e..92354d9b 100644 --- a/src/Reopt/TypeInference/Constraints.hs +++ b/src/Reopt/TypeInference/Constraints.hs @@ -549,17 +549,20 @@ trivialSubC ctx s t = subtype' resolveVar resolveVar s t -- | @absurdSubC s t ctx@ returns @True@ if `s <: t` is an absurd constraint given `ctx`. -- N.B., this is intended to be a conservative check (i.e., sound but incomplete). absurdSubC :: Context -> Ty -> Ty -> Bool -absurdSubC ctx s t = not $ subtype' resolveL resolveR s t - where resolveL x = findLowerBound x (ctxVarBoundsMap ctx) - resolveR x = findUpperBound x (ctxVarBoundsMap ctx) +absurdSubC ctx s t = traceContextualBinOp "absurdSubC" ctx s t $ + not $ subtype' resolveL resolveR s t + where resolveL x = lowerConcretization (VarTy x) ctx + resolveR x = upperConcretization (VarTy x) ctx -- | Is this equality constraint trivial in the current context? trivialEqC :: Context -> Ty -> Ty -> Bool -trivialEqC ctx s t = trivialSubC ctx s t && trivialSubC ctx t s +trivialEqC ctx s t = traceContextualBinOp "trivialEqC" ctx s t $ + trivialSubC ctx s t && trivialSubC ctx t s -- | @absurdEqC s t ctx@ returns @True@ if `s = t` is an absurd constraint given `ctx`. absurdEqC :: Context -> Ty -> Ty -> Bool -absurdEqC ctx s t = (absurdSubC ctx s t) || (absurdSubC ctx t s) +absurdEqC ctx s t = traceContextualBinOp "absurdEqC" ctx s t $ + (absurdSubC ctx s t) || (absurdSubC ctx t s) -- | @traceContext description ctx ctx'@ reports how the context changed via @trace@. traceContext :: PP.Doc () -> Context -> Context -> Context @@ -575,6 +578,23 @@ traceCOpContext :: PP.Doc () -> TyConstraint -> Context -> Context -> Context traceCOpContext fnNm c ctx ctx' = traceContext (fnNm<>"(" <> (PP.pretty $ c)<> ")") ctx ctx' +traceContextualUnOp :: (PP.Pretty a, PP.Pretty b) => PP.Doc () -> Context -> a -> b -> b +traceContextualUnOp opName ctx arg res = + if not traceUnification then res else + let msg = PP.vsep [ PP.hsep [">>> ", opName , "(" , PP.pretty arg , ") in context"] + , PP.indent 4 $ PP.pretty ctx + , PP.hsep ["<<< ", PP.pretty res]] + in trace (show msg) res + +traceContextualBinOp :: (PP.Pretty a, PP.Pretty b, PP.Pretty c) => PP.Doc () -> Context -> a -> b -> c -> c +traceContextualBinOp opName ctx arg1 arg2 res = + if not traceUnification then res else + let msg = PP.vsep [ PP.hsep [">>> ", opName , "(" , PP.pretty arg1 , ", ", PP.pretty arg2 , ") in context"] + , PP.indent 4 $ PP.pretty ctx + , PP.hsep ["<<< ", PP.pretty res]] + in trace (show msg) res + + -- | @solveEqC (s,t) ctx@ updates @ctx@ with the equality -- `s == t`. Cf. TIE Algorithm 1. If @Nothing@ is returned, the equality -- failed the occurs check. FIXME should we have a `decomposeEqC` similar to `decomposeSubC`? @@ -754,32 +774,51 @@ finalizeBounds ctx vars = fsSolutions $ execState solveVars (FinalizerState vars newtype TyUnificationError = TyUnificationError String processAtomicConstraints :: Context -> Context -processAtomicConstraints ctx = traceContext "processAtomicConstraints" ctx $ - case dequeueEqC ctx of - Just (ctx', c) -> processAtomicConstraints $ solveEqC ctx' c - Nothing -> - case dequeueSubC ctx of - Just (ctx', c) -> processAtomicConstraints $ solveSubC ctx' c - Nothing -> ctx +processAtomicConstraints ctx0 = traceContext "processAtomicConstraints" ctx0 $ go ctx0 + where go :: Context -> Context + go ctx = + case dequeueEqC ctx of + Just (ctx', c) -> processAtomicConstraints $ solveEqC ctx' c + Nothing -> + case dequeueSubC ctx of + Just (ctx', c) -> processAtomicConstraints $ solveSubC ctx' c + Nothing -> ctx -- | Reduce a constraint given the context. reduceC :: Context -> TyConstraint -> TyConstraint -reduceC ctx = go +reduceC ctx c0 = traceContextualUnOp "reduceC" ctx c0 $ go c0 where + sub t = substEqs t ctx go :: TyConstraint -> TyConstraint go = \case TopC -> TopC BotC -> BotC - c@(EqC s t) -> if absurdEqC ctx s t then BotC - else if trivialEqC ctx s t then TopC - else c - c@(SubC s t) -> if absurdSubC ctx s t then BotC - else if trivialEqC ctx s t then TopC - else c + c@(EqC rawS rawT) -> + let s = sub rawS + t = sub rawT + in if absurdEqC ctx s t then BotC + else if trivialEqC ctx s t then TopC + else c + c@(SubC rawS rawT) -> + let s = sub rawS + t = sub rawT + in if absurdSubC ctx s t then BotC + else if trivialEqC ctx s t then TopC + else c OrC c1 c2 cs -> orC $ map go $ c1:c2:cs AndC c1 c2 cs -> andC $ map go $ c1:c2:cs +-- | `absurdC ctx c` returns @True@ if `c` is absurd/unsatisfiable in context +-- `ctx`, otherwise @False@ is returned. N.B., this is intended to be a sound +-- and conservative check in the sense that @True@ always implies the constraint +-- is absurd, but @False@ really just means we were unable to prove it was +-- unsatisfiable, which could be because it _is_ satisfiable, or because +-- we need some additional logic to be more complete. +absurdC :: Context -> TyConstraint -> Bool +absurdC ctx c = reduceC ctx c == BotC + + -- | Attempt to reduce and eliminate disjunctions in the given context. Any -- resulting non-disjuncts are added to their respective field in the context. reduceDisjuncts :: Context -> Context diff --git a/tests/Main.hs b/tests/Main.hs index ed7a5a99..43de64c9 100644 --- a/tests/Main.hs +++ b/tests/Main.hs @@ -11,7 +11,8 @@ main = do x64AsmTests <- namesMatching "tests/x64/*.exe" T.defaultMain $ T.testGroup "ReoptTests" [ - TC.constraintTests, + TC.absurdTests, + TC.tyEnvTests, T.reoptTests x64AsmTests ] diff --git a/tests/TyConstraintTests.hs b/tests/TyConstraintTests.hs index 7df5b34e..ec32f052 100644 --- a/tests/TyConstraintTests.hs +++ b/tests/TyConstraintTests.hs @@ -4,7 +4,8 @@ {-# LANGUAGE RankNTypes #-} module TyConstraintTests - ( constraintTests, + ( absurdTests, + tyEnvTests, ) where @@ -25,10 +26,13 @@ import Reopt.TypeInference.Constraints andC, ptrTy, int32Ty, - int64Ty) + int64Ty, + initContext, + reduceContext, + absurdC) -x0,x1,x2,x3 :: TyVar -x0Ty,x1Ty,x2Ty,x3Ty :: Ty +x0,x1,x2,x3,x4 :: TyVar +x0Ty,x1Ty,x2Ty,x3Ty,x4Ty :: Ty x0 = TyVar 0 x0Ty = VarTy x0 x1 = TyVar 1 @@ -37,45 +41,129 @@ x2 = TyVar 2 x2Ty = VarTy x2 x3 = TyVar 3 x3Ty = VarTy x3 +x4 = TyVar 4 +x4Ty = VarTy x4 + +---------------------------------------------------------------------------- +-- Constraint Satisfiability/Absurdity tests + +-- | `mkAbsurdTests testName ctxCs tgtCs` constructs a context from `ctxCs` and +-- checks that each constraints in `tgtCs` is either absurd or not (depending on +-- the accompanying Bool). +mkAbsurdTests :: String -> [TyConstraint] -> [(TyConstraint, Bool)] -> T.TestTree +mkAbsurdTests name contextConstraints unsatisfiableConstraints = + T.testGroup name $ map singleTest unsatisfiableConstraints + where ctx = reduceContext $ initContext contextConstraints + singleTest (c, expected) = + T.testCase (show $ (PP.pretty c)) + $ T.assertEqual "absurdC" + expected + (absurdC ctx c) + +absurdTests :: T.TestTree +absurdTests = T.testGroup "Constraint Satisfiability Tests" + [ mkAbsurdTests + "simple equality constraints" + [] + [(EqC int32Ty int64Ty, True), + (EqC (ptrTy 64 int32Ty) (ptrTy 64 int64Ty), True), + (EqC int64Ty int64Ty, False), + (EqC (ptrTy 64 int64Ty) (ptrTy 64 int64Ty), False)], + mkAbsurdTests + "simple equality constraints with type variable equalities" + [(EqC x0Ty int32Ty), (EqC x1Ty int64Ty)] + [(EqC x0Ty x1Ty, True), + (EqC (ptrTy 64 x0Ty) (ptrTy 64 x1Ty), True), + (EqC x1Ty x1Ty, False), + (EqC (ptrTy 64 x1Ty) (ptrTy 64 x1Ty), False)], + mkAbsurdTests + "simple equality constraints with bounded type variables 1" + [(SubC x0Ty int32Ty), (SubC x1Ty int64Ty)] + [(EqC x0Ty x1Ty, False), + (EqC (ptrTy 64 x0Ty) (ptrTy 64 x1Ty), False), + (EqC x1Ty x1Ty, False), + (EqC (ptrTy 64 x1Ty) (ptrTy 64 x1Ty), False)], + mkAbsurdTests + "simple equality constraints with bounded type variables 2" + [(SubC x0Ty int32Ty), (SubC int32Ty x0Ty), (SubC x1Ty int64Ty), (SubC int64Ty x1Ty)] + [(EqC x0Ty x1Ty, True), + (EqC (ptrTy 64 x0Ty) (ptrTy 64 x1Ty), True), + (EqC x1Ty x1Ty, False), + (EqC (ptrTy 64 x1Ty) (ptrTy 64 x1Ty), False)], + mkAbsurdTests + "simple subtype constraints" + [] + [(SubC int32Ty int64Ty, False), + (SubC (ptrTy 64 int32Ty) (ptrTy 64 int64Ty), False), + (SubC int64Ty int64Ty, False), + (SubC int64Ty int32Ty, True), + (SubC (ptrTy 64 int64Ty) (ptrTy 64 int32Ty), True)], + mkAbsurdTests + "simple subtype constraints with type variable equalities" + [(EqC x0Ty int32Ty), (EqC x1Ty int64Ty)] + [(SubC x0Ty x1Ty, False), + (SubC (ptrTy 64 x0Ty) (ptrTy 64 x1Ty), False), + (SubC x1Ty x1Ty, False), + (SubC x1Ty x0Ty, True), + (SubC (ptrTy 64 x1Ty) (ptrTy 64 x0Ty), True)]] + +---------------------------------------------------------------------------- +-- Type Environment tests -constraintTests :: T.TestTree -constraintTests = T.testGroup "Type Constraint Tests" + +newtype TypeEnv = TypeEnv [(TyVar, Ty)] + deriving (Eq) + +instance Show TypeEnv where + show (TypeEnv xs) = show $ bimap PP.pretty PP.pretty <$> xs + +tyEnv :: [(TyVar, Ty)] -> TypeEnv +tyEnv = TypeEnv . sortBy (compare `on` fst) + + +mkTyEnvTest :: String -> [TyConstraint] -> [(TyVar, Ty)] -> T.TestTree +mkTyEnvTest name cs expected = T.testCase name $ (tyEnv actual) T.@?= (tyEnv expected) + where actual = Map.toList $ unifyConstraints cs + +tyEnvTests :: T.TestTree +tyEnvTests = T.testGroup "Type Constraint Tests" [ eqCTests , subCTests , orCTests + , complexCTests ] -- Simple tests having to do with equality constraints eqCTests :: T.TestTree eqCTests = T.testGroup "Equality Constraint Tests" - [ mkTest "Single EqC var left" [EqC x0Ty int64Ty] [(x0, int64Ty)], - mkTest "Single EqC var right" [EqC int64Ty x0Ty] [(x0, int64Ty)], - mkTest "Multiple EqCs" [EqC x0Ty int64Ty, EqC x1Ty int32Ty] + [ mkTyEnvTest "Single EqC var left" [EqC x0Ty int64Ty] [(x0, int64Ty)], + mkTyEnvTest "Single EqC var right" [EqC int64Ty x0Ty] [(x0, int64Ty)], + mkTyEnvTest "Multiple EqCs" [EqC x0Ty int64Ty, EqC x1Ty int32Ty] [(x0, int64Ty), (x1, int32Ty)], - mkTest "EqC Transitivity 1" [EqC x0Ty x1Ty, EqC x1Ty int32Ty] + mkTyEnvTest "EqC Transitivity 1" [EqC x0Ty x1Ty, EqC x1Ty int32Ty] [(x0, int32Ty), (x1, int32Ty)], - mkTest "EqC Transitivity 2" [EqC x1Ty int32Ty, EqC x0Ty x1Ty] + mkTyEnvTest "EqC Transitivity 2" [EqC x1Ty int32Ty, EqC x0Ty x1Ty] [(x0, int32Ty), (x1, int32Ty)], - mkTest "EqC Transitivity 2" [EqC x1Ty x2Ty, EqC x0Ty x1Ty, EqC x2Ty int64Ty] + mkTyEnvTest "EqC Transitivity 2" [EqC x1Ty x2Ty, EqC x0Ty x1Ty, EqC x2Ty int64Ty] [(x0, int64Ty), (x1, int64Ty), (x2, int64Ty)] ] -- Simple tests having to do with equality constraints. subCTests :: T.TestTree subCTests = T.testGroup "Equality Constraint Tests" - [ mkTest "Single SubC upper bound" [SubC x0Ty int64Ty] [(x0, int64Ty)], - mkTest "Single SubC lower bound" [SubC int64Ty x0Ty] [(x0, int64Ty)], - mkTest "Single SubC lower+upper bounds" [SubC x0Ty int64Ty, SubC int32Ty x0Ty] + [ mkTyEnvTest "Single SubC upper bound" [SubC x0Ty int64Ty] [(x0, int64Ty)], + mkTyEnvTest "Single SubC lower bound" [SubC int64Ty x0Ty] [(x0, int64Ty)], + mkTyEnvTest "Single SubC lower+upper bounds" [SubC x0Ty int64Ty, SubC int32Ty x0Ty] [(x0, int32Ty)], - mkTest "Multiple SubCs 1" [SubC int64Ty x0Ty, SubC x0Ty int64Ty] [(x0, int64Ty)], - mkTest "Multiple SubCs 2" [SubC int64Ty x0Ty, SubC x0Ty int64Ty, SubC x1Ty int32Ty] + mkTyEnvTest "Multiple SubCs 1" [SubC int64Ty x0Ty, SubC x0Ty int64Ty] [(x0, int64Ty)], + mkTyEnvTest "Multiple SubCs 2" [SubC int64Ty x0Ty, SubC x0Ty int64Ty, SubC x1Ty int32Ty] [(x0, int64Ty), (x1, int32Ty)], - mkTest "Multiple SubCs 3" [SubC int64Ty x0Ty, SubC x0Ty int64Ty, SubC x1Ty int32Ty, SubC x1Ty x0Ty] + mkTyEnvTest "Multiple SubCs 3" [SubC int64Ty x0Ty, SubC x0Ty int64Ty, SubC x1Ty int32Ty, SubC x1Ty x0Ty] [(x0, int64Ty), (x1, int32Ty)], - mkTest "SubC Transitivity 1" + mkTyEnvTest "SubC Transitivity 1" [SubC x0Ty int64Ty, SubC x1Ty x0Ty] [(x0, int64Ty), (x1, int64Ty)], - mkTest "SubC Transitivity 2" + mkTyEnvTest "SubC Transitivity 2" [SubC x0Ty int64Ty, SubC x1Ty x0Ty] [(x0, int64Ty), (x1, int64Ty)] ] @@ -83,19 +171,19 @@ subCTests = T.testGroup "Equality Constraint Tests" -- | Some (basic?) tests focusing on disjunctions. orCTests :: T.TestTree orCTests = T.testGroup "Disjunctive Constraint Tests" - [ mkTest "disjunctive syllogism 1" + [ mkTyEnvTest "disjunctive syllogism 1" [ orC [andC [EqC x0Ty (ptrTy 64 int64Ty), SubC x1Ty int64Ty], andC [EqC x1Ty (ptrTy 64 int64Ty), SubC x0Ty int64Ty]], SubC x0Ty int64Ty] [(x0, int64Ty), (x1, ptrTy 64 int64Ty)], - mkTest "disjunctive syllogism 2" + mkTyEnvTest "disjunctive syllogism 2" [ orC [andC [EqC x0Ty (ptrTy 64 int64Ty), SubC x1Ty int64Ty], andC [EqC x1Ty (ptrTy 64 int64Ty), SubC x0Ty int64Ty], andC [SubC x0Ty int64Ty, SubC x0Ty int64Ty]], SubC int32Ty x0Ty, SubC int32Ty x1Ty] [(x0, int32Ty), (x1, int32Ty)], - mkTest "disjunctive syllogism 3" + mkTyEnvTest "disjunctive syllogism 3" [ orC [andC [EqC x0Ty (ptrTy 64 int64Ty), SubC x1Ty int64Ty], andC [EqC x1Ty (ptrTy 64 int64Ty), SubC x0Ty int64Ty], andC [SubC x0Ty int64Ty, SubC x0Ty int64Ty]], @@ -106,19 +194,25 @@ orCTests = T.testGroup "Disjunctive Constraint Tests" [(x0, int32Ty), (x1, int32Ty), (x2, int32Ty), (x3, int32Ty)] ] -newtype TypeEnv = TypeEnv [(TyVar, Ty)] - deriving (Eq) - -instance Show TypeEnv where - show (TypeEnv xs) = show $ bimap PP.pretty PP.pretty <$> xs +-- | Non-basic (?) tests. +complexCTests :: T.TestTree +complexCTests = T.testGroup "Complex Constraint Tests" + [ mkTyEnvTest "variables related by equalities 1" + [ EqC x0Ty (ptrTy 64 x1Ty), + EqC x1Ty x2Ty, + EqC x2Ty x3Ty, + EqC x3Ty int64Ty, + orC [andC [EqC x0Ty (ptrTy 64 int32Ty), EqC x4Ty int64Ty], + andC [EqC x0Ty (ptrTy 64 int64Ty), EqC x4Ty int32Ty]] + ] + [(x0, ptrTy 64 int64Ty), + (x1, int64Ty), + (x2, int64Ty), + (x3, int64Ty), + (x4, int32Ty)] + ] -tyEnv :: [(TyVar, Ty)] -> TypeEnv -tyEnv = TypeEnv . sortBy (compare `on` fst) -mkTest :: String -> [TyConstraint] -> [(TyVar, Ty)] -> T.TestTree -mkTest name cs expected = - let actual = Map.toList $ unifyConstraints cs - in T.testCase name $ (tyEnv actual) T.@?= (tyEnv expected)