Merge pull request #424 from ethereum/better-simplifications

Fixing up BufLength, the use of nubOrd, and adding one more PLT rule

CHANGELOG.md

@@ -7,6 +7,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Added
 - New solc-specific simplification rules that should make the final Props a lot more readable
+- Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
+  and further solc-specific simplifications of Expr
 
 ## [0.52.0] - 2023-10-26
 

hevm.cabal

@@ -286,7 +286,8 @@ common test-base
     optics-extra,
     witch,
     unliftio-core,
-    exceptions
+    exceptions,
+    MissingH
 
 library test-utils
   import:

src/EVM/Expr.hs

@@ -421,7 +421,7 @@ bufLengthEnv env useEnv buf = go (Lit 0) buf
   where
     go :: Expr EWord -> Expr Buf -> Expr EWord
     go l (ConcreteBuf b) = EVM.Expr.max l (Lit (unsafeInto . BS.length $ b))
-    go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b))
+    go l (AbstractBuf b) = EVM.Expr.max l (BufLength (AbstractBuf b))
     go l (WriteWord idx _ b) = go (EVM.Expr.max l (add idx (Lit 32))) b
     go l (WriteByte idx _ b) = go (EVM.Expr.max l (add idx (Lit 1))) b
     go l (CopySlice _ dstOffset size _ dst) = go (EVM.Expr.max l (add dstOffset size)) dst
@@ -946,9 +946,7 @@ simplify e = if (mapExpr go e == e)
     go (EVM.Types.Not (EVM.Types.Not a)) = a
 
     -- Some trivial min / max eliminations
-    go (Max a b) = case (a, b) of
-                    (Lit 0, _) -> b
-                    _ -> EVM.Expr.max a b
+    go (Max a b) = EVM.Expr.max a b
     go (Min a b) = case (a, b) of
                      (Lit 0, _) -> Lit 0
                      _ -> EVM.Expr.min a b
@@ -1012,6 +1010,8 @@ simplifyProp prop =
     go (PLEq (Lit l) (Lit r)) = PBool (l <= r)
     go (PLEq a (Max b _)) | a == b = PBool True
     go (PLEq a (Max _ b)) | a == b = PBool True
+    go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
+    go (PLT (Lit 0) (Eq a b)) = PEq a b
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)
@@ -1086,7 +1086,7 @@ flattenProps (a:ax) = case a of
 
 -- removes redundant (constant True/False) props
 remRedundantProps :: [Prop] -> [Prop]
-remRedundantProps p = collapseFalse . filter (\x -> x /= PBool True) . nubOrd $ p
+remRedundantProps p = nubOrd $ collapseFalse . filter (\x -> x /= PBool True) $ p
   where
     collapseFalse ps = if isJust $ find (== PBool False) ps then [PBool False] else ps
 
@@ -1285,6 +1285,8 @@ min :: Expr EWord -> Expr EWord -> Expr EWord
 min x y = normArgs Min Prelude.min x y
 
 max :: Expr EWord -> Expr EWord -> Expr EWord
+max (Lit 0) y = y
+max x (Lit 0) = x
 max x y = normArgs Max Prelude.max x y
 
 numBranches :: Expr End -> Int

src/EVM/Types.hs

@@ -479,17 +479,30 @@ instance Ord Prop where
   PBool a <= PBool b = a <= b
   PEq (a :: Expr x) (b :: Expr x) <= PEq (c :: Expr y) (d :: Expr y)
     = case eqT @x @y of
-       Just Refl -> a <= c && b <= d
-       Nothing -> False
-  PLT a b <= PLT c d = a <= c && b <= d
-  PGT a b <= PGT c d = a <= c && b <= d
-  PGEq a b <= PGEq c d = a <= c && b <= d
-  PLEq a b <= PLEq c d = a <= c && b <= d
+       Just Refl -> a <= c || b <= d
+       Nothing -> toNum a <= toNum c
+  PLT a b <= PLT c d = a <= c || b <= d
+  PGT a b <= PGT c d = a <= c || b <= d
+  PGEq a b <= PGEq c d = a <= c || b <= d
+  PLEq a b <= PLEq c d = a <= c || b <= d
   PNeg a <= PNeg b = a <= b
