### Install Gigahorse via Docker

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Use the provided installation scripts to set up Gigahorse on amd64 or arm64 architectures.

```bash
curl -s -L https://raw.githubusercontent.com/nevillegrech/gigahorse-toolchain/master/scripts/docker/install/install_amd64 | bash
```

```bash
curl -s -L https://raw.githubusercontent.com/nevillegrech/gigahorse-toolchain/master/scripts/docker/install/install_arm64 | bash
```

--------------------------------

### Verify Gigahorse Installation

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Refresh the shell environment and verify the installation by checking the help output.

```bash
source ~/.bashrc
gigahorse --help
```

--------------------------------

### Install Souffle Addon Functors

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Build the custom functors required for the Souffle analysis engine.

```bash
# builds all, sets libfunctors.so as a link to libsoufflenum.so
cd souffle-addon && make WORD_SIZE=$(souffle --version | sed -n 3p | cut -c12,13)
```

--------------------------------

### Model Smart Contract Storage

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Example demonstrating how Solidity contract declarations map to Gigahorse storage construct inferences.

```solidity
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
}
```

```solidity
Variable(Constant(0x0)) // uint256 supply
Variable(Constant(0x1)) // address owner , bool isPaused
Variable(Array(Constant(0x2))) // uint256 [] supplies
Variable(Mapping(Constant(0x3))) // mapping admins
// the 2 fields of struct value of nested mapping complex :
Variable(Mapping(Mapping(Constant(0x4))))
Variable(Offset(Mapping(Mapping(Constant(0x4))), 1))
```

--------------------------------

### Visualize IR block structure

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Example of the textual representation generated in contract.tac files.

```text
    Begin block 0x3e
    prev=[0xb], succ=[0x10ee, 0x49]
    =================================
    0x3f: v3f(0xf42fdfb) = CONST 
    0x44: v44 = EQ v3f(0xf42fdfb), v32
    0x10c7: v10c7(0x10ee) = CONST 
    0x10c8: JUMPI v10c7(0x10ee), v44
```

--------------------------------

### Run Decompilation with Call-Site Context Sensitivity

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/Advanced.md

Use the -M flag to specify a context sensitivity algorithm for decompilation. This example demonstrates running a contract with call-site context sensitivity.

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

--------------------------------

### Get All Storage Variable Accesses

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Retrieve all accesses to storage variables, including the statement, storage construct, and loaded variable. This rule uses the StorageLoad predicate.

```Datalog
#include "clientlib/storage_modeling/storage_modeling.dl"

// Get all storage variable accesses
.decl StorageVariableAccess(stmt: Statement, construct: StorageConstruct, loadedVar: Variable)
.output StorageVariableAccess

StorageVariableAccess(stmt, cons, var) :-
  StorageLoad(stmt, cons, var).
```

--------------------------------

### Get Return Values from External Calls

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Retrieve the return values from external calls. This rule relies on the ExternalCall_ActualReturn predicate.

```Datalog
// Get return values from external calls
.decl CallReturns(call: Statement, returnVar: Variable, index: number)
.output CallReturns

CallReturns(call, returnVar, index) :-
  ExternalCall_ActualReturn(call, returnVar, index).
```

--------------------------------

### Get Actual Arguments of External Calls

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Extract the actual arguments passed to external calls. This rule uses MemoryStatement_ActualArg and CALLStatement predicates.

```Datalog
#include "clientlib/memory_modeling/memory_modeling.dl"

// Get actual arguments of external calls
.decl CallArguments(call: Statement, arg: Variable, index: number)
.output CallArguments

CallArguments(call, arg, index) :-
  MemoryStatement_ActualArg(call, arg, index),
  CALLStatement(call, _).
```

--------------------------------

### Get Struct Field Information

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Extract information about struct field accesses, including the statement, struct ID, and field offset. This rule analyzes storage statements involving struct variables.

```Datalog
// Get struct field information
.decl StructFieldAccess(stmt: Statement, structID: symbol, fieldOffset: number)
.output StructFieldAccess

StructFieldAccess(stmt, structID, offset) :-
  StorageStmtKindAndConstruct(stmt, _, $Storage(), $Variable($Offset(inner, offset))),
  DataStructureValueIsStruct($Storage(), inner, structID, _).
```

--------------------------------

### Initialize and Draw Graph with Vis.js

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/tooling/gigahorse.html

Initializes global variables and draws a network graph using the Vis.js library. Requires a container element with the ID 'mynetwork'.

