Update rewrite rules

Update

MOre te

Author: msooseth

src/EVM/Expr.hs

@@ -1073,9 +1073,6 @@ 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
@@ -1104,7 +1101,6 @@ simplify e = if (mapExpr go e == e)
     -- Notice: all Add is normalized, hence the 1st argument is
     --    expected to be Lit, if any. Hence `orig` needs to be the
     --    2nd argument for Add. However, Sub is not normalized
-    go (Add (Lit x) (Add (Lit y) orig)) = add (Lit (x+y)) orig
     -- add + sub NOTE: every combination of Sub is needed (2)
     go (Add (Lit x) (Sub (Lit y) orig)) = sub (Lit (x+y)) orig
     go (Add (Lit x) (Sub orig (Lit y))) = add (Lit (x-y)) orig
@@ -1117,18 +1113,27 @@ simplify e = if (mapExpr go e == e)
     go (Sub (Lit x) (Add (Lit y) orig)) = sub (Lit (x-y)) orig
     go (Sub (Add (Lit x) orig) (Lit y) ) = add (Lit (x-y)) orig
 
+    -- Add+Add / Mul+Mul / Xor+Xor simplifications, taking
+    --     advantage of associativity and commutativity
+    -- Since Lit is smallest in the ordering, it will always be the first argument
+    --     hence these will collect Lits. See `simp-assoc..` tests
+    go (Add (Lit a) (Add (Lit b) x)) = add (Lit (a+b)) x
+    go (Mul (Lit a) (Mul (Lit b) x)) = mul (Lit (a*b)) x
+    go (Xor (Lit a) (Xor (Lit b) x)) = EVM.Expr.xor (Lit (Data.Bits.xor a b)) x
+    go (Add a (Add b c)) = add (l !! 0) (add (l !! 1) (l !! 2))
+      where l = sort [a, b, c]
+    go (Mul a (Mul b c)) = mul (l !! 0) (mul (l !! 1) (l !! 2))
+      where l = sort [a, b, c]
+    go (Xor a (Xor b c)) = x (l !! 0) (x (l !! 1) (l !! 2))
+      where l = sort [a, b, c]
+            x = EVM.Expr.xor
+
     -- redundant add / sub
     go (Sub (Add a b) c)
       | a == c = b
       | b == c = a
       | otherwise = sub (add a b) c
 
-    -- Add is associative. We are doing left-growing trees because LIT is
-    -- arranged to the left. This way, they accumulate in all combinations.
-    -- See `sim-assoc-add` test cases in test.hs
-    go (Add a (Add b c)) = add (add a b) c
-    go (Add (Add (Lit a) x) (Lit b)) = add (Lit (a+b)) x
-
     -- add / sub identities
     go (Add a b)
       | b == (Lit 0) = a
@@ -1139,6 +1144,9 @@ simplify e = if (mapExpr go e == e)
       | b == (Lit 0) = a
       | otherwise = sub a b
 
+    -- XOR normalization
+    go (Xor a  b) = EVM.Expr.xor a b
+
     -- SHL / SHR by 0
     go (SHL a v)
       | a == (Lit 0) = v
@@ -1192,11 +1200,6 @@ simplify e = if (mapExpr go e == e)
                      (Lit 0, _) -> Lit 0
                      _ -> EVM.Expr.min a b
 
-    -- Mul is associative. We are doing left-growing trees because LIT is
-    -- arranged to the left. This way, they accumulate in all combinations.
-    -- See `sim-assoc-add` test cases in test.hs
-    go (Mul a (Mul b c)) = mul (mul a b) c
-    go (Mul (Mul (Lit a) x) (Lit b)) = mul (Lit (a*b)) x
 
     -- Some trivial mul eliminations
     go (Mul a b) = case (a, b) of

test/test.hs

@@ -559,11 +559,11 @@ tests = testGroup "hevm"
       let simp = Expr.simplifyProp $ PLT (Max (Lit 5) (BufLength (AbstractBuf "txdata"))) (Lit 99)
       assertEqualM "max-buflength rules" simp $ PLT (BufLength (AbstractBuf "txdata")) (Lit 99)
     , test "simp-assoc-add1" $ do
-      let simp = Expr.simplify $        Add (Var "a") (Add (Var "b") (Var "c"))
-      assertEqualM "assoc rules" simp $ Add (Add (Var "a") (Var "b")) (Var "c")
+      let simp = Expr.simplify $        Add (Add (Var "c") (Var "a")) (Var "b")
+      assertEqualM "assoc rules" simp $ Add (Var "a") (Add (Var "b") (Var "c"))
     , test "simp-assoc-add2" $ do
