Adapt to CrySL 4.0.0 and set Java version to 17

.github/dependabot.yml

@@ -6,7 +6,3 @@ updates:
     interval: weekly
     time: "04:00"
   open-pull-requests-limit: 10
-  ignore:
-  - dependency-name: com.google.crypto.tink:tink
-    versions:
-    - 1.5.0

.github/workflows/approve_dependabotifications.yml

@@ -1,7 +1,10 @@
 name: Dependabot auto-approve
-on:
-  pull_request_target:
-   paths: ["**/pom.xml"]
+
+# Currently disabled because the action is not compatible with merge queues
+on: [workflow_dispatch]
+  # pull_request_target:
+  #   paths: ["**/pom.xml"]
+
 
 permissions:
   contents: write

.github/workflows/build_and_test.yml

@@ -10,7 +10,7 @@ on:
     types: [opened, reopened]
 
 env:
-  JAVA_VERSION: 11
+  JAVA_VERSION: 17
 
 jobs:
   # Build the CryptoAnalysis module and run its tests

.github/workflows/deploy_and_release.yml

@@ -6,8 +6,6 @@ jobs:
   deployment:
     runs-on: ubuntu-latest
     environment: Deploy
-    name: CryptoAnalysis Deployment
-
     steps:
       - name: Checkout source code
         uses: actions/checkout@v4
@@ -19,25 +17,27 @@ jobs:
         with:
           distribution: 'adopt'
           java-package: 'jdk'
-          java-version: '11'
+          java-version: '17'
           server-id: 'ossrh' # must match the serverId configured for the nexus-staging-maven-plugin
           server-username: OSSRH_USERNAME # Env var that holds your OSSRH user name
           server-password: OSSRH_PASSWORD # Env var that holds your OSSRH user pw
           gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }} # Substituted with the value stored in the referenced secret
           gpg-passphrase: SIGN_KEY_PASS # Env var that holds the key's passphrase
 
-      - name: Set up Maven
-        uses: stCarolas/[email protected]
-        with:
-          maven-version: 3.6.3
-
       - name: Build & Deploy CryptoAnalysis
         run: mvn -B -U clean deploy -Pdeployment -DskipTests
         env:
           SIGN_KEY_PASS: ${{ secrets.GPG_PRIVATE_KEY_PASSPHRASE }}
           OSSRH_USERNAME: ${{ secrets.SONATYPE_USER }}
           OSSRH_PASSWORD: ${{ secrets.SONATYPE_PW }}
 
+  release:
+    runs-on: ubuntu-latest
+    needs: deployment
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+
       - name: Fetch all tags
         run: git fetch --tags
 

.github/workflows/merge_queue_mac.yml

@@ -4,7 +4,7 @@ on:
   merge_group:
 
 env:
-  JAVA_VERSION: 11
+  JAVA_VERSION: 17
 
 jobs:
   # This name must be equal to the corresponding build_and_test action

.github/workflows/merge_queue_ubuntu.yml

@@ -4,7 +4,7 @@ on:
   merge_group:
 
 env:
-  JAVA_VERSION: 11
+  JAVA_VERSION: 17
 
 jobs:
   # This name must be equal to the corresponding build_and_test job

.github/workflows/merge_queue_windows.yml

@@ -4,7 +4,7 @@ on:
   merge_group:
 
 env:
-  JAVA_VERSION: 11
+  JAVA_VERSION: 17
 
 jobs:
   # This name must be equal to the corresponding build_and_test job

.github/workflows/version.yml

@@ -23,12 +23,7 @@ jobs:
         with:
           distribution: 'adopt'
           java-package: jdk
-          java-version: '11'
-      # Sets up Maven version
-      - name: Set up Maven
-        uses: stCarolas/[email protected]
-        with:
-          maven-version: 3.6.3
+          java-version: '17'
       # Semantic versioning
       - name: Semantic versioning
         id: versioning

CryptoAnalysis/pom.xml

@@ -54,29 +54,16 @@
             <groupId>de.fraunhofer.iem</groupId>
             <artifactId>testCore</artifactId>
         </dependency>
+        <dependency>
+            <groupId>de.darmstadt.tu.crossing.CrySL</groupId>
+            <artifactId>CrySLParser</artifactId>
+        </dependency>
         <!-- https://mvnrepository.com/artifact/org.json/json -->
         <dependency>
             <groupId>org.json</groupId>
             <artifactId>json</artifactId>
             <version>20240303</version>
         </dependency>
