Allow dealing with abi.encodeWithSelector

CHANGELOG.md

@@ -5,6 +5,10 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## Added
+- JoinBytes simplification rule
+- New simplification rule to help deal with abi.encodeWithSelector
+
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value
   This should improve issues when "Unexpected Symbolic Arguments to Opcode" was

src/EVM/Expr.hs

@@ -993,6 +993,20 @@ simplify e = if (mapExpr go e == e)
             where simplifiedBuf = BS.take (unsafeInto (n+sz)) buf
     go (CopySlice a b c d f) = copySlice a b c d f
 
+    go (JoinBytes (LitByte a0)  (LitByte a1)  (LitByte a2)  (LitByte a3)
+      (LitByte a4)  (LitByte a5)  (LitByte a6)  (LitByte a7)
+      (LitByte a8)  (LitByte a9)  (LitByte a10) (LitByte a11)
+      (LitByte a12) (LitByte a13) (LitByte a14) (LitByte a15)
+      (LitByte a16) (LitByte a17) (LitByte a18) (LitByte a19)
+      (LitByte a20) (LitByte a21) (LitByte a22) (LitByte a23)
+      (LitByte a24) (LitByte a25) (LitByte a26) (LitByte a27)
+      (LitByte a28) (LitByte a29) (LitByte a30) (LitByte a31)) =
+        let b =  map fromIntegral [a0, a1, a2, a3 ,a4, a5, a6, a7
+                                  ,a8, a9, a10, a11 ,a12, a13, a14, a15
+                                  ,a16, a17, a18, a19 ,a20, a21, a22, a23
+                                  ,a24, a25, a26, a27 ,a28, a29, a30, a31]
+        in Lit (constructWord256 b)
+
     go (IndexWord a b) = indexWord a b
 
     -- LT
@@ -1418,6 +1432,11 @@ indexWord i@(Lit idx) e@(And (Lit mask) w)
     fullWordMask = (2 ^ (256 :: W256)) - 1
     unmaskedBytes = fromIntegral $ (countLeadingZeros mask) `Prelude.div` 8
     isByteAligned m = (countLeadingZeros m) `Prelude.mod` 8 == 0
+-- This pattern happens in Solidity for function selectors. Since Lit 0xfff... (28 bytes of 0xff)
+-- is masking the function selector, it can be simplified to just the function selector bytes. Remember,
+-- indexWord takes the MSB i-th byte when called with (indexWord i).
+indexWord (Lit a) (Or funSel (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _)) | a < 4 =
+  indexWord (Lit a) funSel
 indexWord (Lit idx) (Lit w)
   | idx <= 31 = LitByte . fromIntegral $ shiftR w (248 - unsafeInto idx * 8)
   | otherwise = LitByte 0

src/EVM/Format.hs

@@ -479,7 +479,7 @@ formatPartial = \case
   JumpIntoSymbolicCode pc idx -> "Encountered a jump into a potentially symbolic code region while executing initcode. pc: " <> pack (show pc) <> " jump dst: " <> pack (show idx)
 
 formatSomeExpr :: SomeExpr -> Text
-formatSomeExpr (SomeExpr e) = formatExpr e
+formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e
 
 formatExpr :: Expr a -> Text
 formatExpr = go

src/EVM/Types.hs

@@ -1329,6 +1329,20 @@ bssToBs :: ByteStringS -> ByteString
 bssToBs (ByteStringS bs) = bs
 
 
+-- Function to construct a W256 from a list of 32 Word8 values
+constructWord256 :: [Word8] -> W256
+constructWord256 bytes
+    | length bytes == 32 = W256 (Word256 (Word128 w256hi w256m1) (Word128 w256m0 w256lo))
+    | otherwise = internalError "List must contain exactly 32 Word8 values"
+  where
+    w256hi = word8sToWord64 (take 8 bytes)
+    w256m1 = word8sToWord64 (take 8 (drop 8 bytes))
+    w256m0 = word8sToWord64 (take 8 (drop 16 bytes))
+    w256lo = word8sToWord64 (take 8 (drop 24 bytes))
+    word8sToWord64 :: [Word8] -> Word64
+    word8sToWord64 = foldl (\acc byte -> (acc `shiftL` 8) .|. fromIntegral byte) 0
+
+
 -- Keccak hashing ----------------------------------------------------------------------------------
 
 