```javascript
var edges; var nodes; var network; var container; var options, data; function drawGraph() { var container = document.getElementById('mynetwork'); nodes = new vis.DataSet([{"font": {"color": "white"}, "id": "Fail", "label": "Fail", "shape": "dot"}, {"font": {"color": "white"}, "id": "Fail.csv", "label": "Fail.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "ByteCodeHex", "label": "ByteCodeHex", "shape": "dot"}, {"font": {"color": "white"}, "id": "bytecode.hex", "label": "bytecode.hex", "shape": "dot"}, {"font": {"color": "white"}, "id": "OpcodePossiblyHalts", "label": "OpcodePossiblyHalts", "shape": "dot"}, {"font": {"color": "white"}, "id": "OpcodePossiblyHalts.csv", "label": "OpcodePossiblyHalts.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "Statement_Opcode", "label": "Statement_Opcode", "shape": "dot"}, {"font": {"color": "white"}, "id": "TAC_Op.csv", "label": "TAC_Op.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "IsStatement", "label": "IsStatement", "shape": "dot"}, {"font": {"color": "white"}, "id": "TAC_Stmt.csv", "label": "TAC_Stmt.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "Statement_Block", "label": "Statement_Block", "shape": "dot"}, {"font": {"color": "white"}, "id": "TAC_Block.csv", "label": "TAC_Block.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "Variable_Value", "label": "Variable_Value", "shape": "dot"}, {"font": {"color": "white"}, "id": "TAC_Variable_Value.csv", "label": "TAC_Variable_Value.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "BasicVariable_Value", "label": "BasicVariable_Value", "shape": "dot"}, {"font": {"color": "white"}, "id": "Variable_BlockValue", "label": "Variable_BlockValue", "shape": "dot"}, {"font": {"color": "white"}, "id": "TAC_Variable_BlockValue.csv", "label": "TAC_Variable_BlockValue.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "LocalBlockEdge", "label": "LocalBlockEdge", "shape": "dot"}, {"font": {"color": "white"}, "id": "LocalBlockEdge.csv", "label": "LocalBlockEdge.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "FallthroughEdge", "label": "FallthroughEdge", "shape": "dot"}, {"font": {"color": "white"}, "id": "IRFallthroughEdge.csv", "label": "IRFallthroughEdge.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "CallGraphEdge", "label": "CallGraphEdge", "shape": "dot"}, {"font": {"color": "white"}, "id": "IRFunctionCall.csv", "label": "IRFunctionCall.csv", "shape": "dot"}, {"font": {"color": "white"}, "id": "FunctionCallReturn", "label": "FunctionCallReturn", "shape": "dot"}, {"font": {"color": "white"}, "id": "IRFunctionCallReturn.csv", "label": "IRFunctionCallReturn.csv", "shape": "dot"}, {"font": {"colo"}}
```

--------------------------------

### Configure Context Sensitivity

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Select specific algorithms to balance decompilation precision and scalability.

```bash
# Use CallSite context sensitivity (block-site based)
python3 gigahorse.py examples/long_running.hex \
    --disable_scalable_fallback \
    -M "CONTEXT_SENSITIVITY=CallSiteContext"

# Use Transactional context (from Elipmoc paper)
python3 gigahorse.py examples/long_running.hex \
    --disable_scalable_fallback \
    -M "CONTEXT_SENSITIVITY=TransactionalContext"
```

--------------------------------

### Execute Manual Pipeline

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Perform step-by-step decompilation for custom workflows or development debugging.

```bash
# Step 1: Set up library paths
cd souffle-addon
export LD_LIBRARY_PATH=$(pwd)
export LIBRARY_PATH=$(pwd)
cd ..

# Step 2: Generate facts from bytecode
./generatefacts examples/long_running.hex facts/

# Step 3: Run the Souffle decompiler
souffle -F facts logic/main.dl -D out/

# Step 4: Visualize the output
cd out && python3 ../clients/visualizeout.py
cat contract.tac
```

--------------------------------

### Run Gigahorse with client analysis

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Executes the lifter with one or more specified client analysis scripts.

```bash
./gigahorse.py  -j <number of jobs> -C clients/visualizeout.py <contracts>
```

--------------------------------

### Initialize and Draw Graph with vis.js

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/tooling/gigahorse.html

This snippet initializes a vis.js network graph with specified data, options, and event handlers for stabilization progress. It requires a container element for the graph and a loading bar element.

