Add missing simplifications, add tests for all concretizations

CHANGELOG.md

@@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - State merging via speculative execution of both branches of a JUMPI, joining the
   resulting states whenever possible. Amount of speculative execution is
   controlled via `merge-max-budget`
+- Missing simplifications for Eq, Mod, SMod, XOR, SHL, SHR, Or and SHA256
 
 ## Changed
 - Simplifier now rewrites `Mul(-1, x)` and `~x + 1` to `Sub(0, x)`

src/EVM/Expr.hs

@@ -212,6 +212,7 @@ peq (Lit x) (Lit y) = PBool (x == y)
 peq (LitAddr x) (LitAddr y) = PBool (x == y)
 peq (LitByte x) (LitByte y) = PBool (x == y)
 peq (ConcreteBuf x) (ConcreteBuf y) = PBool (x == y)
+peq (ConcreteStore x) (ConcreteStore y) = PBool (x == y)
 peq a b
   | a == b = PBool True
   | otherwise = let args = sort [a, b]
@@ -1107,6 +1108,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
 
     -- LT
     go (EVM.Types.LT _ (Lit 0)) = Lit 0
+    go (EVM.Types.LT (Lit a) _) | a == maxLit = Lit 0
     go (EVM.Types.LT a (Lit 1)) = iszero a
     go (EVM.Types.LT a b) = lt a b
 
@@ -1125,9 +1127,14 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     -- literal addresses
     go (WAddr (LitAddr a)) = Lit $ into a
 
+    -- SHA256
+    go (SHA256 (ConcreteBuf bs)) = Lit (sha256' bs)
+
     -- Mod
     go (Mod _ (Lit 0)) = Lit 0
+    go (Mod _ (Lit 1)) = Lit 0
     go (SMod _ (Lit 0)) = Lit 0
+    go (SMod _ (Lit 1)) = Lit 0
     go (Mod a b) | a == b = Lit 0
     go (SMod a b) | a == b = Lit 0
     go (Mod (Lit 0) _) = Lit 0
@@ -1226,6 +1233,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | otherwise = sub a b
 
     -- XOR normalization
+    go (Xor a b) | a == b = Lit 0
     go (Xor (Lit a) b) | a == maxLit = EVM.Expr.not b
     go (Xor a  b) = EVM.Expr.xor a b
 
@@ -1237,10 +1245,12 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     go (EqByte a b) = eqByte a b
 
     -- SHL / SHR / SAR
+    go (SHL (Lit a) _) | a >= 256 = Lit 0
     go (SHL a v)
       | a == (Lit 0) = v
       | v == (Lit 0) = v
       | otherwise = shl a v
+    go (SHR (Lit a) _) | a >= 256 = Lit 0
     go (SHR a v)
       | a == (Lit 0) = v
       | v == (Lit 0) = v
@@ -1264,6 +1274,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | a == b = a
       | a == (Lit 0) = b
       | b == (Lit 0) = a
+      | a == (Lit maxLit) || b == (Lit maxLit) = Lit maxLit
       | otherwise = EVM.Expr.or a b
 
 

src/EVM/Types.hs

@@ -19,7 +19,7 @@ import Control.Arrow ((>>>))
 import Control.Monad (mzero)
 import Control.Monad.ST (ST, RealWorld)
 import Control.Monad.State.Strict (StateT)
-import Crypto.Hash (hash, Keccak_256, Digest)
+import Crypto.Hash (hash, Keccak_256, SHA256, Digest)
 import Data.Aeson qualified as JSON
 import Data.Aeson.Types qualified as JSON
 import Data.Bifunctor (first)
@@ -1543,6 +1543,14 @@ keccak buf = Keccak buf
 keccak' :: ByteString -> W256
 keccak' = keccakBytes >>> BS.take 32 >>> word
 
+sha256' :: ByteString -> W256
+sha256' = sha256Bytes >>> BS.take 32 >>> word
+
+sha256Bytes :: ByteString -> ByteString
+sha256Bytes =
+  (hash :: ByteString -> Digest SHA256)
+    >>> BA.convert
+
 abiKeccak :: ByteString -> FunctionSelector
 abiKeccak =
   keccakBytes