SOLTIX: Scalable automated framework for testing Solidity compilers.

SOLTIX is a framework for automated testing of Solidity compilers supported by the Ethereum Foundation and the ICE Center, ETH Zurich. The research and development of SOLTIX started at the ICE center, as the MSc thesis project of Nils Weller under the supervision of Dr. Petar Tsankov and Prof. Martin Vechev.

The project now is an open platform welcoming contributors from the Ethereum community. To learn more about the framework, build on top of it or extend it to other virtual machines, please get in touch with the core team and contributors at our Discord group.

Bugs found so far

So far SOLTIX has found several bugs in the official Solidity compiler (solc) and ganache-cli.

1. Solidity compiler bugs

SOLTIX has found the following two bugs in the solc solidity compiler:

1. Exponentiation bug: This bug results in incorrect computations of exponents. The bug was fixed in version 0.4.25.

2. Internal compiler error bug: This bug results in an internal compiler error in various solc versions. The bug was fixed in version 0.5.1.

Optimization-related errors have been observed with some test cases (1, 2) on solc 0.5.0+commit.1d4f565a.Emscripten.clang. These have not been analyzed in detail, as they no longer occur with more recent versions.

2. Ganache-cli bugs

SOLTIX has also discovered two bugs in ganache-cli:

1. Shift and exponentiation crashes: The bugs have not been fixed yet.

SOLTIX overview

SOLTIX tests the Solidity compiler and, in turn, the Ethereum Virtual Machine (EVM) in a fully automated way. For this purpose, SOLTIX provides the following two testing modules:

1. Testing via synthesis of random Solidity contracts

The synthesis module tests the Solidity compiler without requiring access to Solidity contracts or transactions. The high-level flow is illustrated in the following figure:

To test the compiler, SOLTIX is provided with a set of parameters (such as number of variables, functions, etc.) which define the Solidity contract which will be synthesized. As a first step, SOLTIX generates transactions and a Solidity contract. The synthesized Solidity contract is instrumented by emit statements that raise an error in case the contract execution is unexpected. In the illustrated example, SOLTIX will execute the transaction foo(10) which should follow the false branch of the if (x != 5) condition. Therefore, SOLTIX throws an error in case the contract's execution proceeds along the true branch. To test the compiler, SOLTIX compiles the Solidity contract into EVM bytecode and executes it, keeping track of all emitted events. Based on the the emitted events, SOLTIX reports an error if an error event has been emitted.

2. Testing via synthesis of semantically equivalent Solidity smart contracts

The equivalence testing module works by generating a large number of semantically equivalent Solidity contracts for a given set of transactions and tests whether they all reach the same state when the transactions are executed. The high-level flow of this module is illustrated in the following figure:

The input to this module is a Solidity contract and a sequence of transactions (e.g. foo(10), foo(15)). First, SOLTIX executes the Solidity contract with the provided transactions and records relevant execution profile information, such as the possible variable values observed at different program counters. In our example, the variable x is assigned values 11 and 16 at Line 4 of the contract (for the provided two transactions). Next, SOLTIX generates a large number of semantically equivalent Solidity contracts. In our example, it introduces a new if (x/2 > y) statement which always holds for the provided transactions. The synthesized Solidity contracts are compiled using solc and executed, while recording the final state of the contracts. The final states are compared to assess whether the compilation step was successful or not.

The remaining part of this document how knowledge on expected behavior is obtained, what types of contracts are generated and how, and how the original equivalence testing technique is integrated to mutated programs.

Contents

1. Getting started
   • Requirements
   • Build
   • Use
     • Generation
     • Execution
2. Known limitations
3. Technical details
   • Contract behavior
   • Code generation
   • Equivalence-testing transformation

Getting started

The framework can be used in Docker or natively on Linux systems.

Docker installation

To build a Docker image containing the ready-to-use framework, run:

docker build . -t soltix

The Docker-specifics section describes how to use it.

Native installation

To perform a native installation of the framework, follow the steps described in this section.

Requirements

• Operating system: Linux or macOS
• Java 8+
• Maven
• NodeJS 10+ (to use truffle and ganache-cli)
• GNU C++ (g++)

For Ubuntu Linux, the dependencies can be installed with apt-get using the commands listed below.

Java 8+ (OpenJDK):

    sudo apt-get -y install openjdk-8-jdk

Maven:

    sudo apt-get install maven

git, wget, cmake, build-essential (to auto-fetch and build geth from github):

    sudo apt-get install git wget cmake build-essential

NodeJS:

    sudo apt-get install nodejs

If nodejs is already installed in a version older than 10, it can be updated using the following commands:

    sudo npm cache clean -f
    sudo npm install -g n
    sudo n stable

Instead of installing or updating nodejs for the whole system, it is also possible to download and build a recent nodejs version in the user's home directory by executing the script:

    ./tools/node-local-setup.sh

This requires no sudo access and creates nodejs binaries in the ~/local/bin directory.

Build

To build and configure the SOLTIX software on Linux (macOS is currently unsupported natively - use docker instead), execute the interactive setup script and answer its questions:

    ./setup.sh

