Add and Mul are associative. Let's make them canonical

CHANGELOG.md

@@ -113,6 +113,7 @@ are no longer explicitly tested or supported.
 - `evalProp` is renamed to `simplifyProp` for consistency
 - Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed.
 - BufLength was not simplified via bufLength function. Fixed.
+- Add and Mul are associative, let's use that to make Expr more canonical
 - `VMOpts` no longer takes an initial store, and instead takes a `baseState`
   which can be either `EmptyBase` or `AbstractBase`. This controls whether
   storage should be inialized as empty or fully abstract. Regardless of this

src/EVM/Expr.hs

@@ -881,6 +881,12 @@ simplify e = if (mapExpr go e == e)
       | 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
@@ -947,11 +953,18 @@ 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
                      (Lit 0, _) -> Lit 0
                      (Lit 1, _) -> b
                      _ -> mul a b
+
     -- Some trivial div eliminations
     go (Div (Lit 0) _) = Lit 0 -- divide 0 by anything (including 0) is zero in EVM
     go (Div _ (Lit 0)) = Lit 0 -- divide anything by 0 is zero in EVM

test/test.hs

@@ -316,6 +316,36 @@ tests = testGroup "hevm"
         let e = ReadByte (Lit 0x0) (WriteWord (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd) (Lit 0x0) (ConcreteBuf "\255\255\255\255"))
         b <- checkEquiv e (Expr.simplify e)
         assertBoolM "Simplifier failed" b
+    , 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")
+    , 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")
+    , 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")
+    , test "simp-assoc-add4" $ do
+      let simp = Expr.simplify $        Add (Lit 1) (Add (Var "b") (Lit 2))
+      assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "b")
+    , test "simp-assoc-add5" $ do
+      let simp = Expr.simplify $        Add (Var "a") (Add (Lit 1) (Lit 2))
+      assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "a")
+    , test "simp-assoc-add6" $ do
+      let simp = Expr.simplify $        Add (Lit 7) (Add (Lit 1) (Lit 2))
+      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")
+    , 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")
+    , 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")
+    , 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 "bufLength-simp" $ do
       let
         a = BufLength (ConcreteBuf "ab")
@@ -1542,6 +1572,28 @@ tests = testGroup "hevm"
         checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
       putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
      ,
+     test "opcode-mul-assoc" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(int256 a, int256 b, int256 c) external pure {
+              int256 tmp1;
+              int256 out1;
+              int256 tmp2;
+              int256 out2;
+              assembly {
+                tmp1 := mul(a, b)
+                out1 := mul(tmp1,c)
+                tmp2 := mul(b, c)
+                out2 := mul(a, tmp2)
+              }
+              assert (out1 == out2);
+              }
+             }
+            |]
+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256,int256)" [AbiIntType 256, AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+        putStrLnM "MUL is associative"
+     ,
      -- TODO look at tests here for SAR: https://github.com/dapphub/dapptools/blob/01ef8ea418c3fe49089a44d56013d8fcc34a1ec2/src/dapp-tests/pass/constantinople.sol#L250
      test "opcode-sar-neg" $ do
         Just c <- solcRuntime "MyContract"