Improve jump table bounds accuracy.

This adds functionality to the jump table bounds to work with trunc
that was deliberately removed in the last patch due to buggy code.

base/macaw-base.cabal

@@ -81,5 +81,10 @@ library
   ghc-prof-options: -O2 -fprof-auto-top
   default-language: Haskell2010
 
+  default-extensions:
+    GADTs
+    ScopedTypeVariables
+    TypeOperators
+
   if impl(ghc >= 8.6)
     default-extensions: NoStarIsType

base/src/Data/Macaw/AbsDomain/JumpBounds.hs

@@ -1,7 +1,4 @@
-{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 module Data.Macaw.AbsDomain.JumpBounds
   ( InitialIndexBounds
@@ -18,28 +15,39 @@ module Data.Macaw.AbsDomain.JumpBounds
 
 import           Control.Lens
 import           Control.Monad.State
-import           Data.Bits
 import           Data.Functor
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
-import           Data.Parameterized.NatRepr (maxUnsigned)
+import           Data.Parameterized.NatRepr
+import           Numeric.Natural
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import           Data.Macaw.CFG
 import           Data.Macaw.Types
 
 -- | An upper bound on a value.
-data UpperBound tp = forall w . (tp ~ BVType w) => IntegerUpperBound Integer
+data UpperBound tp where
+  -- | @IntegerUpperBound b v@ indicates the low @b@ bits of the value
+  -- are at most @v@ when the bitvector is treated as an unsigned
+  -- integer.
+  UBVUpperBound :: (u <= w) => !(NatRepr u) -> !Natural -> UpperBound (BVType w)
 
 instance Eq (UpperBound tp) where
-  IntegerUpperBound x == IntegerUpperBound y = x == y
+  UBVUpperBound u x == UBVUpperBound v y =
+    case testEquality u v of
+      Nothing -> False
+      Just Refl -> x == y
 
 instance MapF.EqF UpperBound where
   eqF = (==)
 
 instance Ord (UpperBound tp) where
-  compare (IntegerUpperBound x) (IntegerUpperBound y) = compare x y
+  compare (UBVUpperBound u x) (UBVUpperBound v y) =
+    case compareF u v of
+      LTF -> LT
+      EQF -> compare x y
+      GTF -> GT
 
 deriving instance Show (UpperBound tp)
 
@@ -54,7 +62,8 @@ instance MapF.TestEquality r => Eq (InitialIndexBounds r) where
 instance ShowF r => Pretty (InitialIndexBounds r) where
   pretty r = vcat $ ppPair <$> MapF.toList (initialRegUpperBound r)
     where ppPair :: MapF.Pair r UpperBound -> Doc
-          ppPair (MapF.Pair k (IntegerUpperBound b)) = text (showF k) <+> text "<=" <+> text (show b)
+          ppPair (MapF.Pair k (UBVUpperBound w b)) =
+            text (showF k) <> text ":[" <> text (show w) <> text "] <= " <> text (show b)
 
 -- | Create initial index bounds that can represent any system state.
 arbitraryInitialBounds :: InitialIndexBounds reg
@@ -63,6 +72,7 @@ arbitraryInitialBounds = InitialIndexBounds { initialRegUpperBound = MapF.empty
 
 type Changed = State Bool
 
+-- | Record the value has changed if the Boolean is true.
 markChanged :: Bool -> Changed ()
 markChanged b = modify (|| b)
 
@@ -80,8 +90,12 @@ joinInitialBounds :: forall r
                   -> Maybe (InitialIndexBounds r)
 joinInitialBounds old new = runChanged $ do
   let combineF :: r tp -> UpperBound tp -> UpperBound tp -> Changed (Maybe (UpperBound tp))
-      combineF _ (IntegerUpperBound x) (IntegerUpperBound y) =
-        markChanged (x < y) $> Just (IntegerUpperBound (max x y))
+      combineF _ (UBVUpperBound u x) (UBVUpperBound v y) =
+        case testEquality u v of
+          Just Refl ->
+            markChanged (x < y) $> Just (UBVUpperBound u (max x y))
+          Nothing ->
+            markChanged True $> Nothing
 
       -- Mark upper bounds exclusively in old set.
       -- If we have any only-old bounds add mark value as changed.
@@ -118,40 +132,57 @@ mkIndexBounds i = IndexBounds { _regBounds = initialRegUpperBound i
 
 -- | Add a inclusive upper bound to a value.
 --
+-- Our operation allows one to set the upper bounds on the low order
+-- of an integer.  This is represented by the extra argument `NatRepr
+-- u`.
+--
 -- This either returns the refined bounds, or `Left msg` where `msg`
 -- is an explanation of what inconsistency was detected.  The upper
 -- bounds must be non-negative.
 addUpperBound :: ( MapF.OrdF (ArchReg arch)
                  , HasRepr (ArchReg arch) TypeRepr
+                 , u <= w
                  )
                => BVValue arch ids w
-               -> Integer -- ^ Upper bound as an unsigned number
+                 -- ^ Value we are adding upper bound for.
+               -> NatRepr u
+                  -- ^ Restrict upper bound to only `u` bits.
+               -> Natural
+               -- ^ Upper bound as an unsigned number
                -> IndexBounds (ArchReg arch) ids
+                 -- ^ Current bounds.
                -> Either String (IndexBounds (ArchReg arch) ids)
-addUpperBound v u bnds
+addUpperBound v u bnd bnds
     -- Do nothing if upper bounds equals or exceeds function
-  | u >= maxUnsigned (typeWidth v) = Right bnds
-  | u < 0 = error "addUpperBound given negative value."
+  | bnd >= fromInteger (maxUnsigned (typeWidth v)) = Right bnds
   | otherwise =
   case v of
-    BVValue _ c | c <= u -> Right bnds
+    BVValue _ c | c <= toInteger bnd -> Right bnds
                 | otherwise -> Left "Constant given upper bound that is statically less than given bounds"
     RelocatableValue{} -> Right bnds
     SymbolValue{}      -> Right bnds
     AssignedValue a ->
       case assignRhs a of
-        EvalApp (UExt x _) -> addUpperBound x u bnds
--- The code below tries to associate an upper bound through a truncation, but this is not sound.
--- The underlying value may have 0 low order bits, but still be a large number.
---        EvalApp (Trunc x w) ->
---          if u < maxUnsigned w then
---            addUpperBound x u bnds
---           else
---            Right $ bnds
+        EvalApp (UExt x _) ->
+          case testLeq u (typeWidth x) of
+            Just LeqProof -> addUpperBound x u bnd bnds
+            Nothing ->
+              case leqRefl (typeWidth x) of
+                LeqProof -> addUpperBound x (typeWidth x) bnd bnds
+        EvalApp (Trunc x w) ->
+          case testLeq u w of
+            Just LeqProof -> do
+              case testLeq u (typeWidth x) of
+                Just LeqProof -> addUpperBound x u bnd bnds
+                Nothing -> error "addUpperBound invariant broken"
+            Nothing -> do
+              case testLeq w (typeWidth x) of
+                Just LeqProof -> addUpperBound x w bnd bnds
+                Nothing -> error "addUpperBound invariant broken"
         _ ->
-          Right $ bnds & assignUpperBound %~ MapF.insertWith min (assignId a) (IntegerUpperBound u)
+          Right $ bnds & assignUpperBound %~ MapF.insertWith min (assignId a) (UBVUpperBound u bnd)
     Initial r ->
-      Right $ bnds & regBounds %~ MapF.insertWith min r (IntegerUpperBound u)
+      Right $ bnds & regBounds %~ MapF.insertWith min r (UBVUpperBound u bnd)
 
 
 -- | Assert a predicate is true/false and update bounds.
@@ -169,13 +200,24 @@ assertPred :: ( OrdF (ArchReg arch)
 assertPred (AssignedValue a) isTrue bnds =
   case assignRhs a of
     -- Given x < c), assert x <= c-1
-    EvalApp (BVUnsignedLt x (BVValue _ c)) | isTrue     -> addUpperBound x (c-1) bnds
+    EvalApp (BVUnsignedLt x (BVValue _ c))
+      | isTrue     ->
+        if c > 0 then
+          addUpperBound x (typeWidth x) (fromInteger (c-1)) bnds
+         else
+          Left "x < 0 must be false."
     -- Given not (c < y), assert y <= c
-    EvalApp (BVUnsignedLt (BVValue _ c) y) | not isTrue -> addUpperBound y c bnds
+    EvalApp (BVUnsignedLt (BVValue _ c) y)
+      | not isTrue -> addUpperBound y (typeWidth y) (fromInteger c) bnds
     -- Given x <= c, assert x <= c
-    EvalApp (BVUnsignedLe x (BVValue _ c)) | isTrue     -> addUpperBound x c bnds
+    EvalApp (BVUnsignedLe x (BVValue _ c))
+      | isTrue     -> addUpperBound x (typeWidth x) (fromInteger c) bnds
     -- Given not (c <= y), assert y <= (c-1)
-    EvalApp (BVUnsignedLe (BVValue _ c) y) | not isTrue -> addUpperBound y (c-1) bnds
+    EvalApp (BVUnsignedLe (BVValue _ c) y) | not isTrue ->
+      if c > 0 then
+        addUpperBound y (typeWidth y) (fromInteger (c-1)) bnds
+       else
+        Left "0 <= x cannot be false"
     -- Given x && y, assert x, then assert y
     EvalApp (AndApp l r) | isTrue     -> (assertPred l True >=> assertPred r True) bnds
     -- Given not (x || y), assert not x, then assert not y
@@ -195,7 +237,7 @@ unsignedUpperBound :: ( MapF.OrdF (ArchReg arch)
 unsignedUpperBound bnds v =
   case v of
     BoolValue _ -> Left "Boolean values do not have bounds."
-    BVValue _ i -> Right (IntegerUpperBound i)
+    BVValue w i -> Right $! UBVUpperBound w (fromInteger i)
     RelocatableValue{} ->
       Left "Relocatable values do not have bounds."
     SymbolValue{} ->
@@ -207,23 +249,32 @@ unsignedUpperBound bnds v =
           case assignRhs a of
             EvalApp (BVAnd _ x y) -> do
               case (unsignedUpperBound bnds x,  unsignedUpperBound bnds y) of
-                (Right (IntegerUpperBound xb), Right (IntegerUpperBound yb)) ->
-                  Right (IntegerUpperBound (min xb yb))
-                (Right xb, Left{}) -> Right xb
+                (Right (UBVUpperBound xw xb), Right (UBVUpperBound yw yb))
+                  | Just Refl <- testEquality xw yw ->
+                    Right (UBVUpperBound xw (min xb yb))
+                (Right xb, _) -> Right xb
                 (Left{}, yb)       -> yb
             EvalApp (SExt x w) -> do
-              IntegerUpperBound r <- unsignedUpperBound bnds x
-              -- sign-extend r
-              pure . IntegerUpperBound
-                $ if r < 2^(natValue w-1)
-                  then r
-                  else maxUnsigned (typeWidth v) .&. r
-            EvalApp (UExt x _) -> do
-              IntegerUpperBound r <- unsignedUpperBound bnds x
-              pure (IntegerUpperBound r)
+              UBVUpperBound u b <- unsignedUpperBound bnds x
+              case testLeq u w of
+                Just LeqProof -> pure $! UBVUpperBound u b
+                Nothing -> error "unsignedUpperBound given bad width"
+            EvalApp (UExt x w) -> do
+              UBVUpperBound u r <- unsignedUpperBound bnds x
+              -- If bound is full width, then we can keep it, otherwise we only have subset.
+              case testEquality u (typeWidth x) of
+                Just Refl -> pure $! UBVUpperBound w r
+                Nothing ->
+                  case testLeq u w of
+                    Just LeqProof -> pure $! UBVUpperBound u r
+                    Nothing -> error "unsignedUpperBound given bad width"
             EvalApp (Trunc x w) -> do
-              IntegerUpperBound xr <- unsignedUpperBound bnds x
-              pure $! IntegerUpperBound (min xr (maxUnsigned w))
+              UBVUpperBound u xr <- unsignedUpperBound bnds x
+              case testLeq u w of
+                Just LeqProof -> do
+                  pure $! UBVUpperBound u xr
+                Nothing -> do
+                  pure $! UBVUpperBound w (min xr (fromInteger (maxUnsigned w)))
             _ -> Left $ "Could not find upper bounds for " ++ show (assignId a) ++ "."
     Initial r ->
       case MapF.lookup r (bnds^.regBounds) of

base/src/Data/Macaw/Discovery.hs

@@ -522,9 +522,10 @@ matchBoundedMemArray mem aps val
     -- Check stride covers at least number of bytes read.
   , memReprBytes tp <= stride
     -- Resolve a static upper bound to array.
-  , Right (Jmp.IntegerUpperBound bnd)
+  , Right (Jmp.UBVUpperBound bndw bnd)
       <- Jmp.unsignedUpperBound (aps^.indexBounds) ixVal
-  , cnt <- bnd+1
+  , Just Refl <- testEquality bndw (typeWidth ixVal)
+  , cnt <- toInteger (bnd+1)
     -- Check array actually fits in memory.
   , cnt * toInteger stride <= segoffBytesLeft base
     -- Get memory contents after base