fix calldataload

Author: MrChico

src/hevm/hevm-cli/hevm-cli.hs

@@ -729,7 +729,7 @@ symvmFromCommand cmd = do
     -- dynamic calldata via (bounded) haskell list
     (Nothing, Nothing, _) -> do
       cd <- sbytes256
-      len <- freshVar_
+      len <- sw256 <$> freshVar_
       return (CalldataDynamic (cd, len), len .<= 256)
 
     -- fully concrete calldata

src/hevm/src/EVM.hs

@@ -225,7 +225,7 @@ data FrameState = FrameState
   , _pc           :: Int
   , _stack        :: [SymWord]
   , _memory       :: Buffer
-  , _memorySize   :: SWord 32
+  , _memorySize   :: SymWord
   , _calldata     :: Calldata
   , _callvalue    :: SymWord
   , _caller       :: SAddr
@@ -723,7 +723,7 @@ exec1 = do
         0x35 -> stackOp1 (const g_verylow) $
           case the state calldata of
             CalldataBuffer bf -> flip readSWord bf
-            CalldataDynamic bf -> \(S _ i) -> readStaticWordWithBound (sFromIntegral i) bf
+            CalldataDynamic bf -> flip readStaticWordWithBound bf
 
         -- op: CALLDATASIZE
         0x36 ->
@@ -1007,7 +1007,7 @@ exec1 = do
         -- op: MSIZE
         0x59 ->
           limitStack 1 . burn g_base $
-            next >> pushSym (sw256 $ sFromIntegral $ the state memorySize)
+            next >> pushSym (the state memorySize)
 
         -- op: GAS
         0x5a ->
@@ -2175,10 +2175,10 @@ accessUnboundedMemoryRange fees f l continue =
   if maybe False ((==) 0) (maybeLitWord l) then continue
   -- TODO: check for l .== 0 in the symbolic case as well
   else do
