gigahorse-toolchain

The memory modeling component is organized into several specialized files. Understanding this layout helps in locating specific logic for customization or debugging:

• memory_modeling.dl: Main entry point for client analyses.
• memory_modeling_api.dl: Defines the public API.
• clienthelpers.dl: Common relations for client reuse.
• memory_addresses.dl: Models free-memory-pointer values and address aliasing.
• core.dl: Core logic mapping memory reads to writes (outputs MemWriteToMemConsStmtResolved).
• uses_defs_abstractions.dl: High-level use/def abstractions based on core.dl.
• arrays.dl: Rules for high-level memory arrays.
• loops.dl: Modeling of memory copying loops.
• components.dl: Common components (e.g., ReachableByPassing).
• helpers.dl: Syntactic patterns and shared relations.
• misc.dl: Low-level relations.
• metrics.dl: Evaluation metrics for memory modeling.

The StorageConstruct type is an Algebraic Data Type (ADT) used to model arbitrarily nested Ethereum storage structures. It allows you to represent everything from simple constants to complex, nested mappings and arrays.

Constructors:

• Constant {value: Value}: A fixed value.
• StaticArray {parConstruct: StorageConstruct, arraySize: number}: A fixed-size array.
• Array {parConstruct: StorageConstruct}: A dynamic array.
• Mapping {parConstruct: StorageConstruct}: A mapping structure.
• Offset {parConstruct: StorageConstruct, offset: number}: A construct with a specific byte offset.
• Variable {construct: StorageConstruct}: A wrapper for a storage variable.
• TightlyPackedVariable {construct: StorageConstruct, byteLow: number, byteHigh: number}: A variable that occupies a specific byte range within a slot.

Example Mapping: If you have a nested mapping mapping (address => mapping(uint256 => vals)) public complex at slot 0x4, the constructs would look like:

• The base mapping: Variable(Mapping(Constant(0x4)))
• An offset within that mapping: Variable(Offset(Mapping(Mapping(Constant(0x4))), 1))

// Example Solidity structure
contract StorageExample {
  uint256 public supply;  // slot 0x0
  address public owner;   // slot 0x1
  bool public isPaused;   // slot 0x1
  uint256[] public supplies; // slot 0x2
  mapping (address => bool) public admins; // slot 0x3
  struct vals {uint256 field0; uint256 field1;}
  mapping (address => mapping(uint256 => vals)) public complex; // slot 0x4
}

// Corresponding Gigahorse constructs
// Variable(Constant(0x0)) // uint256 supply
// Variable(Constant(0x1)) // address owner, bool isPaused
// Variable(Array(Constant(0x2))) // uint256 [] supplies
// Variable(Mapping(Constant(0x3))) // mapping admins
// Variable(Mapping(Mapping(Constant(0x4)))) // complex mapping base
// Variable(Offset(Mapping(Mapping(Constant(0x4))), 1)) // field in complex mapping

For development purposes (e.g., visualizing the CFG of the lifted IR), you can manually run the three stages of the pipeline: Fact generation, Souffle execution, and Visualization.

Prerequisites: You must set LD_LIBRARY_PATH and LIBRARY_PATH to the directory containing libfunctors.so (typically within the souffle-addon directory).

Pipeline Steps:

1. Fact Generation: Translates EVM bytecode into relational format.
2. Souffle Execution: Runs the main decompilation step (the Datalog program).
3. Visualization: Processes the relational output.

It is suggested to add these paths to your .bashrc file.

# Setup environment
cd souffle-addon
export LD_LIBRARY_PATH=`pwd` 
export LIBRARY_PATH=`pwd` 

# 1. Fact generation
./generatefacts <contract> facts

# 2. Run main.dl using Souffle
souffle -F facts logic/main.dl

# 3. Visualize results
clients/visualizeout.py

The gigahorse.py script performs binary lifting from EVM code to a high-level three-address representation. It can process individual .hex files or entire directories of contracts.

Basic Usage

Run on a single contract:

./gigahorse.py examples/long_running.hex

Run on a directory of contracts (bulk analysis):

