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

@@ -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)" $

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)

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]
       _ -> []
   _ -> []
 

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"
 

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'

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

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)