Fixed property-based violation node detection

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt

@@ -462,6 +462,7 @@ private fun postVerificationLogging(
             ),
             parseContext,
             witnessFile,
+            config.inputConfig.property,
           )
         val yamlWitnessFile = File(resultFolder, "witness.yml")
         YmlWitnessWriter()

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt

@@ -24,15 +24,17 @@ import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker
 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.functype.FuncAppExpr
 import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
-import hu.bme.mit.theta.xcfa.analysis.XcfaAction
-import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
-import hu.bme.mit.theta.xcfa.analysis.XcfaState
-import hu.bme.mit.theta.xcfa.analysis.isInlined
+import hu.bme.mit.theta.solver.ProofNode
+import hu.bme.mit.theta.xcfa.analysis.*
 import hu.bme.mit.theta.xcfa.cli.params.HornConfig
 import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
 import hu.bme.mit.theta.xcfa.model.XCFA
+import hu.bme.mit.theta.xcfa.model.XcfaLocation
 import hu.bme.mit.theta.xcfa2chc.toCHC
 
 fun getHornChecker(
@@ -60,10 +62,44 @@ fun getHornChecker(
     if (result.isSafe) {
       SafetyResult.safe(EmptyProof.getInstance())
     } else if (result.isUnsafe) {
-      val proof = result.asUnsafe().cex
-      val state =
-        XcfaState<PtrState<PredState>>(xcfa, mapOf(), PtrState(PredState.of(proof.proofNode.expr)))
-      SafetyResult.unsafe(Trace.of(listOf(state), listOf()), EmptyProof.getInstance())
+      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)
+      }
+
+      SafetyResult.unsafe(Trace.of(states.reversed(), actions.reversed()), EmptyProof.getInstance())
     } else {
       SafetyResult.unknown()
     }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/GraphmlWitnessWriter.kt

@@ -21,6 +21,7 @@ import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.solver.SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.cli.witnesses.GraphmlWitness
@@ -42,6 +43,7 @@ class GraphmlWitnessWriter {
     cexSolverFactory: SolverFactory,
     parseContext: ParseContext,
     witnessfile: File,
+    property: ErrorDetection,
   ) {
     // TODO eliminate the need for the instanceof check
     if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex is Trace<*, *>) {
@@ -52,7 +54,8 @@ class GraphmlWitnessWriter {
           parseContext,
         )
 
-      val witnessTrace = traceToWitness(trace = concrTrace, parseContext = parseContext)
+      val witnessTrace =
+        traceToWitness(trace = concrTrace, parseContext = parseContext, property = property)
       val graphmlWitness = GraphmlWitness(witnessTrace, inputFile)
       val xml = graphmlWitness.toPrettyXml()
       witnessfile.writeText(xml)

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt

@@ -81,7 +81,8 @@ class YmlWitnessWriter {
           parseContext,
         )
 
-      val witnessTrace = traceToWitness(trace = concrTrace, parseContext = parseContext)
+      val witnessTrace =
+        traceToWitness(trace = concrTrace, parseContext = parseContext, property = property)
 
       val witness =
         YamlWitness(

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt

@@ -18,15 +18,18 @@ package hu.bme.mit.theta.xcfa.cli.witnesses
 import com.google.common.collect.Lists
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.c2xcfa.getCMetaData
 import hu.bme.mit.theta.core.model.Valuation
 import hu.bme.mit.theta.core.stmt.HavocStmt
 import hu.bme.mit.theta.core.type.LitExpr
 import hu.bme.mit.theta.core.type.bvtype.BvLitExpr
 import hu.bme.mit.theta.core.type.fptype.FpLitExpr
 import hu.bme.mit.theta.frontend.ParseContext
+import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
+import hu.bme.mit.theta.xcfa.analysis.getXcfaErrorPredicate
 import hu.bme.mit.theta.xcfa.model.*
 import java.math.BigInteger
 
@@ -41,10 +44,13 @@ fun traceToWitness(
   verbosity: Verbosity = Verbosity.SOURCE_EXISTS,
   trace: Trace<XcfaState<ExplState>, XcfaAction>,
   parseContext: ParseContext,
+  property: ErrorDetection,
 ): Trace<WitnessNode, WitnessEdge> {
   val newStates = ArrayList<WitnessNode>()
   val newActions = ArrayList<WitnessEdge>()
 
+  val isError = getXcfaErrorPredicate(property)
+
   var lastNode =
     WitnessNode(id = "N${newStates.size}", entry = true, sink = false, violation = false)
   newStates.add(lastNode)
@@ -59,7 +65,17 @@ fun traceToWitness(
         id = "N${newStates.size}",
         entry = false,
         sink = false,
-        violation = state.processes.any { it.value.locs.any(XcfaLocation::error) },
+        violation =
+          isError.test( // this is a hack so that a simple explstate can become a ptrstate
+            XcfaState(
+              state.xcfa,
+              state.processes,
+              PtrState(state.sGlobal),
+              state.mutexes,
+              state.threadLookup,
+              state.bottom,
+            )
+          ),
         xcfaLocations = state.processes.map { Pair(it.key, it.value.locs) }.toMap(),
         cSources =
           state.processes
@@ -113,7 +129,17 @@ fun traceToWitness(
       id = "N${newStates.size}",
       entry = false,
       sink = false,
-      violation = lastState.processes.any { it.value.locs.any(XcfaLocation::error) },
+      violation =
+        isError.test( // this is a hack so that a simple explstate can become a ptrstate
+          XcfaState(
+            lastState.xcfa,
+            lastState.processes,
+            PtrState(lastState.sGlobal),
+            lastState.mutexes,
+            lastState.threadLookup,
+            lastState.bottom,
+          )
+        ),
       xcfaLocations = lastState.processes.map { Pair(it.key, it.value.locs) }.toMap(),
       cSources =
         lastState.processes

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java

@@ -91,7 +91,7 @@ public static Trace<XcfaState<ExplState>, XcfaAction> concretize(
         for (int i = 0; i < sbeTrace.getStates().size(); ++i) {
             cfaStates.add(
                     new XcfaState<>(
-                            null,
+                            sbeTrace.getState(i).getXcfa(),
                             sbeTrace.getState(i).getProcesses(),
                             ExplState.of(
                                     ImmutableValuation.from(