Skip to content

Commit

Permalink
Fix check on negated alternatives for RequiredPredicates (related to C…
Browse files Browse the repository at this point in the history 
…ROSSINGTUD#372 )
  • Loading branch information
@smeyer198
smeyer198 committed Jan 14, 2024
1 parent 9f6b1c9 commit 9d5b472
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 51 deletions.
59 changes: 23 additions & 36 deletions CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -394,58 +394,45 @@ private boolean checkPredicates(Collection<ISLConstraint> relConstraints) {
if (pred instanceof RequiredCrySLPredicate) {
RequiredCrySLPredicate reqPred = (RequiredCrySLPredicate) pred;
if (reqPred.getPred().isNegated()) {
boolean violated = false;
for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
if (reqPred.getPred().equals(ensPred.getPredicate())) {
return false;
if (reqPred.getPred().equals(ensPred.getPredicate()) && doPredsMatch(reqPred.getPred(), ensPred)) {
violated = true;
}
}
remainingPredicates.remove(pred);
if (!violated) {
remainingPredicates.remove(pred);
}
} else {
for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
if (reqPred.getPred().equals(ensPred.getPredicate()) && doPredsMatch(reqPred.getPred(), ensPred)) {
remainingPredicates.remove(pred);
}
}
}
} else {
} else if (pred instanceof AlternativeReqPredicate) {
AlternativeReqPredicate alt = (AlternativeReqPredicate) pred;
List<CrySLPredicate> alternatives = alt.getAlternatives();
boolean satisfied = false;
List<CrySLPredicate> negatives = alternatives.parallelStream().filter(e -> e.isNegated()).collect(Collectors.toList());

if (negatives.size() == alternatives.size()) {
for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
if (alternatives.parallelStream().anyMatch(e -> e.getPredName().equals(ensPred.getPredicate().getPredName()))) {
return false;
}
}
remainingPredicates.remove(pred);
} else if (negatives.isEmpty()) {
for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
if (alternatives.parallelStream().anyMatch(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred))) {
remainingPredicates.remove(pred);
break;
}
}
} else {
boolean neg = true;

for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
if (negatives.parallelStream().anyMatch(e -> e.equals(ensPred.getPredicate()))) {
neg = false;
}
List<CrySLPredicate> positives = alternatives.stream().filter(e -> !e.isNegated()).collect(Collectors.toList());
List<CrySLPredicate> negatives = alternatives.stream().filter(e -> e.isNegated()).collect(Collectors.toList());

alternatives.removeAll(negatives);
if (alternatives.parallelStream().allMatch(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred))) {
satisfied = true;
}
boolean satisfied = false;
List<CrySLPredicate> ensuredNegatives = alternatives.stream().filter(e -> e.isNegated()).collect(Collectors.toList());

if (satisfied | neg) {
remainingPredicates.remove(pred);
}
for (EnsuredCrySLPredicate ensPred : ensuredPredicates) {
// Check if any positive alternative is satisfied by the ensured predicate
if (positives.stream().anyMatch(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred))) {
satisfied = true;
}

// Negated alternatives that are ensured are not satisfied
List<CrySLPredicate> violatedNegAlternatives = negatives.stream().filter(e -> e.equals(ensPred.getPredicate()) && doPredsMatch(e, ensPred)).collect(Collectors.toList());
ensuredNegatives.removeAll(violatedNegAlternatives);
}

if (satisfied || !ensuredNegatives.isEmpty()) {
remainingPredicates.remove(pred);
}
}
}

Expand Down Expand Up @@ -518,7 +505,7 @@ private boolean doPredsMatch(CrySLPredicate pred, EnsuredCrySLPredicate ensPred)
requiredPredicatesExist = false;
}
}
return pred.isNegated() != requiredPredicatesExist;
return requiredPredicatesExist;
}

private Collection<String> retrieveValueFromUnit(CallSiteWithParamIndex cswpi, Collection<ExtractedValue> collection) {
Expand Down
23 changes: 8 additions & 15 deletions CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ public void pred1OnPos1() {
Assertions.predicateErrors(1);
}

@Ignore
@Test
public void notPred1onPos1() {
A pred1OnA = new A();
Expand Down Expand Up @@ -215,7 +214,6 @@ public void pred1onPos1_AND_pred2onPos2() {
Assertions.predicateErrors(4);
}

@Ignore
@Test
public void pred1onPos1_AND_notPred2onPos2() {
A pred1onA = new A();
Expand Down Expand Up @@ -248,7 +246,6 @@ public void pred1onPos1_AND_notPred2onPos2() {
Assertions.predicateErrors(4);
}

@Ignore
@Test
public void notPred1onPos1_AND_pred2onPos2() {
A pred1onA = new A();
Expand Down Expand Up @@ -281,7 +278,6 @@ public void notPred1onPos1_AND_pred2onPos2() {
Assertions.predicateErrors(4);
}

@Ignore
@Test
public void notPred1onPos1_AND_notPred2onPos2() {
A pred1onA = new A();
Expand Down Expand Up @@ -347,7 +343,7 @@ public void pred1onPos1_OR_pred1onPos2(){
Assertions.predicateErrors(2); // two, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void pred1onPos1_OR_notPred1onPos2(){
A pred1onA = new A();
Expand Down Expand Up @@ -378,7 +374,7 @@ public void pred1onPos1_OR_notPred1onPos2(){
Assertions.predicateErrors(2); // two, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void notPred1onPos1_OR_pred1onPos2(){
A pred1onA = new A();
Expand Down Expand Up @@ -479,7 +475,6 @@ public void pred1onPos1_OR_pred2onPos2() {
Assertions.predicateErrors(2); // two, because each parameter will be reported
}

@Ignore
@Test
public void pred1onP1_OR_notPred2onP2() {
A pred1onA = new A();
Expand Down Expand Up @@ -514,7 +509,6 @@ public void pred1onP1_OR_notPred2onP2() {
Assertions.predicateErrors(2); // two, because each parameter will be reported
}

@Ignore
@Test
public void notPred1onP1_OR_pred2onP2() {
A pred1onA = new A();
Expand Down Expand Up @@ -549,7 +543,6 @@ public void notPred1onP1_OR_pred2onP2() {
Assertions.predicateErrors(2); // two, because each parameter will be reported
}

@Ignore
@Test
public void notPred1onP1_OR_notPred2onP2() {
A pred1onA = new A();
Expand Down Expand Up @@ -631,7 +624,7 @@ public void pred1onPos1_OR_pred1onPos2_OR_pred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // NullPointerException
@Ignore
@Test
public void pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
A pred1onA = new A();
Expand Down Expand Up @@ -678,7 +671,7 @@ public void pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3() {
A pred1onA = new A();
Expand Down Expand Up @@ -725,7 +718,7 @@ public void notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
A pred1onA = new A();
Expand Down Expand Up @@ -772,7 +765,7 @@ public void notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3() {
A pred1onA = new A();
Expand Down Expand Up @@ -820,7 +813,7 @@ public void pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3() {
A pred1onA = new A();
Expand Down Expand Up @@ -867,7 +860,7 @@ public void pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3() {
Assertions.predicateErrors(3); // three, because each parameter will be reported
}

@Ignore // Nullpointer
@Ignore
@Test
public void notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3() {
A pred1onA = new A();
Expand Down

0 comments on commit 9d5b472

Please sign in to comment.