Skip to content

Commit

Permalink
Merge pull request #458 from rex4539/typos
Browse files Browse the repository at this point in the history
Fix typos
  • Loading branch information
msooseth authored Feb 22, 2024
2 parents a0af750 + f6685fe commit 7a8a48d
Show file tree
Hide file tree
Showing 14 changed files with 45 additions and 45 deletions.
2 changes: 1 addition & 1 deletion hevm.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
12 changes: 6 additions & 6 deletions src/EVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
_ ->
Expand Down Expand Up @@ -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 }
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/EVM/ABI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 16 additions & 16 deletions src/EVM/Expr.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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


Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
--
--
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/EVM/Keccak.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions src/EVM/SMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/EVM/Solidity.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
4 changes: 2 additions & 2 deletions src/EVM/Solvers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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)

Expand Down
6 changes: 3 additions & 3 deletions src/EVM/SymExec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ _ _ -> []
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/EVM/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions test/EVM/Test/Tracing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
-}
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/contracts/pass/dsProvePass.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion test/contracts/pass/transfer.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
Expand Down
4 changes: 2 additions & 2 deletions test/test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down Expand Up @@ -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|
Expand Down

0 comments on commit 7a8a48d

Please sign in to comment.