```javascript
function drawGraph() {
var container = document.getElementById('mynetwork');
var nodes = [
  {"arrows": "to", "from": "discovery0.ContinuationEntry.csv", "to": "discovery0.ContinuationEntry"},
  {"arrows": "to", "from": "discovery1.ContinuationEntry.csv", "to": "discovery1.ContinuationEntry"},
  {"arrows": "to", "from": "discovery2.ContinuationEntry.csv", "to": "discovery2.ContinuationEntry"},
  {"arrows": "to", "from": "discovery3.ContinuationEntry.csv", "to": "discovery3.ContinuationEntry"},
  {"arrows": "to", "from": "discovery0.InContinuation.csv", "to": "discovery0.InContinuation"},
  {"arrows": "to", "from": "discovery1.InContinuation.csv", "to": "discovery1.InContinuation"},
  {"arrows": "to", "from": "discovery2.InContinuation.csv", "to": "discovery2.InContinuation"},
  {"arrows": "to", "from": "discovery3.InContinuation.csv", "to": "discovery3.InContinuation"},
  {"arrows": "to", "from": "CommonReturnAddress.csv", "to": "CommonReturnAddress"},
  {"arrows": "to", "from": "IsCallReturn.csv", "to": "IsCallReturn"},
  {"arrows": "to", "from": "IsCallCall.csv", "to": "IsCallCall"},
  {"arrows": "to", "from": "MaxContextDepth.csv", "to": "InputMaxContextDepth"},
  {"arrows": "to", "from": "DropLast.csv", "to": "DropLast"},
  {"arrows": "to", "from": "MaxContextDepth.csv", "to": "InputMaxContextDepth"},
  {"arrows": "to", "from": "DropLast.csv", "to": "DropLast"},
  {"arrows": "to", "from": "A.facts", "to": "A"},
  {"arrows": "to", "from": "B.facts", "to": "B"},
  {"arrows": "to", "from": "O.csv", "to": "O"},
  {"arrows": "to", "from": "Hash.csv", "to": "Hash"}
];
var edges = [
  {"arrows": "to", "from": "discovery0.ContinuationEntry", "to": "discovery0.ContinuationEntry.csv"}, 
  {"arrows": "to", "from": "discovery1.ContinuationEntry", "to": "discovery1.ContinuationEntry.csv"}, 
  {"arrows": "to", "from": "discovery2.ContinuationEntry", "to": "discovery2.ContinuationEntry.csv"}, 
  {"arrows": "to", "from": "discovery3.ContinuationEntry", "to": "discovery3.ContinuationEntry.csv"}, 
  {"arrows": "to", "from": "discovery0.InContinuation", "to": "discovery0.InContinuation.csv"}, 
  {"arrows": "to", "from": "discovery1.InContinuation", "to": "discovery1.InContinuation.csv"}, 
  {"arrows": "to", "from": "discovery2.InContinuation", "to": "discovery2.InContinuation.csv"}, 
  {"arrows": "to", "from": "discovery3.InContinuation", "to": "discovery3.InContinuation.csv"}, 
  {"arrows": "to", "from": "CommonReturnAddress", "to": "CommonReturnAddress.csv"}, 
  {"arrows": "to", "from": "IsCallReturn", "to": "IsCallReturn.csv"}, 
  {"arrows": "to", "from": "IsCallCall", "to": "IsCallCall.csv"}, 
  {"arrows": "to", "from": "MaxContextDepth.csv", "to": "InputMaxContextDepth"}, 
  {"arrows": "to", "from": "DropLast", "to": "DropLast.csv"}, 
  {"arrows": "to", "from": "MaxContextDepth.csv", "to": "InputMaxContextDepth"}, 
  {"arrows": "to", "from": "DropLast", "to": "DropLast.csv"}, 
  {"arrows": "to", "from": "A.facts", "to": "A"}, 
  {"arrows": "to", "from": "B.facts", "to": "B"}, 
  {"arrows": "to", "from": "O", "to": "O.csv"}, 
  {"arrows": "to", "from": "Hash", "to": "Hash.csv"}
];
var data = {nodes: nodes, edges: edges};
var options = { "configure": { "enabled": true, "filter": [ "physics" ] }, "edges": { "color": { "inherit": true }, "smooth": { "enabled": false, "type": "continuous" } }, "interaction": { "dragNodes": true, "hideEdgesOnDrag": false, "hideNodesOnDrag": false }, "physics": { "enabled": true, "stabilization": { "enabled": true, "fit": true, "iterations": 1000, "onlyDynamicEdges": false, "updateInterval": 50 } } };
// if this network requires displaying the configure window, // put it in its div
options.configure["container"] = document.getElementById("config");
network = new vis.Network(container, data, options);
network.on("stabilizationProgress", function(params) {
  document.getElementById('loadingBar').removeAttribute("style");
  var maxWidth = 496;
  var minWidth = 20;
  var widthFactor = params.iterations/params.total;
  var width = Math.max(minWidth,maxWidth * widthFactor);
  document.getElementById('bar').style.width = width + 'px';
  document.getElementById('text').innerHTML = Math.round(widthFactor*100) + '%';
});
network.once("stabilizationIterationsDone", function() {
  document.getElementById('text').innerHTML = '100%';
  document.getElementById('bar').style.width = '496px';
  document.getElementById('loadingBar').style.opacity = 0;
  // really clean the dom element
  setTimeout(function () {document.getElementById('loadingBar').style.display = 'none';}, 500);
});
return network;
}
drawGraph();
```

--------------------------------

### Template for Datalog client analysis

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Standard boilerplate for creating a new client analysis using the provided decompiler libraries.

```datalog
#include "clientlib/decompiler_imports.dl"

.output ...
```

--------------------------------

### Configure Decompilation Options

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Adjust analysis behavior using timeouts, context depth, and precision-enhancing flags.

```bash
# Set custom timeout (300 seconds) with verbose output
./gigahorse.py -T 300 -v examples/long_running.hex

# Use specific context depth for decompilation precision
./gigahorse.py -cd 15 examples/long_running.hex

# Disable scalable fallback for more precise but slower analysis
./gigahorse.py --disable_scalable_fallback examples/long_running.hex

# Enable early cloning for improved precision (increases analysis time ~1.5x)
./gigahorse.py --early_cloning examples/long_running.hex

# Run with debug mode for development
./gigahorse.py --debug -i examples/long_running.hex
```

--------------------------------

### Run Main Datalog Program with Souffle

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/Advanced.md

Execute the main decompilation logic using Souffle. This command assumes the 'facts' directory contains the generated facts and 'logic/main.dl' is the Datalog program.

```bash
souffle -F facts logic/main.dl
```

--------------------------------

### Run Gigahorse on an individual contract

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Executes the lifter on a single .hex file.

```bash
./gigahorse.py examples/long_running.hex
```

--------------------------------

### Execute analysis and inspect results

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Run analysis scripts against bytecode and inspect the generated JSON and CSV output files.

```bash
# Run analysis
./gigahorse.py -C clients/analytics_client.dl examples/long_running.hex

# Check results summary
cat results.json
# Output format: [[filename, [detected_properties], [flags], {analytics}], ...]
# Example:
# [["long_running.hex", ["Analytics_Loop", "Analytics_GlobalVariable"], [], {
#   "disassemble_time": 0.05,
#   "decomp_time": 2.3,
#   "inline_time": 1.1,
#   "client_time": 0.8,
#   "bytecode_size": 4521,
#   "decompiler_config": "default"
# }]]

# Check individual analysis outputs
ls .temp/long_running/out/
# Analytics_Loop.csv
# Analytics_GlobalVariable.csv
# Analytics_Map.csv
# TAC_Op.csv
# TAC_Block.csv
# TAC_Def.csv
# TAC_Use.csv
# ...

# View specific relation output
cat .temp/long_running/out/Analytics_Loop.csv
```

