Skip to content

Commit

Permalink
Adapt to Java 17 constructs
Browse files Browse the repository at this point in the history
  • Loading branch information
@smeyer198
smeyer198 committed Dec 14, 2024
1 parent 982aeb5 commit 0f7fa9a
Show file tree
Hide file tree
Showing 37 changed files with 295 additions and 724 deletions.
26 changes: 6 additions & 20 deletions CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
import crysl.rule.ISLConstraint;
import java.util.ArrayList;
import java.util.List;
import java.util.Objects;
import java.util.stream.Collectors;

public class AlternativeReqPredicate implements ISLConstraint {
Expand All @@ -22,30 +23,15 @@ public AlternativeReqPredicate(CrySLPredicate alternativeOne, Statement stmt, in

@Override
public int hashCode() {
final int prime = 31;
int result = 1;
result = prime * result + ((alternatives == null) ? 0 : alternatives.hashCode());
result = prime * result + ((stmt == null) ? 0 : stmt.hashCode());
result = prime * result + paramIndex;
return result;
return Objects.hash(alternatives, stmt, paramIndex);
}

@Override
public boolean equals(Object obj) {
if (this == obj) return true;
if (obj == null) return false;
if (getClass() != obj.getClass()) return false;
AlternativeReqPredicate other = (AlternativeReqPredicate) obj;
if (alternatives == null) {
if (other.alternatives != null) return false;
} else if (!alternatives.equals(other.alternatives)) return false;
if (stmt == null) {
return other.stmt == null;
} else if (!stmt.equals(other.stmt)) {
return false;
}

return paramIndex == other.paramIndex;
return obj instanceof AlternativeReqPredicate other
&& Objects.equals(alternatives, other.alternatives)
&& Objects.equals(stmt, other.stmt)
&& paramIndex == other.paramIndex;
}

public Statement getLocation() {
Expand Down
11 changes: 5 additions & 6 deletions CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import com.google.common.collect.Multimap;
import crysl.rule.CrySLPredicate;
import java.util.Collection;
import java.util.Objects;
import typestate.TransitionFunction;

public class AnalysisSeedWithEnsuredPredicate extends IAnalysisSeed {
Expand Down Expand Up @@ -110,17 +111,15 @@ public void addEnsuredPredicate(EnsuredCrySLPredicate predicate) {
expectedPredicates.get(statement);

for (ExpectedPredicateOnSeed predOnSeed : predicateOnSeeds) {
if (!predOnSeed.getPredicate().equals(predicate.getPredicate())) {
if (!predOnSeed.predicate().equals(predicate.getPredicate())) {
continue;
}

if (!(predOnSeed.getSeed() instanceof AnalysisSeedWithSpecification)) {
if (!(predOnSeed.seed() instanceof AnalysisSeedWithSpecification seedWithSpec)) {
continue;
}

AnalysisSeedWithSpecification seedWithSpec =
(AnalysisSeedWithSpecification) predOnSeed.getSeed();
seedWithSpec.addEnsuredPredicate(predicate, statement, predOnSeed.getParamIndex());
seedWithSpec.addEnsuredPredicate(predicate, statement, predOnSeed.paramIndex());
}
}

Expand All @@ -131,7 +130,7 @@ public void addEnsuredPredicate(EnsuredCrySLPredicate predicate) {

@Override
public int hashCode() {
return super.hashCode();
return Objects.hash(super.hashCode());
}

@Override
Expand Down
91 changes: 28 additions & 63 deletions CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Objects;
import java.util.Optional;
import java.util.stream.Collectors;
import typestate.TransitionFunction;
Expand Down Expand Up @@ -172,12 +173,10 @@ private void evaluateTypestateOrder() {

private void typeStateChangeAtStatement(Statement statement, State stateNode) {
if (typeStateChange.put(statement, stateNode)) {
if (stateNode instanceof ReportingErrorStateNode) {
ReportingErrorStateNode errorStateNode = (ReportingErrorStateNode) stateNode;

if (stateNode instanceof ReportingErrorStateNode errorStateNode) {
TypestateError typestateError =
new TypestateError(
this, statement, specification, errorStateNode.getExpectedCalls());
this, statement, specification, errorStateNode.expectedCalls());
this.addError(typestateError);
scanner.getAnalysisReporter().reportError(this, typestateError);
}
Expand All @@ -202,11 +201,10 @@ private void evaluateIncompleteOperations() {
continue;
}

if (!(n.to() instanceof WrappedState)) {
if (!(n.to() instanceof WrappedState wrappedState)) {
continue;
}

WrappedState wrappedState = (WrappedState) n.to();
for (TransitionEdge t : specification.getUsagePattern().getAllTransitions()) {
if (t.getLeft().equals(wrappedState.delegate()) && !t.from().equals(t.to())) {
Collection<CrySLMethod> labels = t.getLabel();
Expand Down Expand Up @@ -322,15 +320,11 @@ public void computeExpectedPredicates(Collection<IAnalysisSeed> seeds) {
private void initializeDependantSeedsFromRequiredPredicates(Collection<IAnalysisSeed> seeds) {
Multimap<Statement, Map.Entry<CrySLPredicate, Integer>> reqPreds = HashMultimap.create();
for (ISLConstraint constraint : constraintSolver.getRequiredPredicates()) {
if (constraint instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) constraint;

if (constraint instanceof RequiredCrySLPredicate reqPred) {
Map.Entry<CrySLPredicate, Integer> entry =
new AbstractMap.SimpleEntry<>(reqPred.getPred(), reqPred.getParamIndex());
reqPreds.put(reqPred.getLocation(), entry);
} else if (constraint instanceof AlternativeReqPredicate) {
AlternativeReqPredicate altPred = (AlternativeReqPredicate) constraint;

} else if (constraint instanceof AlternativeReqPredicate altPred) {
for (CrySLPredicate predicate : altPred.getAlternatives()) {
Map.Entry<CrySLPredicate, Integer> entry =
new AbstractMap.SimpleEntry<>(predicate, altPred.getParamIndex());
Expand Down Expand Up @@ -644,22 +638,16 @@ private void ensurePredicateAtStatement(EnsuredCrySLPredicate ensPred, Statement
Collection<ExpectedPredicateOnSeed> expectedPredsAtStatement =
expectedPredicates.get(statement);
for (ExpectedPredicateOnSeed expectedPredicateOnSeed : expectedPredsAtStatement) {
CrySLPredicate predicate = expectedPredicateOnSeed.getPredicate();
IAnalysisSeed seed = expectedPredicateOnSeed.getSeed();
int paramIndex = expectedPredicateOnSeed.getParamIndex();
CrySLPredicate predicate = expectedPredicateOnSeed.predicate();
IAnalysisSeed seed = expectedPredicateOnSeed.seed();
int paramIndex = expectedPredicateOnSeed.paramIndex();

if (predicate.equals(ensPred.getPredicate())) {
if (seed instanceof AnalysisSeedWithSpecification) {
AnalysisSeedWithSpecification seedWithSpec =
(AnalysisSeedWithSpecification) seed;

if (seed instanceof AnalysisSeedWithSpecification seedWithSpec) {
seedWithSpec.addEnsuredPredicateFromOtherRule(ensPred, statement, paramIndex);
scanner.getAnalysisReporter()
.onGeneratedPredicate(this, ensPred, seedWithSpec, statement);
} else if (seed instanceof AnalysisSeedWithEnsuredPredicate) {
AnalysisSeedWithEnsuredPredicate seedWithoutSpec =
(AnalysisSeedWithEnsuredPredicate) seed;

} else if (seed instanceof AnalysisSeedWithEnsuredPredicate seedWithoutSpec) {
seedWithoutSpec.addEnsuredPredicate(ensPred);
scanner.getAnalysisReporter()
.onGeneratedPredicate(this, ensPred, seedWithoutSpec, statement);
Expand Down Expand Up @@ -708,9 +696,7 @@ private Collection<State> getStatesAtStatement(Statement statement) {

public void addEnsuredPredicate(
EnsuredCrySLPredicate ensPred, Statement statement, int paramIndex) {
if (ensPred instanceof HiddenPredicate) {
HiddenPredicate hiddenPredicate = (HiddenPredicate) ensPred;

if (ensPred instanceof HiddenPredicate hiddenPredicate) {
Map.Entry<HiddenPredicate, Integer> predAtIndex =
new AbstractMap.SimpleEntry<>(hiddenPredicate, paramIndex);
hiddenPredicates.put(statement, predAtIndex);
Expand Down Expand Up @@ -771,12 +757,10 @@ private boolean isPredicateNegatingState(CrySLPredicate ensPred, State stateNode

// Negated predicate does not have a condition, i.e. no "after" -> predicate is negated
// in all states
if (!(negPred instanceof CrySLCondPredicate)) {
if (!(negPred instanceof CrySLCondPredicate condNegPred)) {
return true;
}

CrySLCondPredicate condNegPred = (CrySLCondPredicate) negPred;

for (StateNode s : condNegPred.getConditionalMethods()) {
if (WrappedState.of(s).equals(stateNode)) {
return true;
Expand Down Expand Up @@ -859,9 +843,7 @@ public Collection<ISLConstraint> computeMissingPredicates() {
Collection<ISLConstraint> remainingPredicates = new HashSet<>(requiredPredicates);

for (ISLConstraint pred : requiredPredicates) {
if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;

if (pred instanceof RequiredCrySLPredicate reqPred) {
// If a negated predicate is ensured, a PredicateContradictionError has to be
// reported
if (reqPred.getPred().isNegated()) {
Expand All @@ -879,17 +861,12 @@ public Collection<ISLConstraint> computeMissingPredicates() {
remainingPredicates.remove(pred);
}
}
} else if (pred instanceof AlternativeReqPredicate) {
AlternativeReqPredicate altPred = (AlternativeReqPredicate) pred;
} else if (pred instanceof AlternativeReqPredicate altPred) {
Collection<CrySLPredicate> alternatives = altPred.getAlternatives();
Collection<CrySLPredicate> positives =
alternatives.stream()
.filter(e -> !e.isNegated())
.collect(Collectors.toList());
alternatives.stream().filter(e -> !e.isNegated()).toList();
Collection<CrySLPredicate> negatives =
alternatives.stream()
.filter(CrySLPredicate::isNegated)
.collect(Collectors.toList());
alternatives.stream().filter(CrySLPredicate::isNegated).toList();
int altParamIndex = altPred.getParamIndex();

boolean satisfied = false;
Expand Down Expand Up @@ -917,7 +894,7 @@ public Collection<ISLConstraint> computeMissingPredicates() {
e ->
doReqPredAndEnsPredMatch(
e, altParamIndex, ensPredAtIndex))
.collect(Collectors.toList());
.toList();
ensuredNegatives.removeAll(violatedNegAlternatives);
}

Expand All @@ -929,9 +906,7 @@ public Collection<ISLConstraint> computeMissingPredicates() {

// Check conditional required predicates
for (ISLConstraint rem : new HashSet<>(remainingPredicates)) {
if (rem instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate singlePred = (RequiredCrySLPredicate) rem;

if (rem instanceof RequiredCrySLPredicate singlePred) {
if (isPredConditionViolated(singlePred.getPred())) {
remainingPredicates.remove(singlePred);
}
Expand All @@ -953,9 +928,7 @@ public Collection<RequiredCrySLPredicate> computeContradictedPredicates() {
Collection<RequiredCrySLPredicate> contradictedPredicates = new HashSet<>();

for (ISLConstraint pred : requiredPredicates) {
if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;

if (pred instanceof RequiredCrySLPredicate reqPred) {
// Only negated predicates can be contradicted
if (!reqPred.getPred().isNegated()) {
continue;
Expand Down Expand Up @@ -1033,20 +1006,19 @@ private boolean doPredsMatch(CrySLPredicate pred, EnsuredCrySLPredicate ensPred)
Collection<String> expVals = Collections.emptySet();

for (CallSiteWithExtractedValue cswpi : ensPred.getParametersToValues()) {
if (cswpi.getCallSiteWithParam().getVarName().equals(parameterI)) {
if (cswpi.callSiteWithParam().varName().equals(parameterI)) {
actVals = retrieveValueFromUnit(cswpi);
}
}
for (CallSiteWithExtractedValue cswpi : constraintSolver.getCollectedValues()) {
if (cswpi.getCallSiteWithParam().getVarName().equals(var)) {
if (cswpi.callSiteWithParam().varName().equals(var)) {
expVals = retrieveValueFromUnit(cswpi);
}
}

String splitter = "";
int index = -1;
if (pred.getParameters().get(i) instanceof CrySLObject) {
CrySLObject obj = (CrySLObject) pred.getParameters().get(i);
if (pred.getParameters().get(i) instanceof CrySLObject obj) {
if (obj.getSplitter() != null) {
splitter = obj.getSplitter().getSplitter();
index = obj.getSplitter().getIndex();
Expand Down Expand Up @@ -1088,7 +1060,7 @@ && doPredsMatch(pred, hiddenPredicate)) {

private Collection<String> retrieveValueFromUnit(CallSiteWithExtractedValue callSite) {
Collection<String> values = new ArrayList<>();
Statement statement = callSite.getCallSiteWithParam().stmt();
Statement statement = callSite.callSiteWithParam().statement();

if (statement.isAssign()) {
Val rightSide = statement.getRightOp();
Expand Down Expand Up @@ -1136,20 +1108,13 @@ public Map<ControlFlowGraph.Edge, DeclaredMethod> getAllCallsOnObject() {

@Override
public int hashCode() {
final int prime = 31;
int result = super.hashCode();
result = prime * result + ((specification == null) ? 0 : specification.hashCode());
return result;
return Objects.hash(super.hashCode(), specification);
}

@Override
public boolean equals(Object obj) {
if (this == obj) return true;
if (!super.equals(obj)) return false;
if (getClass() != obj.getClass()) return false;
AnalysisSeedWithSpecification other = (AnalysisSeedWithSpecification) obj;
if (specification == null) {
return other.specification == null;
} else return specification.equals(other.specification);
return super.equals(obj)
&& obj instanceof AnalysisSeedWithSpecification other
&& Objects.equals(specification, other.specification);
}
}
15 changes: 3 additions & 12 deletions CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import crypto.extractparameter.CallSiteWithExtractedValue;
import crysl.rule.CrySLPredicate;
import java.util.Collection;
import java.util.Objects;

public class EnsuredCrySLPredicate {

Expand All @@ -29,21 +30,11 @@ public String toString() {

@Override
public int hashCode() {
final int prime = 31;
int result = 1;
result = prime * result + ((predicate == null) ? 0 : predicate.hashCode());
return result;
return Objects.hash(predicate);
}

@Override
public boolean equals(Object obj) {
if (this == obj) return true;
if (obj == null) return false;
if (getClass() != obj.getClass()) return false;
EnsuredCrySLPredicate other = (EnsuredCrySLPredicate) obj;
if (predicate == null) {
if (other.predicate != null) return false;
} else if (!predicate.equals(other.predicate)) return false;
return true;
return obj instanceof EnsuredCrySLPredicate other && predicate.equals(other.predicate);
}
}
Loading

0 comments on commit 0f7fa9a

Please sign in to comment.