Merge pull request #198 from ftsrg/xcfa-refactor

XCFA-refactor 2023 [draft]

.github/actions/badge-creation/action.yml

@@ -27,7 +27,9 @@ runs:
         path: ${{ inputs.path }}/badge.svg
     - name: setup rsync for windows
       if: runner.os == 'Windows'
-      uses: GuillaumeFalourd/setup-rsync@2b503a403f7185e6872bbc56f903d7395ddd75a2
+      shell: bash
+      run: |
+        choco install -y rsync
     - name: Deploy badges
       if: github.ref == 'refs/heads/master' && always() && github.event_name != 'pull_request'
       uses: leventeBajczi/github-pages-deploy-action-winfix@6d31a3c68a3912555731864c0d5ef4239b02369d # v0.3

.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
+        cp $GITHUB_ACTION_PATH/theta.xml 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/svcomp24/theta.zip
+        unzip theta.zip
+        mv Theta theta
+    - 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

.github/actions/benchexec-test/theta.xml

@@ -0,0 +1,104 @@
+<?xml version="1.0"?>
+<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
+<benchmark tool="theta" timelimit="120 s" hardtimelimit="130 s">
+
+    <resultfiles>**/witness.*</resultfiles>
+
+    <option name="--disable-xcfa-serialization"/>
+    <option name="--disable-c-serialization"/>
+    <option name="--disable-arg-generation"/>
+    <option name="--backend">PORTFOLIO</option>
+    <option name="--portfolio">COMPLEX</option>
+    <option name="--loglevel">INFO</option>
+
+    <rundefinition name="SV-COMP24_unreach-call">
+        <tasks name="ReachSafety-Arrays">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Arrays.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-BitVectors">
+            <includesfile>../sv-benchmarks/c/ReachSafety-BitVectors.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-ControlFlow">
+            <includesfile>../sv-benchmarks/c/ReachSafety-ControlFlow.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-ECA">
+            <includesfile>../sv-benchmarks/c/ReachSafety-ECA.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Floats">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Floats.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Heap">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Heap.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Loops">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Loops.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-ProductLines">
+            <includesfile>../sv-benchmarks/c/ReachSafety-ProductLines.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Recursive">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Recursive.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Sequentialized">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Sequentialized.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-XCSP">
+            <includesfile>../sv-benchmarks/c/ReachSafety-XCSP.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Combinations">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Combinations.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Hardware">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Hardware.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Hardness">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Hardness.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+        <tasks name="ReachSafety-Fuzzle">
+            <includesfile>../sv-benchmarks/c/ReachSafety-Fuzzle.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+
+        <tasks name="ConcurrencySafety-Main">
+            <includesfile>../sv-benchmarks/c/ConcurrencySafety-Main.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
+        </tasks>
+    </rundefinition>
+
+    <rundefinition name="SV-COMP24_no-data-race">
+        <tasks name="NoDataRace-Main">
+            <includesfile>../sv-benchmarks/c/NoDataRace-Main.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/no-data-race.prp</propertyfile>
+        </tasks>
+    </rundefinition>
+
+    <rundefinition name="SV-COMP24_no-overflow">
+        <tasks name="ConcurrencySafety-NoOverflows">
+            <includesfile>../sv-benchmarks/c/ConcurrencySafety-NoOverflows.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile>
+        </tasks>
+    </rundefinition>
+
+    <rundefinition name="SV-COMP24_valid-memsafety">
+        <tasks name="ConcurrencySafety-MemSafety">
+            <includesfile>../sv-benchmarks/c/ConcurrencySafety-MemSafety.set</includesfile>
+            <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
+        </tasks>
+    </rundefinition>
+
+
+</benchmark>