Syrup is a tool that applies super-optimization techniques to
optimize Ethereum's smart contracts. In order to do so, Syrup splits
smart contracts into basic block, and for each of them, tries to find
a sequence of EVM instructions that leads to the same stack as the
original block but spends less gas.
Syrup uses an intermediate representation (Stack Functional
Specification or SFS) on the impact a sequence of instructions has on
a block, and from this representation, a Max-SMT encoding is derived
to find the best translation. The SFS defines the state of the stack
after executing the basic block in terms of the state of the initial stack.
This version of the syrup tool is implemented entirely in Python3
and considers further configurations in the Max-SMT encoding to
determine the best options for its usage, as well as more
simplification rules.
The folder ethir/source contains static executables of different versions of Solidity compiler. Add it to the PATH and test that it is installed.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
solcv7 --version
solcv8 --version
In case you want to install the latest version:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
Static executables of the Ethereum Virtual Machine are provided in the folder ethir/source. Add it to the PATh and test that it is installed.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
In case you want to install the latest version:
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
3. Install Z3
Use pip install command to install Z3
pip3 install z3
pip3 install z3-solver
Use pip install command to install six and requests python
libraries.
pip install six
pip install requests
Download an static executable of the SMT solvers used from the following links:
- Z3: https://github.com/Z3Prover/z3/releases/tag/z3-4.8.12
- Barcelogic: Send an email to [email protected]. Subject: "Static Executable Syrup".
- OptiMathSAT: http://optimathsat.disi.unitn.it/pages/download-js.html
When they are downloaded, create a directory called bin in the root directory of the repository and move them to this folder.
Syrup 2.0 can take either a Solidity smart contract, EVM bytecode,
an isolated basic block or the SFS of a basic block as input. Examples
are available in the following links:
- Solidity smart contracts: https://github.com/costa-group/syrup-python/tree/master/examples/tosem-benchmarks-a
- EVM bytecode: https://github.com/costa-group/syrup-python/tree/master/examples/tosem-benchmarks-b
- Basic block: https://github.com/costa-group/syrup-python/tree/master/examples/basic-blocks
- SFS: https://github.com/costa-group/syrup-python/tree/master/examples/blocks
Syrup 2.0 stores all the output from its execution in the folder
/tmp/syrup/solutions. For each analyzed contract, it creates three
folders in this directory containing all the relevant information for
each optimized sub-block:
-
evm: generated bytecode of the solution.
-
disasm: opcodes from the solution, in format human-readable.
-
total_gas: gas associated to each generated block.
Syrup 2.0 aims to determine the most suitable configuration in order
to make the framework feasible to include in real-world
compilers. As such, there exists several flags that allow the user to
specify different combinations of constraints and timeouts. These
configurations have been studied in detail and a
visualizer has been
implemented to interpret the experiments. The encoding names used in
the visualizer are depicted below.
By default, the encoding that has been determined to work the best so
far is enabled. It can be disabled using -disable-default-encoding
flag. When disabled, the same encoding as Syrup 1.0 is produced by
default: O'SFS + CL. The following flags
activate different constraints to be included:
- -inequality-gas-model : change soft constraint encoding from O'SFS to OSFS
- -pushed-once : enable hard constraint Numerical values pushed at least once or CN
- -no-output-before-pop : enable hard constraint Restricted opcodes before POP or CR
- -at-most : enable hard constraint Uninterpreted opcodes at most once or CU
Other flags can be enabled to add other hard constraints or modify the soft constraints. However, they have not been fully checked and it is not guaranteed the produced blocks are indeed equivalent to the initial ones.
The timeout per block can be specified using -tout flag. It is set to 10 seconds by default. When the timeout is reached, the underlying SMT solver halts its execution and returns the best model so far. If no model was found, empty files are produced.
Execute the following command to analyze a provided smart contract:
syrup_full_execution.py -s SOURCE -storage [-b] [-isb] [-json] [-solver
{z3,barcelogic,oms}] [-v]
[-at-most] [-pushed-once] [-tout
timeout] [-inequality-gas-model]
[-instruction-order]
[-no-output-before-pop]
[-initial-solution]
[-disable-default-encoding]
[-number-instruction-gas-model]
where the:
- SOURCE represents the source file where the Solidity smart contract, EVM bytecode, SFS or basic block is stored
- -b is needed when analyzing EVM bytecode
- -isb is needed when analyzing a basic block
- -json is needed when analyzing a SFS
- -solver allows selecting the desired SMT solver
- -v activates the lightweight verifier included in
Syrup 2.0 - -tout allows specifying a desired timeout for the optimization process of each of the basic blocks of the smart contract under analysis. It is set to 10s by default
For instances, to analyze the smart contract 0x001385C23468Cb4614831aD9205F041Cf64A2958.sol using OptiMathSAT as SMT solver, the initial configuration with CN and a timeout of 5 seconds, you have to execute the following command:
./syrup_full_execution.py -s examples/tosem-benchmarks-a/0x001385C23468Cb4614831aD9205F041Cf64A2958.sol -storage -solver oms -disable-default-encoding -pushed-once -tout 5
The directory examples contains the benchmarks used in the experimental section (Section 5) of the paper (directories tosem-benchmarks-a and tosem-benchmarks-b respectively) submitted to TOSEM. The smart contracts located in tosem-benchmarks-a are those selected for experiments (i) and (ii) and the ones located in tosem-benchmarks-b the contracts used for experiments (iii).
In order to reproduce the results, you can find the scripts used in the directory scripts:
-
Script process_benchmarks_a.sh (process_benchmarks_b.sh respectively) generates the SFS for all the blocks of the smart contracts located in the directory tosem-benchmarks-a (tosem-benchmarks b respectively). These scripts generate two new directories in the root directory of the repository: results-a for the smart contracts analyzed in the set tosem-benchmarks-a and results-b for those in tosem-benchmarks-b. There, you can find a new directory sfs-a (sfs-b respectively) with the SFSs generated for each of the basic blocks.
-
Before running the experiments, we need to clean those repositories, i.e just leave the json files representing the SFSs for each file. In order to do so, run script remove_jsons_intermediate_dir_benchmark_a.py (remove_jsons_intermediate_dir_benchmark_a.py respectively).
-
Once, the SFSs are generated you have to execute the script analyze_all_blocks_in_contract_benchmark_a.py (respectively analyze_all_blocks_in_contract_benchmark_b.py) to reproduce the experiments in Section 5.2 and 5.3 (Section 5.4 respectively). This scripts accepts several mandatory flags in order to allow multiple configurations to study:
- -solver {z3,barcelogic,oms}
- -tout timeout : Timeout in seconds
- -csv-folder csv_folder : Folder in which the results from the experiments are stored. Inside this folder, the subfolder solver + "_" + timeout + "s/" is created. This subfolder contains a csv file for each analyzed file, containing a row for each sub-block analyzed
- -inequality-gas-model, -pushed-once, -no-output-before-pop, -at-most, -disable-default-encoding : flags used to modify the Max-SMT encoding configuration
Note that multiple executions of this script can lead to inconsistencies, as all intermediate files are stored in the same folder. This can lead to name clashing and thus, incoherent results. In order to avoid this behavior, rename the variable syrup_folder in the file params/paths.py to another name before running again the script.
For instance, if we want to study the initial configuration with CU encoding when applied to Z3 and with a timeout of 15 seconds, run the following command:
./analyze_all_blocks_in_contract_benchmark_a.py -solver z3 -tout 15 -disable-default-encoding -at-most -csv-folder ../results-a/block_results/at_most/
As a result, the folder /results-a/block_results/at_most/z3_15s is created.
Note that the execution of the script can take several hours depending on the timeout set and the configuration studied.
- Finally, to obtain the global results per configuration instead of having a csv file per file, execute the script generate_info_per_contract_with_verifier_time.py. This file accepts the path to the general folder that stores all the experiments and generates a csv file for each encoding.
For instance, in previous example, the general folder in which we will store the experiments is ../results-a/block_results/. Thus, we need to run the following command:
./generate_info_per_contract_with_verifier_time.py -block-results-folder ../results-a/block_results/ -combined-csvs-folder ../results-a/combined_results/