Fix memloc

.github/actions/build-spec-transformation/patch.diff

@@ -9,7 +9,7 @@ index 86a7a74e..56f3336a 100644
 -                [
 -                    f"lib/cpachecker/bin/cpachecker",
 +                [   "java", "-cp",
-+                    f"{os.path.dirname(os.path.dirname(__file__))}/cpachecker/runtime/*:{os.path.dirname(os.path.dirname(__file__))}/cpachecker/cpachecker.jar",
++                    f"{os.path.dirname(os.path.dirname(os.path.dirname(__file__)))}/cpachecker/runtime/*:{os.path.dirname(os.path.dirname(os.path.dirname(__file__)))}/cpachecker/cpachecker.jar",
 +                    "org.sosy_lab.cpachecker.cmdline.CPAMain",
                      "--preprocess",
                      "--option",

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.5"
+    version = "6.8.6"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

scripts/theta-start.sh

@@ -7,6 +7,11 @@ IN=$1
 export VERIFIER_NAME=TOOL_NAME
 export VERIFIER_VERSION=TOOL_VERSION
 
+if [ "$1" == "--version" ]; then
+    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version || echo $VERIFIER_VERSION
+    exit
+fi
+
 JAVA_VERSION=17
 JAVA_FALLBACK_PATH="/usr/lib/jvm/java-$JAVA_VERSION-openjdk-amd64/bin/:/usr/lib/jvm/java-$JAVA_VERSION-openjdk/bin/:/usr/lib/jvm/java-$JAVA_VERSION/bin/"
 grep -o "openjdk $JAVA_VERSION" <<< "$(java --version)" >/dev/null || export PATH="$JAVA_FALLBACK_PATH":$PATH
@@ -33,35 +38,31 @@ remove_property() {
     echo "${args[@]}"
 }
 
-if [ "$1" == "--version" ]; then
-    LD_LIBRARY_PATH=$scriptdir/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar --version
-else
-    modified_args=$(remove_property "${@:2}")
-    property=$(cat .property && rm .property)
-    echo "Verifying input '$IN' with property '$property' using arguments '$modified_args'"
+modified_args=$(remove_property "${@:2}")
+property=$(cat .property && rm .property)
+echo "Verifying input '$IN' with property '$property' using arguments '$modified_args'"
 
-    if [ "$(basename "$property")" == "termination.prp" ]; then
-        transformed_property=$(dirname "$property")/unreach-call.prp
-        echo "Mapping property '$property' to '$transformed_property'"
-        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
-        "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
-        IN="output/transformed_program.c"
-    elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
-        transformed_property=$(dirname "$property")/unreach-call.prp
-        echo "Mapping property '$property' to '$transformed_property'"
-        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
-        "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
-        IN="output/transformed_program.c"
-    else
-        transformed_property="$property"
-    fi
+if [ "$(basename "$property")" == "termination.prp" ]; then
+    transformed_property=$(dirname "$property")/unreach-call.prp
+    echo "Mapping property '$property' to '$transformed_property'"
+    python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
+    "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
+    IN="output/transformed_program.c"
+elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
+    transformed_property=$(dirname "$property")/unreach-call.prp
+    echo "Mapping property '$property' to '$transformed_property'"
+    python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
+    "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
+    IN="output/transformed_program.c"
+else
+    transformed_property="$property"
+fi
 
-    echo LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
-    LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
+echo LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
+LD_LIBRARY_PATH="$scriptdir"/lib java -Xss120m -Xmx14210m -jar "$scriptdir"/theta.jar $modified_args --input "$IN" --property "$transformed_property" --smt-home "$scriptdir"/solvers
 
-    if [ "$(basename "$property")" == "termination.prp" ]; then
-        echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
-    elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
-        echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
-    fi
+if [ "$(basename "$property")" == "termination.prp" ]; then
+    echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
+elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
+    echo "Not yet mapping witnesses from '$transformed_property' to '$property', hoping for the best"
 fi

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaExactPo.kt

@@ -16,47 +16,60 @@
 package hu.bme.mit.theta.xcfa.analysis.oc
 
 import hu.bme.mit.theta.xcfa.model.XcfaEdge
+import hu.bme.mit.theta.xcfa.model.XcfaLabel
 import hu.bme.mit.theta.xcfa.model.XcfaLocation
 import hu.bme.mit.theta.xcfa.model.XcfaProcedure
 
-internal class XcfaExactPo(private val threads: Set<Thread>) {
+private data class GlobalEdge(
+  val pid: Int,
+  val source: XcfaLocation?,
+  val target: XcfaLocation,
+  val label: XcfaLabel?,
+) {
 
-  private val reachableEdges = threads.associate { it.pid to ReachableEdges(it.procedure) }
+  constructor(pid: Int, edge: XcfaEdge) : this(pid, edge.source, edge.target, edge.label)
 
-  private data class Edge(val source: XcfaLocation?, val target: XcfaLocation, val pid: Int) {
+  constructor(event: E) : this(event.pid, event.edge)
+}
 
-    val edge: Pair<XcfaLocation?, XcfaLocation>
-      get() = source to target
+private data class LocalEdge(
+  val source: XcfaLocation?,
+  val target: XcfaLocation,
+  val label: XcfaLabel?,
+) {
+  constructor(edge: XcfaEdge) : this(edge.source, edge.target, edge.label)
 
-    constructor(event: E) : this(event.edge.source, event.edge.target, event.pid)
-  }
+  constructor(edge: GlobalEdge) : this(edge.source, edge.target, edge.label)
+}
+
+internal class XcfaExactPo(private val threads: Set<Thread>) {
+
+  private val reachableEdges = threads.associate { it.pid to ReachableEdges(it.procedure) }
 
   fun isPo(from: E?, to: E): Boolean {
     from ?: return true
     if (from.clkId == to.clkId) return true
-    val possiblePathPoints = mutableListOf(Edge(from))
-    val visited = mutableSetOf<Edge>()
+    val possiblePathPoints = mutableListOf(GlobalEdge(from))
+    val visited = mutableSetOf<GlobalEdge>()
     while (possiblePathPoints.isNotEmpty()) {
       val current = possiblePathPoints.removeFirst()
       if (!visited.add(current)) continue
-      if (current.pid == to.pid && reachableEdges[current.pid]!!.reachable(current.edge, to.edge))
+      if (current.pid == to.pid && reachableEdges[current.pid]!!.reachable(current, to.edge))
         return true
 
       threads
         .filter {
           it.startEvent?.pid == current.pid &&
-            reachableEdges[current.pid]!!.reachable(current.edge, it.startEvent.edge)
+            reachableEdges[current.pid]!!.reachable(current, it.startEvent.edge)
         }
         .forEach { thread ->
-          possiblePathPoints.add(Edge(null, thread.procedure.initLoc, thread.pid))
+          possiblePathPoints.add(GlobalEdge(thread.pid, null, thread.procedure.initLoc, null))
         }
 
       threads
         .find { it.pid == current.pid }
         ?.let { thread ->
-          thread.joinEvents.forEach {
-            possiblePathPoints.add(Edge(it.edge.source, it.edge.target, it.pid))
-          }
+          thread.joinEvents.forEach { possiblePathPoints.add(GlobalEdge(it.pid, it.edge)) }
         }
     }
 
@@ -66,45 +79,41 @@ internal class XcfaExactPo(private val threads: Set<Thread>) {
 
 private class ReachableEdges(procedure: XcfaProcedure) {
 
-  private data class Edge(val source: XcfaLocation?, val target: XcfaLocation) {
-    constructor(edge: XcfaEdge) : this(edge.source, edge.target)
-  }
-
-  private infix fun XcfaLocation?.to(other: XcfaLocation) = Edge(this, other)
+  private infix fun XcfaLocation?.to(other: XcfaLocation) = LocalEdge(this, other, null)
 
-  private val ids = mutableMapOf<Edge, Int>()
+  private val ids = mutableMapOf<LocalEdge, Int>()
   private var reachable: Array<Array<Boolean>>
 
   init {
     val toVisit = mutableListOf(null to procedure.initLoc)
     val initials = mutableListOf<Pair<Int, Int>>()
     while (toVisit.isNotEmpty()) { // assumes xcfa contains no cycles (an OC checker requirement)
-      val (source, target) = toVisit.removeFirst()
+      val edge = toVisit.removeFirst()
       val id = ids.size
-      ids[source to target] = id
+      ids[edge] = id
 
-      if (source == procedure.initLoc) {
+      if (edge.source == procedure.initLoc) {
         initials.add(ids[null to procedure.initLoc]!! to id)
       } else {
-        source
+        edge.source
           ?.incomingEdges
-          ?.filter { Edge(it) in ids }
-          ?.forEach { initials.add(ids[Edge(it)]!! to id) }
+          ?.filter { LocalEdge(it) in ids }
+          ?.forEach { initials.add(ids[LocalEdge(it)]!! to id) }
       }
-      target.outgoingEdges
-        .filter { Edge(it) in ids }
-        .forEach { initials.add(id to ids[Edge(it)]!!) }
+      edge.target.outgoingEdges
+        .filter { LocalEdge(it) in ids }
+        .forEach { initials.add(id to ids[LocalEdge(it)]!!) }
 
       val toAdd =
-        target.outgoingEdges.map { it.source to it.target }.filter { it !in ids && it !in toVisit }
+        edge.target.outgoingEdges.map { LocalEdge(it) }.filter { it !in ids && it !in toVisit }
       toVisit.addAll(toAdd)
     }
     reachable = Array(ids.size) { Array(ids.size) { false } }
     close(initials) // close reachable transitively
   }
 
-  fun reachable(from: Pair<XcfaLocation?, XcfaLocation>, to: XcfaEdge): Boolean =
-    reachable[ids[from.first to from.second]!!][ids[Edge(to)]!!]
+  fun reachable(from: GlobalEdge, to: XcfaEdge): Boolean =
+    reachable[ids[LocalEdge(from)]!!][ids[LocalEdge(to)]!!]
 
   private fun close(initials: List<Pair<Int, Int>>) {
     val toClose = initials.toMutableList()

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt

@@ -154,11 +154,12 @@ class XcfaOcChecker(
       }
       .also {
         logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it")
-        if (xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) {
+        if (it.isSafe && xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) {
           logger.writeln(
             Logger.Level.MAINSTEP,
             "Incomplete loop unroll used: safe result is unreliable.",
           )
+          logger.writeln(Logger.Level.RESULT, SafetyResult.unknown<EmptyProof, Cex>().toString())
           throw NotSolvableException()
         }
       }