-    m0 <- sw256 <$> sFromIntegral <$> use (state . memorySize)
-    let m1@(S _ m1') = 32 * ceilSDiv (smax m0 (f + l)) 32
+    m0 <- use (state . memorySize)
+    let m1 = 32 * ceilSDiv (smax m0 (f + l)) 32
     burnSym (memoryCost fees m1 - memoryCost fees m0) $ do
-      assign (state . memorySize) (sFromIntegral m1')
+      assign (state . memorySize) m1
       continue
 
 accessMemoryRange
@@ -2205,7 +2205,7 @@ copyCalldataToMemory
  :: Calldata -> SymWord -> SymWord -> SymWord -> EVM ()
 copyCalldataToMemory (CalldataBuffer bf) size xOffset yOffset =
   copyBytesToMemory bf size xOffset yOffset
-copyCalldataToMemory (CalldataDynamic (b, l)) size xOffset yOffset =
+copyCalldataToMemory (CalldataDynamic (b, (S _ l))) size xOffset yOffset =
   case (maybeLitWord size, maybeLitWord xOffset, maybeLitWord yOffset) of
     (Just size', Just xOffset', Just yOffset') ->
       copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) (litWord size') (litWord xOffset') (litWord yOffset')

src/hevm/src/EVM/SymExec.hs

@@ -111,7 +111,7 @@ abstractVM typesignature concreteArgs x storagemodel calldatamodel = do
 
                         BoundedCD -> do
                            cd <- sbytes256
-                           len <- freshVar_
+                           len <- sw256 <$> freshVar_
                            return (CalldataDynamic (cd, len), len .<= 256)
            Just (name, typs) -> do symbytes <- staticCalldata name typs concreteArgs
                                    return (CalldataBuffer (StaticSymBuffer symbytes), sTrue)
@@ -340,7 +340,7 @@ showCounterexample vm maybesig = do
       SAddr caller' = view (EVM.state . EVM.caller) vm
 --  cdlen' <- num <$> getValue cdlen
   calldatainput <- case calldata' of
-    CalldataDynamic (cd, cdlen) -> do
+    CalldataDynamic (cd, (S _ cdlen)) -> do
       cdlen' <- num <$> getValue cdlen
       mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack
     CalldataBuffer (StaticSymBuffer cd) -> mapM (getValue.fromSized) cd >>= return . pack

src/hevm/src/EVM/Symbolic.hs

@@ -187,8 +187,8 @@ writeMemory' bs1 (C _ n) (C _ src) (C _ dst) bs0 =
 readMemoryWord' :: Word -> [SWord 8] -> SymWord
 readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)
 
-readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
-readMemoryWord32' (C _ i) m = fromBytes $ truncpad 4 (drop (num i) m)
+readMemoryWord32' :: Word -> [SWord 8] -> SymWord
+readMemoryWord32' (C _ i) m = sw256 $ fromBytes $ truncpad 4 (drop (num i) m)
 
 setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
 setMemoryWord' (C _ i) (S _ x) =
@@ -208,8 +208,8 @@ readSWord' (C _ i) x =
   else swordAt (num i) x
 
 -- | Operations over dynamic symbolic memory (smt list of bytes)
-readByteOrZero'' :: SWord 32 -> SList (WordN 8) -> SWord 8
-readByteOrZero'' i bs =
+readByteOrZero'' :: SymWord -> SList (WordN 8) -> SWord 8
+readByteOrZero'' (S _ i) bs =
   ite (sFromIntegral (SL.length bs) .> i + 1)
   (bs .!! (sFromIntegral i))
   (literal 0)
@@ -265,24 +265,24 @@ read32At :: SInteger -> SList (WordN 8) -> SymWord
 read32At i x = sw256 $ fromBytes $ [x .!! literal i | i <- [0..31]]
 
 -- | Although calldata can be modeled perfectly well directly as a Buffer,
--- we allow for it to take on a special form; the pair ([SWord 8], SWord 32)
+-- we allow for it to take on a special form; the pair ([SWord 8], SymWord)
 -- where the second argument is understood as the length of the list.
 -- This allows us to 'fake' dynamically sized calldata arrays in a way
 -- that has proven more efficient than `SList`.
 data Calldata
   = CalldataBuffer Buffer
-  | CalldataDynamic ([SWord 8], SWord 32)
+  | CalldataDynamic ([SWord 8], SymWord)
   deriving Show
 
 -- a whole foldable instance seems overkill, but length is always good to have!
-len :: Buffer -> SymWord --SWord 32
+len :: Buffer -> SymWord
 len (DynamicSymBuffer a) = sw256 $ sFromIntegral $ SL.length a
 len (StaticSymBuffer bs) = litWord . num $ length bs
 len (ConcreteBuffer bs) = litWord . num $ BS.length bs
 
 cdlen :: Calldata -> SymWord
 cdlen (CalldataBuffer bf) = len bf
-cdlen (CalldataDynamic (_, a)) = sw256 $ sFromIntegral a
+cdlen (CalldataDynamic (_, a)) = a
 
 grab :: Int -> Buffer -> Buffer
 grab n (StaticSymBuffer bs) = StaticSymBuffer $ take n bs
@@ -310,7 +310,7 @@ grabS n bs = case unliteral n of
 readByteOrZero :: Int -> Buffer -> SWord 8
 readByteOrZero i (StaticSymBuffer bs) = readByteOrZero' i bs
 readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs
-readByteOrZero i (DynamicSymBuffer bs) = readByteOrZero'' (literal $ num i) bs
+readByteOrZero i (DynamicSymBuffer bs) = readByteOrZero'' (litWord $ num i) bs
 
 -- pad up to 1000 bytes in the dynamic case
 sliceWithZero :: SymWord -> SymWord -> Buffer -> Buffer
@@ -343,11 +343,13 @@ readMemoryWord i bf = case (maybeLitWord i, bf) of
 
 readMemoryWord32 :: SymWord -> Buffer -> SWord 32
 readMemoryWord32 i m = case (maybeLitWord i, m) of
-  (Just i', StaticSymBuffer m') -> readMemoryWord32' i' m'
+  (Just i', StaticSymBuffer m') -> let S _ s = readMemoryWord32' i' m'
+                                   in sFromIntegral s
   (Just i', ConcreteBuffer m') -> num $ Concrete.readMemoryWord32 i' m'
   (_, DynamicSymBuffer m') -> case truncpad' 4 $ dropS i m' of
     ConcreteBuffer s -> literal $ num $ Concrete.readMemoryWord32 0 s
-    StaticSymBuffer s -> readMemoryWord32' 0 s
+    StaticSymBuffer s -> let S _ s' = readMemoryWord32' 0 s
+                         in sFromIntegral s'
     DynamicSymBuffer s -> fromBytes [s .!! literal k | k <- [0..3]]
 
 
@@ -369,7 +371,7 @@ setMemoryByte i x m = case (maybeLitWord i, m) of
 readSWord :: SymWord -> Buffer -> SymWord
 readSWord i bf = case (maybeLitWord i, bf) of
   (Just i', StaticSymBuffer x) -> readSWord' i' x
-  (Just i', ConcreteBuffer x) -> num $ Concrete.readMemoryWord i' x
+  (Just i', ConcreteBuffer x) -> litWord $ Concrete.readBlobWord i' x
   _  -> readSWord'' i (dynamize bf)
 
 
@@ -381,9 +383,9 @@ select' xs err ind = walk xs ind err
 -- Generates a ridiculously large set of constraints (roughly 25k) when
 -- the index is symbolic, but it still seems (kind of) manageable
 -- for the solvers.
-readStaticWordWithBound :: SWord 32 -> ([SWord 8], SWord 32) -> SymWord
-readStaticWordWithBound ind (xs, bound) =
-  case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
+readStaticWordWithBound :: SymWord -> ([SWord 8], SymWord) -> SymWord
+readStaticWordWithBound (S _ ind) (xs, S _ bound) =
+  case (num <$> unliteral ind, num <$> unliteral bound) of
     (Just i, Just b) ->
       let bs = truncpad 32 $ drop i (take b xs)
       in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)