lisa-analyzer · VincenzoArceri · Jan 9, 2025 · Oct 30, 2024 · Oct 30, 2024 · Oct 31, 2024
diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml
@@ -0,0 +1,23 @@
+name: 'Docker build image test'
+
+on:
+  pull_request:
+    branches:
+      - master
+  push:
+    branches:
+      - master
+
+jobs:
+  docker-test:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+
+      - name: Build Docker image
+        run: docker build -t evmlisa:test .
+
+      - name: Remove Docker image
+        run: docker rmi evmlisa:test
diff --git a/.gitignore b/.gitignore
@@ -10,8 +10,33 @@
 # Ignore output directories that contain generated results
 evm-outputs/
 test-ground-truth-stats/
-evm-testcases/ground-truth/test/logs.txt
-evm-testcases/ground-truth/test/statistics.csv
+evm-testcases/ground-truth/test-ground-truth-results/logs.txt
+evm-testcases/ground-truth/test-ground-truth-results/statistics.csv
+
+# Ignore benchmark results
+# SolidiFI reentrancy
+scripts/python/journal/reentrancy-solidifi/results/
+scripts/python/journal/reentrancy-solidifi/json/
+scripts/python/journal/reentrancy-solidifi/bytecode/
+scripts/python/journal/vanilla-solidifi/results/
+scripts/python/journal/vanilla-solidifi/json/
+scripts/python/journal/vanilla-solidifi/bytecode/
+
+# smartbugs reentrancy
+scripts/python/journal/reentrancy-smartbugs/results/
+scripts/python/journal/reentrancy-smartbugs/json/
+scripts/python/journal/reentrancy-smartbugs/bytecode/
+
+# SliSE reentrancy
+scripts/python/journal/reentrancy-slise-db1/results/
+scripts/python/journal/reentrancy-slise-db1/json/
+scripts/python/journal/reentrancy-slise-db1/bytecode/
+scripts/python/journal/reentrancy-slise-db1/match-file-index.json
+
+scripts/python/journal/execution/
+scripts/python/journal/images/
+scripts/python/journal/DAppSCAN/
+scripts/python/journal/SliSE/
 
 # Ignore downloaded bytecode
 evm-testcases/benchmark/

diff --git a/.project b/.project
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
 	<name>evm-lisa</name>
-	<comment>Project emv-lisa created by Buildship.</comment>
+	<comment></comment>
 	<projects>
 	</projects>
 	<buildSpec>
@@ -20,15 +20,4 @@
 		<nature>org.eclipse.jdt.core.javanature</nature>
 		<nature>org.eclipse.buildship.core.gradleprojectnature</nature>
 	</natures>
-	<filteredResources>
-		<filter>
-			<id>1698415238879</id>
-			<name></name>
-			<type>30</type>
-			<matcher>
-				<id>org.eclipse.core.resources.regexFilterMatcher</id>
-				<arguments>node_modules|\.git|__CREATED_BY_JAVA_LANGUAGE_SERVER__</arguments>
-			</matcher>
-		</filter>
-	</filteredResources>
 </projectDescription>
diff --git a/README.md b/README.md
@@ -88,18 +88,25 @@ This command will initiate the analysis process for the specified smart contract
 
 ```
 Options:
- -a,--address <arg>          address of an Ethereum smart contract
- -b,--benchmark <arg>        filepath of the benchmark suite (i.e., a list of smart contract addresses)
- -C,--cores <arg>            number of cores to use
- -c,--dump-cfg               dump the CFG
- -d,--dump-analysis <arg>    dump the analysis (html, dot)
- -D,--download-bytecode      download the bytecode, without analyzing it
- -f,--filepath <arg>         filepath of an EVM bytecode smart contract
- -o,--output <arg>           output directory path
- -q,--stack-size <arg>       maximal height of stack
- -s,--dump-stats             dump statistics
- -S,--use-live-storage       use the live storage in SLOAD
- -w,--stack-set-size <arg>   maximal size of stack sets
+ -a,--address <arg>                        Address of an Ethereum smart contract.
+ -b,--benchmark <arg>                      Filepath of the benchmark.
+ -c,--cores <arg>                          Number of cores used in benchmark.
+    --checker-reentrancy                   Enable re-entrancy checker.
+    --checker-txorigin                     Enable tx-origin checker.
+    --creation-code                        Parse bytecode as creation code (instead of runtime code).
+    --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.
+    --filepath-mnemonic <arg>              Filepath of the mnemonic 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.
 ```
 
 # 🔍 Abstract Stack Set Domain

diff --git a/build.gradle b/build.gradle
@@ -34,10 +34,10 @@ dependencies {
  	// Apache Commons CLI
  	implementation 'commons-cli:commons-cli:1.4'
 
- 	implementation 'io.github.lisa-analyzer:lisa-program:0.1b8'
- 	implementation 'io.github.lisa-analyzer:lisa-analyses:0.1b8'
- 	implementation 'io.github.lisa-analyzer:lisa-sdk:0.1b8'
- 	implementation 'io.github.lisa-analyzer:lisa-imp:0.1b8'
+ 	implementation 'io.github.lisa-analyzer:lisa-program:0.1'
+ 	implementation 'io.github.lisa-analyzer:lisa-analyses:0.1'
+ 	implementation 'io.github.lisa-analyzer:lisa-sdk:0.1'
+ 	implementation 'io.github.lisa-analyzer:lisa-imp:0.1'
  	implementation group: 'commons-cli', name: 'commons-cli', version: '1.5.0'
  	implementation 'io.github.cdimascio:dotenv-java:3.0.0'
 

diff --git a/evm-testcases/cfs/add/report.json b/evm-testcases/cfs/add/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/add"
   }

diff --git a/evm-testcases/cfs/addmod/report.json b/evm-testcases/cfs/addmod/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/addmod"
   }

diff --git a/evm-testcases/cfs/and/report.json b/evm-testcases/cfs/and/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/and"
   }

diff --git a/evm-testcases/cfs/byte/report.json b/evm-testcases/cfs/byte/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/byte"
   }

diff --git a/evm-testcases/cfs/div/report.json b/evm-testcases/cfs/div/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/div"
   }

diff --git a/evm-testcases/cfs/if/report.json b/evm-testcases/cfs/if/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/if"
   }

diff --git a/evm-testcases/cfs/if_else/report.json b/evm-testcases/cfs/if_else/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/if_else"
   }

diff --git a/evm-testcases/cfs/if_else_npbj/report.json b/evm-testcases/cfs/if_else_npbj/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/if_else_npbj"
   }

diff --git a/evm-testcases/cfs/lt/report.json b/evm-testcases/cfs/lt/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/lt"
   }

diff --git a/evm-testcases/cfs/mod/report.json b/evm-testcases/cfs/mod/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/mod"
   }

diff --git a/evm-testcases/cfs/mstore/report.json b/evm-testcases/cfs/mstore/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/mstore"
   }

diff --git a/evm-testcases/cfs/mstore/untyped_program.evm-testcases_cfs_mstore_mstore_eth.sol().json b/evm-testcases/cfs/mstore/untyped_program.evm-testcases_cfs_mstore_mstore_eth.sol().json
diff --git a/evm-testcases/cfs/mstore8/report.json b/evm-testcases/cfs/mstore8/report.json
@@ -31,6 +31,7 @@
     "serializeInputs" : "false",
     "serializeResults" : "true",
     "syntacticChecks" : "",
+    "useWideningPoints" : "false",
     "wideningThreshold" : "5",
     "workdir" : "evm-outputs/cfs/mstore8"
   }