Fixing up assoc mul&add to make it concretize always

Also fixing up the test that was broken

src/EVM/Expr.hs

@@ -883,6 +883,7 @@ simplify e = if (mapExpr go e == e)
 
     -- Add is associative
     go (Add (Add a b) c) = add a (add b c)
+    go (Add (Lit a) (Add (Lit b) x)) = add (Lit (a+b)) x
 
     -- add / sub identities
     go (Add a b)
@@ -952,6 +953,8 @@ simplify e = if (mapExpr go e == e)
 
     -- Mul is associative
     go (Mul (Mul a b) c) = mul a (mul b c)
+    go (Mul (Lit a) (Mul (Lit b) x)) = mul (Lit (a*b)) x
+
     -- Some trivial mul eliminations
     go (Mul a b) = case (a, b) of
                      (Lit 0, _) -> Lit 0

test/test.hs

@@ -316,6 +316,30 @@ 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 (Add (Var "a") (Var "b")) (Var "c")
+      assertEqualM "assoc rules" simp $ Add (Var "a") (Add (Var "b") (Var "c"))
+    , test "simp-assoc-add2" $ do
+      let simp = Expr.simplify $        Add (Add (Lit 1) (Var "b")) (Var "c")
+      assertEqualM "assoc rules" simp $ Add (Lit 1) (Add (Var "b") (Var "c"))
+    , test "simp-assoc-add3" $ do
+      let simp = Expr.simplify       $  Add (Add (Lit 1) (Lit 2)) (Var "c")
+      assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "c")
+    , test "simp-assoc-add4" $ do
+      let simp = Expr.simplify       $  Add (Add (Lit 1) (Var "b")) (Lit 2)
+      assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "b")
+    , test "simp-assoc-add5" $ do
+      let simp = Expr.simplify       $  Add (Add (Var "a") (Lit 1)) (Lit 2)
+      assertEqualM "assoc rules" simp $ Add (Lit 3) (Var "a")
+    , test "simp-assoc-add6" $ do
+      let simp = Expr.simplify       $  Add (Add (Lit 7) (Lit 1)) (Lit 2)
+      assertEqualM "assoc rules" simp $ Lit 10
+    , test "simp-assoc-mul1" $ do
+      let simp = Expr.simplify $        Mul (Mul (Var "a") (Var "b")) (Var "c")
+      assertEqualM "assoc rules" simp $ Mul (Var "a") (Mul (Var "b") (Var "c"))
+    , test "simp-assoc-mul2" $ do
+      let simp = Expr.simplify       $  Mul (Mul (Var "a") (Lit 2)) (Lit 3)
+      assertEqualM "assoc rules" simp $ Mul (Lit 6) (Var "a")
     , test "bufLength-simp" $ do
       let
         a = BufLength (ConcreteBuf "ab")
@@ -1562,7 +1586,7 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256,int256)" [AbiIntType 256, AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "MUL is associative"
+        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