Merge remote-tracking branch 'origin/develop' into breaking

Author: chriseth

.circleci/soltest_all.sh

@@ -28,8 +28,8 @@ set -e
 
 REPODIR="$(realpath "$(dirname "$0")"/..)"
 
-EVM_VALUES=(homestead byzantium constantinople petersburg istanbul berlin)
-DEFAULT_EVM=berlin
+EVM_VALUES=(homestead byzantium constantinople petersburg istanbul berlin london)
+DEFAULT_EVM=london
 [[ " ${EVM_VALUES[*]} " =~ $DEFAULT_EVM ]]
 OPTIMIZE_VALUES=(0 1)
 STEPS=$(( 1 + ${#EVM_VALUES[@]} * ${#OPTIMIZE_VALUES[@]} ))

CMakeLists.txt

@@ -21,7 +21,7 @@ include(EthPolicy)
 eth_policy()
 
 # project name and version should be set after cmake_policy CMP0048
-set(PROJECT_VERSION "0.8.7")
+set(PROJECT_VERSION "0.8.8")
 # OSX target needed in order to support std::visit
 set(CMAKE_OSX_DEPLOYMENT_TARGET "10.14")
 project(solidity VERSION ${PROJECT_VERSION} LANGUAGES C CXX)

Changelog.md

@@ -4,32 +4,49 @@ Breaking changes:
  * `error` is now a keyword that can only be used for defining errors.
 
 
-### 0.8.7 (unreleased)
+### 0.8.8 (unreleased)
 
 Language Features:
 
 
+Compiler Features:
+
+
+Bugfixes:
+
+
+
+### 0.8.7 (2021-08-11)
+
+Language Features:
+ * Introduce global ``block.basefee`` for retrieving the base fee of the current block.
+ * Yul: Introduce builtin ``basefee()`` for retrieving the base fee of the current block.
+
+
 Compiler Features:
  * AssemblyStack: Also run opcode-based optimizer when compiling Yul code.
- * Yul EVM Code Transform: Do not reuse stack slots that immediately become unreachable.
- * Yul EVM Code Transform: Also pop unused argument slots for functions without return variables (under the same restrictions as for functions with return variables).
- * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default).
  * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``.
+ * EVM: Set the default EVM version to "London".
+ * SMTChecker: Do not check underflow and overflow by default.
  * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``.
+ * SMTChecker: new setting to enable/disable encoding of division and modulo with slack variables. The command line option is ``--model-checker-div-mod-slacks`` and the JSON option is ``settings.modelChecker.divModWithSlacks``.
+ * Yul EVM Code Transform: Also pop unused argument slots for functions without return variables (under the same restrictions as for functions with return variables).
+ * Yul EVM Code Transform: Do not reuse stack slots that immediately become unreachable.
+ * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default).
 
 
 Bugfixes:
  * Code Generator: Fix crash when passing an empty string literal to ``bytes.concat()``.
  * Code Generator: Fix internal compiler error when calling functions bound to calldata structs and arrays.
  * Code Generator: Fix internal compiler error when passing a 32-byte hex literal or a zero literal to ``bytes.concat()`` by disallowing such literals.
+ * Commandline Interface: Apply ``--optimizer-runs`` option in assembly / yul mode.
  * Commandline Interface: Fix crash when a directory path is passed to ``--standard-json``.
  * Commandline Interface: Read JSON from standard input when ``--standard-json`` gets ``-`` as a file name.
  * Standard JSON: Include source location for errors in files with empty name.
  * Type Checker: Fix internal error and prevent static calls to unimplemented modifiers.
  * Yul Code Generator: Fix internal compiler error when using a long literal with bitwise negation.
  * Yul Code Generator: Fix source location references for calls to builtin functions.
  * Yul Parser: Fix source location references for ``if`` statements.
- * Commandline Interface: Apply ``--optimizer-runs`` option in assembly / yul mode.
 
 
 ### 0.8.6 (2021-06-22)

docs/bugs_by_version.json

@@ -1551,5 +1551,9 @@
     "0.8.6": {
         "bugs": [],
         "released": "2021-06-22"
+    },
+    "0.8.7": {
+        "bugs": [],
+        "released": "2021-08-11"
     }
 }

docs/cheatsheet.rst

