Merge pull request #550 from ethereum/enforce-lhs-constants

Enforce that LHS are constants for commutative operations

CHANGELOG.md

@@ -30,6 +30,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Add `freshAddresses` field in `VMOpts` so that initial fresh address can be given as input
 - Add documentation about limitations and workarounds
 - More verbose error messages in case of symbolic arguments to opcode
+* Tests to enforce that in Expr and Prop, constants are on the LHS whenever possible
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing

src/EVM/Expr.hs

@@ -1047,6 +1047,9 @@ simplify e = if (mapExpr go e == e)
     -- literal addresses
     go (WAddr (LitAddr a)) = Lit $ into a
 
+    -- XOR normalization
+    go (Xor a  b) = EVM.Expr.xor a b
+
     -- simple div/mod/add/sub
     go (Div o1@(Lit _)  o2@(Lit _)) = EVM.Expr.div  o1 o2
     go (SDiv o1@(Lit _) o2@(Lit _)) = EVM.Expr.sdiv o1 o2
@@ -1605,3 +1608,25 @@ concKeccakOnePass orig@(Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) orig2@(WriteW
     (64, ConcreteBuf a) -> Lit (keccak' a)
     _ -> orig
 concKeccakOnePass x = x
+
+lhsConstHelper :: Expr a -> Maybe ()
+lhsConstHelper = go
+  where
+    go :: Expr a -> Maybe ()
+    go (Mul _ (Lit _)) = Nothing
+    go (Add _ (Lit _)) = Nothing
+    go (Min _ (Lit _)) = Nothing
+    go (Max _ (Lit _)) = Nothing
+    go (Eq _ (Lit _))  = Nothing
+    go (And _ (Lit _)) = Nothing
+    go (Or _ (Lit _))  = Nothing
+    go (Xor _ (Lit _)) = Nothing
+    go _ = Just ()
+
+-- Commutative operators should have the constant on the LHS
+checkLHSConstProp :: Prop -> Bool
+checkLHSConstProp a = isJust $ mapPropM_ lhsConstHelper a
+
+-- Commutative operators should have the constant on the LHS
+checkLHSConst :: Expr a -> Bool
+checkLHSConst a = isJust $ mapExprM_ lhsConstHelper a

test/test.hs

@@ -544,13 +544,13 @@ tests = testGroup "hevm"
   , adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) $ testGroup "SimplifierTests"
     [ testProperty  "buffer-simplification" $ \(expr :: Expr Buf) -> prop $ do
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , testProperty "store-simplification" $ \(expr :: Expr Storage) -> prop $ do
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , testProperty "load-simplification" $ \(GenWriteStorageLoad expr) -> prop $ do
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , ignoreTest $ testProperty "load-decompose" $ \(GenWriteStorageLoad expr) -> prop $ do
         putStrLnM $ T.unpack $ formatExpr expr
         let simp = Expr.simplify expr
@@ -561,49 +561,49 @@ tests = testGroup "hevm"
         checkEquiv expr decomposed
     , testProperty "byte-simplification" $ \(expr :: Expr Byte) -> prop $ do
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , testProperty "word-simplification" $ \(ZeroDepthWord expr) -> prop $ do
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , testProperty "readStorage-equivalance" $ \(store, slot) -> prop $ do
         let simplified = Expr.readStorage' slot store
             full = SLoad slot store
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "writeStorage-equivalance" $ \(val, GenWriteStorageExpr (slot, store)) -> prop $ do
         let simplified = Expr.writeStorage slot val store
             full = SStore slot val store
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "readWord-equivalance" $ \(buf, idx) -> prop $ do
         let simplified = Expr.readWord idx buf
             full = ReadWord idx buf
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "writeWord-equivalance" $ \(idx, val, WriteWordBuf buf) -> prop $ do
         let simplified = Expr.writeWord idx val buf
             full = WriteWord idx val buf
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "arith-simplification" $ \(_ :: Int) -> prop $ do
         expr <- liftIO $ generate . sized $ genWordArith 15
         let simplified = Expr.simplify expr
-        checkEquiv expr simplified
+        checkEquivAndLHS expr simplified
     , testProperty "readByte-equivalance" $ \(buf, idx) -> prop $ do
         let simplified = Expr.readByte idx buf
             full = ReadByte idx buf
-        checkEquiv simplified full
+        checkEquiv full simplified
     -- we currently only simplify concrete writes over concrete buffers so that's what we test here
     , testProperty "writeByte-equivalance" $ \(LitOnly val, LitOnly buf, GenWriteByteIdx idx) -> prop $ do
         let simplified = Expr.writeByte idx val buf
             full = WriteByte idx val buf
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "copySlice-equivalance" $ \(srcOff, GenCopySliceBuf src, GenCopySliceBuf dst, LitWord @300 size) -> prop $ do
         -- we bias buffers to be concrete more often than not
         dstOff <- liftIO $ generate (maybeBoundedLit 100_000)
         let simplified = Expr.copySlice srcOff dstOff size src dst
             full = CopySlice srcOff dstOff size src dst
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "indexWord-equivalence" $ \(src, LitWord @50 idx) -> prop $ do
         let simplified = Expr.indexWord idx src
             full = IndexWord idx src
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "indexWord-mask-equivalence" $ \(src :: Expr EWord, LitWord @35 idx) -> prop $ do
         mask <- liftIO $ generate $ do
           pow <- arbitrary :: Gen Int
@@ -615,7 +615,7 @@ tests = testGroup "hevm"
           input = And mask src
           simplified = Expr.indexWord idx input
           full = IndexWord idx input
-        checkEquiv simplified full
+        checkEquiv full simplified
     , testProperty "toList-equivalance" $ \buf -> prop $ do
         let
           -- transforms the input buffer to give it a known length
@@ -653,21 +653,21 @@ tests = testGroup "hevm"
           _ -> liftIO $ assertFailure "must evaluate down to a literal bool"
     , testProperty "simplifyProp-equivalence-sym" $ \(p) -> prop $ do
         let simplified = Expr.simplifyProp p
-        checkEquivProp simplified p
+        checkEquivPropAndLHS p simplified
     , testProperty "simpProp-equivalence-sym-Prop" $ \(ps :: [Prop]) -> prop $ do
         let simplified = pand (Expr.simplifyProps ps)
-        checkEquivProp simplified (pand ps)
+        checkEquivPropAndLHS (pand ps) simplified
     , testProperty "simpProp-equivalence-sym-LitProp" $ \(LitProp p) -> prop $ do
         let simplified = pand (Expr.simplifyProps [p])
-        checkEquivProp simplified p
+        checkEquivPropAndLHS p simplified
     , testProperty "storage-slot-simp-property" $ \(StorageExp s) -> prop $ do
         -- we have to run `Expr.structureArraySlots` on the unsimplified system, or
         -- we'd need some form of minimal simplifier for things to work out. As long as
         -- we trust the structureArraySlots, this is fine, as that function is standalone,
         -- and quite minimal
         let s2 = Expr.structureArraySlots s
         let simplified = Expr.simplify s2
-        checkEquiv simplified s2
+        checkEquivAndLHS s2 simplified
     ]
   , testGroup "isUnsat-concrete-tests" [
       test "disjunction-left-false" $ do
@@ -3639,9 +3639,21 @@ tests = testGroup "hevm"
 checkEquivProp :: App m => Prop -> Prop -> m Bool
 checkEquivProp = checkEquivBase (\l r -> PNeg (PImpl l r .&& PImpl r l))
 
+checkEquivPropAndLHS :: App m => Prop -> Prop -> m Bool
+checkEquivPropAndLHS orig simp = do
+  let lhsConst = Expr.checkLHSConstProp simp
+  equiv <- checkEquivProp orig simp
+  pure $ lhsConst && equiv
+
 checkEquiv :: (Typeable a, App m) => Expr a -> Expr a -> m Bool
 checkEquiv = checkEquivBase (./=)
 
+checkEquivAndLHS :: (Typeable a, App m) => Expr a -> Expr a -> m Bool
+checkEquivAndLHS orig simp = do
+  let lhsConst =  Expr.checkLHSConst simp
+  equiv <- checkEquiv orig simp
+  pure $ lhsConst && equiv
+
 checkEquivBase :: (Eq a, App m) => (a -> a -> Prop) -> a -> a -> m Bool
 checkEquivBase mkprop l r = do
   conf <-  readConfig