Added specification transformation (#317)

* Added specification transformation * Version bump * Setting environment variables for VERIFIER_NAME and VERIFIER_VERSION * Adding back commented out code * Testing is now done per-rundef * Added logging to benchexec * updated download-upload artifacts * not hardcoding Theta * Fixed folder * Enhanced logging * Task -> rundef * Handling multiple task sets in same rundef * added binary building * Fixed patch * Fixed shell * Fixed cpachecker * clone * java 17 for cpachecker * fix path * nuitka -> nuitka3 * installing fuse2 for nuitka * added yes yes * Fixed SIGPIPE * Fix path * Moving fixed * Trying to convince matrix to work * Trying to better support multiple zips * removed unzipping * Exiting on error * chmod +x * Added better handling of java-17 * adding spec * Added guards to not rebuild specification-transformation all the time * Fix syntax * Fix syntax * Added built library * Added logging * Syntax fix * Syntax fix * Added env step * Syntax fix * Syntax fix
ftsrg · Nov 10, 2024 · 67ad033 · 67ad033
1 parent c85c711
commit 67ad033
Show file tree

Hide file tree

Showing 14 changed files with 756 additions and 166 deletions.
diff --git a/.github/actions/benchexec-report/action.yml b/.github/actions/benchexec-report/action.yml
@@ -11,7 +11,7 @@ runs:
         sudo add-apt-repository ppa:sosy-lab/benchmarking
         sudo apt install benchexec
     - name: Download artifacts
-      uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
+      uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v3.0.2
       with:
         path: artifacts
     - name: Generate tables
@@ -21,7 +21,7 @@ runs:
         cd artifacts
         EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
         echo "Message<<$EOF" >> $GITHUB_OUTPUT
-        header1=$(printf '|task set|'; for f in BenchexecResults*; do echo "${f##*-}"; done | sort -u | xargs printf '%s|')
+        header1=$(printf '| Rundefinition |'; for f in BenchexecResults*; do echo "${f##*-}"; done | sort -u | xargs printf '%s|')
         header2=$(printf '|--|'; for ff in $(for f in BenchexecResults*; do echo "${f##*-}"; done | sort -u); do printf -- '--|'; done)
         echo "$header1" >> $GITHUB_OUTPUT
         printf "$header2" >> $GITHUB_OUTPUT
@@ -33,11 +33,23 @@ runs:
             pushd $i
             table-generator -d *xml.bz2
             sed -i 's/\.\.\/sv-benchmarks/https:\/\/gitlab\.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/raw\/main/g' *.html
-            unzip *.zip
-            rm *.zip
-            correct=$(tail -n9 *.txt | grep '  correct:' | awk ' { print $2 } ')
-            incorrect=$(tail -n9 *.txt | grep '  incorrect:' | awk ' { print $2 } ')
-            all=$(tail -n9 *.txt | grep 'Statistics:' | awk ' { print $2 } ')
+            for zipfile in *.zip
+            do
+              correct=0
+              incorrect=0
+              all=0
+              for txt in *.txt
+              do
+                new_correct=$(tail -n9 $txt | grep '  correct:' | awk ' { print $2 } ')
+                correct=$((correct + new_correct))
+                new_incorrect=$(tail -n9 $txt | grep '  incorrect:' | awk ' { print $2 } ')
+                incorrect=$((incorrect + new_incorrect))
+                new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ')
+                all=$((all + new_all))
+                echo "Found $new_correct correct and $new_incorrect incorrect results out of $new_all tasks in $txt"
+              done
+            done
+            echo "Summary: found $correct correct and $incorrect incorrect results out of $all tasks in $i"
             emoji=":white_check_mark:"
             [ $correct -eq 0 ] && emoji=":question:"
             [ $incorrect -eq 0 ] || emoji=":exclamation:"
@@ -57,7 +69,7 @@ runs:
         echo >> $GITHUB_OUTPUT
         echo "$EOF" >> $GITHUB_OUTPUT
     - name: Upload results
-      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:
         name: BenchexecResults
         path: artifacts

diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml
@@ -1,12 +1,12 @@
 name: 'Run tests using benchexec'
 description: 'Running benchexec tests on xcfa-cli'
 inputs:
-    task:
-        required: true
-    test_number:
+    rundef:
         required: true
     portfolio:
         required: true
+    tool:
+        required: true
 runs:
   using: "composite"
   steps:
@@ -39,31 +39,33 @@ runs:
           cd sv-benchmarks
           git sparse-checkout add c
           git checkout
-    - uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
+          pwd
+          ls -l
+    - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v3.0.2
       name: Get zip
       with:
-        name: Theta_SV-COMP
+        name: ${{ inputs.tool }}
         path: release/
     - name: Unzip 
       shell: bash
       run: |
-        unzip release/Theta.zip
-        sed -i 's/ --input \$1/ --portfolio ${{ inputs.portfolio }} --input \$1/g' Theta/theta-start.sh
-#    - name: Cut setfile if too long
-#      id: setfile
-#      shell: bash
-#      run: |
-#        cd sv-benchmarks/c
-#        for i in $(sed 's/#.*$//g' ${{ inputs.task }}.set); do find . -wholename ./$i; done | while read line; do grep "${line#./}" $GITHUB_ACTION_PATH/unsupported.txt >/dev/null 2>/dev/null || test -z $(yq e '.properties.[] | select(.property_file == "../properties/unreach-call.prp")' $line) >/dev/null 2>/dev/null || echo  $(echo $line | sha1sum | awk ' { print $1 } ') $line ; done | sort -k1 | awk ' { $1=""; print $0 } ' | awk '{$1=$1};1' > all-files.txt
-#        head -n${{ inputs.test_number }} all-files.txt > ${{ inputs.task }}.set
-#        echo "length=$(cat ${{ inputs.task }}.set | wc -l)" >> "$GITHUB_OUTPUT"
-#        cat ${{ inputs.task }}.set
+        unzip release/*.zip
     - name: Run benchexec
       shell: bash
       run: |
-        timeout 300 benchexec xml/theta.xml -n 2 --no-container --tool-directory Theta -t ${{ inputs.task }} || true
+        sed -i 's/<option name="--portfolio">STABLE<\/option>/<option name="--portfolio">${{ inputs.portfolio }}<\/option>/g' xml/theta.xml
+        cat xml/theta.xml
+        folder=$(dirname $(find . -name "theta.jar" | head -n1))
+        echo $folder
+        pwd
+        for task in $(cat xml/theta.xml | grep 'tasks name=' | grep -oP '(?<=").*(?=")')
+        do
+          echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'"
+          echo "timeout 60 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true"
+          timeout 60 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true
+        done
     - name: Upload results
-      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:
-        name: BenchexecResults-${{ inputs.task }}-${{ inputs.portfolio }}
+        name: BenchexecResults-${{ inputs.rundef }}-${{ inputs.portfolio }}
         path: results