Solidity v0.8.1 introduces many new features for the SMTChecker (see below), updates the emscripten version for building soljson.js to 2.0.12, allows to catch panic errors and adds other small improvements.

Notable New Features

SMTChecker Counterexamples and Synthesis of External Functions

The SMTChecker already reports transaction traces as counterexamples to failing verification targets, but 0.8.1 adds internal calls, msg.value and synthesized unknown code called externally in the form of reentrant calls to counterexamples. A recent blog post presents that topic in more detail.

How to select SMTChecker targets

Prior to 0.8.1, the SMTChecker would automatically create verification targets for all types. Now the user can choose which verification targets should be checked via the CLI option --model-checker-targets, or the standard JSON setting modelCheckerSettings.targets. The valid target strings are underflow, overflow, divByZero, constantCondition, balance, popEmptyArray and assert. Multiple targets can be chosen simultaneously separated by a comma, without spaces: underflow,overflow,assert. For a detailed description of the verification targets, please see the SMTChecker docs.

Catch Panic

The Panic(uint) revert error was introduced with 0.8.0, but there was not yet a way to catch and decode such an error in a try/catch statement. This has been added now:

try otherContract.f() { }
catch Panic(uint _code) {
  if (_code == 0x01) { revert("Assertion failed"); }
  else if (_code == 0x11) { revert ("Underflow/overflow"); }
  // We ignore the other errors.
}

If you neither have a catch Panic(uint) clause nor a catch clause without error type in your try/catch statement, the revert will “bubble up”, i.e. the calling contract will revert.

Regardless of whether or not you catch the error, the effects of the call will always be reverted.

Note that you cannot know whether the error happened in the called contract (otherContract) itself or in a contract called from otherContract.

Code Length Shortcut

From v0.8.0 on, the size of the code at address a could be accessed by using a.code.length. However, this involved copying the code to memory, even if you did not use a.code. In this release, a shortcut was implemented that directly returns the value of extcodesize(<address>) and avoids copying code to memory.

Full Changelog

Language Features:

  • Possibility to use catch Panic(uint code) to catch a panic failure from an external call.

Compiler Features:

  • Code Generator: Reduce the cost of <address>.code.length by using extcodesize directly.
  • Command Line Interface: Allow = as separator between library name and address in --libraries commandline option.
  • Command Line Interface: New option --model-checker-targets allows specifying which targets should be checked. The valid options are all, constantCondition, underflow, overflow, divByZero, balance, assert, popEmptyArray, where the default is all. Multiple targets can be chosen at the same time, separated by a comma without spaces: underflow,overflow,assert.
  • Command Line Interface: Only accept library addresses with a prefix of 0x in --libraries commandline option.
  • Optimizer: Add rule to replace iszero(sub(x,y)) by eq(x,y).
  • Parser: Report meaningful error if parsing a version pragma failed.
  • SMTChecker: Output internal and trusted external function calls in a counterexample’s transaction trace.
  • SMTChecker: Show msg.value in counterexample transaction traces when greater than 0.
  • SMTChecker: Show contract name in counterexample function call.
  • SMTChecker: Support ABI functions as uninterpreted functions.
  • SMTChecker: Support try/catch statements.
  • SMTChecker: Synthesize untrusted functions called externally.
  • SMTChecker: Use checked arithmetic by default and support unchecked blocks.
  • Standard JSON: New option modelCheckerSettings.targets allows specifying which targets should be checked. The valid options are all, constantCondition, underflow, overflow, divByZero, balance, assert, popEmptyArray, where the default is all. Multiple targets can be chosen at the same time, separated by a comma without spaces: underflow,overflow,assert.

Bugfixes:

  • Code Generator: Fix length check when decoding malformed error data in catch clause.
  • Control Flow Graph: Fix missing error caused by read from/write to uninitialized variables.
  • SMTChecker: Fix false negatives in overriding modifiers and functions.
  • SMTChecker: Fix false negatives in the presence of inline assembly.
  • SMTChecker: Fix false negatives when analyzing external function calls.
  • SMTChecker: Fix internal error on block.chainid.
  • SMTChecker: Fix internal error on pushing string literal to bytes array.
  • SMTChecker: Fix missing type constraints for block variables.
  • Type Checker: Fix infinite loop when accessing circular constants from inline assembly.
  • Type Checker: Fix internal error caused by constant structs containing mappings.
  • Type System: Disallow implicit conversion from uintN to intM when M > N, and by extension, explicit conversion between the same types is also disallowed.

Build System:

  • Update the soljson.js build to emscripten 2.0.12 and boost 1.75.0.

A big thank you to all contributors who helped make this release possible!

Download the new version of Solidity here.