few more type env tests, absurd constraint tests

src/Reopt/TypeInference/Constraints.hs

@@ -526,17 +526,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
@@ -552,6 +555,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`?
@@ -730,32 +750,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

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
     ]
 

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,65 +41,149 @@ 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)]
   ]
 
 -- | 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)