Merge pull request #11742 from ethereum/develop

Merge develop into breaking

.circleci/config.yml

@@ -9,20 +9,20 @@ version: 2.1
 parameters:
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-6
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-8
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:da44d7f78e093f7f0415abf07f7c1fd1c2ed4fa65fefea428821a05186c42ec9"
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:9c3cdfc1d573d1ca3edacd892590a9a83487a1f746a6ca2093d7e009818c5179"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-6
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-8
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:c78dd9c48d393b57afe053aeb2d0d358a9f31ac85039a181724c2f8408d0bcf8"
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:61232feea23c8c57e82cf5fae890f8b86bbec353cdc04f2fcba383ca589e1d8b"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-9
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-11
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5078e1d74ab6f4329e9218c2d8c0ebe2d42817a3d4c3c62ce887100cbe9bc739"
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:4acb2674eab3e7939d6dc6caa0b8320f4dd79484325242b58473ca2875792d90"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-5
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-6
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d28afb9624c2352ea40f157d1a321ffac77f54a21e33a8e8744f9126b780ded4"
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154"
 
 orbs:
   win: circleci/windows@2.2.0
@@ -811,7 +811,7 @@ jobs:
 
   t_ems_solcjs:
     docker:
-      - image: buildpack-deps:latest
+      - image: << pipeline.parameters.ubuntu-2004-docker-image >>
     environment:
       TERM: xterm
     steps:
@@ -822,7 +822,7 @@ jobs:
           name: Install test dependencies
           command: |
             apt-get update
-            apt-get install -qqy --no-install-recommends nodejs npm cvc4
+            apt-get install -qqy --no-install-recommends nodejs npm
       - run:
           name: Test solcjs
           no_output_timeout: 30m

.circleci/osx_install_dependencies.sh

@@ -48,21 +48,23 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip
+  z3_version="z3-4.8.12"
-  unzip z3-4.8.10-x64-osx-10.15.7.zip
+  osx_version="osx-10.15.7"
-  rm -f z3-4.8.10-x64-osx-10.15.7.zip
+  wget "https://github.com/Z3Prover/z3/releases/download/$z3_version/$z3_version-x64-$osx_version.zip"
-  cp z3-4.8.10-x64-osx-10.15.7/bin/libz3.a /usr/local/lib
+  unzip "$z3_version-x64-$osx_version.zip"
-  cp z3-4.8.10-x64-osx-10.15.7/bin/z3 /usr/local/bin
+  rm -f "$z3_version-x64-$osx_version.zip"
-  cp z3-4.8.10-x64-osx-10.15.7/include/* /usr/local/include
+  cp "$z3_version-x64-$osx_version/bin/libz3.a" /usr/local/lib
-  rm -rf z3-4.8.10-x64-osx-10.15.7
+  cp "$z3_version-x64-$osx_version/bin/z3" /usr/local/bin
+  cp "$z3_version-x64-$osx_version"/include/* /usr/local/include
+  rm -rf "$z3_version-x64-$osx_version"
 
   # evmone
-  wget https://github.com/ethereum/evmone/releases/download/v0.7.0/evmone-0.7.0-darwin-x86_64.tar.gz
+  wget https://github.com/ethereum/evmone/releases/download/v0.8.0/evmone-0.8.0-darwin-x86_64.tar.gz
-  tar xzpf evmone-0.7.0-darwin-x86_64.tar.gz -C /usr/local
+  tar xzpf evmone-0.8.0-darwin-x86_64.tar.gz -C /usr/local
-  rm -f evmone-0.7.0-darwin-x86_64.tar.gz
+  rm -f evmone-0.8.0-darwin-x86_64.tar.gz
 
   # hera
-  wget https://github.com/ewasm/hera/releases/download/v0.3.2-evmc8/hera-0.3.2+commit.dc886eb7-darwin-x86_64.tar.gz
+  wget https://github.com/ewasm/hera/releases/download/v0.5.0/hera-0.5.0-darwin-x86_64.tar.gz
-  tar xzpf hera-0.3.2+commit.dc886eb7-darwin-x86_64.tar.gz -C /usr/local
+  tar xzpf hera-0.5.0-darwin-x86_64.tar.gz -C /usr/local
-  rm -f hera-0.3.2+commit.dc886eb7-darwin-x86_64.tar.gz
+  rm -f hera-0.5.0-darwin-x86_64.tar.gz
 fi

Changelog.md

@@ -14,14 +14,22 @@ Compiler Features:
  * 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``.
+ * 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``.
 
 
 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: 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/060-breaking-changes.rst

@@ -89,13 +89,13 @@ New Features
 This section lists things that were not possible prior to Solidity 0.6.0
 or were more difficult to achieve.
 
- * The :ref:`try/catch statement <try-catch>` allows you to react on failed external calls.
+* The :ref:`try/catch statement <try-catch>` allows you to react on failed external calls.
- * ``struct`` and ``enum`` types can be declared at file level.
+* ``struct`` and ``enum`` types can be declared at file level.
- * Array slices can be used for calldata arrays, for example ``abi.decode(msg.data[4:], (uint, uint))``
+* Array slices can be used for calldata arrays, for example ``abi.decode(msg.data[4:], (uint, uint))``
   is a low-level way to decode the function call payload.
- * Natspec supports multiple return parameters in developer documentation, enforcing the same naming check as ``@param``.
+* Natspec supports multiple return parameters in developer documentation, enforcing the same naming check as ``@param``.
- * Yul and Inline Assembly have a new statement called ``leave`` that exits the current function.
+* Yul and Inline Assembly have a new statement called ``leave`` that exits the current function.
- * Conversions from ``address`` to ``address payable`` are now possible via ``payable(x)``, where
+* Conversions from ``address`` to ``address payable`` are now possible via ``payable(x)``, where
   ``x`` must be of type ``address``.
 
 

docs/abi-spec.rst

@@ -78,6 +78,7 @@ The following (fixed-size) array type exists:
 - ``<type>[M]``: a fixed-length array of ``M`` elements, ``M >= 0``, of the given type.
 
   .. note::
+
       While this ABI specification can express fixed-length arrays with zero elements, they're not supported by the compiler.
 
 The following non-fixed-size types exist:
@@ -124,12 +125,12 @@ Design Criteria for the Encoding
 
 The encoding is designed to have the following properties, which are especially useful if some arguments are nested arrays:
 
-  1. The number of reads necessary to access a value is at most the depth of the value
+1. The number of reads necessary to access a value is at most the depth of the value
    inside the argument array structure, i.e. four reads are needed to retrieve ``a_i[k][l][r]``. In a
    previous version of the ABI, the number of reads scaled linearly with the total number of dynamic
    parameters in the worst case.
 
-  2. The data of a variable or array element is not interleaved with other data and it is
+2. The data of a variable or array element is not interleaved with other data and it is
    relocatable, i.e. it only uses relative "addresses".
 
 
@@ -236,6 +237,7 @@ Examples
 Given the contract:
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.4.16 <0.9.0;
@@ -312,21 +314,21 @@ these are directly the values we want to pass, whereas for the dynamic types ``u
 we use the offset in bytes to the start of their data area, measured from the start of the value
 encoding (i.e. not counting the first four bytes containing the hash of the function signature). These are:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000123`` (``0x123`` padded to 32 bytes)
+- ``0x0000000000000000000000000000000000000000000000000000000000000123`` (``0x123`` padded to 32 bytes)
- - ``0x0000000000000000000000000000000000000000000000000000000000000080`` (offset to start of data part of second parameter, 4*32 bytes, exactly the size of the head part)
+- ``0x0000000000000000000000000000000000000000000000000000000000000080`` (offset to start of data part of second parameter, 4*32 bytes, exactly the size of the head part)
- - ``0x3132333435363738393000000000000000000000000000000000000000000000`` (``"1234567890"`` padded to 32 bytes on the right)
+- ``0x3132333435363738393000000000000000000000000000000000000000000000`` (``"1234567890"`` padded to 32 bytes on the right)
- - ``0x00000000000000000000000000000000000000000000000000000000000000e0`` (offset to start of data part of fourth parameter = offset to start of data part of first dynamic parameter + size of data part of first dynamic parameter = 4\*32 + 3\*32 (see below))
+- ``0x00000000000000000000000000000000000000000000000000000000000000e0`` (offset to start of data part of fourth parameter = offset to start of data part of first dynamic parameter + size of data part of first dynamic parameter = 4\*32 + 3\*32 (see below))
 
 After this, the data part of the first dynamic argument, ``[0x456, 0x789]`` follows:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements of the array, 2)
+- ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements of the array, 2)
- - ``0x0000000000000000000000000000000000000000000000000000000000000456`` (first element)
+- ``0x0000000000000000000000000000000000000000000000000000000000000456`` (first element)
- - ``0x0000000000000000000000000000000000000000000000000000000000000789`` (second element)
+- ``0x0000000000000000000000000000000000000000000000000000000000000789`` (second element)
 
 Finally, we encode the data part of the second dynamic argument, ``"Hello, world!"``:
 
- - ``0x000000000000000000000000000000000000000000000000000000000000000d`` (number of elements (bytes in this case): 13)
+- ``0x000000000000000000000000000000000000000000000000000000000000000d`` (number of elements (bytes in this case): 13)
- - ``0x48656c6c6f2c20776f726c642100000000000000000000000000000000000000`` (``"Hello, world!"`` padded to 32 bytes on the right)
+- ``0x48656c6c6f2c20776f726c642100000000000000000000000000000000000000`` (``"Hello, world!"`` padded to 32 bytes on the right)
 
 All together, the encoding is (newline after function selector and each 32-bytes for clarity):
 
@@ -348,14 +350,14 @@ with values ``([[1, 2], [3]], ["one", "two", "three"])`` but start from the most
 
 First we encode the length and data of the first embedded dynamic array ``[1, 2]`` of the first root array ``[[1, 2], [3]]``:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements in the first array, 2; the elements themselves are ``1`` and ``2``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements in the first array, 2; the elements themselves are ``1`` and ``2``)
- - ``0x0000000000000000000000000000000000000000000000000000000000000001`` (first element)
+- ``0x0000000000000000000000000000000000000000000000000000000000000001`` (first element)
- - ``0x0000000000000000000000000000000000000000000000000000000000000002`` (second element)
+- ``0x0000000000000000000000000000000000000000000000000000000000000002`` (second element)
 
 Then we encode the length and data of the second embedded dynamic array ``[3]`` of the first root array ``[[1, 2], [3]]``:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000001`` (number of elements in the second array, 1; the element is ``3``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000001`` (number of elements in the second array, 1; the element is ``3``)
- - ``0x0000000000000000000000000000000000000000000000000000000000000003`` (first element)
+- ``0x0000000000000000000000000000000000000000000000000000000000000003`` (first element)
 
 Then we need to find the offsets ``a`` and ``b`` for their respective dynamic arrays ``[1, 2]`` and ``[3]``.
 To calculate the offsets we can take a look at the encoded data of the first root array ``[[1, 2], [3]]``
@@ -380,12 +382,12 @@ thus ``b = 0x00000000000000000000000000000000000000000000000000000000000000a0``.
 
 Then we encode the embedded strings of the second root array:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of characters in word ``"one"``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of characters in word ``"one"``)
- - ``0x6f6e650000000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"one"``)
+- ``0x6f6e650000000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"one"``)
- - ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of characters in word ``"two"``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of characters in word ``"two"``)
- - ``0x74776f0000000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"two"``)
+- ``0x74776f0000000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"two"``)
- - ``0x0000000000000000000000000000000000000000000000000000000000000005`` (number of characters in word ``"three"``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000005`` (number of characters in word ``"three"``)
- - ``0x7468726565000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"three"``)
+- ``0x7468726565000000000000000000000000000000000000000000000000000000`` (utf8 representation of word ``"three"``)
 
 In parallel to the first root array, since strings are dynamic elements we need to find their offsets ``c``, ``d`` and ``e``:
 
@@ -416,11 +418,11 @@ and have the same encodings for a function with a signature ``g(string[],uint[][
 
 Then we encode the length of the first root array:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements in the first root array, 2; the elements themselves are ``[1, 2]``  and ``[3]``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000002`` (number of elements in the first root array, 2; the elements themselves are ``[1, 2]``  and ``[3]``)
 
 Then we encode the length of the second root array:
 
- - ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of strings in the second root array, 3; the strings themselves are ``"one"``, ``"two"`` and ``"three"``)
+- ``0x0000000000000000000000000000000000000000000000000000000000000003`` (number of strings in the second root array, 3; the strings themselves are ``"one"``, ``"two"`` and ``"three"``)
 
 Finally we find the offsets ``f`` and ``g`` for their respective root dynamic arrays ``[[1, 2], [3]]`` and
 ``["one", "two", "three"]``, and assemble parts in the correct order:
@@ -656,7 +658,7 @@ As an example, the code
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.4 <0.9.0;
+    pragma solidity >=0.7.5 <0.9.0;
     pragma abicoder v2;
 
     contract Test {
@@ -761,16 +763,17 @@ As an example, the encoding of ``int16(-1), bytes1(0x42), uint16(0x03), string("
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^ string("Hello, world!") without a length field
 
 More specifically:
- - During the encoding, everything is encoded in-place. This means that there is
+
+- During the encoding, everything is encoded in-place. This means that there is
   no distinction between head and tail, as in the ABI encoding, and the length
   of an array is not encoded.
- - The direct arguments of ``abi.encodePacked`` are encoded without padding,
+- The direct arguments of ``abi.encodePacked`` are encoded without padding,
   as long as they are not arrays (or ``string`` or ``bytes``).
- - The encoding of an array is the concatenation of the
+- The encoding of an array is the concatenation of the
   encoding of its elements **with** padding.
- - Dynamically-sized types like ``string``, ``bytes`` or ``uint[]`` are encoded
+- Dynamically-sized types like ``string``, ``bytes`` or ``uint[]`` are encoded
   without their length field.
- - The encoding of ``string`` or ``bytes`` does not apply padding at the end
+- The encoding of ``string`` or ``bytes`` does not apply padding at the end
   unless it is part of an array or struct (then it is padded to a multiple of
   32 bytes).
 
@@ -801,11 +804,11 @@ Indexed event parameters that are not value types, i.e. arrays and structs are n
 stored directly but instead a keccak256-hash of an encoding is stored. This encoding
 is defined as follows:
 
- - the encoding of a ``bytes`` and ``string`` value is just the string contents
+- the encoding of a ``bytes`` and ``string`` value is just the string contents
   without any padding or length prefix.
- - the encoding of a struct is the concatenation of the encoding of its members,
+- the encoding of a struct is the concatenation of the encoding of its members,
   always padded to a multiple of 32 bytes (even ``bytes`` and ``string``).
- - the encoding of an array (both dynamically- and statically-sized) is
+- the encoding of an array (both dynamically- and statically-sized) is
   the concatenation of the encoding of its elements, always padded to a multiple
   of 32 bytes (even ``bytes`` and ``string``) and without any length prefix
 

docs/assembly.rst

@@ -234,7 +234,7 @@ This means that the allocatable memory starts at ``0x80``, which is the initial
 of the free memory pointer.
 
 Elements in memory arrays in Solidity always occupy multiples of 32 bytes (this is
-even true for ``byte[]``, but not for ``bytes`` and ``string``). Multi-dimensional memory
+even true for ``bytes1[]``, but not for ``bytes`` and ``string``). Multi-dimensional memory
 arrays are pointers to memory arrays. The length of a dynamic array is stored at the
 first slot of the array and followed by the array elements.
 

docs/bugs.rst

@@ -19,14 +19,14 @@ which can be used to check which bugs affect a specific version of the compiler.
 Contract source verification tools and also other tools interacting with
 contracts should consult this list according to the following criteria:
 
- - It is mildly suspicious if a contract was compiled with a nightly
+- It is mildly suspicious if a contract was compiled with a nightly
   compiler version instead of a released version. This list does not keep
   track of unreleased or nightly versions.
- - It is also mildly suspicious if a contract was compiled with a version that was
+- It is also mildly suspicious if a contract was compiled with a version that was
   not the most recent at the time the contract was created. For contracts
   created from other contracts, you have to follow the creation chain
   back to a transaction and use the date of that transaction as creation date.
- - It is highly suspicious if a contract was compiled with a compiler that
+- It is highly suspicious if a contract was compiled with a compiler that
   contains a known bug and the contract was created at a time where a newer
   compiler version containing a fix was already released.
 

docs/cheatsheet.rst

@@ -158,7 +158,8 @@ Global Variables
 Function Visibility Specifiers
 ==============================
 
-::
+.. code-block:: solidity
+    :force:
 
     function myFunction() <visibility specifier> returns (bool) {
         return true;
@@ -192,8 +193,8 @@ Reserved Keywords
 
 These keywords are reserved in Solidity. They might become part of the syntax in the future:
 
-``after``, ``alias``, ``apply``, ``auto``, ``case``, ``copyof``, ``default``,
+``after``, ``alias``, ``apply``, ``auto``, ``byte``, ``case``, ``copyof``, ``default``,
-``define``, ``final``, ``immutable``, ``implements``, ``in``, ``inline``, ``let``, ``macro``, ``match``,
+``define``, ``final``, ``implements``, ``in``, ``inline``, ``let``, ``macro``, ``match``,
 ``mutable``, ``null``, ``of``, ``partial``, ``promise``, ``reference``, ``relocatable``,
 ``sealed``, ``sizeof``, ``static``, ``supports``, ``switch``, ``typedef``, ``typeof``,
-``unchecked``.
+``var``.

docs/common-patterns.rst

@@ -130,6 +130,7 @@ The use of **function modifiers** makes these
 restrictions highly readable.
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity ^0.8.4;
@@ -293,6 +294,7 @@ function finishes.
     will run even if the function explicitly returns.
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity ^0.8.4;

docs/conf.py

@@ -23,9 +23,11 @@ from pygments_lexer_solidity import SolidityLexer, YulLexer
 # add these directories to sys.path here. If the directory is relative to the
 # documentation root, use os.path.abspath to make it absolute, like shown here.
 
+ROOT_PATH = os.path.dirname(os.path.realpath(__file__))
+
+sys.path.insert(0, os.path.join(ROOT_PATH, 'ext'))
+
 def setup(sphinx):
-    thisdir = os.path.dirname(os.path.realpath(__file__))
-    sys.path.insert(0, thisdir + '/utils')
     sphinx.add_lexer('Solidity', SolidityLexer)
     sphinx.add_lexer('Yul', YulLexer)
 
@@ -39,7 +41,10 @@ def setup(sphinx):
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = [ 'sphinx_a4doc' ]
+extensions = [
+    'sphinx_a4doc',
+    'html_extra_template_renderer',
+]
 
 a4_base_path = os.path.dirname(__file__) + '/grammar'
 
@@ -156,7 +161,20 @@ html_js_files = ["js/toggle.js"]
 # Add any extra paths that contain custom files (such as robots.txt or
 # .htaccess) here, relative to this directory. These files are copied
 # directly to the root of the documentation.
-html_extra_path = ["_static/css", "_static/robots.txt"]
+html_extra_path = ["_static/css"]
+
+# List of templates of static files to be included in the HTML output.
+# Keys represent paths to input files and values are dicts containing:
+# - target: The path where the rendered template should be placed.
+# - context: A dictionary listing variables that can be used inside the template.
+# All paths must be absolute.
+# Rendered templates are automatically added to html_extra_path setting.
+html_extra_templates = {
+    os.path.join(ROOT_PATH, "robots.txt.template"): {
+        'target': os.path.join(ROOT_PATH, "_static/robots.txt"),
+        'context': {'LATEST_VERSION': version},
+    }
+}
 
 # If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
 # using the given strftime format.

docs/contracts/events.rst

@@ -73,7 +73,7 @@ four indexed arguments rather than three.
     In particular, it is possible to "fake" the signature of another event
     using an anonymous event.
 
-::
+.. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.4.21 <0.9.0;
@@ -97,7 +97,7 @@ four indexed arguments rather than three.
 
 The use in the JavaScript API is as follows:
 
-::
+.. code-block:: javascript
 
     var abi = /* abi as generated by the compiler */;
     var ClientReceipt = web3.eth.contract(abi);

docs/contracts/function-modifiers.rst

