Adding smoke test to xcfa-cli

.github/actions/benchexec-report/action.yml

@@ -0,0 +1,77 @@
+name: 'Report on benchexec tests'
+description: 'Collecting results of benchexec runs, and creating report'
+runs:
+  using: "composite"
+  steps:
+    - name: Checkout repository
+      uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
+    - name: Install benchexec
+      shell: bash
+      run: |
+        sudo add-apt-repository ppa:sosy-lab/benchmarking
+        sudo apt install benchexec
+    - name: Download artifacts
+      uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
+      with:
+        path: artifacts
+    - name: Generate tables
+      id: generate
+      shell: bash
+      run: |
+        cd artifacts
+        EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
+        echo "Message<<$EOF" >> $GITHUB_OUTPUT
+        for i in *
+        do 
+          if (ls $i/*xml.bz2 >/dev/null 2>/dev/null)
+          then
+            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 } ')
+            emoji=":white_check_mark:"
+            [ $correct -eq 0 ] && emoji=":question:"
+            [ $incorrect -eq 0 ] || emoji=":exclamation:"
+            echo "<details><summary> $emoji ${i#BenchexecResults-} ($correct / $incorrect / $all)</summary>" >> $GITHUB_OUTPUT
+            echo >> $GITHUB_OUTPUT
+            echo '`table-generator`'" output: [HTML](https://theta.mit.bme.hu/benchmark-results/${{ github.head_ref }}/$i/$(ls *.html))/[CSV](https://theta.mit.bme.hu/benchmark-results/${{ github.head_ref }}/$i/$(ls *.csv))" >> $GITHUB_OUTPUT
+            echo >> $GITHUB_OUTPUT
+            echo '```'  >> $GITHUB_OUTPUT
+            cat *.txt  >> $GITHUB_OUTPUT
+            echo '```'  >> $GITHUB_OUTPUT
+            echo "</details>" >> $GITHUB_OUTPUT
+            echo >> $GITHUB_OUTPUT
+            echo >> $GITHUB_OUTPUT
+            popd
+          else
+            rm -rf $i
+          fi
+        done
+        echo "$EOF" >> $GITHUB_OUTPUT
+    - name: Upload results
+      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      with:
+        name: BenchexecResults
+        path: artifacts
+    - name: Deploy to GHPages
+      if: github.event_name == 'pull_request'
+      uses: JamesIves/github-pages-deploy-action@22a6ee251d6f13c6ab1ecb200d974f1a6feb1b8d # v4.4.2
+      with:
+        branch: gh-pages
+        folder: artifacts
+        target-folder: benchmark-results/${{ github.head_ref }}/
+        single-commit: true
+    - name: Comment on PR
+      if: github.event_name == 'pull_request'
+      uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e
+      with: 
+        comment_tag: 'diffcheck'
+        mode: 'recreate'
+        message: |
+          Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):
+
+          ${{ steps.generate.outputs.Message }}

.github/actions/benchexec-test/action.yml

@@ -0,0 +1,65 @@
+name: 'Run tests using benchexec'
+description: 'Running benchexec tests on xcfa-cli'
+inputs:
+    task:
+        required: true
+    test_number:
+        required: true
+runs:
+  using: "composite"
+  steps:
+    - name: Checkout repository
+      uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
+    - name: Install benchexec and dependencies
+      shell: bash
+      run: |
+        sudo add-apt-repository ppa:sosy-lab/benchmarking
+        sudo apt install benchexec openjdk-17-jre-headless libgomp1 libmpfr-dev
+    - name: Get benchmark definition file
+      shell: bash
+      run: |
+        mkdir -p xml
+        wget https://gitlab.com/sosy-lab/sv-comp/bench-defs/-/raw/main/benchmark-defs/theta.xml -P xml
+        sed -i 's/<benchmark tool="theta" timelimit="990 s" hardtimelimit="1050 s" memlimit="15 GB" cpuCores="4">/<benchmark tool="theta" timelimit="120 s" hardtimelimit="130 s">/g' xml/theta.xml
+    - name: Get sv-benchmarks
+      shell: bash
+      run: |
+        git clone --filter=blob:none --no-checkout --depth 1 --sparse https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git
+        cd sv-benchmarks
+        git sparse-checkout add c
+        git checkout
+    - name: Get archive
+      shell: bash
+      run: |
+        wget https://github.com/ftsrg/theta/releases/download/svcomp23/theta.zip
+        unzip theta.zip
+    - uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
+      name: Get JAR
+      with:
+        name: ThetaJars
+        path: jar/
+    - name: Add new jar to archive
+      shell: bash
+      run: |
+        mv jar/xcfa/xcfa-cli/build/libs/*-all.jar theta/theta.jar
+        ls -l theta
+    - 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
+    - name: Run benchexec
+      shell: bash
+      if: steps.setfile.outputs.length != '0'
+      run: |
+        benchexec xml/theta.xml --no-container --tool-directory theta -t ${{ inputs.task }}
+    - name: Upload results
+      uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
+      if: steps.setfile.outputs.length != '0'
+      with:
+        name: BenchexecResults-${{ inputs.task }}
+        path: results