From 9d5b4725417484d859b5125a0758d0ea2ba9ea3a Mon Sep 17 00:00:00 2001 From: Sven Meyer Date: Sun, 14 Jan 2024 15:19:37 +0100 Subject: [PATCH] Fix check on negated alternatives for RequiredPredicates (related to #372 ) --- .../AnalysisSeedWithSpecification.java | 59 ++++++++----------- .../customrules/RequiredPredicatesTest.java | 23 +++----- 2 files changed, 31 insertions(+), 51 deletions(-) diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java index 3bb00f6db..00d704370 100644 --- a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java +++ b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java @@ -394,12 +394,15 @@ private boolean checkPredicates(Collection 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)) { @@ -407,45 +410,29 @@ private boolean checkPredicates(Collection relConstraints) { } } } - } else { + } else if (pred instanceof AlternativeReqPredicate) { AlternativeReqPredicate alt = (AlternativeReqPredicate) pred; List alternatives = alt.getAlternatives(); - boolean satisfied = false; - List 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 positives = alternatives.stream().filter(e -> !e.isNegated()).collect(Collectors.toList()); + List 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 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 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); + } } } @@ -518,7 +505,7 @@ private boolean doPredsMatch(CrySLPredicate pred, EnsuredCrySLPredicate ensPred) requiredPredicatesExist = false; } } - return pred.isNegated() != requiredPredicatesExist; + return requiredPredicatesExist; } private Collection retrieveValueFromUnit(CallSiteWithParamIndex cswpi, Collection collection) { diff --git a/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java b/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java index b0e7e166a..51be45d88 100644 --- a/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java +++ b/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java @@ -42,7 +42,6 @@ public void pred1OnPos1() { Assertions.predicateErrors(1); } - @Ignore @Test public void notPred1onPos1() { A pred1OnA = new A(); @@ -215,7 +214,6 @@ public void pred1onPos1_AND_pred2onPos2() { Assertions.predicateErrors(4); } - @Ignore @Test public void pred1onPos1_AND_notPred2onPos2() { A pred1onA = new A(); @@ -248,7 +246,6 @@ public void pred1onPos1_AND_notPred2onPos2() { Assertions.predicateErrors(4); } - @Ignore @Test public void notPred1onPos1_AND_pred2onPos2() { A pred1onA = new A(); @@ -281,7 +278,6 @@ public void notPred1onPos1_AND_pred2onPos2() { Assertions.predicateErrors(4); } - @Ignore @Test public void notPred1onPos1_AND_notPred2onPos2() { A pred1onA = new A(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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(); @@ -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();