Updated actions

ftsrg · Nov 12, 2024 · a27fb7e · a27fb7e
1 parent 35fd050
commit a27fb7e
Show file tree

Hide file tree

Showing 11 changed files with 32 additions and 40 deletions.
diff --git a/.github/actions/build-archive/action.yml b/.github/actions/build-archive/action.yml
@@ -58,15 +58,13 @@ runs:
       with:
         name: specification-transformation
         path: ./
-    - name: Move file to overwrite specification-transformation.bin
-      shell: bash
-      run: |
-        mv specification-transformation.bin $GITHUB_ACTION_PATH/specification-transformation.bin
     - name: Copy specification transformation binary and license
       shell: bash
       run: |
-        cp $GITHUB_ACTION_PATH/specification-transformation.bin ${{ inputs.name }}/${{ inputs.name }}/
-        chmod +x ${{ inputs.name }}/${{ inputs.name }}/specification-transformation.bin
+        zipfile=$(realpath ./specification-transformation.zip)
+        pushd ${{ inputs.name }}/${{ inputs.name }}/
+        unzip $zipfile
+        popd
         cp $GITHUB_ACTION_PATH/specification-transformation.bin.LICENSE ${{ inputs.name }}/${{ inputs.name }}/
         cp $GITHUB_ACTION_PATH/offset.sh ${{ inputs.name }}/${{ inputs.name }}/
     - name: ZIP archive

diff --git a/.github/actions/build-spec-transformation/action.yml b/.github/actions/build-spec-transformation/action.yml
@@ -7,8 +7,8 @@ runs:
     - name: Print file path
       shell: bash
       run: |
-        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }}
-        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
+        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }}
+        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
     - name: Setup java 17
       if: env.file_exists == 'false'
       uses: actions/setup-java@5ffc13f4174014e2d4d4572b3d74c3fa61aeb2c2 # v3.11.0
@@ -37,25 +37,19 @@ runs:
         mv lib/cpachecker/lib/java/runtime/*.jar cpachecker/runtime/
         mv lib/cpachecker/config cpachecker/
         mv lib/cpachecker/cpachecker.jar cpachecker/
-    - name: Install nuitka
+    - name: zip file
       if: env.file_exists == 'false'
       shell: bash
       run: |
-        sudo apt update && sudo apt -y --no-install-recommends install nuitka libfuse2
-    - name: Run nuitka
-      if: env.file_exists == 'false'
-      shell: bash
-      run: |
-        cd specification-transformation
-        bash -c "yes yes || true" | nuitka3 --onefile --standalone --include-data-dir="cpachecker=cpachecker" src/specification-transformation.py 
+        zip specification-transformation.zip specification-transformation/cpachecker specification-transformation/src -r
     - name: Move if exists
       if: env.file_exists == 'true'
       shell: bash
       run: |
         mkdir specification-transformation
-        mv $GITHUB_ACTION_PATH/specification-transformation.bin specification-transformation/
+        mv $GITHUB_ACTION_PATH/specification-transformation.zip ./
     - name: Upload results
       uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:
         name: specification-transformation
-        path: specification-transformation/specification-transformation.bin
+        path: specification-transformation.zip
diff --git a/.github/actions/build-spec-transformation/specification-transformation.bin b/.github/actions/build-spec-transformation/specification-transformation.bin
diff --git a/.github/workflows/check-copyright.yml b/.github/workflows/check-copyright.yml
@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-copyright:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

diff --git a/.github/workflows/check-formatting.yml b/.github/workflows/check-formatting.yml
@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-formatting:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

diff --git a/.github/workflows/check-version.yml b/.github/workflows/check-version.yml
@@ -9,7 +9,7 @@ concurrency:
 
 jobs:
   check-version:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |

diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml
@@ -18,7 +18,7 @@ concurrency:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -64,7 +64,7 @@ jobs:
             portfolio: BOUNDED
           - tool: Thorn_SV-COMP
             portfolio: HORN
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: create-archives
     steps:
       - name: Checkout repository
@@ -78,23 +78,23 @@ jobs:
 
   collect-results:
     needs: test-benchexec
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
       - name: Generate report
         uses: ./.github/actions/benchexec-report
 
   create-spec-transformation:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
       - name: Create spec-transformation
         uses: ./.github/actions/build-spec-transformation
 
   create-archives:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: [build, create-spec-transformation]
     strategy:
       matrix:
@@ -118,7 +118,7 @@ jobs:
 
   javadoc:
     needs: build
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -129,7 +129,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest]
+        os: [ubuntu-24.04]
     needs: build
     runs-on: ${{ matrix.os }}
     steps:
@@ -142,15 +142,15 @@ jobs:
       - name: Run tests
         uses: ./.github/actions/test-action
       - name: Positive outcome badge
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
           status: "Success"
           color: "green"
           path: "badges/test-${{ runner.os }}"
       - name: Negative outcome badge
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
@@ -162,7 +162,7 @@ jobs:
   deploy-release:
     needs: [test-linux, create-archives]
     if: "${{ github.event.inputs.message != '' &&  github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -177,7 +177,7 @@ jobs:
   deploy-maven:
     # needs: test-linux
     if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -194,7 +194,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -231,7 +231,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -269,7 +269,7 @@ jobs:
           repository: ftsrg/${{ matrix.dockerprojects }}
 
   deploy-docs:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

diff --git a/.github/workflows/reformat-code.yml b/.github/workflows/reformat-code.yml
@@ -10,7 +10,7 @@ on:
 
 jobs:
   reformat:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92
       id: generate-token

diff --git a/.github/workflows/sonar.yml b/.github/workflows/sonar.yml
@@ -13,7 +13,7 @@ concurrency:
 
 jobs:
   run-sonar:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

diff --git a/.github/workflows/version-bump.yml b/.github/workflows/version-bump.yml
@@ -15,7 +15,7 @@ on:
 
 jobs:
   version-bump:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - name: Set java home to java 17
       run: |

diff --git a/scripts/theta-start.sh b/scripts/theta-start.sh
@@ -43,13 +43,13 @@ else
     if [ "$(basename "$property")" == "termination.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     else