Alternatively, to use default values for everything, use:

    ./setup.sh --use-defaults

This will generate a settings.cfg.sh file that contains various configurable settings, such as the compiler to be used (solcjs or solc) and its optimization settings. Note that ganache-cli and restricted code generation options are used by default - switching to geth and enabling more advanced features is desirable for many purposes.

Use

A basic introduction to the most important framework commands is given below. A technical overview on what these commands do is described at the end of this document in the technical details section.

Docker specifics

The commands described below have the same form regardless of whether you use the Docker image or a native installation. When using Docker, they are started with the "docker run" command. Because state is not persisted in the container, command sequences such as:

    docker run soltix ./soltix/bin/generate-contract-set.sh ... <output-directory>
    docker run soltix ./test-env-truffle/bin/run-all-tests.sh <output-directory>

would normally fail due to the contract set getting purged when the generation command ends. In order to address this, a local filesystem directory can be mounted as container volume to store contracts - this is also desirable when working on test code.

To store contracts in the host's current working directory (in $PWD/TMP) and address them from the container by using a "/VOL" prefix, the following example commands generate and execute a contract set containing one contract):

    docker run --mount type=bind,source=$PWD,target=/VOL soltix ./soltix/bin/generate-contract-set.sh 1 1 1 1 1 1 /VOL/TMP --complete
    docker run --mount type=bind,source=$PWD,target=/VOL soltix ./test-env-truffle/bin/run-all-tests.sh /VOL/TMP 0

Generated contract sets can automatically be parallelized with docker instances, as described in the section on combined generation and execution. These scripts also remove the necessity of storing intermediate generated contracts in a mounted volume.

Introduction

As described in the overview, the framework can execute smart contracts - using randomly generated transactions - and analyze their behavior to infer potential miscompilations.

The test process for one smart contract can be separated into

1. An optional contract generation phase
2. A contract execution phase

The framework's contract generation functions can be used to produce the initial seed program for the execution phase, but an externally supplied contract may be used instead as well.

If equivalence-testing transformation is requested, the contract execution phase will involve multiple intertwined additional steps to profile the supplied seed program, generate multiple variants of the seed program, and execute them to detect behavioral differences.

As described in the contract behavior section, executing contracts without any equivalence-testing transformations can also be produce meaningful information on program execution correctness, particularly for contracts that are self-contained due to internal correctness checks - as described below - or to compare the behavior of the same contract executed at varying optimization levels.

The generation scripts are described below, followed by the execution scripts, and finally a section on convenience scripts that combine generation and execution and also enable parallelization with docker.

Generation

This section describes the optional seed program generation phase in the test process introduced above. There are two types of contracts that can be generated. Both of them contain storage variables, as well as functions that differ in the code they contain:

1. Assignment sequence (AS) contracts use a sequence of assignment expression statements
2. Complete contracts use random statement combinations including (potentially nested) control structures

AS contracts contain built-in correctness checks that verify the correct program behavior - at the cost of structural simplicity. Complete contracts add more complexity, but have no such built-in correctness checks. This makes their combination with equivalence-testing or different optimization level testing particularly desirable to obtain meaningful tests.

Generating a single contract

A random contract with a Solidity file and test transactions can be generated using the generate-contract.sh script.

A contract is generally identified by the following 6-tuple:

1. Random number seed number
2. Number of functions in contract
3. Minimum number of code units per function
4. Maximum number of code units per function
5. Number of variables in contract
6. Choice of contract type (--assignmentSequence or --complete)

Since random numbers are currently generated by the Java PRNG, the same 6-tuple may however produce programs that vary between systems using different Java PRNG versions.

Example

To generate an AS contract with a PRNG seed of 0, 10 functions, 1-2 code units per function, and 20 variables in the directory "X", run:

    ./soltix/bin/generate-contract.sh 0 10 1 2 20 X --assignmentSequence

This will automatically also generate 4 semantically equivalent contract files, since the expected behavior of AS is known at generation time.

To do the same thing for a contract of type "complete":

    ./soltix/bin/generate-contract.sh 0 10 1 2 20 X --complete

This will not generate any mutations, since complete contracts must first be executed with instrumentation to measure their behavior.

Generating a contract set

A contract set containing multiple contracts can be generated using the generate-contract-set.sh script. Its first argument is the count of contracts to generate, the remaining arguments are the same as in the single-contract case above - with the given seed getting incremented for each generated contract.

To generate 5 contracts in sub-directories to directory "X" with the same properties as in the precding example (10 functions, 1-2 code units per function, 20 variables) from seed 0 to 4, run:

    ./soltix/bin/generate-contract-set.sh 5 0 10 1 2 20 X --complete

Execution

This section describes the execution phase in the test process summarized in the introduction. It works on contracts that were either generated in the generation phase described above, or made available from some external source. The execution phase may involve multiple execution and code generation steps if semantically equivalent transformations are requested.

Generated contracts are already available in the form of a truffle-compatible project directory containing the contract, a deployment script, and a test file with the transactions. Externally supplied contracts are expected