idealSeedSolver) {
- return scanner.debugger(idealSeedSolver.getSeed());
- }
-
@Override
public int getTimeout() {
return scanner.getTimeout();
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/UnEnsuredPredicate.java b/CryptoAnalysis/src/main/java/crypto/analysis/UnEnsuredPredicate.java
new file mode 100644
index 000000000..ca8a6d60a
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/UnEnsuredPredicate.java
@@ -0,0 +1,147 @@
+package crypto.analysis;
+
+import crypto.analysis.errors.AbstractConstraintsError;
+import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AbstractOrderError;
+import crypto.analysis.errors.ForbiddenMethodError;
+import crypto.analysis.errors.PredicateConstraintError;
+import crypto.extractparameter.CallSiteWithExtractedValue;
+import crysl.rule.CrySLPredicate;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Objects;
+import java.util.Set;
+
+/**
+ * Wrapper class for a single {@link CrySLPredicate} that could not be ensured during the analysis.
+ * If a seed cannot generate a predicate due to some violations from its CrySL rule, the analysis
+ * keeps track of those violations and the seed s.t. other seeds can reason about why the predicate
+ * was not ensured. This way, the analysis can connect corresponding subsequent errors.
+ *
+ * See the paper
+ */
+public class UnEnsuredPredicate extends AbstractPredicate {
+
+ private final AnalysisSeedWithSpecification generatingSeed;
+ private final Collection violations;
+
+ /** Collection of violations that may cause a predicate to be not ensured */
+ public enum Violations {
+ /** Violation if there is a call to a method from the FORBIDDEN section. */
+ CallToForbiddenMethod,
+
+ /**
+ * Violation if there is an unsatisfied constraint. Constraints include basic constraints
+ * from the CONSTRAINTS section and required predicates from the REQUIRES section.
+ */
+ ConstraintsAreNotSatisfied,
+
+ /**
+ * Violation if the condition of predicate from the ENSURES section is not satisfied. Note
+ * that the analysis does not report an error because the condition is not required to be
+ * satisfied.
+ */
+ ConditionIsNotSatisfied,
+
+ /**
+ * Violation if there are dataflow paths where the seed does not reach an accepting state to
+ * generate a predicate.
+ */
+ GeneratingStateMayNotBeReached,
+
+ /**
+ * Violation if there is no dataflow path where the seed reaches an accepting state to
+ * generate a predicate.
+ */
+ GeneratingStateIsNeverReached
+ }
+
+ public UnEnsuredPredicate(
+ CrySLPredicate predicate,
+ Collection parametersToValues,
+ AnalysisSeedWithSpecification generatingSeed,
+ Collection violations) {
+ super(predicate, parametersToValues);
+
+ this.generatingSeed = generatingSeed;
+ this.violations = Set.copyOf(violations);
+ }
+
+ public AnalysisSeedWithSpecification getGeneratingSeed() {
+ return generatingSeed;
+ }
+
+ public Collection getViolations() {
+ return violations;
+ }
+
+ /**
+ * Compute the preceding errors that cause the predicate stored in this class to be not ensured.
+ *
+ * @return the errors that cause the predicate to be not ensured
+ */
+ public Collection getPrecedingErrors() {
+ Collection result = new HashSet<>();
+
+ // Collect all ForbiddenMethodErrors
+ if (violations.contains(Violations.CallToForbiddenMethod)) {
+ Collection forbiddenMethodErrors =
+ generatingSeed.getErrors().stream()
+ .filter(e -> e instanceof ForbiddenMethodError)
+ .toList();
+ result.addAll(forbiddenMethodErrors);
+ }
+
+ /* Collect the ConstraintErrors. This includes error violating constraints from the
+ * CONSTRAINTS section and violated predicates from the REQUIRES section.
+ */
+ if (violations.contains(Violations.ConstraintsAreNotSatisfied)) {
+ Collection constraintErrors =
+ generatingSeed.getErrors().stream()
+ .filter(e -> e instanceof AbstractConstraintsError)
+ .toList();
+ result.addAll(constraintErrors);
+ }
+
+ /* If the predicate condition in the ENSURES section is not satisfied, a
+ * PredicateConstraintError is created. Note that these errors are not reported since
+ * they are not required to be satisfied. However, a corresponding error indicate that
+ * the condition is not satisfied.
+ */
+ if (violations.contains(Violations.ConditionIsNotSatisfied)) {
+ PredicateConstraintError error =
+ new PredicateConstraintError(generatingSeed, getPredicate());
+ result.add(error);
+ }
+
+ // Collect all errors that cause the seed to not reach an accepting state
+ if (violations.contains(Violations.GeneratingStateMayNotBeReached)
+ || violations.contains(Violations.GeneratingStateIsNeverReached)) {
+ Collection orderError =
+ generatingSeed.getErrors().stream()
+ .filter(e -> e instanceof AbstractOrderError)
+ .toList();
+ result.addAll(orderError);
+ }
+
+ return result;
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(super.hashCode(), generatingSeed, violations);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj)
+ && obj instanceof UnEnsuredPredicate other
+ && Objects.equals(generatingSeed, other.getGeneratingSeed())
+ && Objects.equals(violations, other.getViolations());
+ }
+
+ @Override
+ public String toString() {
+ return "Hidden: " + getPredicate().getPredName();
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java
new file mode 100644
index 000000000..b52f40f7a
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractConstraintsError.java
@@ -0,0 +1,25 @@
+package crypto.analysis.errors;
+
+import boomerang.scene.Statement;
+import crypto.analysis.IAnalysisSeed;
+import crysl.rule.CrySLRule;
+
+/**
+ * Super class for all errors that violate a constraint from the CONSTRAINTS and REQUIRES section
+ */
+public abstract class AbstractConstraintsError extends AbstractError {
+
+ public AbstractConstraintsError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) {
+ super(seed, errorStmt, rule);
+ }
+
+ @Override
+ public int hashCode() {
+ return super.hashCode();
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj);
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java
index a48aafb39..f82a7cd92 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java
@@ -5,10 +5,10 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLMethod;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
import java.util.Collection;
import java.util.HashSet;
import java.util.Map;
+import java.util.Objects;
public abstract class AbstractError {
@@ -16,16 +16,16 @@ public abstract class AbstractError {
private final Statement errorStmt;
private final CrySLRule rule;
- private final Collection causedByErrors; // preceding
- private final Collection willCauseErrors; // subsequent
+ private final Collection precedingErrors; // preceding
+ private final Collection subsequentErrors; // subsequent
public AbstractError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) {
this.seed = seed;
this.errorStmt = errorStmt;
this.rule = rule;
- this.causedByErrors = new HashSet<>();
- this.willCauseErrors = new HashSet<>();
+ this.precedingErrors = new HashSet<>();
+ this.subsequentErrors = new HashSet<>();
}
public abstract String toErrorMarkerString();
@@ -50,24 +50,28 @@ public int getLineNumber() {
return errorStmt.getStartLineNumber();
}
- public void addCausingError(AbstractError parent) {
- causedByErrors.add(parent);
+ public void addPrecedingError(AbstractError error) {
+ precedingErrors.add(error);
}
public void addCausingError(Collection parents) {
- causedByErrors.addAll(parents);
+ precedingErrors.addAll(parents);
}
public void addSubsequentError(AbstractError subsequentError) {
- willCauseErrors.add(subsequentError);
+ subsequentErrors.add(subsequentError);
+ }
+
+ public Collection getPrecedingErrors() {
+ return precedingErrors;
}
public Collection getSubsequentErrors() {
- return this.willCauseErrors;
+ return subsequentErrors;
}
public Collection getRootErrors() {
- return this.causedByErrors;
+ return this.precedingErrors;
}
public String toString() {
@@ -112,34 +116,14 @@ protected String formatMethodName(CrySLMethod method) {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {seed, errorStmt, rule});
+ return Objects.hash(seed, errorStmt, rule);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
-
- AbstractError other = (AbstractError) obj;
- if (seed == null) {
- if (other.getSeed() != null) return false;
- } else if (!seed.equals(other.getSeed())) {
- return false;
- }
-
- if (errorStmt == null) {
- if (other.getErrorStatement() != null) return false;
- } else if (!errorStmt.equals(other.getErrorStatement())) {
- return false;
- }
-
- if (rule == null) {
- if (other.getRule() != null) return false;
- } else if (!rule.equals(other.getRule())) {
- return false;
- }
-
- return true;
+ return obj instanceof AbstractError other
+ && Objects.equals(seed, other.seed)
+ && Objects.equals(errorStmt, other.errorStmt)
+ && Objects.equals(rule, other.rule);
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractOrderError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractOrderError.java
new file mode 100644
index 000000000..a8a7d1893
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractOrderError.java
@@ -0,0 +1,23 @@
+package crypto.analysis.errors;
+
+import boomerang.scene.Statement;
+import crypto.analysis.IAnalysisSeed;
+import crysl.rule.CrySLRule;
+
+/** Super class for all errors from the ORDER section */
+public abstract class AbstractOrderError extends AbstractError {
+
+ public AbstractOrderError(IAnalysisSeed seed, Statement errorStmt, CrySLRule rule) {
+ super(seed, errorStmt, rule);
+ }
+
+ @Override
+ public int hashCode() {
+ return super.hashCode();
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj);
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiredPredicateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiredPredicateError.java
new file mode 100644
index 000000000..8b899ab63
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractRequiredPredicateError.java
@@ -0,0 +1,58 @@
+package crypto.analysis.errors;
+
+import boomerang.scene.Statement;
+import crypto.analysis.IAnalysisSeed;
+import crypto.analysis.UnEnsuredPredicate;
+import crysl.rule.CrySLRule;
+import java.util.Collection;
+import java.util.Objects;
+import java.util.Set;
+
+/**
+ * Super class for errors that work with a {@link UnEnsuredPredicate}. Currently, there are {@link
+ * RequiredPredicateError} that hold errors with single violated predicates and {@link
+ * AlternativeReqPredicateError} that hold errors for violated predicates with alternatives.
+ */
+public abstract class AbstractRequiredPredicateError extends AbstractConstraintsError {
+
+ private final Collection unEnsuredPredicates;
+
+ public AbstractRequiredPredicateError(
+ IAnalysisSeed seed,
+ Statement errorStmt,
+ CrySLRule rule,
+ Collection unEnsuredPredicates) {
+ super(seed, errorStmt, rule);
+
+ this.unEnsuredPredicates = Set.copyOf(unEnsuredPredicates);
+ }
+
+ public Collection getHiddenPredicates() {
+ return unEnsuredPredicates;
+ }
+
+ protected String getParamIndexAsText(int paramIndex) {
+ return switch (paramIndex) {
+ case -1 -> "Return value";
+ case 0 -> "First parameter";
+ case 1 -> "Second parameter";
+ case 2 -> "Third parameter";
+ case 3 -> "Fourth parameter";
+ case 4 -> "Fifth parameter";
+ case 5 -> "Sixth parameter";
+ default -> (paramIndex + 1) + "th parameter";
+ };
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(super.hashCode(), unEnsuredPredicates);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj)
+ && obj instanceof AbstractRequiredPredicateError other
+ && Objects.equals(unEnsuredPredicates, other.getHiddenPredicates());
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/AlternativeReqPredicateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AlternativeReqPredicateError.java
new file mode 100644
index 000000000..eedff51e5
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/AlternativeReqPredicateError.java
@@ -0,0 +1,97 @@
+package crypto.analysis.errors;
+
+import crypto.analysis.AlternativeReqPredicate;
+import crypto.analysis.AnalysisSeedWithSpecification;
+import crypto.analysis.RequiredCrySLPredicate;
+import crypto.analysis.UnEnsuredPredicate;
+import crysl.rule.CrySLPredicate;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+
+/**
+ * Error that models a violation of required predicates with alternatives. Predicates from the
+ * REQUIRES section may have the form
+ *
+ * {@code
+ * REQUIRES
+ * generatedKey[...] || generatedPubKey[...] || generatedPrivKey[...];
+ * }
+ *
+ * If the base predicate "generatedKey" and any (relevant) alternative is not ensured, an error of
+ * this class is reported.
+ */
+public class AlternativeReqPredicateError extends AbstractRequiredPredicateError {
+
+ private final Collection contradictedPredicate;
+ private final Collection relevantPredicates;
+
+ public AlternativeReqPredicateError(
+ AnalysisSeedWithSpecification seed,
+ AlternativeReqPredicate violatedPred,
+ Collection unEnsuredPredicates) {
+ super(seed, violatedPred.getLocation(), seed.getSpecification(), unEnsuredPredicates);
+
+ this.contradictedPredicate = List.copyOf(violatedPred.getAllAlternatives());
+ this.relevantPredicates = Set.copyOf(violatedPred.getRelAlternatives());
+ }
+
+ public Collection getContradictedPredicate() {
+ return contradictedPredicate;
+ }
+
+ public Collection getRelevantPredicates() {
+ return relevantPredicates;
+ }
+
+ @Override
+ public String toErrorMarkerString() {
+ Collection added = new HashSet<>();
+
+ List msg = new ArrayList<>();
+ for (RequiredCrySLPredicate pred : relevantPredicates) {
+ StringBuilder temp = new StringBuilder();
+ temp.append(getParamIndexAsText(pred.getParamIndex()));
+
+ if (pred.getPred().isNegated()) {
+ temp.append(" is generated as ");
+ } else {
+ temp.append(" was not properly generated as ");
+ }
+ temp.append(pred.getPred().getPredName());
+
+ msg.add(temp.toString());
+ added.add(pred.getPred());
+ }
+
+ for (CrySLPredicate pred : contradictedPredicate) {
+ if (added.contains(pred)) {
+ continue;
+ }
+ msg.add(pred.getPredName() + " was not ensured (not relevant)");
+ }
+
+ return String.join(" AND ", msg);
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(super.hashCode(), contradictedPredicate, relevantPredicates);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj)
+ && obj instanceof AlternativeReqPredicateError other
+ && Objects.equals(contradictedPredicate, other.getContradictedPredicate())
+ && Objects.equals(relevantPredicates, other.getRelevantPredicates());
+ }
+
+ @Override
+ public String toString() {
+ return "AlternativeReqPredicateError: " + toErrorMarkerString();
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/CallToError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/CallToError.java
index 58818d6fe..db46b93dc 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/CallToError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/CallToError.java
@@ -3,10 +3,10 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLMethod;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
import java.util.Collection;
+import java.util.Objects;
-public class CallToError extends AbstractError {
+public class CallToError extends AbstractConstraintsError {
private final Collection requiredMethods;
@@ -31,22 +31,14 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), requiredMethods});
+ return Objects.hash(super.hashCode(), requiredMethods);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
-
- CallToError other = (CallToError) obj;
- if (!super.equals(other)) return false;
- if (requiredMethods == null) {
- return other.getRequiredMethods() == null;
- } else {
- return requiredMethods.equals(other.getRequiredMethods());
- }
+ return super.equals(obj)
+ && obj instanceof CallToError other
+ && Objects.equals(requiredMethods, other.getRequiredMethods());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ConstraintError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ConstraintError.java
index 2017362cb..27f2ee185 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ConstraintError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ConstraintError.java
@@ -13,10 +13,10 @@
import crysl.rule.CrySLSplitter;
import crysl.rule.CrySLValueConstraint;
import crysl.rule.ISLConstraint;
-import java.util.Arrays;
import java.util.Collection;
+import java.util.Objects;
-public class ConstraintError extends AbstractError {
+public class ConstraintError extends AbstractConstraintsError {
private final CallSiteWithExtractedValue callSite;
private final ISLConstraint violatedConstraint;
@@ -26,7 +26,7 @@ public ConstraintError(
CallSiteWithExtractedValue cs,
CrySLRule rule,
ISLConstraint constraint) {
- super(seed, cs.getCallSiteWithParam().stmt(), rule);
+ super(seed, cs.callSiteWithParam().statement(), rule);
this.callSite = cs;
this.violatedConstraint = constraint;
@@ -49,24 +49,20 @@ private String evaluateBrokenConstraint(final ISLConstraint constraint) {
StringBuilder msg = new StringBuilder();
if (constraint instanceof CrySLValueConstraint) {
return evaluateValueConstraint((CrySLValueConstraint) constraint);
- } else if (constraint instanceof CrySLArithmeticConstraint) {
- final CrySLArithmeticConstraint brokenArthConstraint =
- (CrySLArithmeticConstraint) constraint;
- msg.append(brokenArthConstraint.getLeft());
+ } else if (constraint instanceof CrySLArithmeticConstraint brokenArithConstraint) {
+ msg.append(brokenArithConstraint.getLeft());
msg.append(" ");
- msg.append(brokenArthConstraint.getOperator());
+ msg.append(brokenArithConstraint.getOperator());
msg.append(" ");
- msg.append(brokenArthConstraint.getRight());
- } else if (constraint instanceof CrySLComparisonConstraint) {
- final CrySLComparisonConstraint brokenCompCons = (CrySLComparisonConstraint) constraint;
+ msg.append(brokenArithConstraint.getRight());
+ } else if (constraint instanceof CrySLComparisonConstraint brokenCompCons) {
msg.append(" Variable ");
msg.append(brokenCompCons.getLeft().getLeft().getName());
msg.append(" must be ");
msg.append(evaluateCompOp(brokenCompCons.getOperator()));
msg.append(" ");
msg.append(brokenCompCons.getRight().getLeft().getName());
- } else if (constraint instanceof CrySLConstraint) {
- final CrySLConstraint crySLConstraint = (CrySLConstraint) constraint;
+ } else if (constraint instanceof CrySLConstraint crySLConstraint) {
final ISLConstraint leftSide = crySLConstraint.getLeft();
final ISLConstraint rightSide = crySLConstraint.getRight();
switch (crySLConstraint.getOperator()) {
@@ -91,21 +87,14 @@ private String evaluateBrokenConstraint(final ISLConstraint constraint) {
}
private String evaluateCompOp(CrySLComparisonConstraint.CompOp operator) {
- switch (operator) {
- case ge:
- return "at least";
- case g:
- return "greater than";
- case l:
- return "lesser than";
- case le:
- return "at most";
- case eq:
- return "equal to";
- case neq:
- return "not equal to";
- }
- return "";
+ return switch (operator) {
+ case ge -> "at least";
+ case g -> "greater than";
+ case l -> "lesser than";
+ case le -> "at most";
+ case eq -> "equal to";
+ case neq -> "not equal to";
+ };
}
private String evaluateValueConstraint(final CrySLValueConstraint brokenConstraint) {
@@ -113,7 +102,7 @@ private String evaluateValueConstraint(final CrySLValueConstraint brokenConstrai
msg.append(" should be any of ");
CrySLSplitter splitter = brokenConstraint.getVar().getSplitter();
if (splitter != null) {
- Statement stmt = callSite.getCallSiteWithParam().stmt();
+ Statement stmt = callSite.callSiteWithParam().statement();
String[] splitValues = new String[] {""};
if (stmt.isAssign()) {
Val rightSide = stmt.getRightOp();
@@ -135,10 +124,8 @@ private String evaluateValueConstraint(final CrySLValueConstraint brokenConstrai
}
}
}
- } else {
- // splitValues =
- // filterQuotes(stmt.getInvokeExpr().getUseBoxes().get(0).getValue().toString()).split(splitter.getSplitter());
}
+
if (splitValues.length >= splitter.getIndex()) {
for (int i = 0; i < splitter.getIndex(); i++) {
msg.append(splitValues[i]);
@@ -165,29 +152,15 @@ public static String filterQuotes(final String dirty) {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), callSite, violatedConstraint});
+ return Objects.hash(super.hashCode(), callSite, violatedConstraint);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- ConstraintError other = (ConstraintError) obj;
- if (callSite == null) {
- if (other.getCallSiteWithExtractedValue() != null) return false;
- } else if (!callSite.equals(other.getCallSiteWithExtractedValue())) {
- return false;
- }
-
- if (violatedConstraint == null) {
- if (other.getViolatedConstraint() != null) return false;
- } else if (!violatedConstraint.equals(other.getViolatedConstraint())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof ConstraintError other
+ && Objects.equals(callSite, other.getCallSiteWithExtractedValue())
+ && Objects.equals(violatedConstraint, other.getViolatedConstraint());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ForbiddenMethodError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ForbiddenMethodError.java
index 6b497c807..b6f25545d 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ForbiddenMethodError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ForbiddenMethodError.java
@@ -5,23 +5,14 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLMethod;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
import java.util.Collection;
-import java.util.HashSet;
+import java.util.Objects;
public class ForbiddenMethodError extends AbstractError {
private final DeclaredMethod calledMethod;
private final Collection alternatives;
- public ForbiddenMethodError(
- IAnalysisSeed seed,
- Statement errorLocation,
- CrySLRule rule,
- DeclaredMethod calledMethod) {
- this(seed, errorLocation, rule, calledMethod, new HashSet<>());
- }
-
public ForbiddenMethodError(
IAnalysisSeed seed,
Statement errorLocation,
@@ -60,29 +51,15 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), calledMethod, alternatives});
+ return Objects.hash(super.hashCode(), calledMethod, alternatives);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- ForbiddenMethodError other = (ForbiddenMethodError) obj;
- if (calledMethod == null) {
- if (other.getCalledMethod() != null) return false;
- } else if (!calledMethod.equals(other.getCalledMethod())) {
- return false;
- }
-
- if (alternatives == null) {
- if (other.getAlternatives() != null) return false;
- } else if (!alternatives.equals(other.getAlternatives())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof ForbiddenMethodError other
+ && Objects.equals(calledMethod, other.getCalledMethod())
+ && Objects.equals(alternatives, other.getAlternatives());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/HardCodedError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/HardCodedError.java
index 452978b1d..db1715fea 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/HardCodedError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/HardCodedError.java
@@ -4,9 +4,9 @@
import crypto.extractparameter.CallSiteWithExtractedValue;
import crysl.rule.CrySLRule;
import crysl.rule.ISLConstraint;
-import java.util.Arrays;
+import java.util.Objects;
-public class HardCodedError extends AbstractError {
+public class HardCodedError extends AbstractConstraintsError {
private final CallSiteWithExtractedValue extractedValue;
private final ISLConstraint violatedConstraint;
@@ -16,7 +16,7 @@ public HardCodedError(
CallSiteWithExtractedValue cs,
CrySLRule rule,
ISLConstraint constraint) {
- super(seed, cs.getCallSiteWithParam().stmt(), rule);
+ super(seed, cs.callSiteWithParam().statement(), rule);
this.extractedValue = cs;
this.violatedConstraint = constraint;
@@ -37,29 +37,15 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), extractedValue, violatedConstraint});
+ return Objects.hash(super.hashCode(), extractedValue, violatedConstraint);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- HardCodedError other = (HardCodedError) obj;
- if (extractedValue == null) {
- if (other.getExtractedValue() != null) return false;
- } else if (!extractedValue.equals(other.getExtractedValue())) {
- return false;
- }
-
- if (violatedConstraint == null) {
- if (other.getViolatedConstraint() != null) return false;
- } else if (!violatedConstraint.equals(other.getViolatedConstraint())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof HardCodedError other
+ && Objects.equals(extractedValue, other.getExtractedValue())
+ && Objects.equals(violatedConstraint, other.getViolatedConstraint());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ImpreciseValueExtractionError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ImpreciseValueExtractionError.java
index 1dbc26a87..fadfdda96 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/ImpreciseValueExtractionError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/ImpreciseValueExtractionError.java
@@ -4,9 +4,9 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLRule;
import crysl.rule.ISLConstraint;
-import java.util.Arrays;
+import java.util.Objects;
-public class ImpreciseValueExtractionError extends AbstractError {
+public class ImpreciseValueExtractionError extends AbstractConstraintsError {
private final ISLConstraint violatedConstraint;
@@ -29,23 +29,14 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), violatedConstraint});
+ return Objects.hash(super.hashCode(), violatedConstraint);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- ImpreciseValueExtractionError other = (ImpreciseValueExtractionError) obj;
- if (violatedConstraint == null) {
- if (other.violatedConstraint != null) return false;
- } else if (!violatedConstraint.equals(other.violatedConstraint)) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof ImpreciseValueExtractionError other
+ && Objects.equals(violatedConstraint, other.getViolatedConstraint());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java
index 4d59f9ecd..2f48ec82f 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/IncompleteOperationError.java
@@ -5,8 +5,8 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLMethod;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
import java.util.Collection;
+import java.util.Objects;
/**
* This class defines-IncompleteOperationError:
@@ -19,7 +19,7 @@
* decryption, this may render the code dead. This error heavily depends on the computed call graph
* (CHA by default).
*/
-public class IncompleteOperationError extends AbstractError {
+public class IncompleteOperationError extends AbstractOrderError {
private final Collection expectedMethodCalls;
private final boolean multiplePaths;
@@ -112,23 +112,15 @@ private String getErrorMarkerStringForMultipleDataflowPaths() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), expectedMethodCalls, multiplePaths});
+ return Objects.hash(super.hashCode(), expectedMethodCalls, multiplePaths);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- IncompleteOperationError other = (IncompleteOperationError) obj;
- if (expectedMethodCalls == null) {
- if (other.getExpectedMethodCalls() != null) return false;
- } else if (expectedMethodCalls != other.getExpectedMethodCalls()) {
- return false;
- }
-
- return multiplePaths == other.isMultiplePaths();
+ return super.equals(obj)
+ && obj instanceof IncompleteOperationError other
+ && Objects.equals(expectedMethodCalls, other.getExpectedMethodCalls())
+ && multiplePaths == other.isMultiplePaths();
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/InstanceOfError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/InstanceOfError.java
index a558a5ec9..c34e4a6b4 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/InstanceOfError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/InstanceOfError.java
@@ -6,9 +6,9 @@
import crysl.rule.CrySLPredicate;
import crysl.rule.CrySLRule;
import crysl.rule.ISLConstraint;
-import java.util.Arrays;
+import java.util.Objects;
-public class InstanceOfError extends AbstractError {
+public class InstanceOfError extends AbstractConstraintsError {
private final CallSiteWithExtractedValue extractedValue;
private final CrySLPredicate violatedConstraint;
@@ -18,7 +18,7 @@ public InstanceOfError(
CallSiteWithExtractedValue cs,
CrySLRule rule,
CrySLPredicate constraint) {
- super(seed, cs.getCallSiteWithParam().stmt(), rule);
+ super(seed, cs.callSiteWithParam().statement(), rule);
this.extractedValue = cs;
this.violatedConstraint = constraint;
@@ -41,29 +41,15 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), extractedValue, violatedConstraint});
+ return Objects.hash(super.hashCode(), extractedValue, violatedConstraint);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- InstanceOfError other = (InstanceOfError) obj;
- if (extractedValue == null) {
- if (other.getExtractedValue() != null) return false;
- } else if (!extractedValue.equals(other.getExtractedValue())) {
- return false;
- }
-
- if (violatedConstraint == null) {
- if (other.getViolatedConstraint() != null) return false;
- } else if (!violatedConstraint.equals(other.getViolatedConstraint())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof InstanceOfError other
+ && Objects.equals(extractedValue, other.getExtractedValue())
+ && Objects.equals(violatedConstraint, other.getViolatedConstraint());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/NeverTypeOfError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/NeverTypeOfError.java
index e1bc9b033..0eb5e2b0e 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/NeverTypeOfError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/NeverTypeOfError.java
@@ -6,9 +6,9 @@
import crysl.rule.CrySLPredicate;
import crysl.rule.CrySLRule;
import crysl.rule.ISLConstraint;
-import java.util.Arrays;
+import java.util.Objects;
-public class NeverTypeOfError extends AbstractError {
+public class NeverTypeOfError extends AbstractConstraintsError {
private final CallSiteWithExtractedValue extractedValue;
private final CrySLPredicate violatedConstraint;
@@ -18,7 +18,7 @@ public NeverTypeOfError(
CallSiteWithExtractedValue cs,
CrySLRule rule,
CrySLPredicate constraint) {
- super(seed, cs.getCallSiteWithParam().stmt(), rule);
+ super(seed, cs.callSiteWithParam().statement(), rule);
this.extractedValue = cs;
this.violatedConstraint = constraint;
@@ -41,29 +41,15 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), extractedValue, violatedConstraint});
+ return Objects.hash(super.hashCode(), extractedValue, violatedConstraint);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- NeverTypeOfError other = (NeverTypeOfError) obj;
- if (extractedValue == null) {
- if (other.getExtractedValue() != null) return false;
- } else if (!extractedValue.equals(other.getExtractedValue())) {
- return false;
- }
-
- if (violatedConstraint == null) {
- if (other.getViolatedConstraint() != null) return false;
- } else if (!violatedConstraint.equals(other.getViolatedConstraint())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof NeverTypeOfError other
+ && Objects.equals(extractedValue, other.getExtractedValue())
+ && Objects.equals(violatedConstraint, other.getViolatedConstraint());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/NoCallToError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/NoCallToError.java
index 5db72f317..53e69930e 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/NoCallToError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/NoCallToError.java
@@ -3,8 +3,9 @@
import boomerang.scene.Statement;
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLRule;
+import java.util.Objects;
-public class NoCallToError extends AbstractError {
+public class NoCallToError extends AbstractConstraintsError {
public NoCallToError(IAnalysisSeed seed, Statement statement, CrySLRule rule) {
super(seed, statement, rule);
@@ -17,12 +18,12 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return super.hashCode();
+ return Objects.hash(super.hashCode());
}
@Override
public boolean equals(Object obj) {
- return super.equals(obj);
+ return super.equals(obj) && obj instanceof NoCallToError;
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java
new file mode 100644
index 000000000..764464e4b
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateConstraintError.java
@@ -0,0 +1,59 @@
+package crypto.analysis.errors;
+
+import crypto.analysis.AnalysisSeedWithSpecification;
+import crysl.rule.CrySLPredicate;
+import java.util.Objects;
+
+/**
+ * This class represents an internal error if the constraint of a predicate to be ensured is
+ * violated and is only used to propagate HiddenPredicates. For example, we have the following
+ * ENSURES block:
+ *
+ * {@code
+ * ENSURES
+ * algorithm in {"AES"} => generatedKey[...]
+ * }
+ *
+ * If the algorithm is not "AES", the predicate "generatedKey" is not ensured. Instead, the analysis
+ * propagates a HiddenPredicate with the cause that the constraint is not satisfied to have a valid
+ * reason. This class then simply indicates that the predicate's constraint is not satisfied. This
+ * error is/should be not reported.
+ */
+public class PredicateConstraintError extends AbstractError {
+
+ private final CrySLPredicate predicate;
+
+ public PredicateConstraintError(AnalysisSeedWithSpecification seed, CrySLPredicate predicate) {
+ super(seed, seed.getOrigin(), seed.getSpecification());
+
+ this.predicate = predicate;
+ }
+
+ public CrySLPredicate getPredicate() {
+ return predicate;
+ }
+
+ @Override
+ public String toErrorMarkerString() {
+ return "Cannot ensure predicate "
+ + predicate.getPredName()
+ + " because its constraint is not satisfied";
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(super.hashCode(), predicate);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return super.equals(obj)
+ && obj instanceof PredicateConstraintError other
+ && Objects.equals(predicate, other.getPredicate());
+ }
+
+ @Override
+ public String toString() {
+ return "PredicateConstraintError: " + toErrorMarkerString();
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java
index 5cf2f60f7..fa4375904 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/PredicateContradictionError.java
@@ -4,9 +4,9 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLPredicate;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
+import java.util.Objects;
-public class PredicateContradictionError extends AbstractError {
+public class PredicateContradictionError extends AbstractConstraintsError {
private final CrySLPredicate contradictedPredicate;
@@ -31,23 +31,14 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), contradictedPredicate});
+ return Objects.hash(super.hashCode(), contradictedPredicate);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- PredicateContradictionError other = (PredicateContradictionError) obj;
- if (contradictedPredicate == null) {
- if (other.getContradictedPredicate() != null) return false;
- } else if (!contradictedPredicate.equals(other.getContradictedPredicate())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof PredicateContradictionError other
+ && Objects.equals(contradictedPredicate, other.getContradictedPredicate());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java
index 5cee34c21..8fcaa8386 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/RequiredPredicateError.java
@@ -1,67 +1,40 @@
package crypto.analysis.errors;
-import crypto.analysis.AlternativeReqPredicate;
import crypto.analysis.AnalysisSeedWithSpecification;
-import crypto.analysis.HiddenPredicate;
import crypto.analysis.RequiredCrySLPredicate;
+import crypto.analysis.UnEnsuredPredicate;
import crysl.rule.CrySLPredicate;
-import java.util.Arrays;
import java.util.Collection;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.stream.Collectors;
+import java.util.Objects;
/**
- * Creates {@link RequiredPredicateError} for all Required Predicate error generates
- * RequiredPredicateError
+ * This error models the violation of predicates from the REQUIRES section. An error is only
+ * reported for single predicates, that is, predicates of the form
+ *
+ * {@code
+ * REQUIRES
+ * generatedKey[...];
+ * }
+ *
+ * If a predicate has alternatives, an {@link AlternativeReqPredicateError} is reported.
*/
-public class RequiredPredicateError extends AbstractError {
+public class RequiredPredicateError extends AbstractRequiredPredicateError {
- private final Collection hiddenPredicates;
- private final Collection contradictedPredicates;
+ private final CrySLPredicate contradictedPredicate;
private final int paramIndex;
public RequiredPredicateError(
- AnalysisSeedWithSpecification seed, RequiredCrySLPredicate violatedPred) {
- super(seed, violatedPred.getLocation(), seed.getSpecification());
+ AnalysisSeedWithSpecification seed,
+ RequiredCrySLPredicate violatedPred,
+ Collection unEnsuredPredicates) {
+ super(seed, violatedPred.getLocation(), seed.getSpecification(), unEnsuredPredicates);
- this.hiddenPredicates = new HashSet<>();
- this.contradictedPredicates = Collections.singletonList(violatedPred.getPred());
+ this.contradictedPredicate = violatedPred.getPred();
this.paramIndex = violatedPred.getParamIndex();
}
- public RequiredPredicateError(
- AnalysisSeedWithSpecification seed, AlternativeReqPredicate violatedPred) {
- super(seed, violatedPred.getLocation(), seed.getSpecification());
-
- this.hiddenPredicates = new HashSet<>();
- this.contradictedPredicates = violatedPred.getAlternatives();
- this.paramIndex = violatedPred.getParamIndex();
- }
-
- public void addHiddenPredicates(Collection hiddenPredicates) {
- this.hiddenPredicates.addAll(hiddenPredicates);
- }
-
- public void mapPrecedingErrors() {
- for (HiddenPredicate hiddenPredicate : hiddenPredicates) {
- Collection precedingErrors = hiddenPredicate.getPrecedingErrors();
- this.addCausingError(precedingErrors);
- precedingErrors.forEach(e -> e.addSubsequentError(this));
- }
- }
-
- /**
- * This method returns a list of contradicting predicates
- *
- * @return list of contradicting predicates
- */
- public Collection getContradictedPredicates() {
- return contradictedPredicates;
- }
-
- public Collection getHiddenPredicates() {
- return hiddenPredicates;
+ public CrySLPredicate getContradictedPredicates() {
+ return contradictedPredicate;
}
public int getParamIndex() {
@@ -70,13 +43,9 @@ public int getParamIndex() {
@Override
public String toErrorMarkerString() {
- StringBuilder msg = new StringBuilder(getParamIndexAsText());
+ StringBuilder msg = new StringBuilder(getParamIndexAsText(paramIndex));
msg.append(" was not properly generated as ");
- String predicateName =
- getContradictedPredicates().stream()
- .map(CrySLPredicate::getPredName)
- .collect(Collectors.joining(" OR "));
- String[] parts = predicateName.split("(?=[A-Z])");
+ String[] parts = contradictedPredicate.getPredName().split("(?=[A-Z])");
msg.append(parts[0]);
for (int i = 1; i < parts.length; i++) {
msg.append(parts[i]);
@@ -84,65 +53,17 @@ public String toErrorMarkerString() {
return msg.toString();
}
- private String getParamIndexAsText() {
- String res;
- switch (paramIndex) {
- case -1:
- return "Return value";
- case 0:
- res = "First ";
- break;
- case 1:
- res = "Second ";
- break;
- case 2:
- res = "Third ";
- break;
- case 3:
- res = "Fourth ";
- break;
- case 4:
- res = "Fifth ";
- break;
- case 5:
- res = "Sixth ";
- break;
- default:
- res = (paramIndex + 1) + "th ";
- break;
- }
- res += "parameter";
- return res;
- }
-
@Override
public int hashCode() {
- return Arrays.hashCode(
- new Object[] {
- super.hashCode(), hiddenPredicates, contradictedPredicates, paramIndex
- });
+ return Objects.hash(super.hashCode(), contradictedPredicate, paramIndex);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- RequiredPredicateError other = (RequiredPredicateError) obj;
- if (hiddenPredicates == null) {
- if (other.getHiddenPredicates() != null) return false;
- } else if (!hiddenPredicates.equals(other.hiddenPredicates)) {
- return false;
- }
-
- if (contradictedPredicates == null) {
- if (other.getContradictedPredicates() != null) return false;
- } else if (!contradictedPredicates.equals(other.getContradictedPredicates())) {
- return false;
- }
-
- return paramIndex == other.getParamIndex();
+ return super.equals(obj)
+ && obj instanceof RequiredPredicateError other
+ && Objects.equals(contradictedPredicate, other.getContradictedPredicates())
+ && paramIndex == other.getParamIndex();
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/TypestateError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/TypestateError.java
index 632a0bd33..750095f91 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/TypestateError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/TypestateError.java
@@ -4,10 +4,10 @@
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLMethod;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
import java.util.Collection;
+import java.util.Objects;
-public class TypestateError extends AbstractError {
+public class TypestateError extends AbstractOrderError {
private final Collection expectedMethodCalls;
@@ -44,23 +44,14 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), expectedMethodCalls});
+ return Objects.hash(super.hashCode(), expectedMethodCalls);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- TypestateError other = (TypestateError) obj;
- if (expectedMethodCalls == null) {
- if (other.getExpectedMethodCalls() != null) return false;
- } else if (!expectedMethodCalls.equals(other.getExpectedMethodCalls())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof TypestateError other
+ && Objects.equals(expectedMethodCalls, other.getExpectedMethodCalls());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/errors/UncaughtExceptionError.java b/CryptoAnalysis/src/main/java/crypto/analysis/errors/UncaughtExceptionError.java
index 31b57b360..bf98725a5 100644
--- a/CryptoAnalysis/src/main/java/crypto/analysis/errors/UncaughtExceptionError.java
+++ b/CryptoAnalysis/src/main/java/crypto/analysis/errors/UncaughtExceptionError.java
@@ -4,7 +4,7 @@
import boomerang.scene.WrappedClass;
import crypto.analysis.IAnalysisSeed;
import crysl.rule.CrySLRule;
-import java.util.Arrays;
+import java.util.Objects;
public class UncaughtExceptionError extends AbstractError {
@@ -27,22 +27,13 @@ public String toErrorMarkerString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), exception});
+ return Objects.hash(super.hashCode(), exception);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- UncaughtExceptionError other = (UncaughtExceptionError) obj;
- if (exception == null) {
- if (other.getException() != null) return false;
- } else if (!exception.equals(other.getException())) {
- return false;
- }
-
- return true;
+ return super.equals(obj)
+ && obj instanceof UncaughtExceptionError other
+ && Objects.equals(exception, other.getException());
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/ComparisonConstraint.java b/CryptoAnalysis/src/main/java/crypto/constraints/ComparisonConstraint.java
index 95d137ecc..54e914ad3 100644
--- a/CryptoAnalysis/src/main/java/crypto/constraints/ComparisonConstraint.java
+++ b/CryptoAnalysis/src/main/java/crypto/constraints/ComparisonConstraint.java
@@ -183,8 +183,8 @@ private Map extractValueAsInt(
try {
for (Map.Entry value :
valueCollection.entrySet()) {
- ExtractedValue extractedValue = value.getValue().getExtractedValue();
- if (extractedValue.getVal().equals(Val.zero())) {
+ ExtractedValue extractedValue = value.getValue().extractedValue();
+ if (extractedValue.val().equals(Val.zero())) {
continue;
}
diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java b/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java
index 226ecaa03..08d60c0a3 100644
--- a/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java
+++ b/CryptoAnalysis/src/main/java/crypto/constraints/ConstraintSolver.java
@@ -5,7 +5,6 @@
import boomerang.scene.DataFlowScope;
import boomerang.scene.Statement;
import boomerang.scene.sparse.SparseCFGCache;
-import com.google.common.collect.Lists;
import crypto.analysis.AlternativeReqPredicate;
import crypto.analysis.AnalysisSeedWithSpecification;
import crypto.analysis.RequiredCrySLPredicate;
@@ -23,7 +22,9 @@
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
+import java.util.Collections;
import java.util.HashSet;
+import java.util.List;
public class ConstraintSolver {
@@ -153,16 +154,15 @@ private void partitionConstraints() {
Collection involvedVarNames = new HashSet<>(cons.getInvolvedVarNames());
for (CallSiteWithExtractedValue callSite : this.getCollectedValues()) {
- CallSiteWithParamIndex callSiteWithParamIndex = callSite.getCallSiteWithParam();
- involvedVarNames.remove(callSiteWithParamIndex.getVarName());
+ CallSiteWithParamIndex callSiteWithParamIndex = callSite.callSiteWithParam();
+ involvedVarNames.remove(callSiteWithParamIndex.varName());
}
if (!involvedVarNames.isEmpty()) {
continue;
}
- if (cons instanceof CrySLPredicate) {
- CrySLPredicate predicate = (CrySLPredicate) cons;
+ if (cons instanceof CrySLPredicate predicate) {
if (predefinedPreds.contains(predicate.getPredName())) {
relConstraints.add(predicate);
continue;
@@ -178,14 +178,31 @@ private void partitionConstraints() {
requiredPredicates.add(pred);
}
}
- } else if (cons instanceof CrySLConstraint) {
- ISLConstraint left = ((CrySLConstraint) cons).getLeft();
+ } else if (cons instanceof CrySLConstraint constraint) {
+ ISLConstraint left = constraint.getLeft();
if (left instanceof CrySLPredicate
&& !predefinedPreds.contains(((CrySLPredicate) left).getPredName())) {
- requiredPredicates.addAll(
- collectAlternativePredicates(
- (CrySLConstraint) cons, new ArrayList<>()));
+
+ List allAlts = new ArrayList<>();
+ extractAlternativePredicates(constraint, allAlts);
+ Collections.reverse(allAlts);
+
+ if (allAlts.isEmpty()) {
+ continue;
+ }
+
+ // Use the left pred as the base predicate to determine the statement
+ Collection basePreds =
+ retrieveValuesForPred(allAlts.get(0));
+ for (RequiredCrySLPredicate reqPred : basePreds) {
+ Collection relAlts =
+ getRelevantPredicates(reqPred, allAlts);
+
+ AlternativeReqPredicate altPred =
+ new AlternativeReqPredicate(reqPred, allAlts, relAlts);
+ requiredPredicates.add(altPred);
+ }
} else {
relConstraints.add(cons);
}
@@ -195,56 +212,40 @@ private void partitionConstraints() {
}
}
- private Collection collectAlternativePredicates(
- CrySLConstraint cons, Collection alts) {
+ private void extractAlternativePredicates(CrySLConstraint cons, List alts) {
CrySLPredicate left = (CrySLPredicate) cons.getLeft();
+ alts.add(left);
- if (alts.isEmpty()) {
- for (CallSiteWithExtractedValue callSite : this.getCollectedValues()) {
- CallSiteWithParamIndex cwpi = callSite.getCallSiteWithParam();
-
- for (ICrySLPredicateParameter p : left.getParameters()) {
- if (p.getName().equals("transformation")) {
- continue;
- }
+ ISLConstraint right = cons.getRight();
+ if (right instanceof CrySLPredicate predicate) {
+ alts.add(predicate);
+ } else if (right instanceof CrySLConstraint constraint) {
+ extractAlternativePredicates(constraint, alts);
+ }
+ }
- if (cwpi.getVarName().equals(p.getName())) {
- alts.add(new AlternativeReqPredicate(left, cwpi.stmt(), cwpi.getIndex()));
- }
- }
- }
+ private Collection getRelevantPredicates(
+ RequiredCrySLPredicate basePred, Collection predicates) {
+ Collection result = new HashSet<>();
- // Extract predicates with 'this' as parameter
- if (left.getParameters().stream().anyMatch(param -> param.getName().equals("this"))) {
- AlternativeReqPredicate altPred =
- new AlternativeReqPredicate(left, seed.getOrigin(), -1);
+ for (CrySLPredicate pred : predicates) {
+ Collection reqPreds = retrieveValuesForPred(pred);
- if (!alts.contains(altPred)) {
- alts.add(altPred);
+ for (RequiredCrySLPredicate reqPred : reqPreds) {
+ if (reqPred.getLocation().equals(basePred.getLocation())) {
+ result.add(reqPred);
}
}
- } else {
- for (AlternativeReqPredicate alt : alts) {
- alt.addAlternative(left);
- }
}
- if (cons.getRight() instanceof CrySLPredicate) {
- for (AlternativeReqPredicate alt : alts) {
- alt.addAlternative((CrySLPredicate) cons.getRight());
- }
- } else {
- return collectAlternativePredicates((CrySLConstraint) cons.getRight(), alts);
- }
-
- return alts;
+ return result;
}
private Collection retrieveValuesForPred(CrySLPredicate pred) {
- Collection result = Lists.newArrayList();
+ Collection result = new ArrayList<>();
for (CallSiteWithExtractedValue callSite : this.getCollectedValues()) {
- CallSiteWithParamIndex cwpi = callSite.getCallSiteWithParam();
+ CallSiteWithParamIndex cwpi = callSite.callSiteWithParam();
for (ICrySLPredicateParameter p : pred.getParameters()) {
// TODO: FIX Cipher rule
@@ -253,12 +254,12 @@ private Collection retrieveValuesForPred(CrySLPredicate
}
// Predicates with _ can have any type
- if (cwpi.getVarName().equals("_")) {
+ if (cwpi.varName().equals("_")) {
continue;
}
- if (cwpi.getVarName().equals(p.getName())) {
- result.add(new RequiredCrySLPredicate(pred, cwpi.stmt(), cwpi.getIndex()));
+ if (cwpi.varName().equals(p.getName())) {
+ result.add(new RequiredCrySLPredicate(pred, cwpi.statement(), cwpi.index()));
}
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/EvaluableConstraint.java b/CryptoAnalysis/src/main/java/crypto/constraints/EvaluableConstraint.java
index 9cf077312..84da0248f 100644
--- a/CryptoAnalysis/src/main/java/crypto/constraints/EvaluableConstraint.java
+++ b/CryptoAnalysis/src/main/java/crypto/constraints/EvaluableConstraint.java
@@ -75,25 +75,25 @@ protected Collection getErrors() {
protected Map extractValueAsString(String varName) {
Map varVal = Maps.newHashMap();
for (CallSiteWithExtractedValue callSite : context.getCollectedValues()) {
- CallSiteWithParamIndex wrappedCallSite = callSite.getCallSiteWithParam();
- Statement statement = wrappedCallSite.stmt();
+ CallSiteWithParamIndex wrappedCallSite = callSite.callSiteWithParam();
+ Statement statement = wrappedCallSite.statement();
- if (!wrappedCallSite.getVarName().equals(varName)) {
+ if (!wrappedCallSite.varName().equals(varName)) {
continue;
}
- ExtractedValue extractedValue = callSite.getExtractedValue();
- Statement allocSite = extractedValue.getInitialStatement();
+ ExtractedValue extractedValue = callSite.extractedValue();
+ Statement allocSite = extractedValue.initialStatement();
InvokeExpr invoker = statement.getInvokeExpr();
if (statement.equals(allocSite)) {
String constant =
- retrieveConstantFromValue(invoker.getArg(wrappedCallSite.getIndex()));
+ retrieveConstantFromValue(invoker.getArg(wrappedCallSite.index()));
varVal.put(constant, callSite);
} else if (allocSite.isAssign()) {
- if (extractedValue.getVal().isConstant()) {
+ if (extractedValue.val().isConstant()) {
String retrieveConstantFromValue =
- retrieveConstantFromValue(extractedValue.getVal());
+ retrieveConstantFromValue(extractedValue.val());
int pos = -1;
for (int i = 0; i < invoker.getArgs().size(); i++) {
@@ -114,7 +114,7 @@ protected Map extractValueAsString(String va
retrieveConstantFromValue,
new CallSiteWithExtractedValue(wrappedCallSite, extractedValue));
}
- } else if (extractedValue.getVal().isNewExpr()) {
+ } else if (extractedValue.val().isNewExpr()) {
varVal.putAll(extractSootArray(wrappedCallSite, extractedValue));
}
}
@@ -131,8 +131,8 @@ protected Map extractValueAsString(String va
*/
protected Map extractSootArray(
CallSiteWithParamIndex callSite, ExtractedValue allocSite) {
- Val arrayLocal = allocSite.getVal();
- Method method = callSite.stmt().getMethod();
+ Val arrayLocal = allocSite.val();
+ Method method = callSite.statement().getMethod();
Map arrVal = Maps.newHashMap();
@@ -186,7 +186,7 @@ private String retrieveConstantFromValue(Val val) {
protected Map extractArray(ExtractedValue extractedValue) {
Map result = new HashMap<>();
- Statement statement = extractedValue.getInitialStatement();
+ Statement statement = extractedValue.initialStatement();
if (!statement.isAssign()) {
return result;
}
@@ -269,8 +269,8 @@ protected boolean couldNotExtractValues(
}
for (CallSiteWithExtractedValue callSite : extractedValueMap.values()) {
- Statement statement = callSite.getCallSiteWithParam().stmt();
- Val extractedVal = callSite.getExtractedValue().getVal();
+ Statement statement = callSite.callSiteWithParam().statement();
+ Val extractedVal = callSite.extractedValue().val();
if (extractedVal.equals(Val.zero())) {
ImpreciseValueExtractionError extractionError =
diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/PredicateConstraint.java b/CryptoAnalysis/src/main/java/crypto/constraints/PredicateConstraint.java
index a5e4e8c3f..dc0cebaa6 100644
--- a/CryptoAnalysis/src/main/java/crypto/constraints/PredicateConstraint.java
+++ b/CryptoAnalysis/src/main/java/crypto/constraints/PredicateConstraint.java
@@ -123,13 +123,13 @@ private void evaluateNeverTypeOfPredicate(CrySLPredicate neverTypeOfPredicate) {
CrySLObject parameterType = objects.get(1);
for (CallSiteWithExtractedValue callSite : context.getCollectedValues()) {
- CallSiteWithParamIndex cs = callSite.getCallSiteWithParam();
+ CallSiteWithParamIndex cs = callSite.callSiteWithParam();
- if (!variable.getName().equals(cs.getVarName())) {
+ if (!variable.getName().equals(cs.varName())) {
continue;
}
- Collection types = callSite.getExtractedValue().getTypes();
+ Collection types = callSite.extractedValue().types();
for (Type type : types) {
if (!parameterType.getJavaType().equals(type.toString())) {
continue;
@@ -157,13 +157,13 @@ private void evaluateHardCodedPredicate(CrySLPredicate hardCodedPredicate) {
CrySLObject variable = objects.get(0);
for (CallSiteWithExtractedValue callSite : context.getCollectedValues()) {
- CallSiteWithParamIndex cs = callSite.getCallSiteWithParam();
+ CallSiteWithParamIndex cs = callSite.callSiteWithParam();
- if (!variable.getVarName().equals(cs.getVarName())) {
+ if (!variable.getVarName().equals(cs.varName())) {
continue;
}
- ExtractedValue extractedValue = callSite.getExtractedValue();
+ ExtractedValue extractedValue = callSite.extractedValue();
if (isHardCodedVariable(extractedValue) || isHardCodedArray(extractedValue)) {
HardCodedError hardCodedError =
new HardCodedError(
@@ -188,14 +188,14 @@ private void evaluateInstanceOfPredicate(CrySLPredicate instanceOfPredicate) {
CrySLObject parameterType = objects.get(1);
for (CallSiteWithExtractedValue callSite : context.getCollectedValues()) {
- CallSiteWithParamIndex cs = callSite.getCallSiteWithParam();
+ CallSiteWithParamIndex cs = callSite.callSiteWithParam();
- if (!variable.getName().equals(cs.getVarName())) {
+ if (!variable.getName().equals(cs.varName())) {
continue;
}
boolean isSubType = false;
- Collection types = callSite.getExtractedValue().getTypes();
+ Collection types = callSite.extractedValue().types();
for (Type type : types) {
if (type.isNullType()) {
continue;
@@ -250,26 +250,26 @@ private List parametersToCryslObjects(
public boolean isHardCodedVariable(ExtractedValue val) {
// Check for basic constants
- if (val.getVal().isConstant()) {
- LOGGER.debug("Value {} is hard coded", val.getVal());
+ if (val.val().isConstant()) {
+ LOGGER.debug("Value {} is hard coded", val.val());
return true;
}
- Statement statement = val.getInitialStatement();
+ Statement statement = val.initialStatement();
// Objects initialized with 'new' are hard coded
if (!statement.isAssign()) {
- LOGGER.debug("Value {} is not hard coded", val.getVal());
+ LOGGER.debug("Value {} is not hard coded", val.val());
return false;
}
Val rightOp = statement.getRightOp();
if (rightOp.isNewExpr()) {
- LOGGER.debug("Value {} is hard coded", val.getVal());
+ LOGGER.debug("Value {} is hard coded", val.val());
return true;
}
- LOGGER.debug("Value {} is not hard coded", val.getVal());
+ LOGGER.debug("Value {} is not hard coded", val.val());
return false;
}
diff --git a/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java b/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java
index cac54f0de..7e10c8ed4 100644
--- a/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java
+++ b/CryptoAnalysis/src/main/java/crypto/constraints/ValueConstraint.java
@@ -10,7 +10,6 @@
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
-import java.util.stream.Collectors;
public class ValueConstraint extends EvaluableConstraint {
@@ -28,9 +27,7 @@ public void evaluate() {
}
List lowerCaseValues =
- valCons.getValueRange().parallelStream()
- .map(String::toLowerCase)
- .collect(Collectors.toList());
+ valCons.getValueRange().parallelStream().map(String::toLowerCase).toList();
for (Map.Entry val : values) {
if (!lowerCaseValues.contains(val.getKey().toLowerCase())) {
ConstraintError error =
diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithExtractedValue.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithExtractedValue.java
index fe26c6ead..59debc10a 100644
--- a/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithExtractedValue.java
+++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithExtractedValue.java
@@ -1,31 +1,14 @@
package crypto.extractparameter;
import boomerang.scene.Val;
-import java.util.Arrays;
-public class CallSiteWithExtractedValue {
-
- private final CallSiteWithParamIndex callSiteWithParam;
- private final ExtractedValue extractedValue;
-
- public CallSiteWithExtractedValue(
- CallSiteWithParamIndex callSiteWithParam, ExtractedValue extractedValue) {
- this.callSiteWithParam = callSiteWithParam;
- this.extractedValue = extractedValue;
- }
-
- public CallSiteWithParamIndex getCallSiteWithParam() {
- return callSiteWithParam;
- }
-
- public ExtractedValue getExtractedValue() {
- return extractedValue;
- }
+public record CallSiteWithExtractedValue(
+ CallSiteWithParamIndex callSiteWithParam, ExtractedValue extractedValue) {
@Override
public String toString() {
String res;
- switch (callSiteWithParam.getIndex()) {
+ switch (callSiteWithParam.index()) {
case -1:
return "Return value";
case 0:
@@ -47,12 +30,12 @@ public String toString() {
res = "Sixth ";
break;
default:
- res = (callSiteWithParam.getIndex() + 1) + "th ";
+ res = (callSiteWithParam.index() + 1) + "th ";
break;
}
res += "parameter";
if (extractedValue != null) {
- Val allocVal = extractedValue.getVal();
+ Val allocVal = extractedValue.val();
if (allocVal.isConstant()) {
res += " (with value " + allocVal.getVariableName() + ")";
@@ -60,31 +43,4 @@ public String toString() {
}
return res;
}
-
- @Override
- public int hashCode() {
- return Arrays.hashCode(new Object[] {callSiteWithParam, extractedValue});
- }
-
- @Override
- public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
-
- CallSiteWithExtractedValue other = (CallSiteWithExtractedValue) obj;
- if (callSiteWithParam == null) {
- if (other.getCallSiteWithParam() != null) return false;
- } else if (!callSiteWithParam.equals(other.getCallSiteWithParam())) {
- return false;
- }
-
- if (extractedValue == null) {
- if (other.getExtractedValue() != null) return false;
- } else if (!extractedValue.equals(other.getExtractedValue())) {
- return false;
- }
-
- return true;
- }
}
diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithParamIndex.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithParamIndex.java
index 64646bbac..27e9a9d32 100644
--- a/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithParamIndex.java
+++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/CallSiteWithParamIndex.java
@@ -1,65 +1,11 @@
package crypto.extractparameter;
import boomerang.scene.Statement;
-import boomerang.scene.Val;
-public class CallSiteWithParamIndex {
-
- private final Statement statement;
- private final Val fact;
- private final String varName;
- private final int index;
-
- public CallSiteWithParamIndex(Statement statement, Val fact, int index, String varName) {
- this.statement = statement;
- this.fact = fact;
- this.index = index;
- this.varName = varName;
- }
-
- public Statement stmt() {
- return statement;
- }
-
- public Val fact() {
- return fact;
- }
-
- public int getIndex() {
- return index;
- }
-
- public String getVarName() {
- return varName;
- }
+public record CallSiteWithParamIndex(Statement statement, int index, String varName) {
@Override
public String toString() {
- return varName + " at " + stmt() + " and " + index;
- }
-
- @Override
- public int hashCode() {
- final int prime = 31;
- int result = 1;
- result = prime * result + index;
- result = prime * result + ((statement == null) ? 0 : statement.hashCode());
- result = prime * result + ((varName == null) ? 0 : varName.hashCode());
- return result;
- }
-
- @Override
- public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
- CallSiteWithParamIndex other = (CallSiteWithParamIndex) obj;
- if (index != other.index) return false;
- if (statement == null) {
- if (other.statement != null) return false;
- } else if (!statement.equals(other.statement)) return false;
- if (varName == null) {
- return other.varName == null;
- } else return varName.equals(other.varName);
+ return varName + " at " + statement + " and " + index;
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterAnalysis.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterAnalysis.java
index 3bb54bc2a..940f23d7d 100644
--- a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterAnalysis.java
+++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterAnalysis.java
@@ -78,9 +78,7 @@ private void addQueryAtCallSite(Statement statement, String varNameInSpec, int i
for (ForwardQuery paramQuery : filteredQueries) {
Val val = paramQuery.var();
- if (val instanceof AllocVal) {
- AllocVal allocVal = (AllocVal) val;
-
+ if (val instanceof AllocVal allocVal) {
Map.Entry entry =
new AbstractMap.SimpleEntry<>(
allocVal.getAllocVal(),
@@ -95,8 +93,7 @@ private void addQueryAtCallSite(Statement statement, String varNameInSpec, int i
}
CallSiteWithParamIndex callSiteWithParam =
- new CallSiteWithParamIndex(
- statement, parameter, index, varNameInSpec);
+ new CallSiteWithParamIndex(statement, index, varNameInSpec);
Collection types = results.getPropagationType();
// If no value could be extracted, add the zero value to indicate it
diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterQuery.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterQuery.java
index 04a6dfea1..c09dbddfd 100644
--- a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterQuery.java
+++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractParameterQuery.java
@@ -5,9 +5,9 @@
import boomerang.results.BackwardBoomerangResults;
import boomerang.scene.ControlFlowGraph;
import boomerang.scene.Val;
-import java.util.Arrays;
import java.util.Collection;
import java.util.HashSet;
+import java.util.Objects;
import wpds.impl.Weight;
public class ExtractParameterQuery extends BackwardQuery {
@@ -62,15 +62,13 @@ public String toString() {
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), index});
+ return Objects.hash(super.hashCode(), index);
}
@Override
public boolean equals(Object obj) {
- if (!super.equals(obj)) return false;
- if (getClass() != obj.getClass()) return false;
-
- ExtractParameterQuery other = (ExtractParameterQuery) obj;
- return index == other.index;
+ return super.equals(obj)
+ && obj instanceof ExtractParameterQuery other
+ && index == other.index;
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractedValue.java b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractedValue.java
index 296a95029..9915dc2fd 100644
--- a/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractedValue.java
+++ b/CryptoAnalysis/src/main/java/crypto/extractparameter/ExtractedValue.java
@@ -3,68 +3,12 @@
import boomerang.scene.Statement;
import boomerang.scene.Type;
import boomerang.scene.Val;
-import java.util.Arrays;
import java.util.Collection;
-public class ExtractedValue {
-
- private final Val val;
- private final Statement initialStatement;
- private final Collection types;
-
- public ExtractedValue(Val val, Statement initialStatement, Collection types) {
- this.val = val;
- this.initialStatement = initialStatement;
- this.types = types;
- }
-
- public Val getVal() {
- return val;
- }
-
- public Statement getInitialStatement() {
- return initialStatement;
- }
-
- public Collection getTypes() {
- return types;
- }
+public record ExtractedValue(Val val, Statement initialStatement, Collection types) {
@Override
public String toString() {
- return "Extracted Value: " + val + " with type " + types;
- }
-
- @Override
- public int hashCode() {
- return Arrays.hashCode(new Object[] {val, initialStatement, types});
- }
-
- @Override
- public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
-
- ExtractedValue other = (ExtractedValue) obj;
- if (val == null) {
- if (other.getVal() != null) return false;
- } else if (!val.equals(other.getVal())) {
- return false;
- }
-
- if (initialStatement == null) {
- if (other.getInitialStatement() != null) return false;
- } else if (!initialStatement.equals(other.getInitialStatement())) {
- return false;
- }
-
- if (types == null) {
- if (other.getTypes() != null) return false;
- } else if (!types.equals(other.getTypes())) {
- return false;
- }
-
- return true;
+ return "Extracted Value: " + val + " with types " + types;
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java b/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java
index 049f8ffd5..aafd27500 100644
--- a/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java
+++ b/CryptoAnalysis/src/main/java/crypto/listener/AnalysisReporter.java
@@ -6,9 +6,11 @@
import boomerang.scene.Statement;
import boomerang.scene.Val;
import com.google.common.collect.Multimap;
-import crypto.analysis.EnsuredCrySLPredicate;
+import crypto.analysis.AbstractPredicate;
+import crypto.analysis.EnsuredPredicate;
import crypto.analysis.IAnalysisSeed;
import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AlternativeReqPredicateError;
import crypto.analysis.errors.CallToError;
import crypto.analysis.errors.ConstraintError;
import crypto.analysis.errors.ForbiddenMethodError;
@@ -183,7 +185,7 @@ public void afterPredicateCheck() {
public void onGeneratedPredicate(
IAnalysisSeed fromSeed,
- EnsuredCrySLPredicate predicate,
+ AbstractPredicate predicate,
IAnalysisSeed toPred,
Statement statement) {
for (IResultsListener listener : resultsListeners) {
@@ -222,60 +224,45 @@ public void checkedConstraints(
public void ensuredPredicates(
IAnalysisSeed seed,
- Multimap> predicates) {
+ Multimap> predicates) {
for (IResultsListener listener : resultsListeners) {
listener.ensuredPredicates(seed, predicates);
}
}
public void reportError(IAnalysisSeed seed, AbstractError error) {
- seed.setSecure(false);
-
for (IAnalysisListener analysisListener : analysisListeners) {
analysisListener.onReportedError(seed, error);
}
for (IErrorListener errorListener : errorListeners) {
- if (error instanceof CallToError) {
- CallToError callToError = (CallToError) error;
+ if (error instanceof CallToError callToError) {
errorListener.reportError(callToError);
- } else if (error instanceof ConstraintError) {
- ConstraintError constraintError = (ConstraintError) error;
+ } else if (error instanceof ConstraintError constraintError) {
errorListener.reportError(constraintError);
- } else if (error instanceof ForbiddenMethodError) {
- ForbiddenMethodError forbiddenMethodError = (ForbiddenMethodError) error;
+ } else if (error instanceof ForbiddenMethodError forbiddenMethodError) {
errorListener.reportError(forbiddenMethodError);
- } else if (error instanceof HardCodedError) {
- HardCodedError hardCodedError = (HardCodedError) error;
+ } else if (error instanceof HardCodedError hardCodedError) {
errorListener.reportError(hardCodedError);
- } else if (error instanceof ImpreciseValueExtractionError) {
- ImpreciseValueExtractionError impreciseError =
- (ImpreciseValueExtractionError) error;
+ } else if (error instanceof ImpreciseValueExtractionError impreciseError) {
errorListener.reportError(impreciseError);
- } else if (error instanceof IncompleteOperationError) {
- IncompleteOperationError incompleteError = (IncompleteOperationError) error;
+ } else if (error instanceof IncompleteOperationError incompleteError) {
errorListener.reportError(incompleteError);
- } else if (error instanceof InstanceOfError) {
- InstanceOfError instanceOfError = (InstanceOfError) error;
+ } else if (error instanceof InstanceOfError instanceOfError) {
errorListener.reportError(instanceOfError);
- } else if (error instanceof NeverTypeOfError) {
- NeverTypeOfError neverTypeOfError = (NeverTypeOfError) error;
+ } else if (error instanceof NeverTypeOfError neverTypeOfError) {
errorListener.reportError(neverTypeOfError);
- } else if (error instanceof NoCallToError) {
- NoCallToError noCallToError = (NoCallToError) error;
+ } else if (error instanceof NoCallToError noCallToError) {
errorListener.reportError(noCallToError);
- } else if (error instanceof PredicateContradictionError) {
- PredicateContradictionError contradictionError =
- (PredicateContradictionError) error;
+ } else if (error instanceof PredicateContradictionError contradictionError) {
errorListener.reportError(contradictionError);
- } else if (error instanceof RequiredPredicateError) {
- RequiredPredicateError predicateError = (RequiredPredicateError) error;
+ } else if (error instanceof RequiredPredicateError predicateError) {
+ errorListener.reportError(predicateError);
+ } else if (error instanceof AlternativeReqPredicateError predicateError) {
errorListener.reportError(predicateError);
- } else if (error instanceof TypestateError) {
- TypestateError typestateError = (TypestateError) error;
+ } else if (error instanceof TypestateError typestateError) {
errorListener.reportError(typestateError);
- } else if (error instanceof UncaughtExceptionError) {
- UncaughtExceptionError exceptionError = (UncaughtExceptionError) error;
+ } else if (error instanceof UncaughtExceptionError exceptionError) {
errorListener.reportError(exceptionError);
} else {
errorListener.reportError(error);
diff --git a/CryptoAnalysis/src/main/java/crypto/listener/ErrorCollector.java b/CryptoAnalysis/src/main/java/crypto/listener/ErrorCollector.java
index 90e408c7f..1f901da2f 100644
--- a/CryptoAnalysis/src/main/java/crypto/listener/ErrorCollector.java
+++ b/CryptoAnalysis/src/main/java/crypto/listener/ErrorCollector.java
@@ -5,6 +5,7 @@
import com.google.common.collect.HashBasedTable;
import com.google.common.collect.Table;
import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AlternativeReqPredicateError;
import crypto.analysis.errors.CallToError;
import crypto.analysis.errors.ConstraintError;
import crypto.analysis.errors.ForbiddenMethodError;
@@ -98,6 +99,11 @@ public void reportError(RequiredPredicateError requiredPredicateError) {
addErrorToCollection(requiredPredicateError);
}
+ @Override
+ public void reportError(AlternativeReqPredicateError alternativeReqPredicateError) {
+ addErrorToCollection(alternativeReqPredicateError);
+ }
+
@Override
public void reportError(TypestateError typestateError) {
addErrorToCollection(typestateError);
diff --git a/CryptoAnalysis/src/main/java/crypto/listener/IErrorListener.java b/CryptoAnalysis/src/main/java/crypto/listener/IErrorListener.java
index 0a75f890f..2fe5798d4 100644
--- a/CryptoAnalysis/src/main/java/crypto/listener/IErrorListener.java
+++ b/CryptoAnalysis/src/main/java/crypto/listener/IErrorListener.java
@@ -1,6 +1,7 @@
package crypto.listener;
import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AlternativeReqPredicateError;
import crypto.analysis.errors.CallToError;
import crypto.analysis.errors.ConstraintError;
import crypto.analysis.errors.ForbiddenMethodError;
@@ -39,6 +40,8 @@ public interface IErrorListener {
void reportError(RequiredPredicateError requiredPredicateError);
+ void reportError(AlternativeReqPredicateError alternativeReqPredicateError);
+
void reportError(TypestateError typestateError);
void reportError(UncaughtExceptionError uncaughtExceptionError);
diff --git a/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java b/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java
index aaef32b58..b77023344 100644
--- a/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java
+++ b/CryptoAnalysis/src/main/java/crypto/listener/IResultsListener.java
@@ -5,7 +5,8 @@
import boomerang.scene.CallGraph;
import boomerang.scene.Statement;
import com.google.common.collect.Multimap;
-import crypto.analysis.EnsuredCrySLPredicate;
+import crypto.analysis.AbstractPredicate;
+import crypto.analysis.EnsuredPredicate;
import crypto.analysis.IAnalysisSeed;
import crypto.analysis.errors.AbstractError;
import crypto.extractparameter.CallSiteWithExtractedValue;
@@ -36,11 +37,11 @@ void checkedConstraints(
void generatedPredicate(
IAnalysisSeed fromSeed,
- EnsuredCrySLPredicate predicate,
+ AbstractPredicate predicate,
IAnalysisSeed toSeed,
Statement statement);
void ensuredPredicates(
IAnalysisSeed seed,
- Multimap> predicates);
+ Multimap> predicates);
}
diff --git a/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java b/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java
index 646d591d8..3e0b71c9c 100644
--- a/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java
+++ b/CryptoAnalysis/src/main/java/crypto/reporting/ReportGenerator.java
@@ -45,7 +45,6 @@ public static String generateReport(
report.append("\t\tStatement: ").append(seed.getOrigin()).append("\n");
report.append("\t\tLine: ").append(seed.getOrigin().getStartLineNumber()).append("\n");
report.append("\t\tMethod: ").append(seed.getMethod()).append("\n");
- report.append("\t\tSHA-256: ").append(seed.getObjectId()).append("\n");
report.append("\t\tSecure: ").append(seed.isSecure()).append("\n");
}
diff --git a/CryptoAnalysis/src/main/java/crypto/reporting/Reporter.java b/CryptoAnalysis/src/main/java/crypto/reporting/Reporter.java
index 8fdd3d7ed..74b7fe133 100644
--- a/CryptoAnalysis/src/main/java/crypto/reporting/Reporter.java
+++ b/CryptoAnalysis/src/main/java/crypto/reporting/Reporter.java
@@ -33,9 +33,9 @@ public enum ReportFormat {
protected Reporter(String outputDir, Collection ruleset) throws IOException {
if (outputDir == null) {
- throw new RuntimeException(
- "Cannot create report without directory (try using --reportDir or setOutputDirectory)");
+ throw new RuntimeException("Cannot create report without report directory");
}
+
this.outputFile = new File(outputDir);
this.ruleset = ruleset;
diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/LabeledMatcherTransition.java b/CryptoAnalysis/src/main/java/crypto/typestate/LabeledMatcherTransition.java
index 78cc40e39..9e0b8078f 100644
--- a/CryptoAnalysis/src/main/java/crypto/typestate/LabeledMatcherTransition.java
+++ b/CryptoAnalysis/src/main/java/crypto/typestate/LabeledMatcherTransition.java
@@ -3,8 +3,8 @@
import boomerang.scene.DeclaredMethod;
import crypto.utils.MatcherUtils;
import crysl.rule.CrySLMethod;
-import java.util.Arrays;
import java.util.Collection;
+import java.util.Objects;
import java.util.Optional;
import typestate.finiteautomata.MatcherTransition;
import typestate.finiteautomata.State;
@@ -52,17 +52,14 @@ public String toString() {
}
@Override
- public boolean equals(Object other) {
- if (!super.equals(other)) {
- return false;
- }
-
- LabeledMatcherTransition matcherTransition = (LabeledMatcherTransition) other;
- return this.methods.equals(matcherTransition.getMethods());
+ public boolean equals(Object obj) {
+ return super.equals(obj)
+ && obj instanceof LabeledMatcherTransition other
+ && Objects.equals(methods, other.getMethods());
}
@Override
public int hashCode() {
- return Arrays.hashCode(new Object[] {super.hashCode(), from(), to(), methods});
+ return Objects.hash(super.hashCode(), from(), to(), methods);
}
}
diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/ReportingErrorStateNode.java b/CryptoAnalysis/src/main/java/crypto/typestate/ReportingErrorStateNode.java
index 9b090ee23..e346a6217 100644
--- a/CryptoAnalysis/src/main/java/crypto/typestate/ReportingErrorStateNode.java
+++ b/CryptoAnalysis/src/main/java/crypto/typestate/ReportingErrorStateNode.java
@@ -4,17 +4,7 @@
import java.util.Collection;
import typestate.finiteautomata.State;
-public class ReportingErrorStateNode implements State {
-
- private final Collection expectedCalls;
-
- public ReportingErrorStateNode(Collection expectedCalls) {
- this.expectedCalls = expectedCalls;
- }
-
- public Collection getExpectedCalls() {
- return expectedCalls;
- }
+public record ReportingErrorStateNode(Collection expectedCalls) implements State {
@Override
public boolean isErrorState() {
@@ -35,14 +25,4 @@ public boolean isAccepting() {
public String toString() {
return "ERR";
}
-
- @Override
- public int hashCode() {
- return this.getClass().hashCode();
- }
-
- @Override
- public boolean equals(Object obj) {
- return obj instanceof ReportingErrorStateNode;
- }
}
diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/TypestateAnalysis.java b/CryptoAnalysis/src/main/java/crypto/typestate/TypestateAnalysis.java
index bf041a297..b603adee6 100644
--- a/CryptoAnalysis/src/main/java/crypto/typestate/TypestateAnalysis.java
+++ b/CryptoAnalysis/src/main/java/crypto/typestate/TypestateAnalysis.java
@@ -46,11 +46,10 @@ public void runTypestateAnalysis() {
Collection seeds = analysisScope.computeSeeds();
for (Query seed : seeds) {
- if (!(seed instanceof ForwardSeedQuery)) {
+ if (!(seed instanceof ForwardSeedQuery query)) {
continue;
}
- ForwardSeedQuery query = (ForwardSeedQuery) seed;
runTypestateAnalysisForSeed(query);
}
}
@@ -90,7 +89,7 @@ public CallGraph callGraph() {
@Override
public Debugger debugger(
IDEALSeedSolver idealSeedSolver) {
- return definition.getDebugger(idealSeedSolver);
+ return new Debugger<>();
}
@Override
@@ -118,11 +117,10 @@ public Map> getRes
WeightedForwardQuery,
ForwardBoomerangResults>
entry : resultHandler.getResults().entrySet()) {
- if (!(entry.getKey() instanceof ForwardSeedQuery)) {
+ if (!(entry.getKey() instanceof ForwardSeedQuery forwardSeedQuery)) {
continue;
}
- ForwardSeedQuery forwardSeedQuery = (ForwardSeedQuery) entry.getKey();
results.put(forwardSeedQuery, entry.getValue());
}
return results;
diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/TypestateDefinition.java b/CryptoAnalysis/src/main/java/crypto/typestate/TypestateDefinition.java
index ed39b3f1c..5c7a76572 100644
--- a/CryptoAnalysis/src/main/java/crypto/typestate/TypestateDefinition.java
+++ b/CryptoAnalysis/src/main/java/crypto/typestate/TypestateDefinition.java
@@ -1,12 +1,9 @@
package crypto.typestate;
-import boomerang.debugger.Debugger;
import boomerang.scene.CallGraph;
import boomerang.scene.DataFlowScope;
import crysl.rule.CrySLRule;
-import ideal.IDEALSeedSolver;
import java.util.Collection;
-import typestate.TransitionFunction;
public interface TypestateDefinition {
@@ -16,7 +13,5 @@ public interface TypestateDefinition {
DataFlowScope getDataFlowScope();
- Debugger getDebugger(IDEALSeedSolver idealSeedSolver);
-
int getTimeout();
}
diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/WrappedState.java b/CryptoAnalysis/src/main/java/crypto/typestate/WrappedState.java
index 74740fe84..00c8cfe02 100644
--- a/CryptoAnalysis/src/main/java/crypto/typestate/WrappedState.java
+++ b/CryptoAnalysis/src/main/java/crypto/typestate/WrappedState.java
@@ -1,6 +1,7 @@
package crypto.typestate;
import crysl.rule.StateNode;
+import java.util.Objects;
import typestate.finiteautomata.State;
public class WrappedState implements State {
@@ -46,22 +47,12 @@ public boolean isInitialState() {
@Override
public int hashCode() {
- final int prime = 31;
- int result = 1;
- result = prime * result + ((delegate == null) ? 0 : delegate.hashCode());
- return result;
+ return Objects.hash(delegate);
}
@Override
public boolean equals(Object obj) {
- if (this == obj) return true;
- if (obj == null) return false;
- if (getClass() != obj.getClass()) return false;
- WrappedState other = (WrappedState) obj;
- if (delegate == null) {
- if (other.delegate != null) return false;
- } else if (!delegate.equals(other.delegate)) return false;
- return true;
+ return obj instanceof WrappedState other && Objects.equals(delegate, other.delegate());
}
@Override
diff --git a/CryptoAnalysis/src/main/java/crypto/visualization/Visualizer.java b/CryptoAnalysis/src/main/java/crypto/visualization/Visualizer.java
new file mode 100644
index 000000000..e8022fbb0
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/visualization/Visualizer.java
@@ -0,0 +1,111 @@
+package crypto.visualization;
+
+import crypto.analysis.IAnalysisSeed;
+import crypto.analysis.errors.AbstractError;
+import java.io.File;
+import java.io.IOException;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import org.graphper.api.Cluster;
+import org.graphper.api.FileType;
+import org.graphper.api.Graphviz;
+import org.graphper.api.Line;
+import org.graphper.api.Subgraph;
+import org.graphper.api.attributes.Rank;
+import org.graphper.draw.ExecuteException;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+public class Visualizer {
+
+ private static final Logger LOGGER = LoggerFactory.getLogger(Visualizer.class);
+ private static final String VISUALIZATION_NAME = "visualization";
+
+ private final File outputFile;
+
+ public Visualizer(String outputDir) throws IOException {
+ if (outputDir == null) {
+ throw new NullPointerException("OutputDir must not be null");
+ }
+
+ this.outputFile = new File(outputDir);
+
+ if (!outputFile.exists()) {
+ throw new IOException("Directory " + outputFile.getAbsolutePath() + " does not exist");
+ }
+
+ if (!outputFile.isDirectory()) {
+ throw new IOException(outputFile.getAbsolutePath() + " is not a directory");
+ }
+ }
+
+ public void createVisualization(Collection seeds)
+ throws ExecuteException, IOException {
+
+ Graphviz.GraphvizBuilder builder = Graphviz.digraph();
+
+ Map errorToNode = new HashMap<>();
+ for (IAnalysisSeed seed : seeds) {
+ Map errorToNodeForSeed = new HashMap<>();
+
+ for (AbstractError error : seed.getErrors()) {
+ WrappedNode node = new WrappedNode(error);
+
+ builder.addNode(node.asGraphicalNode());
+ errorToNodeForSeed.put(error, node);
+ }
+
+ if (!errorToNodeForSeed.isEmpty()) {
+ Cluster cluster = createClusterForSeed(seed, errorToNodeForSeed);
+ builder.cluster(cluster);
+ }
+
+ errorToNode.putAll(errorToNodeForSeed);
+ }
+
+ Collection lines = createLines(errorToNode);
+ for (Line line : lines) {
+ builder.addLine(line);
+ }
+
+ Graphviz graphviz = builder.build();
+ graphviz.toFile(FileType.PNG).save(outputFile.getAbsolutePath(), VISUALIZATION_NAME);
+ LOGGER.info(
+ "Written visualization to {}",
+ outputFile.getAbsolutePath() + File.separator + VISUALIZATION_NAME + ".png");
+ }
+
+ private Cluster createClusterForSeed(
+ IAnalysisSeed seed, Map errorToNode) {
+ Subgraph.SubgraphBuilder subgraphBuilder = Subgraph.builder().rank(Rank.SAME);
+
+ for (AbstractError error : errorToNode.keySet()) {
+ subgraphBuilder.addNode(errorToNode.get(error).asGraphicalNode());
+ }
+
+ Subgraph subgraph = subgraphBuilder.build();
+
+ return WrappedCluster.forSeed(seed, subgraph).asGraphicalCluster();
+ }
+
+ private Collection createLines(Map errorToNode) {
+ Collection result = new HashSet<>();
+
+ for (AbstractError error : errorToNode.keySet()) {
+ WrappedNode from = errorToNode.get(error);
+
+ for (AbstractError subError : error.getSubsequentErrors()) {
+ if (errorToNode.containsKey(subError)) {
+ WrappedNode to = errorToNode.get(subError);
+
+ Line line = WrappedLine.forLine(from, to).asGraphicalLine();
+ result.add(line);
+ }
+ }
+ }
+
+ return result;
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/visualization/WrappedCluster.java b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedCluster.java
new file mode 100644
index 000000000..57c9c89ab
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedCluster.java
@@ -0,0 +1,55 @@
+package crypto.visualization;
+
+import crypto.analysis.IAnalysisSeed;
+import java.util.Objects;
+import org.graphper.api.Cluster;
+import org.graphper.api.Subgraph;
+import org.graphper.api.attributes.ClusterShapeEnum;
+import org.graphper.api.attributes.Color;
+import org.graphper.api.attributes.Labeljust;
+
+public class WrappedCluster {
+
+ private final IAnalysisSeed seed;
+ private final Subgraph subgraph;
+ private Cluster cluster;
+
+ private WrappedCluster(IAnalysisSeed seed, Subgraph subgraph) {
+ this.seed = seed;
+ this.subgraph = subgraph;
+ }
+
+ public static WrappedCluster forSeed(IAnalysisSeed seed, Subgraph subgraph) {
+ return new WrappedCluster(seed, subgraph);
+ }
+
+ public Cluster asGraphicalCluster() {
+ if (cluster == null) {
+ cluster =
+ Cluster.builder()
+ .subgraph(subgraph)
+ .label(" " + seed.getFact().getVariableName())
+ .labeljust(Labeljust.LEFT)
+ .shape(ClusterShapeEnum.RECT)
+ .bgColor(Color.ofRGB("#E8E8E8")) // Gray-ish
+ .build();
+ }
+
+ return cluster;
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(seed);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return obj instanceof WrappedCluster other && Objects.equals(seed, other.seed);
+ }
+
+ @Override
+ public String toString() {
+ return "Cluster: " + seed;
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/visualization/WrappedLine.java b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedLine.java
new file mode 100644
index 000000000..12bbab5d1
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedLine.java
@@ -0,0 +1,45 @@
+package crypto.visualization;
+
+import java.util.Objects;
+import org.graphper.api.Line;
+
+public class WrappedLine {
+
+ private final WrappedNode from;
+ private final WrappedNode to;
+ private Line line;
+
+ private WrappedLine(WrappedNode from, WrappedNode to) {
+ this.from = from;
+ this.to = to;
+ }
+
+ public static WrappedLine forLine(WrappedNode from, WrappedNode to) {
+ return new WrappedLine(from, to);
+ }
+
+ public Line asGraphicalLine() {
+ if (line == null) {
+ line = Line.builder(from.asGraphicalNode(), to.asGraphicalNode()).build();
+ }
+
+ return line;
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(from, to);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return obj instanceof WrappedLine other
+ && Objects.equals(from, other.from)
+ && Objects.equals(to, other.to);
+ }
+
+ @Override
+ public String toString() {
+ return from + " -> " + to;
+ }
+}
diff --git a/CryptoAnalysis/src/main/java/crypto/visualization/WrappedNode.java b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedNode.java
new file mode 100644
index 000000000..ec4217ef9
--- /dev/null
+++ b/CryptoAnalysis/src/main/java/crypto/visualization/WrappedNode.java
@@ -0,0 +1,76 @@
+package crypto.visualization;
+
+import crypto.analysis.errors.AbstractConstraintsError;
+import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AbstractOrderError;
+import crypto.analysis.errors.AbstractRequiredPredicateError;
+import crypto.analysis.errors.ForbiddenMethodError;
+import crypto.analysis.errors.PredicateConstraintError;
+import java.util.Objects;
+import org.graphper.api.Node;
+import org.graphper.api.attributes.Color;
+import org.graphper.api.attributes.NodeShapeEnum;
+
+public class WrappedNode {
+
+ private final AbstractError error;
+ private Node graphicalNode;
+
+ public WrappedNode(AbstractError error) {
+ this.error = error;
+ }
+
+ public Node asGraphicalNode() {
+ if (graphicalNode == null) {
+ graphicalNode =
+ Node.builder()
+ .label(getLabel())
+ .shape(NodeShapeEnum.RECT)
+ .fillColor(getColor())
+ .build();
+ }
+
+ return graphicalNode;
+ }
+
+ private String getLabel() {
+ return error.getClass().getSimpleName()
+ + "\nClass: "
+ + error.getErrorStatement().getMethod().getDeclaringClass()
+ + "\n"
+ + error.getErrorStatement()
+ + "\nLine: "
+ + error.getLineNumber();
+ }
+
+ private Color getColor() {
+ if (error instanceof ForbiddenMethodError) {
+ return Color.ofRGB("#9AF6FF"); // turquoise-ish
+ } else if (error instanceof AbstractOrderError) {
+ return Color.ofRGB("#FFF7AB"); // Yellow-ish
+ } else if (error instanceof AbstractRequiredPredicateError) {
+ return Color.ofRGB("#FFEBB2"); // Orange-ish
+ } else if (error instanceof AbstractConstraintsError) {
+ return Color.ofRGB("#C1D4FF"); // Blue-ish
+ } else if (error instanceof PredicateConstraintError) {
+ return Color.INDIGO;
+ } else {
+ return Color.WHITE;
+ }
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(error);
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ return obj instanceof WrappedNode other && Objects.equals(error, other.error);
+ }
+
+ @Override
+ public String toString() {
+ return "Node: " + error;
+ }
+}
diff --git a/CryptoAnalysis/src/test/java/test/UsagePatternErrorListener.java b/CryptoAnalysis/src/test/java/test/UsagePatternErrorListener.java
index 5a85d8c68..95e773b47 100644
--- a/CryptoAnalysis/src/test/java/test/UsagePatternErrorListener.java
+++ b/CryptoAnalysis/src/test/java/test/UsagePatternErrorListener.java
@@ -1,6 +1,7 @@
package test;
import crypto.analysis.errors.AbstractError;
+import crypto.analysis.errors.AlternativeReqPredicateError;
import crypto.analysis.errors.CallToError;
import crypto.analysis.errors.ConstraintError;
import crypto.analysis.errors.ForbiddenMethodError;
@@ -192,6 +193,16 @@ public void reportError(RequiredPredicateError requiredPredicateError) {
}
}
+ @Override
+ public void reportError(AlternativeReqPredicateError alternativeReqPredicateError) {
+ for (Assertion a : assertions) {
+ if (a instanceof PredicateErrorCountAssertion) {
+ PredicateErrorCountAssertion errorCountAssertion = (PredicateErrorCountAssertion) a;
+ errorCountAssertion.increaseCount();
+ }
+ }
+ }
+
@Override
public void reportError(TypestateError typestateError) {
for (Assertion a : assertions) {
diff --git a/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java b/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java
index dbaa88eaa..fd444d2af 100644
--- a/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java
+++ b/CryptoAnalysis/src/test/java/test/UsagePatternResultsListener.java
@@ -9,7 +9,8 @@
import com.google.common.collect.HashMultimap;
import com.google.common.collect.Multimap;
import com.google.common.collect.Table;
-import crypto.analysis.EnsuredCrySLPredicate;
+import crypto.analysis.AbstractPredicate;
+import crypto.analysis.EnsuredPredicate;
import crypto.analysis.IAnalysisSeed;
import crypto.analysis.errors.AbstractError;
import crypto.extractparameter.CallSiteWithExtractedValue;
@@ -102,7 +103,7 @@ public void checkedConstraints(
@Override
public void generatedPredicate(
IAnalysisSeed fromSeed,
- EnsuredCrySLPredicate predicate,
+ AbstractPredicate predicate,
IAnalysisSeed toSeed,
Statement statement) {
for (Assertion a : assertions) {
@@ -155,7 +156,7 @@ public void generatedPredicate(
@Override
public void ensuredPredicates(
IAnalysisSeed seed,
- Multimap> predicates) {
+ Multimap> predicates) {
for (Assertion a : assertions) {
if (a instanceof HasEnsuredPredicateAssertion) {
HasEnsuredPredicateAssertion assertion = (HasEnsuredPredicateAssertion) a;
@@ -166,10 +167,10 @@ public void ensuredPredicates(
Collection values =
seed.getAnalysisResults().asStatementValWeightTable().columnKeySet();
- Collection> ensuredPreds =
+ Collection> ensuredPreds =
predicates.get(assertion.getStmt());
- for (Map.Entry ensPred : ensuredPreds) {
+ for (Map.Entry ensPred : ensuredPreds) {
assertion.reported(values, ensPred.getKey());
}
}
@@ -183,10 +184,10 @@ public void ensuredPredicates(
Collection values =
seed.getAnalysisResults().asStatementValWeightTable().columnKeySet();
- Collection> ensuredPreds =
+ Collection> ensuredPreds =
predicates.get(assertion.getStmt());
- for (Map.Entry