scribble

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.

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.

This patch release adds just 2 pieces of additional instrumentation metadata (#179 ):

• the text of the original annotation
• the names of variables in the debugEventEncoding

This release brings fixes for:

- using Counters.Counter #174
- Cannot find module 'path/posix' #175

This release contains:

• new --base-path and --include-paths arguments to Scribble. These 2 arguments are passed down to solc when compiling code to obtain an AST.
• Fix for a small bug in the grammar of fixed bytes type in Scribble (#173 )

This release contains:

• bump solc-typed-ast to 9.1.3
• change scribble to use the better multi-file compiling support in solc-typed-ast (#164)
• removed (now) obsolete merging and sanity checking logic

This release features:

• Fix a remaining issue with #160 from the previous 0.6.6 release - when running scribble through the fuzz command we were still placing the utils file in the wrong place
• Fix for Scribble doesn't correctly handle visiblity for private state vars (#163 )
• Better support for Solidity 0.8.13 (#162)

This release contains:

• Place utils contracts under node_modules when package remapping is present (Fixes #160)
• Bump solc-typed-ast to v9.1.1 (Fixes #155)

This release brings the following improvements:

• bump nodejs version to v16 LTS
• bump solc-typed-ast to v9.0.0
• [EXPERIMENTAL] add support for # let x := ...; annotations before a statement
• [EXPERIMENTAL] add support for if_succeeds annotation on a statement or code block
• change default Solidity compiler from WASM to native
• Add new --compiler-kind command line option allowing to select which compiler to use (native or wasm)
• Disallow arrays and maps in old() statements

WARNING: 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.

This patch release contains a single fix for:

#149 scribble produces invalid code given a constant let-binding used in a new context

This release contains the following fixes;

• Support annotation label short-hand with just a string (#138)
• Add macro standard library support (#139), add macro definitions for ERC20, ERC721
• Fix crash in ^0.8.4 due to revert statements (#147)
• Fix crash in annotations with $result[i] (#145)

This release brings:

• Support for Solidity 0.8.8, 0.8.9, 0.8.10
• Fix for #132 - Multitple 'AssertionFailed' events inserted in inheritance
• Fix for #131 - ErrorDefinition nodes not supported in merging
• Fix for #119 - Disarm fails when instrumented code fails to compile

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

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

This PR introduces 2 new small language features, and several bug fixes.

1. Language Features:

• #123 Support abi.encodePacked in scribble

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) {
      ...
   }
}

• #93 Support require-annotations to guide tools

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:

1. #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.

2. #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.

2. Instrumentation/command line options:

• #106 Add optional assertions for checking property coverage

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.

3. Bug Fixes:

• #121 Scribble grammar unnecessarily requires forall be wrapped in parenthesis
• #104 forall broken in new #limit annotation
• #103 Broken instrumentation for overriding public variables
• #101 Type-checker needs to support library-level constants
• #100 When interposing on constructors super constructor invocations get put on the wrong function.
• #99 Don't apply contract-level if_succeeds annotations to view functions
• #98 Unable to use forall on arrays with elements of used-defined type
• #89 if_updated annotations lost when mixing in forall annotations
• #88 Scribble crashes when mixing for_all and if_updated on nested mappings

This release includes fixes for the following issues:

• #85 Scribble crashes in the presence of assignments from storage pointers to storage pointers
• #86 Scribble needs to disallow equality comparisons between reference types

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.

This PR adds:

Language Features:

• Support for assertions in side functions with the new #assert

CLI:

• Adds a new --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)
• Change debug event signatures format in instrumentation metadata to be more generic, and handle cases where multiple shadowing identifiers are present in annotations

Bug Fixes:

• Fix crash when instrumenting code with public variable accessor calls
• Fix crash when tuples in ternary operators are encountered
• Fix crash on circular imports
• Fix crash when both InheritanceSpecifiers and ModifierInvocations for the same base contract are present
• Fix incorrect handling of imports in Scribble
• Fix bug in arming code with cutom maps and solidty < 0.8.6

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.

This release brings:

1. Support for Solidity 0.8.4, 0.8.5 and 0.8.6

2. Extends the universal quantification support to work over maps. (i.e. forall (address a in m) ... where m is a map works now)

3. 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.

4. 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.).

5. Fixed a bug in debug events where identifiers appearing inside of old(...) expressions had their new value reported erroneously.

6. Cleanup of InstrumentationContext and smaller fixes.