Merge pull request #305 from ftsrg/frontend-update-2024

Frontend update 2024
ftsrg · Oct 19, 2024 · 81fbe00 · 81fbe00
2 parents 991b764 + 8749d32
commit 81fbe00
Show file tree

Hide file tree

Showing 148 changed files with 4,318 additions and 2,231 deletions.
diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml
@@ -49,23 +49,21 @@ runs:
       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
+#    - 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 -n 2 --no-container --tool-directory Theta -t ${{ inputs.task }}
+        timeout 300 benchexec xml/theta.xml -n 2 --no-container --tool-directory Theta -t ${{ inputs.task }} || true
     - name: Upload results
       uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
-      if: steps.setfile.outputs.length != '0'
       with:
         name: BenchexecResults-${{ inputs.task }}-${{ inputs.portfolio }}
         path: results
diff --git a/.github/actions/benchexec-test/theta.xml b/.github/actions/benchexec-test/theta.xml
@@ -11,90 +11,90 @@
     <option name="--loglevel">INFO</option>
 
     <rundefinition name="SV-COMP24_unreach-call">
-        <tasks name="ReachSafety-Arrays">
-            <includesfile>../sv-benchmarks/c/ReachSafety-Arrays.set</includesfile>
+        <tasks name="Arrays">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="BitVectors">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="ControlFlow">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="ECA">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Floats">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Heap">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Loops">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="ProductLines">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Recursive">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Sequentialized">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="XCSP">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Combinations">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Hardware">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Hardness">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Fuzzle">
+            <includesfile>../sv-benchmarks/c/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>
+        <tasks name="Concurrency">
+            <includesfile>../sv-benchmarks/c/Concurrency.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>
+        <tasks name="NoDataRace">
+            <includesfile>../sv-benchmarks/c/Concurrency.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>
+            <includesfile>../sv-benchmarks/c/Concurrency.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>
+            <includesfile>../sv-benchmarks/c/ConcurrencySafety.set</includesfile>
             <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
         </tasks>
     </rundefinition>

diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml
@@ -49,7 +49,24 @@ jobs:
   test-benchexec:
     strategy:
       matrix:
-        task: [ReachSafety-Arrays, ReachSafety-BitVectors, ReachSafety-ControlFlow, ReachSafety-ECA, ReachSafety-Floats, ReachSafety-Heap, ReachSafety-Loops, ReachSafety-ProductLines, ReachSafety-Recursive, ReachSafety-Sequentialized, ReachSafety-XCSP, ReachSafety-Combinations, ReachSafety-Hardware, ConcurrencySafety-Main, NoDataRace-Main, ConcurrencySafety-NoOverflows, ConcurrencySafety-MemSafety]
+        task:
+          - Arrays
+          - BitVectors
+          - ControlFlow
+          - ECA
+          - Floats
+          - Heap
+          - Loops
+          - ProductLines
+          - Recursive
+          - Sequentialized
+          - XCSP
+          - Combinations
+          - Hardware
+          - Concurrency
+          - NoDataRace
+          - ConcurrencySafety-NoOverflows
+          - ConcurrencySafety-MemSafety
         portfolio: [CEGAR, BOUNDED, HORN]
     runs-on: ubuntu-latest
     needs: create-archives

diff --git a/build.gradle.kts b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.5.2"
+    version = "6.6.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts
@@ -44,7 +44,8 @@ dependencies {
 // https://github.com/gradle/kotlin-dsl/issues/1207
 configurations.all {
     val isKotlinCompiler = name == "embeddedKotlin" || name.startsWith("kotlin") || name.startsWith(
-        "kapt")
+        "kapt"
+    )
     if (!isKotlinCompiler) {
         resolutionStrategy.eachDependency {
             if (requested.group == "org.jetbrains.kotlin" && requested.module.name == "kotlin-compiler-embeddable") {

diff --git a/buildSrc/src/main/kotlin/maven-artifact.gradle.kts b/buildSrc/src/main/kotlin/maven-artifact.gradle.kts
@@ -107,11 +107,14 @@ tasks {
         repositories {
             maven {
                 val releasesRepoUrl = uri(
-                    "https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/")
+                    "https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/"
+                )
                 val snapshotsRepoUrl = uri(
-                    "https://s01.oss.sonatype.org/content/repositories/snapshots/")
+                    "https://s01.oss.sonatype.org/content/repositories/snapshots/"
+                )
                 url = if (version.toString()
-                        .endsWith("SNAPSHOT")) snapshotsRepoUrl else releasesRepoUrl
+                        .endsWith("SNAPSHOT")
+                ) snapshotsRepoUrl else releasesRepoUrl
                 credentials {
                     username = System.getenv("OSSRH_USERNAME")
                     password = System.getenv("OSSRH_PASSWORD")