test/test.hs

@@ -702,6 +702,11 @@ tests = testGroup "hevm"
     , testProperty "simplifyProp-equivalence-sym" $ \(p) -> prop $ do
         let simplified = Expr.simplifyProp p
         checkEquivPropAndLHS p simplified
+    , testProperty "simplify-joinbytes" $ \(SymbolicJoinBytes exprList) -> prop $ do
+        let x = joinBytesFromList exprList
+        let simplified = Expr.simplify x
+        y <- checkEquiv x simplified
+        assertBoolM "Must be equal" y
     , testProperty "simpProp-equivalence-sym-Prop" $ \(ps :: [Prop]) -> prop $ do
         let simplified = pand (Expr.simplifyProps ps)
         checkEquivPropAndLHS (pand ps) simplified
@@ -1306,6 +1311,22 @@ tests = testGroup "hevm"
         r <- allBranchesFail c Nothing
         assertBoolM "all branches must fail" (isRight r)
       ,
+      test "cheatcode-with-selector" $ do
+        Just c <- solcRuntime "C"
+            [i|
+            contract C {
+            function prove_warp_symbolic(uint128 jump) public {
+                    uint pre = block.timestamp;
+                    address hevm = 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D;
+                    (bool success, ) = hevm.call(abi.encodeWithSelector(bytes4(keccak256("warp(uint256)")), block.timestamp+jump));
+                    require(success, "Call to hevm.warp failed");
+                    assert(block.timestamp == pre + jump);
+                }
+            }
+            |]
+        Right e <- reachableUserAsserts c Nothing
+        assertBoolM "The expression should not contain Partial." $ Prelude.not $ Expr.containsNode isPartial e
+      ,
       test "call ffi when disabled" $ do
         Just c <- solcRuntime "C"
             [i|
@@ -4016,6 +4037,23 @@ instance Arbitrary (Expr EWord) where
 instance Arbitrary (Expr Byte) where
   arbitrary = sized genByte
 
+newtype SymbolicJoinBytes = SymbolicJoinBytes [Expr Byte]
+  deriving (Eq, Show)
+
+instance Arbitrary SymbolicJoinBytes where
+  arbitrary = liftM SymbolicJoinBytes $ replicateM 32 arbitrary
+
+joinBytesFromList :: [Expr Byte] -> Expr EWord
+joinBytesFromList [a0, a1, a2, a3, a4, a5, a6, a7,
+                   a8, a9, a10, a11, a12, a13, a14, a15,
+                   a16, a17, a18, a19, a20, a21, a22, a23,
+                   a24, a25, a26, a27, a28, a29, a30, a31] =
+  JoinBytes a0 a1 a2 a3 a4 a5 a6 a7
+            a8 a9 a10 a11 a12 a13 a14 a15
+            a16 a17 a18 a19 a20 a21 a22 a23
+            a24 a25 a26 a27 a28 a29 a30 a31
+joinBytesFromList _ = internalError "List must contain exactly 32 elements"
+
 instance Arbitrary (Expr Buf) where
   arbitrary = sized defaultBuf
 
@@ -4303,6 +4341,7 @@ genWord litFreq 0 = frequency
       --, liftM2 SelfBalance arbitrary arbitrary
       --, liftM2 Gas arbitrary arbitrary
       , fmap Lit arbitrary
+      , fmap joinBytesFromList $ replicateM 32 arbitrary
       , fmap Var (genName "word")
       ]
     )