solidity-frontend Directory Reference

Directory dependency graph for solidity-frontend:

Files
	pattern_check.cpp
	Implementation of pattern-based vulnerability detection.
	pattern_check.h
	Pattern-based vulnerability detection for Solidity contracts.
	solidity_convert.cpp
	Top-level conversion driver and static member initialization.
	solidity_convert.h
	Core AST-to-irep2 converter for the Solidity frontend.
	solidity_convert_builtin.cpp
	Built-in function and low-level call handling for the Solidity frontend.
	solidity_convert_call.cpp
	Function call conversion for the Solidity frontend.
	solidity_convert_constructor.cpp
	Constructor conversion for the Solidity frontend.
	solidity_convert_contract.cpp
	Contract-level conversion for the Solidity frontend.
	solidity_convert_decl.cpp
	Declaration conversion for the Solidity frontend.
	solidity_convert_expr.cpp
	Expression conversion for the Solidity frontend.
	solidity_convert_inheritance.cpp
	Contract inheritance handling for the Solidity frontend.
	solidity_convert_literals.cpp
	Literal conversion for the Solidity frontend.
	solidity_convert_mapping.cpp
	Mapping type conversion for the Solidity frontend.
	solidity_convert_modifier.cpp
	Function and modifier definition conversion for the Solidity frontend.
	solidity_convert_ref.cpp
	Reference and symbol resolution for the Solidity frontend.
	solidity_convert_stmt.cpp
	Statement conversion for the Solidity frontend.
	solidity_convert_tuple.cpp
	Tuple expression conversion for the Solidity frontend.
	solidity_convert_type.cpp
	Type conversion for the Solidity frontend.
	solidity_convert_util.cpp
	Utility and helper functions for the Solidity converter.
	solidity_grammar.cpp
	Implementation of Solidity grammar classification functions.
	solidity_grammar.h
	Solidity grammar enumerations and classification helpers.
	solidity_language.cpp
	Implementation of the Solidity language frontend.
	solidity_language.h
	Solidity language frontend interface for ESBMC.
	typecast.cpp
	Implementation of Solidity type casting utilities.
	typecast.h
	Type casting utilities for the Solidity frontend.

Detailed Description

ESBMC Solidity Front-end

Overview

The ESBMC Solidity frontend accepts smart contracts written in the Solidity language together with the Solidity AST (in compact JSON form). Based on these inputs, the frontend translates the contract into a C++-style intermediate representation and automatically generates a verification harness (a main function). The generated program is then verified by ESBMC's backend.

Usage

Quick start

Pass a .sol file directly to ESBMC — it will automatically find and invoke solc:

esbmc example.sol --k-induction

ESBMC searches for solc in this order: --solc-bin <path> > $SOLC environment variable > solc in $PATH. You can specify a particular solc binary:

esbmc --solc-bin /path/to/solc example.sol --k-induction

Manual AST generation (legacy)

You can also generate the AST yourself and pass both files:

solc --ast-compact-json example.sol > example.solast
esbmc --sol example.sol example.solast --k-induction

Note that different versions of solc may produce slightly different AST formats and also support different Solidity syntaxes. The frontend is currently developed and tested against Solidity 0.8.0.

• For contracts written in pre-0.5.0 Solidity, ESBMC will report unsupported version and terminate at the frontend stage without verification.
• For contracts in the range 0.5.0–0.7.0, ESBMC will issue a warning but continue verification. However, due to AST/semantic mismatches, unexpected errors or imprecise results may occur.

Bug detection

# use --multi-property if you want to report all found bugs at once
esbmc example.sol --k-induction --multi-property

As with ESBMC in general, ESBMC-Solidity supports common bug classes, including arithmetic overflow/underflow, division by zero, null-dereference, array-out-of-bounds, assertion violations, etc. Use ESBMC command-line options to enable or configure specific checks (e.g. overflow checks, pointer checks, etc.).

Additionally, ESBMC-Solidity provides the --reentry-check option to detect potential reentrancy behaviors. When enabled, the frontend inserts assertions and instrumentation to capture possible reentrant call traces.

Note that a reported reentrancy behavior is an indicator (possible reentrancy path) and does not necessarily imply a concrete exploit (for example, actual loss of funds). The report should be inspected together with the generated counterexample trace.

