From 64f828a7aba4892e219197a679df48d6d4de9e03 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sun, 16 Feb 2025 21:53:11 +0100
Subject: [PATCH] fixed var naming and inductive/invariant flags

---
 .../theta/xcfa/cli/utils/YmlWitnessWriter.kt   | 18 +++++++++++++++---
 .../theta/xcfa/cli/witnesses/YamlWitness.kt    |  4 ++--
 2 files changed, 17 insertions(+), 5 deletions(-)

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
index 68e3673216..ace6ab8c21 100644
--- 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
@@ -23,8 +23,12 @@ import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.c2xcfa.CMetaData
+import hu.bme.mit.theta.core.decl.Decls.Var
+import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.Or
+import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.utils.ExprUtils
+import hu.bme.mit.theta.core.utils.changeVars
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
 import hu.bme.mit.theta.solver.SolverFactory
@@ -33,6 +37,7 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.cli.witnesses.*
 import hu.bme.mit.theta.xcfa.model.MetaData
+import hu.bme.mit.theta.xcfa.passes.changeVars
 import hu.bme.mit.theta.xcfa.toC
 import java.io.File
 import java.util.*
@@ -149,10 +154,9 @@ class YmlWitnessWriter {
                             concrTrace.actions[cycleHeadFirst - 1]?.edge?.metadata,
                           )
                           ?: error("Cycle head's metadata is missing."),
-                      value = cycleHead.sGlobal.toExpr().toC(parseContext),
+                      value =
+                        cycleHead.sGlobal.toExpr().replaceVars(parseContext).toC(parseContext),
                       format = "c_expression",
-                      invariant = false,
-                      inductive = false,
                     ),
                     (0..<lassoTrace.length()).flatMap {
                       listOfNotNull(
@@ -201,6 +205,14 @@ class YmlWitnessWriter {
   }
 }
 
+private fun Expr<BoolType>.replaceVars(parseContext: ParseContext): Expr<BoolType> {
+  val vars =
+    ExprUtils.getVars(this).associateWith {
+      Var(parseContext.metadata.getMetadataValue(it.name, "cName").get() as String, it.type)
+    }
+  return this.changeVars(vars)
+}
+
 private fun getLocation(inputFile: File, metadata: MetaData?): Location? {
   val line =
     (metadata as? CMetaData)?.lineNumberStart
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
index 3778dbfea0..46c7a7adb8 100644
--- 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
@@ -274,8 +274,8 @@ data class CycleHeadContent(
   val location: Location,
   val value: String,
   val format: String,
-  val invariant: Boolean?,
-  val inductive: Boolean?,
+  val invariant: Boolean? = null,
+  val inductive: Boolean? = null,
 )
 
 @Serializable