Skip to content

Commit d6e6e05

Browse files
blishkoblishko
authored
Merge pull request #929 from argotorg/canonical-comparison-simplifications
Expr: Canonicalize transformations
2 parents 0efc157 + e8bb8bf commit d6e6e05

File tree

1 file changed

+81
-90
lines changed

1 file changed

+81
-90
lines changed

‎src/EVM/Expr.hs‎

Lines changed: 81 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -1049,6 +1049,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
10491049
go (IsZero (IsZero (IsZero a))) = iszero a
10501050
go (IsZero (IsZero (LT x y))) = lt x y
10511051
go (IsZero (IsZero (Eq x y))) = eq x y
1052+
go (IsZero (IsZero a)) = lt (Lit 0) a
10521053
go (IsZero (Xor x y)) = eq x y
10531054
go (IsZero a) = iszero a
10541055

@@ -1062,6 +1063,47 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
10621063
| a == b = Lit 1
10631064
| otherwise = eq a b
10641065

1066+
-- COMPARISONS
1067+
-- First special cases
1068+
1069+
-- we write at least 32, so if x <= 32, it's FALSE
1070+
go o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit x))
1071+
| x <= 32 = Lit 0
1072+
| otherwise = o
1073+
-- we write at least 32, so if x < 32, it's TRUE
1074+
go o@(EVM.Types.LT (Lit x) (BufLength (WriteWord {})))
1075+
| x < 32 = Lit 1
1076+
| otherwise = o
1077+
1078+
-- If a >= b then the value of the `Max` expression can never be < b
1079+
go o@(LT (Max (Lit a) _) (Lit b))
1080+
| a >= b = Lit 0
1081+
| otherwise = o
1082+
go o@(SLT (Sub (Max (Lit a) _) (Lit b)) (Lit c))
1083+
= let sa, sb, sc :: Int256
1084+
sa = fromIntegral a
1085+
sb = fromIntegral b
1086+
sc = fromIntegral c
1087+
in if sa >= sb && sa - sb >= sc
1088+
then Lit 0
1089+
else o
1090+
1091+
-- normalize all comparisons in terms of (S)LT
1092+
go (EVM.Types.GT a b) = lt b a
1093+
go (EVM.Types.GEq a b) = iszero (lt a b)
1094+
go (EVM.Types.LEq a b) = iszero (lt b a)
1095+
go (SGT a b) = slt b a
1096+
1097+
-- LT
1098+
go (EVM.Types.LT _ (Lit 0)) = Lit 0
1099+
go (EVM.Types.LT a (Lit 1)) = iszero a
1100+
go (EVM.Types.LT a b) = lt a b
1101+
1102+
-- SLT
1103+
go (SLT _ (Lit a)) | a == minLitSigned = Lit 0
1104+
go (SLT (Lit a) _) | a == maxLitSigned = Lit 0
1105+
go (SLT a b) = slt a b
1106+
10651107
-- redundant ITE
10661108
go (ITE (Lit x) a b)
10671109
| x == 0 = b
@@ -1221,15 +1263,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
12211263
| otherwise = t
12221264
go (ITE (Or a b@(Lit _)) t f) = ITE (Or b a) t f
12231265

1224-
-- we write at least 32, so if x <= 32, it's FALSE
1225-
go o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit x))
1226-
| x <= 32 = Lit 0
1227-
| otherwise = o
1228-
-- we write at least 32, so if x < 32, it's TRUE
1229-
go o@(EVM.Types.LT (Lit x) (BufLength (WriteWord {})))
1230-
| x < 32 = Lit 1
1231-
| otherwise = o
1232-
12331266
-- Double NOT is a no-op, since it's a bitwise inversion
12341267
go (EVM.Types.Not (EVM.Types.Not a)) = a
12351268

@@ -1261,35 +1294,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
12611294
-- NOTE: we can't simplify (Lit 0)^k. If k is 0 it's 1, otherwise it's 0.
12621295
-- this is encoded in SMT.hs instead, via an SMT "ite"
12631296

