Skip to content

Commit c5ea083

Browse files
merendamattiamerendamattia
committed
Added mnemonic option for input file and refactoring
1 parent 92f399a commit c5ea083

File tree

2 files changed

+133
-86
lines changed

2 files changed

+133
-86
lines changed

‎README.md‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,16 +91,18 @@ Options:
9191
-a,--address <arg> Address of an Ethereum smart contract.
9292
-b,--benchmark <arg> Filepath of the benchmark.
9393
-c,--cores <arg> Number of cores used in benchmark.
94+
--checker-reentrancy Enable re-entrancy checker.
95+
--checker-txorigin Enable tx-origin checker.
9496
--creation-code Parse bytecode as creation code (instead of runtime code).
9597
--dot Export a dot-notation file.
9698
--download-bytecode Download the bytecode.
9799
--dump-report Dump analysis report.
98100
--dump-stats Dump statistics.
99101
-f,--filepath-bytecode <arg> Filepath of the bytecode file.
102+
--filepath-mnemonic <arg> Filepath of the mnemonic file.
100103
--html Export a graphic HTML report.
101104
--link-unsound-jumps-to-all-jumpdest Link all the unsound jumps to all jumpdest.
102105
-o,--output <arg> Output directory path.
103-
--reentrancy-checker Enable re-entrancy checker.
104106
--serialize-inputs Serialize inputs.
105107
--stack-set-size <arg> Dimension of stack-set (default: 8).
106108
--stack-size <arg> Dimension of stack (default: 32).

‎src/main/java/it/unipr/EVMLiSA.java‎

