Merge pull request #163 from arcz/fix-regressions

Fix SAR arithmetic overflow and copySlice regressions

Author: d-xo

CHANGELOG.md

@@ -5,9 +5,16 @@ 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).
 
+## Unreleased
+
+### Fixed
+
+- Arithmetic overflow in concrete `SAR` edge case
+- Unnecessary application of `CopySlice` in concrete edge case
+
 ## [0.50.1] - 2022-12-29
 
-## Fixed
+### Fixed
 
 - `hevm exec` no longer fails with `hevm: No match in record selector smttimeout`
 - the `gas`, `gaslimit`, `priorityfee`, and `gasprice` cli options are now respected

src/EVM/Expr.hs

@@ -181,8 +181,12 @@ shr = op2
 
 sar :: Expr EWord -> Expr EWord -> Expr EWord
 sar = op2 SAR (\x y ->
-  let asSigned = (fromIntegral y) :: Int256
-  in fromIntegral $ shiftR asSigned (fromIntegral x))
+  let msb = testBit y 255
+      asSigned = fromIntegral y :: Int256
+  in if x > 256 then
+       if msb then maxBound else 0
+     else
+       fromIntegral $ shiftR asSigned (fromIntegral x))
 
 -- ** Bufs ** --------------------------------------------------------------------------------------
 
@@ -319,7 +323,6 @@ copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e
 
 copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e@(ConcreteBuf dst)
   | dstOffset < maxBytes
-  , srcOffset < maxBytes
   , size < maxBytes =
       let hd = padRight (num dstOffset) $ BS.take (num dstOffset) dst
           sl = if srcOffset > num (BS.length src)

test/BlockchainTests.hs

@@ -112,13 +112,7 @@ ciIgnoredFiles =
 
 commonProblematicTests :: Map String (TestTree -> TestTree)
 commonProblematicTests = Map.fromList
-  [ ("twoOps_d0g0v0_London", expectFailBecause "TODO: regression")
-  , ("sar_2^256-1_0_d0g0v0_London", expectFailBecause "TODO: regression")
-  , ("shiftCombinations_d0g0v0_London", expectFailBecause "TODO: regression")
-  , ("shiftSignedCombinations_d0g0v0_London", expectFailBecause "TODO: regression")
-  , ("bufferSrcOffset_d14g0v0_London", expectFailBecause "TODO: regression")
-  , ("bufferSrcOffset_d38g0v0_London", expectFailBecause "TODO: regression")
-  , ("loopMul_d0g0v0_London", ignoreTestBecause "hevm is too slow")
+  [ ("loopMul_d0g0v0_London", ignoreTestBecause "hevm is too slow")
   , ("loopMul_d1g0v0_London", ignoreTestBecause "hevm is too slow")
   , ("loopMul_d2g0v0_London", ignoreTestBecause "hevm is too slow")
   , ("CALLBlake2f_MaxRounds_d0g0v0_London", ignoreTestBecause "very slow, bypasses timeout due time spent in FFI")