-        <dependency>
-            <groupId>org.eclipse.xtext</groupId>
-            <artifactId>org.eclipse.xtext.xbase</artifactId>
-            <version>2.36.0</version>
-        </dependency>
-        <!-- https://mvnrepository.com/artifact/org.eclipse.emf/org.eclipse.emf.common -->
-        <dependency>
-            <groupId>org.eclipse.emf</groupId>
-            <artifactId>org.eclipse.emf.common</artifactId>
-            <version>2.31.0</version>
-        </dependency>
-        <!-- https://mvnrepository.com/artifact/org.eclipse.emf/org.eclipse.emf.ecore -->
-        <dependency>
-            <groupId>org.eclipse.emf</groupId>
-            <artifactId>org.eclipse.emf.ecore</artifactId>
-            <version>2.37.0</version>
-        </dependency>
         <!-- https://mvnrepository.com/artifact/com.fasterxml.jackson.core/jackson-core -->
         <dependency>
             <groupId>com.fasterxml.jackson.core</groupId>
@@ -91,31 +78,6 @@
     </dependencies>
 
     <build>
-        <pluginManagement>
-            <plugins>
-                <plugin>
-                    <groupId>org.eclipse.m2e</groupId>
-                    <artifactId>lifecycle-mapping</artifactId>
-                    <version>1.0.0</version>
-                    <configuration>
-                        <lifecycleMappingMetadata>
-                            <pluginExecutions>
-                                <pluginExecution>
-                                    <pluginExecutionFilter>
-                                        <groupId>org.apache.maven.plugins</groupId>
-                                        <artifactId>maven-dependency-plugin</artifactId>
-                                        <versionRange>3.3.0</versionRange>
-                                        <goals>
-                                            <goal>unpack</goal>
-                                        </goals>
-                                    </pluginExecutionFilter>
-                                </pluginExecution>
-                            </pluginExecutions>
-                        </lifecycleMappingMetadata>
-                    </configuration>
-                </plugin>
-            </plugins>
-        </pluginManagement>
         <plugins>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>

CryptoAnalysis/src/main/java/crypto/analysis/AlternativeReqPredicate.java

@@ -1,8 +1,8 @@
 package crypto.analysis;
 
 import boomerang.scene.Statement;
-import crypto.rules.CrySLPredicate;
-import crypto.rules.ISLConstraint;
+import crysl.rule.CrySLPredicate;
+import crysl.rule.ISLConstraint;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.stream.Collectors;

CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithEnsuredPredicate.java

@@ -7,7 +7,7 @@
 import boomerang.scene.Val;
 import com.google.common.collect.HashMultimap;
 import com.google.common.collect.Multimap;
-import crypto.rules.CrySLPredicate;
+import crysl.rule.CrySLPredicate;
 import java.util.Collection;
 import typestate.TransitionFunction;
 

CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java

@@ -19,19 +19,19 @@
 import crypto.constraints.ConstraintSolver;
 import crypto.constraints.EvaluableConstraint;
 import crypto.extractparameter.CallSiteWithExtractedValue;
-import crypto.rules.CrySLCondPredicate;
-import crypto.rules.CrySLForbiddenMethod;
-import crypto.rules.CrySLMethod;
-import crypto.rules.CrySLObject;
-import crypto.rules.CrySLPredicate;
-import crypto.rules.CrySLRule;
-import crypto.rules.ICrySLPredicateParameter;
-import crypto.rules.ISLConstraint;
-import crypto.rules.StateNode;
-import crypto.rules.TransitionEdge;
 import crypto.typestate.ReportingErrorStateNode;
 import crypto.typestate.WrappedState;
 import crypto.utils.MatcherUtils;
+import crysl.rule.CrySLCondPredicate;
+import crysl.rule.CrySLForbiddenMethod;
+import crysl.rule.CrySLMethod;
+import crysl.rule.CrySLObject;
+import crysl.rule.CrySLPredicate;
+import crysl.rule.CrySLRule;
+import crysl.rule.ICrySLPredicateParameter;
+import crysl.rule.ISLConstraint;
+import crysl.rule.StateNode;
+import crysl.rule.TransitionEdge;
 import java.util.AbstractMap;
 import java.util.ArrayList;
 import java.util.Arrays;

CryptoAnalysis/src/main/java/crypto/analysis/CryptoAnalysisDataFlowScope.java

@@ -3,7 +3,7 @@
 import boomerang.scene.DataFlowScope;
 import boomerang.scene.DeclaredMethod;
 import boomerang.scene.Method;
-import crypto.rules.CrySLRule;
+import crysl.rule.CrySLRule;
 import java.util.Collection;
 import java.util.HashSet;
 import org.slf4j.Logger;

CryptoAnalysis/src/main/java/crypto/analysis/CryptoScanner.java

@@ -9,7 +9,6 @@
 import boomerang.scene.sparse.SparseCFGCache;
 import com.google.common.collect.Table;
 import crypto.analysis.errors.AbstractError;
-import crypto.cryslhandler.RulesetReader;
 import crypto.exceptions.CryptoAnalysisException;
 import crypto.listener.AnalysisPrinter;
 import crypto.listener.AnalysisReporter;
@@ -18,7 +17,8 @@
 import crypto.listener.IAnalysisListener;
 import crypto.listener.IErrorListener;
 import crypto.listener.IResultsListener;
