diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index 650b0c0f4..77078d616 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -140,7 +140,7 @@ public AbstractStack top() { LinkedList result = new LinkedList<>(); for (int i = 0; i < STACK_LIMIT; i++) - result.addLast(KIntegerSet.TOP); + result.addLast(KIntegerSet.NUMERIC_TOP); return new AbstractStack(result); } @@ -212,7 +212,7 @@ public AbstractStack clone() { private static LinkedList clone(LinkedList list) { LinkedList result = new LinkedList<>(); for (KIntegerSet item : list) - result.add(item.copy()); + result.add(item); return result; } @@ -237,7 +237,7 @@ public KIntegerSet pop() { if (!stack.getFirst().isTop()) stack.addFirst(KIntegerSet.BOTTOM); else - stack.addFirst(KIntegerSet.TOP); + stack.addFirst(KIntegerSet.NUMERIC_TOP); return result; } @@ -294,7 +294,7 @@ public KIntegerSet getSecondElement() { if (isBottom()) return KIntegerSet.BOTTOM; else if (isTop()) - return KIntegerSet.TOP; + return KIntegerSet.NUMERIC_TOP; return this.stack.get(STACK_LIMIT - 2); } diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java index 0664f6c4a..c2d4c0b47 100644 --- a/src/main/java/it/unipr/analysis/EVMAbstractState.java +++ b/src/main/java/it/unipr/analysis/EVMAbstractState.java @@ -1,5 +1,15 @@ 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; @@ -17,13 +27,6 @@ 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; public class EVMAbstractState implements ValueDomain, BaseLattice { @@ -160,7 +163,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -172,7 +175,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -184,7 +187,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -196,7 +199,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -208,7 +211,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -220,7 +223,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -232,7 +235,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -244,7 +247,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -256,7 +259,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -268,7 +271,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -280,7 +283,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -292,7 +295,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -304,7 +307,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -316,7 +319,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -328,7 +331,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -352,7 +355,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -376,7 +379,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -388,7 +391,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -563,7 +566,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo resultStack.pop(); resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); result.add(resultStack); } @@ -717,7 +720,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet resultKIntegerSet = KIntegerSet.ZERO; if (target.isTop() || indexOfByte.isTop()) { - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); } else { for (BigInteger value : target) { byte[] valueAsByteArray = value.toByteArray(); @@ -792,7 +795,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet offset = resultStack.pop(); KIntegerSet length = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); result.add(resultStack); } @@ -806,7 +809,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet address = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -820,7 +823,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet offset = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -864,7 +867,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet address = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -909,7 +912,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet address = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -923,7 +926,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet blockNumber = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -952,9 +955,9 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo if (mu_i.equals(KIntegerSet.ZERO)) { // This is an error. We cannot read from memory if // there is no active words saved - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); } else if (offset.isTop()) { - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); new_mu_i = mu_i; } else { resultStack.push(offset.mload(memory)); @@ -1041,7 +1044,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo AbstractStack resultStack = stack.clone(); KIntegerSet key = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NUMERIC_TOP); result.add(resultStack); } @@ -1471,7 +1474,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet offset = resultStack.pop(); KIntegerSet length = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1488,7 +1491,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet length = resultStack.pop(); KIntegerSet salt = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1508,7 +1511,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet outOffset = resultStack.pop(); KIntegerSet outLength = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1528,7 +1531,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet outOffset = resultStack.pop(); KIntegerSet outLength = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1561,7 +1564,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet outOffset = resultStack.pop(); KIntegerSet outLength = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1580,7 +1583,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo KIntegerSet outOffset = resultStack.pop(); KIntegerSet outLength = resultStack.pop(); - resultStack.push(KIntegerSet.TOP); + resultStack.push(KIntegerSet.NOT_JUMPDEST_TOP); result.add(resultStack); } @@ -1712,20 +1715,14 @@ public EVMAbstractState assume(ValueExpression expression, ProgramPoint src, Pro UnaryOperator op = un.getOperator(); if (op instanceof JumpiOperator) { // JUMPI - KIntegerSet condition = ((KIntegerSet) ((Constant) un.getExpression()).getValue()); - - if (condition.isDefinitelyFalse()) { - // if condition is surely false, return bottom - return bottom(); - } else if (condition.isDefinitelyTrue()) { - // if condition is surely true, return the result - return new EVMAbstractState(stacks.clone(), memory, mu_i); - } else if (condition.isUnknown()) { - // Condition could be either true or false - // Return the result - return new EVMAbstractState(stacks.clone(), memory, mu_i); - } else + + @SuppressWarnings("unchecked") + Pair, Set> split = ((Pair, Set>) ((Constant) un.getExpression()).getValue()); + if (split.getLeft().isEmpty() && split.getRight().isEmpty()) + return top(); + else if (split.getLeft().isEmpty()) return bottom(); + return new EVMAbstractState(new AbstractStackSet(split.getLeft(), false), memory, mu_i); } else if (op instanceof LogicalNegation) { // Get the expression wrapped by LogicalNegation @@ -1736,23 +1733,14 @@ public EVMAbstractState assume(ValueExpression expression, ProgramPoint src, Pro // Check if LogicalNegation is wrapping a JUMPI if (wrappedOperator instanceof JumpiOperator) { // !JUMPI - KIntegerSet condition = ((KIntegerSet) ((Constant) ((UnaryExpression) wrappedExpr) - .getExpression()).getValue()); - - if (condition.isDefinitelyFalse()) { - // if condition is surely false, return the - // result - return new EVMAbstractState(stacks.clone(), memory, mu_i); - } else if (condition.isDefinitelyTrue()) { - // if condition is surely true, return the - // bottom - return bottom(); - } else if (condition.isUnknown()) { - // Condition could be either true or false - // Return the result - return new EVMAbstractState(stacks.clone(), memory, mu_i); - } else + + @SuppressWarnings("unchecked") + Pair, Set> split = ((Pair, Set>) ((Constant) ((UnaryExpression) wrappedExpr).getExpression()).getValue()); + if (split.getLeft().isEmpty() && split.getRight().isEmpty()) + return top(); + else if (split.getRight().isEmpty()) return bottom(); + return new EVMAbstractState(new AbstractStackSet(split.getRight(), false), memory, mu_i); } } } diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java index c2cd471d8..25315df11 100644 --- a/src/main/java/it/unipr/analysis/KIntegerSet.java +++ b/src/main/java/it/unipr/analysis/KIntegerSet.java @@ -12,13 +12,14 @@ public class KIntegerSet extends SetLattice { private static final BigInteger ONE_INT = BigInteger.valueOf(1); private static final BigInteger MAX = BigInteger.valueOf((long) Math.pow(2, 256)); - public static final int K = 2; + public static final int K = 1; public static final KIntegerSet ZERO = new KIntegerSet(0); public static final KIntegerSet ONE = new KIntegerSet(1); public static final KIntegerSet ZERO_OR_ONE = new KIntegerSet(0, 1); - public static final KIntegerSet TOP = new KIntegerSet(Collections.emptySet(), true); + public static final KIntegerSet NUMERIC_TOP = new KIntegerSet(Collections.emptySet(), true); + public static final KIntegerSet NOT_JUMPDEST_TOP = new KIntegerSet(7); public static final KIntegerSet BOTTOM = new KIntegerSet(Collections.emptySet(), false); public KIntegerSet(BigInteger i) { @@ -47,16 +48,31 @@ public KIntegerSet(Set elements, boolean isTop) { @Override public KIntegerSet top() { - return TOP; + return NUMERIC_TOP; } @Override public KIntegerSet bottom() { return BOTTOM; } + + @Override + public boolean isBottom() { + return elements != null && super.isBottom(); + } + + @Override + public boolean isTop() { + return elements != null && super.isTop(); + } + @Override public KIntegerSet lubAux(KIntegerSet other) throws SemanticException { + if (isTopNotJumpdest()) + return this; + else if (other.isTopNotJumpdest()) + return other; KIntegerSet result = super.lubAux(other); return result.size() > K ? top() : result; } @@ -92,12 +108,14 @@ public boolean equals(Object obj) { return false; return true; } - + public KIntegerSet isZero() { if (isBottom()) return bottom(); else if (isTop()) return KIntegerSet.ZERO_OR_ONE; + else if (isTopNotJumpdest()) + return NOT_JUMPDEST_TOP; else if (equals(ZERO)) return KIntegerSet.ONE; else if (!contains(ZERO_INT)) @@ -110,6 +128,8 @@ public KIntegerSet sum(KIntegerSet other) { return bottom(); 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) @@ -128,7 +148,9 @@ public KIntegerSet sub(KIntegerSet other) { return bottom(); 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) { @@ -141,14 +163,6 @@ else if (isTop() || other.isTop()) return new KIntegerSet(elements); } - public KIntegerSet copy() { - if (isBottom()) - return bottom(); - else if (isTop()) - return top(); - return this; // new KIntegerSet(this.elements()); - } - public KIntegerSet mul(KIntegerSet other) { if (isBottom() || other.isBottom()) return bottom(); @@ -156,7 +170,9 @@ else if (this.equals(ZERO) || other.equals(ZERO)) return ZERO; 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) { @@ -177,6 +193,8 @@ public KIntegerSet div(KIntegerSet other) { return bottom(); 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) @@ -196,6 +214,8 @@ public KIntegerSet mod(KIntegerSet other) { return bottom(); 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) @@ -215,7 +235,9 @@ public KIntegerSet addmod(KIntegerSet that, KIntegerSet other) { return bottom(); 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) @@ -233,7 +255,9 @@ public KIntegerSet mulmod(KIntegerSet that, KIntegerSet other) { return bottom(); 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) @@ -251,7 +275,9 @@ public KIntegerSet exp(KIntegerSet other) { return bottom(); 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) { @@ -259,7 +285,7 @@ else if (isTop() || other.isTop()) for (int k = 0; j.compareTo(BigInteger.valueOf(k)) > 0; k++) if (r.compareTo(MAX) > 0) - return TOP; + return NUMERIC_TOP; else r = r.multiply(i); elements.add(r); @@ -274,7 +300,9 @@ public KIntegerSet lt(KIntegerSet other) { return KIntegerSet.BOTTOM; 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) @@ -293,7 +321,9 @@ public KIntegerSet gt(KIntegerSet other) { return KIntegerSet.BOTTOM; 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) @@ -312,7 +342,9 @@ public KIntegerSet eq(KIntegerSet other) { return KIntegerSet.BOTTOM; 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) @@ -333,6 +365,8 @@ else if (this.equals(ZERO) || other.equals(ZERO)) return ZERO; 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) @@ -347,6 +381,8 @@ public KIntegerSet or(KIntegerSet other) { return bottom(); 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) @@ -361,6 +397,8 @@ public KIntegerSet xor(KIntegerSet other) { return bottom(); 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) @@ -375,6 +413,8 @@ public KIntegerSet not() { return bottom(); else if (isTop()) return top(); + else if (isTopNotJumpdest()) + return NOT_JUMPDEST_TOP; Set elements = new HashSet<>(K); for (BigInteger i : this.elements) @@ -391,6 +431,8 @@ public KIntegerSet shl(KIntegerSet other) { return bottom(); 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) @@ -405,6 +447,8 @@ public KIntegerSet shr(KIntegerSet other) { return bottom(); 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) @@ -419,6 +463,8 @@ public KIntegerSet sar(KIntegerSet other) { return bottom(); 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) @@ -434,13 +480,15 @@ public KIntegerSet mload(Memory memory) throws SemanticException { return bottom(); else if (isTop()) return top(); + else if (isTopNotJumpdest()) + return NOT_JUMPDEST_TOP; KIntegerSet r = KIntegerSet.BOTTOM; for (BigInteger i : this.elements) { KIntegerSet state = memory.getState(i); if (state.isBottom()) - r = r.lub(KIntegerSet.TOP); + r = r.lub(KIntegerSet.NUMERIC_TOP); else r = r.lub(state); } @@ -615,7 +663,7 @@ public static byte[] shiftArithmeticRight(byte[] byteArray, int shiftBitCount) { * otherwise. */ public boolean isDefinitelyTrue() { - if (isTop() || isBottom()) + if (isTop() || isBottom() || isTopNotJumpdest()) return false; return !this.elements().contains(ZERO_INT); } @@ -627,7 +675,7 @@ public boolean isDefinitelyTrue() { * @return {@code true} if this set is zero, {@code false} otherwise. */ public boolean isDefinitelyFalse() { - if (isTop() || isBottom()) + if (isTop() || isBottom() || isTopNotJumpdest()) return false; return this.equals(ZERO); } @@ -639,6 +687,10 @@ public boolean isDefinitelyFalse() { * determined, {@code false} otherwise */ public boolean isUnknown() { - return isTop() || (!isBottom() && !isDefinitelyFalse() && !isDefinitelyTrue()); + return isTop() || isTopNotJumpdest() || (!isBottom() && !isDefinitelyFalse() && !isDefinitelyTrue()); + } + + public boolean isTopNotJumpdest() { + return this == NOT_JUMPDEST_TOP; } } \ No newline at end of file diff --git a/src/main/java/it/unipr/cfg/Jump.java b/src/main/java/it/unipr/cfg/Jump.java index dfc69ba7e..4de459be2 100644 --- a/src/main/java/it/unipr/cfg/Jump.java +++ b/src/main/java/it/unipr/cfg/Jump.java @@ -1,6 +1,5 @@ package it.unipr.cfg; -import it.unipr.analysis.EVMAbstractState; import it.unipr.analysis.operator.JumpOperator; import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; @@ -56,37 +55,6 @@ public String toString() { T extends TypeDomain> AnalysisState semantics( AnalysisState entryState, InterproceduralAnalysis interprocedural, StatementStore expressions) throws SemanticException { - - EVMAbstractState valueState = entryState.getDomainInstance(EVMAbstractState.class); - EVMCFG cfg = (EVMCFG) getProgram().getAllCFGs().stream().findAny().get(); -// Set jumpDestinations = cfg.getAllJumpdest(); -// -// // 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() && !valueState.isTop()) { -// AbstractStackSet stacks = valueState.getStacks(); -// -// for (AbstractStack a : stacks) { -// KIntegerSet stack = a.getTop(); -// if (!stack.isBottom() && !stack.isTop()) { -// Set filteredDests = jumpDestinations.stream() -// .filter(t -> t.getLocation() instanceof ProgramCounterLocation) -// .filter(pc -> stack -// .contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc()))) -// .collect(Collectors.toSet()); -// -// // For each JUMPDEST, add the missing edge from this node to -// // the JUMPDEST. -// for (Statement jmp : filteredDests) { -// if (!cfg.containsEdge(new TrueEdge(this, jmp))) { -// cfg.addEdge(new TrueEdge(this, jmp)); -// } -// } -// } -// } -// } - Constant dummy = new Constant(Untyped.INSTANCE, this.getCFG().getOutgoingEdges(this).size(), getLocation()); return entryState.smallStepSemantics(new it.unive.lisa.symbolic.value.UnaryExpression(Untyped.INSTANCE, dummy, JumpOperator.INSTANCE, getLocation()), this); diff --git a/src/main/java/it/unipr/cfg/Jumpi.java b/src/main/java/it/unipr/cfg/Jumpi.java index b4af7216f..71b1ea0c3 100644 --- a/src/main/java/it/unipr/cfg/Jumpi.java +++ b/src/main/java/it/unipr/cfg/Jumpi.java @@ -1,5 +1,10 @@ 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; @@ -53,48 +58,33 @@ 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); -// EVMCFG cfg = (EVMCFG) getProgram().getAllCFGs().stream().findAny().get(); -// Set jumpDestinations = cfg.getAllJumpdest(); -// -// // 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() && !valueState.isTop()) { -// AbstractStackSet stacks = valueState.getStacks(); -// -// for (AbstractStack a : stacks) { -// -// KIntegerSet stack = a.getTop(); -// if (!stack.isBottom() && !stack.isTop()) { -// Set filteredDests = jumpDestinations.stream() -// .filter(t -> t.getLocation() instanceof ProgramCounterLocation) -// .filter(pc -> stack -// .contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc()))) -// .collect(Collectors.toSet()); -// -// // For each JUMPDEST, add the missing edge from this node to -// // the JUMPDEST. -// for (Statement jmp : filteredDests) { -// if (!cfg.containsEdge(new TrueEdge(this, jmp))) { -// cfg.addEdge(new TrueEdge(this, jmp)); -// } -// } -// } -// } -// } - KIntegerSet b = KIntegerSet.BOTTOM; - if (!valueState.isBottom() && !valueState.isTop()) - for (AbstractStack st : valueState.getStacks()) - b = b.lub(st.getSecondElement()); + // Split here + Set trueStacks = new HashSet<>(); + Set falseStacks = new HashSet<>(); + if (!valueState.isBottom() && !valueState.isTop()) { + for (AbstractStack st : valueState.getStacks()) { + AbstractStack result = st.clone(); + result.pop(); + KIntegerSet condition = result.pop(); + if (condition.isDefinitelyTrue()) + trueStacks.add(result); + else if (condition.isDefinitelyFalse()) + falseStacks.add(result); + else if (condition.isUnknown()) { + trueStacks.add(result); + falseStacks.add(result); + } + } + } - Constant dummy = new Constant(Untyped.INSTANCE, b, getLocation()); + Constant dummy = new Constant(Untyped.INSTANCE, Pair.of(trueStacks, falseStacks), getLocation()); return entryState.smallStepSemantics(new it.unive.lisa.symbolic.value.UnaryExpression(Untyped.INSTANCE, dummy, JumpiOperator.INSTANCE, getLocation()), this); } diff --git a/src/main/java/it/unipr/checker/JumpSolver.java b/src/main/java/it/unipr/checker/JumpSolver.java index a1385b807..4e9d18fef 100644 --- a/src/main/java/it/unipr/checker/JumpSolver.java +++ b/src/main/java/it/unipr/checker/JumpSolver.java @@ -137,7 +137,7 @@ public void afterExecution( if (topStack.isBottom()) { this.unreachableJumps.add(node); continue; - } else if (topStack.isTop()) { + } else if (topStack.isTop() && !topStack.isTopNotJumpdest()) { System.err.println("Reachable: " + this.cfgToAnalyze.reachableFrom(entryPoint, node)); this.unsoundJumps.add(node); }