-      let simp = Expr.simplify $        Add (Lit 1) (Add (Var "b") (Var "c"))
-      assertEqualM "assoc rules" simp $ Add (Add (Lit 1) (Var "b")) (Var "c")
+      let simp = Expr.simplify $        Add (Add (Lit 1) (Var "c")) (Var "b")
+      assertEqualM "assoc rules" simp $ Add (Lit 1) (Add (Var "b") (Var "c"))
     , test "simp-assoc-add3" $ do
       let simp = Expr.simplify $        Add (Lit 1) (Add (Lit 2) (Var "c"))
       assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "c")
@@ -578,16 +578,22 @@ tests = testGroup "hevm"
       assertEqualM "assoc rules" simp $ Lit 10
     , test "simp-assoc-add-7" $ do
       let simp = Expr.simplify $        Add (Var "a") (Add (Var "b") (Lit 2))
-      assertEqualM "assoc rules" simp $ Add (Add (Lit 2) (Var "a")) (Var "b")
+      assertEqualM "assoc rules" simp $ Add (Lit 2) (Add (Var "a") (Var "b"))
     , test "simp-assoc-add8" $ do
       let simp = Expr.simplify $        Add (Add (Var "a") (Add (Lit 0x2) (Var "b"))) (Add (Var "c") (Add (Lit 0x2) (Var "d")))
-      assertEqualM "assoc rules" simp $ Add (Add (Add (Add (Lit 0x4) (Var "a")) (Var "b")) (Var "c")) (Var "d")
+      assertEqualM "assoc rules" simp $ Add (Lit 4) (Add (Var "a") (Add (Var "b") (Add (Var "c") (Var "d"))))
     , test "simp-assoc-mul1" $ do
-      let simp = Expr.simplify $        Mul (Var "a") (Mul (Var "b") (Var "c"))
-      assertEqualM "assoc rules" simp $ Mul (Mul (Var "a") (Var "b")) (Var "c")
+      let simp = Expr.simplify $        Mul (Mul (Var "b") (Var "a")) (Var "c")
+      assertEqualM "assoc rules" simp $ Mul (Var "a") (Mul (Var "b") (Var "c"))
     , test "simp-assoc-mul2" $ do
       let simp = Expr.simplify       $  Mul (Lit 2) (Mul (Var "a") (Lit 3))
       assertEqualM "assoc rules" simp $ Mul (Lit 6) (Var "a")
+    , test "simp-assoc-xor1" $ do
+      let simp = Expr.simplify       $  Xor (Lit 2) (Xor (Var "a") (Lit 3))
+      assertEqualM "assoc rules" simp $ Xor (Lit 1) (Var "a")
+    , test "simp-assoc-xor2" $ do
+      let simp = Expr.simplify       $  Xor (Lit 2) (Xor (Var "b") (Xor (Var "a") (Lit 3)))
+      assertEqualM "assoc rules" simp $ Xor (Lit 1) (Xor (Var "a") (Var "b"))
     , test "simp-zero-write-extend-buffer-len" $ do
         let
           expr = BufLength $ CopySlice (Lit 0) (Lit 0x10) (Lit 0) (AbstractBuf "buffer") (ConcreteBuf "bimm")
@@ -1508,7 +1514,10 @@ tests = testGroup "hevm"
             |]
         let sig = Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
         (_, k) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
-        putStrLnM $ "Ret: " <> (show k)
+        let numErrs = sum $ map (fromEnum . isError) k
+        assertEqualM "number of errors (i.e. copySlice issues) is 1" 1 numErrs
+        let errStrings = mapMaybe EVM.SymExec.getError k
+        assertEqualM "All errors are from copyslice" True $ all ("CopySlice" `List.isInfixOf`) errStrings
       ,
       test "symbolic-copyslice" $ do
         Just c <- solcRuntime "MyContract"
@@ -4691,11 +4700,11 @@ tests = testGroup "hevm"
             putStrLnM "------------- END -----------------"
           Just aPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredASym
           Just bPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredBSym
-          procs <- liftIO $ getNumProcessors
-          withSolvers CVC5 (unsafeInto procs) 1 (Just 100) $ \s -> do
+          procs <- liftIO getNumProcessors
+          withSolvers Bitwuzla (unsafeInto procs) 1 (Just 100) $ \s -> do
             calldata <- mkCalldata Nothing []
             (res, _) <- equivalenceCheck s aPrgm bPrgm opts calldata False
-            end <- liftIO $ getCurrentTime
+            end <- liftIO getCurrentTime
             case any isCex res of
               False -> liftIO $ do
                 print $ "OK. Took " <> (show $ diffUTCTime end start) <> " seconds"