-import crypto.rules.CrySLRule;
+import crysl.CrySLParser;
+import crysl.rule.CrySLRule;
 import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Collection;
@@ -58,8 +58,8 @@ protected final void initialize() {
         // Read the ruleset
         analysisReporter.beforeReadingRuleset(getRulesetPath());
         try {
-            RulesetReader reader = new RulesetReader();
-            ruleset = reader.readRulesFromPath(getRulesetPath());
+            CrySLParser parser = new CrySLParser();
+            ruleset = parser.parseRulesFromDirectory(getRulesetPath());
         } catch (IOException e) {
             throw new CryptoAnalysisException("Could not read rules: " + e.getMessage());
         }

CryptoAnalysis/src/main/java/crypto/analysis/EnsuredCrySLPredicate.java

@@ -1,7 +1,7 @@
 package crypto.analysis;
 
 import crypto.extractparameter.CallSiteWithExtractedValue;
-import crypto.rules.CrySLPredicate;
+import crysl.rule.CrySLPredicate;
 import java.util.Collection;
 
 public class EnsuredCrySLPredicate {

CryptoAnalysis/src/main/java/crypto/analysis/HiddenPredicate.java

@@ -11,7 +11,7 @@
 import crypto.analysis.errors.RequiredPredicateError;
 import crypto.analysis.errors.TypestateError;
 import crypto.extractparameter.CallSiteWithExtractedValue;
-import crypto.rules.CrySLPredicate;
+import crysl.rule.CrySLPredicate;
 import java.util.Collection;
 import java.util.stream.Collectors;
 

CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java

@@ -8,7 +8,7 @@
 import com.google.common.collect.HashMultimap;
 import com.google.common.collect.Multimap;
 import crypto.analysis.errors.AbstractError;
-import crypto.rules.CrySLPredicate;
+import crysl.rule.CrySLPredicate;
 import java.math.BigInteger;
 import java.security.MessageDigest;
 import java.security.NoSuchAlgorithmException;
@@ -110,20 +110,6 @@ protected Collection<CrySLPredicate> expectedPredicatesAtStatement(Statement sta
         return predicates;
     }
 
-    public Collection<IAnalysisSeed> getDependantSeeds() {
-        Collection<IAnalysisSeed> seeds = new HashSet<>();
-
-        for (ExpectedPredicateOnSeed seed : expectedPredicates.values()) {
-            if (this.equals(seed.getSeed())) {
-                continue;
-            }
-
-            seeds.add(seed.getSeed());
-        }
-
-        return seeds;
-    }
-
     public Method getMethod() {
         return origin.getMethod();
     }

CryptoAnalysis/src/main/java/crypto/analysis/PredicateHandler.java

@@ -2,7 +2,7 @@
 
 import crypto.analysis.errors.PredicateContradictionError;
 import crypto.analysis.errors.RequiredPredicateError;
-import crypto.rules.ISLConstraint;
+import crysl.rule.ISLConstraint;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashMap;

CryptoAnalysis/src/main/java/crypto/analysis/RequiredCrySLPredicate.java

@@ -1,8 +1,8 @@
 package crypto.analysis;
 
 import boomerang.scene.Statement;
-import crypto.rules.CrySLPredicate;
-import crypto.rules.ISLConstraint;
+import crysl.rule.CrySLPredicate;
+import crysl.rule.ISLConstraint;
 import java.util.List;
 
 public class RequiredCrySLPredicate implements ISLConstraint {

CryptoAnalysis/src/main/java/crypto/analysis/SeedGenerator.java

@@ -6,10 +6,10 @@
 import boomerang.scene.DataFlowScope;
 import boomerang.scene.Statement;
 import boomerang.scene.Val;
-import crypto.rules.CrySLRule;
 import crypto.typestate.ForwardSeedQuery;
 import crypto.typestate.TypestateAnalysis;
 import crypto.typestate.TypestateDefinition;
+import crysl.rule.CrySLRule;
 import ideal.IDEALSeedSolver;
 import java.util.Collection;
 import java.util.Collections;

CryptoAnalysis/src/main/java/crypto/analysis/errors/AbstractError.java

@@ -3,8 +3,8 @@
 import boomerang.scene.Method;
 import boomerang.scene.Statement;
 import crypto.analysis.IAnalysisSeed;
-import crypto.rules.CrySLMethod;
-import crypto.rules.CrySLRule;
+import crysl.rule.CrySLMethod;
+import crysl.rule.CrySLRule;
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.HashSet;

CryptoAnalysis/src/main/java/crypto/analysis/errors/CallToError.java

@@ -1,8 +1,8 @@
 package crypto.analysis.errors;
 
 import crypto.analysis.IAnalysisSeed;
-import crypto.rules.CrySLMethod;
-import crypto.rules.CrySLRule;
+import crysl.rule.CrySLMethod;
+import crysl.rule.CrySLRule;
 import java.util.Arrays;
 import java.util.Collection;