Major refactoring, introducing EVMLiSA as a Library

.gitignore

@@ -10,10 +10,16 @@
 # Ignore output directories that contain generated results
 evm-outputs/
 test-ground-truth-stats/
-evm-testcases/ground-truth/test-ground-truth-results/logs.txt
-evm-testcases/ground-truth/test-ground-truth-results/statistics.csv
 evm-testcases/ground-truth/test/*
 
+# Ignore 50-ground-truth file
+evm-testcases/ground-truth/50-ground-truth/**/*.html
+evm-testcases/ground-truth/50-ground-truth/**/*.opcode
+evm-testcases/ground-truth/50-ground-truth/**/*.json
+evm-testcases/ground-truth/50-ground-truth/**/*.dot
+evm-testcases/ground-truth/50-ground-truth/**/*.js
+
+
 # Ignore benchmark file
 scripts/python/benchmark-checkers/**/bytecode/**
 scripts/python/benchmark-checkers/**/abi/**

README.md

@@ -12,96 +12,132 @@ EVMLiSA is a static analyzer based on abstract interpretation for [EVM bytecode]
 EVMLiSA is based on the peer-reviewed publication
 > Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella. _**"Towards a Sound Construction of EVM Bytecode Control-Flow Graphs"**_. In Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2024), co-located with ECOOP 2024.
 
-# 🛠 Building EVMLiSA
-Compiling EVMLiSA requires:
-- JDK >= 11 (optional using Docker)
-- [Gradle](https://gradle.org/releases/) >= 8.0 (optional using Docker)
+## Table of Contents
+
+- [Requirements](#requirements)
+- [Installation](#installation)
+  - [Environment Setup](#environment-setup)
+- [Execution Methods](#execution-methods)
+  - [Using Docker](#using-docker)
+  - [Using CLI](#using-command-line)
+- [Options](#options)
+- [The Abstract Stack Set Domain](#the-abstract-stack-set-domain)
+- [Jump Classification](#jump-classification)
+- [Usage Example](#usage-example)
+  - [Example Output](#example-output)
+- [EVMLiSA as a Library](#EVMLiSA-as-a-library)
+
+---
+
+## Requirements
+
+To build and run EVMLiSA, you will need:
+
+- JDK 11 or higher (optional when using Docker)
+- [Gradle](https://gradle.org/releases/) 8.0 or higher (optional when using Docker)
 - [Etherscan API key](https://etherscan.io/myapikey)
 
-You need to:
-- Clone the repository:
-  ```bash
-  git clone https://github.com/lisa-analyzer/evm-lisa.git
-  cd evm-lisa
-  ```
-- Import the project into the Eclipse/IntelliJ workspace as a Gradle project (optional).
+## Installation
 
-# ⚙️ Running EVMLiSA
-Before running EVMLiSA, ensure you have set up an Environment Variable with your Etherscan API Key. Follow the steps below to set up the environment variable:
+1. Clone the repository:
+   ```bash
+   git clone https://github.com/lisa-analyzer/evm-lisa.git
+   cd evm-lisa
+   ```
 
-1. Begin by creating a file named `.env` in the EVMLiSA project.
-2. Inside the `.env` file, add the following line:
-```
-ETHERSCAN_API_KEY=<your_etherscan_api_key>
-```
-3. Replace `<your_etherscan_api_key>` with your Etherscan API key.
+2. (Optional) Import the project into Eclipse or IntelliJ as a Gradle project.
 
-> Here you can find how to generate an [Etherscan API key](https://etherscan.io/myapikey).
+### Environment Setup
 
-Once you have set up the environment variable, you can run EVMLiSA via Docker or via Bash.
+Before running EVMLiSA, you must configure your Etherscan API key:
 
-## Via Docker
-Build the container:
-```
-mkdir -p execution/docker &&
-docker build -t evm-lisa:latest .
-```
+1. Create a `.env` file in the project root directory.
+2. Add the following line to the file:
+   ```
+   ETHERSCAN_API_KEY=<your_etherscan_api_key>
+   ```
+3. Replace `<your_etherscan_api_key>` with your actual key from [Etherscan](https://etherscan.io/myapikey).
 
-Then you can run EVMLiSA with:
-```
-docker run --rm -it \
--v $(pwd)/.env:/app/.env \
--v $(pwd)/execution/docker:/app/execution/results \
-evm-lisa:latest \
-[options]
-```
+Alternatively, you can pass your API key directly using the `--etherscan-api-key <key>` option when executing the analyzer.
 
-- `-v $(pwd)/.env:/app/.env`: mount the `.env` file.
-- `-v $(pwd)/execution/docker:/app/execution/results`: share the results' folder.
+## Execution Methods
 
-## Via Bash
-Build the Project:
-```bash
-./gradlew assemble
-```
+### Using Docker
 
-Then you can run EVMLiSA with:
-```bash
-java -jar build/libs/evm-lisa-all.jar [options]
-```
+1. Build the Docker container:
+   ```bash
+   mkdir -p execution/docker &&
+   docker build -t evm-lisa:latest .
+   ```
+
+2. Run EVMLiSA with Docker:
+   ```bash
+   docker run --rm -it \
+   -v $(pwd)/.env:/app/.env \
+   -v $(pwd)/execution/docker:/app/execution/results \
+   evm-lisa:latest \
+   [options]
+   ```
+
+   - `-v $(pwd)/.env:/app/.env`: Mounts your environment file
+   - `-v $(pwd)/execution/docker:/app/execution/results`: Shares the results directory
+
+### Using Command Line
+
+1. Build the project:
+   ```bash
+   ./gradlew assemble
+   ```
+
+2. Run EVMLiSA:
+   ```bash
+   java -jar build/libs/evm-lisa-all.jar [options]
+   ```
+
+## Options
 
 ```
 Options:
- -a,--address <arg>                        Address of an Ethereum smart contract.
- -b,--benchmark <arg>                      Filepath of the benchmark.
-    --basic-blocks                         Generate CFG with basic blocks.
- -c,--cores <arg>                          Number of cores used in benchmark.
-    --checker-reentrancy                   Enable re-entrancy checker.
-    --checker-timestampdependency          Enable timestamp-dependency checker.
-    --checker-txorigin                     Enable tx-origin checker.
-    --dot                                  Export a dot-notation file.
-    --download-bytecode                    Download the bytecode.
-    --dump-report                          Dump analysis report.
-    --dump-stats                           Dump statistics.
- -f,--filepath-bytecode <arg>              Filepath of the bytecode file.
-    --html                                 Export a graphic HTML report.
-    --link-unsound-jumps-to-all-jumpdest   Link all the unsound jumps to all jumpdest.
- -o,--output <arg>                         Output directory path.
-    --serialize-inputs                     Serialize inputs.
-    --stack-set-size <arg>                 Dimension of stack-set (default: 8).
-    --stack-size <arg>                     Dimension of stack (default: 32).
-    --use-live-storage                     Use the live storage in SLOAD.
+ -a,--address <arg>                        Address of an Ethereum smart contract
+    --abi <arg>                            ABI of the bytecode to be analyzed (JSON format).
+    --abi-path <arg>                       Filepath of the ABI file
+ -b,--bytecode <arg>                       Bytecode to be analyzed (e.g., 0x6080...)
+    --benchmark <arg>                      Filepath of the benchmark
+    --bytecode-path <arg>                  Filepath of the bytecode file
+ -c,--cores <arg>                          Number of cores used in benchmark
+    --checker-all                          Enable all security checkers
+    --checker-reentrancy                   Enable reentrancy checker
+    --checker-timestampdependency          Enable timestamp-dependency checker
+    --checker-txorigin                     Enable tx-origin checker
+    --etherscan-api-key <arg>              Insert your Etherscan API key
+    --link-unsound-jumps-to-all-jumpdest   Link all unsound jumps to all jumpdest
+    --output-directory-path <arg>          Filepath of the output directory
+    --stack-set-size <arg>                 Dimension of stack-set (default: 8)
+    --stack-size <arg>                     Dimension of stack (default: 32)
+    --use-live-storage                     Use the live storage in SLOAD
 ```
 
-# 🔍 Abstract Stack Set Domain
-In the analysis of EVM bytecode programs, EVMLiSA employs a domain of sets of abstract stacks to enhance precision, particularly when loops are encountered in the source code.
+## The Abstract Stack Set Domain
+
+In analyzing EVM bytecode programs, EVMLiSA employs a domain of sets of abstract stacks to enhance precision, particularly for code containing loops.
+
+The analyzer introduces the abstract stack powerset domain $\texttt{SetSt}_{k,h,l}$ consisting of sets of abstract stacks with at most $l$ elements and a maximum height of $h$. This domain allows the analyzer to maintain collections of abstract stacks, avoiding the need to compute the least upper bound (lub) and allowing each element of an abstract stack to be a $k$ integer set.
+
+## Jump Classification
+
+EVMLiSA classifies jump instructions in the following categories:
+
+- **Resolved**: All destinations of the jump node have been successfully resolved
+- **Definitely unreachable**: The jump node is unreachable (reached with the bottom abstract state)
+- **Maybe unreachable**: The jump node is not reachable from the entry point, but may be reachable via a potentially unsound jump node
+- **Unsound**: The jump node is reached with a stack containing an unknown numerical value that may correspond to a valid jump destination
+- **Maybe unsound**: The stack set exceeded the maximum configured stack size
 
-EVMLiSA introduces the abstract stack powerset domain $\texttt{SetSt}_{k,h,l}$ which consists of sets of abstract stacks with at most $l$ elements and an height of at most $h$. This domain allows the analyzer to maintain collections of abstract stacks, avoiding the need to compute the lub and allowing each element of an abstract stack to be a $k$ integer set.
+## Usage Example
 
-# 📋 Running example
-Here is an example of how to run EVMLiSA. In this example, we will analyze a smart contract at the address `0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B` with specific options for stack size, stack-set size, live storage usage and the dump of the CFG:
+Analyze a smart contract with specific configuration parameters:
 
-- Bash:
+**Using Command Line:**
 ```bash
 java -jar build/libs/evm-lisa-all.jar \
 -a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B \
@@ -110,7 +146,7 @@ java -jar build/libs/evm-lisa-all.jar \
 --link-unsound-jumps-to-all-jumpdest
 ```
 
-- Docker:
+**Using Docker:**
 ```bash
 docker run --rm -it \
 -v $(pwd)/.env:/app/.env \
@@ -122,10 +158,11 @@ evm-lisa:latest \
 --link-unsound-jumps-to-all-jumpdest
 ```
 
-> Use `docker run -a stderr` to dump only the json report as standard output.
+> **Tip**: Use `docker run -a stderr` to output only the JSON report to standard output.
 
-The expected output is as follows:
-```yaml
+### Example Output
+
+```
 ##############
 Total opcodes: 344
 Total jumps: 45
@@ -137,17 +174,26 @@ Maybe unsound jumps: 0
 ##############
 ```
 
-### Jump classification
-- _Resolved_: all the destinations of the jump node have been resolved;
-- _Definitely unreachable_: the jump node is unreachable (i.e., it is reached with the bottom abstract state);
-- _Maybe unreachable_: the jump node is not reachable in the CFG, starting from its entry point, but it may be reachable via a (maybe) unsound jump node (if any);
-- _Unsound_: the jump node is reached at least with a stack with an unknown numerical value that may correspond to a
-valid jump destination as the top element;
-- _Maybe unsound_: the stack set exceeded the maximal stack size.
+## EVMLiSA as a Library
 
----
+EVMLiSA can be integrated as a Java library to analyze EVM smart contracts programmatically:
+
+```java
+// Analyze by contract address
+EVMLiSA.analyzeContract(new SmartContract("0x123456..."));
+
+// Analyze from bytecode file path
+EVMLiSA.analyzeContract(new SmartContract(Path.of("bytecode", "code.bytecode")));
+
+// Analyze from bytecode string
+EVMLiSA.analyzeContract(new SmartContract().setBytecode("0x6080..."));
+
+// Analyze multiple contracts
+EVMLiSA.analyzeSetOfContracts(Path.of("list-of-contracts.txt"));
+```
 
 ## Contributors
+
 <a href="https://github.com/lisa-analyzer/evm-lisa/graphs/contributors">
   <img src="https://contrib.rocks/image?repo=lisa-analyzer/evm-lisa" />
 </a>

build.gradle

@@ -20,7 +20,6 @@ plugins {
 repositories {
     // Use jcenter for resolving dependencies.
     // You can declare any Maven/Ivy/file repository here.
-    jcenter()
     mavenCentral()   
 }
 
@@ -43,6 +42,8 @@ dependencies {
  	implementation 'io.github.cdimascio:dotenv-java:3.0.0'
 
  	implementation 'org.json:json:20210307'
+
+    implementation 'org.bouncycastle:bcprov-jdk15on:1.70'
 }
 
 
@@ -147,7 +148,7 @@ tasks.register('checkCodeStyle') {
 }
 
 tasks.named('shadowJar') {
-    archiveBaseName = 'evm-lisa'
+    archiveBaseName.set('evm-lisa')
     manifest {
         attributes(
                 'Main-Class': mainClassName

evm-testcases/cfs/while/report.json

@@ -3,14 +3,14 @@
   "files" : [ "report.json", "untyped_program.evm-testcases_cfs_while_while_eth.sol().json" ],
   "info" : {
     "cfgs" : "1",
-    "duration" : "23ms",
-    "end" : "2025-02-26T11:44:06.360+01:00",
+    "duration" : "281ms",
+    "end" : "2025-03-17T15:38:36.216+01:00",
     "expressions" : "6",
     "files" : "1",
     "globals" : "0",
     "members" : "1",
     "programs" : "1",
-    "start" : "2025-02-26T11:44:06.337+01:00",
+    "start" : "2025-03-17T15:38:35.935+01:00",
     "statements" : "16",
     "units" : "0",
     "version" : "0.1",