Add 2 more Expr simplifications related to negative numbers, enable NOT concretization (#1017)

* Add 2 more Expr simplifications related to negative numbers

* Update src/EVM/Expr.hs

Co-authored-by: blishko <blishko@argot.org>

* Update test/EVM/Expr/ExprTests.hs

Co-authored-by: blishko <blishko@argot.org>

* Update test/EVM/Expr/ExprTests.hs

Co-authored-by: blishko <blishko@argot.org>

* Update test/EVM/Expr/ExprTests.hs

Co-authored-by: blishko <blishko@argot.org>

* Oops, not concretization was missing

Testing

* Cleaner, thanks to @blishko

---------

Co-authored-by: blishko <blishko@argot.org>

Author: msooseth

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   controlled via `merge-max-budget`
 
 ## Changed
+- Simplifier now rewrites `Mul(-1, x)` and `~x + 1` to `Sub(0, x)`
 - `AbiFunction` and `AbiBytes` parser is now more strict
 - We now check length of AbiArrayDynamic and don't crash in case it's too large
 - SMT queries now run in separate processes, which allows us to better manage

src/EVM/Expr.hs

@@ -1212,6 +1212,9 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | b == c = a
       | otherwise = sub (add a b) c
 
+    -- Negation: ~x + 1 = 0 - x (two's complement)
+    go (Add (Lit 1) (Not b)) = Sub (Lit 0) b
+
     -- add / sub identities
     go (Add a b)
       | b == (Lit 0) = a
@@ -1223,8 +1226,14 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | otherwise = sub a b
 
     -- XOR normalization
+    go (Xor (Lit a) b) | a == maxLit = EVM.Expr.not b
     go (Xor a  b) = EVM.Expr.xor a b
 
+    -- Not simplification
+    go (EVM.Types.Not (EVM.Types.Not a)) = a
+    go (Not a) = EVM.Expr.not a
+
+    -- EqByte
     go (EqByte a b) = eqByte a b
 
     -- SHL / SHR / SAR
@@ -1257,8 +1266,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | b == (Lit 0) = a
       | otherwise = EVM.Expr.or a b
 
-    -- Double NOT is a no-op, since it's a bitwise inversion
-    go (EVM.Types.Not (EVM.Types.Not a)) = a
 
     -- Some trivial min / max eliminations
     go (Max a b) = EVM.Expr.max a b
@@ -1271,6 +1278,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     go (Mul a b) = case (a, b) of
                      (Lit 0, _) -> Lit 0
                      (Lit 1, _) -> b
+                     (Lit v, _) | v == maxLit -> Sub (Lit 0) b
                      _ -> mul a b
 
     -- Some trivial (s)div eliminations

test/EVM/Expr/ExprTests.hs

@@ -279,6 +279,21 @@ basicSimplificationTests = testGroup "Basic simplification tests"
         a = successPath [PEq (Add (Lit 1) (Lit 2)) (Sub (Lit 4) (Lit 1))]
         b = Expr.simplify a
       assertEqual "Must simplify down" (successPath []) b
+  , testCase "simp-mul-neg1" $ do
+      let simp = Expr.simplify $ Mul (Lit Expr.maxLit) (Var "x")
+      assertEqual "mul by -1 is negation" (Sub (Lit 0) (Var "x")) simp
+  , testCase "simp-not-plus1" $ do
+      let simp = Expr.simplify $ Add (Lit 1) (Not (Var "x"))
+      assertEqual "~x + 1 is negation" (Sub (Lit 0) (Var "x")) simp
+  , testCase "simp-xor-maxlit-plus1" $ do
+      let simp = Expr.simplify $ Add (Lit 1) (Xor (Lit Expr.maxLit) (Var "x"))
+      assertEqual "xor(maxLit, x) + 1 is negation" (Sub (Lit 0) (Var "x")) simp
+  , testCase "simp-double-not" $ do
+      let simp = Expr.simplify $ Not (Not (Var "a"))
+      assertEqual "Not should be concretized" (Var "a") simp
+  , testCase "simp-not-concrete" $ do
+      let simp = Expr.simplify $ Not (Lit 0x55)
+      assertEqual "Not should be concretized" (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffaa) simp
   ]
 
 propSimplificationTests :: TestTree
@@ -847,4 +862,4 @@ isSatOrUnknown :: SMTResult -> Bool
 isSatOrUnknown res = isSat res || isUnknown res
 
 isUnsatOrUnknown :: SMTResult -> Bool
-isUnsatOrUnknown res = isQed res || isUnknown res
+isUnsatOrUnknown res = isQed res || isUnknown res