--------------------------------

### Define StorageLocation

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Provides a uniform abstraction for both standard and transient storage.

```solidity
.type StorageLocation = Storage {}
                      | TransientStorage {}
```

--------------------------------

### Visualize Decompilation Results

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/Advanced.md

This command visualizes the intermediate representation (IR) and outputs from the Datalog programs. It's the final step in the manual pipeline for development.

```bash
clients/visualizeout.py
```

--------------------------------

### Create Custom Datalog Analysis

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Define security analysis logic using Datalog and execute it against a target contract.

```datalog
// my_analysis.dl - Custom security analysis example
#include "clientlib/decompiler_imports.dl"

// Find all external calls
.decl ExternalCallFound(stmt: Statement, target: Variable)
.output ExternalCallFound

ExternalCallFound(stmt, target) :-
  CALL(stmt, _, target, _, _, _, _, _, _).

ExternalCallFound(stmt, target) :-
  STATICCALL(stmt, _, target, _, _, _, _, _).

ExternalCallFound(stmt, target) :-
  DELEGATECALL(stmt, _, target, _, _, _, _, _).

// Find calls with non-constant targets (potential vulnerability)
.decl DynamicCallTarget(stmt: Statement)
.output DynamicCallTarget

DynamicCallTarget(stmt) :-
  ExternalCallFound(stmt, target),
  !Variable_Value(target, _).
```

```bash
# Run custom analysis
./gigahorse.py -C my_analysis.dl examples/long_running.hex
cat .temp/long_running/out/DynamicCallTarget.csv
```

--------------------------------

### Custom Flow Analysis with Specific Transfer Functions

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Implement custom flow analysis by defining transfer functions for specific statement opcodes and block boundaries. Initialize with LocalFlowAnalysis.

```Datalog
// Custom flow analysis with specific transfer functions
.init myFlowAnalysis = LocalFlowAnalysis
myFlowAnalysis.TransferStmt(stmt) :-
  Statement_Opcode(stmt, "ADD").
myFlowAnalysis.TransferStmt(stmt) :-
  Statement_Opcode(stmt, "SUB").
myFlowAnalysis.TransferBoundary(block) :-
  IsBlock(block).
```

--------------------------------

### Analyze Contract Creation Operations

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Detects contract creation operations (CREATE and CREATE2), extracting the value transferred and the address of the created contract.

```Datalog
#include "clientlib/decompiler_imports.dl"

// Contract creation
.decl ContractCreation(stmt: Statement, value: Variable, createdAddr: Variable)
.output ContractCreation

ContractCreation(stmt, val, addr) :- CREATE(stmt, val, _, _, addr).
ContractCreation(stmt, val, addr) :- CREATE2(stmt, val, _, _, _, addr).
```

--------------------------------

### Storage Modeling API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Reconstruct contract storage layout and analyze storage access patterns.

```APIDOC
## Storage Modeling API

### Description
Reconstruct contract storage layout and analyze storage access patterns.

### Request Example
```datalog
#include "clientlib/storage_modeling/storage_modeling.dl"

.decl StorageVariableAccess(stmt: Statement, construct: StorageConstruct, loadedVar: Variable)
.output StorageVariableAccess

StorageVariableAccess(stmt, cons, var) :-
  StorageLoad(stmt, cons, var).
```
```

--------------------------------

### Clone Gigahorse Repository

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/README.md

Use the recursive flag to ensure all submodules are included during the initial clone.

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

--------------------------------

### Custom May-Happen-Before Analysis for Reentrancy

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Implements a custom 'may-happen-before' analysis to detect potential reentrancy risks between external calls and state-modifying operations.

```Datalog
#include "clientlib/dominators.dl"

// Custom may-happen-before analysis
.init storeAfterCall = MayHappenBeforeGlobal
storeAfterCall.Before(stmt) :- CALLStatement(stmt, _).
storeAfterCall.After(stmt) :- SSTORE(stmt, _, _).

.decl ReentrancyRisk(callStmt: Statement, sstoreStmt: Statement)
.output ReentrancyRisk

ReentrancyRisk(call, sstore) :-
  storeAfterCall.MayHappenBefore(call, sstore).
```

--------------------------------

### Analyze function structure with Datalog

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Use these relations to extract public functions, arguments, return values, call graphs, and function boundaries from decompiled bytecode.

```datalog
#include "clientlib/decompiler_imports.dl"

// Get all public functions with selectors
.decl PublicFunctions(func: Function, selector: symbol, name: symbol)
.output PublicFunctions

PublicFunctions(func, selector, name) :-
  PublicFunctionId(func, selector, name).

// Get function arguments (internal functions)
.decl FunctionArguments(func: Function, arg: Variable, position: number)
.output FunctionArguments

FunctionArguments(func, arg, pos) :-
  FormalArgs(func, arg, pos).

// Get function return values
.decl FunctionReturns(func: Function, returnVar: Variable, position: number)
.output FunctionReturns

FunctionReturns(func, ret, pos) :-
  FormalReturnArgs(func, ret, pos).

// Call graph edges
.decl InternalCallGraph(callerBlock: Block, calleeFunc: Function)
.output InternalCallGraph

InternalCallGraph(block, func) :-
  CallGraphEdge(block, func).

// Function entry and exit blocks
.decl FunctionBoundaries(func: Function, entryBlock: Block, exitBlock: Block)
.output FunctionBoundaries

FunctionBoundaries(func, entry, exit) :-
  InFunction(entry, func),
  FunctionEntry(entry),
  InFunction(exit, func),
  FunctionExit(exit).
```