1264-
-- If a >= b then the value of the `Max` expression can never be < b
1265-
go o@(LT (Max (Lit a) _) (Lit b))
1266-
| a >= b = Lit 0
1267-
| otherwise = o
1268-
go o@(SLT (Sub (Max (Lit a) _) (Lit b)) (Lit c))
1269-
= let sa, sb, sc :: Int256
1270-
sa = fromIntegral a
1271-
sb = fromIntegral b
1272-
sc = fromIntegral c
1273-
in if sa >= sb && sa - sb >= sc
1274-
then Lit 0
1275-
else o
1276-
1277-
-- normalize all comparisons in terms of (S)LT
1278-
go (EVM.Types.GT a b) = lt b a
1279-
go (EVM.Types.GEq a b) = leq b a
1280-
go (EVM.Types.LEq a b) = iszero (lt b a)
1281-
go (SGT a b) = slt b a
1282-
1283-
-- LT
1284-
go (EVM.Types.LT _ (Lit 0)) = Lit 0
1285-
go (EVM.Types.LT a (Lit 1)) = iszero a
1286-
go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)
1287-
go (EVM.Types.LT a b) = lt a b
1288-
1289-
-- SLT
1290-
go (SLT _ (Lit a)) | a == minLitSigned = Lit 0
1291-
go (SLT (Lit a) _) | a == maxLitSigned = Lit 0
1292-
go (SLT a b) = slt a b
12931297

12941298
-- simple div/mod/add/sub
12951299
go (Div o1 o2) = EVM.Expr.div o1 o2
@@ -1319,6 +1323,16 @@ simplifyProp prop =
13191323
let new = mapProp' go (simpInnerExpr prop)
13201324
in if (new == prop) then prop else simplifyProp new
13211325
where
1326+
isBoolLike :: Expr EWord -> Bool
1327+
isBoolLike = \case
1328+
LT{} -> True
1329+
SLT{} -> True
1330+
Eq{} -> True
1331+
IsZero{} -> True
1332+
GT{} -> internalError "Should not encounter GT at this point!"
1333+
LEq{} -> internalError "Should not encounter LEq at this point!"
1334+
GEq{} -> internalError "Should not encounter GEq at this point!"
1335+
_ -> False
13221336
go :: Prop -> Prop
13231337

13241338
-- Rewrite PGT/GEq to PLT/PLEq
@@ -1341,54 +1355,44 @@ simplifyProp prop =
13411355
go (PLEq (Sub a b) c) | a == c = PLEq b a
13421356
go (PLEq a (Lit 0)) = peq (Lit 0) a
13431357
go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
1344-
go (PLT (Lit 0) (Eq a b)) = peq a b
1345-
go (PLEq a b) = pleq a b
1346-
1347-
-- when it's PLT but comparison on the RHS then it's just (PEq 1 RHS)
1348-
go (PLT (Lit 0) (a@LT {})) = peq (Lit 1) a
1349-
go (PLT (Lit 0) (a@LEq {})) = peq (Lit 1) a
1350-
go (PLT (Lit 0) (a@SLT {})) = peq (Lit 1) a
1351-
go (PLT (Lit 0) (a@GT {})) = peq (Lit 1) a
1352-
go (PLT (Lit 0) (a@GEq {})) = peq (Lit 1) a
1353-
go (PLT (Lit 0) (a@SGT {})) = peq (Lit 1) a
1358+
1359+
go (PLT (Lit 0) e)
1360+
| isBoolLike e = peq (Lit 1) e
1361+
1362+
-- all possible simplifications for PLT and PLEq have to be covered by this point
1363+
go p@(PLT {}) = p
1364+
go p@(PLEq {}) = p
1365+
1366+
go (PEq (Lit 1) (Eq a b)) = peq a b
1367+
go (PEq (Lit 1) (LT a b)) = PLT a b
1368+
go (PEq (Lit 1) (IsZero e)) = PEq (Lit 0) e
1369+
1370+
go (PEq (Lit 0) (IsZero e))
1371+
| isBoolLike e = PEq (Lit 1) e
1372+
go (PEq (Lit 0) (IsZero e)) = PNeg (PEq (Lit 0) e)
1373+
go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)
1374+
go (PEq (Lit 0) (LT a b)) = PLEq b a
1375+
1376+
go (PEq (Lit 0) (Sub a b)) = peq a b
1377+
go (PEq (Lit 0) (Or a b)) = peq (Lit 0) a `PAnd` peq (Lit 0) b
1378+
go (PEq a1 (Add a2 y)) | a1 == a2 = peq (Lit 0) y
1379+
go (PEq l r) = peq l r
1380+
13541381
go (POr (PLEq a1 (Lit b)) (PLEq (Lit c) a2)) | a1 == a2 && c == b+1 = PBool True
13551382

