Change the Array storage type and related utilities to use Natural

instead of `Bytes` to describe array sizes and indices.

Fixes #198

crucible-llvm/src/Lang/Crucible/LLVM/Bytes.hs

@@ -21,6 +21,7 @@ module Lang.Crucible.LLVM.Bytes
   , bytesToBV
   , toBytes
   , bitsToBytes
+  , natBytesMul
   )  where
 
 import qualified Data.BitVector.Sized as BV
@@ -54,5 +55,9 @@ toBytes = Bytes . fromIntegral
 bitsToBytes :: Integral a => a -> Bytes
 bitsToBytes n = Bytes ( (fromIntegral n + 7) `div` 8 )
 
+-- | Multiply a number of bytes by a natural number
+natBytesMul :: Natural -> Bytes -> Bytes
+natBytesMul n (Bytes x) = Bytes (toInteger n * x)
+
 type Addr = Bytes
 type Offset = Bytes

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs

@@ -56,7 +56,9 @@ import qualified Data.Map as Map
 import Data.Maybe
 import Data.Vector (Vector)
 import qualified Data.Vector as V
+import Numeric.Natural
 
+import Lang.Crucible.Panic
 import Lang.Crucible.LLVM.Bytes
 import Lang.Crucible.LLVM.MemModel.Type
 
@@ -176,19 +178,20 @@ splitTypeValue tp d subFn = assert (d > 0) $
     X86_FP80 -> BVToX86_FP80 (subFn 0 (bitvectorType 10))
     Array n0 etp -> assert (n0 > 0) $ do
       let esz = storageTypeSize etp
-      let (c,part) = assert (esz > 0) $ d `divMod` esz
-      let n = n0 - c
-      let o = d - part -- (Bytes c) * esz
+      let (c,part) = assert (esz > 0) $ toInteger d `divMod` toInteger esz
+      let n = toInteger n0 - toInteger c
+      let o = d - toBytes part -- (Bytes c) * esz
       let consPartial
-            | part == 0 = subFn o (arrayType n etp)
+            | n < 0 = panic "splitTypeValue" ["Unexpected array size: " ++ show n, show tp, show d]
+            | part == 0 = subFn o (arrayType (fromInteger n) etp)
             | n > 1 =
                 ConsArray (subFn o etp)
-                          (subFn (o+esz) (arrayType (n-1) etp))
+                          (subFn (o+esz) (arrayType (fromInteger (n-1)) etp))
             | otherwise = assert (n == 1) $
                 singletonArray etp (subFn o etp)
       let result
-            | c > 0 = assert (c < n0) $
-              AppendArray (subFn 0 (arrayType c etp))
+            | c > 0 = assert (c < toInteger n0) $
+              AppendArray (subFn 0 (arrayType (fromInteger c) etp))
                           consPartial
             | otherwise = consPartial
       result
@@ -398,7 +401,7 @@ data ValueView
   | FloatToBV ValueView
   | DoubleToBV ValueView
   | X86_FP80ToBV ValueView
-  | ArrayElt Bytes StorageType Bytes ValueView
+  | ArrayElt Natural StorageType Natural ValueView
 
   | FieldVal (Vector (Field StorageType)) Int ValueView
   deriving (Show, Eq, Ord)
@@ -472,12 +475,14 @@ loadBitvector lo lw so v = do
     Array n tp -> snd $ foldl1 cv (val <$> r)
       where cv (wx,x) (wy,y) = (wx + wy, concatBV wx x wy y)
             esz = storageTypeSize tp
-            c0 = assert (esz > 0) $ (lo - so) `div` esz
-            (c1,p1) = (le - so) `divMod` esz
+            c0 = assert (esz > 0) $ toInteger (lo - so) `div` toInteger esz
+            (c1, p1) = toInteger (le - so) `divMod` toInteger esz
             -- Get range of indices to read.
             r | p1 == 0 = assert (c1 > c0) [c0..c1-1]
               | otherwise = assert (c1 >= c0) [c0..c1]
