argotorg / argotorg/solidity

Selective function inlining and optimisation

Open
#14,789 3 comments 0 reactions 0 assignees View on GitHub
feature must have eventually optimizer
Dominant language
C++
Stars
25.7k
Forks
6.2k
Avg merge
2d 19h
Merged PRs (30d)
29

Description

## Abstract

At Runtime Verification (RV), we are developing tooling based on symbolic execution that allows us to verify properties of Solidity programs by analysing the corresponding compiled EVM bytecode. An important aspect of our analysis is reasoning about symbolic dynamically-sized data structures in memory, such as byte arrays and arrays of byte arrays. These data structures often get copied to memory in chunks of 32 bytes with the help of auto-generated auxiliary functions, such as the ones generated by the [`copyToMemoryFunction`](https://github.com/ethereum/solidity/blob/ec563a12cb9247d985df1e52cfacd9d03520fa2c/libsolidity/codegen/YulUtilFunctions.cpp#L83) function of the codebase. We reason about these function by writing, proving, and then reusing summaries of their behaviour. This is a standard approach that allows us to jump over the 32-byte-copying loops. These summaries would ideally be written once-and-for-all, and could be made reusable by any symbolic analysis of EVM bytecode.

The issue that we are faced with is that the EVM bytecode corresponding to these functions is often inlined and heavily optimised in ways that rely on the structure of the rest of the program, which we are not able to predict. We are therefore unable to provide a universal summary per function, but have to recreate the summaries every time the compiler chooses to do a different optimisation. This makes the verification effort brittle, severely negatively impacting the resilience and maintainability of the obtained proofs.

Importantly, this issue is not limited to our verification efforts alone, and is very likely to appear in any symbolic analysis of EVM bytecode that attempts to reason about symbolic dynamically-sized data structures.

## Motivation

The above-described issue could be addressed by extending the Solidity compiler with a mechanism that would allow the user to choose the functions that are not to be inlined and/or optimised during the compilation process. This would ensure the stability of the associated bytecode.

This solution came up as a result of a recent discussion between RV and @ekpyron.

Nota bene: this feature request could be rendered obsolete when #14741 is implemented, if `MCOPY` was to be used instead of the 32-byte-copying loops.

## Specification

I am not sufficiently familiar with the codebase to give a precise specification. At the UI level, I presume it would involve a flag to the compiler (for example, `--dont-inline` or `--dont-optimise`) followed by a list of function identifiers to not be inlined/optimised.

## Backwards Compatibility

As this feature would be optional, there should be no issues with backwards compatibility.

Contributor guide

Open the contributing guide

Research direction

Start with libsolidity/codegen/YulUtilFunctions.cpp and its copyToMemoryFunction entry point, then trace how compiler inlining and optimisation options are exposed. The issue still needs a precise function-selection interface, affected compiler stages, and tests defining stable output for selected functions before implementation can be scoped.

Written by the indexing model from the issue text.

Assessment

Tech stack
cpp, solidity
Domain
compilers
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
25/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.