Merge pull request #7716 from ethereum/develop

Merge develop into release for 0.5.13

.circleci/config.yml

@@ -104,17 +104,6 @@ defaults:
       name: command line tests
       command: ./test/cmdlineTests.sh
 
-  - test_ubuntu1904: &test_ubuntu1904
-      docker:
-        - image: ethereum/solidity-buildpack-deps:ubuntu1904
-      steps:
-        - checkout
-        - attach_workspace:
-            at: build
-        - run: *run_soltest
-        - store_test_results: *store_test_results
-        - store_artifacts: *artifacts_test_results
-
   - test_ubuntu1904_clang: &test_ubuntu1904_clang
       docker:
         - image: ethereum/solidity-buildpack-deps:ubuntu1904-clang
@@ -126,7 +115,7 @@ defaults:
         - store_test_results: *store_test_results
         - store_artifacts: *artifacts_test_results
 
-  - test_ubuntu1904_all: &test_ubuntu1904
+  - test_ubuntu1904: &test_ubuntu1904
       docker:
         - image: ethereum/solidity-buildpack-deps:ubuntu1904
       steps:
@@ -423,40 +412,61 @@ jobs:
 
   b_osx:
     macos:
-      xcode: "10.0.0"
+      xcode: "11.0.0"
     environment:
       TERM: xterm
       CMAKE_BUILD_TYPE: Debug
-      CMAKE_OPTIONS: -DLLL=ON
     steps:
       - checkout
+      - restore_cache:
+          keys:
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
       - run:
           name: Install build dependencies
-          command: |
+          command: ./.circleci/osx_install_dependencies.sh
-            brew unlink python
+      - save_cache:
-            brew install z3
+          key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
-            brew install boost
+          paths:
-            brew install cmake
+            - /usr/local/bin
-            brew install wget
+            - /usr/local/sbin
-            ./scripts/install_obsolete_jsoncpp_1_7_4.sh
+            - /usr/local/lib
+            - /usr/local/include
+            - /usr/local/Cellar
+            - /usr/local/Homebrew
       - run: *run_build
       - store_artifacts: *artifacts_solc
-      - persist_to_workspace: *artifacts_executables
+      - persist_to_workspace: *artifacts_build_dir
+
+  t_osx_soltest:
+    macos:
+      xcode: "11.0.0"
+    environment:
+      EVM: constantinople
+      OPTIMIZE: 0
+      TERM: xterm
+    steps:
+      - checkout
+      - restore_cache:
+          keys:
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
+      - attach_workspace:
+          at: build
+      - run: *run_soltest
+      - store_test_results: *store_test_results
+      - store_artifacts: *artifacts_test_results
 
   t_osx_cli:
     macos:
-      xcode: "10.0.0"
+      xcode: "11.0.0"
     environment:
       TERM: xterm
     steps:
       - checkout
+      - restore_cache:
+          keys:
+            - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
       - attach_workspace:
           at: build
-      - run:
-          name: Install dependencies
-          command: |
-            brew unlink python
-            brew install z3
       - run: *run_cmdline_tests
       - store_artifacts: *artifacts_test_results
 
@@ -568,7 +578,7 @@ jobs:
     environment:
       EVM: constantinople
       OPTIMIZE: 0
-      flags: --no-smt
+      SOLTEST_FLAGS: --no-smt
       ASAN_OPTIONS: check_initialization_order=true:detect_stack_use_after_return=true:strict_init_order=true:strict_string_checks=true:detect_invalid_pointer_pairs=2
 
   t_ems_solcjs:
@@ -660,6 +670,7 @@ workflows:
       # OS/X build and tests
       - b_osx: *workflow_trigger_on_tags
       - t_osx_cli: *workflow_osx
+      - t_osx_soltest: *workflow_osx
 
       # Ubuntu build and tests
       - b_ubu: *workflow_trigger_on_tags

.circleci/docker/Dockerfile.clang.ubuntu1904

@@ -57,12 +57,12 @@ RUN git clone --recursive -b boost-1.69.0 https://github.com/boostorg/boost.git
     ./bootstrap.sh --with-toolset=clang --prefix=/usr; \
     ./b2 toolset=clang headers; \
     ./b2 toolset=clang variant=release \
-        system regex filesystem unit_test_framework program_options \
+        system filesystem unit_test_framework program_options \
         install -j $(($(nproc)/2)); \
     rm -rf /usr/src/boost
 
 # Z3
-RUN git clone --depth 1 -b Z3-4.8.5 https://github.com/Z3Prover/z3.git \
+RUN git clone --depth 1 -b z3-4.8.6 https://github.com/Z3Prover/z3.git \
     /usr/src/z3; \
     cd /usr/src/z3; \
     python scripts/mk_make.py --prefix=/usr ; \

.circleci/docker/Dockerfile.ubuntu1804

@@ -34,7 +34,7 @@ RUN set -ex; \
 		build-essential \
 		software-properties-common \
 		cmake ninja-build clang++-8 \
-		libboost-regex-dev libboost-filesystem-dev libboost-test-dev libboost-system-dev \
+		libboost-filesystem-dev libboost-test-dev libboost-system-dev \
 		libboost-program-options-dev \
 		libjsoncpp-dev \
 		llvm-8-dev libz3-static-dev \

.circleci/docker/Dockerfile.ubuntu1904

@@ -34,7 +34,7 @@ RUN set -ex; \
 		build-essential \
 		software-properties-common \
 		cmake ninja-build clang++-8 libc++-8-dev libc++abi-8-dev \
-		libboost-regex-dev libboost-filesystem-dev libboost-test-dev libboost-system-dev \
+		libboost-filesystem-dev libboost-test-dev libboost-system-dev \
 		libboost-program-options-dev \
 		libjsoncpp-dev \
 		llvm-8-dev libcvc4-dev libz3-static-dev libleveldb1d \

.circleci/osx_install_dependencies.sh

@@ -0,0 +1,59 @@
+#! /bin/bash
+#------------------------------------------------------------------------------
+# Bash script to install osx dependencies
+#
+# The documentation for solidity is hosted at:
+#
+#     https://solidity.readthedocs.org
+#
+# ------------------------------------------------------------------------------
+# 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/>
+#
+# (c) 2016-2019 solidity contributors.
+# ------------------------------------------------------------------------------
+
+# note that the following directories may be cached by circleci:
+# - /usr/local/bin
+# - /usr/local/sbin
+# - /usr/local/lib
+# - /usr/local/include
+# - /usr/local/Cellar
+# - /usr/local/Homebrew
+
+if [ ! -f /usr/local/lib/libz3.a ] # if this file does not exists (cache was not restored), rebuild dependencies
+then
+  brew unlink python
+  brew install boost
+  brew install cmake
+  brew install wget
+  brew install coreutils
+  ./scripts/install_obsolete_jsoncpp_1_7_4.sh
+
+  # z3
+  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-osx-10.14.6.zip
+  unzip z3-4.8.6-x64-osx-10.14.6.zip
+  rm -f z3-4.8.6-x64-osx-10.14.6.zip
+  cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
+  cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin
+  cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include
+  rm -rf z3-4.8.6-x64-osx-10.14.6
+
+  # evmone
+  wget https://github.com/ethereum/evmone/releases/download/v0.1.0/evmone-0.1.0-darwin-x86_64.tar.gz
+  tar xzpf evmone-0.1.0-darwin-x86_64.tar.gz -C /usr/local
+  rm -f evmone-0.1.0-darwin-x86_64.tar.gz
+fi
+

.circleci/soltest.sh

@@ -12,6 +12,7 @@
 #     EVM=version_string      Specifies EVM version to compile for (such as homestead, etc)
 #     OPTIMIZE=1              Enables backend optimizer
 #     ABI_ENCODER_V2=1        Enables ABI encoder version 2
+#     SOLTEST_FLAGS=<flags>   Appends <flags> to default SOLTEST_ARGS
 #
 # ------------------------------------------------------------------------------
 # This file is part of solidity.
@@ -54,7 +55,7 @@ get_logfile_basename() {
 }
 
 BOOST_TEST_ARGS="--color_output=no --show_progress=yes --logger=JUNIT,error,test_results/`get_logfile_basename`.xml"
-SOLTEST_ARGS="--evm-version=$EVM --evmonepath /usr/lib/libevmone.so $flags"
+SOLTEST_ARGS="--evm-version=$EVM $SOLTEST_FLAGS"
 test "${OPTIMIZE}" = "1" && SOLTEST_ARGS="${SOLTEST_ARGS} --optimize"
 test "${ABI_ENCODER_V2}" = "1" && SOLTEST_ARGS="${SOLTEST_ARGS} --abiencoderv2 --optimize-yul"
 

CMakeLists.txt

@@ -10,7 +10,7 @@ include(EthPolicy)
 eth_policy()
 
 # project name and version should be set after cmake_policy CMP0048
-set(PROJECT_VERSION "0.5.12")
+set(PROJECT_VERSION "0.5.13")
 project(solidity VERSION ${PROJECT_VERSION} LANGUAGES C CXX)
 
 include(TestBigEndian)

CODING_STYLE.md

@@ -119,7 +119,7 @@ Use `solAssert` and `solUnimplementedAssert` generously to check assumptions tha
 4. Favour declarations close to use; don't habitually declare at top of scope ala C.
 5. Pass non-trivial parameters as const reference, unless the data is to be copied into the function, then either pass by const reference or by value and use std::move.
 6. If a function returns multiple values, use std::tuple (std::pair acceptable) or better introduce a struct type. Do not use */& arguments.
-7. Use parameters of pointer type only if ``nullptr`` is a valid argument, use references otherwise. Often, ``boost::optional`` is better suited than a raw pointer.
+7. Use parameters of pointer type only if ``nullptr`` is a valid argument, use references otherwise. Often, ``std::optional`` is better suited than a raw pointer.
 8. Never use a macro where adequate non-preprocessor C++ can be written.
 9. Only use ``auto`` if the type is very long and rather irrelevant.
 10. Do not pass bools: prefer enumerations instead.
@@ -135,12 +135,12 @@ enum class Accuracy
 };
 struct MeanSigma
 {
-	float mean;
+	float mean = 0.0f;
-	float standardDeviation;
+	float standardDeviation = 1.0f;
 };
 double const d = 0;
-int i;
+int i = 0;
-int j;
+int j = 0;
 char* s;
 MeanAndSigma ms meanAndSigma(std::vector<float> const& _v, Accuracy _a);
 Derived* x = dynamic_cast<Derived*>(base);

Changelog.md

@@ -1,3 +1,30 @@
+### 0.5.13 (2019-11-14)
+
+Language Features:
+ * Allow to obtain the address of a linked library with ``address(LibraryName)``.
+
+
+Compiler Features:
+ * Code Generator: Use SELFBALANCE opcode for ``address(this).balance`` if using Istanbul EVM.
+ * EWasm: Experimental EWasm binary output via ``--ewasm`` and as documented in standard-json.
+ * SMTChecker: Add break/continue support to the CHC engine.
+ * SMTChecker: Support assignments to multi-dimensional arrays and mappings.
+ * SMTChecker: Support inheritance and function overriding.
+ * Standard JSON Interface: Output the storage layout of a contract when artifact ``storageLayout`` is requested.
+ * TypeChecker: List possible candidates when overload resolution fails.
+ * TypeChecker: Disallow variables of library types.
+
+
+Bugfixes:
+ * Code Generator: Fixed a faulty assert that would wrongly trigger for array sizes exceeding unsigned integer.
+ * SMTChecker: Fix internal error when accessing indices of fixed bytes.
+ * SMTChecker: Fix internal error when using function pointers as arguments.
+ * SMTChecker: Fix internal error when implicitly converting string literals to fixed bytes.
+ * Type Checker: Disallow constructor of the same class to be used as modifier.
+ * Type Checker: Treat magic variables as unknown identifiers in inline assembly.
+
+
+
 ### 0.5.12 (2019-10-01)
 
 Language Features:
@@ -10,6 +37,7 @@ Compiler Features:
  * SMTChecker: Add loop support to the CHC engine.
  * Yul Optimizer: Take side-effect-freeness of user-defined functions into account.
  * Yul Optimizer: Remove redundant mload/sload operations.
+ * Yul Optimizer: Use the fact that branch conditions have certain value inside the branch.
 
 
 Bugfixes:

README.md