@@ -84,6 +84,7 @@ Global Variables
   to ``abi.encodeWithSelector(bytes4(keccak256(bytes(signature)), ...)```
 - ``bytes.concat(...) returns (bytes memory)``: :ref:`Concatenates variable number of
   arguments to one byte array<bytes-concat>`
+- ``block.basefee`` (``uint``): current block's base fee (`EIP-3198 <https://eips.ethereum.org/EIPS/eip-3198>`_ and `EIP-1559 <https://eips.ethereum.org/EIPS/eip-1559>`_)
 - ``block.chainid`` (``uint``): current chain id
 - ``block.coinbase`` (``address payable``): current block miner's address
 - ``block.difficulty`` (``uint``): current block difficulty

docs/grammar/SolidityLexer.g4

@@ -284,7 +284,8 @@ YulEVMBuiltin:
 	| 'returndatacopy' | 'extcodehash' | 'create' | 'create2' | 'call' | 'callcode'
 	| 'delegatecall' | 'staticcall' | 'return' | 'revert' | 'selfdestruct' | 'invalid'
 	| 'log0' | 'log1' | 'log2' | 'log3' | 'log4' | 'chainid' | 'origin' | 'gasprice'
-	| 'blockhash' | 'coinbase' | 'timestamp' | 'number' | 'difficulty' | 'gaslimit';
+	| 'blockhash' | 'coinbase' | 'timestamp' | 'number' | 'difficulty' | 'gaslimit'
+	| 'basefee';
 
 YulLBrace: '{' -> pushMode(YulMode);
 YulRBrace: '}' -> popMode;

docs/resources.rst

@@ -1,45 +1,49 @@
+#########
 Resources
----------
+#########
 
-General
-~~~~~~~
+General Resources
+=================
 
-* `Ethereum <https://ethereum.org>`_
+* `Ethereum.org Developer Portal <https://ethereum.org/en/developers/>`_
+* `Ethereum StackExchange <https://ethereum.stackexchange.com/>`_
+* `Solidity Portal <https://soliditylang.org/>`_
+* `Solidity Changelog <https://github.com/ethereum/solidity/blob/develop/Changelog.md>`_
+* `Solidity Source Code on GitHub <https://github.com/ethereum/solidity/>`_
+* `Solidity Language Users Chat <https://matrix.to/#/#ethereum_solidity:gitter.im>`_
+* `Solidity Compiler Developers Chat <https://matrix.to/#/#ethereum_solidity-dev:gitter.im>`_
+* `Awesome Solidity <https://github.com/bkrem/awesome-solidity>`_
+* `Solidity by Example <https://solidity-by-example.org/>`_
 
-* `Changelog <https://github.com/ethereum/solidity/blob/develop/Changelog.md>`_
 
-* `Source Code <https://github.com/ethereum/solidity/>`_
+Integrated (Ethereum) Development Environments
+==============================================
 
-* `Ethereum Stackexchange <https://ethereum.stackexchange.com/>`_
+    * `Brownie <https://eth-brownie.readthedocs.io/en/stable/>`_
+        Python-based development and testing framework for smart contracts targeting the Ethereum Virtual Machine.
 
-* `Language Users Chat <https://gitter.im/ethereum/solidity/>`_
+    * `Dapp <https://dapp.tools/>`_
+        Tool for building, testing and deploying smart contracts from the command line.
 
-* `Compiler Developers Chat <https://gitter.im/ethereum/solidity-dev/>`_
+    * `Embark <https://framework.embarklabs.io/>`_
+        Developer platform for building and deploying decentralized applications.
 
-Solidity Integrations
-~~~~~~~~~~~~~~~~~~~~~
-
-* Generic:
-
-    * `EthFiddle <https://ethfiddle.com/>`_
-        Solidity IDE in the Browser. Write and share your Solidity code. Uses server-side components.
+    * `Hardhat <https://hardhat.org/>`_
+        Ethereum development environment with local Ethereum network, debugging features and plugin ecosystem.
 
     * `Remix <https://remix.ethereum.org/>`_
         Browser-based IDE with integrated compiler and Solidity runtime environment without server-side components.
 
-    * `Solhint <https://github.com/protofire/solhint>`_
-        Solidity linter that provides security, style guide and best practice rules for smart contract validation.
+    * `Scaffold-ETH <https://github.com/austintgriffith/scaffold-eth>`_
+        Ethereum development stack focused on fast product iterations.
 
-    * `Solidity IDE <https://github.com/System-Glitch/Solidity-IDE>`_
-        Browser-based IDE with integrated compiler, Ganache and local file system support.
+    * `Truffle <https://www.trufflesuite.com/truffle>`_
+        Ethereum development framework.
 
-    * `Ethlint <https://github.com/duaraghav8/Ethlint>`_
-        Linter to identify and fix style and security issues in Solidity.
+Editor Integrations
+===================
 
-    * `Superblocks Lab <https://lab.superblocks.com/>`_
-        Browser-based IDE. Built-in browser-based VM and Metamask integration (one click deployment to Testnet/Mainnet).
-
-* Atom:
+* Atom
 
     * `Etheratom <https://github.com/0mkara/etheratom>`_
         Plugin for the Atom editor that features syntax highlighting, compilation and a runtime environment (Backend node & VM compatible).
@@ -50,63 +54,67 @@ Solidity Integrations
     * `Atom Solium Linter <https://atom.io/packages/linter-solium>`_
         Configurable Solidity linter for Atom using Solium (now Ethlint) as a base.
 
-* Eclipse:
-
-   * `YAKINDU Solidity Tools <https://yakindu.github.io/solidity-ide/>`_
-        Eclipse based IDE. Features context sensitive code completion and help, code navigation, syntax coloring, built in compiler, quick fixes and templates.
-
-* Emacs:
+* Emacs
 
     * `Emacs Solidity <https://github.com/ethereum/emacs-solidity/>`_
         Plugin for the Emacs editor providing syntax highlighting and compilation error reporting.
 
-* IntelliJ:
+* IntelliJ
 
     * `IntelliJ IDEA plugin <https://plugins.jetbrains.com/plugin/9475-intellij-solidity>`_
         Solidity plugin for IntelliJ IDEA (and all other JetBrains IDEs)
 
-* Sublime:
+* Sublime
 
     * `Package for SublimeText - Solidity language syntax <https://packagecontrol.io/packages/Ethereum/>`_
         Solidity syntax highlighting for SublimeText editor.
 
-* Vim:
+* Vim
 
     * `Vim Solidity <https://github.com/tomlion/vim-solidity/>`_
         Plugin for the Vim editor providing syntax highlighting.
 
     * `Vim Syntastic <https://github.com/vim-syntastic/syntastic>`_
         Plugin for the Vim editor providing compile checking.
 
-* Visual Studio Code:
+* Visual Studio Code
 
     * `Visual Studio Code extension <https://juan.blanco.ws/solidity-contracts-in-visual-studio-code/>`_
         Solidity plugin for Microsoft Visual Studio Code that includes syntax highlighting and the Solidity compiler.
 
 Solidity Tools
-~~~~~~~~~~~~~~
+==============
 
 * `ABI to Solidity interface converter <https://gist.github.com/chriseth/8f533d133fa0c15b0d6eaf3ec502c82b>`_
     A script for generating contract interfaces from the ABI of a smart contract.
 
-* `Dapp <https://dapp.tools/dapp/>`_
-    Build tool, package manager, and deployment assistant for Solidity.
+* `abi-to-sol <https://github.com/gnidan/abi-to-sol>`_
+    Tool to generate Solidity interface source from a given ABI JSON.
 
 * `Doxity <https://github.com/DigixGlobal/doxity>`_
     Documentation Generator for Solidity.
 
+* `Ethlint <https://github.com/duaraghav8/Ethlint>`_
+    Linter to identify and fix style and security issues in Solidity.
+
 * `evmdis <https://github.com/Arachnid/evmdis>`_
     EVM Disassembler that performs static analysis on the bytecode to provide a higher level of abstraction than raw EVM operations.
 
 * `EVM Lab <https://github.com/ethereum/evmlab/>`_
     Rich tool package to interact with the EVM. Includes a VM, Etherchain API, and a trace-viewer with gas cost display.
 
+* `hevm <https://github.com/dapphub/dapptools/tree/master/src/hevm#readme>`_
+    EVM debugger and symbolic execution engine.
+
 * `leafleth <https://github.com/clemlak/leafleth>`_
     A documentation generator for Solidity smart-contracts.
 
 * `PIET <https://piet.slock.it/>`_
     A tool to develop, audit and use Solidity smart contracts through a simple graphical interface.
 
+* `sol2uml <https://www.npmjs.com/package/sol2uml>`_
+    Unified Modeling Language (UML) class diagram generator for Solidity contracts.
+
 * `solc-select <https://github.com/crytic/solc-select>`_
     A script to quickly switch between Solidity compiler versions.
 
@@ -119,8 +127,8 @@ Solidity Tools
 * `solgraph <https://github.com/raineorshine/solgraph>`_
     Visualize Solidity control flow and highlight potential security vulnerabilities.
 
-* `Securify <https://securify.ch/>`_
-    Fully automated online static analyzer for smart contracts, providing a security report based on vulnerability patterns.
+* `Solhint <https://github.com/protofire/solhint>`_
+    Solidity linter that provides security, style guide and best practice rules for smart contract validation.
 
 * `Sūrya <https://github.com/ConsenSys/surya/>`_
     Utility tool for smart contract systems, offering a number of visual outputs and information about the contracts' structure. Also supports querying the function call graph.
@@ -129,7 +137,7 @@ Solidity Tools
     A tool for mutation generation, with configurable rules and support for Solidity and Vyper.
 
 Third-Party Solidity Parsers and Grammars
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+=========================================
 
 * `Solidity Parser for JavaScript <https://github.com/solidity-parser/parser>`_
     A Solidity parser for JS built on top of a robust ANTLR4 grammar.

docs/smtchecker.rst

@@ -34,6 +34,9 @@ The other verification targets that the SMTChecker checks at compile time are:
 - Out of bounds index access.
 - Insufficient funds for a transfer.
 
+All the targets above are automatically checked by default if all engines are
+enabled, except underflow and overflow for Solidity >=0.8.7.
+
 The potential warnings that the SMTChecker reports are:
 
 - ``<failing  property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
@@ -93,8 +96,10 @@ Overflow
     }
 
 The contract above shows an overflow check example.
