Merge pull request #426 from ethereum/more-prop-simp2

Simplify earlier and don't check reachability for FALSE

CHANGELOG.md

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - New solc-specific simplification rules that should make the final Props a lot more readable
 - Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
   and further solc-specific simplifications of Expr
+- Simplify earlier and don't check reachability for things statically determined to be FALSE
 
 ## [0.52.0] - 2023-10-26
 

src/EVM/Expr.hs

@@ -1326,6 +1326,7 @@ constFoldProp ps = oneRun ps (ConstState mempty True)
     oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat
     go :: Prop -> State ConstState ()
     go x = case x of
+        -- PEq
         PEq (Lit l) a -> do
           s <- get
           case Map.lookup a s.values of
@@ -1336,6 +1337,16 @@ constFoldProp ps = oneRun ps (ConstState mempty True)
               let vs' = Map.insert a l s.values
               put $ s{values=vs'}
         PEq a b@(Lit _) -> go (PEq b a)
+        -- PNeg
+        PNeg (PEq (Lit l) a) -> do
+          s <- get
+          case Map.lookup a s.values of
+            Just l2 -> case l==l2 of
+                True -> put ConstState {canBeSat=False, values=mempty}
+                False -> pure ()
+            Nothing -> pure()
+        PNeg (PEq a b@(Lit _)) -> go $ PNeg (PEq b a)
+        -- Others
         PAnd a b -> do
           go a
           go b

src/EVM/SymExec.hs

@@ -567,14 +567,9 @@ verify solvers opts preState maybepost = do
       Nothing -> pure (expr, [Qed ()])
       Just post -> liftIO $ do
         let
-          -- Filter out any leaves that can be statically shown to be safe
-          canViolate = flip filter flattened $
-            \leaf -> case Expr.simplifyProp (post preState leaf) of
-              PBool True -> False
-              _ -> True
-          assumes = preState.constraints
-          withQueries = canViolate <&> \leaf ->
-            (assertProps conf (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
+          -- Filter out any leaves from `flattened` that can be statically shown to be safe
+          tocheck = flip map flattened $ \leaf -> (toPropsFinal leaf preState.constraints post, leaf)
+          withQueries = filter canBeSat tocheck <&> \(a, leaf) -> (assertProps conf a, leaf)
         putStrLn $ "Checking for reachability of "
                      <> show (length withQueries)
                      <> " potential property violation(s)"
@@ -586,6 +581,12 @@ verify solvers opts preState maybepost = do
         let cexs = filter (\(res, _) -> not . isUnsat $ res) results
         pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
   where
+    toProps leaf constr post = PNeg (post preState leaf) : constr <> extractProps leaf
+    toPropsFinal leaf constr post = if opts.simp then Expr.simplifyProps $ toProps leaf constr post
+                                                 else toProps leaf constr post
+    canBeSat (a, _) = case a of
+        [PBool False] -> False
+        _ -> True
     toVRes :: (CheckSatResult, Expr End) -> VerifyResult
     toVRes (res, leaf) = case res of
       Sat model -> Cex (leaf, expandCex preState model)

test/test.hs

@@ -2702,7 +2702,16 @@ tests = testGroup "hevm"
   ]
   , testGroup "simplification-working"
   [
-    test "prop-simp-bool1" $ do
+    test "PEq-and-PNot-PEq-1" $ do
+      let a = [PEq (Lit 0x539) (Var "arg1"),PNeg (PEq (Lit 0x539) (Var "arg1"))]
+      assertEqualM "Must simplify to PBool False" (Expr.simplifyProps a) ([PBool False])
+    , test "PEq-and-PNot-PEq-2" $ do
+      let a = [PEq (Var "arg1") (Lit 0x539),PNeg (PEq (Lit 0x539) (Var "arg1"))]
+      assertEqualM "Must simplify to PBool False" (Expr.simplifyProps a) ([PBool False])
+    , test "PEq-and-PNot-PEq-3" $ do
+      let a = [PEq (Var "arg1") (Lit 0x539),PNeg (PEq (Var "arg1") (Lit 0x539))]
+      assertEqualM "Must simplify to PBool False" (Expr.simplifyProps a) ([PBool False])
+    , test "prop-simp-bool1" $ do
       let
         a = successGen [PAnd (PBool True) (PBool False)]
         b = Expr.simplify a