13561383
-- negations
13571384
go (PNeg (PBool b)) = PBool (Prelude.not b)
13581385
go (PNeg (PNeg a)) = a
13591386
go (PNeg (PGT a b)) = PLEq a b
13601387
go (PNeg (PGEq a b)) = PLT a b
1361-
go (PNeg (PLT a b)) = PGEq a b
1362-
go (PNeg (PLEq a b)) = PGT a b
1388+
go (PNeg (PLT a b)) = PLEq b a
1389+
go (PNeg (PLEq a b)) = PLT b a
13631390
go (PNeg (PAnd a b)) = POr (PNeg a) (PNeg b)
13641391
go (PNeg (POr a b)) = PAnd (PNeg a) (PNeg b)
1365-
go (PNeg (PEq (Lit 1) (IsZero b))) = PEq (Lit 0) (IsZero b)
1366-
1367-
go (PEq (Lit 0) (Or a b)) = peq (Lit 0) a `PAnd` peq (Lit 0) b
1368-
1369-
-- PEq rewrites (notice -- GT/GEq is always rewritten to LT by simplify)
1370-
go (PEq (Lit 1) (IsZero (LT a b))) = PLEq b a
1371-
go (PEq (Lit 1) (IsZero (LEq a b))) = PLT b a
1372-
go (PEq (Lit 0) (IsZero a)) = PLT (Lit 0) a
1373-
go (PEq a1 (Add a2 y)) | a1 == a2 = peq (Lit 0) y
1374-
1375-
-- solc specific stuff
1376-
go (PLT (Lit 0) (IsZero (Eq a b))) = PNeg (peq a b)
1377-
1378-
-- iszero(a) -> (a == 0)
1379-
-- iszero(iszero(a))) -> ~(a == 0) -> a > 0
1380-
-- iszero(iszero(a)) == 0 -> ~~(a == 0) -> a == 0
1381-
-- ~(iszero(iszero(a)) == 0) -> ~~~(a == 0) -> ~(a == 0) -> a > 0
1382-
go (PNeg (PEq (Lit 0) (IsZero (IsZero a)))) = PLT (Lit 0) a
1383-
1384-
-- iszero(a) -> (a == 0)
1385-
-- iszero(a) == 0 -> ~(a == 0)
1386-
-- ~(iszero(a) == 0) -> ~~(a == 0) -> a == 0
1387-
go (PNeg (PEq (Lit 0) (IsZero a))) = peq (Lit 0) a
1388-
1389-
-- a < b == 0 -> ~(a < b)
1390-
-- ~(a < b == 0) -> ~~(a < b) -> a < b
1391-
go (PNeg (PEq (Lit 0) (LT a b))) = PLT a b
1392+
go (PNeg (PEq (Lit 1) e))
1393+
| isBoolLike e = PEq (Lit 0) e
1394+
go (PNeg (PEq (Lit 0) e))
1395+
| isBoolLike e = PEq (Lit 1) e
13921396

13931397
-- And/Or
13941398
go (PAnd (PBool l) (PBool r)) = PBool (l && r)
@@ -1407,19 +1411,6 @@ simplifyProp prop =
14071411
go (PImpl (PBool True) b) = b
14081412
go (PImpl (PBool False) _) = PBool True
14091413

1410-
-- Double negation (no need for GT/GEq, as it's rewritten to LT/LEq)
1411-
1412-
-- Eq
1413-
go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)
1414-
go (PEq (Lit 1) (Eq a b)) = peq a b
1415-
go (PEq (Lit 0) (Sub a b)) = peq a b
1416-
go (PEq (Lit 0) (LT a b)) = PLEq b a
1417-
go (PEq (Lit 0) (LEq a b)) = PLT b a
1418-
go (PEq (Lit 1) (LT a b)) = PLT a b
1419-
go (PEq (Lit 1) (LEq a b)) = PLEq a b
1420-
go (PEq (Lit 1) (GT a b)) = PGT a b
1421-
go (PEq (Lit 1) (GEq a b)) = PGEq a b
1422-
go (PEq l r) = peq l r
14231414

14241415
go p = p
14251416

0 commit comments

Comments
 (0)