-The SMTChecker will, by default, check every reachable arithmetic operation
-in the contract for potential underflow and overflow.
+The SMTChecker does not check underflow and overflow by default for Solidity >=0.8.7,
+so we need to use the command line option ``--model-checker-targets "underflow,overflow"``
+or the JSON option ``settings.modelChecker.targets = ["underflow", "overflow"]``.
+See :ref:`this section for targets configuration<smtchecker_targets>`.
 Here, it reports the following:
 
 .. code-block:: text
@@ -447,6 +452,8 @@ If the SMTChecker does not manage to solve the contract properties with the defa
 a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout <time>`` or
 the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeout.
 
+.. _smtchecker_targets:
+
 Verification Targets
 ====================
 
@@ -471,6 +478,8 @@ The keywords that represent the targets are:
 A common subset of targets might be, for example:
 ``--model-checker-targets assert,overflow``.
 
+All targets are checked by default, except underflow and overflow for Solidity >=0.8.7.
+
 There is no precise heuristic on how and when to split verification targets,
 but it can be useful especially when dealing with large contracts.
 
@@ -479,7 +488,7 @@ Unproved Targets
 
 If there are any unproved targets, the SMTChecker issues one warning stating
 how many unproved targets there are. If the user wishes to see all the specific
-unproved targets, the CLI option ``--model-checker-show-unproved true`` and
+unproved targets, the CLI option ``--model-checker-show-unproved`` and
 the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
 
 Verified Contracts
