From 2a8c2f4a9df75edc91702b8ea737bc07bc0356f6 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 8 Nov 2023 15:42:01 +0100 Subject: [PATCH 1/2] Fixing up BufLength, the use of nubOrd, and adding one more PLT rule --- CHANGELOG.md | 2 ++ hevm.cabal | 3 ++- src/EVM/Expr.hs | 12 +++++++----- src/EVM/Types.hs | 33 +++++++++++++++++++++++---------- test/test.hs | 24 ++++++++++++++++++++++++ 5 files changed, 58 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fca9b5bc..9c119a220 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/hevm.cabal b/hevm.cabal index f0d617f04..feba37329 100644 --- a/hevm.cabal +++ b/hevm.cabal @@ -286,7 +286,8 @@ common test-base optics-extra, witch, unliftio-core, - exceptions + exceptions, + MissingH library test-utils import: diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index bcb2d5877..129b43011 100644 --- a/src/EVM/Expr.hs +++ b/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 diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index 13296066e..14a6e5eff 100644 --- a/src/EVM/Types.hs +++ b/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 diff --git a/test/test.hs b/test/test.hs index c7d0b33bb..e549a5d96 100644 --- a/test/test.hs +++ b/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,22 @@ 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) + , 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" (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 "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp) ] , testGroup "equivalence-checking" [ From d191847b6271e4713f53df8643fde2aab332ac87 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 9 Nov 2023 12:54:24 +0100 Subject: [PATCH 2/2] A bit more elements to the tests --- test/test.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/test.hs b/test/test.hs index e549a5d96..8296072d6 100644 --- a/test/test.hs +++ b/test/test.hs @@ -2741,9 +2741,11 @@ tests = testGroup "hevm" 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))] @@ -2752,6 +2754,7 @@ tests = testGroup "hevm" , 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"