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

.circleci/soltest_all.sh

@@ -28,8 +28,8 @@ set -e
 
 REPODIR="$(realpath "$(dirname "$0")"/..)"
 
-EVM_VALUES=(homestead byzantium constantinople petersburg istanbul berlin)
+EVM_VALUES=(homestead byzantium constantinople petersburg istanbul berlin london)
-DEFAULT_EVM=berlin
+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,24 +4,42 @@ 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.
@@ -29,7 +47,6 @@ Bugfixes:
  * 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
+    * `Hardhat <https://hardhat.org/>`_
-~~~~~~~~~~~~~~~~~~~~~
+        Ethereum development environment with local Ethereum network, debugging features and plugin ecosystem.
-
-* Generic:
-
-    * `EthFiddle <https://ethfiddle.com/>`_
-        Solidity IDE in the Browser. Write and share your Solidity code. Uses server-side components.
 
     * `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>`_
+    * `Scaffold-ETH <https://github.com/austintgriffith/scaffold-eth>`_
-        Solidity linter that provides security, style guide and best practice rules for smart contract validation.
+        Ethereum development stack focused on fast product iterations.
 
-    * `Solidity IDE <https://github.com/System-Glitch/Solidity-IDE>`_
+    * `Truffle <https://www.trufflesuite.com/truffle>`_
-        Browser-based IDE with integrated compiler, Ganache and local file system support.
+        Ethereum development framework.
 
-    * `Ethlint <https://github.com/duaraghav8/Ethlint>`_
+Editor Integrations
-        Linter to identify and fix style and security issues in Solidity.
+===================
 
-    * `Superblocks Lab <https://lab.superblocks.com/>`_
+* Atom
-        Browser-based IDE. Built-in browser-based VM and Metamask integration (one click deployment to Testnet/Mainnet).
-
-* 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,27 +54,22 @@ Solidity Integrations
     * `Atom Solium Linter <https://atom.io/packages/linter-solium>`_
         Configurable Solidity linter for Atom using Solium (now Ethlint) as a base.
 
-* Eclipse:
+* Emacs
-
-   * `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 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.
@@ -78,35 +77,44 @@ Solidity Integrations
     * `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/>`_
+* `abi-to-sol <https://github.com/gnidan/abi-to-sol>`_
-    Build tool, package manager, and deployment assistant for Solidity.
+    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/>`_
+* `Solhint <https://github.com/protofire/solhint>`_
-    Fully automated online static analyzer for smart contracts, providing a security report based on vulnerability patterns.
+    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
+The SMTChecker does not check underflow and overflow by default for Solidity >=0.8.7,
-in the contract for potential underflow and overflow.
+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

docs/using-the-compiler.rst

@@ -169,10 +169,12 @@ at each version. Backward compatibility is not guaranteed between each version.
    - The compiler behaves the same way as with constantinople.
 - ``istanbul``
    - Opcodes ``chainid`` and ``selfbalance`` are available in assembly.
-- ``berlin`` (**default**)
+- ``berlin``
    - Gas costs for ``SLOAD``, ``*CALL``, ``BALANCE``, ``EXT*`` and ``SELFDESTRUCT`` increased. The
      compiler assumes cold gas costs for such operations. This is relevant for gas estimation and
      the optimizer.
+- ``london`` (**default**)
+   - The block's base fee (`EIP-3198 <https://eips.ethereum.org/EIPS/eip-3198>`_ and `EIP-1559 <https://eips.ethereum.org/EIPS/eip-1559>`_) can be accessed via the global ``block.basefee`` or ``basefee()`` in inline assembly.
 
 
 .. index:: ! standard JSON, ! --standard-json
@@ -400,13 +402,23 @@ Input Description
             "source1.sol": ["contract1"],
             "source2.sol": ["contract2", "contract3"]
           },
+          // Choose whether division and modulo operations should be replaced by
+          // multiplication with slack variables. Default is `true`.
+          // Using `false` here is recommended if you are using the CHC engine
+          // and not using Spacer as the Horn solver (using Eldarica, for example).
+          // See the Formal Verification section for a more detailed explanation of this option.
+          "divModWithSlacks": true,
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
           // Choose whether to output all unproved targets. The default is `false`.
           "showUnproved": true,
+          // Choose which solvers should be used, if available.
+          // See the Formal Verification section for the solvers description.
+          "solvers": ["cvc4", "smtlib2", "z3"],
           // Choose which targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
-          // If the option is not given all targets are checked by default.
+          // If the option is not given all targets are checked by default,
+          // except underflow/overflow for Solidity >=0.8.7.
           // See the Formal Verification section for the targets description.
           "targets": ["underflow", "overflow", "assert"],
           // Timeout for each SMT query in milliseconds.

docs/yul.rst

@@ -717,8 +717,8 @@ This document does not want to be a full description of the Ethereum virtual mac
 Please refer to a different document if you are interested in the precise semantics.
 
 Opcodes marked with ``-`` do not return a result and all others return exactly one value.
-Opcodes marked with ``F``, ``H``, ``B``, ``C`` or ``I`` are present since Frontier, Homestead,
+Opcodes marked with ``F``, ``H``, ``B``, ``C``, ``I`` and ``L`` are present since Frontier, Homestead,
-Byzantium, Constantinople or Istanbul, respectively.
+Byzantium, Constantinople, Istanbul or London respectively.
 
 In the following, ``mem[a...b)`` signifies the bytes of memory starting at position ``a`` up to
 but not including position ``b`` and ``storage[p]`` signifies the storage contents at slot ``p``.
@@ -879,7 +879,9 @@ the ``dup`` and ``swap`` instructions as well as ``jump`` instructions, labels a
 | log4(p, s, t1, t2, t3,  | `-` | F | log with topics t1, t2, t3, t4 and data mem[p...(p+s))          |
 | t4)                     |     |   |                                                                 |
 +-------------------------+-----+---+-----------------------------------------------------------------+
-| chainid()               |     | I | ID of the executing chain (EIP 1344)                            |
+| chainid()               |     | I | ID of the executing chain (EIP-1344)                            |
++-------------------------+-----+---+-----------------------------------------------------------------+
+| basefee()               |     | L | current block's base fee (EIP-3198 and EIP-1559)                |
 +-------------------------+-----+---+-----------------------------------------------------------------+
 | origin()                |     | F | transaction sender                                              |
 +-------------------------+-----+---+-----------------------------------------------------------------+

libevmasm/Instruction.cpp

@@ -84,6 +84,7 @@ std::map<std::string, Instruction> const solidity::evmasm::c_instructions =
 	{ "GASLIMIT", Instruction::GASLIMIT },
 	{ "CHAINID", Instruction::CHAINID },
 	{ "SELFBALANCE", Instruction::SELFBALANCE },
+	{ "BASEFEE", Instruction::BASEFEE },
 	{ "POP", Instruction::POP },
 	{ "MLOAD", Instruction::MLOAD },
 	{ "MSTORE", Instruction::MSTORE },
@@ -230,6 +231,7 @@ static std::map<Instruction, InstructionInfo> const c_instructionInfo =
 	{ Instruction::GASLIMIT,	{ "GASLIMIT",		0, 0, 1, false, Tier::Base } },
 	{ Instruction::CHAINID,		{ "CHAINID",		0, 0, 1, false, Tier::Base } },
 	{ Instruction::SELFBALANCE,	{ "SELFBALANCE",	0, 0, 1, false, Tier::Low } },