--------------------------------

### TAC Instructions Reference API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

APIs for working with the three-address code (TAC) instruction set generated by the decompiler.

```APIDOC
## TAC Instructions Reference

Work with the three-address code instruction set produced by the decompiler.

### Binary arithmetic operations
```datalog
.decl ArithmeticOp(stmt: Statement, op: Opcode, result: Variable)
.output ArithmeticOp

ArithmeticOp(stmt, op, result) :- BinArith(op), Statement_Opcode(stmt, op), Statement_Defines(stmt, result, _).
```

### All CALL variants
```datalog
.decl AllCalls(stmt: Statement, target: Variable, callType: symbol)
.output AllCalls

AllCalls(stmt, target, "CALL") :- CALL(stmt, _, target, _, _, _, _, _, _).
AllCalls(stmt, target, "STATICCALL") :- STATICCALL(stmt, _, target, _, _, _, _, _).
AllCalls(stmt, target, "DELEGATECALL") :- DELEGATECALL(stmt, _, target, _, _, _, _, _).
AllCalls(stmt, target, "CALLCODE") :- CALLCODE(stmt, _, target, _, _, _, _, _, _).
```

### Contract creation
```datalog
.decl ContractCreation(stmt: Statement, value: Variable, createdAddr: Variable)
.output ContractCreation

ContractCreation(stmt, val, addr) :- CREATE(stmt, val, _, _, addr).
ContractCreation(stmt, val, addr) :- CREATE2(stmt, val, _, _, _, addr).
```

### Environment information access
```datalog
.decl EnvironmentAccess(stmt: Statement, envType: Opcode, result: Variable)
.output EnvironmentAccess

EnvironmentAccess(stmt, "CALLER", result) :- CALLER(stmt, result).
EnvironmentAccess(stmt, "ORIGIN", result) :- ORIGIN(stmt, result).
EnvironmentAccess(stmt, "CALLVALUE", result) :- CALLVALUE(stmt, result).
EnvironmentAccess(stmt, "ADDRESS", result) :- ADDRESS(stmt, result).
EnvironmentAccess(stmt, "TIMESTAMP", result) :- TIMESTAMP(stmt, result).
```

### Function call and return (internal)
```datalog
.decl InternalCall(stmt: Statement, targetFunc: Variable)
.output InternalCall

InternalCall(stmt, target) :- CALLPRIVATE(stmt, target).
```

### PHI nodes (SSA form)
```datalog
.decl PhiNode(stmt: Statement, fromVar: Variable, toVar: Variable)
.output PhiNode

PhiNode(stmt, from, to) :- PHI(stmt, from, to).
```
```

--------------------------------

### Loop Analysis API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

APIs for analyzing loop structures to identify gas optimization opportunities and potential vulnerabilities like reentrancy.

```APIDOC
## Loop Analysis API

Analyze loop structures for gas optimization and vulnerability detection.

### Find all structured loops
```datalog
.decl LoopInfo(loopHead: Block, bodyBlock: Block)
.output LoopInfo

LoopInfo(loop, body) :- BlockInStructuredLoop(body, loop).
```

### Find loops with state-modifying operations (potential gas issues)
```datalog
.decl LoopWithSSTORE(loop: Block, sstoreStmt: Statement)
.output LoopWithSSTORE

LoopWithSSTORE(loop, stmt) :- StatementInStructuredLoop(stmt, loop), SSTORE(stmt, _, _).
```

### Find loops with external calls (reentrancy concern)
```datalog
.decl LoopWithExternalCall(loop: Block, callStmt: Statement)
.output LoopWithExternalCall

LoopWithExternalCall(loop, stmt) :- StatementInStructuredLoop(stmt, loop), CALLStatement(stmt, _).
```

### Detect high-level loops (good control flow)
```datalog
.decl WellStructuredLoop(loop: Block)
.output WellStructuredLoop

WellStructuredLoop(loop) :- HighLevelLoop(loop).
```

### Find loop exit conditions
```datalog
.decl LoopCondition(loop: Block, conditionVar: Variable)
.output LoopCondition

LoopCondition(loop, condVar) :- LoopExitCond(condVar, loop).
```
```

--------------------------------

### Decompile EVM Bytecode

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Basic commands for decompiling contracts, including batch processing and visualization output.

```bash
# Decompile a single contract
./gigahorse.py examples/long_running.hex

# Decompile with visualization client to produce human-readable TAC
./gigahorse.py -C clients/visualizeout.py examples/long_running.hex

# Batch analysis of a directory with 8 parallel jobs
./gigahorse.py -j 8 -C clients/visualizeout.py contracts/

# View the decompiled output
cat .temp/long_running/out/contract.tac
```

--------------------------------

### Find Owner-Only Patterns

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identify blocks that appear to be owner-only protected by checking for statically guarded blocks with specific conditions on the guard value. Excludes constant guards and 'this'.

```Datalog
// Find owner-only patterns
.decl OwnerOnlyBlock(block: Block, ownerStorageSlot: Value)
.output OwnerOnlyBlock

OwnerOnlyBlock(block, slot) :-
  StaticallyGuardedBlock(block, slot),
  substr(slot, 0, 9) != "CONSTANT_",
  slot != "this".
```

--------------------------------

