Merge pull request #789 from CROSSINGTUD/develop

Merge for new release

.github/actions/performance/action.yml

@@ -0,0 +1,70 @@
+name: Test Performance
+
+inputs:
+  test-results-path:
+    description: "Path to the test results directory"
+    required: true
+  source-branch:
+    description: "Branch that holds the file with previous results"
+    required: true
+  current-results:
+    description: "File that stores previous results"
+    required: true
+  output-file:
+    description: "File where the results are storted in"
+    required: true
+
+runs:
+  using: "composite"
+  steps: 
+    - name: Aggregate test results from multiple directories
+      run: |
+        total_time=0
+          
+        if [ -d ${{ inputs.test-results-path }} ]; then
+          echo "Processing directory: ${{ inputs.test-results-path }}"
+            
+          for file in ${{ inputs.test-results-path }}/*.txt; do
+            if [ -f "$file" ]; then
+              echo "Processing file: $file"
+                
+              # Extract the time elapsed from each relevant line in the file and sum it up
+              file_time=$(grep -oP "Time elapsed: \K[\d\.]+" "$file" | awk '{sum += $1} END {print sum}')
+              if [ -n "$file_time" ]; then
+                echo "Time found: $file_time seconds"
+                total_time=$(echo "$total_time + $file_time" | bc)
+              else
+                echo "No time elapsed found in file: $file"
+              fi
+            else
+              echo "No files found in directory: ${{ inputs.test-results-path }}"
+            fi
+          done
+        else
+          echo "Directory does not exist: ${{ inputs.test-results-path }}"
+        fi
+  
+        # Convert total time to minutes, seconds, and milliseconds
+        total_time_int=$(printf "%.0f" "$total_time")
+        minutes=$((total_time_int / 60))
+        seconds=$((total_time_int % 60))
+        milliseconds=$(printf "%.0f" "$(echo "($total_time - $total_time_int) * 1000" | bc)")
+
+        echo "Total Time Calculated: ${minutes}m ${seconds}s ${milliseconds}ms"
+        timestamp=$(date +"%Y-%m-%d %H:%M:%S")
+        echo "${timestamp}, Total Time: ${minutes}m ${seconds}s ${milliseconds}ms" >> ${{ inputs.output-file }}
+      shell: bash
+
+    - name: Combine current and past results
+      run: |
+        git checkout ${{ inputs.source-branch }}
+        if [ -f ${{ inputs.current-results }} ]; then
+          git checkout ${{ inputs.source-branch }} ${{ inputs.current-results }}
+          cat ${{ inputs.output-file }} >> ${{ inputs.current-results }}
+          mv ${{ inputs.current-results }} ${{ inputs.output-file }}
+        fi
+      shell: bash
+
+    - name: Switch to default branch
+      run: git checkout ${{ github.ref_name }}
+      shell: bash

.github/workflows/build_and_test.yml

@@ -2,12 +2,7 @@ name: Build And Test (Basic)
 description: Basic build and tests for the submodules on each push and pull request
 
 on:
-  push:
-    branches-ignore:
-      - master
-      - develop
   pull_request:
-    types: [opened, reopened]
   workflow_dispatch:
 
 env:

.github/workflows/deploy_and_release.yml

@@ -31,6 +31,21 @@ jobs:
           OSSRH_USERNAME: ${{ secrets.SONATYPE_USER }}
           OSSRH_PASSWORD: ${{ secrets.SONATYPE_PW }}
 
+  synchronize:
+    runs-on: ubuntu-latest
+    needs: deployment
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Synchronize master and develop
+        run: |
+          gh pr create -B develop -H master -t "Synchronize version in master and develop" -b "Update the version in `develop` from `master`"
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
   release:
     runs-on: ubuntu-latest
     needs: deployment
@@ -77,7 +92,7 @@ jobs:
       - name: Zip JavaCryptographicArchitecture folder
         run: |
           echo "Zipping the JavaCryptographicArchitecture folder..."
-          zip -r JavaCryptographicArchitecture.zip CryptoAnalysis/src/main/resources/JavaCryptographicArchitecture
+          zip -r JavaCryptographicArchitecture.zip CryptoAnalysis/src/test/resources/rules/JavaCryptographicArchitecture
 
       - name: Create GitHub Release
         run: |

.github/workflows/performance.yml

@@ -0,0 +1,182 @@
+name: Performance Analysis
+
+on:
+  workflow_dispatch:
+    #inputs:
+    #  analysis:
+    #    type: boolean
+    #    required: false
+    #    default: false
+    #  android:
+    #    type: boolean
+    #    required: false
+    #    default: false
+    #  soot:
+    #    type: boolean
+    #    required: false
+    #    default: false
+
+env:
+  JAVA_VERSION: 17
+
+jobs:
+  performance-analysis:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Build and test Analysis
+        uses: ./.github/actions/analysis
+        with:
+          java-version: ${{ env.JAVA_VERSION }}
+
+      - name: Create or update gh-pages-output directory
+        run: mkdir -p gh-pages-output
+
+      - name: Extract performance
+        uses: ./.github/actions/performance
+        with:
+          test-results-path: CryptoAnalysis/shippable/testresults
+          source-branch: gh-pages
+          current-results: analysis_history.txt
+          output-file: gh-pages-output/analysis_history.txt
+
+      - name: Store Analysis performance
+        uses: actions/upload-artifact@v4
+        with:
+          name: analysis-performance
+          path: gh-pages-output/analysis_history.txt
+
+  performance-android:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Build and test Android Scanner
+        uses: ./.github/actions/scanner-android
+        with:
+          java-version: ${{ env.JAVA_VERSION }}
+
+      - name: Create or update gh-pages-output directory
+        run: mkdir -p gh-pages-output
+
+      - name: Extract performance
+        uses: ./.github/actions/performance
+        with:
+          test-results-path: HeadlessAndroidScanner/shippable/testresults
+          source-branch: gh-pages
+          current-results: android_history.txt
+          output-file: gh-pages-output/android_history.txt
+
+      - name: Store Android performance
+        uses: actions/upload-artifact@v4
+        with:
+          name: android-performance
+          path: gh-pages-output/android_history.txt
+
+  performance-soot:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Build and test JavaScanner with Soot
+        uses: ./.github/actions/scanner-soot
+        with:
+          java-version: ${{ env.JAVA_VERSION }}
+
+      - name: Create or update gh-pages-output directory
+        run: mkdir -p gh-pages-output
+
+      - name: Extract performance
+        uses: ./.github/actions/performance
+        with:
+          test-results-path: HeadlessJavaScanner/shippable/testresults
+          source-branch: gh-pages
+          current-results: soot_history.txt
+          output-file: gh-pages-output/soot_history.txt
+
+      - name: Store Soot performance
+        uses: actions/upload-artifact@v4
+        with:
+          name: soot-performance
+          path: gh-pages-output/soot_history.txt
+
+  performance-report:
+    runs-on: ubuntu-latest
+    needs: [performance-analysis, performance-android, performance-soot]
+    steps:
+      - name: Checkout source code
+        uses: actions/checkout@v4
+        with:
+          ref: gh-pages
+
+      - name: Load performance files
+        uses: actions/download-artifact@v4
+        with:
+          path: gh-pages-output
+          merge-multiple: true
+
+      - name: Generate HTML report
+        run: |
+          echo "<html><body>" > gh-pages-output/index.html
+          echo "<div style=\"display: flex; flex-wrap: wrap; gap: 0 50px;\">" >> gh-pages-output/index.html
+
+          echo "<div style=\"flex: 1 1 200px; min-width: 200px;\"><h1>Analysis</h1><ul>" >> gh-pages-output/index.html
+
+          if [ -f gh-pages-output/analysis_history.txt ]; then
+            cat gh-pages-output/analysis_history.txt | while read line; do
+              echo "${line}"
+              echo "<li>${line}</li>" >> gh-pages-output/index.html
+            done
+          fi
+
+          echo "</ul></div>" >> gh-pages-output/index.html
+
+          echo "<div style=\"flex: 1 1 200px; min-width: 200px;\"><h1>AndroidScanner</h1><ul>" >> gh-pages-output/index.html
+
+          if [ -f gh-pages-output/android_history.txt ]; then
+            cat gh-pages-output/android_history.txt | while read line; do
+              echo "${line}"
+              echo "<li>${line}</li>" >> gh-pages-output/index.html
+            done
+          fi
+
+          echo "</ul></div>" >> gh-pages-output/index.html
+
+          echo "<div style=\"flex: 1 1 200px; min-width: 200px;\"><h1>JavaScanner (Soot)</h1><ul>" >> gh-pages-output/index.html
+
+          if [ -f gh-pages-output/soot_history.txt ]; then
+            cat gh-pages-output/soot_history.txt | while read line; do
+              echo "${line}"
+              echo "<li>${line}</li>" >> gh-pages-output/index.html
+            done
+          fi
+
+          echo "</ul></div>" >> gh-pages-output/index.html
+
+          echo "</div>" >> gh-pages-output/index.html
+          echo "</body></html>" >> gh-pages-output/index.html
+  
+      - name: Deploy to GitHub Pages
+        uses: peaceiris/actions-gh-pages@v4
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./gh-pages-output
+
+      - name: Delete artifacts
+        uses: geekyeggo/delete-artifact@v5
+        with:
+          failOnError: false
+          name: |
+            analysis-performance
+            android-performance
+            soot-performance

.github/workflows/style.yml

@@ -14,6 +14,13 @@ jobs:
     steps:
       - name: Checkout source code
         uses: actions/checkout@v4
+      # Set up Java version
+      - name: Set up Java 17
+        uses: actions/setup-java@v4
+        with:
+          distribution: adopt
+          java-package: jdk
+          java-version: 17
       # Restores Maven dependecies
       - name: Restore local Maven repository
         uses: actions/cache@v4

CryptoAnalysis/pom.xml

@@ -75,6 +75,11 @@
             <artifactId>jackson-databind</artifactId>
             <version>2.18.2</version>
         </dependency>
+        <dependency>
+            <groupId>org.graphper</groupId>
+            <artifactId>graph-support</artifactId>
+            <version>1.4.0</version>
+        </dependency>
     </dependencies>
 
     <build>

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

@@ -3,13 +3,20 @@
 import crypto.extractparameter.CallSiteWithExtractedValue;
 import crysl.rule.CrySLPredicate;
 import java.util.Collection;
+import java.util.Objects;
 
-public class EnsuredCrySLPredicate {
+/**
+ * Super class for predicates that are propagated during the analysis. Each predicate is either an
+ * {@link EnsuredPredicate} or an {@link UnEnsuredPredicate}. The former ones keep track of all
+ * predicates from the ENSURES section where no violations from a rule are found. The latter ones
+ * are propagated to keep track of predicates and seeds if there is a violation.
+ */
+public abstract class AbstractPredicate {
 
     private final CrySLPredicate predicate;
     private final Collection<CallSiteWithExtractedValue> parametersToValues;
 
-    public EnsuredCrySLPredicate(
+    public AbstractPredicate(
             CrySLPredicate predicate, Collection<CallSiteWithExtractedValue> parametersToValues) {
         this.predicate = predicate;
         this.parametersToValues = parametersToValues;
@@ -23,27 +30,14 @@ public Collection<CallSiteWithExtractedValue> getParametersToValues() {
         return parametersToValues;
     }
 
-    public String toString() {
-        return "Proved " + predicate.getPredName();
-    }
-
     @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 AbstractPredicate other
+                && Objects.equals(predicate, other.getPredicate());
     }
 }