fixed witness formats

ftsrg · Feb 17, 2025 · a26a51f · a26a51f
1 parent 64f828a
commit a26a51f
Show file tree

Hide file tree

Showing 5 changed files with 57 additions and 91 deletions.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt
@@ -32,15 +32,15 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import java.util.*
 
 fun MonolithicExpr.createMonolithicL2S(): MonolithicExpr {
-  val saved = Decls.Var("saved", BoolType.getInstance())
+  val saved = Decls.Var("__saved_", BoolType.getInstance())
   val saveMap: MutableMap<VarDecl<*>, VarDecl<*>> = HashMap()
   val tmpVars: Set<VarDecl<*>> = Containers.createSet()
   ExprUtils.collectVars(initExpr, tmpVars)
   ExprUtils.collectVars(transExpr, tmpVars)
   ExprUtils.collectVars(propExpr, tmpVars)
   val vars = Collections.unmodifiableCollection(tmpVars)
   for (varDecl in vars) {
-    val newVar: VarDecl<*> = Decls.Var("_saved_" + varDecl.name, varDecl.type)
+    val newVar: VarDecl<*> = Decls.Var("__saved_" + varDecl.name, varDecl.type)
     saveMap[varDecl] = newVar
   }
 

diff --git a/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt
@@ -187,11 +187,12 @@ fun XCFA.valToState(val1: Valuation): XcfaState<PtrState<ExplState>> {
     PtrState(
       ExplState.of(
         ImmutableValuation.from(
-          val1
-            .toMap()
-            .filter { it.key.name != "__loc_" && !it.key.name.startsWith("__temp_") }
-            .map { Pair(Decls.Var("_" + "_" + it.key.name, it.key.type), it.value) }
-            .toMap()
+          val1.toMap().filter {
+            it.key.name != "__loc_" &&
+              it.key.name != "__edge_" &&
+              !it.key.name.startsWith("__temp_") &&
+              !it.key.name.startsWith("__saved_")
+          }
         )
       )
     ),

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt
@@ -139,35 +139,39 @@ class YmlWitnessWriter {
                   )
                 }
                 .map { ContentItem(it) } +
-                run {
-                  val loc = cycleHead.processes.values.first().locs.first
-                  ContentItem(
-                    CycleHeadContent(
-                      location =
-                        getLocation(inputFile, loc.metadata)
-                          ?: getLocation(inputFile, backEdgeTrace.actions.last())
-                          ?: getLocation(inputFile, backEdgeTrace.actions.last()?.edge?.metadata)
-                          ?: getLocation(inputFile, lassoTrace.actions.last())
-                          ?: getLocation(inputFile, lassoTrace.actions.last()?.edge?.metadata)
-                          ?: getLocation(
-                            inputFile,
-                            concrTrace.actions[cycleHeadFirst - 1]?.edge?.metadata,
-                          )
-                          ?: error("Cycle head's metadata is missing."),
-                      value =
-                        cycleHead.sGlobal.toExpr().replaceVars(parseContext).toC(parseContext),
-                      format = "c_expression",
-                    ),
-                    (0..<lassoTrace.length()).flatMap {
-                      listOfNotNull(
-                        lassoTrace.states
-                          .get(it)
-                          ?.toSegment(lassoTrace.actions.getOrNull(it - 1), inputFile),
-                        lassoTrace.actions.getOrNull(it)?.toSegment(inputFile),
-                      )
-                    },
+                ContentItem(
+                  WaypointContent(
+                    type = WaypointType.RECURRENCE_CONDITION,
+                    location =
+                      getLocation(inputFile, cycleHead.processes.values.first().locs.first.metadata)
+                        ?: getLocation(inputFile, backEdgeTrace.actions.last())
+                        ?: getLocation(inputFile, backEdgeTrace.actions.last()?.edge?.metadata)
+                        ?: getLocation(inputFile, lassoTrace.actions.last())
+                        ?: getLocation(inputFile, lassoTrace.actions.last()?.edge?.metadata)
+                        ?: getLocation(
+                          inputFile,
+                          concrTrace.actions[cycleHeadFirst - 1]?.edge?.metadata,
+                        )
+                        ?: error("Cycle head's metadata is missing."),
+                    constraint =
+                      Constraint(
+                        value =
+                          cycleHead.sGlobal.toExpr().replaceVars(parseContext).toC(parseContext),
+                        format = Format.C_EXPRESSION,
+                      ),
+                    action = Action.CYCLE,
                   )
-                },
+                ) +
+                (0..<lassoTrace.length())
+                  .flatMap {
+                    listOfNotNull(
+                      lassoTrace.states
+                        .get(it)
+                        ?.toSegment(lassoTrace.actions.getOrNull(it - 1), inputFile, Action.CYCLE),
+                      lassoTrace.actions.getOrNull(it)?.toSegment(inputFile, Action.CYCLE),
+                    )
+                  }
+                  .map { ContentItem(it) },
           )
         } else {
           val witnessTrace =
@@ -233,21 +237,28 @@ private fun getLocation(inputFile: File, witnessEdge: WitnessEdge?): Location? {
   return endLoc
 }
 
-private fun WitnessNode.toSegment(witnessEdge: WitnessEdge?, inputFile: File): WaypointContent? {
+private fun WitnessNode.toSegment(
+  witnessEdge: WitnessEdge?,
+  inputFile: File,
+  action: Action = Action.FOLLOW,
+): WaypointContent? {
   if (violation) {
     val loc = xcfaLocations.values.first().first()
     val locLoc =
       getLocation(inputFile, loc.metadata)
         ?: getLocation(inputFile, witnessEdge)
         ?: getLocation(inputFile, witnessEdge?.edge?.metadata)
         ?: return null
-    return WaypointContent(type = WaypointType.TARGET, location = locLoc, action = Action.FOLLOW)
+    return WaypointContent(type = WaypointType.TARGET, location = locLoc, action = action)
   } else {
     return null
   }
 }
 
-private fun WitnessEdge.toSegment(inputFile: File): WaypointContent? {
+private fun WitnessEdge.toSegment(
+  inputFile: File,
+  action: Action = Action.FOLLOW,
+): WaypointContent? {
   val endLoc =
     Location(
       fileName = inputFile.name,
@@ -277,12 +288,7 @@ private fun WitnessEdge.toSegment(inputFile: File): WaypointContent? {
     } else if (returnFromFunction != null) {
       Triple(endLoc, Constraint(value = returnFromFunction), WaypointType.FUNCTION_RETURN)
     } else return null
-  return WaypointContent(
-    type = type,
-    constraint = constraint,
-    location = loc,
-    action = Action.FOLLOW,
-  )
+  return WaypointContent(type = type, constraint = constraint, location = loc, action = action)
 }
 
 private fun Proof.toContent(inputFile: File, parseContext: ParseContext): List<ContentItem> {

diff --git a/...xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java b/...xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/XcfaTraceConcretizer.java
@@ -56,7 +56,7 @@ public static Trace<XcfaState<ExplState>, XcfaAction> concretize(
         List<XcfaState<PtrState<?>>> sbeStates = new ArrayList<>();
         List<XcfaAction> sbeActions = new ArrayList<>();
 
-        sbeStates.add(trace.getState(0).withState(new PtrState<>(ExplState.top())));
+        sbeStates.add(trace.getState(0));
 
         Map<Type, List<Triple<Expr<?>, Expr<?>, Expr<IntType>>>> nextW = Collections.emptyMap();
         for (int i = 0; i < trace.getActions().size(); ++i) {
@@ -74,7 +74,7 @@ public static Trace<XcfaState<ExplState>, XcfaAction> concretize(
                             trace.getAction(i).getInCnt());
             sbeActions.add(action);
             nextW = action.nextWriteTriples();
-            sbeStates.add(trace.getState(i + 1).withState(new PtrState<>(ExplState.top())));
+            sbeStates.add(trace.getState(i + 1));
         }
         Trace<XcfaState<?>, XcfaAction> sbeTrace = Trace.of(sbeStates, sbeActions);
         final ExprTraceChecker<ItpRefutation> checker =

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
@@ -156,30 +156,13 @@ enum class Language {
  *   a mapping that describes one invariant.
  */
 @Serializable
-data class ContentItem(
-  val segment: Segment? = null,
-  val invariant: Invariant? = null,
-  val cycle: Cycle? = null,
-) {
-  constructor(wpContent: WaypointContent) : this(listOf(Waypoint(wpContent)))
+data class ContentItem(val segment: Segment? = null, val invariant: Invariant? = null) {
 
-  constructor(
-    cycleHeadContent: CycleHeadContent,
-    segments: List<WaypointContent>,
-  ) : this(
-    cycle =
-      listOf(CycleItem(cycleHeadContent)) +
-        segments.map { CycleItem(segment = listOf(Waypoint(it))) }
-  )
+  constructor(wpContent: WaypointContent) : this(listOf(Waypoint(wpContent)))
 }
 
 typealias Segment = List<Waypoint>
 
-typealias Cycle = List<CycleItem>
-
-@Serializable
-data class CycleItem(val cycleHead: CycleHeadContent? = null, val segment: Segment? = null)
-
 @Serializable data class Waypoint(val waypoint: WaypointContent)
 
 /**
@@ -252,39 +235,14 @@ data class WaypointContent(
   val action: Action,
 )
 
-/**
- * A `cycle_head` expresses the recurrent set of the non-termination.
- *
- * @param location The location must point to the first character of an arbitrary statement or a
- *   declaration that is within a compound statement. If column is not given, it is assumed to match
- *   the leftmost suitable position.
- * @param value The key `value` holds the actual string expressing the recurrent set (e.g., "s <=
- *   i*255 && 0 <= i && i <= 255 && n <= 255"). The recurrent set value must be a side-effect-free C
- *   expression over variables in the scope of the statement or declaration inside a compound
- *   statement to which the location points.
- * @param format The format specifies the format of the invariant string (e.g., `c_expression`).
- * @param invariant The key `invariant` is a boolean value that is true if the recurrent set is an
- *   invariant. It is false if the recurrent set is not an invariant.
- * @param inductive The key `inductive` is a boolean value that is true if the recurrent set is a
- *   1-inductive invariant. It is false if the recurrent set is not an invariant or if it is an
- *   invariant which is not 1-inductive.
- */
-@Serializable
-data class CycleHeadContent(
-  val location: Location,
-  val value: String,
-  val format: String,
-  val invariant: Boolean? = null,
-  val inductive: Boolean? = null,
-)
-
 @Serializable
 enum class WaypointType {
   @SerialName("assumption") ASSUMPTION,
   @SerialName("target") TARGET,
   @SerialName("function_enter") FUNCTION_ENTER,
   @SerialName("function_return") FUNCTION_RETURN,
   @SerialName("branching") BRANCHING,
+  @SerialName("recurrence_condition") RECURRENCE_CONDITION,
 }
 
 /**
@@ -332,6 +290,7 @@ data class Location(
 enum class Action {
   @SerialName("follow") FOLLOW,
   @SerialName("avoid") AVOID,
+  @SerialName("cycle") CYCLE,
 }
 
 @Serializable