### Storage Analysis Relations

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Definitions for tracking storage statements, high-level uses, loads, stores, and data structure metadata.

```APIDOC
## StorageStmtKindAndConstruct

### Description
Maps Storage and Transient Storage statements to their corresponding construct and their StorageStmtKind.

### Parameters
- **stmt** (Statement) - The storage statement.
- **kind** (StorageStmtKind) - The kind of storage statement.
- **loc** (StorageLocation) - The location of the storage.
- **construct** (StorageConstruct) - The associated storage construct.

## StorageStmt_HighLevelUses

### Description
Provides information about storage and transient storage statements on potentially nested data structures, including index variables and field offsets.

### Parameters
- **stmt** (Statement) - The storage statement.
- **accessVar** (Variable) - The variable being accessed.
- **offset** (number) - The field offset.
- **i** (number) - Index variable identifier.
- **nestedness** (number) - The level of nesting.

## StorageLoad

### Description
Provides storage load information. For packed variables, the load is considered the statement that extracts the bytes defining the variable.

### Parameters
- **load** (Statement) - The statement extracting the value.
- **cons** (StorageConstruct) - The storage construct.
- **loadedVar** (Variable) - The variable loaded.

## StorageStore

### Description
Provides SSTORE statement write information. One SSTORE can write multiple constructs due to optimized packed variable patterns.

### Parameters
- **store** (Statement) - The SSTORE statement.
- **cons** (StorageConstruct) - The storage construct.
- **write** (VarOrConstWrite) - The variable or constant written.

## ArrayDeleteOp

### Description
Identifies when an array is deleted by setting its length to zero and erasing contents in a loop.

### Parameters
- **sstore** (Statement) - The SSTORE statement setting length to zero.
- **loop** (Block) - The loop erasing contents.
- **loc** (StorageLocation) - The storage location.
- **array** (StorageConstruct) - The array construct.

## DataStructureValueIsStruct

### Description
Identifies if a data structure construct has a value or element that is a struct.

### Parameters
- **loc** (StorageLocation) - The storage location.
- **cons** (StorageConstruct) - The storage construct.
- **structID** (symbol) - The unique identifier for the struct.
- **elemNum** (number) - The element number.

## StructToString

### Description
Maps a struct ID to its Solidity-like string definition.

### Parameters
- **structID** (symbol) - The unique identifier for the struct.
- **stringStruct** (symbol) - The string representation of the struct definition.
```

--------------------------------

### Find All Structured Loops

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identifies all structured loops within the analyzed code. Useful for general loop analysis.

```Datalog
#include "clientlib/loops.dl"

// Find all structured loops
.decl LoopInfo(loopHead: Block, bodyBlock: Block)
.output LoopInfo

LoopInfo(loop, body) :-
  BlockInStructuredLoop(body, loop).
```

--------------------------------

### Memory Modeling API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Analyze EVM memory operations including external calls, SHA3, LOGs, and array manipulations.

```APIDOC
## Memory Modeling API

### Description
Analyze EVM memory operations including external calls, SHA3, LOGs, and array manipulations.

### Request Example
```datalog
#include "clientlib/memory_modeling/memory_modeling.dl"

.decl CallArguments(call: Statement, arg: Variable, index: number)
.output CallArguments

CallArguments(call, arg, index) :-
  MemoryStatement_ActualArg(call, arg, index),
  CALLStatement(call, _).
```
```

--------------------------------

### Find Loops with State-Modifying Operations

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Detects loops containing SSTORE operations, which may indicate potential gas inefficiencies or vulnerabilities.

```Datalog
#include "clientlib/loops.dl"

// Find loops with state-modifying operations (potential gas issues)
.decl LoopWithSSTORE(loop: Block, sstoreStmt: Statement)
.output LoopWithSSTORE

LoopWithSSTORE(loop, stmt) :-
  StatementInStructuredLoop(stmt, loop),
  SSTORE(stmt, _, _).
```

--------------------------------

### Identify All CALL Variants

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Collects all types of external calls (CALL, STATICCALL, DELEGATECALL, CALLCODE) along with their target variables.

```Datalog
#include "clientlib/decompiler_imports.dl"

// All CALL variants
.decl AllCalls(stmt: Statement, target: Variable, callType: symbol)
.output AllCalls

AllCalls(stmt, target, "CALL") :- CALL(stmt, _, target, _, _, _, _, _, _).
AllCalls(stmt, target, "STATICCALL") :- STATICCALL(stmt, _, target, _, _, _, _, _).
AllCalls(stmt, target, "DELEGATECALL") :- DELEGATECALL(stmt, _, target, _, _, _, _, _).
AllCalls(stmt, target, "CALLCODE") :- CALLCODE(stmt, _, target, _, _, _, _, _, _).
```

--------------------------------

### Generate Facts from EVM Bytecode

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/Advanced.md

This command generates relational facts from EVM bytecode, which is the first step in manually executing the Gigahorse pipeline for development.

```bash
./generatefacts <contract> facts
```

--------------------------------

### Find Mapping Accesses

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identify accesses to storage mappings, extracting the statement and the key variable used. This rule involves complex pattern matching on storage constructs.

```Datalog
// Find mapping accesses
.decl MappingAccess(stmt: Statement, mappingSlot: Value, keyVar: Variable)
.output MappingAccess

MappingAccess(stmt, slot, keyVar) :-
  StorageStmtKindAndConstruct(stmt, $VariableAccess(), $Storage(), cons),
  cons = $Mapping($Constant(slot)),
  StorageStmt_HighLevelUses(stmt, keyVar, 0, 0, 1).
```