./gigahorse.py <directory_of_hex_files>

Pipeline Behavior

1. Decompilation: Attempts a shrinking context-sensitivity configuration first. If it times out, it falls back to a scalable-fallback (finite-precise) configuration.
2. Inlining: Performs rounds of inlining small functions to assist client libraries.

Configuration Flags

• --disable_scalable_fallback: Disables the second attempt with the scalable-fallback configuration.
• --disable_inline: Disables the function inlining functionality.
• -j <number of jobs>: Specifies the number of parallel jobs.
• -C <client_path>: Specifies a client analysis to run after lifting. Clients can be a comma-separated list of path-reachable or fully-qualified filenames.

Output

• Decompilation results: Stored in the .temp directory.
• Execution metadata: Stored in results.json. This file contains a list of triples [filename, properties, flags].
  • properties: A list of detected issues (non-empty output relations in datalog files).
  • flags: Auxiliary info like "ERROR" or "TIMEOUT".

To install Gigahorse from a local clone, you must first ensure the repository is cloned with submodules.

1. Clone the repository

git clone git@github.com:nevillegrech/gigahorse-toolchain.git --recursive

If you already cloned without --recursive, run git submodule update --init --recursive to fetch the souffle-addon submodule.

2. Install System Dependencies (Debian-based)

You need the following installed on your system:

• Boost libraries: apt install libboost-all-dev
• Z3: apt install libz3-dev
• Souffle: Version 2.3 or 2.4.1 (recommended to use the 2.4.1 release).
• uv: The Astral Python project manager. Install via curl -LsSf https://astral.sh/uv/install.sh | sh.

3. Build Souffle Addon

Navigate to the souffle-addon directory and build the custom functors:

cd souffle-addon && make WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13)

4. Set up Python Environment

Use uv to provision CPython 3.13 and project dependencies into a local .venv:

uv sync

Optional Extras:

• For Datalog directive parsing and interactive graph visualization: uv sync --extra tooling
• For Graphviz/dot rendering: uv sync --extra viz

Gigahorse uses a tiered system to generate facts (intermediate representations) from Ethereum smart contracts. The process is managed by a MixedFactGenerator which selects the appropriate strategy based on the input filename pattern.

There are three main types of generators:

1. DecompilerFactGenerator: The primary method. It uses a multi-stage fallback mechanism to handle complex contracts. It starts with a precise decompiler and, if it fails or times out, falls back to ScalableDecomp and finally LastResortDecomp by reducing the MaxContextDepth.csv value.
2. ContractStitchingGenerator: Used for multi-contract manifests. It takes a JSON manifest containing multiple contract addresses and IDs, extracts their individual facts, prefixes identifiers to prevent collisions, and merges them into a single set of relations.
3. CustomFactGenerator: Allows running user-defined scripts or Datalog files. It supports both .dl files (run via Souffle) and other scripts (run as subprocesses with -i input and -o output flags).

Generators are assigned a priority (FACT_GEN_HIGH_PRIORITY or FACT_GEN_LOW_PRIORITY) to determine the order of execution.

Gigahorse supports several context sensitivity algorithms to control the precision and depth of the decompilation. You can select an algorithm using the -M flag with the CONTEXT_SENSITIVITY key.

Available Algorithms:

• TransactionalWithShrinkingContext: The default. A composite algorithm that includes a public entry point component and a variable depth selective context component that can shrink to drop elements that no longer provide precision.
• TransactionalContext: The algorithm from the Elipmoc paper. A composite algorithm with a public entry point and variable depth selective context.
• CallSiteContext: Call-site (or block-site) context sensitivity with variable depth.
• CallSiteContextPlus: Call-site context sensitivity including a public function component.
• SelectiveContext: Selective call-site context including only dynamic jumps.
• SelectiveContextPlus: Selective context including a public function component.

You can also control the maximum context depth using the -cd flag.

Note: Changing the algorithm via the default 2-step pipeline is not recommended as it may override defaults for both configurations.

python3.8 gigahorse.py examples/long_running.hex --disable_scalable_fallback -M "CONTEXT_SENSITIVITY=CallSiteContext"