Much better simplification

Author: msooseth

src/EVM/Expr.hs

@@ -72,16 +72,24 @@ normArgs sym conc l r = case (l, r) of
   where
     doOp = op2 sym conc
 
+-- Same as `normArgs`, but for commutative operators it orders the arguments canonically
+-- This helps in cases when (PEq x1 x2) is comparing x1 and x2 that are equivalent modulo commutativity.
+-- In such cases, normArgsOrd will make sure x1 and x2 look the same.
+normArgsOrd :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
+normArgsOrd sym conc l r = if l < r then doOp l r else doOp r l
+  where
+    doOp = op2 sym conc
+
 -- Integers
 
 add :: Expr EWord -> Expr EWord -> Expr EWord
-add = normArgs Add (+)
+add = normArgsOrd Add (+)
 
 sub :: Expr EWord -> Expr EWord -> Expr EWord
 sub = op2 Sub (-)
 
 mul :: Expr EWord -> Expr EWord -> Expr EWord
-mul = normArgs Mul (*)
+mul = normArgsOrd Mul (*)
 
 div :: Expr EWord -> Expr EWord -> Expr EWord
 div = op2 Div (\x y -> if y == 0 then 0 else Prelude.div x y)
@@ -156,21 +164,21 @@ sgt = op2 SGT (\x y ->
   in if sx > sy then 1 else 0)
 
 eq :: Expr EWord -> Expr EWord -> Expr EWord
-eq = normArgs Eq (\x y -> if x == y then 1 else 0)
+eq = normArgsOrd Eq (\x y -> if x == y then 1 else 0)
 
 iszero :: Expr EWord -> Expr EWord
 iszero = op1 IsZero (\x -> if x == 0 then 1 else 0)
 
 -- Bits
 
 and :: Expr EWord -> Expr EWord -> Expr EWord
-and = normArgs And (.&.)
+and = normArgsOrd And (.&.)
 
 or :: Expr EWord -> Expr EWord -> Expr EWord
-or = normArgs Or (.|.)
+or = normArgsOrd Or (.|.)
 
 xor :: Expr EWord -> Expr EWord -> Expr EWord
-xor = normArgs Xor Data.Bits.xor
+xor = normArgsOrd Xor Data.Bits.xor
 
 not :: Expr EWord -> Expr EWord
 not = op1 Not complement