-            val i = retValue (so + i*esz) (ArrayElt n tp i v)
+            val i
+              | i >= 0 = retValue (so + natBytesMul (fromInteger i) esz) (ArrayElt n tp (fromInteger i) v)
+              | otherwise = panic "loadBitvector" ["Bad array index", show i, show (lo, lw, so, v)]
     Struct sflds -> assert (not (null r)) $ snd $ foldl1 cv r
       where cv (wx,x) (wy,y) = (wx+wy, concatBV wx x wy y)
             r = concat (zipWith val [0..] (V.toList sflds))

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -67,6 +67,7 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Vector (Vector)
 import qualified Data.Vector as V
+import           Numeric.Natural
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import qualified Data.BitVector.Sized as BV
@@ -641,9 +642,9 @@ selectHighBv _ _ _ (NoErr _ v) =
 -- | Look up an element in a partial LLVM array value.
 arrayElt ::
   IsExprBuilder sym =>
-  Bytes ->
+  Natural ->
   StorageType ->
-  Bytes ->
+  Natural ->
   PartLLVMVal sym ->
   IO (PartLLVMVal sym)
 arrayElt sz tp idx (NoErr p (LLVMValZero _)) -- TODO(langston) typecheck

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Type.hs

@@ -40,6 +40,7 @@ import Control.Monad.State
 import Data.Typeable
 import Data.Vector (Vector)
 import qualified Data.Vector as V
+import Numeric.Natural
 
 import Lang.Crucible.LLVM.Bytes
 
@@ -62,7 +63,7 @@ data StorageTypeF v
   | Float
   | Double
   | X86_FP80
-  | Array !Bytes !v
+  | Array !Natural !v -- ^ Number of elements and element type
   | Struct !(Vector (Field v))
   deriving (Eq, Ord, Show, Typeable)
 
@@ -93,7 +94,7 @@ mkStorageType tf = StorageType tf $
     Float -> 4
     Double -> 8
     X86_FP80 -> 10
-    Array n e -> n * storageTypeSize e
+    Array n e -> natBytesMul n (storageTypeSize e)
     Struct flds -> assert (V.length flds > 0) (fieldEnd (V.last flds))
 
 bitvectorType :: Bytes -> StorageType
@@ -108,8 +109,8 @@ doubleType = mkStorageType Double
 x86_fp80Type :: StorageType
 x86_fp80Type = mkStorageType X86_FP80
 
-arrayType :: Bytes -> StorageType -> StorageType
-arrayType n e = StorageType (Array n e) (n * storageTypeSize e)
+arrayType :: Natural -> StorageType -> StorageType
+arrayType n e = StorageType (Array n e) (natBytesMul n (storageTypeSize e))
 
 structType :: V.Vector (Field StorageType) -> StorageType
 structType flds = assert (V.length flds > 0) $
@@ -135,7 +136,7 @@ typeEnd a tp = seq a $
     Double -> a + 8
     X86_FP80 -> a + 10
     Array 0 _   -> a
-    Array n etp -> typeEnd (a + (n-1) * (storageTypeSize etp)) etp
+    Array n etp -> typeEnd (a + natBytesMul (n-1) (storageTypeSize etp)) etp
     Struct flds -> typeEnd (a + fieldOffset f) (f^.fieldVal)
       where f = V.last flds
 

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Value.hs

@@ -271,9 +271,11 @@ zeroExpandLLVMVal sym (StorageType tpf _sz) =
     Float    -> LLVMValFloat SingleSize <$> iFloatPZero sym SingleFloatRepr
     Double   -> LLVMValFloat DoubleSize <$> iFloatPZero sym DoubleFloatRepr
     X86_FP80 -> LLVMValFloat X86_FP80Size <$> iFloatPZero sym X86_80FloatRepr
-    Array n ty ->
-      LLVMValArray ty . V.replicate (fromIntegral (bytesToInteger n)) <$>
-        zeroExpandLLVMVal sym ty
+    Array n ty
+      | toInteger n < toInteger (maxBound :: Int) ->
+        LLVMValArray ty . V.replicate (fromIntegral n :: Int) <$>
+          zeroExpandLLVMVal sym ty
+      | otherwise -> panic "zeroExpandLLVMVal" ["Array length too large", show n]
     Struct vec ->
       LLVMValStruct <$>
         V.zipWithM (\f t -> (f,) <$> zeroExpandLLVMVal sym t) vec (fmap (view fieldVal) vec)