+	{ Instruction::BASEFEE,     { "BASEFEE",        0, 0, 1, false, Tier::Base } },
 	{ Instruction::POP,			{ "POP",			0, 1, 0, false, Tier::Base } },
 	{ Instruction::MLOAD,		{ "MLOAD",			0, 1, 1, true, Tier::VeryLow } },
 	{ Instruction::MSTORE,		{ "MSTORE",			0, 2, 0, true, Tier::VeryLow } },

libevmasm/Instruction.h

@@ -88,6 +88,7 @@ enum class Instruction: uint8_t
 	GASLIMIT,			///< get the block's gas limit
 	CHAINID,			///< get the config's chainid param
 	SELFBALANCE,		///< get balance of the current account
+	BASEFEE,            ///< get the block's basefee
 
 	POP = 0x50,			///< remove item from stack
 	MLOAD,				///< load word from memory

libevmasm/SemanticInformation.cpp

@@ -353,6 +353,7 @@ bool SemanticInformation::invalidInPureFunctions(Instruction _instruction)
 	case Instruction::CALLER:
 	case Instruction::CALLVALUE:
 	case Instruction::CHAINID:
+	case Instruction::BASEFEE:
 	case Instruction::GAS:
 	case Instruction::GASPRICE:
 	case Instruction::EXTCODESIZE:

liblangutil/EVMVersion.cpp

@@ -46,8 +46,9 @@ bool EVMVersion::hasOpcode(Instruction _opcode) const
 		return hasChainID();
 	case Instruction::SELFBALANCE:
 		return hasSelfBalance();
+	case Instruction::BASEFEE:
+		return hasBaseFee();
 	default:
 		return true;
 	}
 }
-

liblangutil/EVMVersion.h

@@ -51,10 +51,11 @@ public:
 	static EVMVersion petersburg() { return {Version::Petersburg}; }
 	static EVMVersion istanbul() { return {Version::Istanbul}; }
 	static EVMVersion berlin() { return {Version::Berlin}; }
+	static EVMVersion london() { return {Version::London}; }
 
 	static std::optional<EVMVersion> fromString(std::string const& _version)
 	{
-		for (auto const& v: {homestead(), tangerineWhistle(), spuriousDragon(), byzantium(), constantinople(), petersburg(), istanbul(), berlin()})
+		for (auto const& v: {homestead(), tangerineWhistle(), spuriousDragon(), byzantium(), constantinople(), petersburg(), istanbul(), berlin(), london()})
 			if (_version == v.name())
 				return v;
 		return std::nullopt;
@@ -75,6 +76,7 @@ public:
 		case Version::Petersburg: return "petersburg";
 		case Version::Istanbul: return "istanbul";
 		case Version::Berlin: return "berlin";
+		case Version::London: return "london";
 		}
 		return "INVALID";
 	}
@@ -87,6 +89,7 @@ public:
 	bool hasExtCodeHash() const { return *this >= constantinople(); }
 	bool hasChainID() const { return *this >= istanbul(); }
 	bool hasSelfBalance() const { return *this >= istanbul(); }
+	bool hasBaseFee() const { return *this >= london(); }
 
 	bool hasOpcode(evmasm::Instruction _opcode) const;
 
@@ -95,11 +98,11 @@ public:
 	bool canOverchargeGasForCall() const { return *this >= tangerineWhistle(); }
 
 private:
-	enum class Version { Homestead, TangerineWhistle, SpuriousDragon, Byzantium, Constantinople, Petersburg, Istanbul, Berlin };
+	enum class Version { Homestead, TangerineWhistle, SpuriousDragon, Byzantium, Constantinople, Petersburg, Istanbul, Berlin, London };
 
 	EVMVersion(Version _version): m_version(_version) {}
 
-	Version m_version = Version::Berlin;
+	Version m_version = Version::London;
 };
 
 }

libsolidity/analysis/TypeChecker.cpp

@@ -742,8 +742,15 @@ bool TypeChecker::visit(InlineAssembly const& _inlineAssembly)
 		yul::Identifier const& _identifier,
 		yul::IdentifierContext _context,
 		bool
-	)
+	) -> bool
 	{
+		if (_context == yul::IdentifierContext::NonExternal)
+		{
+			// Hack until we can disallow any shadowing: If we found an internal reference,
+			// clear the external references, so that codegen does not use it.
+			_inlineAssembly.annotation().externalReferences.erase(& _identifier);
+			return false;
+		}
 		auto ref = _inlineAssembly.annotation().externalReferences.find(&_identifier);
 		if (ref == _inlineAssembly.annotation().externalReferences.end())
 			return false;
@@ -2947,6 +2954,12 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 				_memberAccess.location(),
 				"\"chainid\" is not supported by the VM version."
 			);
