SOLTIX: Scalable testing of Solidity compilers
We are happy to release SOLTIX, a scalable framework for automated testing of Solidity compilers.
What is SOLTIX?
SOLTIX is a framework for automated testing of Solidity compilers. It started as the master thesis project of Nils Weller, supervised by researchers from the ICE center, and then evolved into a larger project that is now officially funded by the Ethereum Foundation.
How does it work?
SOLTIX tests the Solidity compiler and, in turn, the Ethereum Virtual Machine (EVM) in a fully automated way. There are two ways to test the compiler:
1. Testing via synthesis of random Solidity contracts
In this mode, to test the compiler SOLTIX automatically generates random Solidity contracts. It then interprets the generated contracts to anticipate the expected values that will appear at runtime and injects statements that would throw an error if the execution is incorrect. In the example of Fig. 1, SOLTIX checks whether the value assigned to variable x equals 5, and emits an error if this is not the case (to indicate an error in the compiler).
2. Testing via synthesis of semantically-equivalent Solidity contracts
In this mode, SOLTIX is provided with a Solidity contract and a sequence of transactions. SOLTIX runs the transactions on the contract and collects runtime information (such as which values may appear at runtime). Based on the collected runtime information, SOLTIX injects statements that must da preserve the semantics of the contract for the provided sequence of transactions. Finally, to check if the contracts are indeed equivalent for these transactions, SOLTIX runs the transactions on the contracts and checks whether all contracts reach an identical final state, as any deviation indicates an error in the compiler.
How effective is SOLTIX?
SOLTIX has already discovered two important bugs in the Solidity compiler:
- Exponentiation bug: This bug results in incorrect computations of exponents. The bug was fixed in version 0.4.25.
- 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.
Further, it has discovered two bugs in ganache-cli; e.g., see shift and exponentiation crashes.
Where to find more information?
Check out the full technical article by Nils to learn more about SOLTIX.
How can I contribute?
The project now is an open platform welcoming contributors from the Ethereum community. To learn more about the project, you can check out the code on GitHub and join our Discord channel:
