Fixing checking assert failure

CHANGELOG.md

@@ -82,6 +82,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   instead of crashing.
 - We no longer produce duplicate SMT assertions regarding concrete keccak values.
 - Ord is now correctly implemented for Prop.
+- We only report FAIL in `test` mode for assertion failures that match the
+  string prefix "assertion failed", or match function selector Panic(uint256)
+  with a parameter 0x1. Previously, `require(a==b, "reason")` was a cause for
+  FAIL in case a!=b was possible. This has now been fixed.
 
 ## Changed
 - Warnings now lead printing FAIL. This way, users don't accidentally think that

src/EVM/SymExec.hs

@@ -508,6 +508,7 @@ getExpr solvers c signature' concreteArgs opts = do
     - 0x51: If you call a zero-initialized variable of internal function type.
 
   see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require
+  NOTE: does not deal with e.g. `assertEq()`
 -}
 checkAssertions :: [Word256] -> Postcondition s
 checkAssertions errs _ = \case

src/EVM/UnitTest.hs

@@ -43,6 +43,8 @@ import Data.Word (Word64)
 import GHC.Natural
 import System.IO (hFlush, stdout)
 import Witch (unsafeInto, into)
+import Data.Vector qualified as V
+import Data.Char (ord)
 
 data UnitTestOptions s = UnitTestOptions
   { rpcInfo     :: Fetch.RpcInfo
@@ -210,9 +212,12 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
             Success _ _ _ store -> if opts.checkFailBit then PNeg (failed store) else PBool True
             Failure _ _ (Revert msg) -> case msg of
               ConcreteBuf b ->
-                if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False
+                -- We need to drop the selector (4B), the offset value (aligned to 32B), and the length of the string (aligned to 32B)
+                -- NOTE: assertTrue/assertFalse does not have the double colon after "assertion failed"
+                let assertFail = selector "Error(string)" `BS.isPrefixOf` b && "assertion failed" `BS.isPrefixOf` (BS.drop (4+32+32) b)
+                in if assertFail || b == panicMsg 0x01 then PBool False
                 else PBool True
-              b -> b ./= ConcreteBuf (panicMsg 0x01)
+              _ -> symbolicFail msg
             Failure _ _ _ -> PBool True
             Partial _ _ _ -> PBool True
             _ -> internalError "Invalid leaf node"
@@ -257,7 +262,14 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     liftIO $ putStr txtResult
     liftIO $ printWarnings ends results t
     pure (not (any isCex results), not (warnings || unexpectedAllRevert))
-
+    where
+      symbolicFail :: Expr Buf -> Prop
+      symbolicFail e =
+        let text = V.fromList $ map (fromIntegral . ord) "assertion failed"
+            panic = e == ConcreteBuf (panicMsg 0x01)
+            assertFail =  V.take (length text) (Expr.concretePrefix e) == text
+        in PBool ((not panic) && (not assertFail))
+--
 printWarnings :: GetUnknownStr b => [Expr 'End] -> [ProofResult a b] -> String -> IO ()
 printWarnings e results testName = do
   when (any isUnknown results || any isError results || any Expr.isPartial e) $ do

test/contracts/fail/assertEq.sol

@@ -0,0 +1,7 @@
+import {Test} from "forge-std/Test.sol";
+
+contract SolidityTest is Test {
+    function prove_assert_equal(uint stuff) public {
+        assertEq(stuff, 0);
+    }
+}

test/contracts/fail/bad-cheatcode.sol

@@ -0,0 +1,13 @@
+import {Test} from "forge-std/Test.sol";
+
+interface Vm {
+  function bad_cheatcode(uint) external returns (bytes32);
+}
+
+contract SolidityTest is Test {
+    function prove_bad_cheatcode(uint stuff) public {
+        Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+        assert(stuff != 4);
+        vm.bad_cheatcode(stuff);
+    }
+}

test/contracts/fail/dsProveFail.sol

@@ -12,7 +12,7 @@ contract SolidityTest is Test {
         assert(false);
     }
 
-    function prove_all_branches_fail() public {
+    function prove_all_branches_revert() public {
         require(false);
     }
 
@@ -26,6 +26,8 @@ contract SolidityTest is Test {
         }
     }
 
+    // This seems to be fast now on SMT solvers, due to built-in heuristics
+    // hence no timeout
     function prove_smtTimeout(uint x, uint y, uint z) public {
         if ((x * y / z) * (x / y) / (x * y) == (x * x * x * y * z / x * z * y)) {
             assertTrue(false);

test/contracts/pass/requireEmpty.sol

@@ -0,0 +1,11 @@
+import {Test} from "forge-std/Test.sol";
+
+contract SolidityTest is Test {
+    function prove_require_emtpy(uint stuff, uint a) public returns (uint) {
+        if (stuff == 0) {
+          require(a == 0);
+          return a;
+        }
+        return a;
+    }
+}

test/contracts/pass/requireString.sol

@@ -0,0 +1,11 @@
+import {Test} from "forge-std/Test.sol";
+
+contract SolidityTest is Test {
+    function prove_require_string(uint stuff, uint a) public returns (uint) {
+        if (stuff == 0) {
+          require(a == 0, "must be 0");
+          return a;
+        }
+        return a;
+    }
+}

test/contracts/pass/revertEmpty.sol

@@ -0,0 +1,7 @@
+import {Test} from "forge-std/Test.sol";
+
+contract SolidityTest is Test {
+    function prove_revert_empty(uint stuff) public {
+        if (stuff == 0) revert();
+    }
+}

test/contracts/pass/revertString.sol

@@ -0,0 +1,7 @@
+import {Test} from "forge-std/Test.sol";
+
+contract SolidityTest is Test {
+    function prove_revert_string(uint stuff) public {
+        if (stuff == 0) revert("stuff");
+    }
+}

test/test.hs

@@ -1763,15 +1763,27 @@ tests = testGroup "hevm"
         runSolidityTest testFile ".*" >>= assertEqualM "test result" (True, True)
     , test "Foundry" $ do
         -- quick smokecheck to make sure that we can parse ForgeStdLib style build outputs
+        -- return is a pair of (No Cex, No Warnings)
         let cases =
-              [ ("test/contracts/pass/trivial.sol", ".*", (True, True))
-              , ("test/contracts/pass/dsProvePass.sol", "proveEasy", (True, True))
-              , ("test/contracts/fail/trivial.sol", ".*", (False, False))
-              , ("test/contracts/fail/dsProveFail.sol", "prove_add", (False, True))
+              [ ("test/contracts/pass/trivial.sol",       ".*", (True, True))
+              , ("test/contracts/pass/dsProvePass.sol",   ".*", (True, True))
+              , ("test/contracts/pass/revertEmpty.sol",   ".*", (True, True))
+              , ("test/contracts/pass/revertString.sol",  ".*", (True, True))
+              , ("test/contracts/pass/requireEmpty.sol",  ".*", (True, True))
+              , ("test/contracts/pass/requireString.sol", ".*", (True, True))
+              , ("test/contracts/fail/trivial.sol",       ".*", (False, False))
+              , ("test/contracts/fail/dsProveFail.sol",   "prove_add", (False, True))
+              , ("test/contracts/fail/dsProveFail.sol",   "prove_multi", (False, True))
+              -- all branches revert, which is a warning
+              , ("test/contracts/fail/dsProveFail.sol",   "prove_trivial.*", (False, False))
+              , ("test/contracts/fail/dsProveFail.sol",   "prove_distributivity", (False, True))
+              , ("test/contracts/fail/assertEq.sol",      ".*", (False, True))
+              -- bad cheatcode detected, hence the warning
+              , ("test/contracts/fail/bad-cheatcode.sol", ".*", (False, False))
               ]
         forM_ cases $ \(testFile, match, expected) -> do
           actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing Foundry
-          putStrLnM $ "Test result for " <> testFile <> ": " <> show actual
+          putStrLnM $ "Test result for " <> testFile <> " match: " <> T.unpack match <> ": " <> show actual
           assertEqualM "Must match" actual  expected
     , test "Trivial-Fail" $ do
         let testFile = "test/contracts/fail/trivial.sol"
@@ -1794,10 +1806,6 @@ tests = testGroup "hevm"
     , test "transfer-dapp" $ do
         let testFile = "test/contracts/pass/transfer.sol"
         runSolidityTest testFile "prove_transfer" >>= assertEqualM "should prove transfer" (True, True)
-    , test "badvault-sym-branch" $ do
-        let testFile = "test/contracts/fail/10_BadVault.sol"
-        runSolidityTestCustom testFile "prove_BadVault_usingExploitLaunchPad"  Nothing Nothing True Nothing Foundry >>=
-          assertEqualM "Must find counterexample" (False, True)
     , test "Prove-Tests-Fail" $ do
         let testFile = "test/contracts/fail/dsProveFail.sol"
         runSolidityTest testFile "prove_trivial" >>= assertEqualM "prove_trivial" (False, False)