+		else if (magicType->kind() == MagicType::Kind::Block && memberName == "basefee" && !m_evmVersion.hasBaseFee())
+			m_errorReporter.typeError(
+				5921_error,
+				_memberAccess.location(),
+				"\"basefee\" is not supported by the VM version."
+			);
 	}
 
 	if (

libsolidity/ast/Types.cpp

@@ -3892,7 +3892,8 @@ MemberList::MemberMap MagicType::nativeMembers(ASTNode const*) const
 			{"difficulty", TypeProvider::uint256()},
 			{"number", TypeProvider::uint256()},
 			{"gaslimit", TypeProvider::uint256()},
-			{"chainid", TypeProvider::uint256()}
+			{"chainid", TypeProvider::uint256()},
+			{"basefee", TypeProvider::uint256()}
 		});
 	case Kind::Message:
 		return MemberList::MemberMap({

libsolidity/codegen/CompilerContext.cpp

@@ -411,6 +411,7 @@ void CompilerContext::appendInlineAssembly(
 		yul::AbstractAssembly& _assembly
 	)
 	{
+		solAssert(_context == yul::IdentifierContext::RValue || _context == yul::IdentifierContext::LValue, "");
 		auto it = std::find(_localVariables.begin(), _localVariables.end(), _identifier.name.str());
 		solAssert(it != _localVariables.end(), "");
 		auto stackDepth = static_cast<size_t>(distance(it, _localVariables.end()));
@@ -520,7 +521,7 @@ void CompilerContext::appendInlineAssembly(
 		analysisInfo,
 		*m_asm,
 		m_evmVersion,
-		identifierAccess,
+		identifierAccess.generateCode,
 		_system,
 		_optimiserSettings.optimizeStackAllocation
 	);

libsolidity/codegen/ContractCompiler.cpp

@@ -702,16 +702,13 @@ bool ContractCompiler::visit(FunctionDefinition const& _function)
 bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly)
 {
 	unsigned startStackHeight = m_context.stackHeight();
-	yul::ExternalIdentifierAccess identifierAccess;
+	yul::ExternalIdentifierAccess::CodeGenerator identifierAccessCodeGen = [&](
-	identifierAccess.resolve = [&](yul::Identifier const& _identifier, yul::IdentifierContext, bool)
+		yul::Identifier const& _identifier,
-	{
+		yul::IdentifierContext _context,
-		auto ref = _inlineAssembly.annotation().externalReferences.find(&_identifier);
+		yul::AbstractAssembly& _assembly
-		if (ref == _inlineAssembly.annotation().externalReferences.end())
+	)
-			return numeric_limits<size_t>::max();
-		return ref->second.valueSize;
-	};
-	identifierAccess.generateCode = [&](yul::Identifier const& _identifier, yul::IdentifierContext _context, yul::AbstractAssembly& _assembly)
 	{
+		solAssert(_context == yul::IdentifierContext::RValue || _context == yul::IdentifierContext::LValue, "");
 		auto ref = _inlineAssembly.annotation().externalReferences.find(&_identifier);
 		solAssert(ref != _inlineAssembly.annotation().externalReferences.end(), "");
 		Declaration const* decl = ref->second.declaration;
@@ -918,7 +915,7 @@ bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly)
 		*analysisInfo,
 		*m_context.assemblyPtr(),
 		m_context.evmVersion(),
-		identifierAccess,
+		identifierAccessCodeGen,
 		false,
 		m_optimiserSettings.optimizeStackAllocation
 	);

libsolidity/codegen/ExpressionCompiler.cpp

@@ -1731,6 +1731,8 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 			m_context << Instruction::GASPRICE;
 		else if (member == "chainid")
 			m_context << Instruction::CHAINID;
+		else if (member == "basefee")
+			m_context << Instruction::BASEFEE;
 		else if (member == "data")
 			m_context << u256(0) << Instruction::CALLDATASIZE;
 		else if (member == "sig")

libsolidity/codegen/YulUtilFunctions.cpp

@@ -445,7 +445,7 @@ string YulUtilFunctions::typedShiftLeftFunction(Type const& _type, Type const& _
 			Whiskers(R"(
 			function <functionName>(value, bits) -> result {
 				bits := <cleanAmount>(bits)
-				result := <cleanup>(<shift>(bits, value))
+				result := <cleanup>(<shift>(bits, <cleanup>(value)))
 			}
 			)")
 			("functionName", functionName)
@@ -3258,6 +3258,7 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 		switch (fromCategory)
 		{
 		case Type::Category::Address:
+		case Type::Category::Contract:
 			body =
 				Whiskers("converted := <convert>(value)")
 					("convert", conversionFunction(IntegerType(160), _to))
@@ -3265,16 +3266,14 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 			break;
 		case Type::Category::Integer:
 		case Type::Category::RationalNumber:
-		case Type::Category::Contract:
 		{
+			solAssert(_from.mobileType(), "");
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&_from))
-				solUnimplementedAssert(!rational->isFractional(), "Not yet implemented - FixedPointType.");
+				if (rational->isFractional())
+					solAssert(toCategory == Type::Category::FixedPoint, "");
+
 			if (toCategory == Type::Category::FixedBytes)
 			{
-				solAssert(
-					fromCategory == Type::Category::Integer || fromCategory == Type::Category::RationalNumber,
-					"Invalid conversion to FixedBytesType requested."
-				);
 				FixedBytesType const& toBytesType = dynamic_cast<FixedBytesType const&>(_to);
 				body =
 					Whiskers("converted := <shiftLeft>(<clean>(value))")
@@ -3283,43 +3282,28 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 					.render();
 			}
 			else if (toCategory == Type::Category::Enum)
-			{
-				solAssert(_from.mobileType(), "");
 				body =
 					Whiskers("converted := <cleanEnum>(<cleanInt>(value))")
 					("cleanEnum", cleanupFunction(_to))
-					// "mobileType()" returns integer type for rational
+					("cleanInt", cleanupFunction(_from))
-					("cleanInt", cleanupFunction(*_from.mobileType()))
 					.render();
-			}
 			else if (toCategory == Type::Category::FixedPoint)
 				solUnimplemented("Not yet implemented - FixedPointType.");
-			else if (toCategory == Type::Category::Address)
+			else if (toCategory == Type::Category::Address || toCategory == Type::Category::Contract)
 				body =
 					Whiskers("converted := <convert>(value)")
 					("convert", conversionFunction(_from, IntegerType(160)))
 					.render();
-			else
+			else if (toCategory == Type::Category::Integer)
 			{
-				solAssert(
+				IntegerType const& to = dynamic_cast<IntegerType const&>(_to);
-					toCategory == Type::Category::Integer ||
-					toCategory == Type::Category::Contract,
-				"");
-				IntegerType const addressType(160);
-				IntegerType const& to =
-					toCategory == Type::Category::Integer ?
-					dynamic_cast<IntegerType const&>(_to) :
-					addressType;
 
 				// Clean according to the "to" type, except if this is
 				// a widening conversion.
 				IntegerType const* cleanupType = &to;
-				if (fromCategory != Type::Category::RationalNumber)
+				if (fromCategory == Type::Category::Integer)
 				{
-					IntegerType const& from =
+					IntegerType const& from = dynamic_cast<IntegerType const&>(_from);
-						fromCategory == Type::Category::Integer ?
-						dynamic_cast<IntegerType const&>(_from) :
-						addressType;
 					if (to.numBits() > from.numBits())
 						cleanupType = &from;
 				}
@@ -3328,6 +3312,8 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to)
 					("cleanInt", cleanupFunction(*cleanupType))
 					.render();
 			}
+			else
+				solAssert(false, "");
 			break;
 		}
 		case Type::Category::Bool:

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -1733,6 +1733,8 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 			define(_memberAccess) << "gasprice()\n";
 		else if (member == "chainid")
 			define(_memberAccess) << "chainid()\n";
+		else if (member == "basefee")
+			define(_memberAccess) << "basefee()\n";
 		else if (member == "data")
 		{
 			IRVariable var(_memberAccess);

libsolidity/formal/BMC.cpp

@@ -80,7 +80,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	{
 		m_solvedTargets = move(_solvedTargets);
 		m_context.setSolver(m_interface.get());
-		m_context.clear();
+		m_context.reset();
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 		createFreeConstants(sourceDependencies(_source));

libsolidity/formal/CHC.cpp

@@ -967,7 +967,7 @@ void CHC::resetSourceAnalysis()
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}
 
-	m_context.clear();
+	m_context.reset();
 	m_context.resetUniqueId();
 	m_context.setAssertionAccumulation(false);
 }

libsolidity/formal/EncodingContext.cpp

@@ -49,12 +49,6 @@ unsigned EncodingContext::newUniqueId()
 	return m_nextUniqueId++;
 }
 
-void EncodingContext::clear()
-{
-	m_variables.clear();
-	reset();
-}
-
 /// Variables.
 
 shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl)

libsolidity/formal/ModelCheckerSettings.cpp

