From f6685fe258f28cf85af321d9bb8fe928538bd188 Mon Sep 17 00:00:00 2001 From: Dimitris Apostolou Date: Thu, 22 Feb 2024 17:38:17 +0200 Subject: [PATCH] Fix typos --- hevm.cabal | 2 +- src/EVM.hs | 12 +++++------ src/EVM/ABI.hs | 2 +- src/EVM/Expr.hs | 32 ++++++++++++++--------------- src/EVM/Keccak.hs | 2 +- src/EVM/SMT.hs | 6 +++--- src/EVM/Solidity.hs | 2 +- src/EVM/Solvers.hs | 4 ++-- src/EVM/SymExec.hs | 6 +++--- src/EVM/Types.hs | 8 ++++---- test/EVM/Test/Tracing.hs | 6 +++--- test/contracts/pass/dsProvePass.sol | 2 +- test/contracts/pass/transfer.sol | 2 +- test/test.hs | 4 ++-- 14 files changed, 45 insertions(+), 45 deletions(-) diff --git a/hevm.cabal b/hevm.cabal index b07cf56e7..be62bcc2a 100644 --- a/hevm.cabal +++ b/hevm.cabal @@ -328,7 +328,7 @@ test-suite test main-is: test.hs --- these tests require network access so we split them into a seperate test +-- these tests require network access so we split them into a separate test -- suite to make it easy to skip them when running nix-build test-suite rpc-tests import: diff --git a/src/EVM.hs b/src/EVM.hs index dc5b053f8..8533ecfe9 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -375,7 +375,7 @@ exec1 = do OpShr -> stackOp2 g_verylow Expr.shr OpSar -> stackOp2 g_verylow Expr.sar - -- more accurately refered to as KECCAK + -- more accurately referred to as KECCAK OpSha3 -> case stk of xOffset:xSize:xs -> @@ -997,7 +997,7 @@ callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize x next else continue (toGas gas') case (fromBal, xValue) of - -- we're not transfering any value, and can skip the balance check + -- we're not transferring any value, and can skip the balance check (_, Lit 0) -> burn (cost - gas') checkCallDepth -- from is in the state, we check if they have enough balance @@ -1376,7 +1376,7 @@ finalize = do case Expr.toList output of Nothing -> partial $ - UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" (wrap [output]) + UnexpectedSymbolicArg pc' "runtime code cannot have an abstract length" (wrap [output]) Just ops -> onContractCode $ RuntimeCode (SymbolicRuntimeCode ops) _ -> @@ -1683,7 +1683,7 @@ cheatActions = let callerAddr = vm.state.caller fetchAccount contractAddr $ \contractAcct -> fetchAccount callerAddr $ \callerAcct -> do let - -- the current contract is persited across forks + -- the current contract is persisted across forks newContracts = Map.insert callerAddr callerAcct $ Map.insert contractAddr contractAcct forkState.env.contracts newEnv = (forkState.env :: Env) { contracts = newContracts } @@ -1893,7 +1893,7 @@ create self this xSize xGas xValue xs newAddr initCode = do -- concrete region (initCode) followed by a potentially symbolic region -- (arguments). -- --- when constructing a contract that has symbolic construcor args, we +-- when constructing a contract that has symbolic constructor args, we -- need to apply some heuristics to convert the (unstructured) initcode -- in memory into this structured representation. The (unsound, bad, -- hacky) way that we do this, is by: looking for the first potentially @@ -2418,7 +2418,7 @@ vmOpIx vm = do self <- currentContract vm self.opIxMap SV.!? vm.state.pc --- Maps operation indicies into a pair of (bytecode index, operation) +-- Maps operation indices into a pair of (bytecode index, operation) mkCodeOps :: ContractCode -> V.Vector (Int, Op) mkCodeOps contractCode = let l = case contractCode of diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs index 6dc9eb756..083ce0d64 100644 --- a/src/EVM/ABI.hs +++ b/src/EVM/ABI.hs @@ -24,7 +24,7 @@ Nested sequences are encoded recursively with no special treatment. - Calldata args are encoded as heterogenous sequences sans length prefix. + Calldata args are encoded as heterogeneous sequences sans length prefix. -} module EVM.ABI diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index a14439dd1..178610587 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -205,11 +205,11 @@ sar = op2 SAR (\x y -> -- | Extracts the byte at a given index from a Buf. -- -- We do our best to return a concrete value wherever possible, but fallback to --- an abstract expresion if nescessary. Note that a Buf is an infinite +-- an abstract expression if necessary. Note that a Buf is an infinite -- structure, so reads outside of the bounds of a ConcreteBuf return 0. This is -- inline with the semantics of calldata and memory, but not of returndata. --- fuly concrete reads +-- fully concrete reads readByte :: Expr EWord -> Expr Buf -> Expr Byte readByte (Lit x) (ConcreteBuf b) = if x <= unsafeInto (maxBound :: Int) && i < BS.length b @@ -235,7 +235,7 @@ readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst then readByte (Lit $ x - (dstOffset - srcOffset)) src else readByte i dst readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) (Lit size) _ dst) - -- the byte we are trying to read is compeletely outside of the sliced region + -- the byte we are trying to read is completely outside of the sliced region = if x - dstOffset >= size then readByte i dst else ReadByte (Lit x) buf @@ -269,7 +269,7 @@ readWord idx b@(WriteWord idx' val buf) readWord (Lit idx) b@(CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst) -- the region we are trying to read is enclosed in the sliced region | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src - -- the region we are trying to read is compeletely outside of the sliced region + -- the region we are trying to read is completely outside of the sliced region | (idx - dstOff) >= size && (idx - dstOff) <= (maxBound :: W256) - 31 = readWord (Lit idx) dst -- the region we are trying to read partially overlaps the sliced region | otherwise = readWordFromBytes (Lit idx) b @@ -343,7 +343,7 @@ copySlice a@(Lit srcOffset) b@(Lit dstOffset) c@(Lit size) d@(ConcreteBuf src) e -- copying 32 bytes can be rewritten to a WriteWord on dst (e.g. CODECOPY of args during constructors) copySlice srcOffset dstOffset (Lit 32) src dst = writeWord dstOffset (readWord srcOffset src) dst --- concrete indicies & abstract src (may produce a concrete result if we are +-- concrete indices & abstract src (may produce a concrete result if we are -- copying from a concrete region of src) copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf dst) | dstOffset < maxBytes, size < maxBytes, srcOffset + (size-1) > srcOffset = let @@ -355,7 +355,7 @@ copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf else CopySlice s d sz src ds | otherwise = CopySlice s d sz src ds --- abstract indicies +-- abstract indices copySlice srcOffset dstOffset size src dst = CopySlice srcOffset dstOffset size src dst @@ -412,7 +412,7 @@ writeWord offset val src = WriteWord offset val src -- | Returns the length of a given buffer -- -- If there are any writes to abstract locations, or CopySlices with an --- abstract size or dstOffset, an abstract expresion will be returned. +-- abstract size or dstOffset, an abstract expression will be returned. bufLength :: Expr Buf -> Expr EWord bufLength = bufLengthEnv mempty False @@ -473,12 +473,12 @@ concretePrefix b = V.create $ do inputLen = case bufLength b of Lit s -> if s > maxIdx then internalError "concretePrefix: input buffer size exceeds 500mb" - -- unafeInto: s is <= 500,000,000 + -- unsafeInto: s is <= 500,000,000 else Just (unsafeInto s) _ -> Nothing - -- recursively reads succesive bytes from `b` until we reach a symbolic - -- byte returns the larged index read from and a reference to the mutable + -- recursively reads successive bytes from `b` until we reach a symbolic + -- byte returns the large index read from and a reference to the mutable -- vec (might not be the same as the input because of the call to grow) go :: forall s . Int -> MVector s Word8 -> ST s (Int, MVector s Word8) go i v @@ -529,7 +529,7 @@ toList buf = case bufLength buf of fromList :: V.Vector (Expr Byte) -> Expr Buf fromList bs = case Prelude.and (fmap isLitByte bs) of True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByte $ bs - -- we want to minimize the size of the resulting expresion, so we do two passes: + -- we want to minimize the size of the resulting expression, so we do two passes: -- 1. write all concrete bytes to some base buffer -- 2. write all symbolic writes on top of this buffer -- this is safe because each write in the input vec is to a single byte at a distinct location @@ -640,7 +640,7 @@ readStorage w st = go (simplify w) st -- the chance of adding a value <= 2^32 to any given keccack output -- leading to an overflow is effectively zero. the chance of an overflow - -- occuring here is 2^32/2^256 = 2^-224, which is close enough to zero + -- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero -- for our purposes. This lets us completely simplify reads from write -- chains involving writes to arrays at literal offsets. (Lit a, Add (Lit b) (Keccak _) ) | a < 256, b < maxW32 -> go slot prev @@ -1147,7 +1147,7 @@ simplifyProp prop = where go :: Prop -> Prop - -- LT/LEq comparisions + -- LT/LEq comparisons go (PLT (Var _) (Lit 0)) = PBool False go (PLEq (Lit 0) (Var _)) = PBool True go (PLT (Lit val) (Var _)) | val == maxLit = PBool False @@ -1298,7 +1298,7 @@ indexWord :: Expr EWord -> Expr EWord -> Expr Byte -- Simplify masked reads: -- -- --- reads across the mask boundry +-- reads across the mask boundary -- return an abstract expression -- │ -- │ @@ -1322,7 +1322,7 @@ indexWord :: Expr EWord -> Expr EWord -> Expr Byte -- indexWord 31 reads from the LSB -- indexWord i@(Lit idx) e@(And (Lit mask) w) - -- if the mask is all 1s then read from the undelrying word + -- if the mask is all 1s then read from the underlying word -- we need this case to avoid overflow | mask == fullWordMask = indexWord (Lit idx) w -- if the index is a read from the masked region then read from the underlying word @@ -1337,7 +1337,7 @@ indexWord i@(Lit idx) e@(And (Lit mask) w) , isByteAligned mask , idx < unmaskedBytes = LitByte 0 - -- if the mask is not a power of 2, or it does not align with a byte boundry return an abstract expression + -- if the mask is not a power of 2, or it does not align with a byte boundary return an abstract expression | idx <= 31 = IndexWord i e -- reads outside the range of the source word return 0 | otherwise = LitByte 0 diff --git a/src/EVM/Keccak.hs b/src/EVM/Keccak.hs index 10b9ec2f2..fe479c64a 100644 --- a/src/EVM/Keccak.hs +++ b/src/EVM/Keccak.hs @@ -65,7 +65,7 @@ injProp (k1@(Keccak b1), k2@(Keccak b2)) = injProp _ = internalError "expected keccak expression" --- Takes a list of props, find all keccak occurences and generates two kinds of assumptions: +-- Takes a list of props, find all keccak occurrences and generates two kinds of assumptions: -- 1. Minimum output value: That the output of the invocation is greater than -- 256 (needed to avoid spurious counterexamples due to storage collisions -- with solidity mappings & value type storage slots) diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index d44847903..a6bdf5fae 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -119,7 +119,7 @@ flattenBufs cex = do bs <- mapM collapse cex.buffers pure $ cex{ buffers = bs } --- | Attemps to collapse a compressed buffer representation down to a flattened one +-- | Attempts to collapse a compressed buffer representation down to a flattened one collapse :: BufModel -> Maybe BufModel collapse model = case toBuf model of Just (ConcreteBuf b) -> Just $ Flat b @@ -696,7 +696,7 @@ exprToSMT = \case Mul a b -> op2 "bvmul" a b Exp a b -> case b of Lit b' -> expandExp a b' - _ -> internalError "cannot encode symbolic exponentation into SMT" + _ -> internalError "cannot encode symbolic exponentiation into SMT" Min a b -> let aenc = exprToSMT a benc = exprToSMT b in @@ -1099,7 +1099,7 @@ getBufs getVal bufs = foldM getBuf mempty bufs p -> parseErr p -- | Takes a Map containing all reads from a store with an abstract base, as --- well as the conrete part of the storage prestate and returns a fully +-- well as the concrete part of the storage prestate and returns a fully -- concretized storage getStore :: (Text -> IO Text) diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs index 47d2b7d8c..b1b33da2c 100644 --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -282,7 +282,7 @@ makeSrcMaps = (\case (_, Fe, _) -> Nothing; x -> Just (done x)) go c (xs, state, p) = (xs, internalError ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p) --- | Reads all solc ouput json files found under the provided filepath and returns them merged into a BuildOutput +-- | Reads all solc output json files found under the provided filepath and returns them merged into a BuildOutput readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput) readBuildOutput root DappTools = do let outDir = root "out" diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs index 1b1612a07..0a7bf54eb 100644 --- a/src/EVM/Solvers.hs +++ b/src/EVM/Solvers.hs @@ -253,7 +253,7 @@ mkTimeout t = T.pack $ show $ (1000 *)$ case t of Nothing -> 300 :: Natural Just t' -> t' --- | Arguments used when spawing a solver instance +-- | Arguments used when spawning a solver instance solverArgs :: Solver -> Maybe Natural -> [Text] solverArgs solver timeout = case solver of Bitwuzla -> @@ -299,7 +299,7 @@ spawnSolver solver timeout = do pure solverInstance Custom _ -> pure solverInstance --- | Cleanly shutdown a running solver instnace +-- | Cleanly shutdown a running solver instance stopSolver :: SolverInstance -> IO () stopSolver (SolverInstance _ stdin stdout process) = cleanupProcess (Just stdin, Just stdout, Nothing, process) diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 1a5342218..495c7d3a3 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -521,7 +521,7 @@ reachable solvers e = do Unsat -> pure ([query], Nothing) r -> internalError $ "Invalid solver result: " <> show r --- | Extract contraints stored in Expr End nodes +-- | Extract constraints stored in Expr End nodes extractProps :: Expr End -> [Prop] extractProps = \case ITE _ _ _ -> [] @@ -838,7 +838,7 @@ formatCex cd sig m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $ where -- we attempt to produce a model for calldata by substituting all variables -- and buffers provided by the model into the original calldata expression. - -- If we have a concrete result then we diplay it, otherwise we diplay + -- If we have a concrete result then we display it, otherwise we display -- `Any`. This is a little bit of a hack (and maybe unsound?), but we need -- it for branches that do not refer to calldata at all (e.g. the top level -- callvalue check inserted by solidity in contracts that don't have any @@ -915,7 +915,7 @@ prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ") -- | If the expression contains any symbolic values, default them to some -- concrete value The intuition here is that if we still have symbolic values --- in our calldata expression after substituing in our cex, then they can have +-- in our calldata expression after substituting in our cex, then they can have -- any value and we can safely pick a random value. This is a bit unsatisfying, -- we should really be doing smth like: https://github.com/ethereum/hevm/issues/334 -- but it's probably good enough for now diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index 81a8c9bf5..fbf5e9288 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -69,7 +69,7 @@ mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256 -- Conversions ------------------------------------------------------------------------------------- --- We ignore hlint to supress the warnings about `fromIntegral` and friends here +-- We ignore hlint to suppress the warnings about `fromIntegral` and friends here #ifndef __HLINT__ instance From Addr Integer where from = fromIntegral @@ -131,7 +131,7 @@ data EType | End deriving (Typeable) --- Variables refering to a global environment +-- Variables referring to a global environment data GVar (a :: EType) where BufVar :: Int -> GVar Buf StoreVar :: Int -> GVar Storage @@ -141,7 +141,7 @@ deriving instance Eq (GVar a) deriving instance Ord (GVar a) {- | - Expr implements an abstract respresentation of an EVM program + Expr implements an abstract representation of an EVM program This type can give insight into the provenance of a term which is useful, both for the aesthetic purpose of printing terms in a richer way, but also to @@ -1379,7 +1379,7 @@ formatString bs = Right s -> "\"" <> T.unpack s <> "\"" Left _ -> "❮utf8 decode failed❯: " <> (show $ ByteStringS bs) --- |'paddedShowHex' displays a number in hexidecimal and pads the number +-- |'paddedShowHex' displays a number in hexadecimal and pads the number -- with 0 so that it has a minimum length of @w@. paddedShowHex :: (Show a, Integral a) => Int -> a -> String paddedShowHex w n = pad ++ str diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs index 5d0ba62dc..4c55745cb 100644 --- a/test/EVM/Test/Tracing.hs +++ b/test/EVM/Test/Tracing.hs @@ -6,7 +6,7 @@ Module : Tracing Description : Tests to fuzz concrete tracing, and symbolic execution Functions here are used to generate traces for the concrete -execution of HEVM and check that against evmtool from go-ehereum. Re-using some +execution of HEVM and check that against evmtool from go-ethereum. Re-using some of this code, we also generate a symbolic expression then evaluate it concretely through Expr.simplify, then check that against evmtool's output. -} @@ -377,7 +377,7 @@ compareTraces hevmTrace evmTrace = go hevmTrace evmTrace pure False go [] [b] = do -- evmtool produces ONE more trace element of the error - -- hevm on the other hand stops and doens't produce one more + -- hevm on the other hand stops and doesn't produce one more if isJust b.error then pure True else do putStrLn $ "Traces don't match. HEVM's trace is longer by:" <> (show b) @@ -605,7 +605,7 @@ removeExtcalls (OpContract ops) = OpContract (filter (noStorageNoExtcalls) ops) where noStorageNoExtcalls :: Op -> Bool noStorageNoExtcalls o = case o of - -- Extrenal info functions + -- External info functions OpExtcodecopy -> False OpExtcodehash -> False OpExtcodesize -> False diff --git a/test/contracts/pass/dsProvePass.sol b/test/contracts/pass/dsProvePass.sol index 4da25eb24..da9a60df4 100644 --- a/test/contracts/pass/dsProvePass.sol +++ b/test/contracts/pass/dsProvePass.sol @@ -75,7 +75,7 @@ contract SolidityTest is DSTest { } function prove_burn(uint supply, uint amt) public { - if (amt > supply) return; // no undeflow + if (amt > supply) return; // no underflow token.mint(address(this), supply); token.burn(address(this), amt); diff --git a/test/contracts/pass/transfer.sol b/test/contracts/pass/transfer.sol index b72af9b18..884ec85d5 100644 --- a/test/contracts/pass/transfer.sol +++ b/test/contracts/pass/transfer.sol @@ -19,7 +19,7 @@ contract SolidityTestFail2 is DSTest { uint expected = usr == address(this) ? 0 // self transfer is a noop - : amt; // otherwise `amt` has been transfered to `usr` + : amt; // otherwise `amt` has been transferred to `usr` assert(expected == postbal - prebal); } } diff --git a/test/test.hs b/test/test.hs index d5dbb99fc..f7102e7df 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1323,7 +1323,7 @@ tests = testGroup "hevm" } |] let sig = Just $ Sig "fun(uint256)" [AbiUIntType 256] - -- we dont' ask the solver about the loop condition until we're + -- we don't ask the solver about the loop condition until we're -- already in an inconsistent path (i == 5, j <= 3, i < j), so we -- will continue looping here until we hit max iterations opts = defaultVeriOpts{ maxIter = Just 10, askSmtIters = 5 } @@ -2375,7 +2375,7 @@ tests = testGroup "hevm" assertBoolM "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0 putStrLnM "Expected counterexample found" , - -- Reverse of thest above + -- Reverse of test above test "check-lsb-msb4 2nd byte rev" $ do Just c <- solcRuntime "C" [i|