@@ -60,6 +60,8 @@ Please follow the
 [Developers Guide](https://solidity.readthedocs.io/en/latest/contributing.html)
 if you want to help.
 
+You can find our current feature and bug priorities for forthcoming releases [in the projects section](https://github.com/ethereum/solidity/projects).
+
 ## Maintainers
 * [@axic](https://github.com/axic)
 * [@chriseth](https://github.com/chriseth)

cmake/EthCompilerSettings.cmake

@@ -23,6 +23,9 @@ endif()
 
 eth_add_cxx_compiler_flag_if_supported(-Wimplicit-fallthrough)
 
+# Prevent the path of the source directory from ending up in the binary via __FILE__ macros.
+eth_add_cxx_compiler_flag_if_supported("-fmacro-prefix-map=${CMAKE_SOURCE_DIR}=/solidity")
+
 if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
 	# Enables all the warnings about constructions that some users consider questionable,
 	# and that are easy to avoid.  Also enable some extra warning flags that are not
@@ -130,6 +133,8 @@ elseif (DEFINED MSVC)
 	add_compile_options(-D_WIN32_WINNT=0x0600)		# declare Windows Vista API requirement
 	add_compile_options(-DNOMINMAX)					# undefine windows.h MAX && MIN macros cause it cause conflicts with std::min && std::max functions
 	add_compile_options(/utf-8)					# enable utf-8 encoding (solves warning 4819)
+	add_compile_options(-DBOOST_REGEX_NO_LIB)		# disable automatic boost::regex library selection
+	add_compile_options(-D_REGEX_MAX_STACK_COUNT=200000L)	# increase std::regex recursion depth limit
 
 	# disable empty object file warning
 	set(CMAKE_STATIC_LINKER_FLAGS "${CMAKE_STATIC_LINKER_FLAGS} /ignore:4221")

cmake/EthDependencies.cmake

@@ -26,7 +26,7 @@ set(ETH_SCRIPTS_DIR ${ETH_CMAKE_DIR}/scripts)
 set(Boost_USE_MULTITHREADED ON)
 option(Boost_USE_STATIC_LIBS "Link Boost statically" ON)
 
-set(BOOST_COMPONENTS "regex;filesystem;unit_test_framework;program_options;system")
+set(BOOST_COMPONENTS "filesystem;unit_test_framework;program_options;system")
 
 find_package(Boost 1.65.0 QUIET REQUIRED COMPONENTS ${BOOST_COMPONENTS})
 

cmake/EthUtils.cmake

@@ -34,3 +34,17 @@ macro(eth_default_option O DEF)
 	endif()
 endmacro()
 
+function(detect_stray_source_files FILELIST DIRECTORY)
+	if(CMAKE_VERSION VERSION_LESS 3.12)
+		file(GLOB sources RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" "${DIRECTORY}/*.cpp" "${DIRECTORY}/*.h")
+	else()
+		file(GLOB sources RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" CONFIGURE_DEPENDS "${DIRECTORY}/*.cpp" "${DIRECTORY}/*.h")
+	endif()
+	foreach(path IN LISTS FILELIST)
+		list(REMOVE_ITEM sources ${path})
+	endforeach()
+	list(LENGTH sources leftover_sources)
+	if (leftover_sources)
+		message(SEND_ERROR "The following source files are present but are not compiled: ${sources}")
+	endif()
+endfunction(detect_stray_source_files)

docs/050-breaking-changes.rst

@@ -292,27 +292,27 @@ Consider you have the following pre-0.5.0 contract already deployed:
 
 ::
 
-   // This will not compile with the current version of the compiler
+    // This will not compile with the current version of the compiler
-   pragma solidity ^0.4.25;
+    pragma solidity ^0.4.25;
-   contract OldContract {
+    contract OldContract {
-      function someOldFunction(uint8 a) {
+        function someOldFunction(uint8 a) {
-         //...
+            //...
-      }
+        }
-      function anotherOldFunction() constant returns (bool) {
+        function anotherOldFunction() constant returns (bool) {
-         //...
+            //...
-      }
+        }
-      // ...
+        // ...
-   }
+    }
 
 This will no longer compile with Solidity v0.5.0. However, you can define a compatible interface for it:
 
 ::
 
-   pragma solidity >=0.5.0 <0.7.0;
+    pragma solidity >=0.5.0 <0.7.0;
-   interface OldContract {
+    interface OldContract {
-      function someOldFunction(uint8 a) external;
+        function someOldFunction(uint8 a) external;
-      function anotherOldFunction() external returns (bool);
+        function anotherOldFunction() external returns (bool);
-   }
+    }
 
 Note that we did not declare ``anotherOldFunction`` to be ``view``, despite it being declared ``constant`` in the original
 contract. This is due to the fact that starting with Solidity v0.5.0 ``staticcall`` is used to call ``view`` functions.
@@ -325,19 +325,19 @@ Given the interface defined above, you can now easily use the already deployed p
 
 ::
 
-   pragma solidity >=0.5.0 <0.7.0;
+    pragma solidity >=0.5.0 <0.7.0;
 
-   interface OldContract {
+    interface OldContract {
-      function someOldFunction(uint8 a) external;
+        function someOldFunction(uint8 a) external;
-      function anotherOldFunction() external returns (bool);
+        function anotherOldFunction() external returns (bool);
-   }
+    }
 
-   contract NewContract {
+    contract NewContract {
-      function doSomething(OldContract a) public returns (bool) {
+        function doSomething(OldContract a) public returns (bool) {
-         a.someOldFunction(0x42);
+            a.someOldFunction(0x42);
-         return a.anotherOldFunction();
+            return a.anotherOldFunction();
-      }
+        }
-   }
+    }
 
 Similarly, pre-0.5.0 libraries can be used by defining the functions of the library without implementation and
 supplying the address of the pre-0.5.0 library during linking (see :ref:`commandline-compiler` for how to use the
@@ -345,17 +345,17 @@ commandline compiler for linking):
 
 ::
 
-   pragma solidity >=0.5.0 <0.7.0;
+    pragma solidity >=0.5.0 <0.7.0;
 
-   library OldLibrary {
+    library OldLibrary {
-      function someFunction(uint8 a) public returns(bool);
+        function someFunction(uint8 a) public returns(bool);
-   }
+    }
 
-   contract NewContract {
+    contract NewContract {
-      function f(uint8 a) public returns (bool) {
+        function f(uint8 a) public returns (bool) {
-         return OldLibrary.someFunction(a);
+            return OldLibrary.someFunction(a);
-      }
+        }
-   }
+    }
 
 
 Example
@@ -368,144 +368,144 @@ Old version:
 
 ::
 
-   // This will not compile
+    // This will not compile
-   pragma solidity ^0.4.25;
+    pragma solidity ^0.4.25;
 
-   contract OtherContract {
+    contract OtherContract {
-      uint x;
+        uint x;
-      function f(uint y) external {
+        function f(uint y) external {
-         x = y;
+            x = y;
-      }
+        }
-      function() payable external {}
+        function() payable external {}
-   }
+    }
 
-   contract Old {
+    contract Old {
-      OtherContract other;
+        OtherContract other;
-      uint myNumber;
+        uint myNumber;
 
-      // Function mutability not provided, not an error.
+        // Function mutability not provided, not an error.
-      function someInteger() internal returns (uint) { return 2; }
+        function someInteger() internal returns (uint) { return 2; }
 
-      // Function visibility not provided, not an error.
+        // Function visibility not provided, not an error.
-      // Function mutability not provided, not an error.
+        // Function mutability not provided, not an error.
-      function f(uint x) returns (bytes) {
+        function f(uint x) returns (bytes) {
-         // Var is fine in this version.
+            // Var is fine in this version.
-         var z = someInteger();
+            var z = someInteger();
-         x += z;
+            x += z;
-         // Throw is fine in this version.
+            // Throw is fine in this version.
-         if (x > 100)
+            if (x > 100)
-            throw;
+                throw;
-         bytes b = new bytes(x);
+            bytes b = new bytes(x);
-         y = -3 >> 1;
+            y = -3 >> 1;
-         // y == -1 (wrong, should be -2)
+            // y == -1 (wrong, should be -2)
-         do {
+            do {
-            x += 1;
+                x += 1;
-            if (x > 10) continue;
+                if (x > 10) continue;
-            // 'Continue' causes an infinite loop.
+                // 'Continue' causes an infinite loop.
-         } while (x < 11);
+            } while (x < 11);
-         // Call returns only a Bool.
+            // Call returns only a Bool.
-         bool success = address(other).call("f");
+            bool success = address(other).call("f");
-         if (!success)
+            if (!success)
-            revert();
+                revert();
-         else {
+            else {
-            // Local variables could be declared after their use.
+                // Local variables could be declared after their use.
-            int y;
+                int y;
-         }
+            }
-         return b;
+            return b;
-      }
+        }
 
-      // No need for an explicit data location for 'arr'
+        // No need for an explicit data location for 'arr'
-      function g(uint[] arr, bytes8 x, OtherContract otherContract) public {
+        function g(uint[] arr, bytes8 x, OtherContract otherContract) public {
-         otherContract.transfer(1 ether);
+            otherContract.transfer(1 ether);
 
-         // Since uint32 (4 bytes) is smaller than bytes8 (8 bytes),
+            // Since uint32 (4 bytes) is smaller than bytes8 (8 bytes),
-         // the first 4 bytes of x will be lost. This might lead to
+            // the first 4 bytes of x will be lost. This might lead to
-         // unexpected behavior since bytesX are right padded.
+            // unexpected behavior since bytesX are right padded.
-         uint32 y = uint32(x);
+            uint32 y = uint32(x);
-         myNumber += y + msg.value;
+            myNumber += y + msg.value;
-      }
+        }
-   }
+    }
 
 New version:
 
 ::
 
-   pragma solidity >=0.5.0 <0.7.0;
+    pragma solidity >=0.5.0 <0.7.0;
 
-   contract OtherContract {
+    contract OtherContract {
-      uint x;
+        uint x;
-      function f(uint y) external {
+        function f(uint y) external {
-         x = y;
+            x = y;
-      }
+        }
-      function() payable external {}
+        function() payable external {}
-   }
+    }
 
-   contract New {
+    contract New {
-      OtherContract other;
+        OtherContract other;
-      uint myNumber;
+        uint myNumber;
 
-      // Function mutability must be specified.
+        // Function mutability must be specified.
-      function someInteger() internal pure returns (uint) { return 2; }
+        function someInteger() internal pure returns (uint) { return 2; }
 
-      // Function visibility must be specified.
+        // Function visibility must be specified.
-      // Function mutability must be specified.
+        // Function mutability must be specified.
-      function f(uint x) public returns (bytes memory) {
+        function f(uint x) public returns (bytes memory) {
-         // The type must now be explicitly given.
+            // The type must now be explicitly given.
-         uint z = someInteger();
+            uint z = someInteger();
-         x += z;
+            x += z;
-         // Throw is now disallowed.
+            // Throw is now disallowed.
-         require(x > 100);
+            require(x > 100);
-         int y = -3 >> 1;
+            int y = -3 >> 1;
-         // y == -2 (correct)
+            require(y == -2);
-         do {
+            do {
-            x += 1;
+                x += 1;
-            if (x > 10) continue;
+                if (x > 10) continue;
-            // 'Continue' jumps to the condition below.
+                // 'Continue' jumps to the condition below.
-         } while (x < 11);
+            } while (x < 11);
 
-         // Call returns (bool, bytes).
+            // Call returns (bool, bytes).
-         // Data location must be specified.
+            // Data location must be specified.
-         (bool success, bytes memory data) = address(other).call("f");
+            (bool success, bytes memory data) = address(other).call("f");
-         if (!success)
+            if (!success)
-            revert();
+                revert();
-         return data;
+            return data;
-      }
+        }
 
-      using address_make_payable for address;
+        using address_make_payable for address;
-      // Data location for 'arr' must be specified
+        // Data location for 'arr' must be specified
-      function g(uint[] memory arr, bytes8 x, OtherContract otherContract, address unknownContract) public payable {
+        function g(uint[] memory /* arr */, bytes8 x, OtherContract otherContract, address unknownContract) public payable {
-         // 'otherContract.transfer' is not provided.
+            // 'otherContract.transfer' is not provided.
-         // Since the code of 'OtherContract' is known and has the fallback
+            // Since the code of 'OtherContract' is known and has the fallback
-         // function, address(otherContract) has type 'address payable'.
+            // function, address(otherContract) has type 'address payable'.
-         address(otherContract).transfer(1 ether);
+            address(otherContract).transfer(1 ether);
 
-         // 'unknownContract.transfer' is not provided.
+            // 'unknownContract.transfer' is not provided.
-         // 'address(unknownContract).transfer' is not provided
+            // 'address(unknownContract).transfer' is not provided
-         // since 'address(unknownContract)' is not 'address payable'.
+            // since 'address(unknownContract)' is not 'address payable'.
-         // If the function takes an 'address' which you want to send
+            // If the function takes an 'address' which you want to send
-         // funds to, you can convert it to 'address payable' via 'uint160'.
+            // funds to, you can convert it to 'address payable' via 'uint160'.
-         // Note: This is not recommended and the explicit type
+            // Note: This is not recommended and the explicit type
-         // 'address payable' should be used whenever possible.
+            // 'address payable' should be used whenever possible.
-         // To increase clarity, we suggest the use of a library for
+            // To increase clarity, we suggest the use of a library for
-         // the conversion (provided after the contract in this example).
+            // the conversion (provided after the contract in this example).
-         address payable addr = unknownContract.make_payable();
+            address payable addr = unknownContract.make_payable();
-         require(addr.send(1 ether));
+            require(addr.send(1 ether));
 
-         // Since uint32 (4 bytes) is smaller than bytes8 (8 bytes),
+            // Since uint32 (4 bytes) is smaller than bytes8 (8 bytes),
-         // the conversion is not allowed.
+            // the conversion is not allowed.
-         // We need to convert to a common size first:
+            // We need to convert to a common size first:
-         bytes4 x4 = bytes4(x); // Padding happens on the right
+            bytes4 x4 = bytes4(x); // Padding happens on the right
-         uint32 y = uint32(x4); // Conversion is consistent
+            uint32 y = uint32(x4); // Conversion is consistent
-         // 'msg.value' cannot be used in a 'non-payable' function.
+            // 'msg.value' cannot be used in a 'non-payable' function.
-         // We need to make the function payable
+            // We need to make the function payable
-         myNumber += y + msg.value;
+            myNumber += y + msg.value;
-      }
+        }
-   }
+    }
 
-   // We can define a library for explicitly converting ``address``
+    // We can define a library for explicitly converting ``address``
-   // to ``address payable`` as a workaround.
+    // to ``address payable`` as a workaround.
-   library address_make_payable {
+    library address_make_payable {
-      function make_payable(address x) internal pure returns (address payable) {
+        function make_payable(address x) internal pure returns (address payable) {
-         return address(uint160(x));
+            return address(uint160(x));
-      }
+        }
-   }
+    }

docs/assembly.rst

@@ -292,7 +292,7 @@ In the grammar, opcodes are represented as pre-defined identifiers.
 | create2(v, p, n, s)     |     | C | create new contract with code mem[p...(p+n)) at address         |
 |                         |     |   | keccak256(0xff . this . s . keccak256(mem[p...(p+n)))           |
 |                         |     |   | and send v wei and return the new address, where ``0xff`` is a  |
-|                         |     |   | 8 byte value, ``this`` is the current contract's address        |
+|                         |     |   | 1 byte value, ``this`` is the current contract's address        |
 |                         |     |   | as a 20 byte value and ``s`` is a big-endian 256-bit value      |
 +-------------------------+-----+---+-----------------------------------------------------------------+
 | call(g, a, v, in,       |     | F | call contract at address a with input mem[in...(in+insize))     |

docs/bugs_by_version.json

@@ -754,6 +754,10 @@
         "bugs": [],
         "released": "2019-10-01"
     },
+    "0.5.13": {
+        "bugs": [],
+        "released": "2019-11-14"
+    },
     "0.5.2": {
         "bugs": [
             "SignedArrayStorageCopy",

docs/common-patterns.rst

@@ -22,9 +22,8 @@ a contract where the goal is to send the most money to the
 contract in order to become the "richest", inspired by
 `King of the Ether <https://www.kingoftheether.com/>`_.
 
-In the following contract, if you are usurped as the richest,
+In the following contract, if you are no longer the richest,
-you will receive the funds of the person who has gone on to
+you receive the funds of the person who is now the richest.
-become the new richest.
 
 ::
 

docs/contracts/libraries.rst

@@ -178,6 +178,9 @@ custom types without the overhead of external function calls:
         }
     }
 
+It is possible to obtain the address of a library by converting
+the library type to the ``address`` type, i.e. using ``address(LibraryName)``.
+
 As the compiler cannot know where the library will be
 deployed at, these addresses have to be filled into the
 final bytecode by a linker

docs/contracts/visibility-and-getters.rst

@@ -150,24 +150,24 @@ to write a function, for example:
 
 ::
 
-  pragma solidity >=0.4.0 <0.7.0;
+    pragma solidity >=0.4.0 <0.7.0;
 
-  contract arrayExample {
+    contract arrayExample {
-    // public state variable
+        // public state variable
-    uint[] public myArray;
+        uint[] public myArray;
 
-    // Getter function generated by the compiler
+        // Getter function generated by the compiler
-    /*
+        /*
-    function myArray(uint i) returns (uint) {
+        function myArray(uint i) public view returns (uint) {
-        return myArray[i];
+            return myArray[i];
+        }
+        */
+
+        // function that returns entire array
+        function getArray() public view returns (uint[] memory) {
+            return myArray;
+        }
     }
-    */
-
-    // function that returns entire array
-    function getArray() returns (uint[] memory) {
-        return myArray;
-    }
-  }
 
 Now you can use ``getArray()`` to retrieve the entire array, instead of
 ``myArray(i)``, which returns a single element per call.

docs/layout-of-source-files.rst

@@ -37,7 +37,7 @@ breaking changes. These releases always have versions of the form
 
 The version pragma is used as follows::
 
-  pragma solidity ^0.5.2;
+    pragma solidity ^0.5.2;
 
 A source file with the line above does not compile with a compiler earlier than version 0.5.2,
 and it also does not work on a compiler starting from version 0.6.0 (this

docs/miscellaneous.rst

@@ -8,6 +8,8 @@ Miscellaneous
 Layout of State Variables in Storage
 ************************************
 
+.. _storage-inplace-encoding:
+
 Statically-sized variables (everything except mapping and dynamically-sized array types) are laid out contiguously in storage starting from position ``0``. Multiple, contiguous items that need less than 32 bytes are packed into a single storage slot if possible, according to the following rules:
 
 - The first item in a storage slot is stored lower-order aligned.
@@ -49,6 +51,8 @@ The elements of structs and arrays are stored after each other, just as if they
 Mappings and Dynamic Arrays
 ===========================
 
+.. _storage-hashed-encoding:
+
 Due to their unpredictable size, mapping and dynamically-sized array types use a Keccak-256 hash
 computation to find the starting position of the value or the array data. These starting positions are always full stack slots.
 
@@ -88,6 +92,267 @@ by checking if the lowest bit is set: short (not set) and long (set).
 .. note::
   Handling invalidly encoded slots is currently not supported but may be added in the future.
 
+JSON Output
+===========
+
+.. _storage-layout-top-level:
+
+The storage layout of a contract can be requested via the :ref:`standard JSON interface <compiler-api>`.  The output is a JSON object containing two keys,
+``storage`` and ``types``.  The ``storage`` object is an array where each
+element has the following form:
+
+
+.. code::
+
+
+    {
+        "astId": 2,
+        "contract": "fileA:A",
+        "label": "x",
+        "offset": 0,
+        "slot": "0",
+        "type": "t_uint256"
+    }
+
+where the example above is the storage layout of ``contract A { uint x; }`` from source unit ``fileA``
+and
+
+- ``astId`` is the id of the AST node of the state variable's declaration
+- ``contract`` is the name of the contract including its path as prefix
+- ``label`` is the name of the state variable
+- ``offset`` is the offset in bytes within the storage slot according to the encoding
+- ``slot`` is the storage slot where the state variable resides or starts. This
+  number may be very large and therefore its JSON value is represented as a
+  string.
+- ``type`` is an identifier used as key to the variable's type information (described in the following)
+
+The given ``type``, in this case ``t_uint256`` represents an element in
+``types``, which has the form:
+
+
+.. code::
+
+    {
+        "encoding": "inplace",
+        "label": "uint256",
+        "numberOfBytes": "32",
+    }
+
+where
+
+- ``encoding`` how the data is encoded in storage, where the possible values are:
+
+  - ``inplace``: data is laid out contiguously in storage (see :ref:`above <storage-inplace-encoding>`).
+  - ``mapping``: Keccak-256 hash-based method (see :ref:`above <storage-hashed-encoding>`).
+  - ``dynamic_array``: Keccak-256 hash-based method (see :ref:`above <storage-hashed-encoding>`).
+  - ``bytes``: single slot or Keccak-256 hash-based depending on the data size (see :ref:`above <bytes-and-string>`).
+
+- ``label`` is the canonical type name.
+- ``numberOfBytes`` is the number of used bytes (as a decimal string). Note that if ``numberOfBytes > 32`` this means that more than one slot is used.
+
+Some types have extra information besides the four above. Mappings contain
+its ``key`` and ``value`` types (again referencing an entry in this mapping
+of types), arrays have its ``base`` type, and structs list their ``members`` in
+the same format as the top-level ``storage`` (see :ref:`above
+<storage-layout-top-level>`).
+
+.. note ::
+  The JSON output format of a contract's storage layout is still considered experimental
+  and is subject to change in non-breaking releases of Solidity.
+
+The following example shows a contract and its storage layout, containing
+value and reference types, types that are encoded packed, and nested types.
+
+
+.. code::
+
+    pragma solidity >=0.4.0 <0.7.0;
+    contract A {
+        struct S {
+            uint128 a;
+            uint128 b;
+            uint[2] staticArray;
+            uint[] dynArray;
+        }
+
+        uint x;
+        uint y;
+        S s;
+        address addr;
+        mapping (uint => mapping (address => bool)) map;
+        uint[] array;
+        string s1;
+        bytes b1;
+    }
+
+.. code::
+
+    "storageLayout": {
+      "storage": [
+        {
+          "astId": 14,
+          "contract": "fileA:A",
+          "label": "x",
+          "offset": 0,
+          "slot": "0",
+          "type": "t_uint256"
+        },
+        {
+          "astId": 16,
+          "contract": "fileA:A",
+          "label": "y",
+          "offset": 0,
+          "slot": "1",
+          "type": "t_uint256"
+        },
+        {
+          "astId": 18,
+          "contract": "fileA:A",
+          "label": "s",
+          "offset": 0,
+          "slot": "2",
+          "type": "t_struct(S)12_storage"
+        },
+        {
+          "astId": 20,
+          "contract": "fileA:A",
+          "label": "addr",
+          "offset": 0,
+          "slot": "6",
+          "type": "t_address"
+        },
+        {
+          "astId": 26,
+          "contract": "fileA:A",
+          "label": "map",
+          "offset": 0,
+          "slot": "7",
+          "type": "t_mapping(t_uint256,t_mapping(t_address,t_bool))"
+        },
+        {
+          "astId": 29,
+          "contract": "fileA:A",
+          "label": "array",
+          "offset": 0,
+          "slot": "8",
+          "type": "t_array(t_uint256)dyn_storage"
+        },
+        {
+          "astId": 31,
+          "contract": "fileA:A",
+          "label": "s1",
+          "offset": 0,
+          "slot": "9",
+          "type": "t_string_storage"
+        },
+        {
+          "astId": 33,
+          "contract": "fileA:A",
+          "label": "b1",
+          "offset": 0,
+          "slot": "10",
+          "type": "t_bytes_storage"
+        }
+      ],
+      "types": {
+        "t_address": {
+          "encoding": "inplace",
+          "label": "address",
+          "numberOfBytes": "20"
+        },
+        "t_array(t_uint256)2_storage": {
+          "base": "t_uint256",
+          "encoding": "inplace",
+          "label": "uint256[2]",
+          "numberOfBytes": "64"
+        },
+        "t_array(t_uint256)dyn_storage": {
+          "base": "t_uint256",
+          "encoding": "dynamic_array",
+          "label": "uint256[]",
+          "numberOfBytes": "32"
+        },
+        "t_bool": {
+          "encoding": "inplace",
+          "label": "bool",
+          "numberOfBytes": "1"
+        },
+        "t_bytes_storage": {
+          "encoding": "bytes",
+          "label": "bytes",
+          "numberOfBytes": "32"
+        },
+        "t_mapping(t_address,t_bool)": {
+          "encoding": "mapping",
+          "key": "t_address",
+          "label": "mapping(address => bool)",
+          "numberOfBytes": "32",
+          "value": "t_bool"
+        },
+        "t_mapping(t_uint256,t_mapping(t_address,t_bool))": {
+          "encoding": "mapping",
+          "key": "t_uint256",
+          "label": "mapping(uint256 => mapping(address => bool))",
+          "numberOfBytes": "32",
+          "value": "t_mapping(t_address,t_bool)"
+        },
+        "t_string_storage": {
+          "encoding": "bytes",
+          "label": "string",
+          "numberOfBytes": "32"
+        },
+        "t_struct(S)12_storage": {
+          "encoding": "inplace",
+          "label": "struct A.S",
+          "members": [
+            {
+              "astId": 2,
+              "contract": "fileA:A",
+              "label": "a",
+              "offset": 0,
+              "slot": "0",
+              "type": "t_uint128"
+            },
+            {
+              "astId": 4,
+              "contract": "fileA:A",
+              "label": "b",
+              "offset": 16,
+              "slot": "0",
+              "type": "t_uint128"
+            },
+            {
+              "astId": 8,
+              "contract": "fileA:A",
+              "label": "staticArray",
+              "offset": 0,
+              "slot": "1",
+              "type": "t_array(t_uint256)2_storage"
+            },
+            {
+              "astId": 11,
+              "contract": "fileA:A",
+              "label": "dynArray",
+              "offset": 0,
+              "slot": "3",
+              "type": "t_array(t_uint256)dyn_storage"
+            }
+          ],
+          "numberOfBytes": "128"
+        },
+        "t_uint128": {
+          "encoding": "inplace",
+          "label": "uint128",
+          "numberOfBytes": "16"
+        },
+        "t_uint256": {
+          "encoding": "inplace",
+          "label": "uint256",
+          "numberOfBytes": "32"
+        }
+      }
+    }
+
 .. index: memory layout
 
 ****************

docs/natspec-format.rst

@@ -49,22 +49,22 @@ The following example shows a contract and a function using all available tags.
 
 .. code:: solidity
 
-   pragma solidity ^0.5.6;
+    pragma solidity ^0.5.6;
 
-   /// @title A simulator for trees
+    /// @title A simulator for trees
-   /// @author Larry A. Gardner
+    /// @author Larry A. Gardner
-   /// @notice You can use this contract for only the most basic simulation
+    /// @notice You can use this contract for only the most basic simulation
-   /// @dev All function calls are currently implemented without side effects
+    /// @dev All function calls are currently implemented without side effects
-   contract Tree {
+    contract Tree {
-       /// @author Mary A. Botanist
+        /// @author Mary A. Botanist
-       /// @notice Calculate tree age in years, rounded up, for live trees
+        /// @notice Calculate tree age in years, rounded up, for live trees
-       /// @dev The Alexandr N. Tetearing algorithm could increase precision
+        /// @dev The Alexandr N. Tetearing algorithm could increase precision
-       /// @param rings The number of rings from dendrochronological sample
+        /// @param rings The number of rings from dendrochronological sample
-       /// @return age in years, rounded up for partial years
+        /// @return age in years, rounded up for partial years
-       function age(uint256 rings) external pure returns (uint256) {
+        function age(uint256 rings) external pure returns (uint256) {
-           return rings + 1;
+            return rings + 1;
-       }
+        }
-   }
+    }
 
 .. _header-tags:
 

docs/resources.rst

@@ -127,6 +127,9 @@ Solidity Tools
 * `Universal Mutator <https://github.com/agroce/universalmutator>`_
     A tool for mutation generation, with configurable rules and support for Solidity and Vyper.
 
+* `PIET <https://piet.slock.it/>`_
+    A tool to develop, audit and use solidity smart contracts through a simple graphical interface.
+
 .. note::
   Information like variable names, comments, and source code formatting is lost in the compilation process and it is not possible to completely recover the original source code. Decompiling smart contracts to view the original source code might not be possible, or the end result that useful.
 

docs/security-considerations.rst

@@ -499,26 +499,26 @@ not mean loss of proving power.
 
 ::
 
-   pragma solidity >=0.5.0;
+    pragma solidity >=0.5.0;
-   pragma experimental SMTChecker;
+    pragma experimental SMTChecker;
 
-   contract Recover
+    contract Recover
-   {
+    {
-           function f(
+        function f(
-                   bytes32 hash,
+            bytes32 hash,
-                   uint8 _v1, uint8 _v2,
+            uint8 _v1, uint8 _v2,
-                   bytes32 _r1, bytes32 _r2,
+            bytes32 _r1, bytes32 _r2,
-                   bytes32 _s1, bytes32 _s2
+            bytes32 _s1, bytes32 _s2
-           ) public pure returns (address) {
+        ) public pure returns (address) {
-                   address a1 = ecrecover(hash, _v1, _r1, _s1);
+            address a1 = ecrecover(hash, _v1, _r1, _s1);
-                   require(_v1 == _v2);
+            require(_v1 == _v2);
-                   require(_r1 == _r2);
+            require(_r1 == _r2);
-                   require(_s1 == _s2);
+            require(_s1 == _s2);
-                   address a2 = ecrecover(hash, _v2, _r2, _s2);
+            address a2 = ecrecover(hash, _v2, _r2, _s2);
-                   assert(a1 == a2);
+            assert(a1 == a2);
-                   return a1;
+            return a1;
-           }
+        }
-   }
+    }
 
 In the example above, the SMTChecker is not expressive enough to actually
 compute ``ecrecover``, but by modelling the function calls as uninterpreted
@@ -552,34 +552,34 @@ types.
 
 ::
 
-   pragma solidity >=0.5.0;
+    pragma solidity >=0.5.0;
-   pragma experimental SMTChecker;
+    pragma experimental SMTChecker;
-   // This will not compile
+    // This will report a warning
-   contract Aliasing
+    contract Aliasing
-   {
+    {
-      uint[] array;
+        uint[] array;
-      function f(
+        function f(
-         uint[] memory a,
+            uint[] memory a,
-         uint[] memory b,
+            uint[] memory b,
-         uint[][] memory c,
+            uint[][] memory c,
-         uint[] storage d
+            uint[] storage d
-      ) internal view {
+        ) internal view {
-         require(array[0] == 42);
+            require(array[0] == 42);
-         require(a[0] == 2);
+            require(a[0] == 2);
-         require(c[0][0] == 2);
+            require(c[0][0] == 2);
-         require(d[0] == 2);
+            require(d[0] == 2);
-         b[0] = 1;
+            b[0] = 1;
-         // Erasing knowledge about memory references should not
+            // Erasing knowledge about memory references should not
-         // erase knowledge about state variables.
+            // erase knowledge about state variables.
-         assert(array[0] == 42);
+            assert(array[0] == 42);
-         // Fails because `a == b` is possible.
+            // Fails because `a == b` is possible.
-         assert(a[0] == 2);
+            assert(a[0] == 2);
-         // Fails because `c[i] == b` is possible.
+            // Fails because `c[i] == b` is possible.
-         assert(c[0][0] == 2);
+            assert(c[0][0] == 2);
-         assert(d[0] == 2);
+            assert(d[0] == 2);
-         assert(b[0] == 1);
+            assert(b[0] == 1);
-      }
+        }
-   }
+    }
 
 After the assignment to ``b[0]``, we need to clear knowledge about ``a`` since
 it has the same type (``uint[]``) and data location (memory).  We also need to

docs/types/mapping-types.rst

@@ -4,7 +4,8 @@
 Mapping Types
 =============
 
-You declare mapping types with the syntax ``mapping(_KeyType => _ValueType)``.
+Mapping types use the syntax ``mapping(_KeyType => _ValueType)`` and variables
+are declared as a mapping type using the syntax ``mapping (_KeyType => _ValueType) _VariableModifiers _VariableName``.
 The ``_KeyType`` can be any elementary type. This means it can be any of
 the built-in value types plus ``bytes`` and ``string``. User-defined
 or complex types like contract types, enums, mappings, structs and any array type
@@ -27,11 +28,16 @@ They cannot be used as parameters or return parameters
 of contract functions that are publicly visible.
 
 You can mark state variables of mapping type as ``public`` and Solidity creates a
-:ref:`getter <visibility-and-getters>` for you. The ``_KeyType`` becomes a
+:ref:`getter <visibility-and-getters>` for you. The ``_KeyType`` becomes a parameter for the getter.
-parameter for the getter. If ``_ValueType`` is a value type or a struct,
+If ``_ValueType`` is a value type or a struct, the getter returns ``_ValueType``.
-the getter returns ``_ValueType``.
 If ``_ValueType`` is an array or a mapping, the getter has one parameter for
-each ``_KeyType``, recursively. For example with a mapping:
+each ``_KeyType``, recursively.
+
+In the example below, the ``MappingExample`` contract defines a public ``balances``
+mapping, with the key type an ``address``, and a value type a ``uint``, mapping
+an Ethereum address to an unsigned integer value. As ``uint`` is a value type, the getter
+returns a value that matches the type, which you can see in the ``MappingUser``
+contract that returns the value at the specified address.
 
 ::
 
@@ -53,7 +59,146 @@ each ``_KeyType``, recursively. For example with a mapping:
         }
     }
 
+The example below is a simplified version of an `ERC20 token <https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/token/ERC20/ERC20.sol>`_.
+``_allowances`` is an example of a mapping type inside another mapping type.
+The example below uses ``_allowances`` to record the amount someone else is allowed to withdraw from your account.
 
-.. note::
+::
-  Mappings are not iterable, but it is possible to implement a data structure
+
-  on top of them. For an example, see `iterable mapping <https://github.com/ethereum/dapp-bin/blob/master/library/iterable_mapping.sol>`_.
+    pragma solidity >=0.4.0 <0.7.0;
+
+    contract MappingExample {
+
+        mapping (address => uint256) private _balances;
+        mapping (address => mapping (address => uint256)) private _allowances;
+
+        event Transfer(address indexed from, address indexed to, uint256 value);
+        event Approval(address indexed owner, address indexed spender, uint256 value);
+
+        function allowance(address owner, address spender) public view returns (uint256) {
+            return _allowances[owner][spender];
+        }
+
+        function transferFrom(address sender, address recipient, uint256 amount) public returns (bool) {
+            _transfer(sender, recipient, amount);
+            approve(sender, msg.sender, amount);
+            return true;
+        }
+
+        function approve(address owner, address spender, uint256 amount) public returns (bool) {
+            require(owner != address(0), "ERC20: approve from the zero address");
+            require(spender != address(0), "ERC20: approve to the zero address");
+
+            _allowances[owner][spender] = amount;
+            emit Approval(owner, spender, amount);
+            return true;
+        }
+
+        function _transfer(address sender, address recipient, uint256 amount) internal {
+            require(sender != address(0), "ERC20: transfer from the zero address");
+            require(recipient != address(0), "ERC20: transfer to the zero address");
+
+            _balances[sender] -= amount;
+            _balances[recipient] += amount;
+            emit Transfer(sender, recipient, amount);
+        }
+    }
+
+
+.. index:: !iterable mappings
+.. _iterable-mappings:
+
+Iterable Mappings
+-----------------
+
+Mappings are not iterable, but it is possible to implement a data structure on
+top of them and iterate over that. For example, the code below implements an
+``IterableMapping`` library that the ``User`` contract then adds data too, and
+the ``sum`` function iterates over to sum all the values.
+
+::
+
+    pragma solidity >=0.4.0 <0.7.0;
+
+    library IterableMapping {
+
+        struct itmap {
+            mapping(uint => IndexValue) data;
+            KeyFlag[] keys;
+            uint size;
+        }
+
+        struct IndexValue { uint keyIndex; uint value; }
+        struct KeyFlag { uint key; bool deleted; }
+
+        function insert(itmap storage self, uint key, uint value) internal returns (bool replaced) {
+            uint keyIndex = self.data[key].keyIndex;
+            self.data[key].value = value;
+            if (keyIndex > 0)
+                return true;
+            else {
+                keyIndex = self.keys.length++;
+                self.data[key].keyIndex = keyIndex + 1;
+                self.keys[keyIndex].key = key;
+                self.size++;
+                return false;
+            }
+        }
+
+        function remove(itmap storage self, uint key) internal returns (bool success) {
+            uint keyIndex = self.data[key].keyIndex;
+            if (keyIndex == 0)
+                return false;
+            delete self.data[key];
+            self.keys[keyIndex - 1].deleted = true;
+            self.size --;
+        }
+
+        function contains(itmap storage self, uint key) internal view returns (bool) {
+            return self.data[key].keyIndex > 0;
+        }
+
+        function iterate_start(itmap storage self) internal view returns (uint keyIndex) {
+            return iterate_next(self, uint(-1));
+        }
+
+        function iterate_valid(itmap storage self, uint keyIndex) internal view returns (bool) {
+            return keyIndex < self.keys.length;
+        }
+
+        function iterate_next(itmap storage self, uint keyIndex) internal view returns (uint r_keyIndex) {
+            keyIndex++;
+            while (keyIndex < self.keys.length && self.keys[keyIndex].deleted)
+                keyIndex++;
+            return keyIndex;
+        }
+
+        function iterate_get(itmap storage self, uint keyIndex) internal view returns (uint key, uint value) {
+            key = self.keys[keyIndex].key;
+            value = self.data[key].value;
+        }
+    }
+
+    // How to use it
+    contract User {
+        // Just a struct holding our data.
+        IterableMapping.itmap data;
+
+        // Insert something
+        function insert(uint k, uint v) public returns (uint size) {
+            // Actually calls itmap_impl.insert, auto-supplying the first parameter for us.
+            IterableMapping.insert(data, k, v);
+            // We can still access members of the struct - but we should take care not to mess with them.
+            return data.size;
+        }
+
+        // Computes the sum of all stored data.
+        function sum() public view returns (uint s) {
+            for (uint i = IterableMapping.iterate_start(data);
+            IterableMapping.iterate_valid(data, i);
+            i = IterableMapping.iterate_next(data, i)) {
+                (, uint value) = IterableMapping.iterate_get(data, i);
+                s += value;
+            }
+        }
+    }

docs/types/operators.rst

@@ -17,7 +17,7 @@ equivalent to ``a = 0``, but it can also be used on arrays, where it assigns a d
 array of length zero or a static array of the same length with all elements set to their
 initial value. ``delete a[x]`` deletes the item at index ``x`` of the array and leaves
 all other elements and the length of the array untouched. This especially means that it leaves
-a gap in the array. If you plan to remove items, a mapping is probably a better choice.
+a gap in the array. If you plan to remove items, a :ref:`mapping <mapping-types>` is probably a better choice.
 
 For structs, it assigns a struct with all members reset. In other words, the value of ``a`` after ``delete a`` is the same as if ``a`` would be declared without assignment, with the following caveat:
 

docs/using-the-compiler.rst

@@ -276,6 +276,7 @@ Input Description
         //   metadata - Metadata
         //   ir - Yul intermediate representation of the code before optimization
         //   irOptimized - Intermediate representation after optimization
+        //   storageLayout - Slots, offsets and types of the contract's state variables.
         //   evm.assembly - New assembly format
         //   evm.legacyAssembly - Old-style assembly format in JSON
         //   evm.bytecode.object - Bytecode object
@@ -376,6 +377,8 @@ Output Description
             "devdoc": {},
             // Intermediate representation (string)
             "ir": "",
+            // See the Storage Layout documentation.
+            "storageLayout": {"storage": [...], "types": {...} },
             // EVM-related outputs
             "evm": {
               // Assembly (string)

libdevcore/CMakeLists.txt

@@ -34,6 +34,10 @@ set(sources
 )
 
 add_library(devcore ${sources})
-target_link_libraries(devcore PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::regex Boost::system)
+target_link_libraries(devcore PUBLIC jsoncpp Boost::boost Boost::filesystem Boost::system)
 target_include_directories(devcore PUBLIC "${CMAKE_SOURCE_DIR}")
 add_dependencies(devcore solidity_BuildInfo.h)
+
+if(SOLC_LINK_STATIC)
+	target_link_libraries(devcore PUBLIC Threads::Threads)
+endif()

libdevcore/CommonData.h

@@ -25,11 +25,10 @@
 
 #include <libdevcore/Common.h>
 
-#include <boost/optional.hpp>
-
 #include <vector>
 #include <type_traits>
 #include <cstring>
+#include <optional>
 #include <string>
 #include <set>
 #include <functional>
@@ -277,7 +276,7 @@ void iterateReplacing(std::vector<T>& _vector, F const& _f)
 	std::vector<T> modifiedVector;
 	for (size_t i = 0; i < _vector.size(); ++i)
 	{
-		if (boost::optional<std::vector<T>> r = _f(_vector[i]))
+		if (std::optional<std::vector<T>> r = _f(_vector[i]))
 		{
 			if (!useModified)
 			{
@@ -305,7 +304,7 @@ void iterateReplacingWindow(std::vector<T>& _vector, F const& _f, std::index_seq
 	size_t i = 0;
 	for (; i + sizeof...(I) <= _vector.size(); ++i)
 	{
-		if (boost::optional<std::vector<T>> r = _f(_vector[i + I]...))
+		if (std::optional<std::vector<T>> r = _f(_vector[i + I]...))
 		{
 			if (!useModified)
 			{

libdevcore/Whiskers.cpp

@@ -25,7 +25,7 @@
 
 #include <libdevcore/Assertions.h>
 
-#include <boost/regex.hpp>
+#include <regex>
 
 using namespace std;
 using namespace dev;
@@ -72,9 +72,9 @@ string Whiskers::render() const
 
 void Whiskers::checkParameterValid(string const& _parameter) const
 {
-	static boost::regex validParam("^" + paramRegex() + "$");
+	static regex validParam("^" + paramRegex() + "$");
 	assertThrow(
-		boost::regex_match(_parameter, validParam),
+		regex_match(_parameter, validParam),
 		WhiskersError,
 		"Parameter" + _parameter + " contains invalid characters."
 	);
@@ -99,6 +99,32 @@ void Whiskers::checkParameterUnknown(string const& _parameter) const
 	);
 }
 
+namespace
+{
+template<class ReplaceCallback>
+string regex_replace(
+	string const& _source,
+	regex const& _pattern,
+	ReplaceCallback _replace,
+	regex_constants::match_flag_type _flags = regex_constants::match_default
+)
+{
+	sregex_iterator curMatch(_source.begin(), _source.end(), _pattern, _flags);
+	sregex_iterator matchEnd;
+	string::const_iterator lastMatchedPos(_source.cbegin());
+	string result;
+	while (curMatch != matchEnd)
+	{
+		result.append(curMatch->prefix().first, curMatch->prefix().second);
+		result.append(_replace(*curMatch));
+		lastMatchedPos = (*curMatch)[0].second;
+		++curMatch;
+	}
+	result.append(lastMatchedPos, _source.cend());
+	return result;
+}
+}
+
 string Whiskers::replace(
 	string const& _template,
 	StringMap const& _parameters,
@@ -106,8 +132,7 @@ string Whiskers::replace(
 	map<string, vector<StringMap>> const& _listParameters
 )
 {
-	using namespace boost;
+	static regex listOrTag("<(" + paramRegex() + ")>|<#(" + paramRegex() + ")>((?:.|\\r|\\n)*?)</\\2>|<\\?(" + paramRegex() + ")>((?:.|\\r|\\n)*?)(<!\\4>((?:.|\\r|\\n)*?))?</\\4>");
-	static regex listOrTag("<(" + paramRegex() + ")>|<#(" + paramRegex() + ")>(.*?)</\\2>|<\\?(" + paramRegex() + ")>(.*?)(<!\\4>(.*?))?</\\4>");
 	return regex_replace(_template, listOrTag, [&](match_results<string::const_iterator> _match) -> string
 	{
 		string tagName(_match[1]);

libevmasm/Assembly.cpp

@@ -258,7 +258,7 @@ Json::Value Assembly::createJsonValue(string _name, int _begin, int _end, string
 string Assembly::toStringInHex(u256 _value)
 {
 	std::stringstream hexStr;
-	hexStr << hex << _value;
+	hexStr << std::uppercase << hex << _value;
 	return hexStr.str();
 }
 

libevmasm/Instruction.cpp

@@ -356,13 +356,13 @@ string dev::eth::disassemble(bytes const& _mem)
 	stringstream ret;
 	eachInstruction(_mem, [&](Instruction _instr, u256 const& _data) {
 		if (!isValidInstruction(_instr))
-			ret << "0x" << hex << int(_instr) << " ";
+			ret << "0x" << std::uppercase << std::hex << int(_instr) << " ";
 		else
 		{
 			InstructionInfo info = instructionInfo(_instr);
 			ret << info.name << " ";
 			if (info.additional)
-				ret << "0x" << hex << _data << " ";
+				ret << "0x" << std::uppercase << std::hex << _data << " ";
 		}
 	});
 	return ret.str();

libevmasm/RuleList.h

@@ -49,7 +49,7 @@ template <class S> S modWorkaround(S const& _a, S const& _b)
 
 // This works around a bug fixed with Boost 1.64.
 // https://www.boost.org/doc/libs/1_68_0/libs/multiprecision/doc/html/boost_multiprecision/map/hist.html#boost_multiprecision.map.hist.multiprecision_2_3_1_boost_1_64
-inline u256 shlWorkaround(u256 const& _x, unsigned _amount)
+template <class S> S shlWorkaround(S const& _x, unsigned _amount)
 {
 	return u256((bigint(_x) << _amount) & u256(-1));
 }
@@ -66,44 +66,50 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart1(
 	Pattern
 )
 {
+	using Word = typename Pattern::Word;
 	return std::vector<SimplificationRule<Pattern>> {
 		// arithmetic on constants
-		{{Instruction::ADD, {A, B}}, [=]{ return A.d() + B.d(); }, false},
+		{{Pattern::Builtins::ADD, {A, B}}, [=]{ return A.d() + B.d(); }, false},
-		{{Instruction::MUL, {A, B}}, [=]{ return A.d() * B.d(); }, false},
+		{{Pattern::Builtins::MUL, {A, B}}, [=]{ return A.d() * B.d(); }, false},
-		{{Instruction::SUB, {A, B}}, [=]{ return A.d() - B.d(); }, false},
+		{{Pattern::Builtins::SUB, {A, B}}, [=]{ return A.d() - B.d(); }, false},
-		{{Instruction::DIV, {A, B}}, [=]{ return B.d() == 0 ? 0 : divWorkaround(A.d(), B.d()); }, false},
+		{{Pattern::Builtins::DIV, {A, B}}, [=]{ return B.d() == 0 ? 0 : divWorkaround(A.d(), B.d()); }, false},
-		{{Instruction::SDIV, {A, B}}, [=]{ return B.d() == 0 ? 0 : s2u(divWorkaround(u2s(A.d()), u2s(B.d()))); }, false},
+		{{Pattern::Builtins::SDIV, {A, B}}, [=]{ return B.d() == 0 ? 0 : s2u(divWorkaround(u2s(A.d()), u2s(B.d()))); }, false},
-		{{Instruction::MOD, {A, B}}, [=]{ return B.d() == 0 ? 0 : modWorkaround(A.d(), B.d()); }, false},
+		{{Pattern::Builtins::MOD, {A, B}}, [=]{ return B.d() == 0 ? 0 : modWorkaround(A.d(), B.d()); }, false},
-		{{Instruction::SMOD, {A, B}}, [=]{ return B.d() == 0 ? 0 : s2u(modWorkaround(u2s(A.d()), u2s(B.d()))); }, false},
+		{{Pattern::Builtins::SMOD, {A, B}}, [=]{ return B.d() == 0 ? 0 : s2u(modWorkaround(u2s(A.d()), u2s(B.d()))); }, false},
-		{{Instruction::EXP, {A, B}}, [=]{ return u256(boost::multiprecision::powm(bigint(A.d()), bigint(B.d()), bigint(1) << 256)); }, false},
+		{{Pattern::Builtins::EXP, {A, B}}, [=]{ return Word(boost::multiprecision::powm(bigint(A.d()), bigint(B.d()), bigint(1) << Pattern::WordSize)); }, false},
-		{{Instruction::NOT, {A}}, [=]{ return ~A.d(); }, false},
+		{{Pattern::Builtins::NOT, {A}}, [=]{ return ~A.d(); }, false},
-		{{Instruction::LT, {A, B}}, [=]() -> u256 { return A.d() < B.d() ? 1 : 0; }, false},
+		{{Pattern::Builtins::LT, {A, B}}, [=]() -> Word { return A.d() < B.d() ? 1 : 0; }, false},
-		{{Instruction::GT, {A, B}}, [=]() -> u256 { return A.d() > B.d() ? 1 : 0; }, false},
+		{{Pattern::Builtins::GT, {A, B}}, [=]() -> Word { return A.d() > B.d() ? 1 : 0; }, false},
-		{{Instruction::SLT, {A, B}}, [=]() -> u256 { return u2s(A.d()) < u2s(B.d()) ? 1 : 0; }, false},
+		{{Pattern::Builtins::SLT, {A, B}}, [=]() -> Word { return u2s(A.d()) < u2s(B.d()) ? 1 : 0; }, false},
-		{{Instruction::SGT, {A, B}}, [=]() -> u256 { return u2s(A.d()) > u2s(B.d()) ? 1 : 0; }, false},
+		{{Pattern::Builtins::SGT, {A, B}}, [=]() -> Word { return u2s(A.d()) > u2s(B.d()) ? 1 : 0; }, false},
-		{{Instruction::EQ, {A, B}}, [=]() -> u256 { return A.d() == B.d() ? 1 : 0; }, false},
+		{{Pattern::Builtins::EQ, {A, B}}, [=]() -> Word { return A.d() == B.d() ? 1 : 0; }, false},
-		{{Instruction::ISZERO, {A}}, [=]() -> u256 { return A.d() == 0 ? 1 : 0; }, false},
+		{{Pattern::Builtins::ISZERO, {A}}, [=]() -> Word { return A.d() == 0 ? 1 : 0; }, false},
-		{{Instruction::AND, {A, B}}, [=]{ return A.d() & B.d(); }, false},
+		{{Pattern::Builtins::AND, {A, B}}, [=]{ return A.d() & B.d(); }, false},
-		{{Instruction::OR, {A, B}}, [=]{ return A.d() | B.d(); }, false},
+		{{Pattern::Builtins::OR, {A, B}}, [=]{ return A.d() | B.d(); }, false},
-		{{Instruction::XOR, {A, B}}, [=]{ return A.d() ^ B.d(); }, false},
+		{{Pattern::Builtins::XOR, {A, B}}, [=]{ return A.d() ^ B.d(); }, false},
-		{{Instruction::BYTE, {A, B}}, [=]{ return A.d() >= 32 ? 0 : (B.d() >> unsigned(8 * (31 - A.d()))) & 0xff; }, false},
+		{{Pattern::Builtins::BYTE, {A, B}}, [=]{
-		{{Instruction::ADDMOD, {A, B, C}}, [=]{ return C.d() == 0 ? 0 : u256((bigint(A.d()) + bigint(B.d())) % C.d()); }, false},
+			return
-		{{Instruction::MULMOD, {A, B, C}}, [=]{ return C.d() == 0 ? 0 : u256((bigint(A.d()) * bigint(B.d())) % C.d()); }, false},
+				A.d() >= Pattern::WordSize / 8 ?
-		{{Instruction::SIGNEXTEND, {A, B}}, [=]() -> u256 {
+				0 :
-			if (A.d() >= 31)
+				(B.d() >> unsigned(8 * (Pattern::WordSize / 8 - 1 - A.d()))) & 0xff;
+		}, false},
+		{{Pattern::Builtins::ADDMOD, {A, B, C}}, [=]{ return C.d() == 0 ? 0 : Word((bigint(A.d()) + bigint(B.d())) % C.d()); }, false},
+		{{Pattern::Builtins::MULMOD, {A, B, C}}, [=]{ return C.d() == 0 ? 0 : Word((bigint(A.d()) * bigint(B.d())) % C.d()); }, false},
+		{{Pattern::Builtins::SIGNEXTEND, {A, B}}, [=]() -> Word {
+			if (A.d() >= Pattern::WordSize / 8 - 1)
 				return B.d();
 			unsigned testBit = unsigned(A.d()) * 8 + 7;
-			u256 mask = (u256(1) << testBit) - 1;
+			Word mask = (Word(1) << testBit) - 1;
 			return boost::multiprecision::bit_test(B.d(), testBit) ? B.d() | ~mask : B.d() & mask;
 		}, false},
-		{{Instruction::SHL, {A, B}}, [=]{
+		{{Pattern::Builtins::SHL, {A, B}}, [=]{
-			if (A.d() > 255)
+			if (A.d() >= Pattern::WordSize)
-				return u256(0);
+				return Word(0);
 			return shlWorkaround(B.d(), unsigned(A.d()));
 		}, false},
-		{{Instruction::SHR, {A, B}}, [=]{
+		{{Pattern::Builtins::SHR, {A, B}}, [=]{
-			if (A.d() > 255)
+			if (A.d() >= Pattern::WordSize)
-				return u256(0);
+				return Word(0);
 			return B.d() >> unsigned(A.d());
 		}, false}
 	};
@@ -118,50 +124,51 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart2(
 	Pattern Y
 )
 {
+	using Word = typename Pattern::Word;
 	return std::vector<SimplificationRule<Pattern>> {
 		// invariants involving known constants
-		{{Instruction::ADD, {X, 0}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::ADD, {X, 0}}, [=]{ return X; }, false},
-		{{Instruction::ADD, {0, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::ADD, {0, X}}, [=]{ return X; }, false},
-		{{Instruction::SUB, {X, 0}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::SUB, {X, 0}}, [=]{ return X; }, false},
-		{{Instruction::SUB, {~u256(0), X}}, [=]() -> Pattern { return {Instruction::NOT, {X}}; }, false},
+		{{Pattern::Builtins::SUB, {~Word(0), X}}, [=]() -> Pattern { return {Pattern::Builtins::NOT, {X}}; }, false},
-		{{Instruction::MUL, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::MUL, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::MUL, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::MUL, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::MUL, {X, 1}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::MUL, {X, 1}}, [=]{ return X; }, false},
-		{{Instruction::MUL, {1, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::MUL, {1, X}}, [=]{ return X; }, false},
-		{{Instruction::MUL, {X, u256(-1)}}, [=]() -> Pattern { return {Instruction::SUB, {0, X}}; }, false},
+		{{Pattern::Builtins::MUL, {X, Word(-1)}}, [=]() -> Pattern { return {Pattern::Builtins::SUB, {0, X}}; }, false},
-		{{Instruction::MUL, {u256(-1), X}}, [=]() -> Pattern { return {Instruction::SUB, {0, X}}; }, false},
+		{{Pattern::Builtins::MUL, {Word(-1), X}}, [=]() -> Pattern { return {Pattern::Builtins::SUB, {0, X}}; }, false},
-		{{Instruction::DIV, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::DIV, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::DIV, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::DIV, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::DIV, {X, 1}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::DIV, {X, 1}}, [=]{ return X; }, false},
-		{{Instruction::SDIV, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SDIV, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::SDIV, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SDIV, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::SDIV, {X, 1}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::SDIV, {X, 1}}, [=]{ return X; }, false},
-		{{Instruction::AND, {X, ~u256(0)}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::AND, {X, ~Word(0)}}, [=]{ return X; }, false},
-		{{Instruction::AND, {~u256(0), X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::AND, {~Word(0), X}}, [=]{ return X; }, false},
-		{{Instruction::AND, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::AND, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::AND, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::AND, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::OR, {X, 0}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::OR, {X, 0}}, [=]{ return X; }, false},
-		{{Instruction::OR, {0, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::OR, {0, X}}, [=]{ return X; }, false},
-		{{Instruction::OR, {X, ~u256(0)}}, [=]{ return ~u256(0); }, true},
+		{{Pattern::Builtins::OR, {X, ~Word(0)}}, [=]{ return ~Word(0); }, true},
-		{{Instruction::OR, {~u256(0), X}}, [=]{ return ~u256(0); }, true},
+		{{Pattern::Builtins::OR, {~Word(0), X}}, [=]{ return ~Word(0); }, true},
-		{{Instruction::XOR, {X, 0}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::XOR, {X, 0}}, [=]{ return X; }, false},
-		{{Instruction::XOR, {0, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::XOR, {0, X}}, [=]{ return X; }, false},
-		{{Instruction::MOD, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::MOD, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::MOD, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::MOD, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::EQ, {X, 0}}, [=]() -> Pattern { return {Instruction::ISZERO, {X}}; }, false },
+		{{Pattern::Builtins::EQ, {X, 0}}, [=]() -> Pattern { return {Pattern::Builtins::ISZERO, {X}}; }, false },
-		{{Instruction::EQ, {0, X}}, [=]() -> Pattern { return {Instruction::ISZERO, {X}}; }, false },
+		{{Pattern::Builtins::EQ, {0, X}}, [=]() -> Pattern { return {Pattern::Builtins::ISZERO, {X}}; }, false },
-		{{Instruction::SHL, {0, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::SHL, {0, X}}, [=]{ return X; }, false},
-		{{Instruction::SHR, {0, X}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::SHR, {0, X}}, [=]{ return X; }, false},
-		{{Instruction::SHL, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SHL, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::SHR, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SHR, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::GT, {X, 0}}, [=]() -> Pattern { return {Instruction::ISZERO, {{Instruction::ISZERO, {X}}}}; }, false},
+		{{Pattern::Builtins::GT, {X, 0}}, [=]() -> Pattern { return {Pattern::Builtins::ISZERO, {{Pattern::Builtins::ISZERO, {X}}}}; }, false},
-		{{Instruction::LT, {0, X}}, [=]() -> Pattern { return {Instruction::ISZERO, {{Instruction::ISZERO, {X}}}}; }, false},
+		{{Pattern::Builtins::LT, {0, X}}, [=]() -> Pattern { return {Pattern::Builtins::ISZERO, {{Pattern::Builtins::ISZERO, {X}}}}; }, false},
-		{{Instruction::GT, {X, ~u256(0)}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::GT, {X, ~Word(0)}}, [=]{ return Word(0); }, true},
-		{{Instruction::LT, {~u256(0), X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::LT, {~Word(0), X}}, [=]{ return Word(0); }, true},
-		{{Instruction::GT, {0, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::GT, {0, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::LT, {X, 0}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::LT, {X, 0}}, [=]{ return Word(0); }, true},
-		{{Instruction::AND, {{Instruction::BYTE, {X, Y}}, {u256(0xff)}}}, [=]() -> Pattern { return {Instruction::BYTE, {X, Y}}; }, false},
+		{{Pattern::Builtins::AND, {{Pattern::Builtins::BYTE, {X, Y}}, {Word(0xff)}}}, [=]() -> Pattern { return {Pattern::Builtins::BYTE, {X, Y}}; }, false},
-		{{Instruction::BYTE, {31, X}}, [=]() -> Pattern { return {Instruction::AND, {X, u256(0xff)}}; }, false}
+		{{Pattern::Builtins::BYTE, {Pattern::WordSize / 8 - 1, X}}, [=]() -> Pattern { return {Pattern::Builtins::AND, {X, Word(0xff)}}; }, false}
 	};
 }
 
@@ -174,18 +181,19 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart3(
 	Pattern
 )
 {
+	using Word = typename Pattern::Word;
 	return std::vector<SimplificationRule<Pattern>> {
 		// operations involving an expression and itself
-		{{Instruction::AND, {X, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::AND, {X, X}}, [=]{ return X; }, true},
-		{{Instruction::OR, {X, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::OR, {X, X}}, [=]{ return X; }, true},
-		{{Instruction::XOR, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::XOR, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::SUB, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SUB, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::EQ, {X, X}}, [=]{ return u256(1); }, true},
+		{{Pattern::Builtins::EQ, {X, X}}, [=]{ return Word(1); }, true},
-		{{Instruction::LT, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::LT, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::SLT, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SLT, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::GT, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::GT, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::SGT, {X, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::SGT, {X, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::MOD, {X, X}}, [=]{ return u256(0); }, true}
+		{{Pattern::Builtins::MOD, {X, X}}, [=]{ return Word(0); }, true}
 	};
 }
 
@@ -198,25 +206,26 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart4(
 	Pattern Y
 )
 {
+	using Word = typename Pattern::Word;
 	return std::vector<SimplificationRule<Pattern>> {
 		// logical instruction combinations
-		{{Instruction::NOT, {{Instruction::NOT, {X}}}}, [=]{ return X; }, false},
+		{{Pattern::Builtins::NOT, {{Pattern::Builtins::NOT, {X}}}}, [=]{ return X; }, false},
-		{{Instruction::XOR, {X, {Instruction::XOR, {X, Y}}}}, [=]{ return Y; }, true},
+		{{Pattern::Builtins::XOR, {X, {Pattern::Builtins::XOR, {X, Y}}}}, [=]{ return Y; }, true},
-		{{Instruction::XOR, {X, {Instruction::XOR, {Y, X}}}}, [=]{ return Y; }, true},
+		{{Pattern::Builtins::XOR, {X, {Pattern::Builtins::XOR, {Y, X}}}}, [=]{ return Y; }, true},
-		{{Instruction::XOR, {{Instruction::XOR, {X, Y}}, X}}, [=]{ return Y; }, true},
+		{{Pattern::Builtins::XOR, {{Pattern::Builtins::XOR, {X, Y}}, X}}, [=]{ return Y; }, true},
-		{{Instruction::XOR, {{Instruction::XOR, {Y, X}}, X}}, [=]{ return Y; }, true},
+		{{Pattern::Builtins::XOR, {{Pattern::Builtins::XOR, {Y, X}}, X}}, [=]{ return Y; }, true},
-		{{Instruction::OR, {X, {Instruction::AND, {X, Y}}}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::OR, {X, {Pattern::Builtins::AND, {X, Y}}}}, [=]{ return X; }, true},
-		{{Instruction::OR, {X, {Instruction::AND, {Y, X}}}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::OR, {X, {Pattern::Builtins::AND, {Y, X}}}}, [=]{ return X; }, true},
-		{{Instruction::OR, {{Instruction::AND, {X, Y}}, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::OR, {{Pattern::Builtins::AND, {X, Y}}, X}}, [=]{ return X; }, true},
-		{{Instruction::OR, {{Instruction::AND, {Y, X}}, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::OR, {{Pattern::Builtins::AND, {Y, X}}, X}}, [=]{ return X; }, true},
-		{{Instruction::AND, {X, {Instruction::OR, {X, Y}}}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::AND, {X, {Pattern::Builtins::OR, {X, Y}}}}, [=]{ return X; }, true},
-		{{Instruction::AND, {X, {Instruction::OR, {Y, X}}}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::AND, {X, {Pattern::Builtins::OR, {Y, X}}}}, [=]{ return X; }, true},
-		{{Instruction::AND, {{Instruction::OR, {X, Y}}, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::AND, {{Pattern::Builtins::OR, {X, Y}}, X}}, [=]{ return X; }, true},
-		{{Instruction::AND, {{Instruction::OR, {Y, X}}, X}}, [=]{ return X; }, true},
+		{{Pattern::Builtins::AND, {{Pattern::Builtins::OR, {Y, X}}, X}}, [=]{ return X; }, true},
-		{{Instruction::AND, {X, {Instruction::NOT, {X}}}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::AND, {X, {Pattern::Builtins::NOT, {X}}}}, [=]{ return Word(0); }, true},
-		{{Instruction::AND, {{Instruction::NOT, {X}}, X}}, [=]{ return u256(0); }, true},
+		{{Pattern::Builtins::AND, {{Pattern::Builtins::NOT, {X}}, X}}, [=]{ return Word(0); }, true},
-		{{Instruction::OR, {X, {Instruction::NOT, {X}}}}, [=]{ return ~u256(0); }, true},
+		{{Pattern::Builtins::OR, {X, {Pattern::Builtins::NOT, {X}}}}, [=]{ return ~Word(0); }, true},
-		{{Instruction::OR, {{Instruction::NOT, {X}}, X}}, [=]{ return ~u256(0); }, true},
+		{{Pattern::Builtins::OR, {{Pattern::Builtins::NOT, {X}}, X}}, [=]{ return ~Word(0); }, true},
 	};
 }
 
@@ -230,58 +239,61 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart5(
 	Pattern
 )
 {
+	using Word = typename Pattern::Word;
+
 	std::vector<SimplificationRule<Pattern>> rules;
 
 	// Replace MOD X, <power-of-two> with AND X, <power-of-two> - 1
-	for (size_t i = 0; i < 256; ++i)
+	for (size_t i = 0; i < Pattern::WordSize; ++i)
 	{
-		u256 value = u256(1) << i;
+		Word value = Word(1) << i;
 		rules.push_back({
-			{Instruction::MOD, {X, value}},
+			{Pattern::Builtins::MOD, {X, value}},
-			[=]() -> Pattern { return {Instruction::AND, {X, value - 1}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::AND, {X, value - 1}}; },
 			false
 		});
 	}
 
 	// Replace SHL >=256, X with 0
 	rules.push_back({
-		{Instruction::SHL, {A, X}},
+		{Pattern::Builtins::SHL, {A, X}},
-		[=]() -> Pattern { return u256(0); },
+		[=]() -> Pattern { return Word(0); },
 		true,
-		[=]() { return A.d() >= 256; }
+		[=]() { return A.d() >= Pattern::WordSize; }
 	});
 
 	// Replace SHR >=256, X with 0
 	rules.push_back({
-		{Instruction::SHR, {A, X}},
+		{Pattern::Builtins::SHR, {A, X}},
-		[=]() -> Pattern { return u256(0); },
+		[=]() -> Pattern { return Word(0); },
 		true,
-		[=]() { return A.d() >= 256; }
+		[=]() { return A.d() >= Pattern::WordSize; }
 	});
 
 	// Replace BYTE(A, X), A >= 32 with 0
 	rules.push_back({
-		{Instruction::BYTE, {A, X}},
+		{Pattern::Builtins::BYTE, {A, X}},
-		[=]() -> Pattern { return u256(0); },
+		[=]() -> Pattern { return Word(0); },
 		true,
-		[=]() { return A.d() >= 32; }
+		[=]() { return A.d() >= Pattern::WordSize / 8; }
 	});
 
 	for (auto const& op: std::vector<Instruction>{
-		Instruction::ADDRESS,
+		Pattern::Builtins::ADDRESS,
-		Instruction::CALLER,
+		Pattern::Builtins::CALLER,
-		Instruction::ORIGIN,
+		Pattern::Builtins::ORIGIN,
-		Instruction::COINBASE
+		Pattern::Builtins::COINBASE
 	})
 	{
-		u256 const mask = (u256(1) << 160) - 1;
+		assertThrow(Pattern::WordSize > 160, OptimizerException, "");
+		Word const mask = (Word(1) << 160) - 1;
 		rules.push_back({
-			{Instruction::AND, {{op, mask}}},
+			{Pattern::Builtins::AND, {{op, mask}}},
 			[=]() -> Pattern { return op; },
 			false
 		});
 		rules.push_back({
-			{Instruction::AND, {{mask, op}}},
+			{Pattern::Builtins::AND, {{mask, op}}},
 			[=]() -> Pattern { return op; },
 			false
 		});
@@ -302,27 +314,27 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart6(
 	std::vector<SimplificationRule<Pattern>> rules;
 	// Double negation of opcodes with boolean result
 	for (auto const& op: std::vector<Instruction>{
-		Instruction::EQ,
+		Pattern::Builtins::EQ,
-		Instruction::LT,
+		Pattern::Builtins::LT,
-		Instruction::SLT,
+		Pattern::Builtins::SLT,
-		Instruction::GT,
+		Pattern::Builtins::GT,
-		Instruction::SGT
+		Pattern::Builtins::SGT
 	})
 		rules.push_back({
-			{Instruction::ISZERO, {{Instruction::ISZERO, {{op, {X, Y}}}}}},
+			{Pattern::Builtins::ISZERO, {{Pattern::Builtins::ISZERO, {{op, {X, Y}}}}}},
 			[=]() -> Pattern { return {op, {X, Y}}; },
 			false
 		});
 
 	rules.push_back({
-		{Instruction::ISZERO, {{Instruction::ISZERO, {{Instruction::ISZERO, {X}}}}}},
+		{Pattern::Builtins::ISZERO, {{Pattern::Builtins::ISZERO, {{Pattern::Builtins::ISZERO, {X}}}}}},
-		[=]() -> Pattern { return {Instruction::ISZERO, {X}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::ISZERO, {X}}; },
 		false
 	});
 
 	rules.push_back({
-		{Instruction::ISZERO, {{Instruction::XOR, {X, Y}}}},
+		{Pattern::Builtins::ISZERO, {{Pattern::Builtins::XOR, {X, Y}}}},
-		[=]() -> Pattern { return { Instruction::EQ, {X, Y} }; },
+		[=]() -> Pattern { return { Pattern::Builtins::EQ, {X, Y} }; },
 		false
 	});
 
@@ -338,14 +350,15 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart7(
 	Pattern Y
 )
 {
+	using Word = typename Pattern::Word;
 	std::vector<SimplificationRule<Pattern>> rules;
 	// Associative operations
-	for (auto const& opFun: std::vector<std::pair<Instruction,std::function<u256(u256 const&,u256 const&)>>>{
+	for (auto const& opFun: std::vector<std::pair<Instruction,std::function<Word(Word const&,Word const&)>>>{
-		{Instruction::ADD, std::plus<u256>()},
+		{Pattern::Builtins::ADD, std::plus<Word>()},
-		{Instruction::MUL, std::multiplies<u256>()},
+		{Pattern::Builtins::MUL, std::multiplies<Word>()},
-		{Instruction::AND, std::bit_and<u256>()},
+		{Pattern::Builtins::AND, std::bit_and<Word>()},
-		{Instruction::OR, std::bit_or<u256>()},
+		{Pattern::Builtins::OR, std::bit_or<Word>()},
-		{Instruction::XOR, std::bit_xor<u256>()}
+		{Pattern::Builtins::XOR, std::bit_xor<Word>()}
 	})
 	{
 		auto op = opFun.first;
@@ -382,13 +395,13 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart7(
 	// Combine two SHL by constant
 	rules.push_back({
 		// SHL(B, SHL(A, X)) -> SHL(min(A+B, 256), X)
-		{Instruction::SHL, {{B}, {Instruction::SHL, {{A}, {X}}}}},
+		{Pattern::Builtins::SHL, {{B}, {Pattern::Builtins::SHL, {{A}, {X}}}}},
 		[=]() -> Pattern {
 			bigint sum = bigint(A.d()) + B.d();
-			if (sum >= 256)
+			if (sum >= Pattern::WordSize)
-				return {Instruction::AND, {X, u256(0)}};
+				return {Pattern::Builtins::AND, {X, Word(0)}};
 			else
-				return {Instruction::SHL, {u256(sum), X}};
+				return {Pattern::Builtins::SHL, {Word(sum), X}};
 		},
 		false
 	});
@@ -396,13 +409,13 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart7(
 	// Combine two SHR by constant
 	rules.push_back({
 		// SHR(B, SHR(A, X)) -> SHR(min(A+B, 256), X)
-		{Instruction::SHR, {{B}, {Instruction::SHR, {{A}, {X}}}}},
+		{Pattern::Builtins::SHR, {{B}, {Pattern::Builtins::SHR, {{A}, {X}}}}},
 		[=]() -> Pattern {
 			bigint sum = bigint(A.d()) + B.d();
-			if (sum >= 256)
+			if (sum >= Pattern::WordSize)
-				return {Instruction::AND, {X, u256(0)}};
+				return {Pattern::Builtins::AND, {X, Word(0)}};
 			else
-				return {Instruction::SHR, {u256(sum), X}};
+				return {Pattern::Builtins::SHR, {Word(sum), X}};
 		},
 		false
 	});
@@ -410,112 +423,112 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart7(
 	// Combine SHL-SHR by constant
 	rules.push_back({
 		// SHR(B, SHL(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask)
-		{Instruction::SHR, {{B}, {Instruction::SHL, {{A}, {X}}}}},
+		{Pattern::Builtins::SHR, {{B}, {Pattern::Builtins::SHL, {{A}, {X}}}}},
 		[=]() -> Pattern {
-			u256 mask = shlWorkaround(u256(-1), unsigned(A.d())) >> unsigned(B.d());
+			Word mask = shlWorkaround(~Word(0), unsigned(A.d())) >> unsigned(B.d());
 
 			if (A.d() > B.d())
-				return {Instruction::AND, {{Instruction::SHL, {A.d() - B.d(), X}}, mask}};
+				return {Pattern::Builtins::AND, {{Pattern::Builtins::SHL, {A.d() - B.d(), X}}, mask}};
 			else if (B.d() > A.d())
-				return {Instruction::AND, {{Instruction::SHR, {B.d() - A.d(), X}}, mask}};
+				return {Pattern::Builtins::AND, {{Pattern::Builtins::SHR, {B.d() - A.d(), X}}, mask}};
 			else
-				return {Instruction::AND, {X, mask}};
+				return {Pattern::Builtins::AND, {X, mask}};
 		},
 		false,
-		[=] { return A.d() < 256 && B.d() < 256; }
+		[=] { return A.d() < Pattern::WordSize && B.d() < Pattern::WordSize; }
 	});
 
 	// Combine SHR-SHL by constant
 	rules.push_back({
 		// SHL(B, SHR(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask)
-		{Instruction::SHL, {{B}, {Instruction::SHR, {{A}, {X}}}}},
+		{Pattern::Builtins::SHL, {{B}, {Pattern::Builtins::SHR, {{A}, {X}}}}},
 		[=]() -> Pattern {
-			u256 mask = shlWorkaround(u256(-1) >> unsigned(A.d()), unsigned(B.d()));
+			Word mask = shlWorkaround((~Word(0)) >> unsigned(A.d()), unsigned(B.d()));
 
 			if (A.d() > B.d())
-				return {Instruction::AND, {{Instruction::SHR, {A.d() - B.d(), X}}, mask}};
+				return {Pattern::Builtins::AND, {{Pattern::Builtins::SHR, {A.d() - B.d(), X}}, mask}};
 			else if (B.d() > A.d())
-				return {Instruction::AND, {{Instruction::SHL, {B.d() - A.d(), X}}, mask}};
+				return {Pattern::Builtins::AND, {{Pattern::Builtins::SHL, {B.d() - A.d(), X}}, mask}};
 			else
-				return {Instruction::AND, {X, mask}};
+				return {Pattern::Builtins::AND, {X, mask}};
 		},
 		false,
-		[=] { return A.d() < 256 && B.d() < 256; }
+		[=] { return A.d() < Pattern::WordSize && B.d() < Pattern::WordSize; }
 	});
 
 	// Move AND with constant across SHL and SHR by constant
-	for (auto shiftOp: {Instruction::SHL, Instruction::SHR})
+	for (auto shiftOp: {Pattern::Builtins::SHL, Pattern::Builtins::SHR})
 	{
 		auto replacement = [=]() -> Pattern {
-			u256 mask =
+			Word mask =
-				shiftOp == Instruction::SHL ?
+				shiftOp == Pattern::Builtins::SHL ?
 				shlWorkaround(A.d(), unsigned(B.d())) :
 				A.d() >> unsigned(B.d());
-			return {Instruction::AND, {{shiftOp, {B.d(), X}}, std::move(mask)}};
+			return {Pattern::Builtins::AND, {{shiftOp, {B.d(), X}}, std::move(mask)}};
 		};
 		rules.push_back({
 			// SH[L/R](B, AND(X, A)) -> AND(SH[L/R](B, X), [ A << B / A >> B ])
-			{shiftOp, {{B}, {Instruction::AND, {{X}, {A}}}}},
+			{shiftOp, {{B}, {Pattern::Builtins::AND, {{X}, {A}}}}},
 			replacement,
 			false,
-			[=] { return B.d() < 256; }
+			[=] { return B.d() < Pattern::WordSize; }
 		});
 		rules.push_back({
 			// SH[L/R](B, AND(A, X)) -> AND(SH[L/R](B, X), [ A << B / A >> B ])
-			{shiftOp, {{B}, {Instruction::AND, {{A}, {X}}}}},
+			{shiftOp, {{B}, {Pattern::Builtins::AND, {{A}, {X}}}}},
 			replacement,
 			false,
-			[=] { return B.d() < 256; }
+			[=] { return B.d() < Pattern::WordSize; }
 		});
 	}
 
 	rules.push_back({
 		// MUL(X, SHL(Y, 1)) -> SHL(Y, X)
-		{Instruction::MUL, {X, {Instruction::SHL, {Y, u256(1)}}}},
+		{Pattern::Builtins::MUL, {X, {Pattern::Builtins::SHL, {Y, Word(1)}}}},
 		[=]() -> Pattern {
-			return {Instruction::SHL, {Y, X}};
+			return {Pattern::Builtins::SHL, {Y, X}};
 		},
 		// Actually only changes the order, does not remove.
 		true
 	});
 	rules.push_back({
 		// MUL(SHL(X, 1), Y) -> SHL(X, Y)
-		{Instruction::MUL, {{Instruction::SHL, {X, u256(1)}}, Y}},
+		{Pattern::Builtins::MUL, {{Pattern::Builtins::SHL, {X, Word(1)}}, Y}},
 		[=]() -> Pattern {
-			return {Instruction::SHL, {X, Y}};
+			return {Pattern::Builtins::SHL, {X, Y}};
 		},
 		false
 	});
 
 	rules.push_back({
 		// DIV(X, SHL(Y, 1)) -> SHR(Y, X)
-		{Instruction::DIV, {X, {Instruction::SHL, {Y, u256(1)}}}},
+		{Pattern::Builtins::DIV, {X, {Pattern::Builtins::SHL, {Y, Word(1)}}}},
 		[=]() -> Pattern {
-			return {Instruction::SHR, {Y, X}};
+			return {Pattern::Builtins::SHR, {Y, X}};
 		},
 		// Actually only changes the order, does not remove.
 		true
 	});
 
 	std::function<bool()> feasibilityFunction = [=]() {
-		if (B.d() > 256)
+		if (B.d() > Pattern::WordSize)
 			return false;
 		unsigned bAsUint = static_cast<unsigned>(B.d());
-		return (A.d() & (u256(-1) >> bAsUint)) == (u256(-1) >> bAsUint);
+		return (A.d() & ((~Word(0)) >> bAsUint)) == ((~Word(0)) >> bAsUint);
 	};
 
 	rules.push_back({
 		// AND(A, SHR(B, X)) -> A & ((2^256-1) >> B) == ((2^256-1) >> B)
-		{Instruction::AND, {A, {Instruction::SHR, {B, X}}}},
+		{Pattern::Builtins::AND, {A, {Pattern::Builtins::SHR, {B, X}}}},
-		[=]() -> Pattern { return {Instruction::SHR, {B, X}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::SHR, {B, X}}; },
 		false,
 		feasibilityFunction
 	});
 
 	rules.push_back({
 		// AND(SHR(B, X), A) -> ((2^256-1) >> B) & A == ((2^256-1) >> B)
-		{Instruction::AND, {{Instruction::SHR, {B, X}}, A}},
+		{Pattern::Builtins::AND, {{Pattern::Builtins::SHR, {B, X}}, A}},
-		[=]() -> Pattern { return {Instruction::SHR, {B, X}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::SHR, {B, X}}; },
 		false,
 		feasibilityFunction
 	});
@@ -538,28 +551,28 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart8(
 	rules += std::vector<SimplificationRule<Pattern>>{
 		{
 			// X - A -> X + (-A)
-			{Instruction::SUB, {X, A}},
+			{Pattern::Builtins::SUB, {X, A}},
-			[=]() -> Pattern { return {Instruction::ADD, {X, 0 - A.d()}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::ADD, {X, 0 - A.d()}}; },
 			false
 		}, {
 			// (X + A) - Y -> (X - Y) + A
-			{Instruction::SUB, {{Instruction::ADD, {X, A}}, Y}},
+			{Pattern::Builtins::SUB, {{Pattern::Builtins::ADD, {X, A}}, Y}},
-			[=]() -> Pattern { return {Instruction::ADD, {{Instruction::SUB, {X, Y}}, A}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::ADD, {{Pattern::Builtins::SUB, {X, Y}}, A}}; },
 			false
 		}, {
 			// (A + X) - Y -> (X - Y) + A
-			{Instruction::SUB, {{Instruction::ADD, {A, X}}, Y}},
+			{Pattern::Builtins::SUB, {{Pattern::Builtins::ADD, {A, X}}, Y}},
-			[=]() -> Pattern { return {Instruction::ADD, {{Instruction::SUB, {X, Y}}, A}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::ADD, {{Pattern::Builtins::SUB, {X, Y}}, A}}; },
 			false
 		}, {
 			// X - (Y + A) -> (X - Y) + (-A)
-			{Instruction::SUB, {X, {Instruction::ADD, {Y, A}}}},
+			{Pattern::Builtins::SUB, {X, {Pattern::Builtins::ADD, {Y, A}}}},
-			[=]() -> Pattern { return {Instruction::ADD, {{Instruction::SUB, {X, Y}}, 0 - A.d()}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::ADD, {{Pattern::Builtins::SUB, {X, Y}}, 0 - A.d()}}; },
 			false
 		}, {
 			// X - (A + Y) -> (X - Y) + (-A)
-			{Instruction::SUB, {X, {Instruction::ADD, {A, Y}}}},
+			{Pattern::Builtins::SUB, {X, {Pattern::Builtins::ADD, {A, Y}}}},
-			[=]() -> Pattern { return {Instruction::ADD, {{Instruction::SUB, {X, Y}}, 0 - A.d()}}; },
+			[=]() -> Pattern { return {Pattern::Builtins::ADD, {{Pattern::Builtins::SUB, {X, Y}}, 0 - A.d()}}; },
 			false
 		}
 	};
@@ -577,29 +590,31 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart9(
 	Pattern Z
 )
 {
+	using Word = typename Pattern::Word;
 	std::vector<SimplificationRule<Pattern>> rules;
 
-	u256 const mask = (u256(1) << 160) - 1;
+	assertThrow(Pattern::WordSize > 160, OptimizerException, "");
+	Word const mask = (Word(1) << 160) - 1;
 	// CREATE
 	rules.push_back({
-		{Instruction::AND, {{Instruction::CREATE, {W, X, Y}}, mask}},
+		{Pattern::Builtins::AND, {{Pattern::Builtins::CREATE, {W, X, Y}}, mask}},
-		[=]() -> Pattern { return {Instruction::CREATE, {W, X, Y}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::CREATE, {W, X, Y}}; },
 		false
 	});
 	rules.push_back({
-		{Instruction::AND, {{mask, {Instruction::CREATE, {W, X, Y}}}}},
+		{Pattern::Builtins::AND, {{mask, {Pattern::Builtins::CREATE, {W, X, Y}}}}},
-		[=]() -> Pattern { return {Instruction::CREATE, {W, X, Y}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::CREATE, {W, X, Y}}; },
 		false
 	});
 	// CREATE2
 	rules.push_back({
-		{Instruction::AND, {{Instruction::CREATE2, {W, X, Y, Z}}, mask}},
+		{Pattern::Builtins::AND, {{Pattern::Builtins::CREATE2, {W, X, Y, Z}}, mask}},
-		[=]() -> Pattern { return {Instruction::CREATE2, {W, X, Y, Z}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::CREATE2, {W, X, Y, Z}}; },
 		false
 	});
 	rules.push_back({
-		{Instruction::AND, {{mask, {Instruction::CREATE2, {W, X, Y, Z}}}}},
+		{Pattern::Builtins::AND, {{mask, {Pattern::Builtins::CREATE2, {W, X, Y, Z}}}}},
-		[=]() -> Pattern { return {Instruction::CREATE2, {W, X, Y, Z}}; },
+		[=]() -> Pattern { return {Pattern::Builtins::CREATE2, {W, X, Y, Z}}; },
 		false
 	});
 
@@ -621,6 +636,14 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleList(
 	Pattern Z
 )
 {
+	using Word = typename Pattern::Word;
+	// Some sanity checks
+	assertThrow(Pattern::WordSize % 8 == 0, OptimizerException, "");
+	assertThrow(Pattern::WordSize >= 8, OptimizerException, "");
+	assertThrow(Pattern::WordSize <= 256, OptimizerException, "");
+	assertThrow(Word(-1) == ~Word(0), OptimizerException, "");
+	assertThrow(Word(-1) + 1 == Word(0), OptimizerException, "");
+
 	std::vector<SimplificationRule<Pattern>> rules;
 	rules += simplificationRuleListPart1(A, B, C, W, X);
 	rules += simplificationRuleListPart2(A, B, C, W, X);

libevmasm/SimplificationRule.h

@@ -20,6 +20,7 @@
 
 #pragma once
 
+#include <libevmasm/Instruction.h>
 #include <functional>
 
 namespace dev
@@ -54,5 +55,85 @@ struct SimplificationRule
 	std::function<bool()> feasible;
 };
 
+struct EVMBuiltins
+{
+	using InstrType = Instruction;
+	static auto constexpr STOP = Instruction::STOP;
+	static auto constexpr ADD = Instruction::ADD;
+	static auto constexpr SUB = Instruction::SUB;
+	static auto constexpr MUL = Instruction::MUL;
+	static auto constexpr DIV = Instruction::DIV;
+	static auto constexpr SDIV = Instruction::SDIV;
+	static auto constexpr MOD = Instruction::MOD;
+	static auto constexpr SMOD = Instruction::SMOD;
+	static auto constexpr EXP = Instruction::EXP;
+	static auto constexpr NOT = Instruction::NOT;
+	static auto constexpr LT = Instruction::LT;
+	static auto constexpr GT = Instruction::GT;
+	static auto constexpr SLT = Instruction::SLT;
+	static auto constexpr SGT = Instruction::SGT;
+	static auto constexpr EQ = Instruction::EQ;
+	static auto constexpr ISZERO = Instruction::ISZERO;
+	static auto constexpr AND = Instruction::AND;
+	static auto constexpr OR = Instruction::OR;
+	static auto constexpr XOR = Instruction::XOR;
+	static auto constexpr BYTE = Instruction::BYTE;
+	static auto constexpr SHL = Instruction::SHL;
+	static auto constexpr SHR = Instruction::SHR;
+	static auto constexpr SAR = Instruction::SAR;
+	static auto constexpr ADDMOD = Instruction::ADDMOD;
+	static auto constexpr MULMOD = Instruction::MULMOD;
+	static auto constexpr SIGNEXTEND = Instruction::SIGNEXTEND;
+	static auto constexpr KECCAK256 = Instruction::KECCAK256;
+	static auto constexpr ADDRESS = Instruction::ADDRESS;
+	static auto constexpr BALANCE = Instruction::BALANCE;
+	static auto constexpr ORIGIN = Instruction::ORIGIN;
+	static auto constexpr CALLER = Instruction::CALLER;
+	static auto constexpr CALLVALUE = Instruction::CALLVALUE;
+	static auto constexpr CALLDATALOAD = Instruction::CALLDATALOAD;
+	static auto constexpr CALLDATASIZE = Instruction::CALLDATASIZE;
+	static auto constexpr CALLDATACOPY = Instruction::CALLDATACOPY;
+	static auto constexpr CODESIZE = Instruction::CODESIZE;
+	static auto constexpr CODECOPY = Instruction::CODECOPY;
+	static auto constexpr GASPRICE = Instruction::GASPRICE;
+	static auto constexpr EXTCODESIZE = Instruction::EXTCODESIZE;
+	static auto constexpr EXTCODECOPY = Instruction::EXTCODECOPY;
+	static auto constexpr RETURNDATASIZE = Instruction::RETURNDATASIZE;
+	static auto constexpr RETURNDATACOPY = Instruction::RETURNDATACOPY;
+	static auto constexpr EXTCODEHASH = Instruction::EXTCODEHASH;
+	static auto constexpr BLOCKHASH = Instruction::BLOCKHASH;
+	static auto constexpr COINBASE = Instruction::COINBASE;
+	static auto constexpr TIMESTAMP = Instruction::TIMESTAMP;
+	static auto constexpr NUMBER = Instruction::NUMBER;
+	static auto constexpr DIFFICULTY = Instruction::DIFFICULTY;
+	static auto constexpr GASLIMIT = Instruction::GASLIMIT;
+	static auto constexpr CHAINID = Instruction::CHAINID;
+	static auto constexpr SELFBALANCE = Instruction::SELFBALANCE;
+	static auto constexpr POP = Instruction::POP;
+	static auto constexpr MLOAD = Instruction::MLOAD;
+	static auto constexpr MSTORE = Instruction::MSTORE;
+	static auto constexpr MSTORE8 = Instruction::MSTORE8;
+	static auto constexpr SLOAD = Instruction::SLOAD;
+	static auto constexpr SSTORE = Instruction::SSTORE;
+	static auto constexpr PC = Instruction::PC;
+	static auto constexpr MSIZE = Instruction::MSIZE;
+	static auto constexpr GAS = Instruction::GAS;
+	static auto constexpr LOG0 = Instruction::LOG0;
+	static auto constexpr LOG1 = Instruction::LOG1;
+	static auto constexpr LOG2 = Instruction::LOG2;
+	static auto constexpr LOG3 = Instruction::LOG3;
+	static auto constexpr LOG4 = Instruction::LOG4;
+	static auto constexpr CREATE = Instruction::CREATE;
+	static auto constexpr CALL = Instruction::CALL;
+	static auto constexpr CALLCODE = Instruction::CALLCODE;
+	static auto constexpr STATICCALL = Instruction::STATICCALL;
+	static auto constexpr RETURN = Instruction::RETURN;
+	static auto constexpr DELEGATECALL = Instruction::DELEGATECALL;
+	static auto constexpr CREATE2 = Instruction::CREATE2;
+	static auto constexpr REVERT = Instruction::REVERT;
+	static auto constexpr INVALID = Instruction::INVALID;
+	static auto constexpr SELFDESTRUCT = Instruction::SELFDESTRUCT;
+};
+
 }
 }

libevmasm/SimplificationRules.h

@@ -87,6 +87,10 @@ public:
 	using Expression = ExpressionClasses::Expression;
 	using Id = ExpressionClasses::Id;
 
+	using Builtins = dev::eth::EVMBuiltins;
+	static constexpr size_t WordSize = 256;
+	using Word = u256;
+
 	// Matches a specific constant value.
 	Pattern(unsigned _value): Pattern(u256(_value)) {}
 	// Matches a specific constant value.

liblangutil/EVMVersion.h

@@ -22,9 +22,9 @@
 
 #include <libevmasm/Instruction.h>
 
+#include <optional>
 #include <string>
 
-#include <boost/optional.hpp>
 #include <boost/operators.hpp>
 
 
@@ -51,12 +51,12 @@ public:
 	static EVMVersion istanbul() { return {Version::Istanbul}; }
 	static EVMVersion berlin() { return {Version::Berlin}; }
 
-	static boost::optional<EVMVersion> fromString(std::string const& _version)
+	static std::optional<EVMVersion> fromString(std::string const& _version)
 	{
 		for (auto const& v: {homestead(), tangerineWhistle(), spuriousDragon(), byzantium(), constantinople(), petersburg(), istanbul(), berlin()})
 			if (_version == v.name())
 				return v;
-		return {};
+		return std::nullopt;
 	}
 
 	bool operator==(EVMVersion const& _other) const { return m_version == _other.m_version; }

liblangutil/Exceptions.cpp

@@ -29,7 +29,7 @@ using namespace langutil;
 Error::Error(Type _type, SourceLocation const& _location, string const& _description):
 	m_type(_type)
 {
-	switch(m_type)
+	switch (m_type)
 	{
 	case Type::DeclarationError:
 		m_typeName = "DeclarationError";

liblangutil/Scanner.cpp

@@ -53,8 +53,9 @@
 #include <liblangutil/Common.h>
 #include <liblangutil/Exceptions.h>
 #include <liblangutil/Scanner.h>
-#include <boost/optional.hpp>
+
 #include <algorithm>
+#include <optional>
 #include <ostream>
 #include <tuple>
 
@@ -187,7 +188,7 @@ bool Scanner::scanHexByte(char& o_scannedByte)
 	return true;
 }
 
-boost::optional<unsigned> Scanner::scanUnicode()
+std::optional<unsigned> Scanner::scanUnicode()
 {
 	unsigned x = 0;
 	for (int i = 0; i < 4; i++)
@@ -718,7 +719,7 @@ bool Scanner::scanEscape()
 		break;
 	case 'u':
 	{
-		if (boost::optional<unsigned> codepoint = scanUnicode())
+		if (auto const codepoint = scanUnicode(); codepoint.has_value())
 			addUnicodeAsUTF8(*codepoint);
 		else
 			return false;

liblangutil/Scanner.h

@@ -57,6 +57,8 @@
 #include <liblangutil/SourceLocation.h>
 #include <libdevcore/Common.h>
 #include <libdevcore/CommonData.h>
+
+#include <optional>
 #include <iosfwd>
 
 namespace langutil
@@ -207,7 +209,7 @@ private:
 	inline Token selectToken(char _next, Token _then, Token _else);
 
 	bool scanHexByte(char& o_scannedByte);
-	boost::optional<unsigned> scanUnicode();
+	std::optional<unsigned> scanUnicode();
 
 	/// Scans a single Solidity token.
 	void scanToken();

libsolidity/CMakeLists.txt

@@ -79,6 +79,8 @@ set(sources
 	formal/BMC.h
 	formal/CHC.cpp
 	formal/CHC.h
+	formal/CHCSmtLib2Interface.cpp
+	formal/CHCSmtLib2Interface.h
 	formal/CHCSolverInterface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h
@@ -111,6 +113,8 @@ set(sources
 	interface/ReadFile.h
 	interface/StandardCompiler.cpp
 	interface/StandardCompiler.h
+	interface/StorageLayout.cpp
+	interface/StorageLayout.h
 	interface/Version.cpp
 	interface/Version.h
 	parsing/DocStringParser.cpp

libsolidity/analysis/ControlFlowBuilder.cpp

@@ -49,7 +49,7 @@ bool ControlFlowBuilder::visit(BinaryOperation const& _operation)
 {
 	solAssert(!!m_currentNode, "");
 
-	switch(_operation.getOperator())
+	switch (_operation.getOperator())
 	{
 		case Token::Or:
 		case Token::And:

libsolidity/analysis/NameAndTypeResolver.cpp

@@ -38,10 +38,12 @@ namespace solidity
 
 NameAndTypeResolver::NameAndTypeResolver(
 	GlobalContext& _globalContext,
+	langutil::EVMVersion _evmVersion,
 	map<ASTNode const*, shared_ptr<DeclarationContainer>>& _scopes,
 	ErrorReporter& _errorReporter
-) :
+):
 	m_scopes(_scopes),
+	m_evmVersion(_evmVersion),
 	m_errorReporter(_errorReporter),
 	m_globalContext(_globalContext)
 {
@@ -324,7 +326,7 @@ bool NameAndTypeResolver::resolveNamesAndTypesInternal(ASTNode& _node, bool _res
 	{
 		if (m_scopes.count(&_node))
 			setScope(&_node);
-		return ReferencesResolver(m_errorReporter, *this, _resolveInsideCode).resolve(_node);
+		return ReferencesResolver(m_errorReporter, *this, m_evmVersion, _resolveInsideCode).resolve(_node);
 	}
 }
 

libsolidity/analysis/NameAndTypeResolver.h

@@ -28,6 +28,8 @@
 #include <libsolidity/ast/ASTAnnotations.h>
 #include <libsolidity/ast/ASTVisitor.h>
 
+#include <liblangutil/EVMVersion.h>
+
 #include <boost/noncopyable.hpp>
 
 #include <list>
@@ -55,6 +57,7 @@ public:
 	/// are filled during the lifetime of this object.
 	NameAndTypeResolver(
 		GlobalContext& _globalContext,
+		langutil::EVMVersion _evmVersion,
 		std::map<ASTNode const*, std::shared_ptr<DeclarationContainer>>& _scopes,
 		langutil::ErrorReporter& _errorReporter
 	);
@@ -130,6 +133,7 @@ private:
 	/// Aliases (for example `import "x" as y;`) create multiple pointers to the same scope.
 	std::map<ASTNode const*, std::shared_ptr<DeclarationContainer>>& m_scopes;
 
+	langutil::EVMVersion m_evmVersion;
 	DeclarationContainer* m_currentScope = nullptr;
 	langutil::ErrorReporter& m_errorReporter;
 	GlobalContext& m_globalContext;

libsolidity/analysis/ReferencesResolver.cpp

@@ -122,11 +122,11 @@ bool ReferencesResolver::visit(ElementaryTypeName const& _typeName)
 	if (!_typeName.annotation().type)
 	{
 		_typeName.annotation().type = TypeProvider::fromElementaryTypeName(_typeName.typeName());
-		if (_typeName.stateMutability().is_initialized())
+		if (_typeName.stateMutability().has_value())
 		{
 			// for non-address types this was already caught by the parser
 			solAssert(_typeName.annotation().type->category() == Type::Category::Address, "");
-			switch(*_typeName.stateMutability())
+			switch (*_typeName.stateMutability())
 			{
 				case StateMutability::Payable:
 					_typeName.annotation().type = TypeProvider::payableAddress();
@@ -323,12 +323,12 @@ bool ReferencesResolver::visit(InlineAssembly const& _inlineAssembly)
 	// Will be re-generated later with correct information
 	// We use the latest EVM version because we will re-run it anyway.
 	yul::AsmAnalysisInfo analysisInfo;
-	boost::optional<Error::Type> errorTypeForLoose = Error::Type::SyntaxError;
+	std::optional<Error::Type> errorTypeForLoose = Error::Type::SyntaxError;
 	yul::AsmAnalyzer(
 		analysisInfo,
 		errorsIgnored,
 		errorTypeForLoose,
-		yul::EVMDialect::looseAssemblyForEVM(EVMVersion{}),
+		yul::EVMDialect::looseAssemblyForEVM(m_evmVersion),
 		resolver
 	).analyze(_inlineAssembly.operations());
 	return false;

libsolidity/analysis/ReferencesResolver.h

@@ -24,6 +24,7 @@
 
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/ast/ASTAnnotations.h>
+#include <liblangutil/EVMVersion.h>
 
 #include <boost/noncopyable.hpp>
 #include <list>
@@ -52,10 +53,12 @@ public:
 	ReferencesResolver(
 		langutil::ErrorReporter& _errorReporter,
 		NameAndTypeResolver& _resolver,
+		langutil::EVMVersion _evmVersion,
 		bool _resolveInsideCode = false
 	):
 		m_errorReporter(_errorReporter),
 		m_resolver(_resolver),
+		m_evmVersion(_evmVersion),
 		m_resolveInsideCode(_resolveInsideCode)
 	{}
 
@@ -96,6 +99,7 @@ private:
 
 	langutil::ErrorReporter& m_errorReporter;
 	NameAndTypeResolver& m_resolver;
+	langutil::EVMVersion m_evmVersion;
 	/// Stack of return parameters.
 	std::vector<ParameterList const*> m_returnParameters;
 	bool const m_resolveInsideCode;

libsolidity/analysis/StaticAnalyzer.cpp

@@ -227,7 +227,7 @@ bool StaticAnalyzer::visit(MemberAccess const& _memberAccess)
 	if (m_constructor)
 	{
 		auto const* expr = &_memberAccess.expression();
-		while(expr)
+		while (expr)
 		{
 			if (auto id = dynamic_cast<Identifier const*>(expr))
 			{

libsolidity/analysis/TypeChecker.cpp

@@ -390,11 +390,13 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 	set<Declaration const*> modifiers;
 	for (ASTPointer<ModifierInvocation> const& modifier: _function.modifiers())
 	{
+		auto baseContracts = dynamic_cast<ContractDefinition const&>(*_function.scope()).annotation().linearizedBaseContracts;
+		// Delete first base which is just the main contract itself
+		baseContracts.erase(baseContracts.begin());
+
 		visitManually(
 			*modifier,
-			_function.isConstructor() ?
+			_function.isConstructor() ? baseContracts : vector<ContractDefinition const*>()
-			dynamic_cast<ContractDefinition const&>(*_function.scope()).annotation().linearizedBaseContracts :
-			vector<ContractDefinition const*>()
 		);
 		Declaration const* decl = &dereference(*modifier->name());
 		if (modifiers.count(decl))
@@ -448,6 +450,9 @@ bool TypeChecker::visit(VariableDeclaration const& _variable)
 	TypePointer varType = _variable.annotation().type;
 	solAssert(!!varType, "Variable type not provided.");
 
+	if (auto contractType = dynamic_cast<ContractType const*>(varType))
+		if (contractType->contractDefinition().isLibrary())
+			m_errorReporter.typeError(_variable.location(), "The type of a variable cannot be a library.");
 	if (_variable.value())
 		expectType(*_variable.value(), *varType);
 	if (_variable.isConstant())
@@ -522,7 +527,12 @@ void TypeChecker::visitManually(
 		_modifier.arguments() ? *_modifier.arguments() : std::vector<ASTPointer<Expression>>();
 	for (ASTPointer<Expression> const& argument: arguments)
 		argument->accept(*this);
-	_modifier.name()->accept(*this);
+
+	{
+		m_insideModifierInvocation = true;
+		ScopeGuard resetFlag{[&] () { m_insideModifierInvocation = false; }};
+		_modifier.name()->accept(*this);
+	}
 
 	auto const* declaration = &dereference(*_modifier.name());
 	vector<ASTPointer<VariableDeclaration>> emptyParameterList;
@@ -695,6 +705,9 @@ bool TypeChecker::visit(InlineAssembly const& _inlineAssembly)
 		}
 		else if (_context == yul::IdentifierContext::LValue)
 		{
+			if (dynamic_cast<MagicVariableDeclaration const*>(declaration))
+				return size_t(-1);
+
 			m_errorReporter.typeError(_identifier.location, "Only local variables can be assigned to in inline assembly.");
 			return size_t(-1);
 		}
@@ -2342,12 +2355,30 @@ bool TypeChecker::visit(Identifier const& _identifier)
 				if (functionType->canTakeArguments(*annotation.arguments))
 					candidates.push_back(declaration);
 			}
-			if (candidates.empty())
+			if (candidates.size() == 1)
-				m_errorReporter.fatalTypeError(_identifier.location(), "No matching declaration found after argument-dependent lookup.");
-			else if (candidates.size() == 1)
 				annotation.referencedDeclaration = candidates.front();
 			else
-				m_errorReporter.fatalTypeError(_identifier.location(), "No unique declaration found after argument-dependent lookup.");
+			{
+				SecondarySourceLocation ssl;
+
+				for (Declaration const* declaration: annotation.overloadedDeclarations)
+					if (declaration->location().isEmpty())
+					{
+						// Try to re-construct function definition
+						string description;
+						for (auto const& param: declaration->functionType(true)->parameterTypes())
+							description += (description.empty() ? "" : ", ") + param->toString(false);
+						description = "function " + _identifier.name() + "(" + description + ")";
+
+						ssl.append("Candidate: " + description, declaration->location());
+					}
+					else
+						ssl.append("Candidate:", declaration->location());
+				if (candidates.empty())
+					m_errorReporter.fatalTypeError(_identifier.location(), ssl, "No matching declaration found after argument-dependent lookup.");
+				else
+					m_errorReporter.fatalTypeError(_identifier.location(), ssl, "No unique declaration found after argument-dependent lookup.");
+			}
 		}
 	}
 	solAssert(
@@ -2376,15 +2407,24 @@ bool TypeChecker::visit(Identifier const& _identifier)
 		if (_identifier.name() == "sha3" && fType->kind() == FunctionType::Kind::KECCAK256)
 			m_errorReporter.typeError(
 				_identifier.location(),
-				"\"sha3\" has been deprecated in favour of \"keccak256\""
+				"\"sha3\" has been deprecated in favour of \"keccak256\"."
 			);
 		else if (_identifier.name() == "suicide" && fType->kind() == FunctionType::Kind::Selfdestruct)
 			m_errorReporter.typeError(
 				_identifier.location(),
-				"\"suicide\" has been deprecated in favour of \"selfdestruct\""
+				"\"suicide\" has been deprecated in favour of \"selfdestruct\"."
 			);
 	}
 
+	if (!m_insideModifierInvocation)
+		if (ModifierType const* type = dynamic_cast<decltype(type)>(_identifier.annotation().type))
+		{
+			m_errorReporter.typeError(
+				_identifier.location(),
+				"Modifier can only be referenced in function headers."
+			);
+		}
+
 	return false;
 }
 

libsolidity/analysis/TypeChecker.h

@@ -166,6 +166,9 @@ private:
 	/// Flag indicating whether we are currently inside a StructDefinition.
 	bool m_insideStruct = false;
 
+	/// Flag indicating whether we are currently inside the invocation of a modifier
+	bool m_insideModifierInvocation = false;
+
 	langutil::ErrorReporter& m_errorReporter;
 };
 

libsolidity/analysis/ViewPureChecker.cpp

@@ -241,7 +241,7 @@ void ViewPureChecker::endVisit(InlineAssembly const& _inlineAssembly)
 void ViewPureChecker::reportMutability(
 	StateMutability _mutability,
 	SourceLocation const& _location,
-	boost::optional<SourceLocation> const& _nestedLocation
+	std::optional<SourceLocation> const& _nestedLocation
 )
 {
 	if (_mutability > m_bestMutabilityAndLocation.mutability)

libsolidity/analysis/ViewPureChecker.h

@@ -23,6 +23,7 @@
 
 #include <map>
 #include <memory>
+#include <optional>
 
 namespace langutil
 {
@@ -67,7 +68,7 @@ private:
 	void reportMutability(
 		StateMutability _mutability,
 		langutil::SourceLocation const& _location,
-		boost::optional<langutil::SourceLocation> const& _nestedLocation = {}
+		std::optional<langutil::SourceLocation> const& _nestedLocation = {}
 	);
 
 	std::vector<std::shared_ptr<ASTNode>> const& m_ast;

libsolidity/ast/AST.h

@@ -36,6 +36,7 @@
 #include <json/json.h>
 
 #include <memory>
+#include <optional>
 #include <string>
 #include <vector>
 
@@ -186,7 +187,7 @@ public:
 
 	static std::string visibilityToString(Declaration::Visibility _visibility)
 	{
-		switch(_visibility)
+		switch (_visibility)
 		{
 		case Declaration::Visibility::Public:
 			return "public";
@@ -912,10 +913,10 @@ public:
 	ElementaryTypeName(
 		SourceLocation const& _location,
 		ElementaryTypeNameToken const& _elem,
-		boost::optional<StateMutability> _stateMutability = {}
+		std::optional<StateMutability> _stateMutability = {}
 	): TypeName(_location), m_type(_elem), m_stateMutability(_stateMutability)
 	{
-		solAssert(!_stateMutability.is_initialized() || _elem.token() == Token::Address, "");
+		solAssert(!_stateMutability.has_value() || _elem.token() == Token::Address, "");
 	}
 
 	void accept(ASTVisitor& _visitor) override;
@@ -923,11 +924,11 @@ public:
 
 	ElementaryTypeNameToken const& typeName() const { return m_type; }
 
-	boost::optional<StateMutability> const& stateMutability() const { return m_stateMutability; }
+	std::optional<StateMutability> const& stateMutability() const { return m_stateMutability; }
 
 private:
 	ElementaryTypeNameToken m_type;
-	boost::optional<StateMutability> m_stateMutability; ///< state mutability for address type
+	std::optional<StateMutability> m_stateMutability; ///< state mutability for address type
 };
 
 /**

libsolidity/ast/ASTAnnotations.h

@@ -26,10 +26,9 @@
 #include <libsolidity/ast/ASTEnums.h>
 #include <libsolidity/ast/ExperimentalFeatures.h>
 
-#include <boost/optional.hpp>
-
 #include <map>
 #include <memory>
+#include <optional>
 #include <set>
 #include <vector>
 
@@ -183,7 +182,7 @@ struct ExpressionAnnotation: ASTAnnotation
 
 	/// Types and - if given - names of arguments if the expr. is a function
 	/// that is called, used for overload resoultion
-	boost::optional<FuncCallArguments> arguments;
+	std::optional<FuncCallArguments> arguments;
 };
 
 struct IdentifierAnnotation: ExpressionAnnotation

libsolidity/ast/ASTEnums.h

@@ -36,7 +36,7 @@ enum class StateMutability { Pure, View, NonPayable, Payable };
 
 inline std::string stateMutabilityToString(StateMutability const& _stateMutability)
 {
-	switch(_stateMutability)
+	switch (_stateMutability)
 	{
 	case StateMutability::Pure:
 		return "pure";

libsolidity/ast/ASTJsonConverter.cpp

@@ -24,6 +24,7 @@
 #include <libsolidity/ast/AST.h>
 #include <libyul/AsmData.h>
 #include <libyul/AsmPrinter.h>
+#include <libdevcore/JSON.h>
 #include <libdevcore/UTF8.h>
 #include <boost/algorithm/string/join.hpp>
 
@@ -147,7 +148,7 @@ Json::Value ASTJsonConverter::typePointerToJson(TypePointer _tp, bool _short)
 	return typeDescriptions;
 
 }
-Json::Value ASTJsonConverter::typePointerToJson(boost::optional<FuncCallArguments> const& _tps)
+Json::Value ASTJsonConverter::typePointerToJson(std::optional<FuncCallArguments> const& _tps)
 {
 	if (_tps)
 	{
@@ -189,7 +190,7 @@ Json::Value ASTJsonConverter::inlineAssemblyIdentifierToJson(pair<yul::Identifie
 
 void ASTJsonConverter::print(ostream& _stream, ASTNode const& _node)
 {
-	_stream << toJson(_node);
+	_stream << jsonPrettyPrint(toJson(_node));
 }
 
 Json::Value&& ASTJsonConverter::toJson(ASTNode const& _node)

libsolidity/ast/ASTJsonConverter.h

@@ -27,10 +27,12 @@
 #include <liblangutil/Exceptions.h>
 
 #include <json/json.h>
+
+#include <algorithm>
+#include <optional>
 #include <ostream>
 #include <stack>
 #include <vector>
-#include <algorithm>
 
 namespace langutil
 {
@@ -169,7 +171,7 @@ private:
 		return json;
 	}
 	static Json::Value typePointerToJson(TypePointer _tp, bool _short = false);
-	static Json::Value typePointerToJson(boost::optional<FuncCallArguments> const& _tps);
+	static Json::Value typePointerToJson(std::optional<FuncCallArguments> const& _tps);
 	void appendExpressionAttributes(
 		std::vector<std::pair<std::string, Json::Value>> &_attributes,
 		ExpressionAnnotation const& _annotation

libsolidity/ast/TypeProvider.h

@@ -22,6 +22,7 @@
 #include <array>
 #include <map>
 #include <memory>
+#include <optional>
 #include <utility>
 
 namespace dev

libsolidity/ast/Types.cpp

@@ -658,7 +658,7 @@ BoolResult FixedPointType::isExplicitlyConvertibleTo(Type const& _convertTo) con
 
 TypeResult FixedPointType::unaryOperatorResult(Token _operator) const
 {
-	switch(_operator)
+	switch (_operator)
 	{
 	case Token::Delete:
 		// "delete" is ok for all fixed types
@@ -1812,10 +1812,10 @@ TypePointer ArrayType::decodingType() const
 
 TypeResult ArrayType::interfaceType(bool _inLibrary) const
 {
-	if (_inLibrary && m_interfaceType_library.is_initialized())
+	if (_inLibrary && m_interfaceType_library.has_value())
 		return *m_interfaceType_library;
 
-	if (!_inLibrary && m_interfaceType.is_initialized())
+	if (!_inLibrary && m_interfaceType.has_value())
 		return *m_interfaceType;
 
 	TypeResult result{TypePointer{}};
@@ -1849,7 +1849,7 @@ u256 ArrayType::memoryDataSize() const
 	solAssert(m_location == DataLocation::Memory, "");
 	solAssert(!isByteArray(), "");
 	bigint size = bigint(m_length) * m_baseType->memoryHeadSize();
-	solAssert(size <= numeric_limits<unsigned>::max(), "Array size does not fit u256.");
+	solAssert(size <= numeric_limits<u256>::max(), "Array size does not fit u256.");
 	return u256(size);
 }
 
@@ -2106,10 +2106,10 @@ MemberList::MemberMap StructType::nativeMembers(ContractDefinition const*) const
 
 TypeResult StructType::interfaceType(bool _inLibrary) const
 {
-	if (_inLibrary && m_interfaceType_library.is_initialized())
+	if (_inLibrary && m_interfaceType_library.has_value())
 		return *m_interfaceType_library;
 
-	if (!_inLibrary && m_interfaceType.is_initialized())
+	if (!_inLibrary && m_interfaceType.has_value())
 		return *m_interfaceType;
 
 	TypeResult result{TypePointer{}};
@@ -2166,7 +2166,7 @@ TypeResult StructType::interfaceType(bool _inLibrary) const
 		}
 	};
 
-	m_recursive = m_recursive.get() || (CycleDetector<StructDefinition>(visitor).run(structDefinition()) != nullptr);
+	m_recursive = m_recursive.value() || (CycleDetector<StructDefinition>(visitor).run(structDefinition()) != nullptr);
 
 	std::string const recursiveErrMsg = "Recursive type not allowed for public or external contract functions.";
 
@@ -2179,13 +2179,13 @@ TypeResult StructType::interfaceType(bool _inLibrary) const
 		else
 			m_interfaceType_library = TypeProvider::withLocation(this, DataLocation::Memory, true);
 
-		if (m_recursive.get())
+		if (m_recursive.value())
 			m_interfaceType = TypeResult::err(recursiveErrMsg);
 
 		return *m_interfaceType_library;
 	}
 
-	if (m_recursive.get())
+	if (m_recursive.value())
 		m_interfaceType = TypeResult::err(recursiveErrMsg);
 	else if (!result.message().empty())
 		m_interfaceType = result;
@@ -2846,7 +2846,7 @@ unsigned FunctionType::sizeOnStack() const
 
 	unsigned size = 0;
 
-	switch(kind)
+	switch (kind)
 	{
 	case Kind::External:
 	case Kind::DelegateCall:
@@ -3373,6 +3373,15 @@ MemberList::MemberMap TypeType::nativeMembers(ContractDefinition const* _current
 	return members;
 }
 
+BoolResult TypeType::isExplicitlyConvertibleTo(Type const& _convertTo) const
+{
+	if (auto const* address = dynamic_cast<AddressType const*>(&_convertTo))
+		if (address->stateMutability() == StateMutability::NonPayable)
+			if (auto const* contractType = dynamic_cast<ContractType const*>(m_actualType))
+				return contractType->contractDefinition().isLibrary();
+	return isImplicitlyConvertibleTo(_convertTo);
+}
+
 ModifierType::ModifierType(ModifierDefinition const& _modifier)
 {
 	TypePointers params;

libsolidity/ast/Types.h

@@ -31,11 +31,11 @@
 #include <libdevcore/CommonIO.h>
 #include <libdevcore/Result.h>
 
-#include <boost/optional.hpp>
 #include <boost/rational.hpp>
 
 #include <map>
 #include <memory>
+#include <optional>
 #include <set>
 #include <string>
 
@@ -769,8 +769,8 @@ private:
 	Type const* m_baseType;
 	bool m_hasDynamicLength = true;
 	u256 m_length;
-	mutable boost::optional<TypeResult> m_interfaceType;
+	mutable std::optional<TypeResult> m_interfaceType;
-	mutable boost::optional<TypeResult> m_interfaceType_library;
+	mutable std::optional<TypeResult> m_interfaceType_library;
 };
 
 /**
@@ -865,12 +865,12 @@ public:
 
 	bool recursive() const
 	{
-		if (m_recursive.is_initialized())
+		if (m_recursive.has_value())
-			return m_recursive.get();
+			return m_recursive.value();
 
 		interfaceType(false);
 
-		return m_recursive.get();
+		return m_recursive.value();
 	}
 
 	std::unique_ptr<ReferenceType> copyForLocation(DataLocation _location, bool _isPointer) const override;
@@ -898,9 +898,9 @@ public:
 private:
 	StructDefinition const& m_struct;
 	// Caches for interfaceType(bool)
-	mutable boost::optional<TypeResult> m_interfaceType;
+	mutable std::optional<TypeResult> m_interfaceType;
-	mutable boost::optional<TypeResult> m_interfaceType_library;
+	mutable std::optional<TypeResult> m_interfaceType_library;
-	mutable boost::optional<bool> m_recursive;
+	mutable std::optional<bool> m_recursive;
 };
 
 /**
@@ -1287,6 +1287,7 @@ public:
 	std::string toString(bool _short) const override { return "type(" + m_actualType->toString(_short) + ")"; }
 	MemberList::MemberMap nativeMembers(ContractDefinition const* _currentScope) const override;
 
+	BoolResult isExplicitlyConvertibleTo(Type const& _convertTo) const override;
 private:
 	TypePointer m_actualType;
 };

libsolidity/codegen/CompilerContext.cpp

@@ -411,7 +411,7 @@ void CompilerContext::appendInlineAssembly(
 		analyzerResult = yul::AsmAnalyzer(
 			analysisInfo,
 			errorReporter,
-			boost::none,
+			std::nullopt,
 			dialect,
 			identifierAccess.resolve
 		).analyze(*parserResult);

libsolidity/codegen/ExpressionCompiler.cpp

@@ -475,7 +475,22 @@ bool ExpressionCompiler::visit(FunctionCall const& _functionCall)
 	{
 		solAssert(_functionCall.arguments().size() == 1, "");
 		solAssert(_functionCall.names().empty(), "");
-		acceptAndConvert(*_functionCall.arguments().front(), *_functionCall.annotation().type);
+		auto const& expression = *_functionCall.arguments().front();
+		auto const& targetType = *_functionCall.annotation().type;
+		if (auto const* typeType = dynamic_cast<TypeType const*>(expression.annotation().type))
+			if (auto const* addressType = dynamic_cast<AddressType const*>(&targetType))
+			{
+				auto const* contractType = dynamic_cast<ContractType const*>(typeType->actualType());
+				solAssert(
+					contractType &&
+					contractType->contractDefinition().isLibrary() &&
+					addressType->stateMutability() == StateMutability::NonPayable,
+					""
+				);
+				m_context.appendLibraryAddress(contractType->contractDefinition().fullyQualifiedName());
+				return false;
+			}
+		acceptAndConvert(expression, targetType);
 		return false;
 	}
 
@@ -1229,6 +1244,28 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 						utils().leftShiftNumberOnStack(224);
 						return false;
 					}
+	// Another special case for `address(this).balance`. Post-Istanbul, we can use the selfbalance
+	// opcode.
+	if (
+		m_context.evmVersion().hasSelfBalance() &&
+		member == "balance" &&
+		_memberAccess.expression().annotation().type->category() == Type::Category::Address
+	)
+		if (FunctionCall const* funCall = dynamic_cast<FunctionCall const*>(&_memberAccess.expression()))
+			if (auto const* addr = dynamic_cast<ElementaryTypeNameExpression const*>(&funCall->expression()))
+				if (
+					addr->typeName().token() == Token::Address &&
+					funCall->arguments().size() == 1
+				)
+					if (auto arg = dynamic_cast<Identifier const*>( funCall->arguments().front().get()))
+						if (
+							arg->name() == "this" &&
+							dynamic_cast<MagicVariableDeclaration const*>(arg->annotation().referencedDeclaration)
+						)
+						{
+							m_context << Instruction::SELFBALANCE;
+							return false;
+						}
 
 	_memberAccess.expression().accept(*this);
 	switch (_memberAccess.expression().annotation().type->category())

libsolidity/codegen/YulUtilFunctions.cpp

@@ -962,11 +962,11 @@ string YulUtilFunctions::readFromCalldata(Type const& _type)
 	return readFromMemoryOrCalldata(_type, true);
 }
 
-string YulUtilFunctions::updateStorageValueFunction(Type const& _type, boost::optional<unsigned> const& _offset)
+string YulUtilFunctions::updateStorageValueFunction(Type const& _type, std::optional<unsigned> const& _offset)
 {
 	string const functionName =
 		"update_storage_value_" +
-		(_offset.is_initialized() ? ("offset_" + to_string(*_offset)) : "") +
+		(_offset.has_value() ? ("offset_" + to_string(*_offset)) : "") +
 		_type.identifier();
 
 	return m_functionCollector->createFunction(functionName, [&] {
@@ -983,11 +983,11 @@ string YulUtilFunctions::updateStorageValueFunction(Type const& _type, boost::op
 			)")
 			("functionName", functionName)
 			("update",
-				_offset.is_initialized() ?
+				_offset.has_value() ?
 					updateByteSliceFunction(_type.storageBytes(), *_offset) :
 					updateByteSliceFunctionDynamic(_type.storageBytes())
 			)
-			("offset", _offset.is_initialized() ? "" : "offset, ")
+			("offset", _offset.has_value() ? "" : "offset, ")
 			("prepare", prepareStoreFunction(_type))
 			.render();
 		}

libsolidity/codegen/YulUtilFunctions.h

@@ -197,7 +197,7 @@ public:
 	/// the specified slot and offset. If offset is not given, it is expected as
 	/// runtime parameter.
 	/// signature: (slot, [offset,] value)
-	std::string updateStorageValueFunction(Type const& _type, boost::optional<unsigned> const& _offset = boost::optional<unsigned>());
+	std::string updateStorageValueFunction(Type const& _type, std::optional<unsigned> const& _offset = std::optional<unsigned>());
 
 	/// Returns the name of a function that will write the given value to
 	/// the specified address.

libsolidity/codegen/ir/IRLValue.cpp

@@ -115,7 +115,7 @@ string IRStorageItem::storeValue(string const& _value, Type const& _sourceType)
 	if (m_type->isValueType())
 		solAssert(_sourceType == *m_type, "Different type, but might not be an error.");
 
-	boost::optional<unsigned> offset;
+	std::optional<unsigned> offset;
 
 	if (m_offset.type() == typeid(unsigned))
 		offset = get<unsigned>(m_offset);

libsolidity/formal/BMC.cpp

@@ -108,14 +108,16 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
 
 bool BMC::visit(ContractDefinition const& _contract)
 {
-	SMTEncoder::visit(_contract);
+	initContract(_contract);
 
 	/// Check targets created by state variable initialization.
 	smt::Expression constraints = m_context.assertions();
 	checkVerificationTargets(constraints);
 	m_verificationTargets.clear();
 
-	return true;
+	SMTEncoder::visit(_contract);
+
+	return false;
 }
 
 void BMC::endVisit(ContractDefinition const& _contract)
@@ -426,15 +428,20 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
 		solAssert(funType, "");
 
+		auto const& functionParams = funDef->parameters();
+		auto const& arguments = _funCall.arguments();
+		unsigned firstParam = 0;
 		if (funType->bound())
 		{
 			auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
 			solAssert(boundFunction, "");
-			funArgs.push_back(expr(boundFunction->expression()));
+			funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
+			firstParam = 1;
 		}
 
-		for (auto arg: _funCall.arguments())
+		solAssert((arguments.size() + firstParam) == functionParams.size(), "");
-			funArgs.push_back(expr(*arg));
+		for (unsigned i = 0; i < arguments.size(); ++i)
+			funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
 		initializeFunctionCallParameters(*funDef, funArgs);
 
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)

libsolidity/formal/CHC.cpp

@@ -17,6 +17,8 @@
 
 #include <libsolidity/formal/CHC.h>
 
+#include <libsolidity/formal/CHCSmtLib2Interface.h>
+
 #ifdef HAVE_Z3
 #include <libsolidity/formal/Z3CHCInterface.h>
 #endif
@@ -30,13 +32,20 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
+CHC::CHC(
+	smt::EncodingContext& _context,
+	ErrorReporter& _errorReporter,
+	map<h256, string> const& _smtlib2Responses
+):
 	SMTEncoder(_context),
 #ifdef HAVE_Z3
 	m_interface(make_shared<smt::Z3CHCInterface>()),
+#else
+	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
 #endif
 	m_outerErrorReporter(_errorReporter)
 {
+	(void)_smtlib2Responses;
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -47,12 +56,24 @@ void CHC::analyze(SourceUnit const& _source)
 	auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
 	solAssert(z3Interface, "");
 	m_context.setSolver(z3Interface->z3Interface());
+#else
+	auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
+	solAssert(smtlib2Interface, "");
+	m_context.setSolver(smtlib2Interface->smtlib2Interface());
+#endif
 	m_context.clear();
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);
 
 	_source.accept(*this);
-#endif
+}
+
+vector<string> CHC::unhandledQueries() const
+{
+	if (auto smtlib2 = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface))
+		return smtlib2->unhandledQueries();
+
+	return {};
 }
 
 bool CHC::visit(ContractDefinition const& _contract)
@@ -62,8 +83,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	reset();
 
-	if (!SMTEncoder::visit(_contract))
+	initContract(_contract);
-		return false;
 
 	m_stateVariables = _contract.stateVariablesIncludingInherited();
 
@@ -89,7 +109,6 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	// If the contract has a constructor it is handled as a function.
 	// Otherwise we zero-initialize all state vars.
-	// TODO take into account state vars init values.
 	if (!_contract.constructor())
 	{
 		string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
@@ -101,14 +120,15 @@ bool CHC::visit(ContractDefinition const& _contract)
 		{
 			auto const& symbVar = m_context.variable(*var);
 			symbVar->increaseIndex();
-			m_interface->declareVariable(symbVar->currentName(), *symbVar->sort());
+			m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
 			m_context.setZeroValue(*symbVar);
 		}
 
 		connectBlocks(constructorPred, interface());
 	}
 
-	return true;
+	SMTEncoder::visit(_contract);
+	return false;
 }
 
 void CHC::endVisit(ContractDefinition const& _contract)
@@ -137,24 +157,22 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	initFunction(_function);
 
+	auto functionEntryBlock = createBlock(m_currentFunction);
+	auto bodyBlock = createBlock(&m_currentFunction->body());
+
+	auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
+	auto bodyPred = predicate(*bodyBlock);
+
 	// Store the constraints related to variable initialization.
 	smt::Expression const& initAssertions = m_context.assertions();
 	m_context.pushSolver();
 
-	solAssert(m_functionBlocks == 0, "");
-
-	createBlock(m_currentFunction);
-	createBlock(&m_currentFunction->body(), "block_");
-
-	auto functionPred = predicate(m_currentFunction);
-	auto bodyPred = predicate(&m_currentFunction->body());
-
 	connectBlocks(interface(), functionPred);
 	connectBlocks(functionPred, bodyPred);
 
 	m_context.popSolver();
 
-	pushBlock(&m_currentFunction->body());
+	setCurrentBlock(*bodyBlock);
 
 	// We need to re-add the constraints that were created for initialization of variables.
 	m_context.addAssertion(initAssertions);
@@ -169,25 +187,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	if (!shouldVisit(_function))
 		return;
 
-	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
+	connectBlocks(m_currentBlock, interface());
-
-	// Function Exit block.
-	createBlock(m_currentFunction);
-	connectBlocks(m_path.back(), predicate(&_function));
-
-	// Rule FunctionExit -> Interface, uses no constraints.
-	clearIndices();
-	m_context.pushSolver();
-	connectBlocks(predicate(&_function), interface());
-	m_context.popSolver();
 
+	solAssert(&_function == m_currentFunction, "");
 	m_currentFunction = nullptr;
-	solAssert(m_path.size() == m_functionBlocks, "");
-	while (m_functionBlocks > 0)
-		popBlock();
-
-	solAssert(m_path.empty(), "");
-
 	SMTEncoder::endVisit(_function);
 }
 
@@ -198,7 +201,38 @@ bool CHC::visit(IfStatement const& _if)
 	bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen;
 	m_unknownFunctionCallSeen = false;
 
-	SMTEncoder::visit(_if);
+	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto ifHeaderBlock = createBlock(&_if, "if_header_");
+	auto trueBlock = createBlock(&_if.trueStatement(), "if_true_");
+	auto falseBlock = _if.falseStatement() ? createBlock(_if.falseStatement(), "if_false_") : nullptr;
+	auto afterIfBlock = createBlock(&functionBody);
+
+	connectBlocks(m_currentBlock, predicate(*ifHeaderBlock));
+
+	setCurrentBlock(*ifHeaderBlock);
+	_if.condition().accept(*this);
+	auto condition = expr(_if.condition());
+
+	connectBlocks(m_currentBlock, predicate(*trueBlock), condition);
+	if (_if.falseStatement())
+		connectBlocks(m_currentBlock, predicate(*falseBlock), !condition);
+	else
+		connectBlocks(m_currentBlock, predicate(*afterIfBlock), !condition);
+
+	setCurrentBlock(*trueBlock);
+	_if.trueStatement().accept(*this);
+	connectBlocks(m_currentBlock, predicate(*afterIfBlock));
+
+	if (_if.falseStatement())
+	{
+		setCurrentBlock(*falseBlock);
+		_if.falseStatement()->accept(*this);
+		connectBlocks(m_currentBlock, predicate(*afterIfBlock));
+	}
+
+	setCurrentBlock(*afterIfBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -214,16 +248,41 @@ bool CHC::visit(WhileStatement const& _while)
 	m_unknownFunctionCallSeen = false;
 
 	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while";
+	auto loopHeaderBlock = createBlock(&_while, namePrefix + "_header_");
+	auto loopBodyBlock = createBlock(&_while.body(), namePrefix + "_body_");
+	auto afterLoopBlock = createBlock(&functionBody);
+
+	auto outerBreakDest = m_breakDest;
+	auto outerContinueDest = m_continueDest;
+	m_breakDest = afterLoopBlock.get();
+	m_continueDest = loopHeaderBlock.get();
 
 	if (_while.isDoWhile())
 		_while.body().accept(*this);
 
-	visitLoop(
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
-		_while,
+
-		&_while.condition(),
+	setCurrentBlock(*loopHeaderBlock);
-		_while.body(),
+
-		nullptr
+	_while.condition().accept(*this);
-	);
+	auto condition = expr(_while.condition());
+
+	connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
+	connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
+
+	// Loop body visit.
+	setCurrentBlock(*loopBodyBlock);
+	_while.body().accept(*this);
+
+	m_breakDest = outerBreakDest;
+	m_continueDest = outerContinueDest;
+
+	// Back edge.
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+	setCurrentBlock(*afterLoopBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -239,16 +298,52 @@ bool CHC::visit(ForStatement const& _for)
 	m_unknownFunctionCallSeen = false;
 
 	solAssert(m_currentFunction, "");
+	auto const& functionBody = m_currentFunction->body();
+
+	auto loopHeaderBlock = createBlock(&_for, "for_header_");
+	auto loopBodyBlock = createBlock(&_for.body(), "for_body_");
+	auto afterLoopBlock = createBlock(&functionBody);
+	auto postLoop = _for.loopExpression();
+	auto postLoopBlock = postLoop ? createBlock(postLoop, "for_post_") : nullptr;
+
+	auto outerBreakDest = m_breakDest;
+	auto outerContinueDest = m_continueDest;
+	m_breakDest = afterLoopBlock.get();
+	m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get();
 
 	if (auto init = _for.initializationExpression())
 		init->accept(*this);
 
-	visitLoop(
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
-		_for,
+	setCurrentBlock(*loopHeaderBlock);
-		_for.condition(),
+
-		_for.body(),
+	auto condition = smt::Expression(true);
-		_for.loopExpression()
+	if (auto forCondition = _for.condition())
-	);
+	{
+		forCondition->accept(*this);
+		condition = expr(*forCondition);
+	}
+
+	connectBlocks(m_currentBlock, predicate(*loopBodyBlock), condition);
+	connectBlocks(m_currentBlock, predicate(*afterLoopBlock), !condition);
+
+	// Loop body visit.
+	setCurrentBlock(*loopBodyBlock);
+	_for.body().accept(*this);
+
+	if (postLoop)
+	{
+		connectBlocks(m_currentBlock, predicate(*postLoopBlock));
+		setCurrentBlock(*postLoopBlock);
+		postLoop->accept(*this);
+	}
+
+	m_breakDest = outerBreakDest;
+	m_continueDest = outerContinueDest;
+
+	// Back edge.
+	connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
+	setCurrentBlock(*afterLoopBlock);
 
 	if (m_unknownFunctionCallSeen)
 		eraseKnowledge();
@@ -301,16 +396,20 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	createReturnedExpressions(_funCall);
 }
 
-void CHC::endVisit(Break const&)
+void CHC::endVisit(Break const& _break)
 {
 	solAssert(m_breakDest, "");
-	m_breakSeen = true;
+	connectBlocks(m_currentBlock, predicate(*m_breakDest));
+	auto breakGhost = createBlock(&_break, "break_ghost_");
+	m_currentBlock = predicate(*breakGhost);
 }
 
-void CHC::endVisit(Continue const&)
+void CHC::endVisit(Continue const& _continue)
 {
 	solAssert(m_continueDest, "");
-	m_continueSeen = true;
+	connectBlocks(m_currentBlock, predicate(*m_continueDest));
+	auto continueGhost = createBlock(&_continue, "continue_ghost_");
+	m_currentBlock = predicate(*continueGhost);
 }
 
 void CHC::visitAssert(FunctionCall const& _funCall)
@@ -319,12 +418,10 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	solAssert(args.size() == 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 
-	solAssert(!m_path.empty(), "");
-
 	createErrorBlock();
 
 	smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
-	connectBlocks(m_path.back(), error(), currentPathConditions() && assertNeg);
+	connectBlocks(m_currentBlock, error(), currentPathConditions() && assertNeg);
 
 	m_verificationTargets.push_back(&_funCall);
 }
@@ -341,85 +438,6 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
-void CHC::visitLoop(
-	BreakableStatement const& _loop,
-	Expression const* _condition,
-	Statement const& _body,
-	ASTNode const* _postLoop
-)
-{
-	bool breakWasSeen = m_breakSeen;
-	bool continueWasSeen = m_continueSeen;
-	m_breakSeen = false;
-	m_continueSeen = false;
-
-	solAssert(m_currentFunction, "");
-	auto const& functionBody = m_currentFunction->body();
-
-	createBlock(&_loop, "loop_header_");
-	createBlock(&_body, "loop_body_");
-	createBlock(&functionBody, "block_");
-
-	connectBlocks(m_path.back(), predicate(&_loop));
-
-	// We need to save the next block here because new blocks
-	// might be created inside the loop body.
-	// This will be m_path.back() in the end of this function.
-	pushBlock(&functionBody);
-
-	smt::Expression loopHeader = predicate(&_loop);
-	pushBlock(&_loop);
-
-	if (_condition)
-		_condition->accept(*this);
-	auto condition = _condition ? expr(*_condition) : smt::Expression(true);
-
-	connectBlocks(loopHeader, predicate(&_body), condition);
-	connectBlocks(loopHeader, predicate(&functionBody), !condition);
-
-	// Loop body visit.
-	pushBlock(&_body);
-
-	m_breakDest = &functionBody;
-	m_continueDest = _postLoop ? _postLoop : &_loop;
-
-	auto functionBlocks = m_functionBlocks;
-	_body.accept(*this);
-	if (_postLoop)
-	{
-		createBlock(_postLoop, "loop_post_");
-		connectBlocks(m_path.back(), predicate(_postLoop));
-		pushBlock(_postLoop);
-		_postLoop->accept(*this);
-	}
-
-	// Back edge.
-	connectBlocks(m_path.back(), predicate(&_loop));
-
-	// Pop all function blocks created by nested inner loops
-	// to adjust the assertion context.
-	for (unsigned i = m_functionBlocks; i > functionBlocks; --i)
-		popBlock();
-	m_functionBlocks = functionBlocks;
-
-	// Loop body
-	popBlock();
-	// Loop header
-	popBlock();
-
-	// New function block starts with indices = 0
-	clearIndices();
-
-	if (m_breakSeen || m_continueSeen)
-	{
-		eraseKnowledge();
-		m_context.resetVariables([](VariableDeclaration const&) { return true; });
-	}
-
-	m_breakSeen = breakWasSeen;
-	m_continueSeen = continueWasSeen;
-}
-
 void CHC::reset()
 {
 	m_stateSorts.clear();
@@ -427,8 +445,9 @@ void CHC::reset()
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
 	m_unknownFunctionCallSeen = false;
-	m_breakSeen = false;
+	m_blockCounter = 0;
-	m_continueSeen = false;
+	m_breakDest = nullptr;
+	m_continueDest = nullptr;
 }
 
 void CHC::eraseKnowledge()
@@ -458,19 +477,12 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
 	return false;
 }
 
-void CHC::pushBlock(ASTNode const* _node)
+void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block)
-{
-	clearIndices();
-	m_context.pushSolver();
-	m_path.push_back(predicate(_node));
-	++m_functionBlocks;
-}
-
-void CHC::popBlock()
 {
 	m_context.popSolver();
-	m_path.pop_back();
+	clearIndices();
-	--m_functionBlocks;
+	m_context.pushSolver();
+	m_currentBlock = predicate(_block);
 }
 
 smt::SortPointer CHC::constructorSort()
@@ -493,25 +505,24 @@ smt::SortPointer CHC::interfaceSort()
 
 smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	if (m_nodeSorts.count(&_function))
-		return m_nodeSorts.at(&_function);
-
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: _function.parameters() + _function.returnParameters())
-		varSorts.push_back(smt::smtSort(*var->type()));
+	{
-	auto sort = make_shared<smt::FunctionSort>(
+		// SMT solvers do not support function types as arguments.
+		if (var->type()->category() == Type::Category::Function)
+			varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
+		else
+			varSorts.push_back(smt::smtSort(*var->type()));
+	}
+	return make_shared<smt::FunctionSort>(
 		m_stateSorts + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[&_function] = move(sort);
 }
 
 smt::SortPointer CHC::sort(ASTNode const* _node)
 {
-	if (m_nodeSorts.count(_node))
-		return m_nodeSorts.at(_node);
-
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
 		return sort(*funDef);
 
@@ -521,12 +532,17 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
 	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: m_currentFunction->localVariables())
-		varSorts.push_back(smt::smtSort(*var->type()));
+	{
-	auto functionBodySort = make_shared<smt::FunctionSort>(
+		// SMT solvers do not support function types as arguments.
+		if (var->type()->category() == Type::Category::Function)
+			varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
+		else
+			varSorts.push_back(smt::smtSort(*var->type()));
+	}
+	return make_shared<smt::FunctionSort>(
 		fSort->domain + varSorts,
 		boolSort
 	);
-	return m_nodeSorts[_node] = move(functionBodySort);
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
@@ -536,7 +552,7 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
 		_name,
 		m_context
 	);
-	m_interface->registerRelation(block->currentValue());
+	m_interface->registerRelation(block->currentFunctionValue());
 	return block;
 }
 
@@ -568,25 +584,24 @@ smt::Expression CHC::error()
 
 smt::Expression CHC::error(unsigned _idx)
 {
-	return m_errorPredicate->valueAtIndex(_idx)({});
+	return m_errorPredicate->functionValueAtIndex(_idx)({});
 }
 
-void CHC::createBlock(ASTNode const* _node, string const& _prefix)
+unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
 {
-	if (m_predicates.count(_node))
+	return createSymbolicBlock(sort(_node),
-	{
+		"block_" +
-		m_predicates.at(_node)->increaseIndex();
+		uniquePrefix() +
-		m_interface->registerRelation(m_predicates.at(_node)->currentValue());
+		"_" +
-	}
+		_prefix +
-	else
+		predicateName(_node));
-		m_predicates[_node] = createSymbolicBlock(sort(_node), _prefix + predicateName(_node));
 }
 
 void CHC::createErrorBlock()
 {
 	solAssert(m_errorPredicate, "");
 	m_errorPredicate->increaseIndex();
-	m_interface->registerRelation(m_errorPredicate->currentValue());
+	m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
 }
 
 void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)
@@ -646,13 +661,20 @@ string CHC::predicateName(ASTNode const* _node)
 	return prefix + to_string(_node->id());
 }
 
-smt::Expression CHC::predicate(ASTNode const* _node)
+smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
 {
-	if (dynamic_cast<FunctionDefinition const*>(_node))
+	return _block(currentBlockVariables());
-		return (*m_predicates.at(_node))(currentFunctionVariables());
-	return (*m_predicates.at(_node))(currentBlockVariables());
 }
 
+smt::Expression CHC::predicate(
+	smt::SymbolicFunctionVariable const& _block,
+	vector<smt::Expression> const& _arguments
+)
+{
+	return _block(_arguments);
+}
+
+
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
 {
 	m_interface->addRule(_rule, _ruleName);
@@ -680,3 +702,8 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
 	}
 	return false;
 }
+
+string CHC::uniquePrefix()
+{
+	return to_string(m_blockCounter++);
+}

libsolidity/formal/CHC.h

@@ -44,12 +44,21 @@ namespace solidity
 class CHC: public SMTEncoder
 {
 public:
-	CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
+	CHC(
+		smt::EncodingContext& _context,
+		langutil::ErrorReporter& _errorReporter,
+		std::map<h256, std::string> const& _smtlib2Responses
+	);
 
 	void analyze(SourceUnit const& _sources);
 
 	std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
 
+	/// 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
+	/// the constructor.
+	std::vector<std::string> unhandledQueries() const;
+
 private:
 	/// Visitor functions.
 	//@{
@@ -66,12 +75,6 @@ private:
 
 	void visitAssert(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
-	void visitLoop(
-		BreakableStatement const& _loop,
-		Expression const* _condition,
-		Statement const& _body,
-		ASTNode const* _postLoop
-	);
 	//@}
 
 	/// Helpers.
@@ -80,8 +83,7 @@ private:
 	void eraseKnowledge();
 	bool shouldVisit(ContractDefinition const& _contract) const;
 	bool shouldVisit(FunctionDefinition const& _function) const;
-	void pushBlock(ASTNode const* _node);
+	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block);
-	void popBlock();
 	//@}
 
 	/// Sort helpers.
@@ -105,9 +107,8 @@ private:
 	smt::Expression error();
 	smt::Expression error(unsigned _idx);
 
-	/// Creates a block for the given _node or increases its SSA index
+	/// Creates a block for the given _node.
-	/// if the block already exists which in practice creates a new function.
+	std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
-	void createBlock(ASTNode const* _node, std::string const& _prefix = "");
 
 	/// Creates a new error block to be used by an assertion.
 	/// Also registers the predicate.
@@ -129,7 +130,9 @@ private:
 	/// @returns the predicate name for a given node.
 	std::string predicateName(ASTNode const* _node);
 	/// @returns a predicate application over the current scoped variables.
-	smt::Expression predicate(ASTNode const* _node);
+	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
+	/// @returns a predicate application over @param _arguments.
+	smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
 	//@}
 
 	/// Solver related.
@@ -140,22 +143,26 @@ private:
 	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 	//@}
 
+	/// Misc.
+	//@{
+	/// Returns a prefix to be used in a new unique block name
+	/// and increases the block counter.
+	std::string uniquePrefix();
+	//@}
+
 	/// Predicates.
 	//@{
 	/// Constructor predicate.
 	/// Default constructor sets state vars to 0.
-	std::unique_ptr<smt::SymbolicVariable> m_constructorPredicate;
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
 
 	/// Artificial Interface predicate.
 	/// Single entry block for all functions.
-	std::unique_ptr<smt::SymbolicVariable> m_interfacePredicate;
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_interfacePredicate;
 
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
-	std::unique_ptr<smt::SymbolicVariable> m_errorPredicate;
+	std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
-
-	/// Maps AST nodes to their predicates.
-	std::unordered_map<ASTNode const*, std::shared_ptr<smt::SymbolicVariable>> m_predicates;
 	//@}
 
 	/// Variables.
@@ -166,9 +173,6 @@ private:
 	/// State variables.
 	/// Used to create all predicates.
 	std::vector<VariableDeclaration const*> m_stateVariables;
-
-	/// Input sorts for AST nodes.
-	std::map<ASTNode const*, smt::SortPointer> m_nodeSorts;
 	//@}
 
 	/// Verification targets.
@@ -183,21 +187,19 @@ private:
 	//@{
 	FunctionDefinition const* m_currentFunction = nullptr;
 
-	/// Number of basic blocks created for the body of the current function.
+	/// The current block.
-	unsigned m_functionBlocks = 0;
+	smt::Expression m_currentBlock = smt::Expression(true);
-	/// The current control flow path.
+
-	std::vector<smt::Expression> m_path;
+	/// Counter to generate unique block names.
+	unsigned m_blockCounter = 0;
+
 	/// Whether a function call was seen in the current scope.
 	bool m_unknownFunctionCallSeen = false;
-	/// Whether a break statement was seen in the current scope.
-	bool m_breakSeen = false;
-	/// Whether a continue statement was seen in the current scope.
-	bool m_continueSeen = false;
 
 	/// Block where a loop break should go to.
-	ASTNode const* m_breakDest;
+	smt::SymbolicFunctionVariable const* m_breakDest = nullptr;
 	/// Block where a loop continue should go to.
-	ASTNode const* m_continueDest;
+	smt::SymbolicFunctionVariable const* m_continueDest = nullptr;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/CHCSmtLib2Interface.cpp

@@ -0,0 +1,160 @@
+/*
+	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/>.
+*/
+
+#include <libsolidity/formal/CHCSmtLib2Interface.h>
+
+#include <libdevcore/Keccak256.h>
+
+#include <boost/algorithm/string/join.hpp>
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/filesystem/operations.hpp>
+
+#include <array>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <stdexcept>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+using namespace dev::solidity::smt;
+
+CHCSmtLib2Interface::CHCSmtLib2Interface(map<h256, string> const& _queryResponses):
+	m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses)),
+	m_queryResponses(_queryResponses)
+{
+	reset();
+}
+
+void CHCSmtLib2Interface::reset()
+{
+	m_accumulatedOutput.clear();
+	m_variables.clear();
+}
+
+void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
+{
+	solAssert(_expr.sort, "");
+	solAssert(_expr.sort->kind == smt::Kind::Function, "");
+	if (!m_variables.count(_expr.name))
+	{
+		auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
+		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		// Relations are predicates which have implicit codomain Bool.
+		m_variables.insert(_expr.name);
+		write(
+			"(declare-rel |" +
+			_expr.name +
+			"| " +
+			domain +
+			")"
+		);
+	}
+}
+
+void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name)
+{
+	write(
+		"(rule (! " +
+		m_smtlib2->toSExpr(_expr) +
+		" :named " +
+		_name +
+		"))"
+	);
+}
+
+pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression const& _block)
+{
+	string accumulated{};
+	swap(m_accumulatedOutput, accumulated);
+	for (auto const& var: m_smtlib2->variables())
+		declareVariable(var.first, var.second);
+	m_accumulatedOutput += accumulated;
+
+	string response = querySolver(
+		m_accumulatedOutput +
+		"\n(query " + _block.name + " :print-certificate true)"
+	);
+
+	CheckResult result;
+	// TODO proper parsing
+	if (boost::starts_with(response, "sat\n"))
+		result = CheckResult::SATISFIABLE;
+	else if (boost::starts_with(response, "unsat\n"))
+		result = CheckResult::UNSATISFIABLE;
+	else if (boost::starts_with(response, "unknown\n"))
+		result = CheckResult::UNKNOWN;
+	else
+		result = CheckResult::ERROR;
+
+	// TODO collect invariants or counterexamples.
+	return make_pair(result, vector<string>{});
+}
+
+void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
+{
+	solAssert(_sort, "");
+	if (_sort->kind == Kind::Function)
+		declareFunction(_name, _sort);
+	else if (!m_variables.count(_name))
+	{
+		m_variables.insert(_name);
+		write("(declare-var |" + _name + "| " + m_smtlib2->toSmtLibSort(*_sort) + ')');
+	}
+}
+
+void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
+{
+	solAssert(_sort, "");
+	solAssert(_sort->kind == smt::Kind::Function, "");
+	// TODO Use domain and codomain as key as well
+	if (!m_variables.count(_name))
+	{
+		auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
+		solAssert(fSort->codomain, "");
+		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
+		m_variables.insert(_name);
+		write(
+			"(declare-fun |" +
+			_name +
+			"| " +
+			domain +
+			" " +
+			codomain +
+			")"
+		);
+	}
+}
+
+void CHCSmtLib2Interface::write(string _data)
+{
+	m_accumulatedOutput += move(_data) + "\n";
+}
+
+string CHCSmtLib2Interface::querySolver(string const& _input)
+{
+	h256 inputHash = dev::keccak256(_input);
+	if (m_queryResponses.count(inputHash))
+		return m_queryResponses.at(inputHash);
+	else
+	{
+		m_unhandledQueries.push_back(_input);
+		return "unknown\n";
+	}
+}

libsolidity/formal/CHCSmtLib2Interface.h

@@ -0,0 +1,75 @@
+/*
+	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/>.
+*/
+
+/**
+ * Interface for solving Horn systems via smtlib2.
+ */
+
+#pragma once
+
+#include <libsolidity/formal/CHCSolverInterface.h>
+
+#include <libsolidity/formal/SMTLib2Interface.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class CHCSmtLib2Interface: public CHCSolverInterface
+{
+public:
+	explicit CHCSmtLib2Interface(std::map<h256, std::string> const& _queryResponses);
+
+	void reset();
+
+	void registerRelation(Expression const& _expr) override;
+
+	void addRule(Expression const& _expr, std::string const& _name) override;
+
+	std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
+
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
+
+	std::vector<std::string> unhandledQueries() const { return m_unhandledQueries; }
+
+	std::shared_ptr<SMTLib2Interface> smtlib2Interface() { return m_smtlib2; }
+
+private:
+	void declareFunction(std::string const& _name, SortPointer const& _sort);
+
+	void write(std::string _data);
+
+	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
+	std::string querySolver(std::string const& _input);
+
+	/// Used to access toSmtLibSort, SExpr, and handle variables.
+	/// Needs to be a shared_ptr since it's also passed to EncodingContext.
+	std::shared_ptr<SMTLib2Interface> m_smtlib2;
+
+	std::string m_accumulatedOutput;
+	std::set<std::string> m_variables;
+
+	std::map<h256, std::string> const& m_queryResponses;
+	std::vector<std::string> m_unhandledQueries;
+};
+
+}
+}
+}

libsolidity/formal/CHCSolverInterface.h

@@ -35,7 +35,7 @@ class CHCSolverInterface
 public:
 	virtual ~CHCSolverInterface() = default;
 
-	virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
+	virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
 
 	/// Takes a function declaration as a relation.
 	virtual void registerRelation(Expression const& _expr) = 0;

libsolidity/formal/CVC4Interface.cpp

@@ -48,10 +48,10 @@ void CVC4Interface::pop()
 	m_solver.pop();
 }
 
-void CVC4Interface::declareVariable(string const& _name, Sort const& _sort)
+void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	if (!m_variables.count(_name))
+	solAssert(_sort, "");
-		m_variables.insert({_name, m_context.mkVar(_name.c_str(), cvc4Sort(_sort))});
+	m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)

libsolidity/formal/CVC4Interface.h

@@ -50,7 +50,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;

libsolidity/formal/ModelChecker.cpp

@@ -24,7 +24,7 @@ using namespace dev::solidity;
 
 ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
 	m_bmc(m_context, _errorReporter, _smtlib2Responses),
-	m_chc(m_context, _errorReporter),
+	m_chc(m_context, _errorReporter, _smtlib2Responses),
 	m_context()
 {
 }
@@ -40,5 +40,5 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 vector<string> ModelChecker::unhandledQueries()
 {
-	return m_bmc.unhandledQueries();
+	return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
 }

libsolidity/formal/SMTEncoder.cpp

@@ -36,12 +36,37 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
-	solAssert(m_currentContract == nullptr, "");
+	solAssert(m_currentContract, "");
-	m_currentContract = &_contract;
 
-	initializeStateVariables(_contract);
+	for (auto const& node: _contract.subNodes())
+		if (!dynamic_pointer_cast<FunctionDefinition>(node))
+			node->accept(*this);
 
-	return true;
+	vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
+	for (auto const& base: _contract.annotation().linearizedBaseContracts)
+		for (auto const& baseFunction: base->definedFunctions())
+		{
+			if (baseFunction->isConstructor())
+				continue;
+			bool overridden = false;
+			for (auto const& function: resolvedFunctions)
+				if (
+					function->name() == baseFunction->name() &&
+					FunctionType(*function).asCallableFunction(false)->
+						hasEqualParameterTypes(*FunctionType(*baseFunction).asCallableFunction(false))
+				)
+				{
+					overridden = true;
+					break;
+				}
+			if (!overridden)
+				resolvedFunctions.push_back(baseFunction);
+		}
+
+	for (auto const& function: resolvedFunctions)
+		function->accept(*this);
+
+	return false;
 }
 
 void SMTEncoder::endVisit(ContractDefinition const& _contract)
@@ -110,9 +135,13 @@ void SMTEncoder::visitFunctionOrModifier()
 			*modifierInvocation->name()->annotation().referencedDeclaration
 		);
 		vector<smt::Expression> modifierArgsExpr;
-		if (modifierInvocation->arguments())
+		if (auto const* arguments = modifierInvocation->arguments())
-			for (auto arg: *modifierInvocation->arguments())
+		{
-				modifierArgsExpr.push_back(expr(*arg));
+			auto const& modifierParams = modifierDef.parameters();
+			solAssert(modifierParams.size() == arguments->size(), "");
+			for (unsigned i = 0; i < arguments->size(); ++i)
+				modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
+		}
 		initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
 		pushCallStack({&modifierDef, modifierInvocation.get()});
 		modifierDef.body().accept(*this);
@@ -512,6 +541,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	}
 }
 
+void SMTEncoder::initContract(ContractDefinition const& _contract)
+{
+	solAssert(m_currentContract == nullptr, "");
+	m_currentContract = &_contract;
+
+	initializeStateVariables(_contract);
+}
+
 void SMTEncoder::initFunction(FunctionDefinition const& _function)
 {
 	solAssert(m_callStack.empty(), "");
@@ -561,10 +598,10 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (_identifier.annotation().type->category() == Type::Category::Function)
-		visitFunctionIdentifier(_identifier);
 	else if (auto decl = identifierToVariable(_identifier))
 		defineExpr(_identifier, currentValue(*decl));
+	else if (_identifier.annotation().type->category() == Type::Category::Function)
+		visitFunctionIdentifier(_identifier);
 	else if (_identifier.name() == "now")
 		defineGlobalVariable(_identifier.name(), _identifier);
 	else if (_identifier.name() == "this")
@@ -665,7 +702,7 @@ void SMTEncoder::endVisit(Return const& _return)
 			}
 		}
 		else if (returnParams.size() == 1)
-			m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
+			m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front()));
 	}
 }
 
@@ -733,6 +770,15 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
+
+		if (varDecl->type()->category() == Type::Category::FixedBytes)
+		{
+			m_errorReporter.warning(
+				_indexAccess.location(),
+				"Assertion checker does not yet support index accessing fixed bytes."
+			);
+			return;
+		}
 	}
 	else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
 	{
@@ -774,78 +820,79 @@ void SMTEncoder::arrayAssignment()
 
 void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide)
 {
-	auto const& indexAccess = dynamic_cast<IndexAccess const&>(_expr);
+	auto toStore = _rightHandSide;
-	if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
+	auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
+	solAssert(indexAccess, "");
+	while (true)
 	{
-		auto varDecl = identifierToVariable(*id);
+		if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess->baseExpression()))
-		solAssert(varDecl, "");
-
-		if (varDecl->hasReferenceOrMappingType())
-			m_context.resetVariables([&](VariableDeclaration const& _var) {
-				if (_var == *varDecl)
-					return false;
-
-				// If both are state variables no need to clear knowledge.
-				if (_var.isStateVariable() && varDecl->isStateVariable())
-					return false;
-
-				TypePointer prefix = _var.type();
-				TypePointer originalType = typeWithoutPointer(varDecl->type());
-				while (
-					prefix->category() == Type::Category::Mapping ||
-					prefix->category() == Type::Category::Array
-				)
-				{
-					if (*originalType == *typeWithoutPointer(prefix))
-						return true;
-					if (prefix->category() == Type::Category::Mapping)
-					{
-						auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
-						solAssert(mapPrefix, "");
-						prefix = mapPrefix->valueType();
-					}
-					else
-					{
-						auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
-						solAssert(arrayPrefix, "");
-						prefix = arrayPrefix->baseType();
-					}
-				}
-				return false;
-			});
-
-		smt::Expression store = smt::Expression::store(
-			m_context.variable(*varDecl)->currentValue(),
-			expr(*indexAccess.indexExpression()),
-			_rightHandSide
-		);
-		m_context.addAssertion(m_context.newValue(*varDecl) == store);
-		// Update the SMT select value after the assignment,
-		// necessary for sound models.
-		defineExpr(indexAccess, smt::Expression::select(
-			m_context.variable(*varDecl)->currentValue(),
-			expr(*indexAccess.indexExpression())
-		));
-	}
-	else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
-	{
-		auto identifier = dynamic_cast<Identifier const*>(leftmostBase(indexAccess));
-		if (identifier)
 		{
-			auto varDecl = identifierToVariable(*identifier);
+			auto varDecl = identifierToVariable(*id);
-			m_context.newValue(*varDecl);
+			solAssert(varDecl, "");
-		}
 
-		m_errorReporter.warning(
+			if (varDecl->hasReferenceOrMappingType())
-			indexAccess.location(),
+				m_context.resetVariables([&](VariableDeclaration const& _var) {
-			"Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
+					if (_var == *varDecl)
-		);
+						return false;
+
+					// If both are state variables no need to clear knowledge.
+					if (_var.isStateVariable() && varDecl->isStateVariable())
+						return false;
+
+					TypePointer prefix = _var.type();
+					TypePointer originalType = typeWithoutPointer(varDecl->type());
+					while (
+						prefix->category() == Type::Category::Mapping ||
+						prefix->category() == Type::Category::Array
+					)
+					{
+						if (*originalType == *typeWithoutPointer(prefix))
+							return true;
+						if (prefix->category() == Type::Category::Mapping)
+						{
+							auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
+							solAssert(mapPrefix, "");
+							prefix = mapPrefix->valueType();
+						}
+						else
+						{
+							auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
+							solAssert(arrayPrefix, "");
+							prefix = arrayPrefix->baseType();
+						}
+					}
+					return false;
+				});
+
+			smt::Expression store = smt::Expression::store(
+				m_context.variable(*varDecl)->currentValue(),
+				expr(*indexAccess->indexExpression()),
+				toStore
+			);
+			m_context.addAssertion(m_context.newValue(*varDecl) == store);
+			// Update the SMT select value after the assignment,
+			// necessary for sound models.
+			defineExpr(*indexAccess, smt::Expression::select(
+				m_context.variable(*varDecl)->currentValue(),
+				expr(*indexAccess->indexExpression())
+			));
+
+			break;
+		}
+		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
+		{
+			toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore);
+			indexAccess = base;
+		}
+		else
+		{
+			m_errorReporter.warning(
+				_expr.location(),
+				"Assertion checker does not yet implement this expression."
+			);
+			break;
+		}
 	}
-	else
-		m_errorReporter.warning(
-			_expr.location(),
-			"Assertion checker does not yet implement this expression."
-		);
 }
 
 void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
@@ -1300,7 +1347,7 @@ void SMTEncoder::createExpr(Expression const& _e)
 void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value)
 {
 	createExpr(_e);
-	solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
+	solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
 	m_context.addAssertion(expr(_e) == _value);
 }
 

libsolidity/formal/SMTEncoder.h

@@ -107,6 +107,7 @@ protected:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void initContract(ContractDefinition const& _contract);
 	void initFunction(FunctionDefinition const& _function);
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);

libsolidity/formal/SMTLib2Interface.cpp

@@ -60,27 +60,29 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareVariable(string const& _name, Sort const& _sort)
+void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	if (_sort.kind == Kind::Function)
+	solAssert(_sort, "");
+	if (_sort->kind == Kind::Function)
 		declareFunction(_name, _sort);
 	else if (!m_variables.count(_name))
 	{
-		m_variables.insert(_name);
+		m_variables.emplace(_name, _sort);
-		write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
+		write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')');
 	}
 }
 
-void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
+void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort.kind == smt::Kind::Function, "");
+	solAssert(_sort, "");
+	solAssert(_sort->kind == smt::Kind::Function, "");
 	// TODO Use domain and codomain as key as well
 	if (!m_variables.count(_name))
 	{
-		FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+		auto const& fSort = dynamic_pointer_cast<FunctionSort>(_sort);
-		string domain = toSmtLibSort(fSort.domain);
+		string domain = toSmtLibSort(fSort->domain);
-		string codomain = toSmtLibSort(*fSort.codomain);
+		string codomain = toSmtLibSort(*fSort->codomain);
-		m_variables.insert(_name);
+		m_variables.emplace(_name, _sort);
 		write(
 			"(declare-fun |" +
 			_name +
@@ -159,6 +161,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Array:
 	{
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+		solAssert(arraySort.domain && arraySort.range, "");
 		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
 	}
 	default:

libsolidity/formal/SMTLib2Interface.h

@@ -48,20 +48,23 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(smt::Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
 
-private:
+	// Used by CHCSmtLib2Interface
-	void declareFunction(std::string const&, Sort const&);
-
 	std::string toSExpr(smt::Expression const& _expr);
 	std::string toSmtLibSort(Sort const& _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
+	std::map<std::string, SortPointer> variables() { return m_variables; }
+
+private:
+	void declareFunction(std::string const& _name, SortPointer const& _sort);
+
 	void write(std::string _data);
 
 	std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
@@ -71,7 +74,7 @@ private:
 	std::string querySolver(std::string const& _input);
 
 	std::vector<std::string> m_accumulatedOutput;
-	std::set<std::string> m_variables;
+	std::map<std::string, SortPointer> m_variables;
 
 	std::map<h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;

libsolidity/formal/SMTPortfolio.cpp

@@ -59,8 +59,9 @@ void SMTPortfolio::pop()
 		s->pop();
 }
 
-void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
+void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
 {
+	solAssert(_sort, "");
 	for (auto const& s: m_solvers)
 		s->declareVariable(_name, _sort);
 }

libsolidity/formal/SMTPortfolio.h

@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(smt::Expression const& _expr) override;
 

libsolidity/formal/SolverInterface.h

@@ -338,13 +338,13 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
+	virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
-	Expression newVariable(std::string _name, SortPointer _sort)
+	Expression newVariable(std::string _name, SortPointer const& _sort)
 	{
 		// Subclasses should do something here
 		solAssert(_sort, "");
-		declareVariable(_name, *_sort);
+		declareVariable(_name, _sort);
-		return Expression(std::move(_name), {}, std::move(_sort));
+		return Expression(std::move(_name), {}, _sort);
 	}
 
 	virtual void addAssertion(Expression const& _expr) = 0;

libsolidity/formal/SymbolicTypes.cpp

@@ -19,6 +19,7 @@
 
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/ast/Types.h>
+#include <libdevcore/CommonData.h>
 #include <memory>
 
 using namespace std;
@@ -139,7 +140,28 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 	else if (isBool(_type.category()))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
 	else if (isFunction(_type.category()))
-		var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
+	{
+		auto const& fType = dynamic_cast<FunctionType const*>(type);
+		auto const& paramsIn = fType->parameterTypes();
+		auto const& paramsOut = fType->returnParameterTypes();
+		auto findFunctionParam = [&](auto&& params) {
+			return find_if(
+				begin(params),
+				end(params),
+				[&](TypePointer _paramType) { return _paramType->category() == solidity::Type::Category::Function; }
+			);
+		};
+		if (
+			findFunctionParam(paramsIn) != end(paramsIn) ||
+			findFunctionParam(paramsOut) != end(paramsOut)
+		)
+		{
+			abstract = true;
+			var = make_shared<SymbolicIntVariable>(TypeProvider::uint256(), type, _uniqueName, _context);
+		}
+		else
+			var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
+	}
 	else if (isInteger(_type.category()))
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	else if (isFixedBytes(_type.category()))

libsolidity/formal/SymbolicVariables.cpp

@@ -19,7 +19,6 @@
 
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/ast/AST.h>
-#include <libsolidity/ast/TypeProvider.h>
 
 using namespace std;
 using namespace dev;
@@ -153,16 +152,38 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	solAssert(m_sort->kind == Kind::Function, "");
 }
 
-void SymbolicFunctionVariable::resetDeclaration()
+Expression SymbolicFunctionVariable::currentValue(solidity::TypePointer const& _targetType) const
 {
-	m_declaration = m_context.newVariable(currentName(), m_sort);
+	return m_abstract.currentValue(_targetType);
+}
+
+Expression SymbolicFunctionVariable::currentFunctionValue() const
+{
+	return m_declaration;
+}
+
+Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
+{
+	return m_abstract.valueAtIndex(_index);
+}
+
+Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
+{
+	return SymbolicVariable::valueAtIndex(_index);
+}
+
+Expression SymbolicFunctionVariable::resetIndex()
+{
+	SymbolicVariable::resetIndex();
+	return m_abstract.resetIndex();
 }
 
 Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
 	resetDeclaration();
-	return currentValue();
+	m_abstract.increaseIndex();
+	return m_abstract.currentValue();
 }
 
 Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) const
@@ -170,6 +191,11 @@ Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) c
 	return m_declaration(_arguments);
 }
 
+void SymbolicFunctionVariable::resetDeclaration()
+{
+	m_declaration = m_context.newVariable(currentName(), m_sort);
+}
+
 SymbolicMappingVariable::SymbolicMappingVariable(
 	solidity::TypePointer _type,
 	string _uniqueName,

libsolidity/formal/SymbolicVariables.h

@@ -20,6 +20,7 @@
 #include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SSAVariable.h>
 #include <libsolidity/ast/Types.h>
+#include <libsolidity/ast/TypeProvider.h>
 #include <memory>
 
 namespace dev
@@ -138,7 +139,12 @@ public:
 };
 
 /**
- * Specialization of SymbolicVariable for FunctionType
+ * Specialization of SymbolicVariable for FunctionType.
+ * Besides containing a symbolic function declaration,
+ * it also has an integer used as abstraction.
+ * By default, the abstract representation is used when
+ * values are requested, and the function declaration is
+ * used when operator() is applied over arguments.
  */
 class SymbolicFunctionVariable: public SymbolicVariable
 {
@@ -154,8 +160,20 @@ public:
 		EncodingContext& _context
 	);
 
-	Expression increaseIndex();
+	Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override;
-	Expression operator()(std::vector<Expression> _arguments) const;
+
+	// Explicit request the function declaration.
+	Expression currentFunctionValue() const;
+
+	Expression valueAtIndex(int _index) const override;
+
+	// Explicit request the function declaration.
+	Expression functionValueAtIndex(int _index) const;
+
+	Expression resetIndex() override;
+	Expression increaseIndex() override;
+
+	Expression operator()(std::vector<Expression> _arguments) const override;
 
 private:
 	/// Creates a new function declaration.
@@ -163,6 +181,14 @@ private:
 
 	/// Stores the current function declaration.
 	Expression m_declaration;
+
+	/// Abstract representation.
+	SymbolicIntVariable m_abstract{
+		TypeProvider::uint256(),
+		TypeProvider::uint256(),
+		m_uniqueName + "_abstract",
+		m_context
+	};
 };
 
 /**

libsolidity/formal/Z3CHCInterface.cpp

@@ -47,8 +47,9 @@ Z3CHCInterface::Z3CHCInterface():
 	m_solver.set(p);
 }
 
-void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort)
+void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
 {
+	solAssert(_sort, "");
 	m_z3Interface->declareVariable(_name, _sort);
 }
 

libsolidity/formal/Z3CHCInterface.h

@@ -37,7 +37,7 @@ public:
 	Z3CHCInterface();
 
 	/// Forwards variable declaration to Z3Interface.
-	void declareVariable(std::string const& _name, Sort const& _sort) override;
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 
 	void registerRelation(Expression const& _expr) override;
 

libsolidity/formal/Z3Interface.cpp

@@ -50,22 +50,25 @@ void Z3Interface::pop()
 	m_solver.pop();
 }
 
-void Z3Interface::declareVariable(string const& _name, Sort const& _sort)
+void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	if (_sort.kind == Kind::Function)
+	solAssert(_sort, "");
-		declareFunction(_name, _sort);
+	if (_sort->kind == Kind::Function)
-	else if (!m_constants.count(_name))
+		declareFunction(_name, *_sort);
-		m_constants.insert({_name, m_context.constant(_name.c_str(), z3Sort(_sort))});
+	else if (m_constants.count(_name))
+		m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(*_sort));
+	else
+		m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort)));
 }
 
 void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
 {
 	solAssert(_sort.kind == smt::Kind::Function, "");
-	if (!m_functions.count(_name))
+	FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
-	{
+	if (m_functions.count(_name))
-		FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+		m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
-		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain))});
+	else
-	}
+		m_functions.emplace(_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)));
 }
 
 void Z3Interface::addAssertion(Expression const& _expr)

libsolidity/formal/Z3Interface.h

@@ -38,7 +38,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const& _name, Sort const& _sort) override;
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;

libsolidity/interface/CompilerStack.cpp

@@ -43,6 +43,7 @@
 #include <libsolidity/interface/ABI.h>
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
+#include <libsolidity/interface/StorageLayout.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/parsing/Parser.h>
 
@@ -95,7 +96,7 @@ CompilerStack::~CompilerStack()
 	TypeProvider::reset();
 }
 
-boost::optional<CompilerStack::Remapping> CompilerStack::parseRemapping(string const& _remapping)
+std::optional<CompilerStack::Remapping> CompilerStack::parseRemapping(string const& _remapping)
 {
 	auto eq = find(_remapping.begin(), _remapping.end(), '=');
 	if (eq == _remapping.end())
@@ -269,7 +270,7 @@ bool CompilerStack::analyze()
 				noErrors = false;
 
 		m_globalContext = make_shared<GlobalContext>();
-		NameAndTypeResolver resolver(*m_globalContext, m_scopes, m_errorReporter);
+		NameAndTypeResolver resolver(*m_globalContext, m_evmVersion, m_scopes, m_errorReporter);
 		for (Source const* source: m_sourceOrder)
 			if (!resolver.registerDeclarations(*source->ast))
 				return false;
@@ -578,6 +579,14 @@ string const& CompilerStack::eWasm(string const& _contractName) const
 	return contract(_contractName).eWasm;
 }
 
+eth::LinkerObject const& CompilerStack::eWasmObject(string const& _contractName) const
+{
+	if (m_stackState != CompilationSuccessful)
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Compilation was not successful."));
+
+	return contract(_contractName).eWasmObject;
+}
+
 eth::LinkerObject const& CompilerStack::object(string const& _contractName) const
 {
 	if (m_stackState != CompilationSuccessful)
@@ -659,6 +668,28 @@ Json::Value const& CompilerStack::contractABI(Contract const& _contract) const
 	return *_contract.abi;
 }
 
+Json::Value const& CompilerStack::storageLayout(string const& _contractName) const
+{
+	if (m_stackState < AnalysisPerformed)
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Analysis was not successful."));
+
+	return storageLayout(contract(_contractName));
+}
+
+Json::Value const& CompilerStack::storageLayout(Contract const& _contract) const
+{
+	if (m_stackState < AnalysisPerformed)
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Analysis was not successful."));
+
+	solAssert(_contract.contract, "");
+
+	// caches the result
+	if (!_contract.storageLayout)
+		_contract.storageLayout.reset(new Json::Value(StorageLayout().generate(*_contract.contract)));
+
+	return *_contract.storageLayout;
+}
+
 Json::Value const& CompilerStack::natspecUser(string const& _contractName) const
 {
 	if (m_stackState < AnalysisPerformed)
@@ -1047,7 +1078,9 @@ void CompilerStack::generateEWasm(ContractDefinition const& _contract)
 	//cout << yul::AsmPrinter{}(*ewasmStack.parserResult()->code) << endl;
 
 	// Turn into eWasm text representation.
-	compiledContract.eWasm = ewasmStack.assemble(yul::AssemblyStack::Machine::eWasm).assembly;
+	auto result = ewasmStack.assemble(yul::AssemblyStack::Machine::eWasm);
+	compiledContract.eWasm = std::move(result.assembly);
+	compiledContract.eWasmObject = std::move(*result.bytecode);
 }
 
 CompilerStack::Contract const& CompilerStack::contract(string const& _contractName) const

libsolidity/interface/CompilerStack.h

@@ -121,7 +121,7 @@ public:
 	void reset(bool _keepSettings = false);
 
 	// Parses a remapping of the format "context:prefix=target".
-	static boost::optional<Remapping> parseRemapping(std::string const& _remapping);
+	static std::optional<Remapping> parseRemapping(std::string const& _remapping);
 
 	/// Sets path remappings.
 	/// Must be set before parsing.
@@ -232,9 +232,12 @@ public:
 	/// @returns the optimized IR representation of a contract.
 	std::string const& yulIROptimized(std::string const& _contractName) const;
 
-	/// @returns the eWasm (text) representation of a contract.
+	/// @returns the eWasm text representation of a contract.
 	std::string const& eWasm(std::string const& _contractName) const;
 
+	/// @returns the eWasm representation of a contract.
+	eth::LinkerObject const& eWasmObject(std::string const& _contractName) const;
+
 	/// @returns the assembled object for a contract.
 	eth::LinkerObject const& object(std::string const& _contractName) const;
 
@@ -269,6 +272,10 @@ public:
 	/// Prerequisite: Successful call to parse or compile.
 	Json::Value const& contractABI(std::string const& _contractName) const;
 
+	/// @returns a JSON representing the storage layout of the contract.
+	/// Prerequisite: Successful call to parse or compile.
+	Json::Value const& storageLayout(std::string const& _contractName) const;
+
 	/// @returns a JSON representing the contract's user documentation.
 	/// Prerequisite: Successful call to parse or compile.
 	Json::Value const& natspecUser(std::string const& _contractName) const;
@@ -312,9 +319,11 @@ private:
 		eth::LinkerObject runtimeObject; ///< Runtime object.
 		std::string yulIR; ///< Experimental Yul IR code.
 		std::string yulIROptimized; ///< Optimized experimental Yul IR code.
-		std::string eWasm; ///< Experimental eWasm code (text representation).
+		std::string eWasm; ///< Experimental eWasm text representation
+		eth::LinkerObject eWasmObject; ///< Experimental eWasm code
 		mutable std::unique_ptr<std::string const> metadata; ///< The metadata json that will be hashed into the chain.
 		mutable std::unique_ptr<Json::Value const> abi;
+		mutable std::unique_ptr<Json::Value const> storageLayout;
 		mutable std::unique_ptr<Json::Value const> userDocumentation;
 		mutable std::unique_ptr<Json::Value const> devDocumentation;
 		mutable std::unique_ptr<std::string const> sourceMapping;
@@ -346,7 +355,7 @@ private:
 	/// The IR is stored but otherwise unused.
 	void generateIR(ContractDefinition const& _contract);
 
-	/// Generate eWasm text representation for a single contract.
+	/// Generate eWasm representation for a single contract.
 	void generateEWasm(ContractDefinition const& _contract);
 
 	/// Links all the known library addresses in the available objects. Any unknown
@@ -378,6 +387,10 @@ private:
 	/// This will generate the JSON object and store it in the Contract object if it is not present yet.
 	Json::Value const& contractABI(Contract const&) const;
 
+	/// @returns the storage layout of the contract as a JSON object.
+	/// This will generate the JSON object and store it in the Contract object if it is not present yet.
+	Json::Value const& storageLayout(Contract const&) const;
+
 	/// @returns the Natspec User documentation as a JSON object.
 	/// This will generate the JSON object and store it in the Contract object if it is not present yet.
 	Json::Value const& natspecUser(Contract const&) const;

libsolidity/interface/StandardCompiler.cpp

@@ -31,8 +31,9 @@
 
 #include <boost/algorithm/cxx11/any_of.hpp>
 #include <boost/algorithm/string.hpp>
-#include <boost/optional.hpp>
+
 #include <algorithm>
+#include <optional>
 
 using namespace std;
 using namespace dev;
@@ -317,7 +318,7 @@ Json::Value collectEVMObject(eth::LinkerObject const& _object, string const* _so
 	return output;
 }
 
-boost::optional<Json::Value> checkKeys(Json::Value const& _input, set<string> const& _keys, string const& _name)
+std::optional<Json::Value> checkKeys(Json::Value const& _input, set<string> const& _keys, string const& _name)
 {
 	if (!!_input && !_input.isObject())
 		return formatFatalError("JSONError", "\"" + _name + "\" must be an object");
@@ -326,46 +327,46 @@ boost::optional<Json::Value> checkKeys(Json::Value const& _input, set<string> co
 		if (!_keys.count(member))
 			return formatFatalError("JSONError", "Unknown key \"" + member + "\"");
 
-	return boost::none;
+	return std::nullopt;
 }
 
-boost::optional<Json::Value> checkRootKeys(Json::Value const& _input)
+std::optional<Json::Value> checkRootKeys(Json::Value const& _input)
 {
 	static set<string> keys{"auxiliaryInput", "language", "settings", "sources"};
 	return checkKeys(_input, keys, "root");
 }
 
-boost::optional<Json::Value> checkSourceKeys(Json::Value const& _input, string const& _name)
+std::optional<Json::Value> checkSourceKeys(Json::Value const& _input, string const& _name)
 {
 	static set<string> keys{"content", "keccak256", "urls"};
 	return checkKeys(_input, keys, "sources." + _name);
 }
 
-boost::optional<Json::Value> checkAuxiliaryInputKeys(Json::Value const& _input)
+std::optional<Json::Value> checkAuxiliaryInputKeys(Json::Value const& _input)
 {
 	static set<string> keys{"smtlib2responses"};
 	return checkKeys(_input, keys, "auxiliaryInput");
 }
 
-boost::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
+std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 {
 	static set<string> keys{"parserErrorRecovery", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings"};
 	return checkKeys(_input, keys, "settings");
 }
 
-boost::optional<Json::Value> checkOptimizerKeys(Json::Value const& _input)
+std::optional<Json::Value> checkOptimizerKeys(Json::Value const& _input)
 {
 	static set<string> keys{"details", "enabled", "runs"};
 	return checkKeys(_input, keys, "settings.optimizer");
 }
 
-boost::optional<Json::Value> checkOptimizerDetailsKeys(Json::Value const& _input)
+std::optional<Json::Value> checkOptimizerDetailsKeys(Json::Value const& _input)
 {
 	static set<string> keys{"peephole", "jumpdestRemover", "orderLiterals", "deduplicate", "cse", "constantOptimizer", "yul", "yulDetails"};
 	return checkKeys(_input, keys, "settings.optimizer.details");
 }
 
-boost::optional<Json::Value> checkOptimizerDetail(Json::Value const& _details, std::string const& _name, bool& _setting)
+std::optional<Json::Value> checkOptimizerDetail(Json::Value const& _details, std::string const& _name, bool& _setting)
 {
 	if (_details.isMember(_name))
 	{
@@ -376,7 +377,7 @@ boost::optional<Json::Value> checkOptimizerDetail(Json::Value const& _details, s
 	return {};
 }
 
-boost::optional<Json::Value> checkMetadataKeys(Json::Value const& _input)
+std::optional<Json::Value> checkMetadataKeys(Json::Value const& _input)
 {
 	if (_input.isObject() && _input.isMember("useLiteralContent") && !_input["useLiteralContent"].isBool())
 		return formatFatalError("JSONError", "\"settings.metadata.useLiteralContent\" must be Boolean");
@@ -384,7 +385,7 @@ boost::optional<Json::Value> checkMetadataKeys(Json::Value const& _input)
 	return checkKeys(_input, keys, "settings.metadata");
 }
 
-boost::optional<Json::Value> checkOutputSelection(Json::Value const& _outputSelection)
+std::optional<Json::Value> checkOutputSelection(Json::Value const& _outputSelection)
 {
 	if (!!_outputSelection && !_outputSelection.isObject())
 		return formatFatalError("JSONError", "\"settings.outputSelection\" must be an object");
@@ -426,7 +427,7 @@ boost::optional<Json::Value> checkOutputSelection(Json::Value const& _outputSele
 		}
 	}
 
-	return boost::none;
+	return std::nullopt;
 }
 /// Validates the optimizer settings and returns them in a parsed object.
 /// On error returns the json-formatted error message.
@@ -635,7 +636,7 @@ boost::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompile
 	{
 		if (!settings["evmVersion"].isString())
 			return formatFatalError("JSONError", "evmVersion must be a string.");
-		boost::optional<langutil::EVMVersion> version = langutil::EVMVersion::fromString(settings["evmVersion"].asString());
+		std::optional<langutil::EVMVersion> version = langutil::EVMVersion::fromString(settings["evmVersion"].asString());
 		if (!version)
 			return formatFatalError("JSONError", "Invalid EVM version requested.");
 		ret.evmVersion = *version;
@@ -886,10 +887,12 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 		string file = contractName.substr(0, colon);
 		string name = contractName.substr(colon + 1);
 
-		// ABI, documentation and metadata
+		// ABI, storage layout, documentation and metadata
 		Json::Value contractData(Json::objectValue);
 		if (isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "abi", wildcardMatchesExperimental))
 			contractData["abi"] = compilerStack.contractABI(contractName);
+		if (isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "storageLayout", false))
+			contractData["storageLayout"] = compilerStack.storageLayout(contractName);
 		if (isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "metadata", wildcardMatchesExperimental))
 			contractData["metadata"] = compilerStack.metadata(contractName);
 		if (isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "userdoc", wildcardMatchesExperimental))
@@ -906,6 +909,8 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
 		// eWasm
 		if (compilationSuccess && isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "ewasm.wast", wildcardMatchesExperimental))
 			contractData["ewasm"]["wast"] = compilerStack.eWasm(contractName);
+		if (compilationSuccess && isArtifactRequested(_inputsAndSettings.outputSelection, file, name, "ewasm.wasm", wildcardMatchesExperimental))
+			contractData["ewasm"]["wasm"] = compilerStack.eWasmObject(contractName).toHex();
 
 		// EVM
 		Json::Value evmData(Json::objectValue);

libsolidity/interface/StandardCompiler.h

@@ -24,7 +24,7 @@
 
 #include <libsolidity/interface/CompilerStack.h>
 
-#include <boost/optional.hpp>
+#include <optional>
 #include <boost/variant.hpp>
 
 namespace dev

libsolidity/interface/StorageLayout.cpp

@@ -0,0 +1,119 @@
+/*
+	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/>.
+*/
+
+#include <libsolidity/interface/StorageLayout.h>
+
+#include <libsolidity/ast/TypeProvider.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+Json::Value StorageLayout::generate(ContractDefinition const& _contractDef)
+{
+	solAssert(!m_contract, "");
+	m_contract = &_contractDef;
+	m_types.clear();
+
+	auto typeType = dynamic_cast<TypeType const*>(_contractDef.type());
+	solAssert(typeType, "");
+	auto contractType = dynamic_cast<ContractType const*>(typeType->actualType());
+	solAssert(contractType, "");
+
+	Json::Value variables(Json::arrayValue);
+	for (auto [var, slot, offset]: contractType->stateVariables())
+		variables.append(generate(*var, slot, offset));
+
+	Json::Value layout;
+	layout["storage"] = move(variables);
+	layout["types"] = move(m_types);
+	return layout;
+}
+
+Json::Value StorageLayout::generate(VariableDeclaration const& _var, u256 const& _slot, unsigned _offset)
+{
+	Json::Value varEntry;
+	TypePointer varType = _var.type();
+
+	varEntry["label"] = _var.name();
+	varEntry["astId"] = int(_var.id());
+	varEntry["contract"] = m_contract->fullyQualifiedName();
+	varEntry["slot"] = _slot.str();
+	varEntry["offset"] = _offset;
+	varEntry["type"] = typeKeyName(varType);
+
+	generate(varType);
+
+	return varEntry;
+}
+
+void StorageLayout::generate(TypePointer _type)
+{
+	if (m_types.isMember(typeKeyName(_type)))
+		return;
+
+	// Register it now to cut recursive visits.
+	Json::Value& typeInfo = m_types[typeKeyName(_type)];
+	typeInfo["label"] = _type->toString(true);
+	typeInfo["numberOfBytes"] = u256(_type->storageBytes() * _type->storageSize()).str();
+
+	if (auto structType = dynamic_cast<StructType const*>(_type))
+	{
+		Json::Value members(Json::arrayValue);
+		auto const& structDef = structType->structDefinition();
+		for (auto const& member: structDef.members())
+		{
+			auto const& offsets = structType->storageOffsetsOfMember(member->name());
+			members.append(generate(*member, offsets.first, offsets.second));
+		}
+		typeInfo["members"] = move(members);
+		typeInfo["encoding"] = "inplace";
+	}
+	else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
+	{
+		typeInfo["key"] = typeKeyName(mappingType->keyType());
+		typeInfo["value"] = typeKeyName(mappingType->valueType());
+		generate(mappingType->keyType());
+		generate(mappingType->valueType());
+		typeInfo["encoding"] = "mapping";
+	}
+	else if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
+	{
+		if (arrayType->isByteArray())
+			typeInfo["encoding"] = "bytes";
+		else
+		{
+			typeInfo["base"] = typeKeyName(arrayType->baseType());
+			generate(arrayType->baseType());
+			typeInfo["encoding"] = arrayType->isDynamicallySized() ? "dynamic_array" : "inplace";
+		}
+	}
+	else
+	{
+		solAssert(_type->isValueType(), "");
+		typeInfo["encoding"] = "inplace";
+	}
+
+	solAssert(typeInfo.isMember("encoding"), "");
+}
+
+string StorageLayout::typeKeyName(TypePointer _type)
+{
+	if (auto refType = dynamic_cast<ReferenceType const*>(_type))
+		return TypeProvider::withLocationIfReference(refType->location(), _type)->richIdentifier();
+	return _type->richIdentifier();
+}

libsolidity/interface/StorageLayout.h

@@ -0,0 +1,58 @@
+/*
+	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/>.
+*/
+/**
+ * Generates the storage layout of a contract.
+ */
+
+#pragma once
+
+#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
+
+#include <json/json.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+class StorageLayout
+{
+public:
+	/// Generates the storage layout of the contract
+	/// @param _contractDef The contract definition
+	/// @return A JSON representation of the contract's storage layout.
+	Json::Value generate(ContractDefinition const& _contractDef);
+
+private:
+	/// Generates the JSON information for a variable and its storage location.
+	Json::Value generate(VariableDeclaration const& _var, u256 const& _slot, unsigned _offset);
+
+	/// Generates the JSON information for @param _type
+	void generate(TypePointer _type);
+
+	/// The key for the JSON object describing a type.
+	std::string typeKeyName(TypePointer _type);
+
+	Json::Value m_types;
+
+	/// Current analyzed contract
+	ContractDefinition const* m_contract = nullptr;
+};
+
+}
+}

libsolidity/parsing/Parser.cpp

@@ -241,7 +241,7 @@ ASTPointer<ImportDirective> Parser::parseImportDirective()
 ContractDefinition::ContractKind Parser::parseContractKind()
 {
 	ContractDefinition::ContractKind kind;
-	switch(m_scanner->currentToken())
+	switch (m_scanner->currentToken())
 	{
 	case Token::Interface:
 		kind = ContractDefinition::ContractKind::Interface;
@@ -388,7 +388,7 @@ StateMutability Parser::parseStateMutability()
 {
 	StateMutability stateMutability(StateMutability::NonPayable);
 	Token token = m_scanner->currentToken();
-	switch(token)
+	switch (token)
 	{
 		case Token::Payable:
 			stateMutability = StateMutability::Payable;
@@ -874,7 +874,9 @@ ASTPointer<TypeName> Parser::parseTypeName(bool _allowVar)
 		ASTNodeFactory nodeFactory(*this);
 		nodeFactory.markEndPosition();
 		m_scanner->next();
-		auto stateMutability = boost::make_optional(elemTypeName.token() == Token::Address, StateMutability::NonPayable);
+		auto stateMutability = elemTypeName.token() == Token::Address
+			? optional<StateMutability>{StateMutability::NonPayable}
+			: nullopt;
 		if (TokenTraits::isStateMutabilitySpecifier(m_scanner->currentToken(), false))
 		{
 			if (elemTypeName.token() == Token::Address)

libyul/AsmAnalysis.h

@@ -31,11 +31,11 @@
 #include <libyul/backends/evm/EVMDialect.h>
 
 #include <boost/variant.hpp>
-#include <boost/optional.hpp>
 
 #include <functional>
 #include <list>
 #include <memory>
+#include <optional>
 
 namespace langutil
 {
@@ -59,7 +59,7 @@ public:
 	explicit AsmAnalyzer(
 		AsmAnalysisInfo& _analysisInfo,
 		langutil::ErrorReporter& _errorReporter,
-		boost::optional<langutil::Error::Type> _errorTypeForLoose,
+		std::optional<langutil::Error::Type> _errorTypeForLoose,
 		Dialect const& _dialect,
 		ExternalIdentifierAccess::Resolver const& _resolver = ExternalIdentifierAccess::Resolver(),
 		std::set<YulString> const& _dataNames = {}
@@ -127,7 +127,7 @@ private:
 	langutil::ErrorReporter& m_errorReporter;
 	langutil::EVMVersion m_evmVersion;
 	Dialect const& m_dialect;
-	boost::optional<langutil::Error::Type> m_errorTypeForLoose;
+	std::optional<langutil::Error::Type> m_errorTypeForLoose;
 	/// Names of data objects to be referenced by builtin functions with literal arguments.
 	std::set<YulString> m_dataNames;
 	ForLoop const* m_currentForLoop = nullptr;

libyul/AsmScope.h

@@ -27,10 +27,10 @@
 #include <libdevcore/Visitor.h>
 
 #include <boost/variant.hpp>
-#include <boost/optional.hpp>
 
 #include <functional>
 #include <memory>
+#include <optional>
 
 namespace yul
 {

libyul/AssemblyStack.cpp

@@ -117,7 +117,7 @@ bool AssemblyStack::analyzeParsed(Object& _object)
 	AsmAnalyzer analyzer(
 		*_object.analysisInfo,
 		m_errorReporter,
-		boost::none,
+		std::nullopt,
 		languageToDialect(m_language, m_evmVersion),
 		{},
 		_object.dataNames()
@@ -200,7 +200,10 @@ MachineAssemblyObject AssemblyStack::assemble(Machine _machine) const
 		Dialect const& dialect = languageToDialect(m_language, EVMVersion{});
 
 		MachineAssemblyObject object;
-		object.assembly = EWasmObjectCompiler::compile(*m_parserResult, dialect);
+		auto result = EWasmObjectCompiler::compile(*m_parserResult, dialect);
+		object.assembly = std::move(result.first);
+		object.bytecode = make_shared<dev::eth::LinkerObject>();
+		object.bytecode->bytecode = std::move(result.second);
 		return object;
 	}
 	}

libyul/CMakeLists.txt

@@ -50,6 +50,8 @@ add_library(yul
 	backends/wasm/EWasmObjectCompiler.h
 	backends/wasm/EWasmToText.cpp
 	backends/wasm/EWasmToText.h
+	backends/wasm/BinaryTransform.cpp
+	backends/wasm/BinaryTransform.h
 	backends/wasm/WasmDialect.cpp
 	backends/wasm/WasmDialect.h
 	backends/wasm/WordSizeTransform.cpp
@@ -66,6 +68,10 @@ add_library(yul
 	optimiser/CallGraphGenerator.h
 	optimiser/CommonSubexpressionEliminator.cpp
 	optimiser/CommonSubexpressionEliminator.h
+	optimiser/ConditionalSimplifier.cpp
+	optimiser/ConditionalSimplifier.h
+	optimiser/ConditionalUnsimplifier.cpp
+	optimiser/ConditionalUnsimplifier.h
 	optimiser/ControlFlowSimplifier.cpp
 	optimiser/ControlFlowSimplifier.h
 	optimiser/DataFlowAnalyzer.cpp

libyul/Utilities.cpp

@@ -113,7 +113,7 @@ u256 yul::valueOfBoolLiteral(Literal const& _literal)
 
 u256 yul::valueOfLiteral(Literal const& _literal)
 {
-	switch(_literal.kind)
+	switch (_literal.kind)
 	{
 		case LiteralKind::Number:
 			return valueOfNumberLiteral(_literal);

libyul/backends/evm/EVMCodeTransform.cpp

@@ -723,9 +723,7 @@ void CodeTransform::visitExpression(Expression const& _expression)
 
 void CodeTransform::visitStatements(vector<Statement> const& _statements)
 {
-	// Workaround boost bug:
+	std::optional<AbstractAssembly::LabelID> jumpTarget = std::nullopt;
-	// https://www.boost.org/doc/libs/1_63_0/libs/optional/doc/html/boost_optional/tutorial/gotchas/false_positive_with__wmaybe_uninitialized.html
-	boost::optional<AbstractAssembly::LabelID> jumpTarget = boost::make_optional(false, AbstractAssembly::LabelID());
 
 	for (auto const& statement: _statements)
 	{
@@ -740,7 +738,7 @@ void CodeTransform::visitStatements(vector<Statement> const& _statements)
 		else if (!functionDefinition && jumpTarget)
 		{
 			m_assembly.appendLabel(*jumpTarget);
-			jumpTarget = boost::none;
+			jumpTarget = std::nullopt;
 		}
 
 		boost::apply_visitor(*this, statement);

libyul/backends/evm/EVMCodeTransform.h

@@ -28,8 +28,8 @@
 #include <libyul/AsmScope.h>
 
 #include <boost/variant.hpp>
-#include <boost/optional.hpp>
 
+#include <optional>
 #include <stack>
 
 namespace langutil