runtimeverification / solidity

Fork of the Solidity Compiler for compiling Solidity to IELE

The Solidity to IELE Compiler

This is the Solidity to IELE compiler, a fork of the Solidity compiler targeting the IELE virtual machine (instead of the EVM).

To learn more about the supported Solidity features and the main differences between the IELE and EVM compilers, see README-IELE-SUPPORT.

Solidity is a statically typed, contract-oriented, high-level language for implementing smart contracts on the Ethereum platform.

Building

Prerequisites

• install IELE.

Dependencies

For MacOS:

brew update
brew install boost
brew install cmake
brew install llvm@11
brew install libxml2
brew upgrade

For Ubuntu-based systems:

sudo apt-get update
sudo apt-get install build-essential cmake g++ gcc git libboost-all-dev unzip llvm-11 zlib1g-dev libz3-dev libxml2-utils

Please note that we have tested the compiler for the Ubuntu 20.04 and MacOS BigSur operation system.

Build the compiler

mkdir build
cd build
cmake ..
make

Usage

Use the compiler like this:

./build/solc/isolc --asm <solidity file>

Testing

To run the execution test suite, first start an IELE vm in separate terminal (this assumes the kiele exexcutable is found in the system's PATH):

kiele vm --port 9001

Then, start the iele-test-clientexecutable in a separate terminal:

iele-test-client <path to Solidity-to-IELE build directory>/ipcfile 9001

Note that, there is no need for an exisiting ipcfile, this command will create a fresh one. You may need to delete an existing ipcfile before you restart this script.

Also note that the iele-test-client executable can be found in "$(dirname `which kiele`)/../lib/kiele", assuming the kiele executable is in the system's PATH.

Finally, you can run the whole execution test suite with:

./build/test/soltest --no_result_code \
                     --report_sink=build/report.xml \
                     --report_level=detailed \
                     --report_format=XML \
                     --log_sink=build/log.xml \
                     --log_level=all \
                     --log_format=XML  \
                     `cat test/failing-exec-tests` \
                     `cat test/out-of-scope-exec-tests` \
                     `cat test/unimplemented-features-tests` \
                     -- \
                     --enforce-no-yul-ewasm \
                     --ipcpath build/ipcfile \
                     --testpath test

xmllint --xpath "//TestCase[@assertions_failed!=@expected_failures]" build/report.xml && false

The output of the last command should look like this for a successful run of the test suite:

XPath set is empty

Alternatively, you can run a specific test with:

./build/test/soltest --no_result_code -t <test name> -- --enforce-no-yul-ewasm --ipcpath build/ipcfile --testpath test

where <test name> is the name with which the test is registered in the test suite. For example, the test found in test/libsolidity/semanticTests/operators/shifts/shift_right.sol, is registered in the test suite with the name semanticTests/operators/shifts/shift_right.

solidity's Issues

Solidity feature: Contract Creation via `new`

Solidity Feature: MemberAccess

I'm not sure what this is, but I noticed several failures in visit(const MemberAccess ..., in the following unsupported case:

  if (dynamic_cast<const TypeType *>(
          memberAccess.expression().annotation().type.get())) {
    solAssert(false, "not implemented yet");
    return false;
  }

Update scripts/install_deps.sh

We have added some dependencies for the Solidity-to-IELE backend, such as llvm-5.0.0 and libxml2-utils. We need to update the install_deps.sh script to reflect those.

Solidity feature: Enums

Solidity feature: Function Modifiers

Solidity feature: Internal Call

Solidity feature: 'returns'

See: http://solidity.readthedocs.io/en/v0.4.21/control-structures.html#output-parameters

Solidity feature: assert

Quite a few contracts failed on the "non implemented yet" assertion inside appendInvalid.
I wasn't quite sure about what that should do, but by looking at who calls appendInvalid, it seems this should handle assertions.

Solidity feature: Mappings

• mappings with integral keys with both finite and infinite keyspaces
• mappings with hashed keyspaces
• mappings with dynamically sized keyspaces (e.g. strings)
• delete for mappings
• copying of structs that have mapping members

Solidity feature: Omitted Function Parameter Names

http://solidity.readthedocs.io/en/latest/control-structures.html?highlight=anonymous#omitted-function-parameter-names

Solidity feature: tuple expression

Solidity feature: Non-scalar arguments in public functions

Solidity feature: Function pointers

Solidity feature: Account Call

• Value Types
• Reference types

Need CI to automatically summarize total tests passing and failing broken down by category.

We need to be able to automatically generate the number of passing and failing tests on each CI build.

Bugfixes (return statement + modifiers, inheritance etc.)

Tests failing because of the interaction of return with modifiers:

• function_modifier_local_variables
• function_modifier_multi_with_return
• function_modifier_multiple_times_local_vars
• return_does_not_skip_modifier

Tests failing because of inheritance and the way we pass args to base constructors:

• pass_dynamic_arguments_to_the_base
• pass_dynamic_arguments_to_the_base_base
• pass_dynamic_arguments_to_the_base_base_with_gap

Solidity feature: Boolean operators (`&&`, `||` etc.)

This appeared several times in the compilationTests\zeppelin folder

• &&
• ||
• ~

Solidity feature: Selfdestruct

Solidity feature: State Variable Initializers

this

Support the this keyword (evaluates to the address of the current contract)

Solidity feature: Strings

Seems we are still missing those...

• string literals
• string and bytes types

Solidity feature: Type Conversions (implicit and explicit)

• fixed bytes
• integers
• enums
• tuples
• functions
• structs and arrays
• addresses
• string literals
• bools

Solidity feature: low-level `log`

This is in addition to what already implemented for #82.
It should be very similar to event, but all arguments have to be provided manually e.g. the contract ID is not added automatically but has to be provided as part of the call.

Solidity feature: Conditionals

E.g. x ? y : z

Solidity feature: Compound Assignment

E.g. x += 1

Encoding function to combine multiple integers into a single bytestring

This will be needed in #25 to store the non-indexed arguments.
In the EVM compiler, this is done by calling utils().abiEncode.

Julia IR Support?

I want to start a discussion between @theo25 and @axic about supporting the Julia IR for the compiler to IELE.

Right now the compiler is being modified to be able to emit IELE code directly from Solidity, but perhaps it makes more sense to emit IELE from Julia, and then have a separate step for lowering Solidity -> Julia.

@theo25 if the code for Solidity -> IELE has not gotten too far past the Julia fragment, do you think it's possible to "finish" the Solidity -> IELE compiler by actually finishing out the Solidity -> Julia compiler?

@axic how much work is needed here for Solidity -> Julia?

Solidity feature: Named Arguments (in function calls)

E.g. f({value: 2, key: 3});

Solidity feature: Bounded Value Types

E.g. int64, bytes16 etc.

Solidity feature: Arrays

Solidity feature: Logging and Events

Scoping Activation

Seems we have a problem with variable scoping, as shown by test C99_scoping_activation (and possibly others, which will be added here as they are found),

For example, consider a call to the following function:

function g() pure public returns (uint x) {
  x = 7;
  {
      x = 3;
      uint x;
      return x; // This should return the new variable, i.e. 0
  }
}

Instead, we return 3. See C99_scoping_activation for more cases,

Need to run all C++ tests on every CI build of solidity

The Solidity repo has a bunch of tests already. We need to adapt the CI to run all of them and fail the build if we have any regressions, but not if tests that haven't been supported yet are failing. We've done this for the command line tests, but not for the tests written using Boost unit testing. We also need to integrate theses numbers into the summary of tests passing and failing (cf. #36)

Solidity feature: payable

functions and accessors without the payable modifier should throw an exception if they are passed funds.

Replacement for unimplemented features

We are not implementing several features of Solidity because they are EVM specific. Usually they are also insecure, as well, and in a few cases they have been deprecated. We need documentation that explains, for each feature, how a program with that feature should be implemented instead.

Solidity feature: Array push and length members

• array.length
• array.push

Solidity feature: Mathematical and Cryptographic Functions

See https://solidity.readthedocs.io/en/v0.4.21/units-and-global-variables.html#mathematical-and-cryptographic-functions

• addmod
• mulmod
• keccak256
• sha256
• sha3
• ripemd160
• ecrecover

Solidity feature: Structs

Solidity feature: accessors

		contract test {
			uint256 public data;
			function test() {
				data = 8;
			}
		}

Seems like a call to data() should return 8 (see simple_accessor in SolidityEndToEndTest,cpp)

Qualified imports and new

When you do a qualified import, it should rename the contract in the outputted iele code for all contracts in the file that contains the qualified import, in order to avoid name collision.

Allow compiler to use fresh variable names for parameters, local vars etc.

Cf modifier parameter with same name as function parameter.

Recursive Structs

Solidity supports recursive structs under certain circumstances. We need to compile these correctly.

Solidity feature: Post/Pre increment/decrement operations

e.g. ++x, y--

Solidity feature: Inheritance

Subfeatures:

• inherited members
• base constructors without arguments
• base constructor arguments
• super keyword
• direct access to base class members.

Need CI to generate coverage report

we need to set up gcov to run the coverage report for the solidity-to-iele compiler on each build of solidity.

Solidity feature: Overloading

Solidity feature: libraries

Bug: `bool_conversion`

This is due to the fact that we don't have type conversions (#13) yet.

Bug: `conditional_expression_tuples`

This fails because the tuples involved in the example are not handled correctly.
Since tuples seems to work fine in other examples, we may have a problem due to the interaction with the conditional expression.

Solidity feature: delete

See e.g. deleteLocals in SolidityEndToEndTest.cpp