@@ -40,9 +40,16 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
 std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
 {
 	set<TargetType> chosenTargets;
-	if (_targets == "default")
+	if (_targets == "default" || _targets == "all")
+	{
+		bool all = _targets == "all";
 		for (auto&& v: targetStrings | ranges::views::values)
+		{
+			if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
+				continue;
 			chosenTargets.insert(v);
+		}
+	}
 	else
 		for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
 		{

libsolidity/formal/ModelCheckerSettings.h

@@ -91,7 +91,10 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
+	/// Adds the default targets, that is, all except underflow and overflow.
 	static ModelCheckerTargets Default() { return *fromString("default"); }
+	/// Adds all targets, including underflow and overflow.
+	static ModelCheckerTargets All() { return *fromString("all"); }
 
 	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
 
@@ -112,6 +115,13 @@ struct ModelCheckerTargets
 struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
+	/// Currently division and modulo are replaced by multiplication with slack vars, such that
+	/// a / b <=> a = b * k + m
+	/// where k and m are slack variables.
+	/// This is the default because Spacer prefers that over precise / and mod.
+	/// This option allows disabling this mechanism since other solvers
+	/// might prefer the precise encoding.
+	bool divModNoSlacks = false;
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
 	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
@@ -123,6 +133,7 @@ struct ModelCheckerSettings
 	{
 		return
 			contracts == _other.contracts &&
+			divModNoSlacks == _other.divModNoSlacks &&
 			engine == _other.engine &&
 			showUnproved == _other.showUnproved &&
 			solvers == _other.solvers &&

libsolidity/formal/SMTEncoder.cpp

@@ -1916,6 +1916,9 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 	IntegerType const& _type
 )
 {
+	if (m_settings.divModNoSlacks)
+		return {_left / _right, _left % _right};
+
 	IntegerType const* intType = &_type;
 	string suffix = "div_mod_" + to_string(m_context.newUniqueId());
 	smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
@@ -3031,6 +3034,15 @@ void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID
 		for (auto node: source->nodes())
 			if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
 				createVariable(*var);
+			else if (
+				auto contract = dynamic_cast<ContractDefinition const*>(node.get());
+				contract && contract->isLibrary()
+			)
+				for (auto var: contract->stateVariables())
+				{
+					solAssert(var->isConstant(), "");
+					createVariable(*var);
+				}
 }
 
 smt::SymbolicState& SMTEncoder::state()

libsolidity/interface/StandardCompiler.cpp

@@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -941,6 +941,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.contracts = {move(sourceContracts)};
 	}
 
+	if (modelCheckerSettings.isMember("divModNoSlacks"))
+	{
+		auto const& divModNoSlacks = modelCheckerSettings["divModNoSlacks"];
+		if (!divModNoSlacks.isBool())
+			return formatFatalError("JSONError", "settings.modelChecker.divModNoSlacks must be a Boolean.");
+		ret.modelCheckerSettings.divModNoSlacks = divModNoSlacks.asBool();
+	}
+
 	if (modelCheckerSettings.isMember("engine"))
 	{
 		if (!modelCheckerSettings["engine"].isString())

libyul/AsmAnalysis.cpp

@@ -146,6 +146,13 @@ vector<YulString> AsmAnalyzer::operator()(Identifier const& _identifier)
 		}
 	}))
 	{
+		if (m_resolver)
+			// We found a local reference, make sure there is no external reference.
+			m_resolver(
+				_identifier,
+				yul::IdentifierContext::NonExternal,
+				m_currentScope->insideFunction()
+			);
 	}
 	else
 	{
@@ -308,7 +315,7 @@ vector<YulString> AsmAnalyzer::operator()(FunctionCall const& _funCall)
 
 		validateInstructions(_funCall);
 	}