--------------------------------

### Memory and Call Relations

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/memory_modeling/README.md

Relations for tracking arguments and return values in memory-related statements and external calls.

```APIDOC
## MemoryStatement_ActualArg(stmt:Statement, actual:Variable, index:number)

### Description
Variable `actual` is the `index`'th argument of memory reading statement `stmt`.

## ExternalCall_ActualReturn(callStmt:Statement, actual:Variable, index:number)

### Description
Variable `actual` loads the `index`'th return of external call `callStmt`.

## ArbitraryCall(callStmt:Statement)

### Description
External call `callStmt` has its entire call-data provided by a caller.

## PublicFunctionArg(pubFun:Function, arg:Variable, index:number)

### Description
Variable `arg` is the `index`th argument of public function `pubFun`.
```

--------------------------------

### Find Blocks that Dominate a Target

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identifies all basic blocks that dominate a specified target block in the control flow graph.

```Datalog
#include "clientlib/dominators.dl"

// Find blocks that dominate a target
.decl BlockDominators(target: Block, dominator: Block)
.output BlockDominators

BlockDominators(target, dom) :-
  Dominates(dom, target).
```

--------------------------------

### Guard Pattern Detection API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Detect common authentication and authorization patterns in smart contracts.

```APIDOC
## Guard Pattern Detection API

### Description
Detect common authentication and authorization patterns in smart contracts.

### Request Example
```datalog
#include "clientlib/guards.dl"

.decl ProtectedBlock(block: Block, guardValue: Value)
.output ProtectedBlock

ProtectedBlock(block, guardVal) :-
  StaticallyGuardedBlock(block, guardVal).
```
```

--------------------------------

### Helper Relations

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/memory_modeling/README.md

Additional helper relations for common patterns like SHA3 hashing and ERC20 function calls.

```APIDOC
## SHA3_1ARG(stmt:Statement, arg:Variable, def:Variable)

### Description
Represents a SHA3 statement with 1 argument.

## CallToSignature(callStmt:Statement, sigText:symbol)

### Description
External call `callStmt` calls a high-level function with a signature of `sigText`.

## ERC20TransferCall(call:Statement, to:Variable, value:Variable)

### Description
Shortcut for ERC20 transfer function calls.
```

--------------------------------

### Find Unguarded State-Modifying Operations

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Detect state-modifying operations (SSTORE) that occur within blocks not protected by any static guard. This rule identifies potential security vulnerabilities.

```Datalog
// Find unguarded state-modifying operations
.decl UnguardedStateChange(stmt: Statement)
.output UnguardedStateChange

UnguardedStateChange(stmt) :-
  SSTORE(stmt, _, _),
  Statement_Block(stmt, block),
  !StaticallyGuardedBlock(block, _).
```

--------------------------------

### Analyze Binary Arithmetic Operations

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Extracts information about binary arithmetic operations, including the statement, opcode, and the variable it defines.

```Datalog
#include "clientlib/decompiler_imports.dl"

// Binary arithmetic operations
.decl ArithmeticOp(stmt: Statement, op: Opcode, result: Variable)
.output ArithmeticOp

ArithmeticOp(stmt, op, result) :-
  BinArith(op),
  Statement_Opcode(stmt, op),
  Statement_Defines(stmt, result, _).
```

--------------------------------

### Array Related Relations

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/memory_modeling/README.md

Relations for tracking array allocations, indexing, and length properties.

```APIDOC
## VarIsArray(var:Variable, arrId:ArrayVariable)

### Description
Variable `var` is array `arrId`.

## ArrayAllocation(arrId:ArrayVariable, elemSize:Value, arrayLength:Variable)

### Description
Array `arrId` is allocated with a type of size `elemSize` and a length equal to the runtime value of variable `arrayLength`.

## ArrayStoreAtIndex(stmt:Statement, arrId:ArrayVariable, index:Variable, from:Variable)

### Description
Statement `stmt` stores `from` into array `arrId` at index `index`.

## ArrayLoadAtIndex(stmt:Statement, arrId:ArrayVariable, index:Variable, to:Variable)

### Description
Statement `stmt` loads `to` from array `arrId` at index `index`.

## ArrayLengthVar(arrId:ArrayVariable, lenVar:Variable)

### Description
Variable `lenVar` loads the length of array `arrId`.
```

--------------------------------

### Dominator and Control Flow Analysis API

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

APIs for analyzing control flow dominance relationships and execution paths, including custom may-happen-before analysis for reentrancy detection.

```APIDOC
## Dominator and Control Flow Analysis

Analyze control flow dominance relationships and execution paths.

### Find blocks that dominate a target
```datalog
.decl BlockDominators(target: Block, dominator: Block)
.output BlockDominators

BlockDominators(target, dom) :- Dominates(dom, target).
```

### Find post-dominators (blocks that will always execute after)
```datalog
.decl BlockPostDominators(block: Block, postDom: Block)
.output BlockPostDominators

BlockPostDominators(block, postDom) :- PostDominates(postDom, block).
```

### Custom may-happen-before analysis
```datalog
.init storeAfterCall = MayHappenBeforeGlobal
storeAfterCall.Before(stmt) :- CALLStatement(stmt, _).
storeAfterCall.After(stmt) :- SSTORE(stmt, _, _).

.decl ReentrancyRisk(callStmt: Statement, sstoreStmt: Statement)
.output ReentrancyRisk

ReentrancyRisk(call, sstore) :- storeAfterCall.MayHappenBefore(call, sstore).
```
```