@@ -18,7 +18,7 @@ if they are marked ``virtual``. For details, please see
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.0 <0.9.0;
+    pragma solidity >=0.7.1 <0.9.0;
 
     contract owned {
         constructor() { owner = payable(msg.sender); }

docs/contracts/functions.rst

@@ -15,7 +15,7 @@ that call them, similar to internal library functions.
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.0 <0.9.0;
+    pragma solidity >=0.7.1 <0.9.0;
 
     function sum(uint[] memory _arr) pure returns (uint s) {
         for (uint i = 0; i < _arr.length; i++)

docs/contracts/libraries.rst

@@ -130,9 +130,10 @@ internal functions in libraries in order to implement
 custom types without the overhead of external function calls:
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >=0.6.8 <0.9.0;
+    pragma solidity ^0.8.0;
 
     struct bigint {
         uint[] limbs;
@@ -150,12 +151,15 @@ custom types without the overhead of external function calls:
             for (uint i = 0; i < r.limbs.length; ++i) {
                 uint a = limb(_a, i);
                 uint b = limb(_b, i);
+                unchecked {
                     r.limbs[i] = a + b + carry;
+
                     if (a + b < a || (a + b == type(uint).max && carry > 0))
                         carry = 1;
                     else
                         carry = 0;
                 }
+            }
             if (carry > 0) {
                 // too bad, we have to add a limb
                 uint[] memory newLimbs = new uint[](r.limbs.length + 1);
@@ -223,13 +227,13 @@ following an internal naming schema and arguments of types not supported in the
 
 The following identifiers are used for the types in the signatures:
 
- - Value types, non-storage ``string`` and non-storage ``bytes`` use the same identifiers as in the contract ABI.
+- Value types, non-storage ``string`` and non-storage ``bytes`` use the same identifiers as in the contract ABI.
- - Non-storage array types follow the same convention as in the contract ABI, i.e. ``<type>[]`` for dynamic arrays and
+- Non-storage array types follow the same convention as in the contract ABI, i.e. ``<type>[]`` for dynamic arrays and
   ``<type>[M]`` for fixed-size arrays of ``M`` elements.
- - Non-storage structs are referred to by their fully qualified name, i.e. ``C.S`` for ``contract C { struct S { ... } }``.
+- Non-storage structs are referred to by their fully qualified name, i.e. ``C.S`` for ``contract C { struct S { ... } }``.
- - Storage pointer mappings use ``mapping(<keyType> => <valueType>) storage`` where ``<keyType>`` and ``<valueType>`` are
+- Storage pointer mappings use ``mapping(<keyType> => <valueType>) storage`` where ``<keyType>`` and ``<valueType>`` are
   the identifiers for the key and value types of the mapping, respectively.
- - Other storage pointer types use the type identifier of their corresponding non-storage type, but append a single space
+- Other storage pointer types use the type identifier of their corresponding non-storage type, but append a single space
   followed by ``storage`` to it.
 
 The argument encoding is the same as for the regular contract ABI, except for storage pointers, which are encoded as a

docs/contracts/visibility-and-getters.rst

@@ -188,16 +188,24 @@ The next example is more complex:
             uint a;
             bytes3 b;
             mapping (uint => uint) map;
+            uint[3] c;
+            uint[] d;
+            bytes e;
         }
         mapping (uint => mapping(bool => Data[])) public data;
     }
 
-It generates a function of the following form. The mapping in the struct is omitted
+It generates a function of the following form. The mapping and arrays (with the
-because there is no good way to provide the key for the mapping:
+exception of byte arrays) in the struct are omitted because there is no good way
+to select individual struct members or provide a key for the mapping:
 
 .. code-block:: solidity
 
-    function data(uint arg1, bool arg2, uint arg3) public returns (uint a, bytes3 b) {
+    function data(uint arg1, bool arg2, uint arg3)
+        public
+        returns (uint a, bytes3 b, bytes memory e)
+    {
         a = data[arg1][arg2][arg3].a;
         b = data[arg1][arg2][arg3].b;
+        e = data[arg1][arg2][arg3].e;
     }

docs/contributing.rst

@@ -112,7 +112,7 @@ starting from the current directory. The required file is called ``libevmone.so`
 ``evmone.dll`` on Windows systems and ``libevmone.dylib`` on macOS. If it is not found, tests that
 use it are skipped. These tests are ``libsolididty/semanticTests``, ``libsolidity/GasCosts``,
 ``libsolidity/SolidityEndToEndTest``, part of the soltest suite. To run all tests, download the library from
-`GitHub <https://github.com/ethereum/evmone/releases/tag/v0.7.0>`_
+`GitHub <https://github.com/ethereum/evmone/releases/tag/v0.8.0>`_
 and place it in the project root path or inside the ``deps`` folder.
 
 If the ``libz3`` library is not installed on your system, you should disable the
@@ -324,7 +324,7 @@ from the documentation or the other tests:
     # extract from tests:
     path/to/solidity/scripts/isolate_tests.py path/to/solidity/test/libsolidity/SolidityEndToEndTest.cpp
     # extract from documentation:
-    path/to/solidity/scripts/isolate_tests.py path/to/solidity/docs docs
+    path/to/solidity/scripts/isolate_tests.py path/to/solidity/docs
 
 The AFL documentation states that the corpus (the initial input files) should not be
 too large. The files themselves should not be larger than 1 kB and there should be

docs/control-structures.rst

@@ -660,6 +660,7 @@ The following example shows how you can use ``require`` to check conditions on i
 and ``assert`` for internal error checking.
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.5.0 <0.9.0;
@@ -786,7 +787,7 @@ A failure in an external call can be caught using a try/catch statement, as foll
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+    pragma solidity >=0.8.1;
 
     interface DataFeed { function getData(address token) external returns (uint value); }
 

docs/examples/blind-auction.rst

@@ -192,6 +192,7 @@ invalid bids.
 
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity ^0.8.4;

docs/ext/html_extra_template_renderer.py

@@ -0,0 +1,45 @@
+import os.path
+
+
+def render_html_extra_templates(app):
+    if app.builder.format != 'html':
+        # Non-HTML builders do not provide .templates.render_string(). Note that a HTML
+        # builder is still used also when building some other formats like json or epub.
+        return
+
+    for input_path, template_config in app.config.html_extra_templates.items():
+        # Requiring absolute paths simplifies the implementation.
+        if not os.path.isabs(input_path):
+            raise RuntimeError(f"Template input path is not absolute: {input_path}")
+        if not os.path.isabs(template_config['target']):
+            raise RuntimeError(f"Template target path is not absolute: {template_config['target']}")
+
+        with open(input_path, 'r') as input_file:
+            # This runs Jinja2, which supports rendering {{ }} tags among other things.
+            rendered_template = app.builder.templates.render_string(
+                input_file.read(),
+                template_config['context'],
+            )
+
+        with open(template_config['target'], 'w') as target_file:
+            target_file.write(rendered_template)
+
+        app.config.html_extra_path.append(template_config['target'])
+
+
+def setup(app):
+    app.add_config_value('html_extra_templates', default={}, rebuild='', types=dict)
+
+    # Register a handler for the env-before-read-docs event. Any event that's fired before static
+    # files get copied would do.
+    app.connect(
+        'env-before-read-docs',
+        lambda app, env, docnames: render_html_extra_templates(app)
+    )
+
+    return {
+        # NOTE: Need to access _raw_config here because setup() runs before app.config is ready.
+        'version': app.config._raw_config['version'],  # pylint: disable=protected-access
+        'parallel_read_safe': True,
+        'parallel_write_safe': True,
+    }

docs/internals/layout_in_memory.rst

@@ -19,7 +19,7 @@ Solidity always places new objects at the free memory pointer and
 memory is never freed (this might change in the future).
 
 Elements in memory arrays in Solidity always occupy multiples of 32 bytes (this
-is even true for ``byte[]``, but not for ``bytes`` and ``string``).
+is even true for ``bytes1[]``, but not for ``bytes`` and ``string``).
 Multi-dimensional memory arrays are pointers to memory arrays. The length of a
 dynamic array is stored at the first slot of the array and followed by the array
 elements.

docs/internals/layout_in_storage.rst

@@ -127,7 +127,7 @@ The type of the value is ``uint256``, so it uses a single slot.
 ------------------------
 
 ``bytes`` and ``string`` are encoded identically.
-In general, the encoding is similar to ``byte1[]``, in the sense that there is a slot for the array itself and
+In general, the encoding is similar to ``bytes1[]``, in the sense that there is a slot for the array itself and
 a data area that is computed using a ``keccak256`` hash of that slot's position.
 However, for short values (shorter than 32 bytes) the array elements are stored together with the length in the same slot.
 

docs/internals/optimizer.rst

@@ -49,6 +49,8 @@ differences, for example, functions may be inlined, combined, or rewritten to el
 redundancies, etc. (compare the output between the flags ``--ir`` and
 ``--optimize --ir-optimized``).
 
+.. _optimizer-parameter-runs:
+
 Optimizer Parameter Runs
 ========================
 
@@ -269,11 +271,11 @@ backtracking.
 All components of the Yul-based optimizer module are explained below.
 The following transformation steps are the main components:
 
- - SSA Transform
+- SSA Transform
- - Common Subexpression Eliminator
+- Common Subexpression Eliminator
- - Expression Simplifier
+- Expression Simplifier
- - Redundant Assign Eliminator
+- Redundant Assign Eliminator
- - Full Function Inliner
+- Full Function Inliner
 
 Optimizer Steps
 ---------------
@@ -281,36 +283,36 @@ Optimizer Steps
 This is a list of all steps the Yul-based optimizer sorted alphabetically. You can find more information
 on the individual steps and their sequence below.
 
- - :ref:`block-flattener`.
+- :ref:`block-flattener`.
- - :ref:`circular-reference-pruner`.
+- :ref:`circular-reference-pruner`.
- - :ref:`common-subexpression-eliminator`.
+- :ref:`common-subexpression-eliminator`.
- - :ref:`conditional-simplifier`.
+- :ref:`conditional-simplifier`.
- - :ref:`conditional-unsimplifier`.
+- :ref:`conditional-unsimplifier`.
- - :ref:`control-flow-simplifier`.
+- :ref:`control-flow-simplifier`.
- - :ref:`dead-code-eliminator`.
+- :ref:`dead-code-eliminator`.
- - :ref:`equivalent-function-combiner`.
+- :ref:`equivalent-function-combiner`.
- - :ref:`expression-joiner`.
+- :ref:`expression-joiner`.
- - :ref:`expression-simplifier`.
+- :ref:`expression-simplifier`.
- - :ref:`expression-splitter`.
+- :ref:`expression-splitter`.
- - :ref:`for-loop-condition-into-body`.
+- :ref:`for-loop-condition-into-body`.
- - :ref:`for-loop-condition-out-of-body`.
+- :ref:`for-loop-condition-out-of-body`.
- - :ref:`for-loop-init-rewriter`.
+- :ref:`for-loop-init-rewriter`.
- - :ref:`functional-inliner`.
+- :ref:`functional-inliner`.
- - :ref:`function-grouper`.
+- :ref:`function-grouper`.
- - :ref:`function-hoister`.
+- :ref:`function-hoister`.
- - :ref:`function-specializer`.
+- :ref:`function-specializer`.
- - :ref:`literal-rematerialiser`.
+- :ref:`literal-rematerialiser`.
- - :ref:`load-resolver`.
+- :ref:`load-resolver`.
- - :ref:`loop-invariant-code-motion`.
+- :ref:`loop-invariant-code-motion`.
- - :ref:`redundant-assign-eliminator`.
+- :ref:`redundant-assign-eliminator`.
- - :ref:`reasoning-based-simplifier`.
+- :ref:`reasoning-based-simplifier`.
- - :ref:`rematerialiser`.
+- :ref:`rematerialiser`.
- - :ref:`SSA-reverser`.
+- :ref:`SSA-reverser`.
- - :ref:`SSA-transform`.
+- :ref:`SSA-transform`.
- - :ref:`structural-simplifier`.
+- :ref:`structural-simplifier`.
- - :ref:`unused-function-parameter-pruner`.
+- :ref:`unused-function-parameter-pruner`.
- - :ref:`unused-pruner`.
+- :ref:`unused-pruner`.
- - :ref:`var-decl-initializer`.
+- :ref:`var-decl-initializer`.
 
 Selecting Optimizations
 -----------------------
@@ -519,7 +521,7 @@ compact again at the end.
 ExpressionSplitter
 ^^^^^^^^^^^^^^^^^^
 
-The expression splitter turns expressions like ``add(mload(x), mul(mload(y), 0x20))``
+The expression splitter turns expressions like ``add(mload(0x123), mul(mload(0x456), 0x20))``
 into a sequence of declarations of unique variables that are assigned sub-expressions
 of that expression so that each function call has only variables or literals
 as arguments.
@@ -529,9 +531,9 @@ The above would be transformed into
 .. code-block:: yul
 
     {
-        let _1 := mload(y)
+        let _1 := mload(0x123)
         let _2 := mul(_1, 0x20)
-        let _3 := mload(x)
+        let _3 := mload(0x456)
         let z := add(_3, _2)
     }
 
@@ -589,8 +591,8 @@ For any variable ``a`` that is assigned to somewhere in the code
 (variables that are declared with value and never re-assigned
 are not modified) perform the following transforms:
 
- - replace ``let a := v`` by ``let a_i := v   let a := a_i``
+- replace ``let a := v`` by ``let a_i := v   let a := a_i``
- - replace ``a := v`` by ``let a_i := v   a := a_i`` where ``i`` is a number such that ``a_i`` is yet unused.
+- replace ``a := v`` by ``let a_i := v   a := a_i`` where ``i`` is a number such that ``a_i`` is yet unused.
 
 Furthermore, always record the current value of ``i`` used for ``a`` and replace each
 reference to ``a`` by ``a_i``.
@@ -633,7 +635,7 @@ The SSA transform converts this snippet to the following:
 
     {
         let a_1 := 1
-        a := a_1
+        let a := a_1
         let a_2 := mload(a_1)
         a := a_2
         let a_3 := sload(a_2)
@@ -677,9 +679,9 @@ joins, the two mappings coming from the two branches are combined in the followi
 Statements that are only in one mapping or have the same state are used unchanged.
 Conflicting values are resolved in the following way:
 
- - "unused", "undecided" -> "undecided"
+- "unused", "undecided" -> "undecided"
- - "unused", "used" -> "used"
+- "unused", "used" -> "used"
- - "undecided, "used" -> "used"
+- "undecided, "used" -> "used"
 
 For for-loops, the condition, body and post-part are visited twice, taking
 the joining control-flow at the condition into account.
@@ -696,7 +698,7 @@ operation where ``unused = 0``, ``undecided = 1`` and ``used = 2``.
 
 The proper way would be to compute
 
-::
+.. code-block:: none
 
     max(s, f(s), f(f(s)), f(f(f(s))), ...)
 
@@ -705,7 +707,7 @@ iterating it has to reach a cycle after at most three iterations,
 and thus ``f(f(f(s)))`` has to equal one of ``s``, ``f(s)``, or ``f(f(s))``
 and thus
 
-::
+.. code-block:: none
 
     max(s, f(s), f(f(s))) = max(s, f(s), f(f(s)), f(f(f(s))), ...).
 
@@ -735,10 +737,10 @@ is side-effect free and its evaluation only depends on the values of variables
 and the call-constant state of the environment. Most expressions are movable.
 The following parts make an expression non-movable:
 
- - function calls (might be relaxed in the future if all statements in the function are movable)
+- function calls (might be relaxed in the future if all statements in the function are movable)
- - opcodes that (can) have side-effects (like ``call`` or ``selfdestruct``)
+- opcodes that (can) have side-effects (like ``call`` or ``selfdestruct``)
- - opcodes that read or write memory, storage or external state information
+- opcodes that read or write memory, storage or external state information
- - opcodes that depend on the current PC, memory size or returndata size
+- opcodes that depend on the current PC, memory size or returndata size
 
 DataflowAnalyzer
 ^^^^^^^^^^^^^^^^
@@ -836,8 +838,8 @@ ReasoningBasedSimplifier
 
 This optimizer uses SMT solvers to check whether ``if`` conditions are constant.
 
- - If ``constraints AND condition`` is UNSAT, the condition is never true and the whole body can be removed.
+- If ``constraints AND condition`` is UNSAT, the condition is never true and the whole body can be removed.
- - If ``constraints AND NOT condition`` is UNSAT, the condition is always true and can be replaced by ``1``.
+- If ``constraints AND NOT condition`` is UNSAT, the condition is always true and can be replaced by ``1``.
 
 The simplifications above can only be applied if the condition is movable.
 
@@ -872,13 +874,13 @@ we cannot assign a specific value.
 
 Current features:
 
- - switch cases: insert "<condition> := <caseLabel>"
+- switch cases: insert "<condition> := <caseLabel>"
- - after if statement with terminating control-flow, insert "<condition> := 0"
+- after if statement with terminating control-flow, insert "<condition> := 0"
 
 Future features:
 
- - allow replacements by "1"
+- allow replacements by "1"
- - take termination of user-defined functions into account
+- take termination of user-defined functions into account
 
 Works best with SSA form and if dead code removal has run before.
 
@@ -898,15 +900,15 @@ ControlFlowSimplifier
 
 Simplifies several control-flow structures:
 
- - replace if with empty body with pop(condition)
+- replace if with empty body with pop(condition)
- - remove empty default switch case
+- remove empty default switch case
- - remove empty switch case if no default case exists
+- remove empty switch case if no default case exists
- - replace switch with no cases with pop(expression)
+- replace switch with no cases with pop(expression)
- - turn switch with single case into if
+- turn switch with single case into if
- - replace switch with only default case with pop(expression) and body
+- replace switch with only default case with pop(expression) and body
- - replace switch with const expr with matching case body
+- replace switch with const expr with matching case body
- - replace ``for`` with terminating control flow and without other break/continue by ``if``
+- replace ``for`` with terminating control flow and without other break/continue by ``if``
- - remove ``leave`` at the end of a function.
+- remove ``leave`` at the end of a function.
 
 None of these operations depend on the data flow. The StructuralSimplifier
 performs similar tasks that do depend on data flow.
@@ -956,13 +958,13 @@ StructuralSimplifier
 This is a general step that performs various kinds of simplifications on
 a structural level:
 
- - replace if statement with empty body by ``pop(condition)``
+- replace if statement with empty body by ``pop(condition)``
- - replace if statement with true condition by its body
+- replace if statement with true condition by its body
- - remove if statement with false condition
+- remove if statement with false condition
- - turn switch with single case into if
+- turn switch with single case into if
- - replace switch with only default case by ``pop(expression)`` and body
+- replace switch with only default case by ``pop(expression)`` and body
- - replace switch with literal expression by matching case body
+- replace switch with literal expression by matching case body
- - replace for loop with false condition by its initialization part
+- replace for loop with false condition by its initialization part
 
 This component uses the Dataflow Analyzer.
 
@@ -1008,8 +1010,8 @@ declarations inside conditional branches will not be moved out of the loop.
 
 Requirements:
 
- - The Disambiguator, ForLoopInitRewriter and FunctionHoister must be run upfront.
+- The Disambiguator, ForLoopInitRewriter and FunctionHoister must be run upfront.
- - Expression splitter and SSA transform should be run upfront to obtain better result.
+- Expression splitter and SSA transform should be run upfront to obtain better result.
 
 
 Function-Level Optimizations
@@ -1089,14 +1091,14 @@ FunctionalInliner
 This component of the optimizer performs restricted function inlining by inlining functions that can be
 inlined inside functional expressions, i.e. functions that:
 
- - return a single value.
+- return a single value.
- - have a body like ``r := <functional expression>``.
+- have a body like ``r := <functional expression>``.
- - neither reference themselves nor ``r`` in the right hand side.
+- neither reference themselves nor ``r`` in the right hand side.
 
 Furthermore, for all parameters, all of the following need to be true:
 
- - The argument is movable.
+- The argument is movable.
- - The parameter is either referenced less than twice in the function body, or the argument is rather cheap
+- The parameter is either referenced less than twice in the function body, or the argument is rather cheap
   ("cost" of at most 1, like a constant up to 0xff).
 
 Example: The function to be inlined has the form of ``function f(...) -> r { r := E }`` where
@@ -1186,16 +1188,18 @@ The SSA transform rewrites
 
 .. code-block:: yul
 
-    a := E
+    let a := calldataload(0)
     mstore(a, 1)
 
 to
 
 .. code-block:: yul
 
-    let a_1 := E
+    let a_1 := calldataload(0)
-    a := a_1
+    let a := a_1
     mstore(a_1, 1)
+    let a_2 := calldataload(0x20)
+    a := a_2
 
 The problem is that instead of ``a``, the variable ``a_1`` is used
 whenever ``a`` was referenced. The SSA transform changes statements
@@ -1204,9 +1208,11 @@ snippet is turned into
 
 .. code-block:: yul
 
-    a := E
+    let a := calldataload(0)
     let a_1 := a
     mstore(a_1, 1)
+    a := calldataload(0x20)
+    let a_2 := a
 
 This is a very simple equivalence transform, but when we now run the
 Common Subexpression Eliminator, it will replace all occurrences of ``a_1``
@@ -1259,7 +1265,7 @@ Reverses the transformation of ForLoopConditionIntoBody.
 
 For any movable ``c``, it turns
 
-::
+.. code-block:: none
 
     for { ... } 1 { ... } {
     if iszero(c) { break }
@@ -1268,7 +1274,7 @@ For any movable ``c``, it turns
 
 into
 
-::
+.. code-block:: none
 
     for { ... } c { ... } {
     ...
@@ -1276,7 +1282,7 @@ into
 
 and it turns
 
-::
+.. code-block:: none
 
     for { ... } 1 { ... } {
     if c { break }
@@ -1285,7 +1291,7 @@ and it turns
 
 into
 
-::
+.. code-block:: none
 
     for { ... } iszero(c) { ... } {
     ...

docs/internals/source_mappings.rst

@@ -56,8 +56,8 @@ used in a single modifier.
 In order to compress these source mappings especially for bytecode, the
 following rules are used:
 
- - If a field is empty, the value of the preceding element is used.
+- If a field is empty, the value of the preceding element is used.
- - If a ``:`` is missing, all following fields are considered empty.
+- If a ``:`` is missing, all following fields are considered empty.
 
 This means the following source mappings represent the same information:
 

docs/introduction-to-smart-contracts.rst

@@ -140,7 +140,9 @@ of a keypair belonging to :ref:`external accounts<accounts>`.
 The keyword ``public`` automatically generates a function that allows you to access the current value of the state
 variable from outside of the contract. Without this keyword, other contracts have no way to access the variable.
 The code of the function generated by the compiler is equivalent
-to the following (ignore ``external`` and ``view`` for now)::
+to the following (ignore ``external`` and ``view`` for now):
+
+.. code-block:: solidity
 
     function minter() external view returns (address) { return minter; }
 
@@ -162,7 +164,9 @@ even better, keep a list, or use a more suitable data type.
 
 The :ref:`getter function<getter-functions>` created by the ``public`` keyword
 is more complex in the case of a mapping. It looks like the
-following::
+following:
+
+.. code-block:: solidity
 
     function balances(address _account) external view returns (uint) {
         return balances[_account];

docs/ir/ir-breaking-changes.rst

@@ -1,6 +1,6 @@
-********************************
+*********************************
 Solidity IR-based Codegen Changes
-********************************
+*********************************
 
 This section highlights the main differences between the old and the IR-based codegen,
 along with the reasoning behind the changes and how to update affected code.
@@ -11,13 +11,13 @@ Semantic Only Changes
 This section lists the changes that are semantic-only, thus potentially
 hiding new and different behavior in existing code.
 
- * When storage structs are deleted, every storage slot that contains a member of the struct is set to zero entirely. Formally, padding space was left untouched.
+- When storage structs are deleted, every storage slot that contains a member of the struct is set to zero entirely. Formally, padding space was left untouched.
-Consequently, if the padding space within a struct is used to store data (e.g. in the context of a contract upgrade), you have to be aware that ``delete`` will now also clear the added member (while it wouldn't have been cleared in the past).
+  Consequently, if the padding space within a struct is used to store data (e.g. in the context of a contract upgrade), you have to be aware that ``delete`` will now also clear the added member (while it wouldn't have been cleared in the past).
 
-.. code-block:: solidity
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.0;
+      pragma solidity >=0.7.1;
 
       contract C {
           struct S {
@@ -33,9 +33,9 @@ Consequently, if the padding space within a struct is used to store data (e.g. i
           }
       }
 
-We have the same behavior for implicit delete, for example when array of structs is shortened.
+  We have the same behavior for implicit delete, for example when array of structs is shortened.
 
- * Function modifiers are implemented in a slightly different way regarding function parameters.
+- Function modifiers are implemented in a slightly different way regarding function parameters.
   This especially has an effect if the placeholder ``_;`` is evaluated multiple times in a modifier.
   In the old code generator, each function parameter has a fixed slot on the stack. If the function
   is run multiple times because ``_;`` is used multiple times or used in a loop, then a change to the
@@ -43,7 +43,7 @@ We have the same behavior for implicit delete, for example when array of structs
   The new code generator implements modifiers using actual functions and passes function parameters on.
   This means that multiple executions of a function will get the same values for the parameters.
 
-.. code-block:: solidity
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
       pragma solidity >=0.7.0;
@@ -54,30 +54,33 @@ We have the same behavior for implicit delete, for example when array of structs
           modifier mod() { _; _; }
       }
 
-If you execute ``f(0)`` in the old code generator, it will return ``2``, while
+  If you execute ``f(0)`` in the old code generator, it will return ``2``, while
-it will return ``1`` when using the new code generator.
+  it will return ``1`` when using the new code generator.
 
- * The order of contract initialization has changed in case of inheritance.
+- The order of contract initialization has changed in case of inheritance.
+
+  The order used to be:
 
-The order used to be:
   - All state variables are zero-initialized at the beginning.
   - Evaluate base constructor arguments from most derived to most base contract.
   - Initialize all state variables in the whole inheritance hierarchy from most base to most derived.
   - Run the constructor, if present, for all contracts in the linearized hierarchy from most base to most derived.
 
-New order:
+  New order:
+
   - All state variables are zero-initialized at the beginning.
   - Evaluate base constructor arguments from most derived to most base contract.
   - For every contract in order from most base to most derived in the linearized hierarchy execute:
+
       1. If present at declaration, initial values are assigned to state variables.
       2. Constructor, if present.
 
 This causes differences in some contracts, for example:
 
-.. code-block:: solidity
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.0;
+      pragma solidity >=0.7.1;
 
       contract A {
           uint x;
@@ -92,16 +95,16 @@ This causes differences in some contracts, for example:
           uint public y = f();
       }
 
-Previously, ``y`` would be set to 0. This is due to the fact that we would first initialize state variables: First, ``x`` is set to 0, and when initializing ``y``, ``f()`` would return 0 causing ``y`` to be 0 as well.
+  Previously, ``y`` would be set to 0. This is due to the fact that we would first initialize state variables: First, ``x`` is set to 0, and when initializing ``y``, ``f()`` would return 0 causing ``y`` to be 0 as well.
-With the new rules, ``y`` will be set to 42. We first initialize ``x`` to 0, then call A's constructor which sets ``x`` to 42. Finally, when initializing ``y``, ``f()`` returns 42 causing ``y`` to be 42.
+  With the new rules, ``y`` will be set to 42. We first initialize ``x`` to 0, then call A's constructor which sets ``x`` to 42. Finally, when initializing ``y``, ``f()`` returns 42 causing ``y`` to be 42.
 
- * Copying ``bytes`` arrays from memory to storage is implemented in a different way. The old code generator always copies full words, while the new one cuts the byte array after its end. The old behaviour can lead to dirty data being copied after the end of the array (but still in the same storage slot).
+- Copying ``bytes`` arrays from memory to storage is implemented in a different way. The old code generator always copies full words, while the new one cuts the byte array after its end. The old behaviour can lead to dirty data being copied after the end of the array (but still in the same storage slot).
-This causes differences in some contracts, for example:
+  This causes differences in some contracts, for example:
 
-.. code-block:: solidity
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+      pragma solidity >=0.8.1;
 
       contract C {
           bytes x;
@@ -118,40 +121,41 @@ This causes differences in some contracts, for example:
           }
       }
 
-Previously ``f()`` would return ``0x6465616462656566313564656164000000000000000000000000000000000010`` (it has correct length, and correct first 8 elements, but then it contains dirty data which was set via assembly).
+  Previously ``f()`` would return ``0x6465616462656566313564656164000000000000000000000000000000000010`` (it has correct length, and correct first 8 elements, but then it contains dirty data which was set via assembly).
-Now it is returning ``0x6465616462656566000000000000000000000000000000000000000000000010`` (it has correct length, and correct elements, but does not contain superfluous data).
+  Now it is returning ``0x6465616462656566000000000000000000000000000000000000000000000010`` (it has correct length, and correct elements, but does not contain superfluous data).
 
-.. index:: ! evaluation order; expression
+  .. index:: ! evaluation order; expression
 
-* For the old code generator, the evaluation order of expressions is unspecified.
+- For the old code generator, the evaluation order of expressions is unspecified.
   For the new code generator, we try to evaluate in source order (left to right), but do not guarantee it.
   This can lead to semantic differences.
 
-For example:
+  For example:
 
-.. code-block:: solidity
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+      pragma solidity >=0.8.1;
       contract C {
           function preincr_u8(uint8 _a) public pure returns (uint8) {
               return ++_a + _a;
           }
       }
 
-The function ``preincr_u8(1)`` returns the following values:
+  The function ``preincr_u8(1)`` returns the following values:
-- Old code generator: 3 (``1 + 2``) but the return value is unspecified in general
-- New code generator: 4 (``2 + 2``) but the return value is not guaranteed
 
-.. index:: ! evaluation order; function arguments
+  - Old code generator: 3 (``1 + 2``) but the return value is unspecified in general
+  - New code generator: 4 (``2 + 2``) but the return value is not guaranteed
 
-On the other hand, function argument expressions are evaluated in the same order by both code generators with the exception of the global functions ``addmod`` and ``mulmod``.
+  .. index:: ! evaluation order; function arguments
-For example:
 
-.. code-block:: solidity
+  On the other hand, function argument expressions are evaluated in the same order by both code generators with the exception of the global functions ``addmod`` and ``mulmod``.
+  For example:
+
+  .. code-block:: solidity
 
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+      pragma solidity >=0.8.1;
       contract C {
           function add(uint8 _a, uint8 _b) public pure returns (uint8) {
               return _a + _b;
@@ -161,17 +165,19 @@ For example:
           }
       }
 
-The function ``g(1, 2)`` returns the following values:
+  The function ``g(1, 2)`` returns the following values:
-- Old code generator: ``10`` (``add(2 + 3, 2 + 3)``) but the return value is unspecified in general
-- New code generator: ``10`` but the return value is not guaranteed
 
-The arguments to the global functions ``addmod`` and ``mulmod`` are evaluated right-to-left by the old code generator
+  - Old code generator: ``10`` (``add(2 + 3, 2 + 3)``) but the return value is unspecified in general
-and left-to-right by the new code generator.
+  - New code generator: ``10`` but the return value is not guaranteed
-For example:
+
+  The arguments to the global functions ``addmod`` and ``mulmod`` are evaluated right-to-left by the old code generator
+  and left-to-right by the new code generator.
+  For example:
+
+  .. code-block:: solidity
 
-::
       // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+      pragma solidity >=0.8.1;
       contract C {
           function f() public pure returns (uint256 aMod, uint256 mMod) {
               uint256 x = 3;
@@ -182,9 +188,34 @@ For example:
           }
       }
 
-The function ``f()`` returns the following values:
+  The function ``f()`` returns the following values:
-- Old code generator: ``aMod = 0`` and ``mMod = 2``
+
-- New code generator: ``aMod = 4`` and ``mMod = 0``
+  - Old code generator: ``aMod = 0`` and ``mMod = 2``
+  - New code generator: ``aMod = 4`` and ``mMod = 0``
+
+- The new code generator imposes a hard limit of ``type(uint64).max`` (``0xffffffffffffffff``) for the free memory pointer. Allocations that would increase its value beyond this limit revert. The old code generator does not have this limit.
+
+  For example:
+
+  .. code-block:: solidity
+
+      // SPDX-License-Identifier: GPL-3.0
+      pragma solidity >0.8.0;
+      contract C {
+          function f() public {
+              uint[] memory arr;
+              // allocation size: 576460752303423481
+              // assumes freeMemPtr points to 0x80 initially
+              uint solYulMaxAllocationBeforeMemPtrOverflow = (type(uint64).max - 0x80 - 31) / 32;
+              // freeMemPtr overflows UINT64_MAX
+              arr = new uint[](solYulMaxAllocationBeforeMemPtrOverflow);
+          }
+      }
+
+  The function `f()` behaves as follows:
+
+  - Old code generator: runs out of gas while zeroing the array contents after the large memory allocation
+  - New code generator: reverts due to free memory pointer overflow (does not run out of gas)
 
 
 Internals
@@ -219,9 +250,10 @@ The new code generator performs cleanup after any operation that can result in d
 For example:
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.0;
+    pragma solidity >=0.8.1;
     contract C {
         function f(uint8 _a) public pure returns (uint _r1, uint _r2)
         {
@@ -234,6 +266,7 @@ For example:
     }
 
 The function ``f(1)`` returns the following values:
+
 - Old code generator: (``fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe``, ``00000000000000000000000000000000000000000000000000000000000000fe``)
 - New code generator: (``00000000000000000000000000000000000000000000000000000000000000fe``, ``00000000000000000000000000000000000000000000000000000000000000fe``)
 

docs/layout-of-source-files.rst

@@ -180,7 +180,7 @@ a `default export <https://developer.mozilla.org/en-US/docs/web/javascript/refer
 
 At a global level, you can use import statements of the following form:
 
-::
+.. code-block:: solidity
 
     import "filename";
 
@@ -195,7 +195,7 @@ symbols explicitly.
 The following example creates a new global symbol ``symbolName`` whose members are all
 the global symbols from ``"filename"``:
 
-::
+.. code-block:: solidity
 
     import * as symbolName from "filename";
 
@@ -203,7 +203,7 @@ which results in all global symbols being available in the format ``symbolName.s
 
 A variant of this syntax that is not part of ES6, but possibly useful is:
 
-::
+.. code-block:: solidity
 
   import "filename" as symbolName;
 
@@ -213,7 +213,7 @@ If there is a naming collision, you can rename symbols while importing. For exam
 the code below creates new global symbols ``alias`` and ``symbol2`` which reference
 ``symbol1`` and ``symbol2`` from inside ``"filename"``, respectively.
 
-::
+.. code-block:: solidity
 
     import {symbol1 as alias, symbol2} from "filename";
 
@@ -253,7 +253,7 @@ Comments
 
 Single-line comments (``//``) and multi-line comments (``/*...*/``) are possible.
 
-::
+.. code-block:: solidity
 
     // This is a single-line comment.
 

docs/metadata.rst

@@ -31,24 +31,24 @@ reduce whitespace to a minimum and sort the keys of all objects to arrive at a
 unique formatting. Comments are not permitted and used here only for
 explanatory purposes.
 
-.. code-block:: none
+.. code-block:: javascript
 
     {
       // Required: The version of the metadata format
-      version: "1",
+      "version": "1",
       // Required: Source code language, basically selects a "sub-version"
       // of the specification
-      language: "Solidity",
+      "language": "Solidity",
       // Required: Details about the compiler, contents are specific
       // to the language.
-      compiler: {
+      "compiler": {
         // Required for Solidity: Version of the compiler
-        version: "0.4.6+commit.2dabbdf0.Emscripten.clang",
+        "version": "0.4.6+commit.2dabbdf0.Emscripten.clang",
         // Optional: Hash of the compiler binary which produced this output
-        keccak256: "0x123..."
+        "keccak256": "0x123..."
       },
       // Required: Compilation source files/source units, keys are file names
-      sources:
+      "sources":
       {
         "myFile.sol": {
           // Required: keccak256 hash of the source file
@@ -68,59 +68,59 @@ explanatory purposes.
         }
       },
       // Required: Compiler settings
-      settings:
+      "settings":
       {
         // Required for Solidity: Sorted list of remappings
-        remappings: [ ":g=/dir" ],
+        "remappings": [ ":g=/dir" ],
         // Optional: Optimizer settings. The fields "enabled" and "runs" are deprecated
         // and are only given for backwards-compatibility.
-        optimizer: {
+        "optimizer": {
-          enabled: true,
+          "enabled": true,
-          runs: 500,
+          "runs": 500,
-          details: {
+          "details": {
             // peephole defaults to "true"
-            peephole: true,
+            "peephole": true,
             // inliner defaults to "true"
-            inliner: true,
+            "inliner": true,
             // jumpdestRemover defaults to "true"
-            jumpdestRemover: true,
+            "jumpdestRemover": true,
-            orderLiterals: false,
+            "orderLiterals": false,
-            deduplicate: false,
+            "deduplicate": false,
-            cse: false,
+            "cse": false,
-            constantOptimizer: false,
+            "constantOptimizer": false,
-            yul: true,
+            "yul": true,
             // Optional: Only present if "yul" is "true"
-            yulDetails: {
+            "yulDetails": {
-              stackAllocation: false,
+              "stackAllocation": false,
-              optimizerSteps: "dhfoDgvulfnTUtnIf..."
+              "optimizerSteps": "dhfoDgvulfnTUtnIf..."
             }
           }
         },
-        metadata: {
+        "metadata": {
           // Reflects the setting used in the input json, defaults to false
-          useLiteralContent: true,
+          "useLiteralContent": true,
           // Reflects the setting used in the input json, defaults to "ipfs"
-          bytecodeHash: "ipfs"
+          "bytecodeHash": "ipfs"
-        }
+        },
         // Required for Solidity: File and name of the contract or library this
         // metadata is created for.
-        compilationTarget: {
+        "compilationTarget": {
           "myFile.sol": "MyContract"
         },
         // Required for Solidity: Addresses for libraries used
-        libraries: {
+        "libraries": {
           "MyLib": "0x123123..."
         }
       },
       // Required: Generated information about the contract.
-      output:
+      "output":
       {
         // Required: ABI definition of the contract
-        abi: [ ... ],
+        "abi": [/* ... */],
         // Required: NatSpec user documentation of the contract
-        userdoc: [ ... ],
+        "userdoc": [/* ... */],
         // Required: NatSpec developer documentation of the contract
-        devdoc: [ ... ],
+        "devdoc": [/* ... */]
       }
     }
 
@@ -147,7 +147,9 @@ the mapping ``{"ipfs": <IPFS hash>, "solc": <compiler version>}`` is stored
 contain more keys (see below) and the beginning of that
 encoding is not easy to find, its length is added in a two-byte big-endian
 encoding. The current version of the Solidity compiler usually adds the following
-to the end of the deployed bytecode::
+to the end of the deployed bytecode
+
+.. code-block:: text
 
     0xa2
     0x64 'i' 'p' 'f' 's' 0x58 0x22 <34 bytes IPFS hash>

docs/natspec-format.rst

@@ -58,7 +58,7 @@ The following example shows a contract and a function using all available tags.
 
   This may change in the future.
 
-.. code:: Solidity
+.. code-block:: Solidity
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.8.2 < 0.9.0;
@@ -166,9 +166,9 @@ Inheritance Notes
 Functions without NatSpec will automatically inherit the documentation of their
 base function. Exceptions to this are:
 
- * When the parameter names are different.
+* When the parameter names are different.
- * When there is more than one base function.
+* When there is more than one base function.
- * When there is an explicit ``@inheritdoc`` tag which specifies which contract should be used to inherit.
+* When there is an explicit ``@inheritdoc`` tag which specifies which contract should be used to inherit.
 
 .. _header-output:
 

docs/path-resolution.rst

@@ -180,7 +180,7 @@ Direct Imports
 
 An import that does not start with ``./`` or ``../`` is a *direct import*.
 
-::
+.. code-block:: solidity
 
     import "/project/lib/util.sol";         // source unit name: /project/lib/util.sol
     import "lib/util.sol";                  // source unit name: lib/util.sol
@@ -464,7 +464,8 @@ Here are the detailed rules governing the behaviour of remappings:
 
 #. **Prefix cannot be empty but context and target are optional.**
 
-   If ``target`` is omitted, it defaults to the value of the ``prefix``.
+   - If ``target`` is the empty string, ``prefix`` is simply removed from import paths.
+   - Empty ``context`` means that the remapping applies to all imports in all source units.
 
 .. index:: Remix IDE, file://
 

docs/requirements.txt

@@ -1,4 +1,8 @@
-sphinx_rtd_theme>=0.3.1
+# Older versions of sphinx-rtd-theme do not work with never docutils but have a bug in the dependency
+# which could result in it being installed anyway and the style (especially bullet points) being broken.
+# See https://github.com/readthedocs/sphinx_rtd_theme/issues/1115
+sphinx_rtd_theme>=0.5.2
+
 pygments-lexer-solidity>=0.7.0
 sphinx-a4doc>=1.2.1
 

docs/security-considerations.rst

@@ -211,6 +211,7 @@ Never use tx.origin for authorization. Let's say you have a wallet contract like
         }
 
         function transferTo(address payable dest, uint amount) public {
+            // THE BUG IS RIGHT HERE, you must use msg.sender instead of tx.origin
             require(tx.origin == owner);
             dest.transfer(amount);
         }

docs/smtchecker.rst

@@ -15,7 +15,7 @@ difference between what you did (the specification) and how you did it
 is what you wanted and that you did not miss any unintended effects of it.
 
 Solidity implements a formal verification approach based on
-`SMT <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>`_ and
+`SMT (Satisfiability Modulo Theories) <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>`_ and
 `Horn <https://en.wikipedia.org/wiki/Horn-satisfiability>`_ solving.
 The SMTChecker module automatically tries to prove that the code satisfies the
 specification given by ``require`` and ``assert`` statements. That is, it considers
@@ -52,6 +52,7 @@ where the default is no engine. Selecting the engine enables the SMTChecker on a
     enables the SMTChecker for all files.
 
 .. note::
+
     The lack of warnings for a verification target represents an undisputed
     mathematical proof of correctness, assuming no bugs in the SMTChecker and
     the underlying solver. Keep in mind that these problems are
@@ -96,7 +97,7 @@ The SMTChecker will, by default, check every reachable arithmetic operation
 in the contract for potential underflow and overflow.
 Here, it reports the following:
 
-.. code-block:: bash
+.. code-block:: text
 
     Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
     Counterexample:
@@ -202,6 +203,7 @@ Note that in this example the SMTChecker will automatically try to prove three p
 3. The assertion is always true.
 
 .. note::
+
     The properties involve loops, which makes it *much much* harder than the previous
     examples, so beware of loops!
 
@@ -231,7 +233,7 @@ For example, changing the code to
 
 gives us:
 
-.. code-block:: bash
+.. code-block:: text
 
     Warning: CHC: Assertion violation happens here.
     Counterexample:
@@ -321,7 +323,7 @@ reachable, by adding the following function.
 This property is false, and while proving that the property is false,
 the SMTChecker tells us exactly *how* to reach (2, 4):
 
-.. code-block:: bash
+.. code-block:: text
 
     Warning: CHC: Assertion violation happens here.
     Counterexample:
@@ -408,7 +410,7 @@ If we "forget" to use the ``mutex`` modifier on function ``set``, the
 SMTChecker is able to synthesize the behavior of the externally called code so
 that the assertion fails:
 
-.. code-block:: bash
+.. code-block:: text
 
     Warning: CHC: Assertion violation happens here.
     Counterexample:
@@ -472,6 +474,14 @@ A common subset of targets might be, for example:
 There is no precise heuristic on how and when to split verification targets,
 but it can be useful especially when dealing with large contracts.
 
+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
+the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
+
 Verified Contracts
 ==================
 
@@ -492,15 +502,13 @@ allowed) of <source>:<contract> pairs in the CLI:
 and via the object ``settings.modelChecker.contracts`` in the :ref:`JSON input<compiler-api>`,
 which has the following form:
 
-.. code-block:: none
+.. code-block:: json
 
-  contracts
+    "contracts": {
-  {
         "source1.sol": ["contract1"],
         "source2.sol": ["contract2", "contract3"]
     }
 
-
 .. _smtchecker_engines:
 
 Natspec Function Abstraction
@@ -557,6 +565,39 @@ calls assume the called code is unknown and can do anything.
 The CHC engine is much more powerful than BMC in terms of what it can prove,
 and might require more computing resources.
 
+SMT and Horn solvers
+====================
+
+The two engines detailed above use automated theorem provers as their logical
+backends.  BMC uses an SMT solver, whereas CHC uses a Horn solver. Often the
+same tool can act as both, as seen in `z3 <https://github.com/Z3Prover/z3>`_,
+which is primarily an SMT solver and makes `Spacer
+<https://spacer.bitbucket.io/>`_ available as a Horn solver, and `Eldarica
+<https://github.com/uuverifiers/eldarica>`_ which does both.
+
+The user can choose which solvers should be used, if available, via the CLI
+option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
+``settings.modelChecker.solvers=[smtlib2,z3]``, where:
+
+- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
+- ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
+  These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
+  any solver binary from the system can be employed to synchronously return the results of the queries to the compiler.
+  This is currently the only way to use Eldarica, for example, since it does not have a C++ API.
+  This can be used by both BMC and CHC depending on which solvers are called.
+- ``z3`` is available
+
+  - if ``solc`` is compiled with it;
+  - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6);
+  - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.
+
+Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety
+of environments, including in the browser, most users will almost never need to be
+concerned about this option. More advanced users might apply this option to try
+alternative solvers on more complex problems.
+
+Please note that certain combinations of chosen engine and solver will lead to
+the SMTChecker doing nothing, for example choosing CHC and ``cvc4``.
 
 *******************************
 Abstraction and False Positives

docs/structure-of-a-contract.rst

@@ -50,7 +50,7 @@ contracts.
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.7.0 <0.9.0;
+    pragma solidity >=0.7.1 <0.9.0;
 
     contract SimpleAuction {
         function bid() public payable { // Function

docs/style-guide.rst

@@ -410,7 +410,9 @@ No:
 
     spam( ham[ 1 ], Coin( { name: "ham" } ) );
 
-Exception::
+Exception:
+
+.. code-block:: solidity
 
     function singleLine() public { spam(); }
 
@@ -996,6 +998,7 @@ No:
 Yes:
 
 .. code-block:: solidity
+    :force:
 
     x = 3;
     x = 100 / 10;
@@ -1005,6 +1008,7 @@ Yes:
 No:
 
 .. code-block:: solidity
+    :force:
 
     x=3;
     x = 100/10;

docs/types/mapping-types.rst

@@ -122,6 +122,7 @@ top of them and iterate over that. For example, the code below implements an
 the ``sum`` function iterates over to sum all the values.
 
 .. code-block:: solidity
+    :force:
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.6.8 <0.9.0;

docs/types/reference-types.rst

@@ -27,13 +27,6 @@ Every reference type has an additional
 annotation, the "data location", about where it is stored. There are three data locations:
 ``memory``, ``storage`` and ``calldata``. Calldata is a non-modifiable,
 non-persistent area where function arguments are stored, and behaves mostly like memory.
-It is required for parameters of external functions but can also be used for other variables.
-
-
-.. note::
-    Prior to version 0.5.0 the data location could be omitted, and would default to different locations
-    depending on the kind of variable, function type, etc., but all complex types must now give an explicit
-    data location.
 
 .. note::
     If you can, try to use ``calldata`` as data location because it will avoid copies and
@@ -41,6 +34,17 @@ It is required for parameters of external functions but can also be used for oth
     data location can also be returned from functions, but it is not possible to
     allocate such types.
 
+.. note::
+    Prior to version 0.6.9 data location for reference-type arguments was limited to
+    ``calldata`` in external functions, ``memory`` in public functions and either
+    ``memory`` or ``storage`` in internal and private ones.
+    Now ``memory`` and ``calldata`` are allowed in all functions regardless of their visibility.
+
+.. note::
+    Prior to version 0.5.0 the data location could be omitted, and would default to different locations
+    depending on the kind of variable, function type, etc., but all complex types must now give an explicit
+    data location.
+
 .. _data-location-assignment:
 
 Data location and assignment behaviour
@@ -139,7 +143,7 @@ a reference to it.
 ``bytes`` and ``string`` as Arrays
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-Variables of type ``bytes`` and ``string`` are special arrays. A ``bytes`` is similar to ``byte[]``,
+Variables of type ``bytes`` and ``string`` are special arrays. The ``bytes`` type is similar to ``bytes1[]``,
 but it is packed tightly in calldata and memory. ``string`` is equal to ``bytes`` but does not allow
 length or index access.
 
@@ -148,8 +152,8 @@ third-party string libraries. You can also compare two strings by their keccak25
 ``keccak256(abi.encodePacked(s1)) == keccak256(abi.encodePacked(s2))`` and
 concatenate two strings using ``bytes.concat(bytes(s1), bytes(s2))``.
 
-You should use ``bytes`` over ``byte[]`` because it is cheaper,
+You should use ``bytes`` over ``bytes1[]`` because it is cheaper,
-since ``byte[]`` adds 31 padding bytes between the elements. As a general rule,
+since ``bytes1[]`` adds 31 padding bytes between the elements. As a general rule,
 use ``bytes`` for arbitrary-length raw byte data and ``string`` for arbitrary-length
 string (UTF-8) data. If you can limit the length to a certain number of bytes,
 always use one of the value types ``bytes1`` to ``bytes32`` because they are much cheaper.
@@ -492,7 +496,7 @@ Array slices are useful to ABI-decode secondary data passed in function paramete
 .. code-block:: solidity
 
     // SPDX-License-Identifier: GPL-3.0
-    pragma solidity >0.8.4 <0.9.0;
+    pragma solidity >=0.8.5 <0.9.0;
     contract Proxy {
         /// @dev Address of the client contract managed by proxy i.e., this contract
         address client;
@@ -559,7 +563,7 @@ shown in the following example:
         function newCampaign(address payable beneficiary, uint goal) public returns (uint campaignID) {
             campaignID = numCampaigns++; // campaignID is return variable
             // We cannot use "campaigns[campaignID] = Campaign(beneficiary, goal, 0, 0)"
-            // because the RHS creates a memory-struct "Campaign" that contains a mapping.
+            // because the right hand side creates a memory-struct "Campaign" that contains a mapping.
             Campaign storage c = campaigns[campaignID];
             c.beneficiary = beneficiary;
             c.fundingGoal = goal;

docs/types/value-types.rst

@@ -128,10 +128,10 @@ The modulo operation ``a % n`` yields the remainder ``r`` after the division of
 by the operand ``n``, where ``q = int(a / n)`` and ``r = a - (n * q)``. This means that modulo
 results in the same sign as its left operand (or zero) and ``a % n == -(-a % n)`` holds for negative ``a``:
 
- * ``int256(5) % int256(2) == int256(1)``
+* ``int256(5) % int256(2) == int256(1)``
- * ``int256(5) % int256(-2) == int256(1)``
+* ``int256(5) % int256(-2) == int256(1)``
- * ``int256(-5) % int256(2) == int256(-1)``
+* ``int256(-5) % int256(2) == int256(-1)``
- * ``int256(-5) % int256(-2) == int256(-1)``
+* ``int256(-5) % int256(-2) == int256(-1)``
 
 .. note::
   Modulo with zero causes a :ref:`Panic error<assert-and-require>`. This check can **not** be disabled through ``unchecked { ... }``.
@@ -184,8 +184,8 @@ Address
 
 The address type comes in two flavours, which are largely identical:
 
- - ``address``: Holds a 20 byte value (size of an Ethereum address).
+- ``address``: Holds a 20 byte value (size of an Ethereum address).
- - ``address payable``: Same as ``address``, but with the additional members ``transfer`` and ``send``.
+- ``address payable``: Same as ``address``, but with the additional members ``transfer`` and ``send``.
 
 The idea behind this distinction is that ``address payable`` is an address you can send Ether to,
 while a plain ``address`` cannot be sent Ether.
@@ -239,6 +239,7 @@ It is possible to query the balance of an address using the property ``balance``
 and to send Ether (in units of wei) to a payable address using the ``transfer`` function:
 
 .. code-block:: solidity
+    :force:
 
     address payable x = address(0x123);
     address myAddress = address(this);
@@ -398,7 +399,7 @@ Members:
 * ``.length`` yields the fixed length of the byte array (read-only).
 
 .. note::
-    The type ``byte[]`` is an array of bytes, but due to padding rules, it wastes
+    The type ``bytes1[]`` is an array of bytes, but due to padding rules, it wastes
     31 bytes of space for each element (except in storage). It is better to use the ``bytes``
     type instead.
 
@@ -510,27 +511,32 @@ String literals can only contain printable ASCII characters, which means the cha
 
 Additionally, string literals also support the following escape characters:
 
- - ``\<newline>`` (escapes an actual newline)
+- ``\<newline>`` (escapes an actual newline)
- - ``\\`` (backslash)
+- ``\\`` (backslash)
- - ``\'`` (single quote)
+- ``\'`` (single quote)
- - ``\"`` (double quote)
+- ``\"`` (double quote)
- - ``\b`` (backspace)
+- ``\n`` (newline)
- - ``\f`` (form feed)
+- ``\r`` (carriage return)
- - ``\n`` (newline)
+- ``\t`` (tab)
- - ``\r`` (carriage return)
+- ``\xNN`` (hex escape, see below)
- - ``\t`` (tab)
+- ``\uNNNN`` (unicode escape, see below)
- - ``\v`` (vertical tab)
- - ``\xNN`` (hex escape, see below)
- - ``\uNNNN`` (unicode escape, see below)
 
 ``\xNN`` takes a hex value and inserts the appropriate byte, while ``\uNNNN`` takes a Unicode codepoint and inserts an UTF-8 sequence.
 
+.. note::
+
+    Until version 0.8.0 there were three additional escape sequences: ``\b``, ``\f`` and ``\v``.
+    They are commonly available in other languages but rarely needed in practice.
+    If you do need them, they can still be inserted via hexadecimal escapes, i.e. ``\x08``, ``\x0c``
+    and ``\x0b``, respectively, just as any other ASCII character.
+
 The string in the following example has a length of ten bytes.
 It starts with a newline byte, followed by a double quote, a single
 quote a backslash character and then (without separator) the
 character sequence ``abcdef``.
 
-::
+.. code-block:: solidity
+    :force:
 
     "\n\"\'\\abc\
     def"
@@ -637,6 +643,7 @@ be passed via and returned from external function calls.
 Function types are notated as follows:
 
 .. code-block:: solidity
+    :force:
 
     function (<parameter types>) {internal|external} [pure|view|payable] [returns (<return types>)]
 
@@ -656,9 +663,9 @@ their parameter types are identical, their return types are identical,
 their internal/external property is identical and the state mutability of ``A``
 is more restrictive than the state mutability of ``B``. In particular:
 
- - ``pure`` functions can be converted to ``view`` and ``non-payable`` functions
+- ``pure`` functions can be converted to ``view`` and ``non-payable`` functions
- - ``view`` functions can be converted to ``non-payable`` functions
+- ``view`` functions can be converted to ``non-payable`` functions
- - ``payable`` functions can be converted to ``non-payable`` functions
+- ``payable`` functions can be converted to ``non-payable`` functions
 
 No other conversions between function types are possible.
 

docs/units-and-global-variables.rst

@@ -10,6 +10,7 @@ Ether Units
 A literal number can take a suffix of ``wei``, ``gwei`` or ``ether`` to specify a subdenomination of Ether, where Ether numbers without a postfix are assumed to be Wei.
 
 .. code-block:: solidity
+    :force:
 
     assert(1 wei == 1);
     assert(1 gwei == 1e9);
@@ -29,11 +30,11 @@ Suffixes like ``seconds``, ``minutes``, ``hours``, ``days`` and ``weeks``
 after literal numbers can be used to specify units of time where seconds are the base
 unit and units are considered naively in the following way:
 
- * ``1 == 1 seconds``
+* ``1 == 1 seconds``
- * ``1 minutes == 60 seconds``
+* ``1 minutes == 60 seconds``
- * ``1 hours == 60 minutes``
+* ``1 hours == 60 minutes``
- * ``1 days == 24 hours``
+* ``1 days == 24 hours``
- * ``1 weeks == 7 days``
+* ``1 weeks == 7 days``
 
 Take care if you perform calendar calculations using these units, because
 not every year equals 365 days and not even every day has 24 hours

docs/using-the-compiler.rst

@@ -30,8 +30,8 @@ set it to ``--optimize-runs=1``. If you expect many transactions and do not care
 output size, set ``--optimize-runs`` to a high number.
 This parameter has effects on the following (this might change in the future):
 
- - the size of the binary search in the function dispatch routine
+- the size of the binary search in the function dispatch routine
- - the way constants like large numbers or strings are stored
+- the way constants like large numbers or strings are stored
 
 .. index:: allowed paths, --allow-paths, base path, --base-path
 
@@ -41,7 +41,7 @@ Base Path and Import Remapping
 The commandline compiler will automatically read imported files from the filesystem, but
 it is also possible to provide :ref:`path redirects <import-remapping>` using ``prefix=path`` in the following way:
 
-::
+.. code-block:: bash
 
     solc github.com/ethereum/dapp-bin/=/usr/local/lib/dapp-bin/ file.sol
 
@@ -134,12 +134,12 @@ On the command line, you can select the EVM version as follows:
 In the :ref:`standard JSON interface <compiler-api>`, use the ``"evmVersion"``
 key in the ``"settings"`` field:
 
-.. code-block:: none
+.. code-block:: javascript
 
     {
-    "sources": { ... },
+      "sources": {/* ... */},
       "settings": {
-      "optimizer": { ... },
+        "optimizer": {/* ... */},
         "evmVersion": "<VERSION>"
       }
     }
@@ -198,7 +198,7 @@ Comments are of course not permitted and used here only for explanatory purposes
 Input Description
 -----------------
 
-.. code-block:: none
+.. code-block:: javascript
 
     {
       // Required: Source code language. Currently supported are "Solidity" and "Yul".
@@ -310,7 +310,7 @@ Input Description
           // "debug" injects strings for compiler-generated internal reverts, implemented for ABI encoders V1 and V2 for now.
           // "verboseDebug" even appends further information to user-supplied revert strings (not yet implemented)
           "revertStrings": "default"
-        }
+        },
         // Metadata settings (optional)
         "metadata": {
           // Use only literal content and not URLs (false by default)
@@ -331,7 +331,7 @@ Input Description
           "myFile.sol": {
             "MyLib": "0x123123..."
           }
-        }
+        },
         // The following can be used to select desired outputs based
         // on file and contract names.
         // If this field is omitted, then the compiler loads and does type checking,
@@ -395,13 +395,15 @@ Input Description
         "modelChecker":
         {
           // Chose which contracts should be analyzed as the deployed one.
-          contracts:
+          "contracts":
           {
             "source1.sol": ["contract1"],
             "source2.sol": ["contract2", "contract3"]
           },
           // 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 targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
           // If the option is not given all targets are checked by default.
@@ -420,7 +422,7 @@ Input Description
 Output Description
 ------------------
 
-.. code-block:: none
+.. code-block:: javascript
 
     {
       // Optional: not present if no errors/warnings were encountered
@@ -431,7 +433,7 @@ Output Description
             "file": "sourceFile.sol",
             "start": 0,
             "end": 100
-          ],
+          },
           // Optional: Further locations (e.g. places of conflicting declarations)
           "secondarySourceLocations": [
             {
@@ -463,7 +465,7 @@ Output Description
           // Identifier of the source (used in source maps)
           "id": 1,
           // The AST object
-          "ast": {},
+          "ast": {}
         }
       },
       // This contains the contract-level outputs.
@@ -476,7 +478,7 @@ Output Description
             // See https://docs.soliditylang.org/en/develop/abi-spec.html
             "abi": [],
             // See the Metadata Output documentation (serialised JSON string)
-            "metadata": "{...}",
+            "metadata": "{/* ... */}",
             // User documentation (natspec)
             "userdoc": {},
             // Developer documentation (natspec)
@@ -484,7 +486,7 @@ Output Description
             // Intermediate representation (string)
             "ir": "",
             // See the Storage Layout documentation.
-            "storageLayout": {"storage": [...], "types": {...} },
+            "storageLayout": {"storage": [/* ... */], "types": {/* ... */} },
             // EVM-related outputs
             "evm": {
               // Assembly (string)
@@ -514,14 +516,14 @@ Output Description
                 // contains a single Yul file.
                 "generatedSources": [{
                   // Yul AST
-                  "ast": { ... }
+                  "ast": {/* ... */},
                   // Source file in its text form (may contain comments)
                   "contents":"{ function abi_decode(start, end) -> data { data := calldataload(start) } }",
                   // Source file ID, used for source references, same "namespace" as the Solidity source files
                   "id": 2,
                   "language": "Yul",
                   "name": "#utility.yul"
-                }]
+                }],
                 // If given, this is an unlinked object.
                 "linkReferences": {
                   "libraryFile.sol": {
@@ -535,7 +537,7 @@ Output Description
                 }
               },
               "deployedBytecode": {
-                ..., // The same layout as above.
+                /* ..., */ // The same layout as above.
                 "immutableReferences": {
                   // There are two references to the immutable with AST ID 3, both 32 bytes long. One is
                   // at bytecode offset 42, the other at bytecode offset 80.
@@ -779,9 +781,9 @@ Running the Upgrade
 
 It is recommended to explicitly specify the upgrade modules by using ``--modules`` argument.
 
-.. code-block:: none
+.. code-block:: bash
 
-   $ solidity-upgrade --modules constructor-visibility,now,dotsyntax Source.sol
+    solidity-upgrade --modules constructor-visibility,now,dotsyntax Source.sol
 
 The command above applies all changes as shown below. Please review them carefully (the pragmas will
 have to be updated manually.)

docs/yul.rst

@@ -157,16 +157,16 @@ where an object is expected.
 Inside a code block, the following elements can be used
 (see the later sections for more details):
 
- - literals, i.e. ``0x123``, ``42`` or ``"abc"`` (strings up to 32 characters)
+- literals, i.e. ``0x123``, ``42`` or ``"abc"`` (strings up to 32 characters)
- - calls to builtin functions, e.g. ``add(1, mload(0))``
+- calls to builtin functions, e.g. ``add(1, mload(0))``
- - variable declarations, e.g. ``let x := 7``, ``let x := add(y, 3)`` or ``let x`` (initial value of 0 is assigned)
+- variable declarations, e.g. ``let x := 7``, ``let x := add(y, 3)`` or ``let x`` (initial value of 0 is assigned)
- - identifiers (variables), e.g. ``add(3, x)``
+- identifiers (variables), e.g. ``add(3, x)``
- - assignments, e.g. ``x := add(y, 3)``
+- assignments, e.g. ``x := add(y, 3)``
- - blocks where local variables are scoped inside, e.g. ``{ let x := 3 { let y := add(x, 1) } }``
+- blocks where local variables are scoped inside, e.g. ``{ let x := 3 { let y := add(x, 1) } }``
- - if statements, e.g. ``if lt(a, b) { sstore(0, 1) }``
+- if statements, e.g. ``if lt(a, b) { sstore(0, 1) }``
- - switch statements, e.g. ``switch mload(0) case 0 { revert() } default { mstore(0, 1) }``
+- switch statements, e.g. ``switch mload(0) case 0 { revert() } default { mstore(0, 1) }``
- - for loops, e.g. ``for { let i := 0} lt(i, 10) { i := add(i, 1) } { mstore(i, 7) }``
+- for loops, e.g. ``for { let i := 0} lt(i, 10) { i := add(i, 1) } { mstore(i, 7) }``
- - function definitions, e.g. ``function f(a, b) -> c { c := add(a, b) }```
+- function definitions, e.g. ``function f(a, b) -> c { c := add(a, b) }```
 
 Multiple syntactical elements can follow each other simply separated by
 whitespace, i.e. there is no terminating ``;`` or newline required.
@@ -198,7 +198,8 @@ has to be specified after a colon:
 
 .. code-block:: yul
 
-    let x := and("abc":uint32, add(3:uint256, 2:uint256))
+    // This will not compile (u32 and u256 type not implemented yet)
+    let x := and("abc":u32, add(3:u256, 2:u256))
 
 
 Function Calls
@@ -212,10 +213,9 @@ they have to be assigned to local variables.
 
 .. code-block:: yul
 
+    function f(x, y) -> a, b { /* ... */ }
     mstore(0x80, add(mload(0x80), 3))
-    // Here, the user-defined function `f` returns
+    // Here, the user-defined function `f` returns two values.
-    // two values. The definition of the function
-    // is missing from the example.
     let x, y := f(1, mload(0))
 
 For built-in functions of the EVM, functional expressions
@@ -271,9 +271,10 @@ that returns multiple values.
 
 .. code-block:: yul
 
+    // This will not compile (u32 and u256 type not implemented yet)
     {
-        let zero:uint32 := 0:uint32
+        let zero:u32 := 0:u32
-        let v:uint256, t:uint32 := f()
+        let v:u256, t:u32 := f()
         let x, y := g()
     }
 
@@ -314,7 +315,7 @@ you need multiple alternatives.
 
 .. code-block:: yul
 
-    if eq(value, 0) { revert(0, 0) }
+    if lt(calldatasize(), 4) { revert(0, 0) }
 
 The curly braces for the body are required.
 
@@ -545,11 +546,18 @@ as explained below) and all declarations
 introduce new identifiers into these scopes.
 
 Identifiers are visible in
-the block they are defined in (including all sub-nodes and sub-blocks).
+the block they are defined in (including all sub-nodes and sub-blocks):
+Functions are visible in the whole block (even before their definitions) while
+variables are only visible starting from the statement after the ``VariableDeclaration``.
 
-As an exception, the scope of the "init" part of the or-loop
+In particular,
+variables cannot be referenced in the right hand side of their own variable
+declaration.
+Functions can be referenced already before their declaration (if they are visible).
+
+As an exception to the general scoping rule, the scope of the "init" part of the for-loop
 (the first block) extends across all other parts of the for loop.
-This means that variables declared in the init part (but not inside a
+This means that variables (and functions) declared in the init part (but not inside a
 block inside the init part) are visible in all other parts of the for-loop.
 
 Identifiers declared in the other parts of the for loop respect the regular
@@ -558,21 +566,15 @@ syntactical scoping rules.
 This means a for-loop of the form ``for { I... } C { P... } { B... }`` is equivalent
 to ``{ I... for {} C { P... } { B... } }``.
 
-
 The parameters and return parameters of functions are visible in the
 function body and their names have to be distinct.
 
-Variables can only be referenced after their declaration. In particular,
+Inside functions, it is not possible to reference a variable that was declared
-variables cannot be referenced in the right hand side of their own variable
+outside of that function.
-declaration.
-Functions can be referenced already before their declaration (if they are visible).
 
 Shadowing is disallowed, i.e. you cannot declare an identifier at a point
 where another identifier with the same name is also visible, even if it is
-not accessible.
+not possible to reference it because it was declared outside the current function.
-
-Inside functions, it is not possible to access a variable that was declared
-outside of that function.
 
 Formal Specification
 --------------------
@@ -984,9 +986,10 @@ that are not known to the Yul compiler. It also allows you to create
 bytecode sequences that will not be modified by the optimizer.
 
 The functions are ``verbatim_<n>i_<m>o("<data>", ...)``, where
- - ``n`` is a decimal between 0 and 99 that specifies the number of input stack slots / variables
+
- - ``m`` is a decimal between 0 and 99 that specifies the number of output stack slots / variables
+- ``n`` is a decimal between 0 and 99 that specifies the number of input stack slots / variables
- - ``data`` is a string literal that contains the sequence of bytes
+- ``m`` is a decimal between 0 and 99 that specifies the number of output stack slots / variables
+- ``data`` is a string literal that contains the sequence of bytes
 
 If you for example want to define a function that multiplies the input
 by two, without the optimizer touching the constant two, you can use
@@ -1021,13 +1024,13 @@ verbatim bytecode that are not checked by
 the compiler. Violations of these restrictions can result in
 undefined behaviour.
 
- - Control-flow should not jump into or out of verbatim blocks,
+- Control-flow should not jump into or out of verbatim blocks,
   but it can jump within the same verbatim block.
- - Stack contents apart from the input and output parameters
+- Stack contents apart from the input and output parameters
   should not be accessed.
- - The stack height difference should be exactly ``m - n``
+- The stack height difference should be exactly ``m - n``
   (output slots minus input slots).
- - Verbatim bytecode cannot make any assumptions about the
+- Verbatim bytecode cannot make any assumptions about the
   surrounding bytecode. All required parameters have to be
   passed in as stack variables.
 
@@ -1175,11 +1178,13 @@ intermediate states. This allows for easy debugging and verification of the opti
 Please refer to the general :ref:`optimizer documentation <optimizer>`
 for more details about the different optimization stages and how to use the optimizer.
 
-If you want to use Solidity in stand-alone Yul mode, you activate the optimizer using ``--optimize``:
+If you want to use Solidity in stand-alone Yul mode, you activate the optimizer using ``--optimize``
+and optionally specify the :ref:`expected number of contract executions <optimizer-parameter-runs>` with
+``--optimize-runs``:
 
 .. code-block:: sh
 
-    solc --strict-assembly --optimize
+    solc --strict-assembly --optimize --optimize-runs 200
 
 In Solidity mode, the Yul optimizer is activated together with the regular optimizer.
 

libevmasm/Assembly.cpp

@@ -76,15 +76,15 @@ namespace
 string locationFromSources(StringMap const& _sourceCodes, SourceLocation const& _location)
 {
 	if (!_location.hasText() || _sourceCodes.empty())
-		return "";
+		return {};
 
-	auto it = _sourceCodes.find(_location.source->name());
+	auto it = _sourceCodes.find(*_location.sourceName);
 	if (it == _sourceCodes.end())
-		return "";
+		return {};
 
 	string const& source = it->second;
 	if (static_cast<size_t>(_location.start) >= source.size())
-		return "";
+		return {};
 
 	string cut = source.substr(static_cast<size_t>(_location.start), static_cast<size_t>(_location.end - _location.start));
 	auto newLinePos = cut.find_first_of("\n");
@@ -152,8 +152,8 @@ public:
 		if (!m_location.isValid())
 			return;
 		m_out << m_prefix << "    /*";
-		if (m_location.source)
+		if (m_location.sourceName)
-			m_out << " \"" + m_location.source->name() + "\"";
+			m_out << " " + escapeAndQuoteString(*m_location.sourceName);
 		if (m_location.hasText())
 			m_out << ":" << to_string(m_location.start) + ":" + to_string(m_location.end);
 		m_out << "  " << locationFromSources(m_sourceCodes, m_location);
@@ -235,9 +235,9 @@ Json::Value Assembly::assemblyJSON(map<string, unsigned> const& _sourceIndices)
 	for (AssemblyItem const& i: m_items)
 	{
 		int sourceIndex = -1;
-		if (i.location().source)
+		if (i.location().sourceName)
 		{
-			auto iter = _sourceIndices.find(i.location().source->name());
+			auto iter = _sourceIndices.find(*i.location().sourceName);
 			if (iter != _sourceIndices.end())
 				sourceIndex = static_cast<int>(iter->second);
 		}

libevmasm/AssemblyItem.cpp

@@ -350,8 +350,8 @@ std::string AssemblyItem::computeSourceMapping(
 		SourceLocation const& location = item.location();
 		int length = location.start != -1 && location.end != -1 ? location.end - location.start : -1;
 		int sourceIndex =
-			location.source && _sourceIndicesMap.count(location.source->name()) ?
+			(location.sourceName && _sourceIndicesMap.count(*location.sourceName)) ?
-			static_cast<int>(_sourceIndicesMap.at(location.source->name())) :
+			static_cast<int>(_sourceIndicesMap.at(*location.sourceName)) :
 			-1;
 		char jump = '-';
 		if (item.getJumpType() == evmasm::AssemblyItem::JumpType::IntoFunction)

liblangutil/CMakeLists.txt

@@ -13,6 +13,7 @@ set(sources
 	ParserBase.h
 	Scanner.cpp
 	Scanner.h
+	CharStreamProvider.h
 	SemVerHandler.cpp
 	SemVerHandler.h
 	SourceLocation.h

liblangutil/CharStream.cpp

@@ -45,9 +45,7 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
 /**
- * @author Christian <c@ethdev.com>
+ * Character stream / input file.
- * @date 2014
- * Solidity scanner.
  */
 
 #include <liblangutil/CharStream.h>
@@ -118,3 +116,15 @@ tuple<int, int> CharStream::translatePositionToLineColumn(int _position) const
 	}
 	return tuple<int, int>(lineNumber, searchPosition - lineStart);
 }
+
+string_view CharStream::text(SourceLocation const& _location) const
+{
+	if (!_location.hasText())
+		return {};
+	solAssert(_location.sourceName && *_location.sourceName == m_name, "");
+	solAssert(static_cast<size_t>(_location.end) <= m_source.size(), "");
+	return string_view{m_source}.substr(
+		static_cast<size_t>(_location.start),
+		static_cast<size_t>(_location.end - _location.start)
+	);
+}

liblangutil/CharStream.h

@@ -45,9 +45,7 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
 /**
- * @author Christian <c@ethdev.com>
+ * Character stream / input file.
- * @date 2014
- * Solidity scanner.
  */
 
 #pragma once
@@ -60,6 +58,8 @@
 namespace solidity::langutil
 {
 
+struct SourceLocation;
+
 /**
  * Bidirectional stream of characters.
  *
@@ -69,8 +69,8 @@ class CharStream
 {
 public:
 	CharStream() = default;
-	explicit CharStream(std::string  _source, std::string  name):
+	CharStream(std::string _source, std::string _name):
-		m_source(std::move(_source)), m_name(std::move(name)) {}
+		m_source(std::move(_source)), m_name(std::move(_name)) {}
 
 	size_t position() const { return m_position; }
 	bool isPastEndOfInput(size_t _charsForward = 0) const { return (m_position + _charsForward) >= m_source.size(); }
@@ -90,6 +90,8 @@ public:
 	std::string const& source() const noexcept { return m_source; }
 	std::string const& name() const noexcept { return m_name; }
 
+	size_t size() const { return m_source.size(); }
+
 	///@{
 	///@name Error printing helper functions
 	/// Functions that help pretty-printing parse errors
@@ -112,6 +114,10 @@ public:
 		return true;
 	}
 
+	/// @returns the substring of the source that the source location references.
+	/// Returns an empty string view if the source location does not `hasText()`.
+	std::string_view text(SourceLocation const& _location) const;
+
 private:
 	std::string m_source;
 	std::string m_name;

liblangutil/CharStreamProvider.h

@@ -0,0 +1,57 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+/**
+ * Interface to retrieve the character stream by a source name.
+ */
+
+#pragma once
+
+#include <liblangutil/CharStream.h>
+#include <liblangutil/Exceptions.h>
+
+#include <string>
+
+namespace solidity::langutil
+{
+
+/**
+ * Interface to retrieve a CharStream (source) from a source name.
+ * Used especially for printing error information.
+ */
+class CharStreamProvider
+{
+public:
+	virtual ~CharStreamProvider() = default;
+	virtual CharStream const& charStream(std::string const& _sourceName) const = 0;
+};
+
+class SingletonCharStreamProvider: public CharStreamProvider
+{
+public:
+	explicit SingletonCharStreamProvider(CharStream const& _charStream):
+		m_charStream(_charStream) {}
+	CharStream const& charStream(std::string const& _sourceName) const override
+	{
+		solAssert(m_charStream.name() == _sourceName, "");
+		return m_charStream;
+	}
+private:
+	CharStream const& m_charStream;
+};
+
+}

liblangutil/ParserBase.h

@@ -24,7 +24,6 @@
 #pragma once
 
 #include <liblangutil/Token.h>
-#include <liblangutil/Scanner.h>
 #include <memory>
 #include <string>
 
@@ -33,6 +32,7 @@ namespace solidity::langutil
 
 class ErrorReporter;
 class Scanner;
+struct SourceLocation;
 struct ErrorId;
 
 class ParserBase
@@ -47,7 +47,7 @@ public:
 		m_parserErrorRecovery = _parserErrorRecovery;
 	}
 
-	std::shared_ptr<CharStream> source() const { return m_scanner->charStream(); }
+	virtual ~ParserBase() = default;
 
 protected:
 	/// Utility class that creates an error and throws an exception if the

liblangutil/Scanner.cpp

@@ -135,24 +135,11 @@ private:
 	bool m_complete;
 };
 
-void Scanner::reset(CharStream _source)
-{
-	m_source = make_shared<CharStream>(std::move(_source));
-	reset();
-}
-
-void Scanner::reset(shared_ptr<CharStream> _source)
-{
-	solAssert(_source.get() != nullptr, "You MUST provide a CharStream when resetting.");
-	m_source = std::move(_source);
-	reset();
-}
-
 void Scanner::reset()
 {
-	m_source->reset();
+	m_source.reset();
 	m_kind = ScannerKind::Solidity;
-	m_char = m_source->get();
+	m_char = m_source.get();
 	skipWhitespace();
 	next();
 	next();
@@ -161,7 +148,7 @@ void Scanner::reset()
 
 void Scanner::setPosition(size_t _offset)
 {
-	m_char = m_source->setPosition(_offset);
+	m_char = m_source.setPosition(_offset);
 	scanToken();
 	next();
 	next();
@@ -227,7 +214,7 @@ void Scanner::rescan()
 		rollbackTo = static_cast<size_t>(m_tokens[Current].location.start);
 	else
 		rollbackTo = static_cast<size_t>(m_skippedComments[Current].location.start);
-	m_char = m_source->rollback(m_source->position() - rollbackTo);
+	m_char = m_source.rollback(m_source.position() - rollbackTo);
 	next();
 	next();
 	next();
@@ -322,12 +309,12 @@ Token Scanner::skipSingleLineComment()
 {
 	// Line terminator is not part of the comment. If it is a
 	// non-ascii line terminator, it will result in a parser error.
-	size_t startPosition = m_source->position();
+	size_t startPosition = m_source.position();
 	while (!isUnicodeLinebreak())
 		if (!advance())
 			break;
 
-	ScannerError unicodeDirectionError = validateBiDiMarkup(*m_source, startPosition);
+	ScannerError unicodeDirectionError = validateBiDiMarkup(m_source, startPosition);
 	if (unicodeDirectionError != ScannerError::NoError)
 		return setError(unicodeDirectionError);
 
@@ -360,28 +347,28 @@ bool Scanner::tryScanEndOfLine()
 size_t Scanner::scanSingleLineDocComment()
 {
 	LiteralScope literal(this, LITERAL_TYPE_COMMENT);
-	size_t endPosition = m_source->position();
+	size_t endPosition = m_source.position();
 
 	skipWhitespaceExceptUnicodeLinebreak();
 
 	while (!isSourcePastEndOfInput())
 	{
-		endPosition = m_source->position();
+		endPosition = m_source.position();
 		if (tryScanEndOfLine())
 		{
 			// Check if next line is also a single-line comment.
 			// If any whitespaces were skipped, use source position before.
 			if (!skipWhitespaceExceptUnicodeLinebreak())
-				endPosition = m_source->position();
+				endPosition = m_source.position();
 
-			if (!m_source->isPastEndOfInput(3) &&
+			if (!m_source.isPastEndOfInput(3) &&
-				m_source->get(0) == '/' &&
+				m_source.get(0) == '/' &&
-				m_source->get(1) == '/' &&
+				m_source.get(1) == '/' &&
-				m_source->get(2) == '/')
+				m_source.get(2) == '/')
 			{
-				if (!m_source->isPastEndOfInput(4) && m_source->get(3) == '/')
+				if (!m_source.isPastEndOfInput(4) && m_source.get(3) == '/')
 					break; // "////" is not a documentation comment
-				m_char = m_source->advanceAndGet(3);
+				m_char = m_source.advanceAndGet(3);
 				if (atEndOfLine())
 					continue;
 				addCommentLiteralChar('\n');
@@ -402,7 +389,7 @@ size_t Scanner::scanSingleLineDocComment()
 
 Token Scanner::skipMultiLineComment()
 {
-	size_t startPosition = m_source->position();
+	size_t startPosition = m_source.position();
 	while (!isSourcePastEndOfInput())
 	{
 		char prevChar = m_char;
@@ -413,7 +400,7 @@ Token Scanner::skipMultiLineComment()
 		// multi-line comments are treated as whitespace.
 		if (prevChar == '*' && m_char == '/')
 		{
-			ScannerError unicodeDirectionError = validateBiDiMarkup(*m_source, startPosition);
+			ScannerError unicodeDirectionError = validateBiDiMarkup(m_source, startPosition);
 			if (unicodeDirectionError != ScannerError::NoError)
 				return setError(unicodeDirectionError);
 
@@ -440,22 +427,22 @@ Token Scanner::scanMultiLineDocComment()
 		if (atEndOfLine())
 		{
 			skipWhitespace();
-			if (!m_source->isPastEndOfInput(1) && m_source->get(0) == '*' && m_source->get(1) == '*')
+			if (!m_source.isPastEndOfInput(1) && m_source.get(0) == '*' && m_source.get(1) == '*')
 			{ // it is unknown if this leads to the end of the comment
 				addCommentLiteralChar('*');
 				advance();
 			}
-			else if (!m_source->isPastEndOfInput(1) && m_source->get(0) == '*' && m_source->get(1) != '/')
+			else if (!m_source.isPastEndOfInput(1) && m_source.get(0) == '*' && m_source.get(1) != '/')
 			{ // skip first '*' in subsequent lines
-				m_char = m_source->advanceAndGet(1);
+				m_char = m_source.advanceAndGet(1);
 				if (atEndOfLine()) // ignores empty lines
 					continue;
 				if (charsAdded)
 					addCommentLiteralChar('\n'); // corresponds to the end of previous line
 			}
-			else if (!m_source->isPastEndOfInput(1) && m_source->get(0) == '*' && m_source->get(1) == '/')
+			else if (!m_source.isPastEndOfInput(1) && m_source.get(0) == '*' && m_source.get(1) == '/')
 			{ // if after newline the comment ends, don't insert the newline
-				m_char = m_source->advanceAndGet(2);
+				m_char = m_source.advanceAndGet(2);
 				endFound = true;
 				break;
 			}
@@ -463,9 +450,9 @@ Token Scanner::scanMultiLineDocComment()
 				addCommentLiteralChar('\n');
 		}
 
-		if (!m_source->isPastEndOfInput(1) && m_source->get(0) == '*' && m_source->get(1) == '/')
+		if (!m_source.isPastEndOfInput(1) && m_source.get(0) == '*' && m_source.get(1) == '/')
 		{
-			m_char = m_source->advanceAndGet(2);
+			m_char = m_source.advanceAndGet(2);
 			endFound = true;
 			break;
 		}
@@ -497,7 +484,7 @@ Token Scanner::scanSlash()
 				return skipSingleLineComment();
 			// doxygen style /// comment
 			m_skippedComments[NextNext].location.start = firstSlashPosition;
-			m_skippedComments[NextNext].location.source = m_source;
+			m_skippedComments[NextNext].location.sourceName = m_sourceName;
 			m_skippedComments[NextNext].token = Token::CommentLiteral;
 			m_skippedComments[NextNext].location.end = static_cast<int>(scanSingleLineDocComment());
 			return Token::Whitespace;
@@ -526,7 +513,7 @@ Token Scanner::scanSlash()
 				return skipMultiLineComment();
 			// we actually have a multiline documentation comment
 			m_skippedComments[NextNext].location.start = firstSlashPosition;
-			m_skippedComments[NextNext].location.source = m_source;
+			m_skippedComments[NextNext].location.sourceName = m_sourceName;
 			Token comment = scanMultiLineDocComment();
 			m_skippedComments[NextNext].location.end = static_cast<int>(sourcePos());
 			m_skippedComments[NextNext].token = comment;
@@ -766,7 +753,7 @@ void Scanner::scanToken()
 	}
 	while (token == Token::Whitespace);
 	m_tokens[NextNext].location.end = static_cast<int>(sourcePos());
-	m_tokens[NextNext].location.source = m_source;
+	m_tokens[NextNext].location.sourceName = m_sourceName;
 	m_tokens[NextNext].token = token;
 	m_tokens[NextNext].extendedTokenInfo = make_tuple(m, n);
 }
@@ -820,11 +807,11 @@ bool Scanner::isUnicodeLinebreak()
 	if (0x0a <= m_char && m_char <= 0x0d)
 		// line feed, vertical tab, form feed, carriage return
 		return true;
-	if (!m_source->isPastEndOfInput(1) && uint8_t(m_source->get(0)) == 0xc2 && uint8_t(m_source->get(1)) == 0x85)
+	if (!m_source.isPastEndOfInput(1) && uint8_t(m_source.get(0)) == 0xc2 && uint8_t(m_source.get(1)) == 0x85)
 		// NEL - U+0085, C2 85 in utf8
 		return true;
-	if (!m_source->isPastEndOfInput(2) && uint8_t(m_source->get(0)) == 0xe2 && uint8_t(m_source->get(1)) == 0x80 && (
+	if (!m_source.isPastEndOfInput(2) && uint8_t(m_source.get(0)) == 0xe2 && uint8_t(m_source.get(1)) == 0x80 && (
-		uint8_t(m_source->get(2)) == 0xa8 || uint8_t(m_source->get(2)) == 0xa9
+		uint8_t(m_source.get(2)) == 0xa8 || uint8_t(m_source.get(2)) == 0xa9
 	))
 		// LS - U+2028, E2 80 A8  in utf8
 		// PS - U+2029, E2 80 A9  in utf8
@@ -834,7 +821,7 @@ bool Scanner::isUnicodeLinebreak()
 
 Token Scanner::scanString(bool const _isUnicode)
 {
-	size_t startPosition = m_source->position();
+	size_t startPosition = m_source.position();
 	char const quote = m_char;
 	advance();  // consume quote
 	LiteralScope literal(this, LITERAL_TYPE_STRING);
@@ -865,7 +852,7 @@ Token Scanner::scanString(bool const _isUnicode)
 
 	if (_isUnicode)
 	{
-		ScannerError unicodeDirectionError = validateBiDiMarkup(*m_source, startPosition);
+		ScannerError unicodeDirectionError = validateBiDiMarkup(m_source, startPosition);
 		if (unicodeDirectionError != ScannerError::NoError)
 			return setError(unicodeDirectionError);
 	}
@@ -919,7 +906,7 @@ void Scanner::scanDecimalDigits()
 	// May continue with decimal digit or underscore for grouping.
 	do
 		addLiteralCharAndAdvance();
-	while (!m_source->isPastEndOfInput() && (isDecimalDigit(m_char) || m_char == '_'));
+	while (!m_source.isPastEndOfInput() && (isDecimalDigit(m_char) || m_char == '_'));
 
 	// Defer further validation of underscore to SyntaxChecker.
 }
@@ -965,7 +952,7 @@ Token Scanner::scanNumber(char _charSeen)
 			scanDecimalDigits();  // optional
 			if (m_char == '.')
 			{
-				if (!m_source->isPastEndOfInput(1) && m_source->get(1) == '_')
+				if (!m_source.isPastEndOfInput(1) && m_source.get(1) == '_')
 				{
 					// Assume the input may be a floating point number with leading '_' in fraction part.
 					// Recover by consuming it all but returning `Illegal` right away.
@@ -973,7 +960,7 @@ Token Scanner::scanNumber(char _charSeen)
 					addLiteralCharAndAdvance(); // '_'
 					scanDecimalDigits();
 				}
-				if (m_source->isPastEndOfInput() || !isDecimalDigit(m_source->get(1)))
+				if (m_source.isPastEndOfInput() || !isDecimalDigit(m_source.get(1)))
 				{
 					// A '.' has to be followed by a number.
 					literal.complete();
@@ -990,7 +977,7 @@ Token Scanner::scanNumber(char _charSeen)
 		solAssert(kind != HEX, "'e'/'E' must be scanned as part of the hex number");
 		if (kind != DECIMAL)
 			return setError(ScannerError::IllegalExponent);
-		else if (!m_source->isPastEndOfInput(1) && m_source->get(1) == '_')
+		else if (!m_source.isPastEndOfInput(1) && m_source.get(1) == '_')
 		{
 			// Recover from wrongly placed underscore as delimiter in literal with scientific
 			// notation by consuming until the end.

liblangutil/Scanner.h

@@ -55,8 +55,6 @@
 #include <liblangutil/Token.h>
 #include <liblangutil/CharStream.h>
 #include <liblangutil/SourceLocation.h>
-#include <libsolutil/Common.h>
-#include <libsolutil/CommonData.h>
 
 #include <optional>
 #include <iosfwd>
@@ -102,17 +100,13 @@ class Scanner
 {
 	friend class LiteralScope;
 public:
-	explicit Scanner(std::shared_ptr<CharStream> _source) { reset(std::move(_source)); }
+	explicit Scanner(CharStream& _source):
-	explicit Scanner(CharStream _source = CharStream()) { reset(std::move(_source)); }
+		m_source(_source),
+		m_sourceName{std::make_shared<std::string>(_source.name())}
+	{
+		reset();
+	}
 
-	std::string const& source() const noexcept { return m_source->source(); }
-
-	std::shared_ptr<CharStream> charStream() noexcept { return m_source; }
-	std::shared_ptr<CharStream const> charStream() const noexcept { return m_source; }
-
-	/// Resets the scanner as if newly constructed with _source as input.
-	void reset(CharStream _source);
-	void reset(std::shared_ptr<CharStream> _source);
 	/// Resets scanner to the start of input.
 	void reset();
 
@@ -125,6 +119,8 @@ public:
 		rescan();
 	}
 
+	CharStream const& charStream() const noexcept { return m_source; }
+
 	/// @returns the next token and advances input
 	Token next();
 
@@ -177,14 +173,6 @@ public:
 	Token peekNextNextToken() const { return m_tokens[NextNext].token; }
 	///@}
 
-	///@{
-	///@name Error printing helper functions
-	/// Functions that help pretty-printing parse errors
-	/// Do only use in error cases, they are quite expensive.
-	std::string lineAtPosition(int _position) const { return m_source->lineAtPosition(_position); }
-	std::tuple<int, int> translatePositionToLineColumn(int _position) const { return m_source->translatePositionToLineColumn(_position); }
-	///@}
-
 private:
 
 	inline Token setError(ScannerError _error) noexcept
@@ -211,8 +199,8 @@ private:
 	void addUnicodeAsUTF8(unsigned codepoint);
 	///@}
 
-	bool advance() { m_char = m_source->advanceAndGet(); return !m_source->isPastEndOfInput(); }
+	bool advance() { m_char = m_source.advanceAndGet(); return !m_source.isPastEndOfInput(); }
-	void rollback(size_t _amount) { m_char = m_source->rollback(_amount); }
+	void rollback(size_t _amount) { m_char = m_source.rollback(_amount); }
 	/// Rolls back to the start of the current token and re-runs the scanner.
 	void rescan();
 
@@ -261,15 +249,16 @@ private:
 	bool isUnicodeLinebreak();
 
 	/// Return the current source position.
-	size_t sourcePos() const { return m_source->position(); }
+	size_t sourcePos() const { return m_source.position(); }
-	bool isSourcePastEndOfInput() const { return m_source->isPastEndOfInput(); }
+	bool isSourcePastEndOfInput() const { return m_source.isPastEndOfInput(); }
 
 	enum TokenIndex { Current, Next, NextNext };
 
 	TokenDesc m_skippedComments[3] = {}; // desc for the current, next and nextnext skipped comment
 	TokenDesc m_tokens[3] = {}; // desc for the current, next and nextnext token
 
-	std::shared_ptr<CharStream> m_source;
+	CharStream& m_source;
+	std::shared_ptr<std::string const> m_sourceName;
 
 	ScannerKind m_kind = ScannerKind::Solidity;
 

liblangutil/SemVerHandler.cpp

@@ -23,12 +23,20 @@
 
 #include <liblangutil/SemVerHandler.h>
 
+#include <liblangutil/Exceptions.h>
+
 #include <functional>
 
 using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
 
+SemVerMatchExpressionParser::SemVerMatchExpressionParser(vector<Token> _tokens, vector<string> _literals):
+	m_tokens(std::move(_tokens)), m_literals(std::move(_literals))
+{
+	solAssert(m_tokens.size() == m_literals.size(), "");
+}
+
 SemVerVersion::SemVerVersion(string const& _versionString)
 {
 	auto i = _versionString.begin();

liblangutil/SemVerHandler.h

@@ -85,11 +85,7 @@ struct SemVerMatchExpression
 class SemVerMatchExpressionParser
 {
 public:
-	SemVerMatchExpressionParser(std::vector<Token> _tokens, std::vector<std::string> _literals):
+	SemVerMatchExpressionParser(std::vector<Token> _tokens, std::vector<std::string> _literals);
-		m_tokens(std::move(_tokens)), m_literals(std::move(_literals))
-	{
-		solAssert(m_tokens.size() == m_literals.size(), "");
-	}
 
 	/// Returns an expression if it was parseable, or nothing otherwise.
 	std::optional<SemVerMatchExpression> parse();

liblangutil/SourceLocation.cpp

@@ -21,16 +21,18 @@
 #include <boost/algorithm/string/split.hpp>
 #include <boost/algorithm/string.hpp>
 
-using namespace solidity;
+#include <iostream>
-namespace solidity::langutil
-{
 
-SourceLocation const parseSourceLocation(std::string const& _input, std::string const& _sourceName, size_t _maxIndex)
+using namespace solidity;
+using namespace solidity::langutil;
+using namespace std;
+
+SourceLocation solidity::langutil::parseSourceLocation(string const& _input, vector<shared_ptr<string const>> const& _sourceNames)
 {
 	// Expected input: "start:length:sourceindex"
-	enum SrcElem : size_t { Start, Length, Index };
+	enum SrcElem: size_t { Start, Length, Index };
 
-	std::vector<std::string> pos;
+	vector<string> pos;
 
 	boost::algorithm::split(pos, _input, boost::is_any_of(":"));
 
@@ -38,19 +40,28 @@ SourceLocation const parseSourceLocation(std::string const& _input, std::string
 	auto const sourceIndex = stoi(pos[Index]);
 
 	astAssert(
-		sourceIndex == -1 || _maxIndex >= static_cast<size_t>(sourceIndex),
+		sourceIndex == -1 || (0 <= sourceIndex && static_cast<size_t>(sourceIndex) < _sourceNames.size()),
 		"'src'-field ill-formatted or src-index too high"
 	);
 
 	int start = stoi(pos[Start]);
 	int end = start + stoi(pos[Length]);
 
-	// ASSUMPTION: only the name of source is used from here on, the m_source of the CharStream-Object can be empty
+	SourceLocation result{start, end, {}};
-	std::shared_ptr<langutil::CharStream> source;
 	if (sourceIndex != -1)
-		source = std::make_shared<langutil::CharStream>("", _sourceName);
+		result.sourceName = _sourceNames.at(static_cast<size_t>(sourceIndex));
-
+	return result;
-	return SourceLocation{start, end, source};
 }
 
+std::ostream& solidity::langutil::operator<<(std::ostream& _out, SourceLocation const& _location)
+{
+	if (!_location.isValid())
+		return _out << "NO_LOCATION_SPECIFIED";
+
+	if (_location.sourceName)
+		_out << *_location.sourceName;
+
+	_out << "[" << _location.start << "," << _location.end << "]";
+
+	return _out;
 }

liblangutil/SourceLocation.h

@@ -23,18 +23,14 @@
 
 #pragma once
 
-#include <libsolutil/Assertions.h>
+#include <iosfwd>
-#include <libsolutil/Exceptions.h>
-
-#include <liblangutil/CharStream.h>
-
-#include <limits>
 #include <memory>
 #include <string>
+#include <tuple>
+#include <vector>
 
 namespace solidity::langutil
 {
-struct SourceLocationError: virtual util::Exception {};
 
 /**
  * Representation of an interval of source positions.
@@ -44,51 +40,44 @@ struct SourceLocation
 {
 	bool operator==(SourceLocation const& _other) const
 	{
-		return source.get() == _other.source.get() && start == _other.start && end == _other.end;
+		return start == _other.start && end == _other.end && equalSources(_other);
 	}
 	bool operator!=(SourceLocation const& _other) const { return !operator==(_other); }
 
-	inline bool operator<(SourceLocation const& _other) const
+	bool operator<(SourceLocation const& _other) const
 	{
-		if (!source|| !_other.source)
+		if (!sourceName || !_other.sourceName)
-			return std::make_tuple(int(!!source), start, end) < std::make_tuple(int(!!_other.source), _other.start, _other.end);
+			return std::make_tuple(int(!!sourceName), start, end) < std::make_tuple(int(!!_other.sourceName), _other.start, _other.end);
 		else
-			return std::make_tuple(source->name(), start, end) < std::make_tuple(_other.source->name(), _other.start, _other.end);
+			return std::make_tuple(*sourceName, start, end) < std::make_tuple(*_other.sourceName, _other.start, _other.end);
 	}
 
-	inline bool contains(SourceLocation const& _other) const
+	bool contains(SourceLocation const& _other) const
 	{
-		if (!hasText() || !_other.hasText() || source.get() != _other.source.get())
+		if (!hasText() || !_other.hasText() || !equalSources(_other))
 			return false;
 		return start <= _other.start && _other.end <= end;
 	}
 
-	inline bool intersects(SourceLocation const& _other) const
+	bool intersects(SourceLocation const& _other) const
 	{
-		if (!hasText() || !_other.hasText() || source.get() != _other.source.get())
+		if (!hasText() || !_other.hasText() || !equalSources(_other))
 			return false;
 		return _other.start < end && start < _other.end;
 	}
 
-	bool isValid() const { return source || start != -1 || end != -1; }
+	bool equalSources(SourceLocation const& _other) const
-
-	bool hasText() const
 	{
-		return
+		if (!!sourceName != !!_other.sourceName)
-			source &&
+			return false;
-			0 <= start &&
+		if (sourceName && *sourceName != *_other.sourceName)
-			start <= end &&
+			return false;
-			end <= int(source->source().length());
+		return true;
 	}
 
-	std::string text() const
+	bool isValid() const { return sourceName || start != -1 || end != -1; }
-	{
+
-		assertThrow(source, SourceLocationError, "Requested text from null source.");
+	bool hasText() const { return sourceName && 0 <= start && start <= end; }
-		assertThrow(0 <= start, SourceLocationError, "Invalid source location.");
-		assertThrow(start <= end, SourceLocationError, "Invalid source location.");
-		assertThrow(end <= int(source->source().length()), SourceLocationError, "Invalid source location.");
-		return source->source().substr(size_t(start), size_t(end - start));
-	}
 
 	/// @returns the smallest SourceLocation that contains both @param _a and @param _b.
 	/// Assumes that @param _a and @param _b refer to the same source (exception: if the source of either one
@@ -97,8 +86,8 @@ struct SourceLocation
 	/// @param _b, then start resp. end of the result will be -1 as well).
 	static SourceLocation smallestCovering(SourceLocation _a, SourceLocation const& _b)
 	{
-		if (!_a.source)
+		if (!_a.sourceName)
-			_a.source = _b.source;
+			_a.sourceName = _b.sourceName;
 
 		if (_a.start < 0)
 			_a.start = _b.start;
@@ -112,27 +101,15 @@ struct SourceLocation
 
 	int start = -1;
 	int end = -1;
-	std::shared_ptr<CharStream> source;
+	std::shared_ptr<std::string const> sourceName;
 };
 
-SourceLocation const parseSourceLocation(
+SourceLocation parseSourceLocation(
 	std::string const& _input,
-	std::string const& _sourceName,
+	std::vector<std::shared_ptr<std::string const>> const& _sourceNames
-	size_t _maxIndex = std::numeric_limits<size_t>::max()
 );
 
 /// Stream output for Location (used e.g. in boost exceptions).
-inline std::ostream& operator<<(std::ostream& _out, SourceLocation const& _location)
+std::ostream& operator<<(std::ostream& _out, SourceLocation const& _location);
-{
-	if (!_location.isValid())
-		return _out << "NO_LOCATION_SPECIFIED";
-
-	if (_location.source)
-		_out << _location.source->name();
-
-	_out << "[" << _location.start << "," << _location.end << "]";
-
-	return _out;
-}
 
 }

liblangutil/SourceReferenceExtractor.cpp

@@ -16,8 +16,9 @@
 */
 // SPDX-License-Identifier: GPL-3.0
 #include <liblangutil/SourceReferenceExtractor.h>
-#include <liblangutil/CharStream.h>
 #include <liblangutil/Exceptions.h>
+#include <liblangutil/CharStreamProvider.h>
+#include <liblangutil/CharStream.h>
 
 #include <algorithm>
 #include <cmath>
@@ -26,46 +27,57 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
 
-SourceReferenceExtractor::Message SourceReferenceExtractor::extract(util::Exception const& _exception, string _category)
+SourceReferenceExtractor::Message SourceReferenceExtractor::extract(
+	CharStreamProvider const& _charStreamProvider,
+	util::Exception const& _exception,
+	string _category
+)
 {
 	SourceLocation const* location = boost::get_error_info<errinfo_sourceLocation>(_exception);
 
 	string const* message = boost::get_error_info<util::errinfo_comment>(_exception);
-	SourceReference primary = extract(location, message ? *message : "");
+	SourceReference primary = extract(_charStreamProvider, location, message ? *message : "");
 
 	std::vector<SourceReference> secondary;
 	auto secondaryLocation = boost::get_error_info<errinfo_secondarySourceLocation>(_exception);
 	if (secondaryLocation && !secondaryLocation->infos.empty())
 		for (auto const& info: secondaryLocation->infos)
-			secondary.emplace_back(extract(&info.second, info.first));
+			secondary.emplace_back(extract(_charStreamProvider, &info.second, info.first));
 
 	return Message{std::move(primary), _category, std::move(secondary), nullopt};
 }
 
-SourceReferenceExtractor::Message SourceReferenceExtractor::extract(Error const& _error)
+SourceReferenceExtractor::Message SourceReferenceExtractor::extract(
+	CharStreamProvider const& _charStreamProvider,
+	Error const& _error
+)
 {
 	string category = (_error.type() == Error::Type::Warning) ? "Warning" : "Error";
-	Message message = extract(_error, category);
+	Message message = extract(_charStreamProvider, _error, category);
 	message.errorId = _error.errorId();
 	return message;
 }
 
-SourceReference SourceReferenceExtractor::extract(SourceLocation const* _location, std::string message)
+SourceReference SourceReferenceExtractor::extract(
+	CharStreamProvider const& _charStreamProvider,
+	SourceLocation const* _location,
+	std::string message
+)
 {
-	if (!_location || !_location->source.get()) // Nothing we can extract here
+	if (!_location || !_location->sourceName) // Nothing we can extract here
 		return SourceReference::MessageOnly(std::move(message));
 
 	if (!_location->hasText()) // No source text, so we can only extract the source name
-		return SourceReference::MessageOnly(std::move(message), _location->source->name());
+		return SourceReference::MessageOnly(std::move(message), *_location->sourceName);
 
-	shared_ptr<CharStream> const& source = _location->source;
+	CharStream const& charStream = _charStreamProvider.charStream(*_location->sourceName);
 
-	LineColumn const interest = source->translatePositionToLineColumn(_location->start);
+	LineColumn const interest = charStream.translatePositionToLineColumn(_location->start);
 	LineColumn start = interest;
-	LineColumn end = source->translatePositionToLineColumn(_location->end);
+	LineColumn end = charStream.translatePositionToLineColumn(_location->end);
 	bool const isMultiline = start.line != end.line;
 
-	string line = source->lineAtPosition(_location->start);
+	string line = charStream.lineAtPosition(_location->start);
 
 	int locationLength =
 		isMultiline ?
@@ -102,7 +114,7 @@ SourceReference SourceReferenceExtractor::extract(SourceLocation const* _locatio
 
 	return SourceReference{
 		std::move(message),
-		source->name(),
+		*_location->sourceName,
 		interest,
 		isMultiline,
 		line,

liblangutil/SourceReferenceExtractor.h

@@ -28,6 +28,8 @@
 namespace solidity::langutil
 {
 
+class CharStreamProvider;
+
 struct LineColumn
 {
 	int line = {-1};
@@ -67,9 +69,9 @@ namespace SourceReferenceExtractor
 		std::optional<ErrorId> errorId;
 	};
 
-	Message extract(util::Exception const& _exception, std::string _category);
+	Message extract(CharStreamProvider const& _charStreamProvider, util::Exception const& _exception, std::string _category);
-	Message extract(Error const& _error);
+	Message extract(CharStreamProvider const& _charStreamProvider, Error const& _error);
-	SourceReference extract(SourceLocation const* _location, std::string message = "");
+	SourceReference extract(CharStreamProvider const& _charStreamProvider, SourceLocation const* _location, std::string message = "");
 }
 
 }

liblangutil/SourceReferenceFormatter.cpp

@@ -21,6 +21,8 @@
 
 #include <liblangutil/SourceReferenceFormatter.h>
 #include <liblangutil/Exceptions.h>
+#include <liblangutil/CharStream.h>
+#include <liblangutil/CharStreamProvider.h>
 #include <libsolutil/UTF8.h>
 #include <iomanip>
 #include <string_view>
@@ -45,6 +47,14 @@ std::string replaceNonTabs(std::string_view _utf8Input, char _filler)
 
 }
 
+std::string SourceReferenceFormatter::formatErrorInformation(Error const& _error, CharStream const& _charStream)
+{
+	return formatErrorInformation(
+		_error,
+		SingletonCharStreamProvider(_charStream)
+	);
+}
+
 AnsiColorized SourceReferenceFormatter::normalColored() const
 {
 	return AnsiColorized(m_stream, m_colored, {WHITE});
@@ -173,10 +183,16 @@ void SourceReferenceFormatter::printExceptionInformation(SourceReferenceExtracto
 
 void SourceReferenceFormatter::printExceptionInformation(util::Exception const& _exception, std::string const& _category)
 {
-	printExceptionInformation(SourceReferenceExtractor::extract(_exception, _category));
+	printExceptionInformation(SourceReferenceExtractor::extract(m_charStreamProvider, _exception, _category));
+}
+
+void SourceReferenceFormatter::printErrorInformation(ErrorList const& _errors)
+{
+	for (auto const& error: _errors)
+		printErrorInformation(*error);
 }
 
 void SourceReferenceFormatter::printErrorInformation(Error const& _error)
 {
-	printExceptionInformation(SourceReferenceExtractor::extract(_error));
+	printExceptionInformation(SourceReferenceExtractor::extract(m_charStreamProvider, _error));
 }

liblangutil/SourceReferenceFormatter.h

@@ -32,42 +32,58 @@
 
 namespace solidity::langutil
 {
+
+class CharStream;
+class CharStreamProvider;
 struct SourceLocation;
 
 class SourceReferenceFormatter
 {
 public:
-	SourceReferenceFormatter(std::ostream& _stream, bool _colored, bool _withErrorIds):
+	SourceReferenceFormatter(
-		m_stream(_stream), m_colored(_colored), m_withErrorIds(_withErrorIds)
+		std::ostream& _stream,
+		CharStreamProvider const& _charStreamProvider,
+		bool _colored,
+		bool _withErrorIds
+	):
+		m_stream(_stream), m_charStreamProvider(_charStreamProvider), m_colored(_colored), m_withErrorIds(_withErrorIds)
 	{}
 
 	/// Prints source location if it is given.
 	void printSourceLocation(SourceReference const& _ref);
 	void printExceptionInformation(SourceReferenceExtractor::Message const& _msg);
 	void printExceptionInformation(util::Exception const& _exception, std::string const& _category);
+	void printErrorInformation(langutil::ErrorList const& _errors);
 	void printErrorInformation(Error const& _error);
 
 	static std::string formatExceptionInformation(
 		util::Exception const& _exception,
 		std::string const& _name,
+		CharStreamProvider const& _charStreamProvider,
 		bool _colored = false,
 		bool _withErrorIds = false
 	)
 	{
 		std::ostringstream errorOutput;
-		SourceReferenceFormatter formatter(errorOutput, _colored, _withErrorIds);
+		SourceReferenceFormatter formatter(errorOutput, _charStreamProvider, _colored, _withErrorIds);
 		formatter.printExceptionInformation(_exception, _name);
 		return errorOutput.str();
 	}
 
-	static std::string formatErrorInformation(Error const& _error)
+	static std::string formatErrorInformation(
+		Error const& _error,
+		CharStreamProvider const& _charStreamProvider
+	)
 	{
 		return formatExceptionInformation(
 			_error,
-			(_error.type() == Error::Type::Warning) ? "Warning" : "Error"
+			(_error.type() == Error::Type::Warning) ? "Warning" : "Error",
+			_charStreamProvider
 		);
 	}
 
+	static std::string formatErrorInformation(Error const& _error, CharStream const& _charStream);
+
 private:
 	util::AnsiColorized normalColored() const;
 	util::AnsiColorized frameColored() const;
@@ -79,6 +95,7 @@ private:
 
 private:
 	std::ostream& m_stream;
+	CharStreamProvider const& m_charStreamProvider;
 	bool m_colored;
 	bool m_withErrorIds;
 };

liblangutil/Token.cpp

@@ -41,6 +41,7 @@
 // along with solidity.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <liblangutil/Token.h>
+#include <liblangutil/Exceptions.h>
 #include <map>
 
 using namespace std;
@@ -48,6 +49,24 @@ using namespace std;
 namespace solidity::langutil
 {
 
+Token TokenTraits::AssignmentToBinaryOp(Token op)
+{
+	solAssert(isAssignmentOp(op) && op != Token::Assign, "");
+	return static_cast<Token>(static_cast<int>(op) + (static_cast<int>(Token::BitOr) - static_cast<int>(Token::AssignBitOr)));
+}
+
+std::string ElementaryTypeNameToken::toString(bool const& tokenValue) const
+{
+	std::string name = TokenTraits::toString(m_token);
+	if (tokenValue || (firstNumber() == 0 && secondNumber() == 0))
+		return name;
+	solAssert(name.size() >= 3, "Token name size should be greater than 3. Should not reach here.");
+	if (m_token == Token::FixedMxN || m_token == Token::UFixedMxN)
+		return name.substr(0, name.size() - 3) + std::to_string(m_firstNumber) + "x" + std::to_string(m_secondNumber);
+	else
+		return name.substr(0, name.size() - 1) + std::to_string(m_firstNumber);
+}
+
 void ElementaryTypeNameToken::assertDetails(Token _baseType, unsigned const& _first, unsigned const& _second)
 {
 	solAssert(TokenTraits::isElementaryTypeName(_baseType), "Expected elementary type name: " + string(TokenTraits::toString(_baseType)));

liblangutil/Token.h

@@ -42,8 +42,6 @@
 
 #pragma once
 
-#include <libsolutil/Common.h>
-#include <liblangutil/Exceptions.h>
 #include <liblangutil/UndefMacros.h>
 
 #include <iosfwd>
@@ -330,11 +328,7 @@ namespace TokenTraits
 
 	bool isYulKeyword(std::string const& _literal);
 
-	inline Token AssignmentToBinaryOp(Token op)
+	Token AssignmentToBinaryOp(Token op);
-	{
-		solAssert(isAssignmentOp(op) && op != Token::Assign, "");
-		return static_cast<Token>(static_cast<int>(op) + (static_cast<int>(Token::BitOr) - static_cast<int>(Token::AssignBitOr)));
-	}
 
 	// @returns the precedence > 0 for binary and compare
 	// operators; returns 0 otherwise.
@@ -394,17 +388,7 @@ public:
 	Token token() const { return m_token; }
 
 	///if tokValue is set to true, then returns the actual token type name, otherwise, returns full type
-	std::string toString(bool const& tokenValue = false) const
+	std::string toString(bool const& tokenValue = false) const;
-	{
-		std::string name = TokenTraits::toString(m_token);
-		if (tokenValue || (firstNumber() == 0 && secondNumber() == 0))
-			return name;
-		solAssert(name.size() >= 3, "Token name size should be greater than 3. Should not reach here.");
-		if (m_token == Token::FixedMxN || m_token == Token::UFixedMxN)
-			return name.substr(0, name.size() - 3) + std::to_string(m_firstNumber) + "x" + std::to_string(m_secondNumber);
-		else
-			return name.substr(0, name.size() - 1) + std::to_string(m_firstNumber);
-	}
 
 private:
 	Token m_token;

libsmtutil/SMTPortfolio.cpp

@@ -40,6 +40,7 @@ SMTPortfolio::SMTPortfolio(
 ):
 	SolverInterface(_queryTimeout)
 {
+	if (_enabledSolvers.smtlib2)
 		m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
 #ifdef HAVE_Z3
 	if (_enabledSolvers.z3 && Z3Interface::available())
@@ -143,10 +144,11 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
 vector<string> SMTPortfolio::unhandledQueries()
 {
 	// This code assumes that the constructor guarantees that
-	// SmtLib2Interface is in position 0.
+	// SmtLib2Interface is in position 0, if enabled.
-	smtAssert(!m_solvers.empty(), "");
+	if (!m_solvers.empty())
-	smtAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
+		if (auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()))
-	return m_solvers.front()->unhandledQueries();
+			return smtlib2->unhandledQueries();
+	return {};
 }
 
 bool SMTPortfolio::solverAnswered(CheckResult result)

libsmtutil/SolverInterface.h

@@ -23,10 +23,13 @@
 
 #include <libsolutil/Common.h>
 
+#include <range/v3/view.hpp>
+
 #include <cstdio>
 #include <map>
 #include <memory>
 #include <optional>
+#include <set>
 #include <string>
 #include <vector>
 
@@ -36,16 +39,71 @@ namespace solidity::smtutil
 struct SMTSolverChoice
 {
 	bool cvc4 = false;
+	bool smtlib2 = false;
 	bool z3 = false;
 
-	static constexpr SMTSolverChoice All() { return {true, true}; }
+	static constexpr SMTSolverChoice All() { return {true, true, true}; }
-	static constexpr SMTSolverChoice CVC4() { return {true, false}; }
+	static constexpr SMTSolverChoice CVC4() { return {true, false, false}; }
-	static constexpr SMTSolverChoice Z3() { return {false, true}; }
+	static constexpr SMTSolverChoice SMTLIB2() { return {false, true, false}; }
-	static constexpr SMTSolverChoice None() { return {false, false}; }
+	static constexpr SMTSolverChoice Z3() { return {false, false, true}; }
+	static constexpr SMTSolverChoice None() { return {false, false, false}; }
+
+	static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
+	{
+		SMTSolverChoice solvers;
+		if (_solvers == "all")
+		{
+			smtAssert(solvers.setSolver("cvc4"), "");
+			smtAssert(solvers.setSolver("smtlib2"), "");
+			smtAssert(solvers.setSolver("z3"), "");
+		}
+		else
+			for (auto&& s: _solvers | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
+				if (!solvers.setSolver(s))
+					return {};
+
+		return solvers;
+	}
+
+	SMTSolverChoice& operator&(SMTSolverChoice const& _other)
+	{
+		cvc4 &= _other.cvc4;
+		smtlib2 &= _other.smtlib2;
+		z3 &= _other.z3;
+		return *this;
+	}
+
+	SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
+	{
+		return *this & _other;
+	}
+
+	bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); }
+
+	bool operator==(SMTSolverChoice const& _other) const noexcept
+	{
+		return cvc4 == _other.cvc4 &&
+			smtlib2 == _other.smtlib2 &&
+			z3 == _other.z3;
+	}
+
+	bool setSolver(std::string const& _solver)
+	{
+		static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
+		if (!solvers.count(_solver))
+			return false;
+		if (_solver == "cvc4")
+			cvc4 = true;
+		else if (_solver == "smtlib2")
+			smtlib2 = true;
+		else if (_solver == "z3")
+			z3 = true;
+		return true;
+	}
 
 	bool none() { return !some(); }
-	bool some() { return cvc4 || z3; }
+	bool some() { return cvc4 || smtlib2 || z3; }
-	bool all() { return cvc4 && z3; }
+	bool all() { return cvc4 && smtlib2 && z3; }
 };
 
 enum class CheckResult

libsolidity/analysis/NameAndTypeResolver.cpp

@@ -520,9 +520,9 @@ bool DeclarationRegistrationHelper::registerDeclaration(
 		Declaration const* conflictingDeclaration = _container.conflictingDeclaration(_declaration, _name);
 		solAssert(conflictingDeclaration, "");
 		bool const comparable =
-			_errorLocation->source &&
+			_errorLocation->sourceName &&
-			conflictingDeclaration->location().source &&
+			conflictingDeclaration->location().sourceName &&
-			_errorLocation->source->name() == conflictingDeclaration->location().source->name();
+			*_errorLocation->sourceName == *conflictingDeclaration->location().sourceName;
 		if (comparable && _errorLocation->start < conflictingDeclaration->location().start)
 		{
 			firstDeclarationLocation = *_errorLocation;

libsolidity/analysis/SyntaxChecker.cpp

@@ -68,7 +68,7 @@ void SyntaxChecker::endVisit(SourceUnit const& _sourceUnit)
 				string(";\"");
 
 		// when reporting the warning, print the source name only
-		m_errorReporter.warning(3420_error, {-1, -1, _sourceUnit.location().source}, errorString);
+		m_errorReporter.warning(3420_error, {-1, -1, _sourceUnit.location().sourceName}, errorString);
 	}
 	if (!m_sourceUnit->annotation().useABICoderV2.set())
 		m_sourceUnit->annotation().useABICoderV2 = true;

libsolidity/ast/ASTJsonConverter.cpp

@@ -110,8 +110,8 @@ void ASTJsonConverter::setJsonNode(
 
 optional<size_t> ASTJsonConverter::sourceIndexFromLocation(SourceLocation const& _location) const
 {
-	if (_location.source && m_sourceIndices.count(_location.source->name()))
+	if (_location.sourceName && m_sourceIndices.count(*_location.sourceName))
-		return m_sourceIndices.at(_location.source->name());
+		return m_sourceIndices.at(*_location.sourceName);
 	else
 		return nullopt;
 }

libsolidity/ast/ASTJsonImporter.cpp

@@ -57,14 +57,12 @@ ASTPointer<T> ASTJsonImporter::nullOrCast(Json::Value const& _json)
 
 map<string, ASTPointer<SourceUnit>> ASTJsonImporter::jsonToSourceUnit(map<string, Json::Value> const& _sourceList)
 {
-	m_sourceList = _sourceList;
 	for (auto const& src: _sourceList)
-		m_sourceLocations.emplace_back(make_shared<string const>(src.first));
+		m_sourceNames.emplace_back(make_shared<string const>(src.first));
-	for (auto const& srcPair: m_sourceList)
+	for (auto const& srcPair: _sourceList)
 	{
 		astAssert(!srcPair.second.isNull(), "");
 		astAssert(member(srcPair.second,"nodeType") == "SourceUnit", "The 'nodeType' of the highest node must be 'SourceUnit'.");
-		m_currentSourceName = srcPair.first;
 		m_sourceUnits[srcPair.first] = createSourceUnit(srcPair.second, srcPair.first);
 	}
 	return m_sourceUnits;
@@ -94,14 +92,14 @@ SourceLocation const ASTJsonImporter::createSourceLocation(Json::Value const& _n
 {
 	astAssert(member(_node, "src").isString(), "'src' must be a string");
 
-	return solidity::langutil::parseSourceLocation(_node["src"].asString(), m_currentSourceName, m_sourceLocations.size());
+	return solidity::langutil::parseSourceLocation(_node["src"].asString(), m_sourceNames);
 }
 
 SourceLocation ASTJsonImporter::createNameSourceLocation(Json::Value const& _node)
 {
 	astAssert(member(_node, "nameLocation").isString(), "'nameLocation' must be a string");
 
-	return solidity::langutil::parseSourceLocation(_node["nameLocation"].asString(), m_currentSourceName, m_sourceLocations.size());
+	return solidity::langutil::parseSourceLocation(_node["nameLocation"].asString(), m_sourceNames);
 }
 
 template<class T>
@@ -616,7 +614,7 @@ ASTPointer<InlineAssembly> ASTJsonImporter::createInlineAssembly(Json::Value con
 	astAssert(m_evmVersion == evmVersion, "Imported tree evm version differs from configured evm version!");
 
 	yul::Dialect const& dialect = yul::EVMDialect::strictAssemblyForEVM(evmVersion.value());
-	shared_ptr<yul::Block> operations = make_shared<yul::Block>(yul::AsmJsonImporter(m_currentSourceName).createBlock(member(_node, "AST")));
+	shared_ptr<yul::Block> operations = make_shared<yul::Block>(yul::AsmJsonImporter(m_sourceNames).createBlock(member(_node, "AST")));
 	return createASTNode<InlineAssembly>(
 		_node,
 		nullOrASTString(_node, "documentation"),
@@ -960,7 +958,8 @@ Json::Value ASTJsonImporter::member(Json::Value const& _node, string const& _nam
 
 Token ASTJsonImporter::scanSingleToken(Json::Value const& _node)
 {
-	langutil::Scanner scanner{langutil::CharStream(_node.asString(), "")};
+	langutil::CharStream charStream(_node.asString(), "");
+	langutil::Scanner scanner{charStream};
 	astAssert(scanner.peekNextToken() == Token::EOS, "Token string is too long.");
 	return scanner.currentToken();
 }

libsolidity/ast/ASTJsonImporter.h

@@ -152,13 +152,10 @@ private:
 	///@}
 
 	// =========== member variables ===============
-	/// Stores filepath as sourcenames to AST in JSON format
+	/// list of source names, order by source index
-	std::map<std::string, Json::Value> m_sourceList;
+	std::vector<std::shared_ptr<std::string const>> m_sourceNames;
-	/// list of filepaths (used as sourcenames)
-	std::vector<std::shared_ptr<std::string const>> m_sourceLocations;
 	/// filepath to AST
 	std::map<std::string, ASTPointer<SourceUnit>> m_sourceUnits;
-	std::string m_currentSourceName;
 	/// IDs already used by the nodes
 	std::set<int64_t> m_usedIDs;
 	/// Configured EVM version

libsolidity/codegen/CompilerContext.cpp

@@ -434,14 +434,14 @@ void CompilerContext::appendInlineAssembly(
 
 	ErrorList errors;
 	ErrorReporter errorReporter(errors);
-	auto scanner = make_shared<langutil::Scanner>(langutil::CharStream(_assembly, _sourceName));
+	langutil::CharStream charStream(_assembly, _sourceName);
 	yul::EVMDialect const& dialect = yul::EVMDialect::strictAssemblyForEVM(m_evmVersion);
 	optional<langutil::SourceLocation> locationOverride;
 	if (!_system)
 		locationOverride = m_asm->currentSourceLocation();
 	shared_ptr<yul::Block> parserResult =
 		yul::Parser(errorReporter, dialect, std::move(locationOverride))
-		.parse(scanner, false);
+		.parse(charStream);
 #ifdef SOL_OUTPUT_ASM
 	cout << yul::AsmPrinter(&dialect)(*parserResult) << endl;
 #endif
@@ -455,7 +455,9 @@ void CompilerContext::appendInlineAssembly(
 			_assembly + "\n"
 			"------------------ Errors: ----------------\n";
 		for (auto const& error: errorReporter.errors())
-			message += SourceReferenceFormatter::formatErrorInformation(*error);
+			// TODO if we have "locationOverride", it will be the wrong char stream,
+			// but we do not have access to the solidity scanner.
+			message += SourceReferenceFormatter::formatErrorInformation(*error, charStream);
 		message += "-------------------------------------------\n";
 
 		solAssert(false, message);
@@ -489,8 +491,8 @@ void CompilerContext::appendInlineAssembly(
 			solAssert(m_generatedYulUtilityCode.empty(), "");
 			m_generatedYulUtilityCode = yul::AsmPrinter(dialect)(*obj.code);
 			string code = yul::AsmPrinter{dialect}(*obj.code);
-			scanner = make_shared<langutil::Scanner>(langutil::CharStream(m_generatedYulUtilityCode, _sourceName));
+			langutil::CharStream charStream(m_generatedYulUtilityCode, _sourceName);
-			obj.code = yul::Parser(errorReporter, dialect).parse(scanner, false);
+			obj.code = yul::Parser(errorReporter, dialect).parse(charStream);
 			*obj.analysisInfo = yul::AsmAnalyzer::analyzeStrictAssertCorrect(dialect, obj);
 		}
 

libsolidity/codegen/YulUtilFunctions.cpp

@@ -4029,7 +4029,7 @@ string YulUtilFunctions::negateNumberWrappingFunction(Type const& _type)
 	IntegerType const& type = dynamic_cast<IntegerType const&>(_type);
 	solAssert(type.isSigned(), "Expected signed type!");
 
-	string const functionName = "negate_" + _type.identifier();
+	string const functionName = "negate_wrapping_" + _type.identifier();
 	return m_functionCollector.createFunction(functionName, [&]() {
 		return Whiskers(R"(
 			function <functionName>(value) -> ret {

libsolidity/codegen/ir/Common.cpp

@@ -129,11 +129,12 @@ string IRNames::zeroValue(Type const& _type, string const& _variableName)
 
 string sourceLocationComment(langutil::SourceLocation const& _location, IRGenerationContext const& _context)
 {
+	solAssert(_location.sourceName, "");
 	return "/// @src "
-		+ to_string(_context.sourceIndices().at(_location.source->name()))
+		+ to_string(_context.sourceIndices().at(*_location.sourceName))
 		+ ":"
 		+ to_string(_location.start)
-		+ ","
+		+ ":"
 		+ to_string(_location.end);
 }
 

libsolidity/codegen/ir/IRGenerator.cpp

@@ -33,15 +33,13 @@
 #include <libyul/AssemblyStack.h>
 #include <libyul/Utilities.h>
 
-#include <libsolutil/CommonData.h>
-#include <libsolutil/Whiskers.h>
-#include <libsolutil/StringUtils.h>
 #include <libsolutil/Algorithms.h>
+#include <libsolutil/CommonData.h>
+#include <libsolutil/StringUtils.h>
+#include <libsolutil/Whiskers.h>
 
 #include <liblangutil/SourceReferenceFormatter.h>
 
-#include <range/v3/view/map.hpp>
-
 #include <sstream>
 #include <variant>
 
@@ -101,7 +99,10 @@ pair<string, string> IRGenerator::run(
 	{
 		string errorMessage;
 		for (auto const& error: asmStack.errors())
-			errorMessage += langutil::SourceReferenceFormatter::formatErrorInformation(*error);
+			errorMessage += langutil::SourceReferenceFormatter::formatErrorInformation(
+				*error,
+				asmStack.charStream("")
+			);
 		solAssert(false, ir + "\n\nInvalid IR generated:\n" + errorMessage + "\n");
 	}
 	asmStack.optimize();
@@ -132,6 +133,7 @@ string IRGenerator::generate(
 	};
 
 	Whiskers t(R"(
+		/// @use-src <useSrcMap>
 		object "<CreationObject>" {
 			code {
 				<sourceLocationComment>
@@ -166,6 +168,16 @@ string IRGenerator::generate(
 	for (VariableDeclaration const* var: ContractType(_contract).immutableVariables())
 		m_context.registerImmutableVariable(*var);
 
+	auto invertedSourceIndicies = invertMap(m_context.sourceIndices());
+
+	string useSrcMap = joinHumanReadable(
+		ranges::views::transform(invertedSourceIndicies, [](auto&& _pair) {
+			return to_string(_pair.first) + ":" + escapeAndQuoteString(_pair.second);
+		}),
+		", "
+	);
+
+	t("useSrcMap", useSrcMap);
 	t("sourceLocationComment", sourceLocationComment(_contract, m_context));
 
 	t("CreationObject", IRNames::creationObject(_contract));
@@ -267,8 +279,8 @@ InternalDispatchMap IRGenerator::generateInternalDispatchFunctions(ContractDefin
 		string funName = IRNames::internalDispatch(arity);
 		m_context.functionCollector().createFunction(funName, [&]() {
 			Whiskers templ(R"(
-				function <functionName>(fun<?+in>, <in></+in>) <?+out>-> <out></+out> {
 				<sourceLocationComment>
+				function <functionName>(fun<?+in>, <in></+in>) <?+out>-> <out></+out> {
 					switch fun
 					<#cases>
 					case <funID>
@@ -278,6 +290,7 @@ InternalDispatchMap IRGenerator::generateInternalDispatchFunctions(ContractDefin
 					</cases>
 					default { <panic>() }
 				}
+				<sourceLocationComment>
 			)");
 			templ("sourceLocationComment", sourceLocationComment(_contract, m_context));
 			templ("functionName", funName);
@@ -324,14 +337,19 @@ string IRGenerator::generateFunction(FunctionDefinition const& _function)
 	return m_context.functionCollector().createFunction(functionName, [&]() {
 		m_context.resetLocalVariables();
 		Whiskers t(R"(
-			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 			<sourceLocationComment>
+			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 				<retInit>
 				<body>
 			}
+			<contractSourceLocationComment>
 		)");
 
 		t("sourceLocationComment", sourceLocationComment(_function, m_context));
+		t(
+			"contractSourceLocationComment",
+			sourceLocationComment(m_context.mostDerivedContract(), m_context)
+		);
 
 		t("functionName", functionName);
 		vector<string> params;
@@ -386,12 +404,13 @@ string IRGenerator::generateModifier(
 	return m_context.functionCollector().createFunction(functionName, [&]() {
 		m_context.resetLocalVariables();
 		Whiskers t(R"(
-			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 			<sourceLocationComment>
+			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 				<assignRetParams>
 				<evalArgs>
 				<body>
 			}
+			<contractSourceLocationComment>
 		)");
 		t("functionName", functionName);
 		vector<string> retParamsIn;
@@ -416,6 +435,11 @@ string IRGenerator::generateModifier(
 		);
 		solAssert(modifier, "");
 		t("sourceLocationComment", sourceLocationComment(*modifier, m_context));
+		t(
+			"contractSourceLocationComment",
+			sourceLocationComment(m_context.mostDerivedContract(), m_context)
+		);
+
 		switch (*_modifierInvocation.name().annotation().requiredLookup)
 		{
 		case VirtualLookup::Virtual:
@@ -466,13 +490,18 @@ string IRGenerator::generateFunctionWithModifierInner(FunctionDefinition const&
 	return m_context.functionCollector().createFunction(functionName, [&]() {
 		m_context.resetLocalVariables();
 		Whiskers t(R"(
-			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 			<sourceLocationComment>
+			function <functionName>(<params>)<?+retParams> -> <retParams></+retParams> {
 				<assignRetParams>
 				<body>
 			}
+			<contractSourceLocationComment>
 		)");
 		t("sourceLocationComment", sourceLocationComment(_function, m_context));
+		t(
+			"contractSourceLocationComment",
+			sourceLocationComment(m_context.mostDerivedContract(), m_context)
+		);
 		t("functionName", functionName);
 		vector<string> retParams;
 		vector<string> retParamsIn;
@@ -510,12 +539,17 @@ string IRGenerator::generateGetter(VariableDeclaration const& _varDecl)
 			solAssert(paramTypes.empty(), "");
 			solUnimplementedAssert(type->sizeOnStack() == 1, "");
 			return Whiskers(R"(
-				function <functionName>() -> rval {
 				<sourceLocationComment>
+				function <functionName>() -> rval {
 					rval := loadimmutable("<id>")
 				}
+				<contractSourceLocationComment>
 			)")
 			("sourceLocationComment", sourceLocationComment(_varDecl, m_context))
+			(
+				"contractSourceLocationComment",
+				sourceLocationComment(m_context.mostDerivedContract(), m_context)
+			)
 			("functionName", functionName)
 			("id", to_string(_varDecl.id()))
 			.render();
@@ -524,12 +558,17 @@ string IRGenerator::generateGetter(VariableDeclaration const& _varDecl)
 		{
 			solAssert(paramTypes.empty(), "");
 			return Whiskers(R"(
-				function <functionName>() -> <ret> {
 				<sourceLocationComment>
+				function <functionName>() -> <ret> {
 					<ret> := <constantValueFunction>()
 				}
+				<contractSourceLocationComment>
 			)")
 			("sourceLocationComment", sourceLocationComment(_varDecl, m_context))
+			(
+				"contractSourceLocationComment",
+				sourceLocationComment(m_context.mostDerivedContract(), m_context)
+			)
 			("functionName", functionName)
 			("constantValueFunction", IRGeneratorForStatements(m_context, m_utils).constantValueFunction(_varDecl))
 			("ret", suffixedVariableNameList("ret_", 0, _varDecl.type()->sizeOnStack()))
@@ -641,16 +680,21 @@ string IRGenerator::generateGetter(VariableDeclaration const& _varDecl)
 		}
 
 		return Whiskers(R"(
-			function <functionName>(<params>) -> <retVariables> {
 			<sourceLocationComment>
+			function <functionName>(<params>) -> <retVariables> {
 				<code>
 			}
+			<contractSourceLocationComment>
 		)")
 		("functionName", functionName)
 		("params", joinHumanReadable(parameters))
 		("retVariables", joinHumanReadable(returnVariables))
 		("code", std::move(code))
 		("sourceLocationComment", sourceLocationComment(_varDecl, m_context))
+		(
+			"contractSourceLocationComment",
+			sourceLocationComment(m_context.mostDerivedContract(), m_context)
+		)
 		.render();
 	});
 }
@@ -757,6 +801,7 @@ void IRGenerator::generateConstructors(ContractDefinition const& _contract)
 		m_context.resetLocalVariables();
 		m_context.functionCollector().createFunction(IRNames::constructor(*contract), [&]() {
 			Whiskers t(R"(
+				<sourceLocationComment>
 				function <functionName>(<params><comma><baseParams>) {
 					<evalBaseArguments>
 					<sourceLocationComment>
@@ -764,6 +809,7 @@ void IRGenerator::generateConstructors(ContractDefinition const& _contract)
 					<initStateVariables>
 					<userDefinedConstructorBody>
 				}
+				<contractSourceLocationComment>
 			)");
 			vector<string> params;
 			if (contract->constructor())
@@ -776,6 +822,10 @@ void IRGenerator::generateConstructors(ContractDefinition const& _contract)
 				contract->location(),
 				m_context
 			));
+			t(
+				"contractSourceLocationComment",
+				sourceLocationComment(m_context.mostDerivedContract(), m_context)
+			);
 
 			t("params", joinHumanReadable(params));
 			vector<string> baseParams = listAllParams(baseConstructorParams);

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -3166,5 +3166,5 @@ bool IRGeneratorForStatements::visit(TryCatchClause const& _clause)
 string IRGeneratorForStatements::linkerSymbol(ContractDefinition const& _library) const
 {
 	solAssert(_library.isLibrary(), "");
-	return "linkersymbol(" + util::escapeAndQuoteYulString(_library.fullyQualifiedName()) + ")";
+	return "linkersymbol(" + util::escapeAndQuoteString(_library.fullyQualifiedName()) + ")";
 }

libsolidity/codegen/ir/README.md

@@ -6,5 +6,5 @@ with EVM dialect.
 
 The main semantic differences to the legacy code generator are the following:
 
- - Arithmetic operations cause a failing assertion if the result is not in range.
+- Arithmetic operations cause a failing assertion if the result is not in range.
- - Resizing a storage array to a length larger than 2**64 causes a failing assertion.
+- Resizing a storage array to a length larger than 2**64 causes a failing assertion.

libsolidity/formal/BMC.cpp

@@ -22,6 +22,9 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 
+#include <liblangutil/CharStream.h>
+#include <liblangutil/CharStreamProvider.h>
+
 #ifdef HAVE_Z3_DLOPEN
 #include <z3_version.h>
 #endif
@@ -37,15 +40,15 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers,
+	ModelCheckerSettings const& _settings,
-	ModelCheckerSettings const& _settings
+	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings),
+	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
 	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
-	if (_enabledSolvers.some())
+	if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
 		if (!_smtlib2Responses.empty())
 			m_errorReporter.warning(
 				5622_error,
@@ -57,8 +60,22 @@ BMC::BMC(
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
+void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
 {
+	if (m_interface->solvers() == 0)
+	{
+		if (!m_noSolverWarning)
+		{
+			m_noSolverWarning = true;
+			m_outerErrorReporter.warning(
+				7710_error,
+				SourceLocation(),
+				"BMC analysis was not possible since no SMT solver was found and enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		m_solvedTargets = move(_solvedTargets);
@@ -67,15 +84,31 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 		createFreeConstants(sourceDependencies(_source));
+		m_unprovedAmt = 0;
 
 		_source.accept(*this);
+
+		if (m_unprovedAmt > 0 && !m_settings.showUnproved)
+			m_errorReporter.warning(
+				2788_error,
+				{},
+				"BMC: " +
+				to_string(m_unprovedAmt) +
+				" 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."
+			);
 	}
 
-	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio
-	// guarantees that SmtLib2Interface is the first solver.
+	// guarantees that SmtLib2Interface is the first solver, if enabled.
-	if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
+	if (
+		!m_interface->unhandledQueries().empty() &&
+		m_interface->solvers() == 1 &&
+		m_settings.solvers.smtlib2
+	)
 	{
 		if (!m_noSolverWarning)
 		{
@@ -83,7 +116,8 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			m_outerErrorReporter.warning(
 				8084_error,
 				SourceLocation(),
-				"BMC analysis was not possible since no SMT solver (Z3 or CVC4) was found."
+				"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
+				" None of the installed solvers was enabled."
 #ifdef HAVE_Z3_DLOPEN
 				" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
 #endif
@@ -650,7 +684,12 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
 		if (uf->annotation().type->isValueType())
 		{
 			expressionsToEvaluate.emplace_back(expr(*uf));
-			expressionNames.push_back(uf->location().text());
+			string expressionName;
+			if (uf->location().hasText())
+				expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text(
+					uf->location()
+				);
+			expressionNames.push_back(move(expressionName));
 		}
 
 	return {expressionsToEvaluate, expressionNames};
@@ -907,9 +946,12 @@ void BMC::checkCondition(
 		solAssert(!_callStack.empty(), "");
 		std::ostringstream message;
 		message << "BMC: " << _description << " happens here.";
+
 		std::ostringstream modelMessage;
+		// Sometimes models have complex smtlib2 expressions that SMTLib2Interface fails to parse.
+		if (values.size() == expressionNames.size())
+		{
 			modelMessage << "Counterexample:\n";
-		solAssert(values.size() == expressionNames.size(), "");
 			map<string, string> sortedModel;
 			for (size_t i = 0; i < values.size(); ++i)
 				if (expressionsToEvaluate.at(i).name != values.at(i))
@@ -917,6 +959,7 @@ void BMC::checkCondition(
 
 			for (auto const& eval: sortedModel)
 				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+		}
 
 		m_errorReporter.warning(
 			_errorHappens,
@@ -931,8 +974,12 @@ void BMC::checkCondition(
 	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
 	case smtutil::CheckResult::UNKNOWN:
+	{
+		++m_unprovedAmt;
+		if (m_settings.showUnproved)
 			m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation);
 		break;
+	}
 	case smtutil::CheckResult::CONFLICTING:
 		m_errorReporter.warning(1584_error, _location, "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;

libsolidity/formal/BMC.h

@@ -62,11 +62,11 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers,
+		ModelCheckerSettings const& _settings,
-		ModelCheckerSettings const& _settings
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
-	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);
+	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
@@ -192,7 +192,10 @@ private:
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
 	/// Targets that were already proven.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_solvedTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_solvedTargets;
+
+	/// Number of verification conditions that could not be proved.
+	size_t m_unprovedAmt = 0;
 };
 
 }

libsolidity/formal/CHC.cpp

@@ -56,25 +56,38 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	SMTSolverChoice _enabledSolvers,
+	ModelCheckerSettings const& _settings,
-	ModelCheckerSettings const& _settings
+	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings),
+	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_outerErrorReporter(_errorReporter),
+	m_outerErrorReporter(_errorReporter)
-	m_enabledSolvers(_enabledSolvers)
 {
-	bool usesZ3 = _enabledSolvers.z3;
+	bool usesZ3 = m_settings.solvers.z3;
 #ifdef HAVE_Z3
 	usesZ3 = usesZ3 && Z3Interface::available();
 #else
 	usesZ3 = false;
 #endif
-	if (!usesZ3)
+	if (!usesZ3 && m_settings.solvers.smtlib2)
 		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
 {
+	if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
+	{
+		if (!m_noSolverWarning)
+		{
+			m_noSolverWarning = true;
+			m_outerErrorReporter.warning(
+				7649_error,
+				SourceLocation(),
+				"CHC analysis was not possible since no Horn solver was enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		resetSourceAnalysis();
@@ -91,6 +104,8 @@ void CHC::analyze(SourceUnit const& _source)
 	}
 
 	bool ranSolver = true;
+	// If ranSolver is true here it's because an SMT solver callback was
+	// actually given and the queries were solved.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
 	if (!ranSolver && !m_noSolverWarning)
@@ -102,7 +117,8 @@ void CHC::analyze(SourceUnit const& _source)
 #ifdef HAVE_Z3_DLOPEN
 			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
 #else
-			"CHC analysis was not possible since no integrated z3 SMT solver was found."
+			"CHC analysis was not possible. No Horn solver was available."
+			" None of the installed solvers was enabled."
 #endif
 		);
 	}
@@ -917,6 +933,7 @@ void CHC::resetSourceAnalysis()
 {
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
+	m_unprovedTargets.clear();
 	m_functionTargetIds.clear();
 	m_verificationTargets.clear();
 	m_queryPlaceholders.clear();
@@ -932,7 +949,7 @@ void CHC::resetSourceAnalysis()
 
 	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
+	usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
@@ -1426,6 +1443,8 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 	case CheckResult::SATISFIABLE:
 	{
 #ifdef HAVE_Z3
+		if (m_settings.solvers.z3)
+		{
 			// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
 			// We now disable those optimizations and check whether we can still solve the problem.
 			auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
@@ -1440,6 +1459,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 				cex = move(cexNoOpt);
 
 			spacer->setSpacerOptions(true);
+		}
 #endif
 		break;
 	}
@@ -1575,6 +1595,32 @@ void CHC::checkVerificationTargets()
 		checkedErrorIds.insert(target.errorId);
 	}
 
+	auto toReport = m_unsafeTargets;
+	if (m_settings.showUnproved)
+		for (auto const& [node, targets]: m_unprovedTargets)
+			for (auto const& [target, info]: targets)
+				toReport[node].emplace(target, info);
+
+	for (auto const& [node, targets]: toReport)
+		for (auto const& [target, info]: targets)
+			m_errorReporter.warning(
+				info.error,
+				info.location,
+				info.message
+			);
+
+	if (!m_settings.showUnproved && !m_unprovedTargets.empty())
+		m_errorReporter.warning(
+			5840_error,
+			{},
+			"CHC: " +
+			to_string(m_unprovedTargets.size()) +
+			" 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."
+		);
+
 	// There can be targets in internal functions that are not reachable from the external interface.
 	// These are safe by definition and are not even checked by the CHC engine, but this information
 	// must still be reported safe by the BMC engine.
@@ -1614,27 +1660,26 @@ void CHC::checkAndReportTarget(
 	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
-		m_unsafeTargets[_target.errorNode].insert(_target.type);
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
-			m_errorReporter.warning(
+			m_unsafeTargets[_target.errorNode][_target.type] = {
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
-			);
+			};
 		else
-			m_errorReporter.warning(
+			m_unsafeTargets[_target.errorNode][_target.type] = {
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg
-			);
+			};
 	}
 	else if (!_unknownMsg.empty())
-		m_errorReporter.warning(
+		m_unprovedTargets[_target.errorNode][_target.type] = {
 			_errorReporterId,
 			location,
 			"CHC: " + _unknownMsg
-		);
+		};
 }
 
 /**
@@ -1741,7 +1786,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 				path.emplace_back("State: " + modelMsg);
 		}
 
-		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
+		string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
 
 		list<string> calls;
 		auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
@@ -1753,7 +1798,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 			if (!pred->isConstructorSummary())
 				for (unsigned v: callGraph[node])
 					_dfs(node, v, depth + 1, _dfs);
-			calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node)));
+			calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider));
 			if (pred->isInternalCall())
 				calls.front() += " -- internal call";
 			else if (pred->isExternalCallTrusted())

libsolidity/formal/CHC.h

@@ -39,6 +39,8 @@
 
 #include <libsmtutil/CHCSolverInterface.h>
 
+#include <liblangutil/SourceLocation.h>
+
 #include <boost/algorithm/string/join.hpp>
 
 #include <map>
@@ -56,14 +58,20 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers,
+		ModelCheckerSettings const& _settings,
-		ModelCheckerSettings const& _settings
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
 	void analyze(SourceUnit const& _sources);
 
-	std::map<ASTNode const*, std::set<VerificationTargetType>> const& safeTargets() const { return m_safeTargets; }
+	struct ReportTargetInfo
-	std::map<ASTNode const*, std::set<VerificationTargetType>> const& unsafeTargets() const { return m_unsafeTargets; }
+	{
+		langutil::ErrorId error;
+		langutil::SourceLocation location;
+		std::string message;
+	};
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
 	/// @returns a list of inputs to the Horn solver that were not part of the argument to
@@ -347,10 +355,12 @@ private:
 	/// Helper mapping unique IDs to actual verification targets.
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
-	/// Targets proven safe.
+	/// Targets proved safe.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_safeTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_safeTargets;
-	/// Targets proven unsafe.
+	/// Targets proved unsafe.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_unsafeTargets;
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
+	/// Targets not proved.
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets;
 	//@}
 
 	/// Control-flow.
@@ -392,9 +402,6 @@ private:
 
 	/// ErrorReporter that comes from CompilerStack.
 	langutil::ErrorReporter& m_outerErrorReporter;
-
-	/// SMT solvers that are chosen at runtime.
-	smtutil::SMTSolverChoice m_enabledSolvers;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -32,16 +32,16 @@ using namespace solidity::frontend;
 
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
+	langutil::CharStreamProvider const& _charStreamProvider,
 	map<h256, string> const& _smtlib2Responses,
 	ModelCheckerSettings _settings,
-	ReadCallback::Callback const& _smtCallback,
+	ReadCallback::Callback const& _smtCallback
-	smtutil::SMTSolverChoice _enabledSolvers
 ):
 	m_errorReporter(_errorReporter),
-	m_settings(_settings),
+	m_settings(move(_settings)),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings)
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -120,8 +120,8 @@ void ModelChecker::analyze(SourceUnit const& _source)
 		m_chc.analyze(_source);
 
 	auto solvedTargets = m_chc.safeTargets();
-	for (auto const& target: m_chc.unsafeTargets())
+	for (auto const& [node, targets]: m_chc.unsafeTargets())
-		solvedTargets[target.first] += target.second;
+		solvedTargets[node] += targets | ranges::views::keys;
 
 	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);
@@ -134,7 +134,7 @@ vector<string> ModelChecker::unhandledQueries()
 
 solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
-	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
+	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
 #ifdef HAVE_Z3
 	available.z3 = solidity::smtutil::Z3Interface::available();
 #endif

libsolidity/formal/ModelChecker.h

@@ -49,10 +49,10 @@ public:
 	/// should be used, even if all are available. The default choice is to use all.
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
+		langutil::CharStreamProvider const& _charStreamProvider,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
 		ModelCheckerSettings _settings = ModelCheckerSettings{},
-		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
+		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback()
-		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
 	);
 
 	// TODO This should be removed for 0.9.0.

libsolidity/formal/ModelCheckerSettings.h

@@ -44,6 +44,9 @@ struct ModelCheckerContracts
 		return has(_source) && contracts.at(_source).count(_contract);
 	}
 
+	bool operator!=(ModelCheckerContracts const& _other) const noexcept { return !(*this == _other); }
+	bool operator==(ModelCheckerContracts const& _other) const noexcept { return contracts == _other.contracts; }
+
 	/// Represents which contracts should be analyzed by the SMTChecker
 	/// as the most derived.
 	/// The key is the source file. If the map is empty, all sources must be analyzed.
@@ -79,6 +82,9 @@ struct ModelCheckerEngine
 			return engineMap.at(_engine);
 		return {};
 	}
+
+	bool operator!=(ModelCheckerEngine const& _other) const noexcept { return !(*this == _other); }
+	bool operator==(ModelCheckerEngine const& _other) const noexcept { return bmc == _other.bmc && chc == _other.chc; }
 };
 
 enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
@@ -97,6 +103,9 @@ struct ModelCheckerTargets
 
 	static std::map<std::string, VerificationTargetType> const targetStrings;
 
+	bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); }
+	bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; }
+
 	std::set<VerificationTargetType> targets;
 };
 
@@ -104,8 +113,22 @@ struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
+	bool showUnproved = false;
+	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
 	std::optional<unsigned> timeout;
+
+	bool operator!=(ModelCheckerSettings const& _other) const noexcept { return !(*this == _other); }
+	bool operator==(ModelCheckerSettings const& _other) const noexcept
+	{
+		return
+			contracts == _other.contracts &&
+			engine == _other.engine &&
+			showUnproved == _other.showUnproved &&
+			solvers == _other.solvers &&
+			targets == _other.targets &&
+			timeout == _other.timeout;
+	}
 };
 
 }

libsolidity/formal/Predicate.cpp

@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <liblangutil/CharStreamProvider.h>
+#include <liblangutil/CharStream.h>
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/TypeProvider.h>
 
@@ -196,12 +198,20 @@ bool Predicate::isInterface() const
 	return m_type == PredicateType::Interface;
 }
 
-string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
+string Predicate::formatSummaryCall(
+	vector<smtutil::Expression> const& _args,
+	langutil::CharStreamProvider const& _charStreamProvider
+) const
 {
 	solAssert(isSummary(), "");
 
 	if (auto funCall = programFunctionCall())
-		return funCall->location().text();
+	{
+		if (funCall->location().hasText())
+			return string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location()));
+		else
+			return {};
+	}
 
 	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars to format the function call,

libsolidity/formal/Predicate.h

@@ -27,6 +27,11 @@
 #include <optional>
 #include <vector>
 
+namespace solidity::langutil
+{
+class CharStreamProvider;
+}
+
 namespace solidity::frontend
 {
 
@@ -142,7 +147,10 @@ public:
 
 	/// @returns a formatted string representing a call to this predicate
 	/// with _args.
-	std::string formatSummaryCall(std::vector<smtutil::Expression> const& _args) const;
+	std::string formatSummaryCall(
+		std::vector<smtutil::Expression> const& _args,
+		langutil::CharStreamProvider const& _charStreamProvider
+	) const;
 
 	/// @returns the values of the state variables from _args at the point
 	/// where this summary was reached.

libsolidity/formal/SMTEncoder.cpp

@@ -30,6 +30,8 @@
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
+#include <liblangutil/CharStreamProvider.h>
+
 #include <range/v3/view.hpp>
 
 #include <boost/range/adaptors.hpp>
@@ -45,11 +47,13 @@ using namespace solidity::frontend;
 
 SMTEncoder::SMTEncoder(
 	smt::EncodingContext& _context,
-	ModelCheckerSettings const& _settings
+	ModelCheckerSettings const& _settings,
+	langutil::CharStreamProvider const& _charStreamProvider
 ):
 	m_errorReporter(m_smtErrors),
 	m_context(_context),
-	m_settings(_settings)
+	m_settings(_settings),
+	m_charStreamProvider(_charStreamProvider)
 {
 }
 

libsolidity/formal/SMTEncoder.h

@@ -43,6 +43,7 @@ namespace solidity::langutil
 {
 class ErrorReporter;
 struct SourceLocation;
+class CharStreamProvider;
 }
 
 namespace solidity::frontend
@@ -53,7 +54,8 @@ class SMTEncoder: public ASTConstVisitor
 public:
 	SMTEncoder(
 		smt::EncodingContext& _context,
-		ModelCheckerSettings const& _settings
+		ModelCheckerSettings const& _settings,
+		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
 	/// @returns true if engine should proceed with analysis.
@@ -469,6 +471,10 @@ protected:
 
 	ModelCheckerSettings const& m_settings;
 
+	/// Character stream for each source,
+	/// used for retrieving source text of expressions for e.g. counter-examples.
+	langutil::CharStreamProvider const& m_charStreamProvider;
+
 	smt::SymbolicState& state();
 };
 

libsolidity/interface/CompilerStack.cpp

@@ -80,7 +80,6 @@
 
 #include <utility>
 #include <map>
-#include <range/v3/view/concat.hpp>
 
 #include <boost/algorithm/string/replace.hpp>
 
@@ -96,7 +95,6 @@ static int g_compilerStackCounts = 0;
 
 CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
 	m_readFile{std::move(_readFile)},
-	m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
 	m_errorReporter{m_errorList}
 {
 	// Because TypeProvider is currently a singleton API, we must ensure that
@@ -229,13 +227,6 @@ void CompilerStack::setModelCheckerSettings(ModelCheckerSettings _settings)
 	m_modelCheckerSettings = _settings;
 }
 
-void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
-{
-	if (m_stackState >= ParsedAndImported)
-		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
-	m_enabledSMTSolvers = _enabledSMTSolvers;
-}
-
 void CompilerStack::setLibraries(std::map<std::string, util::h160> const& _libraries)
 {
 	if (m_stackState >= ParsedAndImported)
@@ -300,7 +291,6 @@ void CompilerStack::reset(bool _keepSettings)
 		m_viaIR = false;
 		m_evmVersion = langutil::EVMVersion();
 		m_modelCheckerSettings = ModelCheckerSettings{};
-		m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEwasm = false;
 		m_revertStrings = RevertStrings::Default;
@@ -323,7 +313,7 @@ void CompilerStack::setSources(StringMap _sources)
 	if (m_stackState != Empty)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set sources before parsing."));
 	for (auto source: _sources)
-		m_sources[source.first].scanner = make_shared<Scanner>(CharStream(/*content*/std::move(source.second), /*name*/source.first));
+		m_sources[source.first].charStream = make_unique<CharStream>(/*content*/std::move(source.second), /*name*/source.first);
 	m_stackState = SourcesSet;
 }
 
@@ -346,8 +336,7 @@ bool CompilerStack::parse()
 	{
 		string const& path = sourcesToParse[i];
 		Source& source = m_sources[path];
-		source.scanner->reset();
+		source.ast = parser.parse(*source.charStream);
-		source.ast = parser.parse(source.scanner);
 		if (!source.ast)
 			solAssert(!Error::containsOnlyWarnings(m_errorReporter.errors()), "Parser returned null but did not report error.");
 		else
@@ -358,7 +347,7 @@ bool CompilerStack::parse()
 				{
 					string const& newPath = newSource.first;
 					string const& newContents = newSource.second;
-					m_sources[newPath].scanner = make_shared<Scanner>(CharStream(newContents, newPath));
+					m_sources[newPath].charStream = make_shared<CharStream>(newContents, newPath);
 					sourcesToParse.push_back(newPath);
 				}
 		}
@@ -387,10 +376,11 @@ void CompilerStack::importASTs(map<string, Json::Value> const& _sources)
 		string const& path = src.first;
 		Source source;
 		source.ast = src.second;
-		string srcString = util::jsonCompactPrint(m_sourceJsons[src.first]);
+		source.charStream = make_shared<CharStream>(
-		ASTPointer<Scanner> scanner = make_shared<Scanner>(langutil::CharStream(srcString, src.first));
+			util::jsonCompactPrint(m_sourceJsons[src.first]),
-		source.scanner = scanner;
+			src.first
-		m_sources[path] = source;
+		);
+		m_sources[path] = move(source);
 	}
 	m_stackState = ParsedAndImported;
 	m_importedSources = true;
@@ -556,7 +546,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
 			auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
 			modelChecker.enableAllEnginesIfPragmaPresent(allSources);
 			modelChecker.checkRequestedSourcesAndContracts(allSources);
@@ -764,9 +754,9 @@ Json::Value CompilerStack::generatedSources(string const& _contractName, bool _r
 				unsigned sourceIndex = sourceIndices()[sourceName];
 				ErrorList errors;
 				ErrorReporter errorReporter(errors);
-				auto scanner = make_shared<langutil::Scanner>(langutil::CharStream(source, sourceName));
+				CharStream charStream(source, sourceName);
 				yul::EVMDialect const& dialect = yul::EVMDialect::strictAssemblyForEVM(m_evmVersion);
-				shared_ptr<yul::Block> parserResult = yul::Parser{errorReporter, dialect}.parse(scanner, false);
+				shared_ptr<yul::Block> parserResult = yul::Parser{errorReporter, dialect}.parse(charStream);
 				solAssert(parserResult, "");
 				sources[0]["ast"] = yul::AsmJsonConverter{sourceIndex}(*parserResult);
 				sources[0]["name"] = sourceName;
@@ -1036,12 +1026,14 @@ string const& CompilerStack::metadata(Contract const& _contract) const
 	return _contract.metadata.init([&]{ return createMetadata(_contract); });
 }
 
-Scanner const& CompilerStack::scanner(string const& _sourceName) const
+CharStream const& CompilerStack::charStream(string const& _sourceName) const
 {
 	if (m_stackState < SourcesSet)
 		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("No sources set."));
 
-	return *source(_sourceName).scanner;
+	solAssert(source(_sourceName).charStream, "");
+
+	return *source(_sourceName).charStream;
 }
 
 SourceUnit const& CompilerStack::ast(string const& _sourceName) const
@@ -1083,37 +1075,24 @@ size_t CompilerStack::functionEntryPoint(
 	return 0;
 }
 
-tuple<int, int, int, int> CompilerStack::positionFromSourceLocation(SourceLocation const& _sourceLocation) const
-{
-	int startLine;
-	int startColumn;
-	int endLine;
-	int endColumn;
-	tie(startLine, startColumn) = scanner(_sourceLocation.source->name()).translatePositionToLineColumn(_sourceLocation.start);
-	tie(endLine, endColumn) = scanner(_sourceLocation.source->name()).translatePositionToLineColumn(_sourceLocation.end);
-
-	return make_tuple(++startLine, ++startColumn, ++endLine, ++endColumn);
-}
-
-
 h256 const& CompilerStack::Source::keccak256() const
 {
 	if (keccak256HashCached == h256{})
-		keccak256HashCached = util::keccak256(scanner->source());
+		keccak256HashCached = util::keccak256(charStream->source());
 	return keccak256HashCached;
 }
 
 h256 const& CompilerStack::Source::swarmHash() const
 {
 	if (swarmHashCached == h256{})
-		swarmHashCached = util::bzzr1Hash(scanner->source());
+		swarmHashCached = util::bzzr1Hash(charStream->source());
 	return swarmHashCached;
 }
 
 string const& CompilerStack::Source::ipfsUrl() const
 {
 	if (ipfsUrlCached.empty())
-		ipfsUrlCached = "dweb:/ipfs/" + util::ipfsHashBase58(scanner->source());
+		ipfsUrlCached = "dweb:/ipfs/" + util::ipfsHashBase58(charStream->source());
 	return ipfsUrlCached;
 }
 
@@ -1474,12 +1453,12 @@ string CompilerStack::createMetadata(Contract const& _contract) const
 		if (!referencedSources.count(s.first))
 			continue;
 
-		solAssert(s.second.scanner, "Scanner not available");
+		solAssert(s.second.charStream, "Character stream not available");
 		meta["sources"][s.first]["keccak256"] = "0x" + toHex(s.second.keccak256().asBytes());
 		if (optional<string> licenseString = s.second.ast->licenseString())
 			meta["sources"][s.first]["license"] = *licenseString;
 		if (m_metadataLiteralSources)
-			meta["sources"][s.first]["content"] = s.second.scanner->source();
+			meta["sources"][s.first]["content"] = s.second.charStream->source();
 		else
 		{
 			meta["sources"][s.first]["urls"] = Json::arrayValue;

libsolidity/interface/CompilerStack.h

@@ -38,6 +38,7 @@
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/EVMVersion.h>
 #include <liblangutil/SourceLocation.h>
+#include <liblangutil/CharStreamProvider.h>
 
 #include <libevmasm/LinkerObject.h>
 
@@ -56,7 +57,7 @@
 
 namespace solidity::langutil
 {
-class Scanner;
+class CharStream;
 }
 
 
@@ -87,7 +88,7 @@ class DeclarationContainer;
  * If error recovery is active, it is possible to progress through the stages even when
  * there are errors. In any case, producing code is only possible without errors.
  */
-class CompilerStack
+class CompilerStack: public langutil::CharStreamProvider
 {
 public:
 	/// Noncopyable.
@@ -120,7 +121,7 @@ public:
 	/// and must not emit exceptions.
 	explicit CompilerStack(ReadCallback::Callback _readFile = ReadCallback::Callback());
 
-	~CompilerStack();
+	~CompilerStack() override;
 
 	/// @returns the list of errors that occurred during parsing and type checking.
 	langutil::ErrorList const& errors() const { return m_errorReporter.errors(); }
@@ -174,8 +175,6 @@ public:
 
 	/// Set model checker settings.
 	void setModelCheckerSettings(ModelCheckerSettings _settings);
-	/// Set which SMT solvers should be enabled.
-	void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
 
 	/// Sets the requested contract names by source.
 	/// If empty, no filtering is performed and every contract
@@ -239,8 +238,8 @@ public:
 	/// by sourceNames().
 	std::map<std::string, unsigned> sourceIndices() const;
 
-	/// @returns the previously used scanner, useful for counting lines during error reporting.
+	/// @returns the previously used character stream, useful for counting lines during error reporting.
-	langutil::Scanner const& scanner(std::string const& _sourceName) const;
+	langutil::CharStream const& charStream(std::string const& _sourceName) const override;
 
 	/// @returns the parsed source unit with the supplied name.
 	SourceUnit const& ast(std::string const& _sourceName) const;
@@ -249,11 +248,6 @@ public:
 	/// does not exist.
 	ContractDefinition const& contractDefinition(std::string const& _contractName) const;
 
-	/// Helper function for logs printing. Do only use in error cases, it's quite expensive.
-	/// line and columns are numbered starting from 1 with following order:
-	/// start line, start column, end line, end column
-	std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const;
-
 	/// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run
 	/// by calling @a addSMTLib2Response).
 	std::vector<std::string> const& unhandledSMTLib2Queries() const { return m_unhandledSMTLib2Queries; }
@@ -349,7 +343,7 @@ private:
 	/// The state per source unit. Filled gradually during parsing.
 	struct Source
 	{
-		std::shared_ptr<langutil::Scanner> scanner;
+		std::shared_ptr<langutil::CharStream> charStream;
 		std::shared_ptr<SourceUnit> ast;
 		util::h256 mutable keccak256HashCached;
 		util::h256 mutable swarmHashCached;
@@ -483,7 +477,6 @@ private:
 	bool m_viaIR = false;
 	langutil::EVMVersion m_evmVersion;
 	ModelCheckerSettings m_modelCheckerSettings;
-	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateEvmBytecode = true;
 	bool m_generateIR = false;

libsolidity/interface/ImportRemapper.h

@@ -35,6 +35,15 @@ class ImportRemapper
 public:
 	struct Remapping
 	{
+		bool operator!=(Remapping const& _other) const noexcept { return !(*this == _other); }
+		bool operator==(Remapping const& _other) const noexcept
+		{
+			return
+				context == _other.context &&
+				prefix == _other.prefix &&
+				target == _other.target;
+		}
+
 		std::string context;
 		std::string prefix;
 		std::string target;

libsolidity/interface/StandardCompiler.cpp

@@ -83,9 +83,9 @@ Json::Value formatFatalError(string const& _type, string const& _message)
 Json::Value formatSourceLocation(SourceLocation const* location)
 {
 	Json::Value sourceLocation;
-	if (location && location->source && !location->source->name().empty())
+	if (location && location->sourceName)
 	{
-		sourceLocation["file"] = location->source->name();
+		sourceLocation["file"] = *location->sourceName;
 		sourceLocation["start"] = location->start;
 		sourceLocation["end"] = location->end;
 	}
@@ -109,6 +109,7 @@ Json::Value formatSecondarySourceLocation(SecondarySourceLocation const* _second
 }
 
 Json::Value formatErrorWithException(
+	CharStreamProvider const& _charStreamProvider,
 	util::Exception const& _exception,
 	bool const& _warning,
 	string const& _type,
@@ -119,7 +120,11 @@ Json::Value formatErrorWithException(
 {
 	string message;
 	// TODO: consider enabling color
-	string formattedMessage = SourceReferenceFormatter::formatExceptionInformation(_exception, _type);
+	string formattedMessage = SourceReferenceFormatter::formatExceptionInformation(
+		_exception,
+		_type,
+		_charStreamProvider
+	);
 
 	if (string const* description = boost::get_error_info<util::errinfo_comment>(_exception))
 		message = ((_message.length() > 0) ? (_message + ":") : "") + *description;
@@ -437,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", "targets", "timeout"};
+	static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -946,6 +951,32 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("showUnproved"))
+	{
+		auto const& showUnproved = modelCheckerSettings["showUnproved"];
+		if (!showUnproved.isBool())
+			return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
+		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
+	}
+
+	if (modelCheckerSettings.isMember("solvers"))
+	{
+		auto const& solversArray = modelCheckerSettings["solvers"];
+		if (!solversArray.isArray())
+			return formatFatalError("JSONError", "settings.modelChecker.solvers must be an array.");
+
+		smtutil::SMTSolverChoice solvers;
+		for (auto const& s: solversArray)
+		{
+			if (!s.isString())
+				return formatFatalError("JSONError", "Every target in settings.modelChecker.solvers must be a string.");
+			if (!solvers.setSolver(s.asString()))
+				return formatFatalError("JSONError", "Invalid model checker solvers requested.");
+		}
+
+		ret.modelCheckerSettings.solvers = solvers;
+	}
+
 	if (modelCheckerSettings.isMember("targets"))
 	{
 		auto const& targetsArray = modelCheckerSettings["targets"];
@@ -1017,6 +1048,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 			Error const& err = dynamic_cast<Error const&>(*error);
 
 			errors.append(formatErrorWithException(
+				compilerStack,
 				*error,
 				err.type() == Error::Type::Warning,
 				err.typeName(),
@@ -1030,6 +1062,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (Error const& _error)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_error,
 			false,
 			_error.typeName(),
@@ -1050,6 +1083,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (CompilerError const& _exception)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_exception,
 			false,
 			"CompilerError",
@@ -1060,6 +1094,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (InternalCompilerError const& _exception)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_exception,
 			false,
 			"InternalCompilerError",
@@ -1070,6 +1105,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (UnimplementedFeatureError const& _exception)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_exception,
 			false,
 			"UnimplementedFeatureError",
@@ -1080,6 +1116,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (yul::YulException const& _exception)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_exception,
 			false,
 			"YulException",
@@ -1090,6 +1127,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 	catch (smtutil::SMTLogicError const& _exception)
 	{
 		errors.append(formatErrorWithException(
+			compilerStack,
 			_exception,
 			false,
 			"SMTLogicException",
@@ -1297,6 +1335,7 @@ Json::Value StandardCompiler::compileYul(InputsAndSettings _inputsAndSettings)
 			auto err = dynamic_pointer_cast<Error const>(error);
 
 			errors.append(formatErrorWithException(
+				stack,
 				*error,
 				err->type() == Error::Type::Warning,
 				err->typeName(),
@@ -1407,7 +1446,7 @@ string StandardCompiler::compile(string const& _input) noexcept
 	try
 	{
 		if (!util::jsonParseStrict(_input, input, &errors))
-			return util::jsonCompactPrint(formatFatalError("JSONError", errors));
+			return util::jsonPrint(formatFatalError("JSONError", errors), m_jsonPrintingFormat);
 	}
 	catch (...)
 	{
@@ -1420,7 +1459,7 @@ string StandardCompiler::compile(string const& _input) noexcept
 
 	try
 	{
-		return util::jsonCompactPrint(output);
+		return util::jsonPrint(output, m_jsonPrintingFormat);
 	}
 	catch (...)
 	{

libsolidity/interface/StandardCompiler.h

@@ -24,6 +24,7 @@
 #pragma once
 
 #include <libsolidity/interface/CompilerStack.h>
+#include <libsolutil/JSON.h>
 
 #include <optional>
 #include <utility>
@@ -46,8 +47,10 @@ public:
 	/// Creates a new StandardCompiler.
 	/// @param _readFile callback used to read files for import statements. Must return
 	/// and must not emit exceptions.
-	explicit StandardCompiler(ReadCallback::Callback _readFile = ReadCallback::Callback()):
+	explicit StandardCompiler(ReadCallback::Callback _readFile = ReadCallback::Callback(),
-		m_readFile(std::move(_readFile))
+		util::JsonFormat const& _format = {}):
+		m_readFile(std::move(_readFile)),
+		m_jsonPrintingFormat(std::move(_format))
 	{
 	}
 
@@ -91,6 +94,8 @@ private:
 	Json::Value compileYul(InputsAndSettings _inputsAndSettings);
 
 	ReadCallback::Callback m_readFile;
+
+	util::JsonFormat m_jsonPrintingFormat;
 };
 
 }

libsolidity/parsing/Parser.cpp

@@ -50,7 +50,12 @@ class Parser::ASTNodeFactory
 {
 public:
 	explicit ASTNodeFactory(Parser& _parser):
-		m_parser(_parser), m_location{_parser.currentLocation().start, -1, _parser.currentLocation().source} {}
+		m_parser(_parser), m_location{
+			_parser.currentLocation().start,
+			-1,
+			_parser.currentLocation().sourceName
+		}
+	{}
 	ASTNodeFactory(Parser& _parser, ASTPointer<ASTNode> const& _childNode):
 		m_parser(_parser), m_location{_childNode->location()} {}
 
@@ -63,7 +68,7 @@ public:
 	template <class NodeType, typename... Args>
 	ASTPointer<NodeType> createNode(Args&& ... _args)
 	{
-		solAssert(m_location.source, "");
+		solAssert(m_location.sourceName, "");
 		if (m_location.end < 0)
 			markEndPosition();
 		return make_shared<NodeType>(m_parser.nextID(), m_location, std::forward<Args>(_args)...);
@@ -76,13 +81,13 @@ private:
 	SourceLocation m_location;
 };
 
-ASTPointer<SourceUnit> Parser::parse(shared_ptr<Scanner> const& _scanner)
+ASTPointer<SourceUnit> Parser::parse(CharStream& _charStream)
 {
 	solAssert(!m_insideModifier, "");
 	try
 	{
 		m_recursionDepth = 0;
-		m_scanner = _scanner;
+		m_scanner = make_shared<Scanner>(_charStream);
 		ASTNodeFactory nodeFactory(*this);
 
 		vector<ASTPointer<ASTNode>> nodes;
@@ -1284,7 +1289,7 @@ ASTPointer<InlineAssembly> Parser::parseInlineAssembly(ASTPointer<ASTString> con
 	}
 
 	yul::Parser asmParser(m_errorReporter, dialect);
-	shared_ptr<yul::Block> block = asmParser.parse(m_scanner, true);
+	shared_ptr<yul::Block> block = asmParser.parseInline(m_scanner);
 	if (block == nullptr)
 		BOOST_THROW_EXCEPTION(FatalError());
 
@@ -2045,9 +2050,9 @@ optional<string> Parser::findLicenseString(std::vector<ASTPointer<ASTNode>> cons
 
 	// Search inside all parts of the source not covered by parsed nodes.
 	// This will leave e.g. "global comments".
-	string const& source = m_scanner->source();
+	using iter = std::string::const_iterator;
-	using iter = decltype(source.begin());
 	vector<pair<iter, iter>> sequencesToSearch;
+	string const& source = m_scanner->charStream().source();
 	sequencesToSearch.emplace_back(source.begin(), source.end());
 	for (ASTPointer<ASTNode> const& node: _nodes)
 		if (node->location().hasText())
@@ -2073,7 +2078,7 @@ optional<string> Parser::findLicenseString(std::vector<ASTPointer<ASTNode>> cons
 	else if (matches.empty())
 		parserWarning(
 			1878_error,
-			{-1, -1, m_scanner->charStream()},
+			{-1, -1, m_scanner->currentLocation().sourceName},
 			"SPDX license identifier not provided in source file. "
 			"Before publishing, consider adding a comment containing "
 			"\"SPDX-License-Identifier: <SPDX-License>\" to each source file. "
@@ -2083,7 +2088,7 @@ optional<string> Parser::findLicenseString(std::vector<ASTPointer<ASTNode>> cons
 	else
 		parserError(
 			3716_error,
-			{-1, -1, m_scanner->charStream()},
+			{-1, -1, m_scanner->currentLocation().sourceName},
 			"Multiple SPDX license identifiers found in source file. "
 			"Use \"AND\" or \"OR\" to combine multiple licenses. "
 			"Please see https://spdx.org for more information."

libsolidity/parsing/Parser.h

@@ -29,7 +29,7 @@
 
 namespace solidity::langutil
 {
-class Scanner;
+class CharStream;
 }
 
 namespace solidity::frontend
@@ -47,7 +47,7 @@ public:
 		m_evmVersion(_evmVersion)
 	{}
 
-	ASTPointer<SourceUnit> parse(std::shared_ptr<langutil::Scanner> const& _scanner);
+	ASTPointer<SourceUnit> parse(langutil::CharStream& _charStream);
 
 private:
 	class ASTNodeFactory;

libsolutil/CommonData.cpp

@@ -192,13 +192,11 @@ string solidity::util::formatAsStringOrNumber(string const& _value)
 		if (c <= 0x1f || c >= 0x7f || c == '"')
 			return "0x" + h256(_value, h256::AlignLeft).hex();
 
-	// The difference in escaping is only in characters below 0x1f and the string does not have them
+	return escapeAndQuoteString(_value);
-	// so this will work for Solidity strings too.
-	return escapeAndQuoteYulString(_value);
 }
 
 
-string solidity::util::escapeAndQuoteYulString(string const& _input)
+string solidity::util::escapeAndQuoteString(string const& _input)
 {
 	string out;
 

libsolutil/CommonData.h

@@ -552,9 +552,9 @@ bool isValidDecimal(std::string const& _string);
 /// _value cannot be longer than 32 bytes.
 std::string formatAsStringOrNumber(std::string const& _value);
 
-/// @returns a string with the usual backslash-escapes for non-ASCII
+/// @returns a string with the usual backslash-escapes for non-printable and non-ASCII
 /// characters and surrounded by '"'-characters.
-std::string escapeAndQuoteYulString(std::string const& _input);
+std::string escapeAndQuoteString(std::string const& _input);
 
 template<typename Container, typename Compare>
 bool containerEqual(Container const& _lhs, Container const& _rhs, Compare&& _compare)

libsolutil/JSON.cpp

@@ -115,18 +115,29 @@ Json::Value removeNullMembers(Json::Value _json)
 
 string jsonPrettyPrint(Json::Value const& _input)
 {
-	static map<string, Json::Value> settings{{"indentation", "  "}, {"enableYAMLCompatibility", true}};
+	return jsonPrint(_input, JsonFormat{ JsonFormat::Pretty });
-	static StreamWriterBuilder writerBuilder(settings);
-	string result = print(_input, writerBuilder);
-	boost::replace_all(result, " \n", "\n");
-	return result;
 }
 
 string jsonCompactPrint(Json::Value const& _input)
 {
-	static map<string, Json::Value> settings{{"indentation", ""}};
+	return jsonPrint(_input, JsonFormat{ JsonFormat::Compact });
-	static StreamWriterBuilder writerBuilder(settings);
+}
-	return print(_input, writerBuilder);
+
+string jsonPrint(Json::Value const& _input, JsonFormat const& _format)
+{
+	map<string, Json::Value> settings;
+	if (_format.format == JsonFormat::Pretty)
+	{
+		settings["indentation"] = string(_format.indent, ' ');
+		settings["enableYAMLCompatibility"] = true;
+	}
+	else
+		settings["indentation"] = "";
+	StreamWriterBuilder writerBuilder(settings);
+	string result = print(_input, writerBuilder);
+	if (_format.format == JsonFormat::Pretty)
+		boost::replace_all(result, " \n", "\n");
+	return result;
 }
 
 bool jsonParseStrict(string const& _input, Json::Value& _json, string* _errs /* = nullptr */)

libsolutil/JSON.h

@@ -33,12 +33,33 @@ namespace solidity::util
 /// Removes members with null value recursively from (@a _json).
 Json::Value removeNullMembers(Json::Value _json);
 
+/// JSON printing format.
+struct JsonFormat
+{
+	enum Format
+	{
+		Compact,
+		Pretty
+	};
+
+	static constexpr uint32_t defaultIndent = 2;
+
+	bool operator==(JsonFormat const& _other) const noexcept { return (format == _other.format) && (indent == _other.indent); }
+	bool operator!=(JsonFormat const& _other) const noexcept { return !(*this == _other); }
+
+	Format format = Compact;
+	uint32_t indent = defaultIndent;
+};
+
 /// Serialise the JSON object (@a _input) with indentation
 std::string jsonPrettyPrint(Json::Value const& _input);
 
 /// Serialise the JSON object (@a _input) without indentation
 std::string jsonCompactPrint(Json::Value const& _input);
 
+/// Serialise the JSON object (@a _input) using specified format (@a _format)
+std::string jsonPrint(Json::Value const& _input, JsonFormat const& _format);
+
 /// Parse a JSON string (@a _input) with enabled strict-mode and writes resulting JSON object to (@a _json)
 /// \param _input JSON input string
 /// \param _json [out] resulting JSON object

libsolutil/StringUtils.h

@@ -177,4 +177,22 @@ inline std::string formatNumberReadable(
 	return str;
 }
 
+/// Safely converts an usigned integer as string into an unsigned int type.
+///
+/// @return the converted number or nullopt in case of an failure (including if it would not fit).
+inline std::optional<unsigned> toUnsignedInt(std::string const& _value)
+{
+	try
+	{
+		auto const ulong = stoul(_value);
+		if (ulong > std::numeric_limits<unsigned>::max())
+			return std::nullopt;
+		return static_cast<unsigned>(ulong);
+	}
+	catch (...)
+	{
+		return std::nullopt;
+	}
+}
+
 }

libsolutil/cxx20.h

@@ -49,4 +49,15 @@ erase_if(std::unordered_map<Key, T, Hash, KeyEqual, Alloc>& _c, Pred _pred)
 	return old_size - _c.size();
 }
 
+// Taken from https://en.cppreference.com/w/cpp/container/vector/erase2
+template<class T, class Alloc, class Pred>
+constexpr typename std::vector<T, Alloc>::size_type
+erase_if(std::vector<T, Alloc>& c, Pred pred)
+{
+	auto it = std::remove_if(c.begin(), c.end(), pred);
+	auto r = std::distance(it, c.end());
+	c.erase(it, c.end());
+	return static_cast<typename std::vector<T, Alloc>::size_type>(r);
+}
+
 }

libyul/AsmJsonImporter.cpp

@@ -26,6 +26,7 @@
 #include <libyul/AST.h>
 #include <libyul/Exceptions.h>
 
+#include <liblangutil/Exceptions.h>
 #include <liblangutil/Scanner.h>
 
 #include <boost/algorithm/string/split.hpp>
@@ -45,7 +46,7 @@ SourceLocation const AsmJsonImporter::createSourceLocation(Json::Value const& _n
 {
 	yulAssert(member(_node, "src").isString(), "'src' must be a string");
 
-	return solidity::langutil::parseSourceLocation(_node["src"].asString(), m_sourceName);
+	return solidity::langutil::parseSourceLocation(_node["src"].asString(), m_sourceNames);
 }
 
 template <class T>
@@ -53,10 +54,7 @@ T AsmJsonImporter::createAsmNode(Json::Value const& _node)
 {
 	T r;
 	SourceLocation location = createSourceLocation(_node);
-	yulAssert(
+	yulAssert(location.hasText(), "Invalid source location in Asm AST");
-		location.source && 0 <= location.start && location.start <= location.end,
-		"Invalid source location in Asm AST"
-	);
 	r.debugData = DebugData::create(location);
 	return r;
 }
@@ -168,7 +166,8 @@ Literal AsmJsonImporter::createLiteral(Json::Value const& _node)
 
 	if (kind == "number")
 	{
-		langutil::Scanner scanner{langutil::CharStream(lit.value.str(), "")};
+		langutil::CharStream charStream(lit.value.str(), "");
+		langutil::Scanner scanner{charStream};
 		lit.kind = LiteralKind::Number;
 		yulAssert(
 			scanner.currentToken() == Token::Number,
@@ -177,7 +176,8 @@ Literal AsmJsonImporter::createLiteral(Json::Value const& _node)
 	}
 	else if (kind == "bool")
 	{
-		langutil::Scanner scanner{langutil::CharStream(lit.value.str(), "")};
+		langutil::CharStream charStream(lit.value.str(), "");
+		langutil::Scanner scanner{charStream};
 		lit.kind = LiteralKind::Boolean;
 		yulAssert(
 			scanner.currentToken() == Token::TrueLiteral ||

libyul/AsmJsonImporter.h

@@ -38,7 +38,9 @@ namespace solidity::yul
 class AsmJsonImporter
 {
 public:
-	explicit AsmJsonImporter(std::string _sourceName) : m_sourceName(std::move(_sourceName)) {}
+	explicit AsmJsonImporter(std::vector<std::shared_ptr<std::string const>> const& _sourceNames):
+		m_sourceNames(_sourceNames)
+	{}
 	yul::Block createBlock(Json::Value const& _node);
 
 private:
@@ -70,8 +72,7 @@ private:
 	yul::Break createBreak(Json::Value const& _node);
 	yul::Continue createContinue(Json::Value const& _node);
 
-	std::string m_sourceName;
+	std::vector<std::shared_ptr<std::string const>> const& m_sourceNames;
-
 };
 
 }

libyul/AsmParser.cpp

@@ -24,14 +24,18 @@
 #include <libyul/AST.h>
 #include <libyul/AsmParser.h>
 #include <libyul/Exceptions.h>
-#include <liblangutil/Scanner.h>
 #include <liblangutil/ErrorReporter.h>
+#include <liblangutil/Exceptions.h>
+#include <liblangutil/Scanner.h>
 #include <libsolutil/Common.h>
 #include <libsolutil/Visitor.h>
 
+#include <range/v3/view/subrange.hpp>
+
 #include <boost/algorithm/string.hpp>
 
 #include <algorithm>
+#include <regex>
 
 using namespace std;
 using namespace solidity;
@@ -53,9 +57,43 @@ shared_ptr<DebugData const> updateLocationEndFrom(
 	return make_shared<DebugData const>(updatedLocation);
 }
 
+optional<int> toInt(string const& _value)
+{
+	try
+	{
+		return stoi(_value);
+	}
+	catch (...)
+	{
+		return nullopt;
+	}
 }
 
-unique_ptr<Block> Parser::parse(std::shared_ptr<Scanner> const& _scanner, bool _reuseScanner)
+}
+
+std::shared_ptr<DebugData const> Parser::createDebugData() const
+{
+	switch (m_useSourceLocationFrom)
+	{
+		case UseSourceLocationFrom::Scanner:
+			return DebugData::create(ParserBase::currentLocation());
+		case UseSourceLocationFrom::LocationOverride:
+			return DebugData::create(m_locationOverride);
+		case UseSourceLocationFrom::Comments:
+			return m_debugDataOverride;
+	}
+	solAssert(false, "");
+}
+
+unique_ptr<Block> Parser::parse(CharStream& _charStream)
+{
+	m_scanner = make_shared<Scanner>(_charStream);
+	unique_ptr<Block> block = parseInline(m_scanner);
+	expectToken(Token::EOS);
+	return block;
+}
+
+unique_ptr<Block> Parser::parseInline(std::shared_ptr<Scanner> const& _scanner)
 {
 	m_recursionDepth = 0;
 
@@ -65,10 +103,9 @@ unique_ptr<Block> Parser::parse(std::shared_ptr<Scanner> const& _scanner, bool _
 	try
 	{
 		m_scanner = _scanner;
-		auto block = make_unique<Block>(parseBlock());
+		if (m_sourceNames)
-		if (!_reuseScanner)
+			fetchSourceLocationFromComment();
-			expectToken(Token::EOS);
+		return make_unique<Block>(parseBlock());
-		return block;
 	}
 	catch (FatalError const&)
 	{
@@ -78,6 +115,55 @@ unique_ptr<Block> Parser::parse(std::shared_ptr<Scanner> const& _scanner, bool _
 	return nullptr;
 }
 
+langutil::Token Parser::advance()
+{
+	auto const token = ParserBase::advance();
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Comments)
+		fetchSourceLocationFromComment();
+	return token;
+}
+
+void Parser::fetchSourceLocationFromComment()
+{
+	solAssert(m_sourceNames.has_value(), "");
+
+	if (m_scanner->currentCommentLiteral().empty())
+		return;
+
+	static regex const lineRE = std::regex(
+		R"~~~((^|\s*)@src\s+(-1|\d+):(-1|\d+):(-1|\d+)(\s+|$))~~~",
+		std::regex_constants::ECMAScript | std::regex_constants::optimize
+	);
+
+	string const text = m_scanner->currentCommentLiteral();
+	auto from = sregex_iterator(text.begin(), text.end(), lineRE);
+	auto to = sregex_iterator();
+
+	for (auto const& matchResult: ranges::make_subrange(from, to))
+	{
+		solAssert(matchResult.size() == 6, "");
+
+		auto const sourceIndex = toInt(matchResult[2].str());
+		auto const start = toInt(matchResult[3].str());
+		auto const end = toInt(matchResult[4].str());
+
+		auto const commentLocation = m_scanner->currentCommentLocation();
+		m_debugDataOverride = DebugData::create();
+		if (!sourceIndex || !start || !end)
+			m_errorReporter.syntaxError(6367_error, commentLocation, "Invalid value in source location mapping. Could not parse location specification.");
+		else if (sourceIndex == -1)
+			m_debugDataOverride = DebugData::create(SourceLocation{*start, *end, nullptr});
+		else if (!(sourceIndex >= 0 && m_sourceNames->count(static_cast<unsigned>(*sourceIndex))))
+			m_errorReporter.syntaxError(2674_error, commentLocation, "Invalid source mapping. Source index not defined via @use-src.");
+		else
+		{
+			shared_ptr<string const> sourceName = m_sourceNames->at(static_cast<unsigned>(*sourceIndex));
+			solAssert(sourceName, "");
+			m_debugDataOverride = DebugData::create(SourceLocation{*start, *end, move(sourceName)});
+		}
+	}
+}
+
 Block Parser::parseBlock()
 {
 	RecursionGuard recursionGuard(*this);
@@ -85,6 +171,7 @@ Block Parser::parseBlock()
 	expectToken(Token::LBrace);
 	while (currentToken() != Token::RBrace)
 		block.statements.emplace_back(parseStatement());
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		block.debugData = updateLocationEndFrom(block.debugData, currentLocation());
 	advance();
 	return block;
@@ -107,6 +194,8 @@ Statement Parser::parseStatement()
 		advance();
 		_if.condition = make_unique<Expression>(parseExpression());
 		_if.body = parseBlock();
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
+			_if.debugData = updateLocationEndFrom(_if.debugData, _if.body.debugData->location);
 		return Statement{move(_if)};
 	}
 	case Token::Switch:
@@ -124,6 +213,7 @@ Statement Parser::parseStatement()
 			fatalParserError(4904_error, "Case not allowed after default case.");
 		if (_switch.cases.empty())
 			fatalParserError(2418_error, "Switch statement without any cases.");
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 			_switch.debugData = updateLocationEndFrom(_switch.debugData, _switch.cases.back().body.debugData->location);
 		return Statement{move(_switch)};
 	}
@@ -206,6 +296,7 @@ Statement Parser::parseStatement()
 		expectToken(Token::AssemblyAssign);
 
 		assignment.value = make_unique<Expression>(parseExpression());
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 			assignment.debugData = updateLocationEndFrom(assignment.debugData, locationOf(*assignment.value));
 
 		return Statement{move(assignment)};
@@ -236,6 +327,7 @@ Case Parser::parseCase()
 	else
 		yulAssert(false, "Case or default case expected.");
 	_case.body = parseBlock();
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		_case.debugData = updateLocationEndFrom(_case.debugData, _case.body.debugData->location);
 	return _case;
 }
@@ -256,6 +348,7 @@ ForLoop Parser::parseForLoop()
 	forLoop.post = parseBlock();
 	m_currentForLoopComponent = ForLoopComponent::ForLoopBody;
 	forLoop.body = parseBlock();
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		forLoop.debugData = updateLocationEndFrom(forLoop.debugData, forLoop.body.debugData->location);
 
 	m_currentForLoopComponent = outerForLoopComponent;
@@ -295,7 +388,7 @@ variant<Literal, Identifier> Parser::parseLiteralOrIdentifier()
 	{
 	case Token::Identifier:
 	{
-		Identifier identifier{DebugData::create(currentLocation()), YulString{currentLiteral()}};
+		Identifier identifier{createDebugData(), YulString{currentLiteral()}};
 		advance();
 		return identifier;
 	}
@@ -326,7 +419,7 @@ variant<Literal, Identifier> Parser::parseLiteralOrIdentifier()
 		}
 
 		Literal literal{
-			DebugData::create(currentLocation()),
+			createDebugData(),
 			kind,
 			YulString{currentLiteral()},
 			kind == LiteralKind::Boolean ? m_dialect.boolType : m_dialect.defaultType
@@ -335,6 +428,7 @@ variant<Literal, Identifier> Parser::parseLiteralOrIdentifier()
 		if (currentToken() == Token::Colon)
 		{
 			expectToken(Token::Colon);
+			if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 				literal.debugData = updateLocationEndFrom(literal.debugData, currentLocation());
 			literal.type = expectAsmIdentifier();
 		}
@@ -367,9 +461,10 @@ VariableDeclaration Parser::parseVariableDeclaration()
 	{
 		expectToken(Token::AssemblyAssign);
 		varDecl.value = make_unique<Expression>(parseExpression());
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 			varDecl.debugData = updateLocationEndFrom(varDecl.debugData, locationOf(*varDecl.value));
 	}
-	else
+	else if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		varDecl.debugData = updateLocationEndFrom(varDecl.debugData, varDecl.variables.back().debugData->location);
 
 	return varDecl;
@@ -416,6 +511,7 @@ FunctionDefinition Parser::parseFunctionDefinition()
 	m_insideFunction = true;
 	funDef.body = parseBlock();
 	m_insideFunction = preInsideFunction;
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		funDef.debugData = updateLocationEndFrom(funDef.debugData, funDef.body.debugData->location);
 
 	m_currentForLoopComponent = outerForLoopComponent;
@@ -443,6 +539,7 @@ FunctionCall Parser::parseCall(variant<Literal, Identifier>&& _initialOp)
 			ret.arguments.emplace_back(parseExpression());
 		}
 	}
+	if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 		ret.debugData = updateLocationEndFrom(ret.debugData, currentLocation());
 	expectToken(Token::RParen);
 	return ret;
@@ -456,6 +553,7 @@ TypedName Parser::parseTypedName()
 	if (currentToken() == Token::Colon)
 	{
 		expectToken(Token::Colon);
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
 			typedName.debugData = updateLocationEndFrom(typedName.debugData, currentLocation());
 		typedName.type = expectAsmIdentifier();
 	}

libyul/AsmParser.h

@@ -23,6 +23,7 @@
 
 #pragma once
 
+#include <libyul/AST.h>
 #include <libyul/ASTForward.h>
 #include <libyul/Dialect.h>
 
@@ -30,6 +31,7 @@
 #include <liblangutil/Scanner.h>
 #include <liblangutil/ParserBase.h>
 
+#include <map>
 #include <memory>
 #include <variant>
 #include <vector>
@@ -45,6 +47,11 @@ public:
 		None, ForLoopPre, ForLoopPost, ForLoopBody
 	};
 
+	enum class UseSourceLocationFrom
+	{
+		Scanner, LocationOverride, Comments,
+	};
+
 	explicit Parser(
 		langutil::ErrorReporter& _errorReporter,
 		Dialect const& _dialect,
@@ -52,25 +59,62 @@ public:
 	):
 		ParserBase(_errorReporter),
 		m_dialect(_dialect),
-		m_locationOverride(std::move(_locationOverride))
+		m_locationOverride{_locationOverride ? *_locationOverride : langutil::SourceLocation{}},
+		m_debugDataOverride{},
+		m_useSourceLocationFrom{
+			_locationOverride ?
+			UseSourceLocationFrom::LocationOverride :
+			UseSourceLocationFrom::Scanner
+		}
+	{}
+
+	/// Constructs a Yul parser that is using the source locations
+	/// from the comments (via @src).
+	explicit Parser(
+		langutil::ErrorReporter& _errorReporter,
+		Dialect const& _dialect,
+		std::optional<std::map<unsigned, std::shared_ptr<std::string const>>> _sourceNames
+	):
+		ParserBase(_errorReporter),
+		m_dialect(_dialect),
+		m_sourceNames{std::move(_sourceNames)},
+		m_debugDataOverride{DebugData::create()},
+		m_useSourceLocationFrom{
+			m_sourceNames.has_value() ?
+			UseSourceLocationFrom::Comments :
+			UseSourceLocationFrom::Scanner
+		}
 	{}
 
 	/// Parses an inline assembly block starting with `{` and ending with `}`.
-	/// @param _reuseScanner if true, do check for end of input after the `}`.
 	/// @returns an empty shared pointer on error.
-	std::unique_ptr<Block> parse(std::shared_ptr<langutil::Scanner> const& _scanner, bool _reuseScanner);
+	std::unique_ptr<Block> parseInline(std::shared_ptr<langutil::Scanner> const& _scanner);
+
+	/// Parses an assembly block starting with `{` and ending with `}`
+	/// and expects end of input after the '}'.
+	/// @returns an empty shared pointer on error.
+	std::unique_ptr<Block> parse(langutil::CharStream& _charStream);
 
 protected:
 	langutil::SourceLocation currentLocation() const override
 	{
-		return m_locationOverride ? *m_locationOverride : ParserBase::currentLocation();
+		if (m_useSourceLocationFrom == UseSourceLocationFrom::Scanner)
+			return ParserBase::currentLocation();
+		return m_locationOverride;
 	}
 
+	langutil::Token advance() override;
+
+	void fetchSourceLocationFromComment();
+
+	/// Creates a DebugData object with the correct source location set.
+	std::shared_ptr<DebugData const> createDebugData() const;
+
 	/// Creates an inline assembly node with the current source location.
 	template <class T> T createWithLocation() const
 	{
 		T r;
-		r.debugData = DebugData::create(currentLocation());
+		r.debugData = createDebugData();
 		return r;
 	}
 
@@ -96,7 +140,11 @@ protected:
 
 private:
 	Dialect const& m_dialect;
-	std::optional<langutil::SourceLocation> m_locationOverride;
+
+	std::optional<std::map<unsigned, std::shared_ptr<std::string const>>> m_sourceNames;
+	langutil::SourceLocation m_locationOverride;
+	std::shared_ptr<DebugData const> m_debugDataOverride;
+	UseSourceLocationFrom m_useSourceLocationFrom = UseSourceLocationFrom::Scanner;
 	ForLoopComponent m_currentForLoopComponent = ForLoopComponent::None;
 	bool m_insideFunction = false;
 };