-  PAnd a b <= PAnd c d = a <= c && b <= d
-  POr a b <= POr c d = a <= c && b <= d
-  PImpl a b <= PImpl c d = a <= c && b <= d
-  _ <= _ = False
+  PAnd a b <= PAnd c d = a <= c || b <= d
+  POr a b <= POr c d = a <= c || b <= d
+  PImpl a b <= PImpl c d = a <= c || b <= d
+  a <= b = asNum a <= asNum b
+    where
+      asNum :: Prop -> Int
+      asNum (PBool {}) = 0
+      asNum (PEq   {}) = 1
+      asNum (PLT   {}) = 2
+      asNum (PGT   {}) = 3
+      asNum (PGEq  {}) = 4
+      asNum (PLEq  {}) = 5
+      asNum (PNeg  {}) = 6
+      asNum (PAnd  {}) = 7
+      asNum (POr   {}) = 8
+      asNum (PImpl {}) = 9
+
 
 
 isPBool :: Prop -> Bool

test/test.hs

@@ -20,6 +20,7 @@ import Data.Binary.Get (runGetOrFail)
 import Data.DoubleWord
 import Data.Either
 import Data.List qualified as List
+import Data.List.Utils as DLU
 import Data.Map.Strict qualified as Map
 import Data.Maybe
 import Data.String.Here
@@ -44,6 +45,7 @@ import Test.Tasty.ExpectedFailure
 import Text.RE.TDFA.String
 import Text.RE.Replace
 import Witch (unsafeInto, into)
+import Data.Containers.ListUtils (nubOrd)
 
 import Optics.Core hiding (pre, re, elements)
 import Optics.State
@@ -316,6 +318,12 @@ tests = testGroup "hevm"
         let e = ReadByte (Lit 0x0) (WriteWord (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd) (Lit 0x0) (ConcreteBuf "\255\255\255\255"))
         b <- checkEquiv e (Expr.simplify e)
         assertBoolM "Simplifier failed" b
+    , test "simp-max-buflength" $ do
+      let simp = Expr.simplify $ Max (Lit 0) (BufLength (AbstractBuf "txdata"))
+      assertEqualM "max-buflength rules" simp $ BufLength (AbstractBuf "txdata")
+    , test "simp-PLT-max" $ do
+      let simp = Expr.simplifyProp $ PLT (Max (Lit 5) (BufLength (AbstractBuf "txdata"))) (Lit 99)
+      assertEqualM "max-buflength rules" simp $ PLT (BufLength (AbstractBuf "txdata")) (Lit 99)
     , test "simp-assoc-add1" $ do
       let simp = Expr.simplify $        Add (Var "a") (Add (Var "b") (Var "c"))
       assertEqualM "assoc rules" simp $ Add (Add (Var "a") (Var "b")) (Var "c")
@@ -2729,6 +2737,25 @@ tests = testGroup "hevm"
         a = successGen [PImpl (PBool False) (PEq (Var "abc") (Var "bcd"))]
         b = Expr.simplify a
       assertEqualM "Must simplify down" (successGen []) b
+    , test "propSimp-no-duplicate1" $ do
+      let a = [PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)), PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x63) (Var "arg2"),PEq (Lit 0x539) (Var "arg1"),PEq TxValue (Lit 0x0),PEq (IsZero (Eq (Lit 0x63) (Var "arg2"))) (Lit 0x0)]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
+    , test "propSimp-no-duplicate2" $ do
+      let a = [PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x539) (Var "arg1"),PNeg (PEq (Lit 0x539) (Var "arg1")),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0)),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "must not duplicate" (length simp) (length $ DLU.uniq simp)
+    , test "full-order-prop1" $ do
+      let a = [PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x539) (Var "arg1"),PNeg (PEq (Lit 0x539) (Var "arg1")),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0)),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
+    , test "full-order-prop2" $ do
+      let a =[PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x63) (Var "arg2"),PEq (Lit 0x539) (Var "arg1"),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x63) (Var "arg2"))) (Lit 0x0),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
   ]
   , testGroup "equivalence-checking"
     [