diff --git a/flake.lock b/flake.lock index 41838511..774f1174 100644 --- a/flake.lock +++ b/flake.lock @@ -3,11 +3,11 @@ "cabal-head": { "flake": false, "locked": { - "lastModified": 1691811891, - "narHash": "sha256-e/dXo93pNSva1aKDpuO392Nig1M51Us96Qm0Peb/3bQ=", + "lastModified": 1693777827, + "narHash": "sha256-zMwVwTztoQGrNIJSxSdVJjYN77rleRjpC+K5AoIl7po=", "owner": "haskell", "repo": "cabal", - "rev": "e77f13945d66fb829525c7249d97a6ad29fc701b", + "rev": "24a4603eebfcf7730f00bb69a02d1568990798d5", "type": "github" }, "original": { @@ -54,11 +54,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1681202837, - "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -68,12 +68,15 @@ } }, "flake-utils_2": { + "inputs": { + "systems": "systems_2" + }, "locked": { - "lastModified": 1678901627, - "narHash": "sha256-U02riOqrKKzwjsxc/400XnElV+UtPUQWpANPlyazjH0=", + "lastModified": 1692799911, + "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", "owner": "numtide", "repo": "flake-utils", - "rev": "93a2b84fc4b70d9e089d029deacc3583435c2ed6", + "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", "type": "github" }, "original": { @@ -103,11 +106,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1677921223, - "narHash": "sha256-TsrPW+VfLu19dYm4uuAaM9LLHm30iZiyW1+0mbFgwbk=", + "lastModified": 1691140388, + "narHash": "sha256-AH3fx2VFGPRSOjnuakab4T4AdUstwTnFTbnkoU4df8Q=", "owner": "shazow", "repo": "foundry.nix", - "rev": "79df1481c10789570c40749a4c8f8aada16f2eea", + "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", "type": "github" }, "original": { @@ -130,11 +133,11 @@ "solidity": "solidity" }, "locked": { - "lastModified": 1695059034, - "narHash": "sha256-LqQBLQ5Pl2xDUKqiiRF1iGRWFxTlgrf4SemusvxsnBM=", + "lastModified": 1697630766, + "narHash": "sha256-mIjEe8hBILwGCiBX9eD7eQcpu364BTNSMA0fCSqF2ao=", "owner": "ethereum", "repo": "hevm", - "rev": "fb7c953cc108f7b2350d1e8ab7212dcf38f309f2", + "rev": "3a52ccf6571106ce80f5528a9a0bc3ed2af26681", "type": "github" }, "original": { @@ -159,11 +162,11 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1684164265, - "narHash": "sha256-ZqNSKSQM12040taiRvSgqwUCPlN1qZAw6nYniYuY1hs=", + "lastModified": 1697718011, + "narHash": "sha256-B72Ah61jRrtVKBgMgxcD9cyx9ApLuzEGQO7GoSpE8qc=", "owner": "nixos", "repo": "nixpkgs", - "rev": "872c89e5a754a04058b4531e54897db5ca734100", + "rev": "ef6f366a9585853405a88e52c933df81d0396e65", "type": "github" }, "original": { @@ -210,6 +213,21 @@ "repo": "default", "type": "github" } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/src/CLI.hs b/src/CLI.hs index b9c29702..d4a56e9f 100644 --- a/src/CLI.hs +++ b/src/CLI.hs @@ -238,10 +238,10 @@ hevm actspec cid sol' code' initcode' solver' timeout debug' = do bytecodes :: Text -> Text -> IO (BS.ByteString, BS.ByteString) bytecodes cid src = do - (json, path) <- solidity' src + json <- solc Solidity src let (Contracts sol', _, _) = fromJust $ readStdJSON json - pure $ ((fromJust . Map.lookup (path <> ":" <> cid) $ sol').creationCode, - (fromJust . Map.lookup (path <> ":" <> cid) $ sol').runtimeCode) + pure $ ((fromJust . Map.lookup ("hevm.sol" <> ":" <> cid) $ sol').creationCode, + (fromJust . Map.lookup ("hevm.sol" <> ":" <> cid) $ sol').runtimeCode) diff --git a/src/HEVM.hs b/src/HEVM.hs index 11ec795d..d4f8509c 100644 --- a/src/HEVM.hs +++ b/src/HEVM.hs @@ -35,7 +35,8 @@ import Syntax.Annotated import Syntax.Untyped (makeIface) import Syntax -import qualified EVM.Types as EVM hiding (Contract(..)) +import EVM.ABI (Sig(..)) +import qualified EVM.Types as EVM hiding (Contract(..), FrameState(..)) import EVM.Expr hiding (op2, inRange) import EVM.SymExec hiding (EquivResult, isPartial) import qualified EVM.SymExec as SymExec (EquivResult) @@ -114,19 +115,19 @@ combineFragments' fragments start base = go (EVM.Lit start) fragments (base, []) -- * Act translation -translateActBehvs :: Act -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata)] +translateActBehvs :: Act -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata, Sig)] translateActBehvs (Act store contracts) bytecode = let slots = slotMap store in concatMap (\(Contract _ behvs) -> translateBehvs slots bytecode behvs) contracts -translateActConstr :: Act -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata) +translateActConstr :: Act -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig) translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor (slotMap store) ctor bytecode translateActConstr (Act _ _) _ = error "TODO multiple contracts" -translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata) +translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig) translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode = (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)], - calldata) + calldata, ifaceToSig iface) where calldata = makeCtrCalldata iface initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) @@ -136,15 +137,18 @@ translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode } initmap = M.fromList [(initAddr, initcontract)] -translateBehvs :: Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)] +translateBehvs :: Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata, Sig)] translateBehvs layout bytecode behvs = let groups = (groupBy sameIface behvs) :: [[Behaviour]] in - fmap (\behvs' -> (behvName behvs', fmap (translateBehv layout bytecode) behvs', behvCalldata behvs')) groups + fmap (\behvs' -> (behvName behvs', fmap (translateBehv layout bytecode) behvs', behvCalldata behvs', behvSig behvs)) groups where behvCalldata (Behaviour _ _ iface _ _ _ _ _:_) = makeCalldata iface behvCalldata [] = error "Internal error: behaviour groups cannot be empty" + behvSig (Behaviour _ _ iface _ _ _ _ _:_) = ifaceToSig iface + behvSig [] = error "Internal error: behaviour groups cannot be empty" + -- TODO remove reduntant name in behaviours sameIface (Behaviour _ _ iface _ _ _ _ _) (Behaviour _ _ iface' _ _ _ _ _) = makeIface iface == makeIface iface' @@ -152,6 +156,11 @@ translateBehvs layout bytecode behvs = behvName (Behaviour _ _ (Interface name _) _ _ _ _ _:_) = name behvName [] = error "Internal error: behaviour groups cannot be empty" +ifaceToSig :: Interface -> Sig +ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args) + where + fromdecl (Decl t _) = t + translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) = EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode) @@ -395,15 +404,15 @@ checkEquiv solvers opts l1 l2 = checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Act -> IO () checkConstructors solvers opts initcode runtimecode act = do - let (_, actbehvs, calldata) = translateActConstr act runtimecode + let (_, actbehvs, calldata, sig) = translateActConstr act runtimecode initVM <- stToIO $ abstractVM calldata initcode Nothing True expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr let simpl = if True then (simplify expr) else expr let solbehvs = removeFails $ flattenExpr simpl putStrLn "\x1b[1mChecking if constructor results are equivalent.\x1b[m" - checkResult =<< checkEquiv solvers opts solbehvs actbehvs + checkResult calldata (Just sig) =<< checkEquiv solvers opts solbehvs actbehvs putStrLn "\x1b[1mChecking if constructor input spaces are the same.\x1b[m" - checkResult =<< checkInputSpaces solvers opts solbehvs actbehvs + checkResult calldata (Just sig) =<< checkInputSpaces solvers opts solbehvs actbehvs where removeFails branches = filter isSuccess $ branches @@ -411,15 +420,15 @@ checkConstructors solvers opts initcode runtimecode act = do checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Act -> IO () checkBehaviours solvers opts bytecode act = do let actbehvs = translateActBehvs act bytecode - flip mapM_ actbehvs $ \(name,behvs,calldata) -> do + flip mapM_ actbehvs $ \(name,behvs,calldata,sig) -> do solbehvs <- removeFails <$> getBranches solvers bytecode calldata putStrLn $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m" -- equivalence check putStrLn "\x1b[1mChecking if behaviour is matched by EVM\x1b[m" - checkResult =<< checkEquiv solvers opts solbehvs behvs + checkResult calldata (Just sig) =<< checkEquiv solvers opts solbehvs behvs -- input space exhaustiveness check putStrLn "\x1b[1mChecking if the input spaces are the same\x1b[m" - checkResult =<< checkInputSpaces solvers opts solbehvs behvs + checkResult calldata (Just sig) =<< checkInputSpaces solvers opts solbehvs behvs where removeFails branches = filter isSuccess $ branches @@ -470,7 +479,7 @@ checkAbi solver opts act bytecode = do ("abi-query-" <> show idx <> ".smt2") (formatSMT2 q <> "\n\n(check-sat)") - checkResult =<< fmap (toVRes msg) <$> mapConcurrently (checkSat solver) queries + checkResult (txdata, []) Nothing =<< fmap (toVRes msg) <$> mapConcurrently (checkSat solver) queries where actSig (Behaviour _ _ iface _ _ _ _ _) = T.pack $ makeIface iface @@ -537,8 +546,8 @@ toVRes msg res = case res of Error e -> error $ "Internal Error: solver responded with error: " <> show e -checkResult :: [EquivResult] -> IO () -checkResult res = +checkResult :: Calldata -> Maybe Sig -> [EquivResult] -> IO () +checkResult calldata sig res = case any isCex res of False -> do putStrLn "\x1b[42mNo discrepancies found\x1b[m" @@ -550,5 +559,5 @@ checkResult res = TIO.putStrLn . T.unlines $ [ "\x1b[41mNot equivalent.\x1b[m" , "" , "-----", "" - ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (\(msg, cex) -> msg <> "\n" <> formatCex (EVM.AbstractBuf "txdata") cex) cexs) + ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (\(msg, cex) -> msg <> "\n" <> formatCex (fst calldata) sig cex) cexs) exitFailure diff --git a/src/Lex.x b/src/Lex.x index e39ba6f4..83e4fa41 100644 --- a/src/Lex.x +++ b/src/Lex.x @@ -98,9 +98,9 @@ tokens :- ")" { mk RPAREN } "[" { mk LBRACK } "]" { mk RBRACK } - "=" { mk EQ } - ">" { mk GT } - "<" { mk LT } + "=" { mk Lex.EQ } + ">" { mk Lex.GT } + "<" { mk Lex.LT } ":" { mk COLON } "+" { mk PLUS } "-" { mk MINUS } diff --git a/src/SMT.hs b/src/SMT.hs index 38ac6e45..fd275b20 100644 --- a/src/SMT.hs +++ b/src/SMT.hs @@ -520,6 +520,7 @@ parseSMTModel s = if length s0Caps == 1 s0Caps = getCaptures s stage0 s1Caps = getCaptures (head s0Caps) stage1 + getCaptures :: String -> String -> [String] getCaptures str regex = captures where (_, _, _, captures) = str =~ regex :: (String, String, String, [String])