Lines changed: 130 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -112,9 +112,10 @@ public void go(String[] args) throws Exception {
112112
String coresOpt = cmd.getOptionValue("cores");
113113
boolean dumpReport = cmd.hasOption("dump-report");
114114
boolean useCreationCode = cmd.hasOption("creation-code");
115-
ENABLE_REENTRANCY_CHECKER = cmd.hasOption("reentrancy-checker");
116-
ENABLE_TXORIGIN_CHECKER = cmd.hasOption("txorigin-checker");
115+
ENABLE_REENTRANCY_CHECKER = cmd.hasOption("checker-reentrancy");
116+
ENABLE_TXORIGIN_CHECKER = cmd.hasOption("checker-txorigin");
117117
boolean linkUnsoundJumpsToAllJumpdestOption = cmd.hasOption("link-unsound-jumps-to-all-jumpdest");
118+
String mnemonicInputFile = cmd.getOptionValue("filepath-mnemonic");
118119

119120
// Download bytecode case
120121
if (downloadBytecode && benchmark != null) {
@@ -186,14 +187,17 @@ public void go(String[] args) throws Exception {
186187
jsonOptions.put("download-bytecode", downloadBytecode);
187188
jsonOptions.put("use-storage-live", useStorageLive);
188189
jsonOptions.put("use-creation-code", useCreationCode);
189-
jsonOptions.put("filepath", filepath);
190+
if (filepath != null)
191+
jsonOptions.put("input-filepath", filepath);
192+
else
193+
jsonOptions.put("input-filepath", mnemonicInputFile);
190194
jsonOptions.put("stack-size", AbstractStack.getStackLimit());
191195
jsonOptions.put("stack-set-size", AbstractStackSet.getStackSetLimit());
192196
jsonOptions.put("benchmark", benchmark);
193197
jsonOptions.put("cores", CORES);
194198
jsonOptions.put("dump-report", dumpReport);
195199
jsonOptions.put("output-directory", OUTPUT_DIR);
196-
jsonOptions.put("link-unsound-jumps-to-all-jumpdest", linkUnsoundJumpsToAllJumpdestOption);
200+
jsonOptions.put("link-unsound-jumps-to-all-jumpdest", JumpSolver.getLinkUnsoundJumpsToAllJumpdest());
197201

198202
// Run benchmark case
199203
if (benchmark != null) {
@@ -230,7 +234,7 @@ public void go(String[] args) throws Exception {
230234
}
231235

232236
// Error case
233-
if (addressSC == null && filepath == null) {
237+
if (addressSC == null && filepath == null && mnemonicInputFile == null) {
234238
log.error("Address or filepath required.");
235239
formatter.printHelp("help", options);
236240
System.exit(1);
@@ -253,21 +257,24 @@ public void go(String[] args) throws Exception {
253257
STATISTICS_FULLPATH = _outputDirPath.resolve(addressSC + "_STATISTICS.csv").toString();
254258
FAILURE_FULLPATH = _outputDirPath.resolve(addressSC + "_FAILURE.csv").toString();
255259

256-
String BYTECODE_FULLPATH = _outputDirPath.resolve(addressSC + ".opcode").toString();
257-
String bytecode;
258-
if (filepath == null) {
259-
bytecode = EVMFrontend.parseContractFromEtherscan(addressSC);
260-
} else {
261-
bytecode = new String(Files.readAllBytes(Paths.get(filepath)));
262-
}
263-
if (useCreationCode) {
264-
jsonOptions.put("bytecode", bytecode);
265-
} else if (bytecode != null) {
266-
// runtime code case
267-
jsonOptions.put("bytecode", bytecode.substring(0, bytecode.indexOf("fe")));
268-
}
260+
String BYTECODE_FULLPATH = mnemonicInputFile;
261+
if (mnemonicInputFile == null) {
262+
BYTECODE_FULLPATH = _outputDirPath.resolve(addressSC + ".opcode").toString();
263+
String bytecode;
264+
if (filepath == null) {
265+
bytecode = EVMFrontend.parseContractFromEtherscan(addressSC);
266+
} else {
267+
bytecode = new String(Files.readAllBytes(Paths.get(filepath)));
268+
}
269+
if (useCreationCode) {
270+
jsonOptions.put("bytecode", bytecode);
271+
} else if (bytecode != null) {
272+
// runtime code case
273+
jsonOptions.put("bytecode", bytecode.substring(0, bytecode.indexOf("fe")));
274+
}
269275

270-
EVMFrontend.opcodesFromBytecode(bytecode, BYTECODE_FULLPATH);
276+
EVMFrontend.opcodesFromBytecode(bytecode, BYTECODE_FULLPATH);
277+
}
271278

272279
Program program = EVMFrontend.generateCfgFromFile(BYTECODE_FULLPATH);
273280

@@ -295,50 +302,12 @@ else if (dumpDot)
295302
try {
296303
LiSA lisa = new LiSA(conf);
297304
lisa.run(program);
298-
Set<Statement> soundlySolved = new HashSet<>();
299-
300-
if (linkUnsoundJumpsToAllJumpdestOption) {
301-
int currentIteration = 0;
302-
int MAX_ITER = 5;
303-
boolean fixpoint;
304-
do {
305-
fixpoint = false;
306-
EVMCFG cfg = checker.getComputedCFG();
307-
Set<Statement> jmpdestNodes = cfg.getAllJumpdest();
308-
for (Statement unsoundNode : checker.getUnsoundJumps())
309-
if (!soundlySolved.contains(unsoundNode)) {
310-
fixpoint = true;
311-
for (Statement jmpdest : jmpdestNodes)
312-
cfg.addEdge(new SequentialEdge(unsoundNode, jmpdest));
313-
}
314-
315-
soundlySolved.addAll(checker.getUnsoundJumps());
316-
317-
program.addCodeMember(cfg);
318-
lisa.run(program);
319-
} while (fixpoint && checker.getUnsoundJumps() != null && ++currentIteration < MAX_ITER);
320-
}
305+
Set<Statement> soundlySolved = getSoundlySolvedJumps(checker, lisa, program);
321306

322307
// Print the results
323308
finish = System.currentTimeMillis();
324309

325-
if (ENABLE_REENTRANCY_CHECKER) {
326-
conf.semanticChecks.clear();
327-
conf.semanticChecks.add(new ReentrancyChecker());
328-
lisa.run(program);
329-
330-
jsonOptions.put("re-entrancy-warning",
331-
MyCache.getInstance().getReentrancyWarnings(checker.getComputedCFG().hashCode()));
332-
}
333-
334-
if (ENABLE_TXORIGIN_CHECKER) {
335-
conf.semanticChecks.clear();
336-
conf.semanticChecks.add(new TxOriginChecker());
337-
lisa.run(program);
338-
339-
jsonOptions.put("tx-origin-warning",
340-
MyCache.getInstance().getTxOriginWarnings(checker.getComputedCFG().hashCode()));
341-
}
310+
checkers(conf, lisa, program, checker, jsonOptions);
342311

343312
MyLogger result = EVMLiSA.dumpStatistics(checker, soundlySolved)
344313
.address(addressSC)
@@ -374,6 +343,23 @@ else if (dumpDot)
374343
}
375344
}
376345

346+
/**
347+
* Performs a new analysis for a given smart contract. This method retrieves
348+
* the bytecode (via API requests to Etherscan.io if necessary), generates
349+
* the Control Flow Graph (CFG), configures the analysis parameters,
350+
* executes the analysis, and collects the results.
351+
*
352+
* @param CONTRACT_ADDR the address of the smart contract to analyze.
353+
* @param jsonOptions a {@link JSONObject} containing configuration
354+
* options and parameters for the analysis. The
355+
* options may be updated during the analysis.
356+
*
357+
* @return a {@link MyLogger} instance containing detailed statistics,
358+
* warnings, and execution logs for the analysis.
359+
*
360+
* @throws Exception if any error occurs during directory setup, bytecode
361+
* retrieval, CFG generation, or analysis execution.
362+
*/
377363
private MyLogger newAnalysis(String CONTRACT_ADDR, JSONObject jsonOptions) throws Exception {
378364
Path bytecodeWorkDir = Paths.get(OUTPUT_DIR, "benchmark", "bytecode", CONTRACT_ADDR);
379365
String BYTECODE_WORKDIR = bytecodeWorkDir.toString();
@@ -426,64 +412,110 @@ private MyLogger newAnalysis(String CONTRACT_ADDR, JSONObject jsonOptions) throw
426412
LiSA lisa = new LiSA(conf);
427413
lisa.run(program);
428414

415+
Set<Statement> soundlySolved = getSoundlySolvedJumps(checker, lisa, program);
416+
417+
long finish = System.currentTimeMillis();
418+
419+
checkers(conf, lisa, program, checker, jsonOptions);
420+
421+
return EVMLiSA.dumpStatistics(checker, soundlySolved)
422+
.address(CONTRACT_ADDR)
423+
.time(finish - start)
424+
.timeLostToGetStorage(MyCache.getInstance().getTimeLostToGetStorage(CONTRACT_ADDR))
425+
.buildJson(jsonOptions)
426+
.build();
427+
}
428+
429+
/**
430+
* Computes the set of jumps that are soundly solved by the JumpSolver. This
431+
* method applies an iterative approach to resolve unsound jumps by
432+
* conservatively attaching them to all jump destinations, as per the
433+
* configuration.
434+
*
435+
* @param checker the {@link JumpSolver} instance responsible for resolving
436+
* jumps
437+
* @param lisa the {@link LiSA} instance used to perform static analysis
438+
* @param program the {@link Program} containing the code being analyzed
439+
*
440+
* @return a {@link Set} of {@link Statement} objects representing the
441+
* soundly solved jumps after applying the iterative resolution
442+
* process
443+
*/
444+
Set<Statement> getSoundlySolvedJumps(JumpSolver checker, LiSA lisa, Program program) {
429445
HashSet<Statement> soundlySolved = new HashSet<>();
430446
if (JumpSolver.getLinkUnsoundJumpsToAllJumpdest()) {
431447
int currentIteration = 0;
432-
int MAX_ITER = 5; // We can do MAX_ITER iteration
448+
int MAX_ITER = 5;
433449
boolean fixpoint;
434450
do {
435451
fixpoint = false;
436452
EVMCFG cfg = checker.getComputedCFG();
437-
Set<Statement> jmpdestNodes = cfg.getAllJumpdest();
453+
Set<Statement> jumpdestNodes = cfg.getAllJumpdest();
438454
for (Statement unsoundNode : checker.getUnsoundJumps())
439455
if (!soundlySolved.contains(unsoundNode)) {
440456
fixpoint = true;
441-
for (Statement jmpdest : jmpdestNodes)
442-
cfg.addEdge(new SequentialEdge(unsoundNode, jmpdest));
457+
for (Statement jumpdest : jumpdestNodes)
458+
cfg.addEdge(new SequentialEdge(unsoundNode, jumpdest));
443459
}
444460

445461
soundlySolved.addAll(checker.getUnsoundJumps());
446462

447-
// last run
448463
program.addCodeMember(cfg);
449-
450464
lisa.run(program);
451465
} while (fixpoint && checker.getUnsoundJumps() != null && ++currentIteration < MAX_ITER);
452466
}
467+
return soundlySolved;
468+
}
453469

454-
// Print the results
455-
long finish = System.currentTimeMillis();
456-
470+
/**
471+
* Executes the specified semantic checkers on the provided program and
472+
* configuration, updating the JSON options with warnings generated by the
473+
* analysis. This method dynamically adds and runs semantic checks based on
474+
* the enabled configuration flags.
475+
*
476+
* @param conf the {@link LiSAConfiguration} used for static analysis
477+
* @param lisa the {@link LiSA} instance performing the analysis
478+
* @param program the {@link Program} representing the analyzed code
479+
* @param checker the {@link JumpSolver} providing CFG information for
480+
* the analysis
481+
* @param jsonOptions the {@link JSONObject} where the results of the
482+
* analysis are stored
483+
*/
484+
void checkers(LiSAConfiguration conf, LiSA lisa, Program program, JumpSolver checker, JSONObject jsonOptions) {
457485
if (ENABLE_REENTRANCY_CHECKER) {
486+
// Clear existing checks and add the ReentrancyChecker
458487
conf.semanticChecks.clear();
459488
conf.semanticChecks.add(new ReentrancyChecker());
460489
lisa.run(program);
461490

491+
// Store re-entrancy warnings in the JSON options
462492
jsonOptions.put("re-entrancy-warning",
463493
MyCache.getInstance().getReentrancyWarnings(checker.getComputedCFG().hashCode()));
464494
}
465495

466496
if (ENABLE_TXORIGIN_CHECKER) {
497+
// Clear existing checks and add the TxOriginChecker
467498
conf.semanticChecks.clear();
468499
conf.semanticChecks.add(new TxOriginChecker());
469500
lisa.run(program);
470501

502+
// Store tx-origin warnings in the JSON options
471503
jsonOptions.put("tx-origin-warning",
472504
MyCache.getInstance().getTxOriginWarnings(checker.getComputedCFG().hashCode()));
473505
}
474-
475-
return EVMLiSA.dumpStatistics(checker, soundlySolved)
476-
.address(CONTRACT_ADDR)
477-
.time(finish - start)
478-
.timeLostToGetStorage(MyCache.getInstance().getTimeLostToGetStorage(CONTRACT_ADDR))
479-
.buildJson(jsonOptions)
480-
.build();
481506
}
482507

483508
/**
484-
* Runs the benchmark for analyzing smart contracts.
509+
* Executes the benchmark for a set of smart contracts. This method handles
510+
* the parallel execution of analyses on the smart contracts, collects the
511+
* results, and logs relevant information, including statistics and
512+
* execution logs.
485513
*
486-
* @throws Exception if an error occurs during the benchmark execution.
514+
* @param jsonOptions a {@link JSONObject} containing configuration options
515+
* and parameters for the benchmark execution.
516+
*
517+
* @throws Exception if an error occurs during the benchmark execution or
518+
* analysis.
487519
*/
488520
private void runBenchmark(JSONObject jsonOptions) throws Exception {
489521
List<String> smartContracts = readSmartContractsFromFile(SMARTCONTRACTS_FULLPATH);
@@ -599,14 +631,19 @@ public void run() {
599631
}
600632

601633
/**
602-
* Calculates and prints statistics about the control flow graph (CFG) of
603-
* the provided EVMCFG object.
634+
* Dumps statistics related to jump resolution within a CFG (Control Flow
635+
* Graph). This method calculates and logs various statistics, such as
636+
* resolved jumps, unreachable jumps, unsound jumps, and more, based on the
637+
* analysis performed by the {@link JumpSolver}.
604638
*
605-
* @param checker The control flow graph (CFG) of the Ethereum Virtual
606-
* Machine (EVM) bytecode.
639+
* @param checker the {@link JumpSolver} instance used to analyze the
640+
* CFG and compute jump-related information.
641+
* @param soundlySolved a set of {@link Statement} objects representing
642+
* jumps that were soundly solved in the CFG.
607643
*
608-
* @return A Triple containing the counts of precisely resolved jumps, sound
609-
* resolved jumps, and unreachable jumps.
644+
* @return a {@link MyLogger} instance containing the computed statistics
645+
* for logging or further analysis; returns {@code null} if no
646+
* entry points are found in the CFG.
610647
*/
611648
public static MyLogger dumpStatistics(JumpSolver checker, Set<Statement> soundlySolved) {
612649
EVMCFG cfg = checker.getComputedCFG();
@@ -952,6 +989,13 @@ private Options getOptions() {
952989
.hasArg(true)
953990
.build();
954991

992+
Option filePathMnemonicOption = Option.builder()
993+
.longOpt("filepath-mnemonic")
994+
.desc("Filepath of the mnemonic file.")
995+
.required(false)
996+
.hasArg(true)
997+
.build();
998+
955999
Option stackSizeOption = Option.builder()
9561000
.longOpt("stack-size")
9571001
.desc("Dimension of stack (default: 32).")
@@ -1045,14 +1089,14 @@ private Options getOptions() {
10451089
.build();
10461090

10471091
Option enableReentrancyCheckerOption = Option.builder()
1048-
.longOpt("reentrancy-checker")
1092+
.longOpt("checker-reentrancy")
10491093
.desc("Enable re-entrancy checker.")
10501094
.required(false)
10511095
.hasArg(false)
10521096
.build();
10531097

10541098
Option enableTxOriginCheckerOption = Option.builder()
1055-
.longOpt("txorigin-checker")
1099+
.longOpt("checker-txorigin")
10561100
.desc("Enable tx-origin checker.")
10571101
.required(false)
10581102
.hasArg(false)
@@ -1061,6 +1105,7 @@ private Options getOptions() {
10611105
options.addOption(addressOption);
10621106
options.addOption(outputOption);
10631107
options.addOption(filePathOption);
1108+
options.addOption(filePathMnemonicOption);
10641109
options.addOption(stackSizeOption);
10651110
options.addOption(stackSetSizeOption);
10661111
options.addOption(benchmarkOption);

0 commit comments

Comments
 (0)