--------------------------------

### Find Loops with External Calls

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identifies loops that include external calls, which could be a source of reentrancy vulnerabilities.

```Datalog
#include "clientlib/loops.dl"

// Find loops with external calls (reentrancy concern)
.decl LoopWithExternalCall(loop: Block, callStmt: Statement)
.output LoopWithExternalCall

LoopWithExternalCall(loop, stmt) :-
  StatementInStructuredLoop(stmt, loop),
  CALLStatement(stmt, _).
```

--------------------------------

### Analyze SHA3 Operations with Known Content

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identify SHA3 operations where the content is known. This rule uses the SHA3_KnownContent predicate.

```Datalog
// Analyze SHA3 operations with known content
.decl KnownHashInput(stmt: Statement, content: symbol)
.output KnownHashInput

KnownHashInput(stmt, content) :-
  SHA3_KnownContent(stmt, content).
```

--------------------------------

### Track Array Write Operations

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Record array write operations, including the statement, array variable, index, and value. This rule uses the ArrayStoreAtIndex predicate.

```Datalog
// Array operations
.decl ArrayWrite(stmt: Statement, array: ArrayVariable, index: Variable, value: Variable)
.output ArrayWrite

ArrayWrite(stmt, arr, idx, val) :-
  ArrayStoreAtIndex(stmt, arr, idx, val).
```

--------------------------------

### Find Post-Dominators

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Determines blocks that post-dominate a given block, meaning they are always executed after the block.

```Datalog
#include "clientlib/dominators.dl"

// Find post-dominators (blocks that will always execute after)
.decl BlockPostDominators(block: Block, postDom: Block)
.output BlockPostDominators

BlockPostDominators(block, postDom) :-
  PostDominates(postDom, block).
```

--------------------------------

### Find Loop Exit Conditions

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Extracts the variables used as conditions for exiting loops. Useful for understanding loop termination logic.

```Datalog
#include "clientlib/loops.dl"

// Find loop exit conditions
.decl LoopCondition(loop: Block, conditionVar: Variable)
.output LoopCondition

LoopCondition(loop, condVar) :-
  LoopExitCond(condVar, loop).
```

--------------------------------

### Use Custom Arithmetic Flows

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Utilize custom flow analysis results to define arithmetic flows between variables. This rule derives flows from the custom analysis.

```Datalog
// Use custom flows
.decl ArithmeticFlows(from: Variable, to: Variable)
ArithmeticFlows(from, to) :- myFlowAnalysis.Flows(from, to).
```

--------------------------------

### Analyze Environment Information Access

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identifies statements that access environment information such as CALLER, ORIGIN, CALLVALUE, ADDRESS, and TIMESTAMP.

```Datalog
#include "clientlib/decompiler_imports.dl"

// Environment information access
.decl EnvironmentAccess(stmt: Statement, envType: Opcode, result: Variable)
.output EnvironmentAccess

EnvironmentAccess(stmt, "CALLER", result) :- CALLER(stmt, result).
EnvironmentAccess(stmt, "ORIGIN", result) :- ORIGIN(stmt, result).
EnvironmentAccess(stmt, "CALLVALUE", result) :- CALLVALUE(stmt, result).
EnvironmentAccess(stmt, "ADDRESS", result) :- ADDRESS(stmt, result).
EnvironmentAccess(stmt, "TIMESTAMP", result) :- TIMESTAMP(stmt, result).
```

--------------------------------

### Define StorageStmtKind

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Defines the types of storage operations, such as variable access or array length manipulation.

```solidity
.type StorageStmtKind = VariableAccess {}
                      | ArrayDataStart {}
                      | ArrayLength {}
```

--------------------------------

### Detect High-Level Loops

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Identifies loops that are considered 'high-level', suggesting good control flow structure.

```Datalog
#include "clientlib/loops.dl"

// Detect high-level loops (good control flow)
.decl WellStructuredLoop(loop: Block)
.output WellStructuredLoop

WellStructuredLoop(loop) :-
  HighLevelLoop(loop).
```

--------------------------------

### Define VarOrConstWrite

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Unifies variable and constant write operations into a single type.

```solidity
.type VarOrConstWrite = VariableWrite {var: Variable}
                      | ConstantWrite {const: Value}
```

--------------------------------

### Define StorageConstruct ADT

Source: https://github.com/nevillegrech/gigahorse-toolchain/blob/master/clientlib/storage_modeling/README.md

Defines the nested ADT structure used to represent contract storage layouts.

```solidity
.type StorageConstruct = Constant {value: Value}
                        | StaticArray {parConstruct: StorageConstruct, arraySize: number}
                        | Array {parConstruct: StorageConstruct}
                        | Mapping {parConstruct: StorageConstruct}
                        | Offset {parConstruct: StorageConstruct, offset: number}
                        | Variable {construct: StorageConstruct}
                        | TightlyPackedVariable {construct: StorageConstruct, byteLow: number, byteHigh: number}
```

--------------------------------

### Analyze PHI Nodes (SSA Form)

Source: https://context7.com/nevillegrech/gigahorse-toolchain/llms.txt

Extracts PHI nodes, which represent variable assignments in the Static Single Assignment (SSA) form.

```Datalog
#include "clientlib/decompiler_imports.dl"

// PHI nodes (SSA form)
.decl PhiNode(stmt: Statement, fromVar: Variable, toVar: Variable)
.output PhiNode

PhiNode(stmt, from, to) :- PHI(stmt, from, to).
```