Bot releases are hidden (Show)
Published by cd1m0 over 2 years ago
This release brings a new experimental annotation: User constants.
User constants allow to create constants attached to contracts (and their inheritance tree) that can be used in other annotation. For example:
/// #const uint256 H := 60 * 60;
/// #const uint256 D := H * 24;
contract A {
/// #if_succeeds D == H * 24;
function testHD() public {}
}
Please note that this feature is still in its experimental phase, and may undergo changes before its made concrete.
Published by cd1m0 over 2 years ago
This patch tweaks the behavior of the --debug-events
flag. Specifically it changes the order of events emitted such that upon a property failure we first emit an AssertionFailedData
event (containing the values of any variables found in the failing property) and then emit the AssertionFailed
event, that marks the actual assertion failure.
Published by cd1m0 over 2 years ago
This patch release adds just 2 pieces of additional instrumentation metadata (#179 ):
Published by cd1m0 over 2 years ago
This release brings fixes for:
- using Counters.Counter #174
- Cannot find module 'path/posix' #175
Published by cd1m0 over 2 years ago
This release contains:
--base-path
and --include-paths
arguments to Scribble. These 2 arguments are passed down to solc when compiling code to obtain an AST.Published by cd1m0 over 2 years ago
This release contains:
Published by cd1m0 over 2 years ago
This release features:
Published by cd1m0 over 2 years ago
This release contains:
Published by cd1m0 over 2 years ago
This release brings the following improvements:
# let x := ...;
annotations before a statementif_succeeds
annotation on a statement or code block--compiler-kind
command line option allowing to select which compiler to use (native or wasm)old()
statementsWARNING: Features marked as [EXPERIMENTAL] may be changed or even removed in the future. Experiment with them at their own discretion, but for now please don't depend on them for critical annotations until these have been stabilized.
Published by cd1m0 over 2 years ago
This patch release contains a single fix for:
#149 scribble produces invalid code given a constant let-binding used in a new context
Published by cd1m0 over 2 years ago
This release contains the following fixes;
$result[i]
(#145)Published by cd1m0 almost 3 years ago
This release brings:
Published by cd1m0 almost 3 years ago
I forgot to merge develop into master for the 0.6.0 release, so actually all of the contents of 0.6.0 are now in the 0.6.1 release. So again:
NOTE: This release has breaking changes for the annotations language. Namely, the deprecated annotations without a '#' before the first word will now be IGNORED and only a warning will be issued when they are detected. (i.e. /// if_succeeds true will be ignored)
This release contains the following fixes:
Add precaution message at the top of instrumented files, "not to be modified manually"
#125 Change behavior to ignore annotations without a "#" and just issue a warning
#67 Support property specifications in custom NatSpec tags (@custom:scribble #if_succeeds...)
Initial support for scribble macro yaml files
Published by cd1m0 almost 3 years ago
NOTE: This release has breaking changes for the annotations language. Namely, the deprecated annotations without a '#' before the first word will now be IGNORED and only a warning will be issued when they are detected. (i.e. /// if_succeeds true
will be ignored)
This release contains the following fixes:
@custom:scribble #if_succeeds...
)Published by cd1m0 almost 3 years ago
This PR introduces 2 new small language features, and several bug fixes.
scribble
now allows abi.encode
, abi.encodePacked
, abi.encodeWithSelector
and abi.encodeWithSignature
in annotations. E.g.
contract Foo {
/// #if_succeeds keccak256(abi.encode(a,b)) == keccak256(res);
function encodeArgs(uint a, uint b) public returns (bytes memory res) {
...
}
}
Two new annotations were added - #try
and #require
. These can be applied on a specific function, or on a contract (in which case they are applied to all mutable functions in the contract).
These two DO NOT correspond to new property types. Instead they are intended to be used as guidance for any back-end tools
that are directed by branch coverage. Thus they should be used with care and not included in the official specification. Specifically:
#require
- as the name suggest #require <predicate>
gets translated directly as a require(predicate);
at the start of a function.
This is intended to prevent an underlying tool from exploring certain function. A common example we have found was fuzzers
unintentionally upgrading a part of a fuzzed contract system, and thus breaking the whole system. This is not an interesting direction to explore, as users often assume that privileged operations such as upgrade will not be performed maliciously.
#try
- #try <predicate>
is translated as a vacuous if statement:
if (predicate) {
_v.scratch = 0x42;
}
The underlying if statement has no effect, but its branch acts as a hint for underlying tools to try certain values.
For example if we have the following code that attempts to execute a swap on UniswapV2:
function swapSomeTokens(uint amountIn, uint minOut, address[] path, ...) {
...
uniswapV2.swapExactTokensForTokens(amountIn, amountOut, path, ...);
}
And a backend fuzzer exercising the backend code, it may be tricky for the fuzzer to guess valid values for the addresses in path
.
Adding the following annotation:
/// #try (address[0] == <DAI ADDR> || address[0] == <WETH>) && (address[0] == <DAI ADDR> || address[0] == <WETH>);
function swapSomeTokens(uint amountIn, uint minOut, address[] path, ...) {
...
Would generate vacuous if statements in the instrumented code that would guide the fuzzer to trying some valid combinations
of token paths, and thus exploring more of the underlying code.
In certain cases due to bugs/missing debugging data it might be tricky to tell which properties were actually covered.
We've added a new --cov-assertions
flag, that will emit a dummy user assertion for each real assertion, that is emitted if the
real assertion is ever reach. So for example for this code:
contract Foo {
/// #if_succeeds {:msg "P0"} true;
function foo() public {
}
}
The instrumented code would look like:
function foo() public {
_original_Foo_foo();
unchecked {
{
emit AssertionFailed("HIT: 0: P0");
if (!(true)) {
emit AssertionFailed("0: P0");
assert(false);
}
}
}
}
Note that if the users sees the underlying tool report HIT: 0: P0
event is reachable, then the underlying tool
has exercised the property P0
at least once.
forall
be wrapped in parenthesisPublished by cd1m0 about 3 years ago
This release includes fixes for the following issues:
Published by cd1m0 about 3 years ago
This is a patch release that changes scribble behavior to not always generate bytecode when compiling.
Specifically in files and flat mode, ir/bytecode generation will not be performed, thus avoiding unrelated failures due to stack limitation violations without proper optimizer settings for example.
Note that if we are compiling in json mode then bytecode generation will still be performed on the final flattened and instrumented code.
Published by cd1m0 about 3 years ago
This PR adds:
Language Features:
#assert
CLI:
--compiler-settings
flag that allows arbitrary settings to be passed to the underlying solidity compiler (e.g. --compiler-settings '{"optimizer": {"enabled": true, "runs": 200}}'
. Note the use of single and double quotes)Bug Fixes:
Published by cd1m0 about 3 years ago
This is a patch release that fixes a bug introduced in 0.5.2 when instrumenting code with map sums or foralls over maps for solidity code older than 0.8.0. The instrumented code included an unchecked
block, which made it fail to compile.
Published by cd1m0 about 3 years ago
This release brings:
Support for Solidity 0.8.4, 0.8.5 and 0.8.6
Extends the universal quantification support to work over maps. (i.e. forall (address a in m) ...
where m
is a map works now)
Adds the new builtin unchecked_sum()
function, which returns the sum of all values in a numeric map/array. As the name suggests, the sum may overflow, and should be used with carefully.
The debug events emitted with --debug-events
have been changed to a new simpler format, and now support arrays as well as include more identifiers. (forall
iterator vars, path identifiers appearing in if_assigned
, etc.).
Fixed a bug in debug events where identifiers appearing inside of old(...)
expressions had their new value reported erroneously.
Cleanup of InstrumentationContext
and smaller fixes.