Skip to content

Fixing checking assert failure #753

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/EVM/SymExec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 15 additions & 3 deletions src/EVM/UnitTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
214 changes: 0 additions & 214 deletions test/contracts/fail/10_BadVault.sol

This file was deleted.

7 changes: 7 additions & 0 deletions test/contracts/fail/assertEq.sol
Original file line number Diff line number Diff line change
@@ -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);
}
}
13 changes: 13 additions & 0 deletions test/contracts/fail/bad-cheatcode.sol
Original file line number Diff line number Diff line change
@@ -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);
}
}
4 changes: 3 additions & 1 deletion test/contracts/fail/dsProveFail.sol
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ contract SolidityTest is Test {
assert(false);
}

function prove_all_branches_fail() public {
function prove_all_branches_revert() public {
require(false);
}

Expand All @@ -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);
Expand Down
11 changes: 11 additions & 0 deletions test/contracts/pass/requireEmpty.sol
Original file line number Diff line number Diff line change
@@ -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;
}
}
11 changes: 11 additions & 0 deletions test/contracts/pass/requireString.sol
Original file line number Diff line number Diff line change
@@ -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;
}
}
7 changes: 7 additions & 0 deletions test/contracts/pass/revertEmpty.sol
Original file line number Diff line number Diff line change
@@ -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();
}
}
7 changes: 7 additions & 0 deletions test/contracts/pass/revertString.sol
Original file line number Diff line number Diff line change
@@ -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");
}
}
26 changes: 17 additions & 9 deletions test/test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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)
Expand Down