Verifying target constraints

By default ESBMC-Solidity analyses every contract present in the provided source program. To restrict verification to a specific contract, use:

--contract <ContractName>

To set multiple contracts:

--contract "ContractA ContractB"

To further restrict the analysis to a particular function, use:

--contract <ContractName> --function <functionName>

--function can be used without --contract, but this is not recommended because specifying --contract disambiguates overloaded / similarly-named functions across contracts. The constraints on contract and function targets help reduce overhead and improve performance.

Modes

The solidity frontend can construct different main harnesses depending on the selected mode. The harness determines how external calls, addresses and inter-contract interactions are modelled, which in turn affects verification purpose and outcomes.

Unbound reasoning (default)

Flag:

--unbound

Description: This is the default mode. External calls and addresses that are not otherwise constrained are modelled symbolically — the verifier makes no assumption about the code behind an external (symbolic) address, preserving soundness.

Bounded cross-contract reasoning

Flag:

--bound

Description: Enabling this mode switches the frontend into bounded cross-contract reasoning. In this mode, certain symbolic addresses can be bound to known contracts (or to a finite set of contracts). This enables the verifier to model inter-contract calls as concrete jumps to the bound implementations and to generate precise traces that reflect real cross-contract interactions (e.g., attacker contracts interacting with a vulnerable contract or reentrancy scenarios).

This mode is particularly useful for analysing the behaviour of a multi-contract system. Use --contract to specify the target contract(s), and --function to set the entry point.

Examples

• Detecting overflow/underflow:

esbmc MyContract.sol --overflow-check --unsigned-overflow-check

• Running k-induction with solidity frontend:

esbmc example.sol --k-induction --multi-property

• Bounded analysis :

esbmc example.sol --bound --contract Vulnerable --function withdraw

Notes

• During parsing and translation the solidity frontend may introduce additional statements, auxiliary variables and assertion instrumentation. This can affect coverage metrics (e.g. --branch-coverage) and the exact locations/format of counterexamples. Use --goto-functions-only to inspect the actual intermediate representation the frontend generates.
• The Solidity frontend is still under active development. When encountering unsupported syntax, ESBMC will terminate (and may sometimes crash) during the parsing stage, without proceeding to verification.
• ESBMC's performance is currently affected by the integer bitwidth, especially when mapping is involved. For example, mapping(uint256 => string) requires more unwinding steps to solve compared to mapping(uint8 => string). You can try the experimental option --16 to set the machine word size to 16 bits and improve performance.
• Since the minimal supported machine word size is 16, overflow/underflow checks for uint8 and int8 are not currently supported.

Cryptographic hash function abstraction

ESBMC models keccak256, sha256, ripemd160, ecrecover, blockhash, and blobhash as nondeterministic (nondet) functions: each call returns a fully unconstrained symbolic value. The real hash algorithm is not computed.

This is an over-approximation — the verifier considers every possible return value, including the real one. Consequences:

• No false negatives (sound for safety): if the verifier reports VERIFICATION SUCCESSFUL, the property truly holds under all possible hash outputs.
• Possible false positives (spurious counterexamples): the verifier may report VERIFICATION FAILED for properties that are actually safe, because it explores hash outputs that cannot occur in reality.
• No functional consistency: two calls to keccak256(x) with identical x may return different nondet values. Properties that rely on "same input → same output" (e.g., commit-reveal patterns, hash-based equality checks) cannot be verified and will produce false alarms.

The operational models are in src/c2goto/library/solidity/solidity_builtins.c.

For Developers

• The Solidity Frontend converts Solidity statements into CPP-style IR – each contract is considered as a class. Yet no other C++ specific syntax are used, meaning all statements are converted to C-style IR. Data structures like mapping, Bytes are written as C-struct internally. Operational models are pre-compiled via the c2goto pipeline (see src/c2goto/library/solidity/).
• The blockchain state is encoded as properties within each contract, such as address, codehash, balance, etc. Note that while in reality a balance is bound to an address, in our modelling it is bound to each contract instance.
• For multi-contract programs, the JSON of each contract is parsed separately. Inheritance is mainly handled by merging the corresponding AST JSON files.