Skip to content

Commit

Permalink
First look at TimestampDependencyChecker
Browse files Browse the repository at this point in the history
  • Loading branch information
denisguareschi committed Jan 9, 2025
1 parent 75a20d7 commit 1cd7d05
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 3 deletions.
26 changes: 24 additions & 2 deletions src/main/java/it/unipr/cfg/EVMCFG.java
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ public class EVMCFG extends CFG {
public Set<Statement> jumpNodes;
public Set<Statement> pushedJumps;
public Set<Statement> sstores;
public Set<Statement> sha3s;

public EVMCFG(CodeMemberDescriptor descriptor, Collection<Statement> entrypoints,
NodeList<CFG, Statement, Edge> list) {
Expand All @@ -54,7 +55,7 @@ public EVMCFG(CodeMemberDescriptor cfgDesc) {
/**
* Returns a set of all the SSTORE statements in the CFG. SSTORE
*
* @return a set of all the JUMPDEST statements in the CFG
* @return a set of all the SSTORE statements in the CFG
*/
public Set<Statement> getAllSstore() {
if (sstores == null) {
Expand All @@ -72,6 +73,28 @@ public Set<Statement> getAllSstore() {

return sstores;
}

/**
* Returns a set of all the SHA3 statements in the CFG. SHA3
*
* @return a set of all the SHA3 statements in the CFG
*/
public Set<Statement> getAllSha3() {
if (sha3s == null) {
NodeList<CFG, Statement, Edge> cfgNodeList = this.getNodeList();
Set<Statement> sha3s = new HashSet<>();

for (Statement statement : cfgNodeList.getNodes()) {
if (statement instanceof Sha3) {
sha3s.add(statement);
}
}

return this.sha3s = sha3s;
}

return sha3s;
}

/**
* Returns a set of all the JUMPDEST statements in the CFG.
Expand Down Expand Up @@ -321,5 +344,4 @@ private boolean dfsSequential(Statement start, Statement target, Set<Statement>

return false;
}

}
23 changes: 22 additions & 1 deletion src/main/java/it/unipr/checker/TimestampDependencyChecker.java
Original file line number Diff line number Diff line change
@@ -1,6 +1,13 @@
package it.unipr.checker;

import java.util.Set;

import it.unipr.analysis.taint.TaintAbstractDomain;
import it.unipr.cfg.Balance;
import it.unipr.cfg.Blockhash;
import it.unipr.cfg.Difficulty;
import it.unipr.cfg.EVMCFG;
import it.unipr.cfg.Timestamp;
import it.unive.lisa.analysis.SimpleAbstractState;
import it.unive.lisa.analysis.heap.MonolithicHeap;
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
Expand All @@ -26,7 +33,21 @@ public boolean visit(
CheckToolWithAnalysisResults<
SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool,
CFG graph, Statement node) {
// TODO Auto-generated method stub

if (node instanceof Timestamp || node instanceof Blockhash || node instanceof Difficulty || node instanceof Balance) {
EVMCFG cfg = ((EVMCFG) graph);
Set<Statement> nsh = cfg.getAllSha3();
Set<Statement> ns = cfg.getAllSstore();
// The function cfg.getAllJumps() returns all jumps, whether being jump or jumpi
// if you want to separete the jumps, a different function need to be done
Set<Statement> nj = cfg.getAllJumps();


}




return SemanticCheck.super.visit(tool, graph, node);
}

Expand Down

0 comments on commit 1cd7d05

Please sign in to comment.