From 3e40c4827dd1b0cf246cdf9c14fbe489d0229a35 Mon Sep 17 00:00:00 2001 From: 0xMere Date: Fri, 1 Mar 2024 22:11:39 +0100 Subject: [PATCH] Optimization: Added Number class --- src/main/java/it/unipr/EVMLiSA.java | 1 + .../it/unipr/analysis/EVMAbstractState.java | 66 ++++--- .../java/it/unipr/analysis/KIntegerSet.java | 165 ++++++++-------- src/main/java/it/unipr/analysis/Memory.java | 7 +- src/main/java/it/unipr/analysis/MyLogger.java | 9 +- src/main/java/it/unipr/analysis/Number.java | 183 ++++++++++++++++++ src/main/java/it/unipr/cfg/EVMCFG.java | 54 +++--- src/main/java/it/unipr/cfg/Jumpi.java | 18 +- .../java/it/unipr/checker/JumpSolver.java | 52 ++--- 9 files changed, 372 insertions(+), 183 deletions(-) create mode 100644 src/main/java/it/unipr/analysis/Number.java diff --git a/src/main/java/it/unipr/EVMLiSA.java b/src/main/java/it/unipr/EVMLiSA.java index 1714bf480..69fee9c7b 100644 --- a/src/main/java/it/unipr/EVMLiSA.java +++ b/src/main/java/it/unipr/EVMLiSA.java @@ -493,6 +493,7 @@ public void run() { int extra = 120000; long blocks = smartContracts.size() / CORES * 20000; long timeToWait = smartContracts.size() * millisPerSmartContract + extra + blocks; + timeToWait = timeToWait * 10; // Statistics long minutes = (timeToWait / 1000) / 60; diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java index 027e2f24b..dc9864c7e 100644 --- a/src/main/java/it/unipr/analysis/EVMAbstractState.java +++ b/src/main/java/it/unipr/analysis/EVMAbstractState.java @@ -1,15 +1,5 @@ package it.unipr.analysis; -import java.math.BigInteger; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.List; -import java.util.Objects; -import java.util.Set; -import java.util.function.Predicate; - -import org.apache.commons.lang3.tuple.Pair; - import it.unipr.analysis.operator.JumpiOperator; import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; @@ -27,6 +17,14 @@ import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.symbolic.value.operator.unary.LogicalNegation; import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; +import java.math.BigInteger; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; +import org.apache.commons.lang3.tuple.Pair; public class EVMAbstractState implements ValueDomain, BaseLattice { @@ -34,7 +32,7 @@ public class EVMAbstractState implements ValueDomain, BaseLatt private static final EVMAbstractState BOTTOM = new EVMAbstractState(new AbstractStackSet().bottom(), new Memory().bottom(), KIntegerSet.BOTTOM); private final boolean isTop; - + /** * The address of the running contract. */ @@ -69,7 +67,7 @@ private EVMAbstractState(boolean isTop, String contractAddress) { this.stacks = new AbstractStackSet(); this.memory = new Memory(); this.mu_i = KIntegerSet.ZERO; - + CONTRACT_ADDRESS = contractAddress; } @@ -153,7 +151,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } case "PushOperator": { // PUSH AbstractStackSet result = new AbstractStackSet(new HashSet<>(stacks.size()), false); - KIntegerSet toPush = new KIntegerSet(this.toBigDecimal(un.getExpression())); + KIntegerSet toPush = new KIntegerSet(toBigInteger(un.getExpression())); for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); @@ -165,8 +163,8 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } case "AddressOperator": { // ADDRESS AbstractStackSet result = new AbstractStackSet(new HashSet<>(stacks.size()), false); - KIntegerSet hex = new KIntegerSet(toBigDecimal(CONTRACT_ADDRESS)); - + KIntegerSet hex = new KIntegerSet(toBigInteger(CONTRACT_ADDRESS)); + for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); resultStack.push(hex); @@ -728,10 +726,10 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo if (target.isTop() || indexOfByte.isTop()) { resultStack.push(KIntegerSet.NUMERIC_TOP); } else { - for (BigInteger value : target) { + for (Number value : target) { byte[] valueAsByteArray = value.toByteArray(); - for (BigInteger index : indexOfByte) { + for (Number index : indexOfByte) { int intIndex = index.intValue(); if (intIndex <= 0 || intIndex >= valueAsByteArray.length) { @@ -992,9 +990,9 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } else { KIntegerSet current_mu_i_lub = KIntegerSet.BOTTOM; - for (BigInteger os : offset) { - BigInteger thirtyTwo = BigInteger.valueOf(32); - BigInteger current_mu_i = os.add(thirtyTwo) + for (Number os : offset) { + Number thirtyTwo = new Number(32); + Number current_mu_i = os.add(thirtyTwo) .divide(thirtyTwo); memoryResult = memory.putState(os, value); @@ -1026,11 +1024,11 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } else { KIntegerSet current_mu_i_lub = KIntegerSet.BOTTOM; - for (BigInteger os : offset) { - BigInteger current_mu_i = os.add(BigInteger.valueOf(1)) - .divide(BigInteger.valueOf(32)); + for (Number os : offset) { + Number current_mu_i = os.add(new Number(1)) + .divide(new Number(32)); - memoryResult = memory.putState(os, value.mod(new KIntegerSet(BigInteger.valueOf(256)))); + memoryResult = memory.putState(os, value.mod(new KIntegerSet(new Number(256)))); current_mu_i_lub = current_mu_i_lub.lub(new KIntegerSet(current_mu_i)); } @@ -1721,9 +1719,10 @@ public EVMAbstractState assume(ValueExpression expression, ProgramPoint src, Pro UnaryOperator op = un.getOperator(); if (op instanceof JumpiOperator) { // JUMPI - + @SuppressWarnings("unchecked") - Pair, Set> split = ((Pair, Set>) ((Constant) un.getExpression()).getValue()); + Pair, Set> split = ((Pair, + Set>) ((Constant) un.getExpression()).getValue()); if (split.getLeft().isEmpty() && split.getRight().isEmpty()) return top(); else if (split.getLeft().isEmpty()) @@ -1741,7 +1740,10 @@ else if (split.getLeft().isEmpty()) if (wrappedOperator instanceof JumpiOperator) { // !JUMPI @SuppressWarnings("unchecked") - Pair, Set> split = ((Pair, Set>) ((Constant) ((UnaryExpression) wrappedExpr).getExpression()).getValue()); + Pair, + Set> split = ((Pair, Set< + AbstractStack>>) ((Constant) ((UnaryExpression) wrappedExpr).getExpression()) + .getValue()); if (split.getLeft().isEmpty() && split.getRight().isEmpty()) return top(); else if (split.getRight().isEmpty()) @@ -1823,17 +1825,17 @@ public boolean isBottom() { * * @return the BigInteger corresponding to the memory word */ - private BigInteger toBigDecimal(SymbolicExpression expression) { + private Number toBigInteger(SymbolicExpression expression) { Constant c = (Constant) expression; String hex = (String) c.getValue(); - return toBigDecimal(hex); + return toBigInteger(hex); } - - private BigInteger toBigDecimal(String str) { + + private Number toBigInteger(String str) { String hexadecimal = str.substring(2); BigInteger bigIntVal = new BigInteger(hexadecimal, 16); // BigDecimal bigDecimalVal = new BigDecimal(bigIntVal); - return bigIntVal; + return new Number(bigIntVal); } @Override diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java index 25315df11..3373b974c 100644 --- a/src/main/java/it/unipr/analysis/KIntegerSet.java +++ b/src/main/java/it/unipr/analysis/KIntegerSet.java @@ -7,10 +7,10 @@ import java.util.HashSet; import java.util.Set; -public class KIntegerSet extends SetLattice { - private static final BigInteger ZERO_INT = BigInteger.valueOf(0); - private static final BigInteger ONE_INT = BigInteger.valueOf(1); - private static final BigInteger MAX = BigInteger.valueOf((long) Math.pow(2, 256)); +public class KIntegerSet extends SetLattice { + private static final Number ZERO_INT = new Number(0); + private static final Number ONE_INT = new Number(1); + private static final Number MAX = new Number((long) Math.pow(2, 256)); public static final int K = 1; @@ -22,7 +22,7 @@ public class KIntegerSet extends SetLattice { public static final KIntegerSet NOT_JUMPDEST_TOP = new KIntegerSet(7); public static final KIntegerSet BOTTOM = new KIntegerSet(Collections.emptySet(), false); - public KIntegerSet(BigInteger i) { + public KIntegerSet(Number i) { this(Collections.singleton(i), false); } @@ -35,14 +35,18 @@ public KIntegerSet(Integer... ints) { if (ints.length <= K) for (Integer i : ints) - this.elements.add(BigInteger.valueOf(i)); + this.elements.add(new Number(i)); + } + + public KIntegerSet(BigInteger i) { + this(new Number(i)); } - public KIntegerSet(Set set) { + public KIntegerSet(Set set) { this(set.size() > K ? Collections.emptySet() : set, set.size() > K); } - public KIntegerSet(Set elements, boolean isTop) { + public KIntegerSet(Set elements, boolean isTop) { super(elements, isTop); } @@ -55,7 +59,7 @@ public KIntegerSet top() { public KIntegerSet bottom() { return BOTTOM; } - + @Override public boolean isBottom() { return elements != null && super.isBottom(); @@ -66,7 +70,6 @@ public boolean isTop() { return elements != null && super.isTop(); } - @Override public KIntegerSet lubAux(KIntegerSet other) throws SemanticException { if (isTopNotJumpdest()) @@ -89,7 +92,7 @@ public KIntegerSet glbAux(KIntegerSet other) throws SemanticException { } @Override - public KIntegerSet mk(Set set) { + public KIntegerSet mk(Set set) { return new KIntegerSet(set); } @@ -108,7 +111,7 @@ public boolean equals(Object obj) { return false; return true; } - + public KIntegerSet isZero() { if (isBottom()) return bottom(); @@ -131,10 +134,10 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) { - BigInteger add = i.add(j); + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) { + Number add = i.add(j); if (add.compareTo(MAX) >= 0) add = add.subtract(MAX); elements.add(add); @@ -150,11 +153,11 @@ else if (isTop() || other.isTop()) return top(); else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) { - BigInteger sub = i.subtract(j); + + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) { + Number sub = i.subtract(j); if (sub.compareTo(ZERO_INT) < 0) sub = sub.add(MAX); elements.add(sub); @@ -172,11 +175,11 @@ else if (isTop() || other.isTop()) return top(); else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) { - BigInteger mul = i.multiply(j); + + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) { + Number mul = i.multiply(j); if (mul.compareTo(ZERO_INT) < 0) mul = mul.add(MAX); if (mul.compareTo(MAX) > 0) @@ -196,9 +199,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) if (j.equals(ZERO_INT)) elements.add(ZERO_INT); else @@ -217,9 +220,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) { + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) { if (j.equals(ZERO_INT)) elements.add(i); @@ -237,11 +240,11 @@ else if (isTop() || other.isTop() || that.isTop()) return top(); else if (isTopNotJumpdest() || other.isTopNotJumpdest() || that.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : that.elements) - for (BigInteger k : other.elements) + + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : that.elements) + for (Number k : other.elements) if (k.equals(ZERO_INT)) elements.add(ZERO_INT); else @@ -257,11 +260,11 @@ else if (isTop() || other.isTop() || that.isTop()) return top(); else if (isTopNotJumpdest() || other.isTopNotJumpdest() || that.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : that.elements) - for (BigInteger k : other.elements) + + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : that.elements) + for (Number k : other.elements) if (k.equals(ZERO_INT)) elements.add(ZERO_INT); else @@ -277,13 +280,13 @@ else if (isTop() || other.isTop()) return top(); else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) { - for (BigInteger j : other.elements) { - BigInteger r = i; - for (int k = 0; j.compareTo(BigInteger.valueOf(k)) > 0; k++) + Set elements = new HashSet<>(K); + for (Number i : this.elements) { + for (Number j : other.elements) { + Number r = i; + + for (int k = 0; j.compareTo(new Number(k)) > 0; k++) if (r.compareTo(MAX) > 0) return NUMERIC_TOP; else @@ -302,10 +305,10 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - + Set r = new HashSet(); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + for (Number i : this.elements) + for (Number j : other.elements) r.add(i.compareTo(j) < 0); if (r.size() == 2) @@ -323,10 +326,10 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - + Set r = new HashSet(); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + for (Number i : this.elements) + for (Number j : other.elements) r.add(i.compareTo(j) > 0); if (r.size() == 2) @@ -344,10 +347,10 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - + Set r = new HashSet(); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + for (Number i : this.elements) + for (Number j : other.elements) r.add(i.compareTo(j) == 0); if (r.size() == 2) @@ -368,9 +371,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) elements.add(i.and(j)); return new KIntegerSet(elements); @@ -384,9 +387,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) elements.add(i.or(j)); return new KIntegerSet(elements); @@ -400,9 +403,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) elements.add(i.xor(j)); return new KIntegerSet(elements); @@ -416,8 +419,8 @@ else if (isTop()) else if (isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) if (i.compareTo(ZERO_INT) >= 0) elements.add(MAX.subtract(i.add(ONE_INT))); else @@ -434,10 +437,10 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) - elements.add(new BigInteger(shiftLeft(j.toByteArray(), i.intValue()))); + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) + elements.add(new Number(new BigInteger(shiftLeft(j.toByteArray(), i.intValue())))); return new KIntegerSet(elements); } @@ -450,9 +453,9 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) elements.add(j.shiftRight(i.intValue())); return new KIntegerSet(elements); @@ -466,11 +469,11 @@ else if (isTop() || other.isTop()) else if (isTopNotJumpdest() || other.isTopNotJumpdest()) return NOT_JUMPDEST_TOP; - Set elements = new HashSet<>(K); - for (BigInteger i : this.elements) - for (BigInteger j : other.elements) + Set elements = new HashSet<>(K); + for (Number i : this.elements) + for (Number j : other.elements) elements.add( - new BigInteger(shiftArithmeticRight(j.toByteArray(), i.intValue()))); + new Number(new BigInteger(shiftArithmeticRight(j.toByteArray(), i.intValue())))); return new KIntegerSet(elements); } @@ -485,7 +488,7 @@ else if (isTopNotJumpdest()) KIntegerSet r = KIntegerSet.BOTTOM; - for (BigInteger i : this.elements) { + for (Number i : this.elements) { KIntegerSet state = memory.getState(i); if (state.isBottom()) r = r.lub(KIntegerSet.NUMERIC_TOP); @@ -689,7 +692,7 @@ public boolean isDefinitelyFalse() { public boolean isUnknown() { return isTop() || isTopNotJumpdest() || (!isBottom() && !isDefinitelyFalse() && !isDefinitelyTrue()); } - + public boolean isTopNotJumpdest() { return this == NOT_JUMPDEST_TOP; } diff --git a/src/main/java/it/unipr/analysis/Memory.java b/src/main/java/it/unipr/analysis/Memory.java index 5b6cf5ec7..a041f6fc5 100644 --- a/src/main/java/it/unipr/analysis/Memory.java +++ b/src/main/java/it/unipr/analysis/Memory.java @@ -1,11 +1,10 @@ package it.unipr.analysis; import it.unive.lisa.analysis.lattices.FunctionalLattice; -import java.math.BigInteger; import java.util.HashMap; import java.util.Map; -public class Memory extends FunctionalLattice { +public class Memory extends FunctionalLattice { /** * Default constructor for Memory. Initializes the Memory with a default @@ -33,7 +32,7 @@ public Memory(KIntegerSet lattice) { * @param function The initial function (mapping of addresses to Intervals) * for the Memory. */ - public Memory(KIntegerSet lattice, Map function) { + public Memory(KIntegerSet lattice, Map function) { super(lattice, function); } @@ -48,7 +47,7 @@ public Memory bottom() { } @Override - public Memory mk(KIntegerSet lattice, Map function) { + public Memory mk(KIntegerSet lattice, Map function) { return new Memory(lattice, function); } diff --git a/src/main/java/it/unipr/analysis/MyLogger.java b/src/main/java/it/unipr/analysis/MyLogger.java index 9ec6180f5..9e62c7cf5 100644 --- a/src/main/java/it/unipr/analysis/MyLogger.java +++ b/src/main/java/it/unipr/analysis/MyLogger.java @@ -40,7 +40,8 @@ private MyLogger() { private MyLogger(String address, int opcodes, int jumps, int preciselyResolvedJumps, int soundResolvedJumps, int definitelyUnreachableJumps, int maybeUnreachableJumps, int totalResolvedJumps, - int notSolvedJumps, int unsoundJumps, int maybeUnsoundJumps, double solvedJumpsPercent, long time, String notes) { + int notSolvedJumps, int unsoundJumps, int maybeUnsoundJumps, double solvedJumpsPercent, long time, + String notes) { this.address = address; this.opcodes = opcodes; this.jumps = jumps; @@ -109,12 +110,12 @@ public MyLogger notSolvedJumps(int notSolvedJumps) { this.notSolvedJumps = notSolvedJumps; return this; } - + public MyLogger unsoundJumps(int unsoundJumps) { this.unsoundJumps = unsoundJumps; return this; } - + public MyLogger maybeUnsoundJumps(int maybeUnsoundJumps) { this.maybeUnsoundJumps = maybeUnsoundJumps; return this; @@ -138,7 +139,7 @@ public MyLogger notes(String notes) { public MyLogger build() { return new MyLogger(address, opcodes, jumps, preciselyResolvedJumps, soundResolvedJumps, definitelyUnreachableJumps, maybeUnreachableJumps, totalResolvedJumps, notSolvedJumps, - unsoundJumps, maybeUnsoundJumps,solvedJumpsPercent, time, notes); + unsoundJumps, maybeUnsoundJumps, solvedJumpsPercent, time, notes); } public int jumpSize() { diff --git a/src/main/java/it/unipr/analysis/Number.java b/src/main/java/it/unipr/analysis/Number.java new file mode 100644 index 000000000..f6b31e151 --- /dev/null +++ b/src/main/java/it/unipr/analysis/Number.java @@ -0,0 +1,183 @@ +package it.unipr.analysis; + +import java.math.BigInteger; +import java.util.Objects; + +public class Number implements Comparable { + public static final BigInteger MAX_INT = BigInteger.valueOf((long) Math.pow(2, 32)); + public static final BigInteger MAX_LONG = BigInteger.valueOf((long) Math.pow(2, 64)); + + static enum Type { + INT, + LONG, + BIGINTEGER + } + + private int i = -1; + private long l = -1; + private BigInteger b; + + public Number(int other) { + this.i = other; + this.b = null; + } + + public Number(long other) { + this.l = other; + this.b = null; + } + + public Number(BigInteger other) { + if (other.compareTo(MAX_INT) < 0) + this.i = other.intValue(); + else if (other.compareTo(MAX_LONG) < 0) + this.l = other.longValue(); + else + this.b = other; + } + + public Type getType() { + if (b != null) + return Type.BIGINTEGER; + if (i != -1) + return Type.INT; + return Type.LONG; + } + + public int getInt() { + return i; + } + + public long getLong() { + return l; + } + + public BigInteger getBigInteger() { + return b; + } + + public BigInteger toBigInteger(Number other) { + BigInteger ot; + if (other.getType() == Type.INT) + ot = BigInteger.valueOf(other.getInt()); + else if (other.getType() == Type.LONG) + ot = BigInteger.valueOf(other.getLong()); + else + ot = other.getBigInteger(); + + return ot; + } + + public Number add(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.add(ot)); + } + + public Number subtract(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.subtract(ot)); + } + + public Number multiply(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.multiply(ot)); + } + + public Number divide(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.divide(ot)); + } + + public Number and(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.and(ot)); + } + + public Number or(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.or(ot)); + } + + public Number xor(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return new Number(me.xor(ot)); + } + + public Number not() { + BigInteger me = toBigInteger(this); + + return new Number(me.not()); + } + + public byte[] toByteArray() { + BigInteger me = toBigInteger(this); + + return me.toByteArray(); + } + + public Number shiftRight(int other) { + BigInteger me = toBigInteger(this); + + return new Number(me.shiftRight(other)); + } + + public Number shiftLeft(int other) { + BigInteger me = toBigInteger(this); + + return new Number(me.shiftLeft(other)); + } + + public int intValue() { + BigInteger me = toBigInteger(this); + + return me.intValue(); + } + + @Override + public String toString() { + if (b != null) + return b.toString(); + if (i != -1) + return i + ""; + return l + ""; + } + + @Override + public int compareTo(Number other) { + BigInteger me = toBigInteger(this); + BigInteger ot = toBigInteger(other); + + return me.compareTo(ot); + } + + @Override + public int hashCode() { + return Objects.hash(b, i, l); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Number other = (Number) obj; + return Objects.equals(b, other.b) && i == other.i && l == other.l; + } +} diff --git a/src/main/java/it/unipr/cfg/EVMCFG.java b/src/main/java/it/unipr/cfg/EVMCFG.java index 77826a23a..e1dfae918 100644 --- a/src/main/java/it/unipr/cfg/EVMCFG.java +++ b/src/main/java/it/unipr/cfg/EVMCFG.java @@ -1,12 +1,5 @@ package it.unipr.cfg; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Map; -import java.util.Map.Entry; -import java.util.Set; - import it.unipr.cfg.push.Push; import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; @@ -33,6 +26,12 @@ import it.unive.lisa.util.datastructures.graph.algorithms.Fixpoint; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import it.unive.lisa.util.datastructures.graph.code.NodeList; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; public class EVMCFG extends CFG { @@ -107,31 +106,32 @@ public int getOpcodeCount() { public Set getAllPushedJumps() { if (pushedJumps == null) { NodeList cfgNodeList = this.getNodeList(); - pushedJumps = new HashSet<>(); + pushedJumps = new HashSet<>(); - for (Edge edge : cfgNodeList.getEdges()) - if ((edge.getDestination() instanceof Jump || edge.getDestination() instanceof Jumpi) && (edge.getSource() instanceof Push)) + for (Edge edge : cfgNodeList.getEdges()) + if ((edge.getDestination() instanceof Jump || edge.getDestination() instanceof Jumpi) + && (edge.getSource() instanceof Push)) pushedJumps.add(edge.getDestination()); } - + return pushedJumps; } public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalyzedCFG fixpoint( - AnalysisState singleton, Map> startingPoints, - InterproceduralAnalysis interprocedural, WorkingSet ws, - FixpointConfiguration conf, - ScopeId id) throws FixpointException { + H extends HeapDomain, + V extends ValueDomain, + T extends TypeDomain> AnalyzedCFG fixpoint( + AnalysisState singleton, Map> startingPoints, + InterproceduralAnalysis interprocedural, WorkingSet ws, + FixpointConfiguration conf, + ScopeId id) throws FixpointException { // we disable optimizations for ascending phases if there is a // descending one: the latter will need full results to start applying // glbs/narrowings from a post-fixpoint boolean isOptimized = conf.optimize && conf.descendingPhaseType == DescendingPhaseType.NONE; Fixpoint> fix = isOptimized ? new OptimizedFixpoint<>(this, false, conf.hotspots) - : new Fixpoint<>(this, false); + : new Fixpoint<>(this, false); EVMAscendingFixpoint asc = new EVMAscendingFixpoint(this, interprocedural, conf.wideningThreshold); @@ -166,13 +166,13 @@ T extends TypeDomain> AnalyzedCFG fixpoint( } private , - T extends TypeDomain, - A extends AbstractState, - H extends HeapDomain> AnalyzedCFG flatten( - boolean isOptimized, AnalysisState singleton, - Map> startingPoints, - InterproceduralAnalysis interprocedural, ScopeId id, - Map> fixpointResults) { + T extends TypeDomain, + A extends AbstractState, + H extends HeapDomain> AnalyzedCFG flatten( + boolean isOptimized, AnalysisState singleton, + Map> startingPoints, + InterproceduralAnalysis interprocedural, ScopeId id, + Map> fixpointResults) { Map> finalResults = new HashMap<>(fixpointResults.size()); for (Entry> e : fixpointResults.entrySet()) { finalResults.put(e.getKey(), e.getValue().postState); @@ -183,7 +183,7 @@ H extends HeapDomain> AnalyzedCFG flatten( return isOptimized ? new OptimizedAnalyzedCFG(this, id, singleton, startingPoints, finalResults, interprocedural) - : new AnalyzedCFG<>(this, id, singleton, startingPoints, finalResults); + : new AnalyzedCFG<>(this, id, singleton, startingPoints, finalResults); } @Override diff --git a/src/main/java/it/unipr/cfg/Jumpi.java b/src/main/java/it/unipr/cfg/Jumpi.java index 71b1ea0c3..f50866cb0 100644 --- a/src/main/java/it/unipr/cfg/Jumpi.java +++ b/src/main/java/it/unipr/cfg/Jumpi.java @@ -1,10 +1,5 @@ package it.unipr.cfg; -import java.util.HashSet; -import java.util.Set; - -import org.apache.commons.lang3.tuple.Pair; - import it.unipr.analysis.AbstractStack; import it.unipr.analysis.EVMAbstractState; import it.unipr.analysis.KIntegerSet; @@ -24,6 +19,9 @@ import it.unive.lisa.symbolic.value.Constant; import it.unive.lisa.type.Untyped; import it.unive.lisa.util.datastructures.graph.GraphVisitor; +import java.util.HashSet; +import java.util.Set; +import org.apache.commons.lang3.tuple.Pair; /** * Jumpi opcode of the program to analyze. @@ -58,11 +56,11 @@ public String toString() { @Override public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, InterproceduralAnalysis interprocedural, - StatementStore expressions) throws SemanticException { + H extends HeapDomain, + V extends ValueDomain, + T extends TypeDomain> AnalysisState semantics( + AnalysisState entryState, InterproceduralAnalysis interprocedural, + StatementStore expressions) throws SemanticException { EVMAbstractState valueState = entryState.getDomainInstance(EVMAbstractState.class); // Split here diff --git a/src/main/java/it/unipr/checker/JumpSolver.java b/src/main/java/it/unipr/checker/JumpSolver.java index a203e6a97..9b2d2ec1f 100644 --- a/src/main/java/it/unipr/checker/JumpSolver.java +++ b/src/main/java/it/unipr/checker/JumpSolver.java @@ -1,12 +1,8 @@ package it.unipr.checker; -import java.math.BigInteger; -import java.util.HashSet; -import java.util.Set; -import java.util.stream.Collectors; - import it.unipr.analysis.EVMAbstractState; import it.unipr.analysis.KIntegerSet; +import it.unipr.analysis.Number; import it.unipr.cfg.EVMCFG; import it.unipr.cfg.Jump; import it.unipr.cfg.Jumpi; @@ -30,14 +26,17 @@ import it.unive.lisa.program.cfg.edge.SequentialEdge; import it.unive.lisa.program.cfg.edge.TrueEdge; import it.unive.lisa.program.cfg.statement.Statement; +import java.util.HashSet; +import java.util.Set; +import java.util.stream.Collectors; /** * A semantic checker that aims at solving JUMP and JUMPI destinations by * filtering all the possible destinations and adding the missing edges. */ public class JumpSolver -implements SemanticCheck>, -MonolithicHeap, EVMAbstractState, TypeEnvironment> { + implements SemanticCheck>, + MonolithicHeap, EVMAbstractState, TypeEnvironment> { /** * The CFG to be analyzed. @@ -60,12 +59,14 @@ public class JumpSolver private Set unreachableJumps; /** - * The set of definitely unsound jumps (i.e., jumps reached by stacks with top at the top) + * The set of definitely unsound jumps (i.e., jumps reached by stacks with + * top at the top) */ private Set unsoundJumps; /** - * The set of maybe unsound jumps (i.e., jumps reached by the top abstract state) + * The set of maybe unsound jumps (i.e., jumps reached by the top abstract + * state) */ private Set maybeUnsoundJumps; @@ -81,11 +82,11 @@ public EVMCFG getComputedCFG() { public Set getUnreachableJumps() { return unreachableJumps; } - + public Set getUnsoundJumps() { return unsoundJumps; } - + public Set getMaybeUnsoundJumps() { return maybeUnsoundJumps; } @@ -93,8 +94,8 @@ public Set getMaybeUnsoundJumps() { @Override public void beforeExecution( CheckToolWithAnalysisResults< - SimpleAbstractState>, - MonolithicHeap, EVMAbstractState, TypeEnvironment> tool) { + SimpleAbstractState>, + MonolithicHeap, EVMAbstractState, TypeEnvironment> tool) { // resets the unreachable jumps set this.unreachableJumps = new HashSet<>(); } @@ -108,9 +109,9 @@ public void beforeExecution( @Override public void afterExecution( CheckToolWithAnalysisResults< - SimpleAbstractState>, - MonolithicHeap, - EVMAbstractState, TypeEnvironment> tool) { + SimpleAbstractState>, + MonolithicHeap, + EVMAbstractState, TypeEnvironment> tool) { if (fixpoint) { Statement entryPoint = cfgToAnalyze.getEntrypoints().stream().findAny().get(); @@ -128,7 +129,7 @@ public void afterExecution( EVMAbstractState, TypeEnvironment> result : tool.getResultOf(this.cfgToAnalyze)) { AnalysisState>, - MonolithicHeap, EVMAbstractState, TypeEnvironment> analysisResult = null; + MonolithicHeap, EVMAbstractState, TypeEnvironment> analysisResult = null; try { analysisResult = result.getAnalysisStateBefore(node); @@ -139,7 +140,8 @@ public void afterExecution( // Retrieve the symbolic stack from the analysis result EVMAbstractState valueState = analysisResult.getState().getValueState(); - // If the abstract stack is top or bottom or it is empty, we do not + // If the abstract stack is top or bottom or it is empty, we + // do not // have enough information // to solve the jump. if (valueState.isBottom()) { @@ -151,9 +153,9 @@ public void afterExecution( } else { for (KIntegerSet topStack : valueState.getTop()) if (topStack.isBottom()) { - this.unreachableJumps.add(node); + this.unreachableJumps.add(node); continue; - } else if (topStack.isTop() && !topStack.isTopNotJumpdest()) + } else if (topStack.isTop() && !topStack.isTopNotJumpdest()) this.unsoundJumps.add(node); } } @@ -193,9 +195,9 @@ public void afterExecution( @Override public boolean visit( CheckToolWithAnalysisResults< - SimpleAbstractState>, - MonolithicHeap, - EVMAbstractState, TypeEnvironment> tool, + SimpleAbstractState>, + MonolithicHeap, + EVMAbstractState, TypeEnvironment> tool, CFG graph, Statement node) { this.cfgToAnalyze = (EVMCFG) graph; @@ -217,7 +219,7 @@ else if (cfgToAnalyze.getAllPushedJumps().contains(node)) EVMAbstractState, TypeEnvironment> result : tool.getResultOf(this.cfgToAnalyze)) { AnalysisState>, - MonolithicHeap, EVMAbstractState, TypeEnvironment> analysisResult = null; + MonolithicHeap, EVMAbstractState, TypeEnvironment> analysisResult = null; try { analysisResult = result.getAnalysisStateBefore(node); @@ -258,7 +260,7 @@ else if (cfgToAnalyze.getAllPushedJumps().contains(node)) Set filteredDests = this.jumpDestinations.stream() .filter(t -> t.getLocation() instanceof ProgramCounterLocation) .filter(pc -> topStack - .contains(BigInteger.valueOf(((ProgramCounterLocation) pc.getLocation()).getPc()))) + .contains(new Number(((ProgramCounterLocation) pc.getLocation()).getPc()))) .collect(Collectors.toSet()); // If there are no JUMPDESTs for this value, skip to the