diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index d83e7a076..0e8fa8e4c 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -31,8 +31,8 @@ public class AbstractStack implements ValueDomain, BaseLattice(Collections.nCopies(STACK_LIMIT, KIntegerSet.BOTTOM)); -// for (int i = 0; i < STACK_LIMIT; i++) -// stack.add(KIntegerSet.BOTTOM); + // for (int i = 0; i < STACK_LIMIT; i++) + // stack.add(KIntegerSet.BOTTOM); } /** @@ -138,11 +138,11 @@ public AbstractStack wideningAux(AbstractStack other) throws SemanticException { @Override public AbstractStack top() { -// LinkedList result = new LinkedList<>(); -// -// for (int i = 0; i < STACK_LIMIT; i++) -// result.addLast(KIntegerSet.TOP); - LinkedList result = new LinkedList(Collections.nCopies(STACK_LIMIT, KIntegerSet.TOP)); + LinkedList result = new LinkedList<>(); + + for (int i = 0; i < STACK_LIMIT; i++) + result.addLast(KIntegerSet.TOP); + // LinkedList result = new LinkedList(Collections.nCopies(STACK_LIMIT, KIntegerSet.TOP)); return new AbstractStack(result); } @@ -157,7 +157,7 @@ public boolean isTop() { if (isBottom()) return false; else if (this.stack.stream() - .anyMatch(element -> !element.isTop())) + .anyMatch(element -> !element.isTop())) return false; else return true; } @@ -214,8 +214,8 @@ else if (isTop()) private static LinkedList clone(LinkedList list) { LinkedList result = new LinkedList<>(); - for (int i = 0; i < list.size(); i++) - result.add(list.get(i).copy()); + for (KIntegerSet item : list) + result.add(item.copy()); return result; } @@ -265,20 +265,30 @@ public List getStack() { @Override public AbstractStack lubAux(AbstractStack other) throws SemanticException { - // Otherwise, let's build a new SymbolicStack LinkedList result = new LinkedList<>(); - for (int i = 0; i < STACK_LIMIT; i++) - result.addLast(this.stack.get(i).lub(other.stack.get(i))); + Iterator thisIterator = this.stack.iterator(); + Iterator otherIterator = other.stack.iterator(); + + while (thisIterator.hasNext() && otherIterator.hasNext()) { + KIntegerSet thisElement = thisIterator.next(); + KIntegerSet otherElement = otherIterator.next(); + result.addLast(thisElement.lub(otherElement)); + } return new AbstractStack(result); } @Override public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { - for (int i = 0; i < STACK_LIMIT; i++) - if (!this.stack.get(i).lessOrEqual(other.stack.get(i))) + Iterator thisIterator = this.stack.iterator(); + Iterator otherIterator = other.stack.iterator(); + + while (thisIterator.hasNext() && otherIterator.hasNext()) { + if (!thisIterator.next().lessOrEqual(otherIterator.next())) { return false; + } + } return true; } diff --git a/src/main/java/it/unipr/analysis/AbstractStackSet.java b/src/main/java/it/unipr/analysis/AbstractStackSet.java index 8addbaf31..092de077a 100644 --- a/src/main/java/it/unipr/analysis/AbstractStackSet.java +++ b/src/main/java/it/unipr/analysis/AbstractStackSet.java @@ -61,10 +61,12 @@ public AbstractStackSet clone() { return TOP; else if (isBottom()) return BOTTOM; - AbstractStackSet result = new AbstractStackSet(new HashSet(), false); - for (AbstractStack stack : elements()) - result.add(stack.clone()); - return result; + return new AbstractStackSet(new HashSet<>(this.elements), false); + +// AbstractStackSet result = new AbstractStackSet(new HashSet(), false); +// for (AbstractStack stack : elements()) +// result.add(stack.clone()); +// return result; } @Override diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java index 0f4f6dcd1..e7a96faef 100644 --- a/src/main/java/it/unipr/analysis/EVMAbstractState.java +++ b/src/main/java/it/unipr/analysis/EVMAbstractState.java @@ -148,7 +148,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); - BigDecimal valueToPush = this.toBigDecimal(un.getExpression()); + BigInteger valueToPush = this.toBigDecimal(un.getExpression()); resultStack.push(new KIntegerSet(valueToPush)); result.add(resultStack); @@ -342,7 +342,7 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo for (AbstractStack stack : stacks) { AbstractStack resultStack = stack.clone(); Integer i = (Integer) ((Constant) un.getExpression()).getValue(); - resultStack.push(new KIntegerSet(new BigDecimal(i))); + resultStack.push(new KIntegerSet(BigInteger.valueOf(i))); result.add(resultStack); } @@ -721,10 +721,10 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo if (target.isTop() || indexOfByte.isTop()) { resultStack.push(KIntegerSet.TOP); } else { - for (BigDecimal value : target) { - byte[] valueAsByteArray = value.unscaledValue().toByteArray(); + for (BigInteger value : target) { + byte[] valueAsByteArray = value.toByteArray(); - for (BigDecimal index : indexOfByte) { + for (BigInteger index : indexOfByte) { int intIndex = index.intValue(); if (intIndex <= 0 || intIndex >= valueAsByteArray.length) { @@ -985,10 +985,10 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } else { KIntegerSet current_mu_i_lub = KIntegerSet.BOTTOM; - for (BigDecimal os : offset) { - BigDecimal thirtyTwo = new BigDecimal(32); - BigDecimal current_mu_i = os.add(thirtyTwo) - .divide(thirtyTwo, RoundingMode.UP); + for (BigInteger os : offset) { + BigInteger thirtyTwo = BigInteger.valueOf(32); + BigInteger current_mu_i = os.add(thirtyTwo) + .divide(thirtyTwo); memoryResult = memory.putState(os, value); @@ -1019,11 +1019,11 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo } else { KIntegerSet current_mu_i_lub = KIntegerSet.BOTTOM; - for (BigDecimal os : offset) { - BigDecimal current_mu_i = os.add(new BigDecimal(1)) - .divide(new BigDecimal(32), RoundingMode.UP); + for (BigInteger os : offset) { + BigInteger current_mu_i = os.add(BigInteger.valueOf(1)) + .divide(BigInteger.valueOf(32)); - memoryResult = memory.putState(os, value.mod(new KIntegerSet(new BigDecimal(256)))); + memoryResult = memory.putState(os, value.mod(new KIntegerSet(BigInteger.valueOf(256)))); current_mu_i_lub = current_mu_i_lub.lub(new KIntegerSet(current_mu_i)); } @@ -1831,13 +1831,13 @@ public boolean isBottom() { * * @return the BigInteger corresponding to the memory word */ - private BigDecimal toBigDecimal(SymbolicExpression expression) { + private BigInteger toBigDecimal(SymbolicExpression expression) { Constant c = (Constant) expression; String hex = (String) c.getValue(); String hexadecimal = hex.substring(2); BigInteger bigIntVal = new BigInteger(hexadecimal, 16); - BigDecimal bigDecimalVal = new BigDecimal(bigIntVal); - return bigDecimalVal; +// BigDecimal bigDecimalVal = new BigDecimal(bigIntVal); + return bigIntVal; } @Override diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java index 2516b73af..3be59f8cb 100644 --- a/src/main/java/it/unipr/analysis/KIntegerSet.java +++ b/src/main/java/it/unipr/analysis/KIntegerSet.java @@ -1,16 +1,18 @@ package it.unipr.analysis; -import it.unive.lisa.analysis.SemanticException; -import it.unive.lisa.analysis.lattices.SetLattice; -import java.math.BigDecimal; import java.math.BigInteger; -import java.math.RoundingMode; import java.util.Collections; import java.util.HashSet; import java.util.Set; -public class KIntegerSet extends SetLattice { - private static final BigDecimal MAX = new BigDecimal(Math.pow(2, 256)); +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.lattices.SetLattice; + +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 static final int K = 2; public static final KIntegerSet ZERO = new KIntegerSet(0); @@ -20,7 +22,8 @@ public class KIntegerSet extends SetLattice { public static final KIntegerSet TOP = new KIntegerSet(Collections.emptySet(), true); public static final KIntegerSet BOTTOM = new KIntegerSet(Collections.emptySet(), false); - public KIntegerSet(BigDecimal i) { + + public KIntegerSet(BigInteger i) { this(Collections.singleton(i), false); } @@ -33,14 +36,14 @@ public KIntegerSet(Integer... ints) { if (ints.length <= K) for (Integer i : ints) - this.elements.add(new BigDecimal(i)); + this.elements.add(BigInteger.valueOf(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); } @@ -72,7 +75,7 @@ public KIntegerSet glbAux(KIntegerSet other) throws SemanticException { } @Override - public KIntegerSet mk(Set set) { + public KIntegerSet mk(Set set) { return new KIntegerSet(set); } @@ -99,7 +102,7 @@ else if (isTop()) return KIntegerSet.ZERO_OR_ONE; else if (equals(ZERO)) return KIntegerSet.ONE; - else if (!contains(new BigDecimal(0))) + else if (!contains(ZERO_INT)) return KIntegerSet.ZERO; return KIntegerSet.ZERO_OR_ONE; } @@ -110,10 +113,10 @@ public KIntegerSet sum(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) { - BigDecimal add = i.add(j); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) { + BigInteger add = i.add(j); if (add.compareTo(MAX) >= 0) add = add.subtract(MAX); elements.add(add); @@ -128,11 +131,11 @@ public KIntegerSet sub(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) { - BigDecimal sub = i.subtract(j); - if (sub.compareTo(new BigDecimal(0)) < 0) + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) { + BigInteger sub = i.subtract(j); + if (sub.compareTo(ZERO_INT) < 0) sub = sub.add(MAX); elements.add(sub); } @@ -145,7 +148,7 @@ public KIntegerSet copy() { return bottom(); else if (isTop()) return top(); - return new KIntegerSet(this.elements()); + return this; //new KIntegerSet(this.elements()); } public KIntegerSet mul(KIntegerSet other) { @@ -156,11 +159,11 @@ else if (this.equals(ZERO) || other.equals(ZERO)) else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) { - BigDecimal mul = i.multiply(j); - if (mul.compareTo(new BigDecimal(0)) < 0) + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) { + BigInteger mul = i.multiply(j); + if (mul.compareTo(ZERO_INT) < 0) mul = mul.add(MAX); if (mul.compareTo(MAX) > 0) mul = mul.subtract(MAX); @@ -177,13 +180,15 @@ public KIntegerSet div(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - if (j.equals(new BigDecimal(0))) - elements.add(new BigDecimal(0)); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + if (j.equals(ZERO_INT)) + elements.add(ZERO_INT); else - elements.add(i.divide(j, RoundingMode.FLOOR)); + elements.add(i.divide(j)); + +// elements.add(i.divide(j, RoundingMode.FLOOR)); return new KIntegerSet(elements); } @@ -194,14 +199,14 @@ public KIntegerSet mod(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) { + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) { - if (j.equals(new BigDecimal(0))) + if (j.equals(ZERO_INT)) elements.add(i); else - elements.add(i.subtract(j.multiply(i.divide(j, RoundingMode.FLOOR)))); + elements.add(i.subtract(j.multiply(i.divide(j)))); } return new KIntegerSet(elements); @@ -213,14 +218,14 @@ public KIntegerSet addmod(KIntegerSet that, KIntegerSet other) { else if (isTop() || other.isTop() || that.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : that.elements) - for (BigDecimal k : other.elements) - if (k.equals(new BigDecimal(0))) - elements.add(new BigDecimal(0)); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : that.elements) + for (BigInteger k : other.elements) + if (k.equals(ZERO_INT)) + elements.add(ZERO_INT); else - elements.add(i.add(j).subtract(k.multiply(i.add(j).divide(k, RoundingMode.FLOOR)))); + elements.add(i.add(j).subtract(k.multiply(i.add(j).divide(k)))); return new KIntegerSet(elements); } @@ -231,14 +236,14 @@ public KIntegerSet mulmod(KIntegerSet that, KIntegerSet other) { else if (isTop() || other.isTop() || that.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : that.elements) - for (BigDecimal k : other.elements) - if (k.equals(new BigDecimal(0))) - elements.add(new BigDecimal(0)); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : that.elements) + for (BigInteger k : other.elements) + if (k.equals(ZERO_INT)) + elements.add(ZERO_INT); else - elements.add(i.multiply(j).subtract(k.multiply(i.multiply(j).divide(k, RoundingMode.FLOOR)))); + elements.add(i.multiply(j).subtract(k.multiply(i.multiply(j).divide(k)))); return new KIntegerSet(elements); } @@ -249,12 +254,12 @@ public KIntegerSet exp(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) { - for (BigDecimal j : other.elements) { - BigDecimal r = i; + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) { + for (BigInteger j : other.elements) { + BigInteger r = i; - for (int k = 0; j.compareTo(new BigDecimal(k)) > 0; k++) + for (int k = 0; j.compareTo(BigInteger.valueOf(k)) > 0; k++) if (r.compareTo(MAX) > 0) return TOP; else @@ -273,8 +278,8 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; Set r = new HashSet(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) r.add(i.compareTo(j) < 0); if (r.size() == 2) @@ -292,8 +297,8 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; Set r = new HashSet(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) r.add(i.compareTo(j) > 0); if (r.size() == 2) @@ -311,8 +316,8 @@ else if (isTop() || other.isTop()) return KIntegerSet.ZERO_OR_ONE; Set r = new HashSet(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) r.add(i.compareTo(j) == 0); if (r.size() == 2) @@ -331,10 +336,10 @@ else if (this.equals(ZERO) || other.equals(ZERO)) else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal(i.toBigInteger().and(j.toBigInteger()))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add(i.and(j)); return new KIntegerSet(elements); } @@ -345,10 +350,10 @@ public KIntegerSet or(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal(i.toBigInteger().or(j.toBigInteger()))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add(i.or(j)); return new KIntegerSet(elements); } @@ -359,10 +364,10 @@ public KIntegerSet xor(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal(i.toBigInteger().xor(j.toBigInteger()))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add(i.xor(j)); return new KIntegerSet(elements); } @@ -373,12 +378,12 @@ public KIntegerSet not() { else if (isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - if (i.compareTo(new BigDecimal(0)) >= 0) - elements.add(MAX.subtract(i.add(new BigDecimal(1)))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + if (i.compareTo(ZERO_INT) >= 0) + elements.add(MAX.subtract(i.add(ONE_INT))); else - elements.add(new BigDecimal(i.toBigInteger().not())); + elements.add(i.not()); return new KIntegerSet(elements); } @@ -389,10 +394,10 @@ public KIntegerSet shl(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal(new BigInteger(shiftLeft(j.toBigInteger().toByteArray(), i.intValue())))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add(new BigInteger(shiftLeft(j.toByteArray(), i.intValue()))); return new KIntegerSet(elements); } @@ -403,10 +408,10 @@ public KIntegerSet shr(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal(j.toBigInteger().shiftRight(i.intValue()))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add(j.shiftRight(i.intValue())); return new KIntegerSet(elements); } @@ -417,11 +422,11 @@ public KIntegerSet sar(KIntegerSet other) { else if (isTop() || other.isTop()) return top(); - Set elements = new HashSet<>(); - for (BigDecimal i : this.elements) - for (BigDecimal j : other.elements) - elements.add(new BigDecimal( - new BigInteger(shiftArithmeticRight(j.toBigInteger().toByteArray(), i.intValue())))); + Set elements = new HashSet<>(); + for (BigInteger i : this.elements) + for (BigInteger j : other.elements) + elements.add( + new BigInteger(shiftArithmeticRight(j.toByteArray(), i.intValue()))); return new KIntegerSet(elements); } @@ -434,7 +439,7 @@ else if (isTop()) KIntegerSet r = KIntegerSet.BOTTOM; - for (BigDecimal i : this.elements) { + for (BigInteger i : this.elements) { KIntegerSet state = memory.getState(i); if (state.isBottom()) r = r.lub(KIntegerSet.TOP); @@ -614,7 +619,7 @@ public static byte[] shiftArithmeticRight(byte[] byteArray, int shiftBitCount) { public boolean isDefinitelyTrue() { if (isTop() || isBottom()) return false; - return !this.elements().contains(new BigDecimal(0)); + return !this.elements().contains(ZERO_INT); } /** diff --git a/src/main/java/it/unipr/analysis/Memory.java b/src/main/java/it/unipr/analysis/Memory.java index db1fd74eb..ed5a47de3 100644 --- a/src/main/java/it/unipr/analysis/Memory.java +++ b/src/main/java/it/unipr/analysis/Memory.java @@ -1,11 +1,12 @@ package it.unipr.analysis; -import it.unive.lisa.analysis.lattices.FunctionalLattice; -import java.math.BigDecimal; +import java.math.BigInteger; import java.util.HashMap; import java.util.Map; -public class Memory extends FunctionalLattice { +import it.unive.lisa.analysis.lattices.FunctionalLattice; + +public class Memory extends FunctionalLattice { /** * Default constructor for Memory. Initializes the Memory with a default @@ -33,7 +34,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 +49,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/checker/JumpSolver.java b/src/main/java/it/unipr/checker/JumpSolver.java index 95095a343..1244428fa 100644 --- a/src/main/java/it/unipr/checker/JumpSolver.java +++ b/src/main/java/it/unipr/checker/JumpSolver.java @@ -1,5 +1,10 @@ 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.cfg.EVMCFG; @@ -25,10 +30,6 @@ 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.math.BigDecimal; -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 @@ -186,7 +187,7 @@ public boolean visit( Set filteredDests = this.jumpDestinations.stream() .filter(t -> t.getLocation() instanceof ProgramCounterLocation) .filter(pc -> topStack - .contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc()))) + .contains(BigInteger.valueOf(((ProgramCounterLocation) pc.getLocation()).getPc()))) .collect(Collectors.toSet()); // If there are no JUMPDESTs for this value, skip to the