malloc var fix

ftsrg · Oct 24, 2024 · 5a8ad9b · 5a8ad9b
1 parent 45909fa
commit 5a8ad9b
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 12 deletions.
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Visualizer.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Visualizer.kt
@@ -15,7 +15,38 @@
  */
 package hu.bme.mit.theta.xcfa.model
 
-fun XCFA.toDot(edgeLabelCustomizer: ((XcfaEdge) -> String)? = null): String {
+typealias LabelCustomizer = (XcfaEdge) -> String
+
+fun XCFA.toDot(edgeLabelCustomizer: LabelCustomizer? = null): String =
+  xcfaToDot(name, procedures.map { DottableProcedure(it) }, edgeLabelCustomizer)
+
+fun XcfaProcedure.toDot(edgeLabelCustomizer: LabelCustomizer?): String =
+  xcfaProcedureToDot(name, locs, edges, edgeLabelCustomizer)
+
+@Suppress("unused")
+fun XcfaBuilder.toDot(edgeLabelCustomizer: LabelCustomizer? = null): String =
+  xcfaToDot(name, getProcedures().map { DottableProcedure(it) }, edgeLabelCustomizer)
+
+fun XcfaProcedureBuilder.toDot(edgeLabelCustomizer: LabelCustomizer?): String =
+  xcfaProcedureToDot(name, getLocs(), getEdges(), edgeLabelCustomizer)
+
+private class DottableProcedure(
+  private val procedure: XcfaProcedure?,
+  private val procedureBuilder: XcfaProcedureBuilder?,
+) {
+  constructor(procedure: XcfaProcedure) : this(procedure, null)
+
+  constructor(procedureBuilder: XcfaProcedureBuilder) : this(null, procedureBuilder)
+
+  fun toDot(edgeLabelCustomizer: LabelCustomizer? = null): String =
+    procedure?.toDot(edgeLabelCustomizer) ?: procedureBuilder!!.toDot(edgeLabelCustomizer)
+}
+
+private fun xcfaToDot(
+  name: String,
+  procedures: List<DottableProcedure>,
+  edgeLabelCustomizer: LabelCustomizer? = null,
+): String {
   val builder = StringBuilder()
   builder.appendLine("digraph G {")
   builder.appendLine("label=\"$name\";")
@@ -30,7 +61,12 @@ fun XCFA.toDot(edgeLabelCustomizer: ((XcfaEdge) -> String)? = null): String {
   return builder.toString()
 }
 
-fun XcfaProcedure.toDot(edgeLabelCustomizer: ((XcfaEdge) -> String)?): String {
+private fun xcfaProcedureToDot(
+  name: String,
+  locs: Set<XcfaLocation>,
+  edges: Set<XcfaEdge>,
+  edgeLabelCustomizer: LabelCustomizer? = null,
+): String {
   val builder = StringBuilder()
   builder.appendLine("label=\"$name\";")
   locs.forEach { builder.appendLine("${it.name}[];") }

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt
@@ -15,17 +15,16 @@
  */
 package hu.bme.mit.theta.xcfa.passes
 
-import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.core.decl.Decls.Var
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.AssignStmt
 import hu.bme.mit.theta.core.stmt.Stmts.Assign
 import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add
 import hu.bme.mit.theta.core.type.anytype.RefExpr
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.utils.TypeUtils.cast
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
-import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.model.*
 
@@ -34,8 +33,8 @@ import hu.bme.mit.theta.xcfa.model.*
  */
 class MallocFunctionPass(val parseContext: ParseContext) : ProcedurePass {
 
-  private val XcfaBuilder.malloc: VarDecl<*> by lazy {
-    Var("__malloc", CPointer(null, null, parseContext).smtType)
+  companion object {
+    private val mallocVar: VarDecl<*> = Var("__malloc", Int())
   }
 
   override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
@@ -51,13 +50,12 @@ class MallocFunctionPass(val parseContext: ParseContext) : ProcedurePass {
           if (predicate((it.label as SequenceLabel).labels[0])) {
             val invokeLabel = it.label.labels[0] as InvokeLabel
             val ret = invokeLabel.params[0] as RefExpr<*>
-            val mallocVar = builder.parent.malloc
             if (builder.parent.getVars().none { it.wrappedVar == mallocVar }) { // initial creation
               builder.parent.addVar(
                 XcfaGlobalVar(mallocVar, CComplexType.getType(ret, parseContext).nullValue)
               )
               val initProc = builder.parent.getInitProcedures().map { it.first }
-              checkState(initProc.size == 1, "Multiple start procedure are not handled well")
+              check(initProc.size == 1) { "Multiple start procedure are not handled well" }
               initProc.forEach {
                 val initAssign =
                   StmtLabel(

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
@@ -41,8 +41,8 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL
       CLibraryFunctionsPass(),
     ),
     listOf(
-        ReferenceElimination(parseContext),
-        MallocFunctionPass(parseContext),
+      ReferenceElimination(parseContext),
+      MallocFunctionPass(parseContext),
     ),
     listOf(
       // optimizing

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt
@@ -64,10 +64,10 @@ class UnusedVarPass(private val uniqueWarningLogger: Logger) : ProcedurePass {
       Sets.union(builder.getVars(), builder.parent.getVars().map { it.wrappedVar }.toSet())
     val varsAndParams = Sets.union(allVars, builder.getParams().map { it.first }.toSet())
     if (!varsAndParams.containsAll(usedVars)) {
-      uniqueWarningLogger.write(
+      uniqueWarningLogger.writeln(
         Logger.Level.INFO,
         "WARNING: There are some used variables not present as declarations: " +
-          "${usedVars.filter { it !in varsAndParams }}\n",
+          usedVars.filter { it !in varsAndParams },
       )
     }