Merge origin/main

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

@@ -20,29 +20,32 @@ runs:
       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
+    - name: Get sv-benchmarks (retry max. 3 times)
+      uses: nick-fields/retry@7152eba30c6575329ac0576536151aca5a72780e # v3.0.0
+      with:
+        timeout_minutes: 15
+        max_attempts: 3
+        shell: bash
+        command: git clone --filter=blob:none --no-checkout --depth 1 --sparse https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git
+    - name: Get C folder (retry max. 3 times)
+      uses: nick-fields/retry@7152eba30c6575329ac0576536151aca5a72780e # v3.0.0
+      with:
+        timeout_minutes: 15
+        max_attempts: 3
+        shell: bash
+        command: |
+          cd sv-benchmarks
+          git sparse-checkout add c
+          git checkout
     - uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
-      name: Get JAR
+      name: Get zip
       with:
-        name: ThetaJars
-        path: jar/
-    - name: Add new jar to archive
+        name: Theta_SV-COMP
+        path: release/
+    - name: Unzip 
       shell: bash
       run: |
-        mv jar/xcfa/xcfa-cli/build/libs/*-all.jar theta/theta.jar
-        ls -l theta
+        unzip release/Theta.zip
     - name: Cut setfile if too long
       id: setfile 
       shell: bash
@@ -56,7 +59,7 @@ runs:
       shell: bash
       if: steps.setfile.outputs.length != '0'
       run: |
-        benchexec xml/theta.xml --no-container --tool-directory theta -t ${{ inputs.task }}
+        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'

.github/actions/cache-build/action.yml

@@ -16,5 +16,5 @@ runs:
     - name: build gradle
       uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
       with:
-        arguments: ${{ inputs.arguments }}
+        arguments: ${{ inputs.arguments }} --info --stacktrace --max-workers 2 --no-daemon
 

.github/actions/create-release/action.yml

@@ -24,7 +24,7 @@ runs:
         echo "tagname=v$version" >> $GITHUB_OUTPUT
         EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
         echo "message<<$EOF" >> $GITHUB_OUTPUT
-        echo $message >> $GITHUB_OUTPUT
+        echo "$message" >> $GITHUB_OUTPUT
         echo "$EOF" >> $GITHUB_OUTPUT
     - name: Verify variables
       shell: bash

.github/actions/docker-deploy/action.yml

@@ -16,18 +16,18 @@ runs:
   steps:
     - name: Checkout
       uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
-    - name: Extract metadata (tags, labels) for DockerHub
-      id: metaDH
-      uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e
-      with:
-        images: ${{ inputs.user-dockerhub }}/${{ inputs.project }}
-        tags: type:raw, value=${{ inputs.version }}
-    - name: Extract metadata (tags, labels) for ghcr.io
-      id: metaGH
-      uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e
-      with:
-        images: ghcr.io/${{ inputs.user-ghcr }}/${{ inputs.project }}
-        tags: type:raw, value=${{ inputs.version }}
+    # - name: Extract metadata (tags, labels) for DockerHub
+    #   id: metaDH
+    #   uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e
+    #   with:
+    #     images: ${{ inputs.user-dockerhub }}/${{ inputs.project }}
+    #     tags: type:raw, value=${{ inputs.version }}
+    # - name: Extract metadata (tags, labels) for ghcr.io
+    #   id: metaGH
+    #   uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e
+    #   with:
+    #     images: ghcr.io/${{ inputs.user-ghcr }}/${{ inputs.project }}
+    #     tags: type:raw, value=${{ inputs.version }}
     - name: Creating path
       id: 'path'
       shell: bash
@@ -39,11 +39,11 @@ runs:
         context: .
         file: ${{ steps.path.outputs.path }}
         push: ${{ inputs.push }}
-        tags: ${{ steps.metaDH.outputs.tags }}
+        tags: ${{ inputs.user-dockerhub }}/${{ inputs.project }}:${{ inputs.version }}
     - name: Build and push to ghcr.io
       uses: docker/build-push-action@2eb1c1961a95fc15694676618e422e8ba1d63825
       with:
         context: .
         file: ${{ steps.path.outputs.path }}
         push: ${{ inputs.push }}
-        tags: ${{ steps.metaGH.outputs.tags }}
+        tags: ghcr.io/${{ inputs.user-ghcr }}/${{ inputs.project }}:${{ inputs.version }}

.github/workflows/linux-build-test-deploy.yml

@@ -13,7 +13,7 @@ on:
 permissions: write-all
 
 concurrency: 
-  group: deploy-${{ github.head_ref }}
+  group: deploy-${{ github.head_ref }}-${{ github.event_name }}
   cancel-in-progress: true
 
 jobs:
@@ -51,7 +51,7 @@ jobs:
       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]
     runs-on: ubuntu-latest
-    needs: build
+    needs: create-archives
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -162,7 +162,7 @@ jobs:
   test-docker:
     strategy:
       matrix:
-        dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli"]
+        dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
@@ -196,7 +196,7 @@ jobs:
     if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
     strategy:
       matrix:
-        dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli"]
+        dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository

.github/workflows/mac-build-test.yml

@@ -15,7 +15,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [macos-latest, macos-13, macos-12, macos-11]
+        os: [macos-latest, macos-13, macos-12]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout repository

.github/workflows/sonar.yml

@@ -33,7 +33,7 @@ jobs:
         if: env.SONAR_TOKEN != '' && github.event_name == 'push'
         uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
         with:
-          arguments: build jacocoTestReport sonar --info -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m
+          arguments: build jacocoTestReport sonar --stacktrace --info --max-workers 2 --no-daemon -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m
       - name: Checkout source branch
         if: github.event_name == 'pull_request_target'
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -48,4 +48,4 @@ jobs:
         if: env.SONAR_TOKEN != '' && github.event_name == 'pull_request_target' && contains(github.event.pull_request.labels.*.name, 'Ready to test')
         uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
         with:
-          arguments: build jacocoTestReport sonar --info -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m  -Dsonar.pullrequest.key=${{ github.event.pull_request.number }}
+          arguments: build jacocoTestReport sonar --info --max-workers 2 --no-daemon -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m  -Dsonar.pullrequest.key=${{ github.event.pull_request.number }}

README.md

@@ -6,14 +6,21 @@
 ![](https://raw.githubusercontent.com/ftsrg/theta/badges/badges/test-Linux/badge.svg)
 ![](https://raw.githubusercontent.com/ftsrg/theta/badges/badges/test-Windows/badge.svg)
 ![](https://raw.githubusercontent.com/ftsrg/theta/badges/badges/test-macOS/badge.svg)
+
+[![](https://img.shields.io/docker/v/ftsrg/theta-cfa-cli?label=cfa&logo=docker)](https://hub.docker.com/r/ftsrg/theta-cfa-cli/)
+[![](https://img.shields.io/docker/v/ftsrg/theta-xsts-cli?label=xsts&logo=docker)](https://hub.docker.com/r/ftsrg/theta-xsts-cli/)
+[![](https://img.shields.io/docker/v/ftsrg/theta-xcfa-cli?label=xcfa&logo=docker)](https://hub.docker.com/r/ftsrg/theta-xcfa-cli/)
+[![](https://img.shields.io/docker/v/ftsrg/theta-xta-cli?label=xta&logo=docker)](https://hub.docker.com/r/ftsrg/theta-xta-cli/)
+[![](https://img.shields.io/docker/v/ftsrg/theta-sts-cli?label=sts&logo=docker)](https://hub.docker.com/r/ftsrg/theta-sts-cli/)
+
 [![Coverage](https://sonarcloud.io/api/project_badges/measure?project=ftsrg_theta&metric=coverage)](https://sonarcloud.io/summary/new_code?id=ftsrg_theta)
 [![Maintainability Rating](https://sonarcloud.io/api/project_badges/measure?project=ftsrg_theta&metric=sqale_rating)](https://sonarcloud.io/summary/new_code?id=ftsrg_theta)
 [![Quality Gate Status](https://sonarcloud.io/api/project_badges/measure?project=ftsrg_theta&metric=alert_status)](https://sonarcloud.io/summary/new_code?id=ftsrg_theta)
 [![Check copyright](https://github.com/ftsrg/theta/actions/workflows/check-copyright.yml/badge.svg)](https://github.com/ftsrg/theta/actions/workflows/check-copyright.yml)
 [![Check formatting](https://github.com/ftsrg/theta/actions/workflows/check-formatting.yml/badge.svg)](https://github.com/ftsrg/theta/actions/workflows/check-formatting.yml)
 [![Apache 2.0 License](https://img.shields.io/badge/license-Apache--2-brightgreen.svg?style=flat)](https://www.apache.org/licenses/LICENSE-2.0)
 
-![Theta logo](doc/theta-logo.png)
+![Theta logo](https://raw.githubusercontent.com/ftsrg/theta/master/doc/theta-logo.png)
 
 ## About
 
@@ -53,7 +60,7 @@ Theta can be divided into the following four layers.
   Formalisms are usually low level, mathematical representations based on first order logic expressions and graph like structures.
   Formalisms can also support higher level languages that can be mapped to that particular formalism by a language front-end (consisting of a specific parser and possibly reductions for simplification of the model).
   The common features of the different formalisms reside in the [`core`](subprojects/common/core) project (e.g., expressions and statements) and each formalism has its own project.
-  Currently, the following formalisms are supported: (extended) symbolic transition systems ([`sts`](subprojects/sts/sts) / [`xsts`](subprojects/xsts/xsts)), control-flow automata ([`cfa`](subprojects/cfa/cfa)) and timed automata ([`xta`](subprojects/xta/xta)).
+  Currently, the following formalisms are supported: (extended) symbolic transition systems ([`sts`](subprojects/sts/sts) / [`xsts`](subprojects/xsts/xsts)), (extended) control-flow automata ([`cfa`](subprojects/cfa/cfa) / [`xcfa`](subprojects/xcfa/xcfa)) and timed automata ([`xta`](subprojects/xta/xta)).
 * **Analysis back-end**: The analysis back-end provides the verification algorithms that can formally prove whether a model meets certain requirements.
   There is an interpreter for each formalism, providing a common interface towards the algorithms (e.g., calculating initial states and successors).
   This ensures that most components of the algorithms work for all formalisms (as long as they provide the interpreter).

buildSrc/gradle.properties

@@ -1,3 +1,19 @@
+#
+#  Copyright 2024 Budapest University of Technology and Economics
+#
+#  Licensed under the Apache License, Version 2.0 (the "License");
+#  you may not use this file except in compliance with the License.
+#  You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+#  Unless required by applicable law or agreed to in writing, software
+#  distributed under the License is distributed on an "AS IS" BASIS,
+#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#  See the License for the specific language governing permissions and
+#  limitations under the License.
+#
+
 javaVersion=17
 kotlinVersion=1.7.10
 shadowVersion=7.1.2
@@ -9,4 +25,6 @@ junitVersion=5.9.3
 junit4Version=4.12
 jacocoVersion=0.8.8
 mockitoVersion=2.2.11
-gsonVersion=2.9.1
+gsonVersion=2.9.1
+javasmtVersion=4.1.1
+sosylabVersion=0.3000-569-g89796f98

buildSrc/src/main/kotlin/Deps.kt

@@ -13,6 +13,7 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
+
 object Deps {
 
     val guava = "com.google.guava:guava:${Versions.guava}"
@@ -25,6 +26,13 @@ object Deps {
     }
 
     val z3 = "lib/com.microsoft.z3.jar"
+    val z3legacy = "lib/com.microsoft.z3legacy.jar"
+
+    val cvc5 = "lib/cvc5.jar"
+
+    val javasmt = "org.sosy-lab:java-smt:${Versions.javasmt}"
+    val javasmtLocal = "lib/javasmt.jar"
+    val sosylabCommon = "org.sosy-lab:common:${Versions.sosylab}"
 
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"
 

buildSrc/src/main/kotlin/java-common.gradle.kts

@@ -56,4 +56,8 @@ tasks {
     withType<Test> {
         useJUnitPlatform()
     }
+
+    withType<Test> {
+        jvmArgs("-Xss5m", "-Xms512m", "-Xmx1g")
+    }
 }

docker/run-theta-xcfa-cli.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+set -Eeuxo pipefail
+
+DOCKER_RUN_OPTIONS="-i"
+
+# Only allocate tty if we detect one
+if [ -t 0 ] && [ -t 1 ]; then
+    DOCKER_RUN_OPTIONS="$DOCKER_RUN_OPTIONS -t"
+fi
+
+ABSPATH=$(realpath "$1")
+DIR=$(dirname "$ABSPATH")
+FILE=/host/$(basename "$ABSPATH")
+shift
+
+docker run "$DOCKER_RUN_OPTIONS" --mount type=bind,source="$DIR",target=/host theta-xcfa-cli:latest --model "$FILE" "$@"

docker/theta-cfa-cli.Dockerfile

@@ -1,7 +1,7 @@
 FROM openjdk:17.0.2-slim
 
 RUN apt-get update && \
-    apt-get install -y --no-install-recommends libgomp1 && \
+    apt-get install -y --no-install-recommends libgomp1 libmpfr-dev && \
     apt-get clean && rm -rf /var/lib/apt/lists/*
 
 RUN mkdir theta

docker/theta-sts-cli.Dockerfile

@@ -1,7 +1,7 @@
 FROM openjdk:17.0.2-slim
 
 RUN apt-get update && \
-    apt-get install -y --no-install-recommends libgomp1 && \
+    apt-get install -y --no-install-recommends libgomp1 libmpfr-dev && \
     apt-get clean && rm -rf /var/lib/apt/lists/*
 
 RUN mkdir theta

docker/theta-xcfa-cli.Dockerfile

@@ -0,0 +1,16 @@
+FROM openjdk:17.0.2-slim
+
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends libgomp1 libmpfr-dev && \
+    apt-get clean && rm -rf /var/lib/apt/lists/*
+
+RUN mkdir theta
+COPY . theta
+WORKDIR /theta
+RUN ./gradlew clean && \
+    ./gradlew theta-xcfa-cli:build && \
+    mv subprojects/xcfa/xcfa-cli/build/libs/theta-xcfa-cli-*-all.jar /theta-xcfa-cli.jar
+WORKDIR /
+
+ENV LD_LIBRARY_PATH="$LD_LIBRARY_PATH:./theta/lib/"
+ENTRYPOINT ["java", "-jar", "theta-xcfa-cli.jar"]

docker/theta-xsts-cli.Dockerfile

@@ -1,7 +1,7 @@
 FROM openjdk:17.0.2-slim
 
 RUN apt-get update && \
-    apt-get install -y --no-install-recommends libgomp1 && \
+    apt-get install -y --no-install-recommends libgomp1 libmpfr-dev && \
     apt-get clean && rm -rf /var/lib/apt/lists/*
 
 RUN mkdir theta

docker/theta-xta-cli.Dockerfile

@@ -1,7 +1,7 @@
 FROM openjdk:17.0.2-slim
 
 RUN apt-get update && \
-    apt-get install -y --no-install-recommends libgomp1 && \
+    apt-get install -y --no-install-recommends libgomp1 libmpfr-dev && \
     apt-get clean && rm -rf /var/lib/apt/lists/*
 
 RUN mkdir theta