@@ -509,7 +518,17 @@ which has the following form:
         "source2.sol": ["contract2", "contract3"]
     }
 
-.. _smtchecker_engines:
+Division and Modulo With Slack Variables
+========================================
+
+Spacer, the default Horn solver used by the SMTChecker, often dislikes division
+and modulo operations inside Horn rules. Because of that, by default the
+Solidity division and modulo operations are encoded using the constraint
+``a = b * d + m`` where ``d = a / b`` and ``m = a % b``.
+However, other solvers, such as Eldarica, prefer the syntactically precise operations.
+The command line flag ``--model-checker-div-mod-no-slacks`` and the JSON option
+``settings.modelChecker.divModNoSlacks`` can be used to toggle the encoding
+depending on the used solver preferences.
 
 Natspec Function Abstraction
 ============================
@@ -523,6 +542,8 @@ body of the function is not used, and when called, the function will:
 - Return a nondeterministic value, and either keep the state variables unchanged if the abstracted function is view/pure, or also set the state variables to nondeterministic values otherwise. This can be used via the annotation ``/// @custom:smtchecker abstract-function-nondet``.
 - Act as an uninterpreted function. This means that the semantics of the function (given by the body) are ignored, and the only property this function has is that given the same input it guarantees the same output. This is currently under development and will be available via the annotation ``/// @custom:smtchecker abstract-function-uf``.
 
+.. _smtchecker_engines:
+
 Model Checking Engines
 ======================
 

docs/units-and-global-variables.rst

@@ -72,6 +72,7 @@ Block and Transaction Properties
 --------------------------------
 
 - ``blockhash(uint blockNumber) returns (bytes32)``: hash of the given block when ``blocknumber`` is one of the 256 most recent blocks; otherwise returns zero
+- ``block.basefee`` (``uint``): current block's base fee (`EIP-3198 <https://eips.ethereum.org/EIPS/eip-3198>`_ and `EIP-1559 <https://eips.ethereum.org/EIPS/eip-1559>`_)
 - ``block.chainid`` (``uint``): current chain id
 - ``block.coinbase`` (``address payable``): current block miner's address
 - ``block.difficulty`` (``uint``): current block difficulty