Changelog History
Page 1
-
v0.43.0 Changes
November 29, 20200.43.0 - 2020-11-29
โ Added
- ๐จ A
--show-tree
option tohevm symbolic
which prints the execution tree explored. - Some symbolic terms are displayed with richer semantic information, instead of the black box
<symbolic>
. - โ
hevm dapp-test
now supports symbolic execution of test methods that are prefixed withprove
orproveFail
- ๐ The
hevm interactive
alias has been removed, as it is equivalent tohevm dapp-test --debug
- โ
hevm dapp-test --match
now matches on contract name and file path, as well as test name - Step through the callstack in debug mode using the arrow keys
๐ Changed
- โ
dapp-test
trace output now detects ds-note events and showsLogNote
- create addresses are shown with
@<address>
in the trace - โ
DSTest.setUp()
is only run if it exists, rather than failing - support new ds-test
log_named_x(string, x)
(previously bytes32 keys) - return arguments are fully displayed in the trace (previously only a single word)
- โช return/revert trace will now show the correct source position
- ๐จ A
-
v0.42.0
October 31, 2020 -
v0.41.0 Changes
August 19, 2020hevm-0.41.0
๐ Changed
- Switched to PVP for version control, starting now at
0.41.0
(MAJOR.MAJOR.MINOR). - โก๏ธ z3 updated to 4.8.7
- โ
Generate more interesting values in property based testing,
and implement proper shrinking for all abi values. - ๐ Fixed soundness bug when using KECCAK or SHA256 opcode/precompile
- ๐ Fixed an issue in debug mode where backstepping could cause path information to be forgotten
- Ensure that pathconditions are consistent when branching, and end the execution with VMFailure: DeadPath if this is not the case
- ๐ Fixed a soundness bug where nonzero jumpconditions were assumed to equal one.
- 0๏ธโฃ default
--smttimeout
changed from unlimited to 20 seconds hevm symbolic --debug
now respects--max-iterations
โ Added
hevm exec --trace
flag to dump a trace- Faster backstepping in interactive mode by saving multiple snapshot states.
- ๐ Support for symbolic storage for multiple contracts
dapp-0.29.0
โ Added
- ๐ Support for solc 0.6.12 for linux
๐ Fixed
๐ Support for libraries. To test a project which includes libraries you need to use:
DAPP_BUILD_EXTRACT=1 dapp test
seth-0.9.1
โ Added
๐ New commands:
seth source <address>
fetches the contract source from etherscanseth bundle-source <address>
fetches contract source and compiles to combined jsonseth run-tx <tx-hash> [--debug, --source <file>, --state <repository>]
,
set hevm options according to the options given andhevm exec
seth debug <tx-hash> [--no-src]
downloads etherscan source, executes previous txs in block and enters into an hevm interactive session for the given tx.--no-src
skips the first step.seth --{max-uint,max-int,min-int}
print the largest numbers (in hex) of a given bitsizeseth call --hevm
executes a call via hevm, rather than the RPCseth call --debug
executes a call interactively via hevm
-
seth --verbose
prints some seth debugging information to stderrseth block
can now be passed the--full
option, which returns the full block.hexdata can be concatenated with
:
, e.g. '0xaa:0xbb' will be read as '0xaabb'.๐ Changed
seth --to-{hex,wei,word,address,dec,int256,ascii,fix,uint256}
and
seth --from-{ascii,wei}
can now read values from stdin.seth call
now accepts empty calldata and also create transactions
via--create
.seth --abi-function-json
no longer returns a singleton list, but rather the JSON object it contained.- โก๏ธ Updated hevm to 0.41.0
- Switched to PVP for version control, starting now at
-
v0.40.0 Changes
July 22, 2020๐ This release makes hevm capable of symbolic execution, and exposes the new
hevm symbolic
orhevm equivalence
.๐ For more details, check out the announcing post https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/ or consult the README for usage options.
Install as always using nix. Check out installation instructions or in brief:
curl -L https://nixos.org/nix/install | sh . "$HOME/.nix-profile/etc/profile.d/nix.sh" curl https://dapp.tools/install | sh
Full changelog:
0.40 - 2020-07-22
- hevm is now capable of symbolic execution!
๐ Changed
As a result, the types of several registers of the EVM have changed to admit symbolic values as well as concrete ones.
state.stack:
Word
->SymWord
.โ state.memory:
ByteString
->[SWord 8]
.state.callvalue:
W256
->SymWord
.state.caller:
Addr
->SAddr
.โ state.returndata:
ByteString
->[SWord 8]
.โ state.calldata:
ByteString
->([SWord 8], (SWord 32))
. The first element is a list of symbolic bytes, the second is the length of calldata. We havefst calldata !! i .== 0
for allsnd calldata < i
.tx.value:
W256
->SymWord
.contract.storage:
Map Word Word
->Storage
, defined as:data Storage= Concrete (Map Word SymWord) | Symbolic (SArray (WordN 256) (WordN 256)) deriving (Show)
โ Added
๐ New cli commands:
hevm symbolic
: search for assertion violations, or step through a symbolic execution in debug mode.hevm equivalence
: compare two programs for equivalence.
๐ See the README for details on usage.
The new module
EVM.SymExec
exposes several library functions dealing with symbolic execution.
In particular,SymExec.interpret
: implements an operational monad script similar toTTY.interpret
andStepper.interpret
, but returns a list of final VM states rather than a single VM.SymExec.verify
: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition.
โ Removed
The concrete versions of a lot of arithmetic operations, replaced with their more general symbolic counterpart.
-
v0.39.0
July 13, 2020 -
v0.34
August 28, 2019 -
v0.33
August 06, 2019 -
v0.32
June 14, 2019 -
v0.31.0 Changes
November 29, 2020[0.31.0] - 2020-11-29
๐ Changed
- โ
dapp test --match
now matches on file path and contract name, as
โ well as test name dapp --use
searches directly for binaries in your path, rather than
usingnix run
, giving a significant speed boost.
- โ
-
v0.28.0
July 13, 2020