From 3543bd90fe0b7a6978422ede6b2420b5077e77b1 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 26 Aug 2024 23:42:42 +0200 Subject: [PATCH] Use simplifying constructor for PEq The idea is to always normalize Prop equalities such that concrete values appear on the left-hand-side. This follows the example of the helper functions for expressions, that also immediately simplify if they get concrete arguments, and normalize arguments for commutative operations. --- src/EVM.hs | 2 +- src/EVM/Expr.hs | 16 ++++++++-------- src/EVM/Keccak.hs | 6 +++--- src/EVM/SMT.hs | 6 +++--- src/EVM/SymExec.hs | 10 +++++----- src/EVM/Traversals.hs | 4 ++-- src/EVM/Types.hs | 12 ++++++++++-- 7 files changed, 32 insertions(+), 24 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index d1cdf5381..cbc95ff65 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1604,7 +1604,7 @@ cheatActions = Map.fromList , action "assume(bool)" $ \sig _ _ input -> case decodeStaticArgs 0 1 input of - [c] -> modifying #constraints ((:) (PEq c (Lit 1))) + [c] -> modifying #constraints ((:) (mkPEq (Lit 1) c)) _ -> vmError (BadCheatCode sig) , action "roll(uint256)" $ diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 896fb919b..182706a29 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -1214,14 +1214,14 @@ simplifyProp prop = go (PLEq a (Max _ b)) | a == b = PBool True go (PLEq (Sub a b) c) | a == c = PLEq b a go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c) - go (PLT (Lit 0) (Eq a b)) = PEq a b + go (PLT (Lit 0) (Eq a b)) = mkPEq a b -- negations go (PNeg (PBool b)) = PBool (Prelude.not b) go (PNeg (PNeg a)) = a -- solc specific stuff - go (PEq (IsZero (IsZero (Eq a b))) (Lit 0)) = PNeg (PEq a b) + go (PEq (IsZero (IsZero (Eq a b))) (Lit 0)) = PNeg (mkPEq a b) -- iszero(a) -> (a == 0) -- iszero(iszero(a))) -> ~(a == 0) -> a > 0 @@ -1232,7 +1232,7 @@ simplifyProp prop = -- iszero(a) -> (a == 0) -- iszero(a) == 0 -> ~(a == 0) -- ~(iszero(a) == 0) -> ~~(a == 0) -> a == 0 - go (PNeg (PEq (IsZero a) (Lit 0))) = PEq a (Lit 0) + go (PNeg (PEq (IsZero a) (Lit 0))) = mkPEq (Lit 0) a -- a < b == 0 -> ~(a < b) -- ~(a < b == 0) -> ~~(a < b) -> a < b @@ -1256,16 +1256,16 @@ simplifyProp prop = go (PImpl (PBool False) _) = PBool True -- Double negation - go (PEq (IsZero (Eq a b)) (Lit 0)) = PEq a b + go (PEq (IsZero (Eq a b)) (Lit 0)) = mkPEq a b go (PEq (IsZero (LT a b)) (Lit 0)) = PLT a b go (PEq (IsZero (GT a b)) (Lit 0)) = PGT a b go (PEq (IsZero (LEq a b)) (Lit 0)) = PLEq a b go (PEq (IsZero (GEq a b)) (Lit 0)) = PGEq a b -- Eq - go (PEq (Eq a b) (Lit 0)) = PNeg (PEq a b) - go (PEq (Eq a b) (Lit 1)) = PEq a b - go (PEq (Sub a b) (Lit 0)) = PEq a b + go (PEq (Eq a b) (Lit 0)) = PNeg (mkPEq a b) + go (PEq (Eq a b) (Lit 1)) = mkPEq a b + go (PEq (Sub a b) (Lit 0)) = mkPEq a b go (PEq (LT a b) (Lit 0)) = PLEq b a go (PEq (Lit l) (Lit r)) = PBool (l == r) go o@(PEq l r) @@ -1282,7 +1282,7 @@ simplifyProp prop = simpInnerExpr (PGEq a b) = simpInnerExpr (PLEq b a) simpInnerExpr (PGT a b) = simpInnerExpr (PLT b a) -- simplifies the inner expression - simpInnerExpr (PEq a b) = PEq (simplify a) (simplify b) + simpInnerExpr (PEq a b) = mkPEq (simplify a) (simplify b) simpInnerExpr (PLT a b) = PLT (simplify a) (simplify b) simpInnerExpr (PLEq a b) = PLEq (simplify a) (simplify b) simpInnerExpr (PNeg a) = PNeg (simpInnerExpr a) diff --git a/src/EVM/Keccak.hs b/src/EVM/Keccak.hs index fe479c64a..e27221dfa 100644 --- a/src/EVM/Keccak.hs +++ b/src/EVM/Keccak.hs @@ -56,12 +56,12 @@ minProp k@(Keccak _) = PGT k (Lit 256) minProp _ = internalError "expected keccak expression" concVal :: Expr EWord -> Prop -concVal k@(Keccak (ConcreteBuf bs)) = PEq (Lit (keccak' bs)) k +concVal k@(Keccak (ConcreteBuf bs)) = mkPEq (Lit (keccak' bs)) k concVal _ = PBool True injProp :: (Expr EWord, Expr EWord) -> Prop injProp (k1@(Keccak b1), k2@(Keccak b2)) = - POr ((b1 .== b2) .&& (bufLength b1 .== bufLength b2)) (PNeg (PEq k1 k2)) + POr ((b1 .== b2) .&& (bufLength b1 .== bufLength b2)) (PNeg (mkPEq k1 k2)) injProp _ = internalError "expected keccak expression" @@ -94,7 +94,7 @@ compute = \case e@(Keccak buf) -> do let b = simplify buf case keccak b of - lit@(Lit _) -> [PEq e lit] + lit@(Lit _) -> [mkPEq lit e] _ -> [] _ -> [] diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index 36a20c18c..e13832fe6 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -278,7 +278,7 @@ assertPropsNoSimp config psPreConc = abstProps = map toProp (Map.toList abstExprToInt) where toProp :: (Expr EWord, Int) -> Prop - toProp (e, num) = PEq e (Var (TS.pack ("abst_" ++ (show num)))) + toProp (e, num) = mkPEq e (Var (TS.pack ("abst_" ++ (show num)))) -- Props storing info that need declaration(s) toDeclarePs = ps <> keccAssump <> keccComp @@ -404,11 +404,11 @@ assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop] assertReads props benv senv = concatMap assertRead allReads where assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop] - assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))] + assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (mkPEq (ReadWord idx buf) (Lit 0))] assertRead (idx, Lit sz, buf) = fmap -- TODO: unsafeInto instead fromIntegral here makes symbolic tests fail - (PImpl (PGEq idx (bufLength buf)) . PEq (ReadByte idx buf) . LitByte . fromIntegral) + (PImpl (PGEq idx (bufLength buf)) . mkPEq (ReadByte idx buf) . LitByte . fromIntegral) [(0::Int)..unsafeInto sz-1] assertRead (_, _, _) = internalError "Cannot generate assertions for accesses of symbolic size" diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index efe3abbc8..da9392a21 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -101,7 +101,7 @@ extractCex (Cex c) = Just c extractCex _ = Nothing bool :: Expr EWord -> Prop -bool e = POr (PEq e (Lit 1)) (PEq e (Lit 0)) +bool e = POr (mkPEq (Lit 1) e) (mkPEq (Lit 0) e) -- | Abstract calldata argument generation symAbiArg :: Text -> AbiType -> CalldataFragment @@ -420,7 +420,7 @@ getExpr solvers c signature' concreteArgs opts = do checkAssertions :: [Word256] -> Postcondition s checkAssertions errs _ = \case Failure _ _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs) - Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs) + Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . mkPEq b . ConcreteBuf . panicMsg) errs) _ -> PBool True -- | By default hevm only checks for user-defined assertions @@ -483,7 +483,7 @@ flattenExpr = go [] where go :: [Prop] -> Expr End -> [Expr End] go pcs = \case - ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f + ITE c t f -> go (PNeg ((mkPEq (Lit 0) c)) : pcs) t <> go (mkPEq (Lit 0) c : pcs) f Success ps trace msg store -> [Success (nubOrd $ ps <> pcs) trace msg store] Failure ps trace e -> [Failure (nubOrd $ ps <> pcs) trace e] Partial ps trace p -> [Partial (nubOrd $ ps <> pcs) trace p] @@ -514,8 +514,8 @@ reachable solvers e = do go conf pcs = \case ITE c t f -> do (tres, fres) <- concurrently - (go conf (PEq (Lit 1) c : pcs) t) - (go conf (PEq (Lit 0) c : pcs) f) + (go conf (mkPEq (Lit 1) c : pcs) t) + (go conf (mkPEq (Lit 0) c : pcs) f) let subexpr = case (snd tres, snd fres) of (Just t', Just f') -> Just $ ITE c t' f' (Just t', Nothing) -> Just t' diff --git a/src/EVM/Traversals.hs b/src/EVM/Traversals.hs index 4b499e7c4..5b0bbe3bc 100644 --- a/src/EVM/Traversals.hs +++ b/src/EVM/Traversals.hs @@ -211,7 +211,7 @@ foldExpr f acc expr = acc <> (go expr) mapProp :: (forall a . Expr a -> Expr a) -> Prop -> Prop mapProp f = \case PBool b -> PBool b - PEq a b -> PEq (mapExpr f (f a)) (mapExpr f (f b)) + PEq a b -> mkPEq (mapExpr f (f a)) (mapExpr f (f b)) PLT a b -> PLT (mapExpr f (f a)) (mapExpr f (f b)) PGT a b -> PGT (mapExpr f (f a)) (mapExpr f (f b)) PLEq a b -> PLEq (mapExpr f (f a)) (mapExpr f (f b)) @@ -612,7 +612,7 @@ mapPropM f = \case PEq a b -> do a' <- mapExprM f a b' <- mapExprM f b - pure $ PEq a' b' + pure $ mkPEq a' b' PLT a b -> do a' <- mapExprM f a b' <- mapExprM f b diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index d419b4607..7f500b847 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -432,6 +432,14 @@ data Prop where PBool :: Bool -> Prop deriving instance (Show Prop) +mkPEq :: (Typeable a) => Expr a -> Expr a -> Prop +mkPEq (Lit x) (Lit y) = PBool (x == y) +mkPEq a@(Lit _) b = PEq a b +mkPEq a b@(Lit _) = PEq b a -- we always put concrete values on LHS +mkPEq a b + | a == b = PBool True + | otherwise = PEq a b + infixr 3 .&& (.&&) :: Prop -> Prop -> Prop x .&& y = PAnd x y @@ -452,9 +460,9 @@ x .>= y = PGEq x y infix 4 .==, ./= (.==) :: (Typeable a) => Expr a -> Expr a -> Prop -x .== y = PEq x y +x .== y = mkPEq x y (./=) :: (Typeable a) => Expr a -> Expr a -> Prop -x ./= y = PNeg (PEq x y) +x ./= y = PNeg (mkPEq x y) pand :: [Prop] -> Prop pand = foldl' PAnd (PBool True)