Add validity checks for IntSet and IntMap

Data/IntMap/Internal.hs

@@ -353,6 +353,15 @@ data IntMap a = Bin {-# UNPACK #-} !Prefix
                     {-# UNPACK #-} !Mask
                     !(IntMap a)
                     !(IntMap a)
+-- Fields:
+--   prefix: The most significant bits shared by all keys in this Bin.
+--   mask: The switching bit to determine if a key should follow the left
+--         or right subtree of a 'Bin'.
+-- Invariant: Nil is never found as a child of Bin.
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
               | Tip {-# UNPACK #-} !Key a
               | Nil
 

Data/IntSet/Internal.hs

@@ -180,6 +180,7 @@ module Data.IntSet.Internal (
     , suffixBitMask
     , prefixBitMask
     , bitmapOf
+    , zero
     ) where
 
 import Control.DeepSeq (NFData(rnf))
@@ -250,8 +251,8 @@ data IntSet = Bin {-# UNPACK #-} !Prefix {-# UNPACK #-} !Mask !IntSet !IntSet
 -- Invariant: In Bin prefix mask left right, left consists of the elements that
 --            don't have the mask bit set; right is all the elements that do.
             | Tip {-# UNPACK #-} !Prefix {-# UNPACK #-} !BitMap
--- Invariant: The Prefix is zero for all but the last 5 (on 32 bit arches) or 6
---            bits (on 64 bit arches). The values of the map represented by a tip
+-- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
+--            (on 64 bit arches). The values of the set represented by a tip
 --            are the prefix plus the indices of the set bits in the bit map.
             | Nil
 
@@ -323,7 +324,7 @@ size = go 0
 
 -- | /O(min(n,W))/. Is the value a member of the set?
 
--- See Note: Local 'go' functions and capturing]
+-- See Note: Local 'go' functions and capturing.
 member :: Key -> IntSet -> Bool
 member !x = go
   where
@@ -1250,6 +1251,7 @@ bitmapOf x = bitmapOfSuffix (suffixOf x)
 {--------------------------------------------------------------------
   Endian independent bit twiddling
 --------------------------------------------------------------------}
+-- Returns True iff the bits set in i and the Mask m are disjoint.
 zero :: Int -> Mask -> Bool
 zero i m
   = (natFromInt i) .&. (natFromInt m) == 0

containers.cabal

@@ -371,6 +371,7 @@ Test-suite intmap-lazy-properties
         Data.IntMap.Lazy
         Data.IntSet
         Data.IntSet.Internal
+        IntMapValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.StrictFold
         Utils.Containers.Internal.StrictPair
@@ -399,6 +400,7 @@ Test-suite intmap-strict-properties
         Data.IntMap.Strict
         Data.IntSet
         Data.IntSet.Internal
+        IntMapValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.StrictFold
         Utils.Containers.Internal.StrictPair
@@ -425,6 +427,7 @@ Test-suite intset-properties
         Data.IntSet.Internal
         Data.Set
         Data.Set.Internal
+        IntSetValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.PtrEquality
         Utils.Containers.Internal.StrictFold

tests/IntMapValidity.hs

@@ -0,0 +1,52 @@
+module IntMapValidity (valid) where
+
+import Data.Bits (xor, (.&.))
+import Data.IntMap.Internal
+import Test.QuickCheck (Property, counterexample, property, (.&&.))
+
+{--------------------------------------------------------------------
+  Assertions
+--------------------------------------------------------------------}
+-- | Returns true iff the internal structure of the IntMap is valid.
+valid :: IntMap a -> Property
+valid t =
+  counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
+  counterexample "commonPrefix" (commonPrefix t) .&&.
+  counterexample "maskRespected" (maskRespected t)
+
+-- Invariant: Nil is never found as a child of Bin.
+nilNeverChildOfBin :: IntMap a  -> Bool
+nilNeverChildOfBin t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ _ l r -> noNilInSet l && noNilInSet r
+  where
+    noNilInSet t' =
+      case t' of
+        Nil -> False
+        Tip _ _ -> True
+        Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
+
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+commonPrefix :: IntMap a -> Bool
+commonPrefix t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    b@(Bin p _ _ _) -> all (sharedPrefix p) (keys b)
+  where
+    sharedPrefix :: Prefix -> Int -> Bool
+    sharedPrefix p a = 0 == (p `xor` (p .&. a))
+
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
+maskRespected :: IntMap a -> Bool
+maskRespected t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ binMask l r ->
+      all (\x -> zero x binMask) (keys l) &&
+      all (\x -> not (zero x binMask)) (keys r)

tests/IntSetValidity.hs

@@ -0,0 +1,86 @@
+{-# LANGUAGE CPP #-}
+module IntSetValidity (valid) where
+
+import Data.Bits (xor, (.&.))
+import Data.IntSet.Internal
+import Test.QuickCheck (Property, counterexample, property, (.&&.))
+
+{--------------------------------------------------------------------
+  Assertions
+--------------------------------------------------------------------}
+-- | Returns true iff the internal structure of the IntSet is valid.
+valid :: IntSet -> Property
+valid t =
+  counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
+  counterexample "maskPowerOfTwo" (maskPowerOfTwo t) .&&.
+  counterexample "commonPrefix" (commonPrefix t) .&&.
+  counterexample "markRespected" (maskRespected t) .&&.
+  counterexample "tipsValid" (tipsValid t)
+
+-- Invariant: Nil is never found as a child of Bin.
+nilNeverChildOfBin :: IntSet -> Bool
+nilNeverChildOfBin t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ _ l r -> noNilInSet l && noNilInSet r
+  where
+    noNilInSet t' =
+      case t' of
+        Nil -> False
+        Tip _ _ -> True
+        Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
+
+-- Invariant: The Mask is a power of 2.  It is the largest bit position at which
+--            two elements of the set differ.
+maskPowerOfTwo :: IntSet -> Bool
+maskPowerOfTwo t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ m l r ->
+      (m `mod` 2 == 0) && maskPowerOfTwo l && maskPowerOfTwo r
+
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+commonPrefix :: IntSet -> Bool
+commonPrefix t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    b@(Bin p _ _ _) -> all (sharedPrefix p) (elems b)
+  where
+    sharedPrefix :: Prefix -> Int -> Bool
+    sharedPrefix p a = 0 == (p `xor` (p .&. a))
+
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
+maskRespected :: IntSet -> Bool
+maskRespected t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ binMask l r ->
+      all (\x -> zero x binMask) (elems l) &&
+      all (\x -> not (zero x binMask)) (elems r)
+
+-- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
+--            (on 64 bit arches). The values of the set represented by a tip
+--            are the prefix plus the indices of the set bits in the bit map.
+--
+-- Note: Valid entries stored in tip omitted.
+tipsValid :: IntSet -> Bool
+tipsValid t =
+  case t of
+    Nil -> True
+    tip@(Tip p b) -> validTipPrefix p
+    Bin _ _ l r -> tipsValid l && tipsValid r
+
+validTipPrefix :: Prefix -> Bool
+#if WORD_SIZE_IN_BITS==32
+-- Last 5 bits of the prefix must be zero for 32 bit arches.
+validTipPrefix p = (0x0000001F .&. p) == 0
+#else
+-- Last 6 bits of the prefix must be zero 64 bit anches.
+validTipPrefix p = (0x000000000000003F .&. p) == 0
+#endif

tests/intmap-properties.hs

@@ -6,6 +6,7 @@ import Data.IntMap.Strict as Data.IntMap hiding (showTree)
 import Data.IntMap.Lazy as Data.IntMap hiding (showTree)
 #endif
 import Data.IntMap.Internal.Debug (showTree)
+import IntMapValidity (valid)
 
 import Data.Monoid
 import Data.Maybe hiding (mapMaybe)
@@ -123,6 +124,8 @@ main = defaultMain
              , testCase "maxView" test_maxView
              , testCase "minViewWithKey" test_minViewWithKey
              , testCase "maxViewWithKey" test_maxViewWithKey
+             , testProperty "valid"                prop_valid
+             , testProperty "empty valid"          prop_emptyValid
              , testProperty "insert to singleton"  prop_singleton
              , testProperty "insert then lookup"   prop_insertLookup
              , testProperty "insert then delete"   prop_insertDelete
@@ -770,28 +773,57 @@ test_maxViewWithKey = do
     maxViewWithKey (fromList [(5,"a"), (3,"b")]) @?= Just ((5,"a"), singleton 3 "b")
     maxViewWithKey (empty :: SMap) @?= Nothing
 
+----------------------------------------------------------------
+-- Valid IntMaps
+----------------------------------------------------------------
+
+forValid :: Testable b => (SMap -> b) -> Property
+forValid f = forAll arbitrary $ \t ->
+    classify (size t == 0) "empty" $
+    classify (size t > 0 && size t <= 10) "small" $
+    classify (size t > 10 && size t <= 64) "medium" $
+    classify (size t > 64) "large" $ f t
+
+forValidUnitTree :: Testable b => (SMap -> b) -> Property
+forValidUnitTree f = forValid f
+
+prop_valid :: Property
+prop_valid = forValidUnitTree $ \t -> valid t
+
 ----------------------------------------------------------------
 -- QuickCheck
 ----------------------------------------------------------------
 
-prop_singleton :: Int -> Int -> Bool
-prop_singleton k x = insert k x empty == singleton k x
+prop_emptyValid :: Property
+prop_emptyValid = valid empty
+
+prop_singleton :: Int -> Int -> Property
+prop_singleton k x =
+  case singleton k x of
+    s ->
+      valid s .&&.
+      s === insert k x empty
 
 prop_insertLookup :: Int -> UMap -> Bool
 prop_insertLookup k t = lookup k (insert k () t) /= Nothing
 
 prop_insertDelete :: Int -> UMap -> Property
-prop_insertDelete k t = (lookup k t == Nothing) ==> (delete k (insert k () t) == t)
+prop_insertDelete k t =
+  lookup k t == Nothing ==>
+    case delete k (insert k () t) of
+      t' -> valid t' .&&. t' === t
 
 prop_deleteNonMember :: Int -> UMap -> Property
 prop_deleteNonMember k t = (lookup k t == Nothing) ==> (delete k t == t)
 
 ----------------------------------------------------------------
 
-prop_unionModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_unionModel xs ys
-  = sort (keys (union (fromList xs) (fromList ys)))
-    == sort (nub (Prelude.map fst xs ++ Prelude.map fst ys))
+prop_unionModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_unionModel xs ys =
+  case union (fromList xs) (fromList ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort (nub (Prelude.map fst xs ++ Prelude.map fst ys))
 
 prop_unionSingleton :: IMap -> Int -> Int -> Bool
 prop_unionSingleton t k x = union (singleton k x) t == insert k x t
@@ -807,15 +839,23 @@ prop_unionSum xs ys
   = sum (elems (unionWith (+) (fromListWith (+) xs) (fromListWith (+) ys)))
     == (sum (Prelude.map snd xs) + sum (Prelude.map snd ys))
 
-prop_differenceModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_differenceModel xs ys
-  = sort (keys (difference (fromListWith (+) xs) (fromListWith (+) ys)))
-    == sort ((List.\\) (nub (Prelude.map fst xs)) (nub (Prelude.map fst ys)))
-
-prop_intersectionModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_intersectionModel xs ys
-  = sort (keys (intersection (fromListWith (+) xs) (fromListWith (+) ys)))
-    == sort (nub ((List.intersect) (Prelude.map fst xs) (Prelude.map fst ys)))
+prop_differenceModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_differenceModel xs ys =
+  case difference (fromListWith (+) xs) (fromListWith (+) ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort ((List.\\)
+                                 (nub (Prelude.map fst xs))
+                                 (nub (Prelude.map fst ys)))
+
+prop_intersectionModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_intersectionModel xs ys =
+  case intersection (fromListWith (+) xs) (fromListWith (+) ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort (nub ((List.intersect)
+                                      (Prelude.map fst xs)
+                                      (Prelude.map fst ys)))
 
 prop_intersectionWithModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
 prop_intersectionWithModel xs ys
@@ -902,19 +942,20 @@ prop_ascDescList :: [Int] -> Bool
 prop_ascDescList xs = toAscList m == reverse (toDescList m)
   where m = fromList $ zip xs $ repeat ()
 
-prop_fromList :: [Int] -> Bool
+prop_fromList :: [Int] -> Property
 prop_fromList xs
   = case fromList (zip xs xs) of
-      t -> t == fromAscList (zip sort_xs sort_xs) &&
-           t == fromDistinctAscList (zip nub_sort_xs nub_sort_xs) &&
-           t == List.foldr (uncurry insert) empty (zip xs xs)
+      t -> valid t .&&.
+           t === fromAscList (zip sort_xs sort_xs) .&&.
+           t === fromDistinctAscList (zip nub_sort_xs nub_sort_xs) .&&.
+           t === List.foldr (uncurry insert) empty (zip xs xs)
   where sort_xs = sort xs
         nub_sort_xs = List.map List.head $ List.group sort_xs
 
 ----------------------------------------------------------------
 
-prop_alter :: UMap -> Int -> Bool
-prop_alter t k = case lookup k t of
+prop_alter :: UMap -> Int -> Property
+prop_alter t k = valid t' .&&. case lookup k t of
     Just _  -> (size t - 1) == size t' && lookup k t' == Nothing
     Nothing -> (size t + 1) == size t' && lookup k t' /= Nothing
   where
@@ -1024,14 +1065,18 @@ prop_deleteMaxModel ys = length ys > 0 ==>
 prop_filter :: Fun Int Bool -> [(Int, Int)] -> Property
 prop_filter p ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
-      m  = fromList xs
-  in  filter (apply p) m == fromList (List.filter (apply p . snd) xs)
+      m  = filter (apply p) (fromList xs)
+  in  valid m .&&.
+      m === fromList (List.filter (apply p . snd) xs)
 
 prop_partition :: Fun Int Bool -> [(Int, Int)] -> Property
 prop_partition p ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
-      m  = fromList xs
-  in  partition (apply p) m == let (a,b) = (List.partition (apply p . snd) xs) in (fromList a, fromList b)
+      m@(l, r) = partition (apply p) (fromList xs)
+  in  valid l .&&.
+      valid r .&&.
+      m === let (a,b) = (List.partition (apply p . snd) xs)
+            in (fromList a, fromList b)
 
 prop_map :: Fun Int Int -> [(Int, Int)] -> Property
 prop_map f ys = length ys > 0 ==>
@@ -1055,8 +1100,10 @@ prop_splitModel :: Int -> [(Int, Int)] -> Property
 prop_splitModel n ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
       (l, r) = split n $ fromList xs
-  in  toAscList l == sort [(k, v) | (k,v) <- xs, k < n] &&
-      toAscList r == sort [(k, v) | (k,v) <- xs, k > n]
+  in  valid l .&&.
+      valid r .&&.
+      toAscList l === sort [(k, v) | (k,v) <- xs, k < n] .&&.
+      toAscList r === sort [(k, v) | (k,v) <- xs, k > n]
 
 prop_splitRoot :: IMap -> Bool
 prop_splitRoot s = loop ls && (s == unions ls)