From e11abb63cccfc2553d01b3f2843979fb85bdceac Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Wed, 20 Nov 2024 21:10:37 +0100
Subject: [PATCH] Fixed tests

---
 .../xcfa/cli/checkers/ConfigToHornChecker.kt  | 101 +++++++++++-------
 1 file changed, 65 insertions(+), 36 deletions(-)

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
index b8d9c6acd8..2e73009d5f 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
@@ -20,12 +20,15 @@ import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.EmptyProof
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.chc.CexTree
 import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker
+import hu.bme.mit.theta.analysis.algorithm.chc.Invariant
 import hu.bme.mit.theta.analysis.pred.PredState
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.anytype.RefExpr
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.core.type.functype.FuncAppExpr
 import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
 import hu.bme.mit.theta.solver.ProofNode
@@ -62,46 +65,72 @@ fun getHornChecker(
     if (result.isSafe) {
       SafetyResult.safe(EmptyProof.getInstance())
     } else if (result.isUnsafe) {
-      val getName = { s: String ->
-        val split = s.split("_")
-        val allButLast = split.subList(0, split.size - 1)
-        allButLast.joinToString("_")
-      }
-      val loc = { proofNode: ProofNode ->
-        if (proofNode.expr is FuncAppExpr<*, *>) {
-          var func: Expr<*> = proofNode.expr
-          while (func is FuncAppExpr<*, *>) {
-            func = func.func
-          }
-          func as RefExpr<*>
-          xcfa.procedures.flatMap { it.locs }.first { it.name == getName(func.decl.name) }
-        } else null
-      }
-      val states = mutableListOf<XcfaState<PtrState<*>>>()
-      val actions = mutableListOf<XcfaAction>()
-      var proofNode: ProofNode? = result.asUnsafe().cex.proofNode
-      var lastLoc: XcfaLocation? = null
-      while (proofNode != null) {
-        loc(proofNode)?.also { currentLoc ->
-          states.add(XcfaState(xcfa, currentLoc, PtrState(PredState.of())))
-          lastLoc?.also {
-            actions.add(
-              XcfaAction(
-                0,
-                xcfa.procedures
-                  .flatMap { it.edges }
-                  .first { it.source == currentLoc && it.target == lastLoc },
+      try {
+        getProperTrace(xcfa, result)
+      } catch (t: Throwable) {
+        SafetyResult.unsafe(
+          Trace.of(
+            listOf(
+              XcfaState(
+                xcfa,
+                xcfa.initProcedures.get(0).first.errorLoc.get(),
+                PtrState(PredState.of(True())),
               )
-            )
-          }
-          lastLoc = currentLoc
-        }
-        proofNode = proofNode.children.getOrNull(0)
+            ),
+            listOf(),
+          ),
+          EmptyProof.getInstance(),
+        )
       }
-
-      SafetyResult.unsafe(Trace.of(states.reversed(), actions.reversed()), EmptyProof.getInstance())
     } else {
       SafetyResult.unknown()
     }
   }
 }
+
+private fun getProperTrace(
+  xcfa: XCFA,
+  result: SafetyResult<Invariant, CexTree>,
+): SafetyResult.Unsafe<EmptyProof, Trace<XcfaState<out PtrState<*>>, XcfaAction>>? {
+  val getName = { s: String ->
+    val split = s.split("_")
+    val allButLast = split.subList(0, split.size - 1)
+    allButLast.joinToString("_")
+  }
+  val loc = { proofNode: ProofNode ->
+    if (proofNode.expr is FuncAppExpr<*, *>) {
+      var func: Expr<*> = proofNode.expr
+      while (func is FuncAppExpr<*, *>) {
+        func = func.func
+      }
+      func as RefExpr<*>
+      xcfa.procedures.flatMap { it.locs }.first { it.name == getName(func.decl.name) }
+    } else null
+  }
+  val states = mutableListOf<XcfaState<PtrState<*>>>()
+  val actions = mutableListOf<XcfaAction>()
+  var proofNode: ProofNode? = result.asUnsafe().cex.proofNode
+  var lastLoc: XcfaLocation? = null
+  while (proofNode != null) {
+    loc(proofNode)?.also { currentLoc ->
+      states.add(XcfaState(xcfa, currentLoc, PtrState(PredState.of())))
+      lastLoc?.also {
+        actions.add(
+          XcfaAction(
+            0,
+            xcfa.procedures
+              .flatMap { it.edges }
+              .first { it.source == currentLoc && it.target == lastLoc },
+          )
+        )
+      }
+      lastLoc = currentLoc
+    }
+    proofNode = proofNode.children.getOrNull(0)
+  }
+
+  return SafetyResult.unsafe(
+    Trace.of(states.reversed(), actions.reversed()),
+    EmptyProof.getInstance(),
+  )
+}