-	else if (!m_currentScope->lookup(_funCall.functionName.name, GenericVisitor{
+	else if (m_currentScope->lookup(_funCall.functionName.name, GenericVisitor{
 		[&](Scope::Variable const&)
 		{
 			m_errorReporter.typeError(
@@ -323,6 +330,16 @@ vector<YulString> AsmAnalyzer::operator()(FunctionCall const& _funCall)
 			returnTypes = &_fun.returns;
 		}
 	}))
+	{
+		if (m_resolver)
+			// We found a local reference, make sure there is no external reference.
+			m_resolver(
+				_funCall.functionName,
+				yul::IdentifierContext::NonExternal,
+				m_currentScope->insideFunction()
+			);
+	}
+	else
 	{
 		if (!validateInstructions(_funCall))
 			m_errorReporter.declarationError(
@@ -539,6 +556,14 @@ void AsmAnalyzer::checkAssignment(Identifier const& _variable, YulString _valueT
 	bool found = false;
 	if (Scope::Identifier const* var = m_currentScope->lookup(_variable.name))
 	{
+		if (m_resolver)
+			// We found a local reference, make sure there is no external reference.
+			m_resolver(
+				_variable,
+				yul::IdentifierContext::NonExternal,
+				m_currentScope->insideFunction()
+			);
+
 		if (!holds_alternative<Scope::Variable>(*var))
 			m_errorReporter.typeError(2657_error, _variable.debugData->location, "Assignment requires variable.");
 		else if (!m_activeVariables.count(&std::get<Scope::Variable>(*var)))
@@ -695,6 +720,8 @@ bool AsmAnalyzer::validateInstructions(evmasm::Instruction _instr, SourceLocatio
 		errorForVM(1561_error, "only available for Istanbul-compatible");
 	else if (_instr == evmasm::Instruction::SELFBALANCE && !m_evmVersion.hasSelfBalance())
 		errorForVM(7721_error, "only available for Istanbul-compatible");
+	else if (_instr == evmasm::Instruction::BASEFEE && !m_evmVersion.hasBaseFee())
+		errorForVM(5430_error, "only available for London-compatible");
 	else if (_instr == evmasm::Instruction::PC)
 		m_errorReporter.error(
 			2450_error,

libyul/backends/evm/AbstractAssembly.h

@@ -117,7 +117,7 @@ public:
 	virtual void markAsInvalid() = 0;
 };
 
-enum class IdentifierContext { LValue, RValue, VariableDeclaration };
+enum class IdentifierContext { LValue, RValue, VariableDeclaration, NonExternal };
 
 /// Object that is used to resolve references and generate code for access to identifiers external
 /// to inline assembly (not used in standalone assembly mode).

libyul/backends/evm/AsmCodeGen.cpp

@@ -37,7 +37,7 @@ void CodeGenerator::assemble(
 	AsmAnalysisInfo& _analysisInfo,
 	evmasm::Assembly& _assembly,
 	langutil::EVMVersion _evmVersion,
-	ExternalIdentifierAccess const& _identifierAccess,
+	ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen,
 	bool _useNamedLabelsForFunctions,
 	bool _optimizeStackAllocation
 )
@@ -51,7 +51,7 @@ void CodeGenerator::assemble(
 		EVMDialect::strictAssemblyForEVM(_evmVersion),
 		builtinContext,
 		_optimizeStackAllocation,
-		_identifierAccess,
+		_identifierAccessCodeGen,
 		_useNamedLabelsForFunctions
 	);
 	transform(_parsedData);

libyul/backends/evm/AsmCodeGen.h

@@ -44,7 +44,7 @@ public:
 		AsmAnalysisInfo& _analysisInfo,
 		evmasm::Assembly& _assembly,
 		langutil::EVMVersion _evmVersion,
-		ExternalIdentifierAccess const& _identifierAccess = ExternalIdentifierAccess(),
+		ExternalIdentifierAccess::CodeGenerator _identifierAccess = {},
 		bool _useNamedLabelsForFunctions = false,
 		bool _optimizeStackAllocation = false
 	);

libyul/backends/evm/EVMCodeTransform.cpp

@@ -61,7 +61,7 @@ CodeTransform::CodeTransform(
 	bool _allowStackOpt,
 	EVMDialect const& _dialect,
 	BuiltinContext& _builtinContext,
-	ExternalIdentifierAccess _identifierAccess,
+	ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen,
 	bool _useNamedLabelsForFunctions,
 	shared_ptr<Context> _context,
 	vector<TypedName> _delayedReturnVariables,
@@ -73,7 +73,7 @@ CodeTransform::CodeTransform(
 	m_builtinContext(_builtinContext),
 	m_allowStackOpt(_allowStackOpt),
 	m_useNamedLabelsForFunctions(_useNamedLabelsForFunctions),
-	m_identifierAccess(move(_identifierAccess)),
+	m_identifierAccessCodeGen(move(_identifierAccessCodeGen)),
 	m_context(move(_context)),
 	m_delayedReturnVariables(move(_delayedReturnVariables)),
 	m_functionExitLabel(_functionExitLabel)
@@ -292,10 +292,10 @@ void CodeTransform::operator()(Identifier const& _identifier)
 		return;
 	}
 	yulAssert(
-		m_identifierAccess.generateCode,
+		m_identifierAccessCodeGen,
 		"Identifier not found and no external access available."
 	);
-	m_identifierAccess.generateCode(_identifier, IdentifierContext::RValue, m_assembly);
+	m_identifierAccessCodeGen(_identifier, IdentifierContext::RValue, m_assembly);
 }
 
 void CodeTransform::operator()(Literal const& _literal)
@@ -391,7 +391,7 @@ void CodeTransform::operator()(FunctionDefinition const& _function)
 		m_allowStackOpt,
 		m_dialect,
 		m_builtinContext,
-		m_identifierAccess,
+		m_identifierAccessCodeGen,
 		m_useNamedLabelsForFunctions,
 		m_context,
 		_function.returnVariables,
@@ -740,10 +740,10 @@ void CodeTransform::generateAssignment(Identifier const& _variableName)
 	else
 	{
 		yulAssert(
-			m_identifierAccess.generateCode,
+			m_identifierAccessCodeGen,
 			"Identifier not found and no external access available."
 		);
-		m_identifierAccess.generateCode(_variableName, IdentifierContext::LValue, m_assembly);
+		m_identifierAccessCodeGen(_variableName, IdentifierContext::LValue, m_assembly);
 	}
 }
 

libyul/backends/evm/EVMCodeTransform.h

@@ -65,7 +65,7 @@ class CodeTransform
 {
 public:
 	/// Create the code transformer.
-	/// @param _identifierAccess used to resolve identifiers external to the inline assembly
+	/// @param _identifierAccessCodeGen used to generate code for identifiers external to the inline assembly
 	/// As a side-effect of its construction, translates the Yul code and appends it to the
 	/// given assembly.
 	/// Throws StackTooDeepError if a variable is not accessible or if a function has too
@@ -77,7 +77,7 @@ public:
 		EVMDialect const& _dialect,
 		BuiltinContext& _builtinContext,
 		bool _allowStackOpt = false,
-		ExternalIdentifierAccess const& _identifierAccess = ExternalIdentifierAccess(),
+		ExternalIdentifierAccess::CodeGenerator const& _identifierAccessCodeGen = {},
 		bool _useNamedLabelsForFunctions = false
 	): CodeTransform(
 		_assembly,
@@ -86,7 +86,7 @@ public:
 		_allowStackOpt,
 		_dialect,
 		_builtinContext,
-		_identifierAccess,
+		_identifierAccessCodeGen,
 		_useNamedLabelsForFunctions,
 		nullptr,
 		{},
@@ -107,7 +107,7 @@ protected:
 		bool _allowStackOpt,
 		EVMDialect const& _dialect,
 		BuiltinContext& _builtinContext,
-		ExternalIdentifierAccess _identifierAccess,
+		ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen,
 		bool _useNamedLabelsForFunctions,
 		std::shared_ptr<Context> _context,
 		std::vector<TypedName> _delayedReturnVariables,
@@ -193,7 +193,7 @@ private:
 	BuiltinContext& m_builtinContext;
 	bool const m_allowStackOpt = true;
 	bool const m_useNamedLabelsForFunctions = false;
-	ExternalIdentifierAccess m_identifierAccess;
+	ExternalIdentifierAccess::CodeGenerator m_identifierAccessCodeGen;
 	std::shared_ptr<Context> m_context;
 
 	/// Set of variables whose reference counter has reached zero,

libyul/backends/evm/EVMDialect.cpp

@@ -112,13 +112,21 @@ pair<YulString, BuiltinFunctionForEVM> createFunction(
 	return {name, f};
 }
 
-set<YulString> createReservedIdentifiers()
+set<YulString> createReservedIdentifiers(langutil::EVMVersion _evmVersion)
 {
+	// TODO remove this in 0.9.0. We allow creating functions or identifiers in Yul with the name
+	// basefee for VMs before london.
+	auto baseFeeException = [&](evmasm::Instruction _instr) -> bool
+	{
+		return _instr == evmasm::Instruction::BASEFEE && _evmVersion < langutil::EVMVersion::london();
+	};
+
 	set<YulString> reserved;
 	for (auto const& instr: evmasm::c_instructions)
 	{
 		string name = instr.first;
 		transform(name.begin(), name.end(), name.begin(), [](unsigned char _c) { return tolower(_c); });
+		if (!baseFeeException(instr.second))
 			reserved.emplace(name);
 	}
 	reserved += vector<YulString>{
@@ -300,7 +308,7 @@ EVMDialect::EVMDialect(langutil::EVMVersion _evmVersion, bool _objectAccess):
 	m_objectAccess(_objectAccess),
 	m_evmVersion(_evmVersion),
 	m_functions(createBuiltins(_evmVersion, _objectAccess)),
-	m_reserved(createReservedIdentifiers())
+	m_reserved(createReservedIdentifiers(_evmVersion))
 {
 }
 

scripts/deps-ppa/static_z3.sh

@@ -24,10 +24,10 @@ set -ev
 
 keyid=70D110489D66E2F6
 email=builds@ethereum.org
-packagename=libz3-static-dev
+packagename=z3-static
-version=4.8.10
+version=4.8.12
 
-DISTRIBUTIONS="focal groovy"
+DISTRIBUTIONS="focal groovy hirsute"
 
 for distribution in $DISTRIBUTIONS
 do
@@ -62,7 +62,7 @@ mkdir debian
 echo 9 > debian/compat
 # TODO: the Z3 packages have different build dependencies
 cat <<EOF > debian/control
-Source: libz3-static-dev
+Source: z3-static
 Section: science
 Priority: extra
 Maintainer: Daniel Kirchner <daniel@ekpyron.org>
@@ -78,6 +78,22 @@ Homepage: https://github.com/Z3Prover/z3
 Vcs-Git: git://github.com/Z3Prover/z3.git
 Vcs-Browser: https://github.com/Z3Prover/z3
 
+Package: z3-static
+Architecture: any
+Breaks: z3
+Replaces: z3
+Depends: \${misc:Depends}, \${shlibs:Depends}
+Description: theorem prover from Microsoft Research
+ Z3 is a state-of-the art theorem prover from Microsoft Research. It can be
+ used to check the satisfiability of logical formulas over one or more
+ theories. Z3 offers a compelling match for software analysis and verification
+ tools, since several common software constructs map directly into supported
+ theories.
+ .
+ The Z3 input format is an extension of the one defined by the SMT-LIB 2.0
+ standard.
+
+
 Package: libz3-static-dev
 Section: libdevel
 Architecture: any-amd64
@@ -133,6 +149,9 @@ usr/include/*
 usr/lib/*/libz3.a
 usr/lib/*/cmake/z3/*
 EOF
+cat <<EOF > debian/z3-static.install
+usr/bin/z3
+EOF
 cat <<EOF > debian/copyright
 Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
 Upstream-Name: z3
@@ -179,7 +198,7 @@ This program is free software: you can redistribute it and/or modify
  Public License version 3 can be found in "/usr/share/common-licenses/GPL-3".
 EOF
 cat <<EOF > debian/changelog
-libz3-static-dev (0.0.1-1ubuntu0) saucy; urgency=low
+z3-static (0.0.1-1ubuntu0) saucy; urgency=low
 
   * Initial release.
 

scripts/error_codes.py

@@ -198,7 +198,8 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
                 # The warning may or may not exist in a compiler build.
         "4591", # "There are more than 256 warnings. Ignoring the rest."
                 # Due to 3805, the warning lists look different for different compiler builds.
-        "1834"  # Unimplemented feature error, as we do not test it anymore via cmdLineTests
+        "1834", # Unimplemented feature error, as we do not test it anymore via cmdLineTests
+        "5430"  # basefee being used in inline assembly for EVMVersion < london
     }
     assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"
     test_ids |= white_ids

scripts/release_ppa.sh

@@ -55,9 +55,9 @@ keyid=379F4801D622CDCF
 email=builds@ethereum.org
 packagename=solc
 
-static_build_distribution=focal
+static_build_distribution=hirsute
 
-DISTRIBUTIONS="focal groovy"
+DISTRIBUTIONS="focal hirsute impish"
 
 if is_release
 then

scripts/test_antlr_grammar.sh

@@ -118,7 +118,9 @@ done < <(
       grep -v -E 'literals/.*_direction_override.*.sol' |
       # Skipping a test with "revert E;" because ANTLR cannot distinguish it from
       # a variable declaration.
-      grep -v -E 'revertStatement/non_called.sol'
+      grep -v -E 'revertStatement/non_called.sol' |
+      # Skipping a test with "let basefee := ..."
+      grep -v -E 'inlineAssembly/basefee_berlin_function.sol'
 )
 
 YUL_FILES=()

scripts/tests.sh

@@ -86,7 +86,7 @@ EVM_VERSIONS="homestead byzantium"
 
 if [ -z "$CI" ]
 then
-    EVM_VERSIONS+=" constantinople petersburg istanbul berlin"
+    EVM_VERSIONS+=" constantinople petersburg istanbul berlin london"
 fi
 
 # And then run the Solidity unit-tests in the matrix combination of optimizer / no optimizer
@@ -96,9 +96,9 @@ do
     for vm in $EVM_VERSIONS
     do
         FORCE_ABIV1_RUNS="no"
-        if [[ "$vm" == "berlin" ]]
+        if [[ "$vm" == "london" ]]
         then
-            FORCE_ABIV1_RUNS="no yes" # run both in berlin
+            FORCE_ABIV1_RUNS="no yes" # run both in london
         fi
         for abiv1 in $FORCE_ABIV1_RUNS
         do

solc/CommandLineParser.cpp

@@ -86,6 +86,7 @@ static string const g_strMetadata = "metadata";
 static string const g_strMetadataHash = "metadata-hash";
 static string const g_strMetadataLiteral = "metadata-literal";
 static string const g_strModelCheckerContracts = "model-checker-contracts";
+static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
 static string const g_strModelCheckerEngine = "model-checker-engine";
 static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
 static string const g_strModelCheckerSolvers = "model-checker-solvers";
@@ -522,7 +523,7 @@ General Information)").c_str(),
 			g_strEVMVersion.c_str(),
 			po::value<string>()->value_name("version")->default_value(EVMVersion{}.name()),
 			"Select desired EVM version. Either homestead, tangerineWhistle, spuriousDragon, "
-			"byzantium, constantinople, petersburg, istanbul or berlin."
+			"byzantium, constantinople, petersburg, istanbul, berlin or london."
 		)
 		(
 			g_strExperimentalViaIR.c_str(),
@@ -720,6 +721,11 @@ General Information)").c_str(),
 			"Multiple pairs <source>:<contract> can be selected at the same time, separated by a comma "
 			"and no spaces."
 		)
+		(
+			g_strModelCheckerDivModNoSlacks.c_str(),
+			"Encode division and modulo operations with their precise operators"
+			" instead of multiplication with slack variables."
+		)
 		(
 			g_strModelCheckerEngine.c_str(),
 			po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
@@ -727,8 +733,7 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerShowUnproved.c_str(),
-			po::value<bool>()->value_name("false,true")->default_value(false),
+			"Show all unproved targets separately."
-			"Select whether to show all unproved targets."
 		)
 		(
 			g_strModelCheckerSolvers.c_str(),
@@ -737,10 +742,10 @@ General Information)").c_str(),
 		)
 		(
 			g_strModelCheckerTargets.c_str(),
-			po::value<string>()->value_name("default,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"),
+			po::value<string>()->value_name("default,all,constantCondition,underflow,overflow,divByZero,balance,assert,popEmptyArray,outOfBounds")->default_value("default"),
 			"Select model checker verification targets. "
-			"Multiple targets can be selected at the same time, separated by a comma "
+			"Multiple targets can be selected at the same time, separated by a comma and no spaces."
-			"and no spaces."
+			" By default all targets except underflow and overflow are selected."
 		)
 		(
 			g_strModelCheckerTimeout.c_str(),
@@ -1092,6 +1097,9 @@ General Information)").c_str(),
 		m_options.modelChecker.settings.contracts = move(*contracts);
 	}
 
+	if (m_args.count(g_strModelCheckerDivModNoSlacks))
+		m_options.modelChecker.settings.divModNoSlacks = true;
+
 	if (m_args.count(g_strModelCheckerEngine))
 	{
 		string engineStr = m_args[g_strModelCheckerEngine].as<string>();
@@ -1105,10 +1113,7 @@ General Information)").c_str(),
 	}
 
 	if (m_args.count(g_strModelCheckerShowUnproved))
-	{
+		m_options.modelChecker.settings.showUnproved = true;
-		bool showUnproved = m_args[g_strModelCheckerShowUnproved].as<bool>();
-		m_options.modelChecker.settings.showUnproved = showUnproved;
-	}
 
 	if (m_args.count(g_strModelCheckerSolvers))
 	{
@@ -1140,6 +1145,7 @@ General Information)").c_str(),
 	m_options.metadata.literalSources = (m_args.count(g_strMetadataLiteral) > 0);
 	m_options.modelChecker.initialize =
 		m_args.count(g_strModelCheckerContracts) ||
+		m_args.count(g_strModelCheckerDivModNoSlacks) ||
 		m_args.count(g_strModelCheckerEngine) ||
 		m_args.count(g_strModelCheckerShowUnproved) ||
 		m_args.count(g_strModelCheckerSolvers) ||

test/EVMHost.cpp

@@ -122,6 +122,8 @@ EVMHost::EVMHost(langutil::EVMVersion _evmVersion, evmc::VM& _vm):
 		m_evmRevision = EVMC_ISTANBUL;
 	else if (_evmVersion == langutil::EVMVersion::berlin())
 		m_evmRevision = EVMC_BERLIN;
+	else if (_evmVersion == langutil::EVMVersion::london())
+		m_evmRevision = EVMC_LONDON;
 	else
 		assertThrow(false, Exception, "Unsupported EVM version");
 
@@ -132,6 +134,8 @@ EVMHost::EVMHost(langutil::EVMVersion _evmVersion, evmc::VM& _vm):
 	tx_context.tx_origin = 0x9292929292929292929292929292929292929292_address;
 	// Mainnet according to EIP-155
 	tx_context.chain_id = evmc::uint256be{1};
+	// The minimum value of basefee
+	tx_context.block_base_fee = evmc::bytes32{7};
 
 	// Reserve space for recording calls.
 	if (!recorded_calls.capacity())

test/cmdlineTests.sh

@@ -169,6 +169,7 @@ EOF
         rm "$stdout_path.bak"
     else
         sed -i.bak -e '/^Warning: This is a pre-release compiler version, please do not use it in production./d' "$stderr_path"
+        sed -i.bak -e '/^Compiler run successful, no output requested\.$/d' "$stderr_path"
         sed -i.bak -e '/^Warning (3805): This is a pre-release compiler version, please do not use it in production./d' "$stderr_path"
         sed -i.bak -e 's/\(^[ ]*auxdata: \)0x[0-9a-f]*$/\1<AUXDATA REMOVED>/' "$stdout_path"
         sed -i.bak -e 's/ Consider adding "pragma .*$//' "$stderr_path"

test/cmdlineTests/abiencoderv2_no_warning/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/combined_json_generated_sources/err

@@ -1,5 +0,0 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> combined_json_generated_sources/input.sol
-
-Warning: Source file does not specify required compiler version!
---> combined_json_generated_sources/input.sol

test/cmdlineTests/combined_json_generated_sources/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/combined_json_generated_sources/input.sol

@@ -1,3 +1,5 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
 pragma abicoder v2;
 
 contract C {

test/cmdlineTests/dup_opt_peephole/err

@@ -1,5 +0,0 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> dup_opt_peephole/input.sol
-
-Warning: Source file does not specify required compiler version!
---> dup_opt_peephole/input.sol

test/cmdlineTests/dup_opt_peephole/input.sol

@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+
 contract C {
 	fallback() external {
 		assembly {

test/cmdlineTests/dup_opt_peephole/output

@@ -1,7 +1,7 @@
 
 ======= dup_opt_peephole/input.sol:C =======
 EVM assembly:
-    /* "dup_opt_peephole/input.sol":0:111  contract C {... */
+    /* "dup_opt_peephole/input.sol":60:171  contract C {... */
   mstore(0x40, 0x80)
   callvalue
   dup1
@@ -23,7 +23,7 @@ tag_1:
 stop
 
 sub_0: assembly {
-        /* "dup_opt_peephole/input.sol":0:111  contract C {... */
+        /* "dup_opt_peephole/input.sol":60:171  contract C {... */
       mstore(0x40, 0x80)
       callvalue
       dup1
@@ -35,19 +35,19 @@ sub_0: assembly {
       revert
     tag_3:
       pop
-        /* "dup_opt_peephole/input.sol":74:75  0 */
+        /* "dup_opt_peephole/input.sol":134:135  0 */
       0x00
-        /* "dup_opt_peephole/input.sol":61:76  calldataload(0) */
+        /* "dup_opt_peephole/input.sol":121:136  calldataload(0) */
       calldataload
-        /* "dup_opt_peephole/input.sol":100:101  x */
+        /* "dup_opt_peephole/input.sol":160:161  x */
       dup1
-        /* "dup_opt_peephole/input.sol":97:98  0 */
+        /* "dup_opt_peephole/input.sol":157:158  0 */
       0x00
-        /* "dup_opt_peephole/input.sol":90:102  sstore(0, x) */
+        /* "dup_opt_peephole/input.sol":150:162  sstore(0, x) */
       sstore
-        /* "dup_opt_peephole/input.sol":47:106  {... */
+        /* "dup_opt_peephole/input.sol":107:166  {... */
       pop
-        /* "dup_opt_peephole/input.sol":0:111  contract C {... */
+        /* "dup_opt_peephole/input.sol":60:171  contract C {... */
       stop
 
     auxdata: <AUXDATA REMOVED>

test/cmdlineTests/exp_base_literal/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/keccak_optimization_deploy_code/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/keccak_optimization_low_runs/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/message_format_utf8/err

@@ -1,36 +1,29 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> message_format_utf8/input.sol
-
-Warning: Source file does not specify required compiler version!
---> message_format_utf8/input.sol
-
 Warning: Statement has no effect.
- --> message_format_utf8/input.sol:2:51:
+ --> message_format_utf8/input.sol:5:51:
   |
-2 | /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; }
+5 | /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; }
   |                                        ^^^^^^^^^^^^^^^^^^^
 
 Warning: Statement has no effect.
- --> message_format_utf8/input.sol:6:25:
+ --> message_format_utf8/input.sol:9:25:
   |
-6 |                         unicode"S = π × r²";
+9 |                         unicode"S = π × r²";
   |                         ^^^^^^^^^^^^^^^^^^^
 
 Warning: Statement has no effect.
- --> message_format_utf8/input.sol:7:39:
+  --> message_format_utf8/input.sol:10:39:
    |
-7 | /* ₀₁₂₃₄⁵⁶⁷⁸⁹ */		unicode"∑ 1/n! ≈ 2.7";                 // tabs in-between
+10 | /* ₀₁₂₃₄⁵⁶⁷⁸⁹ */		unicode"∑ 1/n! ≈ 2.7";                 // tabs in-between
    |                 		^^^^^^^^^^^^^^^^^^^^^
 
 Warning: Statement has no effect.
- --> message_format_utf8/input.sol:8:30:
+  --> message_format_utf8/input.sol:11:30:
    |
-8 | /* Ŀŏŗėɯ ïƥŝʉɱ */		unicode"μὴ		χεῖρον		βέλτιστον"; // tabs in-between and inside
+11 | /* Ŀŏŗėɯ ïƥŝʉɱ */		unicode"μὴ		χεῖρον		βέλτιστον"; // tabs in-between and inside
    |                  		^^^^^^^^^^		^^^^^^		^^^^^^^^^^
 
 Warning: Function state mutability can be restricted to pure
-  --> message_format_utf8/input.sol:12:2:
+  --> message_format_utf8/input.sol:15:2:
    |
-12 | 	function selector() public returns(uint) { // starts with tab
+15 | 	function selector() public returns(uint) { // starts with tab
    | 	^ (Relevant source part starts here and spans across multiple lines).
-

test/cmdlineTests/message_format_utf8/input.sol

@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+
 contract Foo {
 /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; }
 

test/cmdlineTests/model_checker_contracts_inexistent_contract/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/model_checker_contracts_inexistent_source/exit

@@ -1 +0,0 @@
-0

test/cmdlineTests/model_checker_divModSlacks_default_all/args

@@ -0,0 +1 @@
+--model-checker-engine all

test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_default_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc

test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_default_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc

test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_all/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_all/err

@@ -0,0 +1,13 @@
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_all/input.sol:6:11:
+  |
+6 | 		return (a / b, a % b);
+  | 		        ^^^^^
+
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_all/input.sol:6:18:
+  |
+6 | 		return (a / b, a % b);
+  | 		               ^^^^^
+
+Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_divModSlacks_false_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-div-mod-no-slacks

test/cmdlineTests/model_checker_divModSlacks_false_chc/err

@@ -0,0 +1,13 @@
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_chc/input.sol:6:11:
+  |
+6 | 		return (a / b, a % b);
+  | 		        ^^^^^
+
+Warning: CHC: Error trying to invoke SMT solver.
+ --> model_checker_divModSlacks_false_chc/input.sol:6:18:
+  |
+6 | 		return (a / b, a % b);
+  | 		               ^^^^^
+
+Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+	function f(uint a, uint b) public pure returns (uint, uint) {
+		require(b != 0);
+		return (a / b, a % b);
+	}
+}

test/cmdlineTests/model_checker_engine_none/err

@@ -1,5 +0,0 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> model_checker_engine_none/input.sol
-
-Warning: Source file does not specify required compiler version!
---> model_checker_engine_none/input.sol

test/cmdlineTests/model_checker_engine_none/input.sol

@@ -1,6 +1,6 @@
-// Removed to yield a warning, otherwise CI test fails with the expectation
+// SPDX-License-Identifier: GPL-3.0
-// "no output requested"
+pragma solidity >=0.0;
-//pragma solidity >=0.0;
+
 contract test {
 	function f(uint x) public pure {
 		assert(x > 0);

test/cmdlineTests/model_checker_show_unproved_false_all_engines/args

@@ -1 +0,0 @@
---model-checker-engine all --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_all_engines/err

@@ -1,3 +0,0 @@
-Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
-
-Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_false_all_engines/input.sol

@@ -1,12 +0,0 @@
-// SPDX-License-Identifier: GPL-3.0
-pragma solidity >=0.0;
-contract C {
-    struct S {
-        uint x;
-    }
-    S s;
-    function f(bool b) public {
-        s.x |= b ? 1 : 2;
-        assert(s.x > 0);
-    }
-}

test/cmdlineTests/model_checker_show_unproved_false_bmc/args

@@ -1 +0,0 @@
---model-checker-engine bmc --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_bmc/err

@@ -1 +0,0 @@
-Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_false_bmc/input.sol

@@ -1,12 +0,0 @@
-// SPDX-License-Identifier: GPL-3.0
-pragma solidity >=0.0;
-contract C {
-    struct S {
-        uint x;
-    }
-    S s;
-    function f(bool b) public {
-        s.x |= b ? 1 : 2;
-        assert(s.x > 0);
-    }
-}

test/cmdlineTests/model_checker_show_unproved_false_chc/args

@@ -1 +0,0 @@
---model-checker-engine chc --model-checker-show-unproved false

test/cmdlineTests/model_checker_show_unproved_false_chc/err

@@ -1 +0,0 @@
-Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_false_chc/input.sol

@@ -1,12 +0,0 @@
-// SPDX-License-Identifier: GPL-3.0
-pragma solidity >=0.0;
-contract C {
-    struct S {
-        uint x;
-    }
-    S s;
-    function f(bool b) public {
-        s.x |= b ? 1 : 2;
-        assert(s.x > 0);
-    }
-}

test/cmdlineTests/model_checker_show_unproved_true_all_engines/args

@@ -1 +1 @@
---model-checker-engine all --model-checker-show-unproved true
+--model-checker-engine all --model-checker-show-unproved

test/cmdlineTests/model_checker_show_unproved_true_bmc/args

@@ -1 +1 @@
---model-checker-engine bmc --model-checker-show-unproved true
+--model-checker-engine bmc --model-checker-show-unproved

test/cmdlineTests/model_checker_show_unproved_true_chc/args

@@ -1 +1 @@
---model-checker-engine chc --model-checker-show-unproved true
+--model-checker-engine chc --model-checker-show-unproved

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/args

@@ -1 +0,0 @@
---model-checker-engine all --model-checker-show-unproved aaa

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/err

@@ -1 +0,0 @@
-the argument ('aaa') for option '--model-checker-show-unproved' is invalid. Valid choices are 'on|off', 'yes|no', '1|0' and 'true|false'

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/exit

@@ -1 +0,0 @@
-1

test/cmdlineTests/model_checker_show_unproved_wrong_all_engines/input.sol

@@ -1,12 +0,0 @@
-// SPDX-License-Identifier: GPL-3.0
-pragma solidity >=0.0;
-contract C {
-    struct S {
-        uint x;
-    }
-    S s;
-    function f(bool b) public {
-        s.x |= b ? 1 : 2;
-        assert(s.x > 0);
-    }
-}

test/cmdlineTests/model_checker_targets_all_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-targets all

test/cmdlineTests/model_checker_targets_all_all_engines/err

@@ -8,7 +8,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 0)
- --> model_checker_targets_all/input.sol:7:3:
+ --> model_checker_targets_all_all_engines/input.sol:7:3:
   |
 7 | 		--x;
   | 		^^^
@@ -23,7 +23,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 2)
- --> model_checker_targets_all/input.sol:8:3:
+ --> model_checker_targets_all_all_engines/input.sol:8:3:
   |
 8 | 		x + type(uint).max;
   | 		^^^^^^^^^^^^^^^^^^
@@ -38,7 +38,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
- --> model_checker_targets_all/input.sol:9:3:
+ --> model_checker_targets_all_all_engines/input.sol:9:3:
   |
 9 | 		2 / x;
   | 		^^^^^
@@ -53,7 +53,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:11:3:
+  --> model_checker_targets_all_all_engines/input.sol:11:3:
    |
 11 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
@@ -68,7 +68,7 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:12:3:
+  --> model_checker_targets_all_all_engines/input.sol:12:3:
    |
 12 | 		arr.pop();
    | 		^^^^^^^^^
@@ -83,20 +83,20 @@ Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0, 1)
-  --> model_checker_targets_all/input.sol:13:3:
+  --> model_checker_targets_all_all_engines/input.sol:13:3:
    |
 13 | 		arr[x];
    | 		^^^^^^
 
 Warning: BMC: Condition is always true.
- --> model_checker_targets_all/input.sol:6:11:
+ --> model_checker_targets_all_all_engines/input.sol:6:11:
   |
 6 | 		require(x >= 0);
   | 		        ^^^^^^
 Note: Callstack:
 
 Warning: BMC: Insufficient funds happens here.
-  --> model_checker_targets_all/input.sol:10:3:
+  --> model_checker_targets_all_all_engines/input.sol:10:3:
    |
 10 | 		a.transfer(x);
    | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_all_bmc/args

@@ -1 +1 @@
---model-checker-engine bmc --model-checker-targets default
+--model-checker-engine bmc --model-checker-targets all

test/cmdlineTests/model_checker_targets_all_chc/args

@@ -1 +1 @@
---model-checker-engine chc --model-checker-targets default
+--model-checker-engine chc --model-checker-targets all

test/cmdlineTests/model_checker_targets_balance_chc/err

@@ -1,2 +0,0 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> model_checker_targets_balance_chc/input.sol

test/cmdlineTests/model_checker_targets_balance_chc/input.sol

@@ -1,4 +1,6 @@
+// SPDX-License-Identifier: GPL-3.0
 pragma solidity >=0.0;
+
 contract test {
 	uint[] arr;
 	function f(address payable a, uint x) public {

test/cmdlineTests/model_checker_targets_constant_condition_chc/err

@@ -1,2 +0,0 @@
-Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
---> model_checker_targets_constant_condition_chc/input.sol

test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol

@@ -1,4 +1,6 @@
+// SPDX-License-Identifier: GPL-3.0
 pragma solidity >=0.0;
+
 contract test {
 	uint[] arr;
 	function f(address payable a, uint x) public {