From ff0e778fd8cbd0f5d3202163c3997b7b06c95338 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 21 Oct 2024 19:45:27 +0200 Subject: [PATCH 1/5] Fixed variable naming --- build.gradle.kts | 2 +- .../mit/theta/xcfa/passes/ReferenceElimination.kt | 14 ++++++-------- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index 108baa86d1..0640cf3cbc 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.6.1" + version = "6.6.2" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index b216917361..083bbf7a49 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -94,15 +94,13 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { return builder } - if (builder.parent.getInitProcedures().any { it.first == builder }) { // we only need this for main - val initLabels = referredVars.values.map { it.second } - val initEdges = builder.initLoc.outgoingEdges - val newInitEdges = initEdges.map { - it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) - } - initEdges.forEach(builder::removeEdge) - newInitEdges.forEach(builder::addEdge) + val initLabels = referredVars.values.map { it.second } + val initEdges = builder.initLoc.outgoingEdges + val newInitEdges = initEdges.map { + it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) } + initEdges.forEach(builder::removeEdge) + newInitEdges.forEach(builder::addEdge) val edges = LinkedHashSet(builder.getEdges()) for (edge in edges) { From ed814a6e0afe701ac57306908b8d83c2ed046d74 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Mon, 21 Oct 2024 18:02:10 +0000 Subject: [PATCH 2/5] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 4316bed633..b76fd9f7ff 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.6.2" + version = "6.6.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From 5d8b8414e162557257979c87ded6112cd1f996c4 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 22 Oct 2024 19:16:31 +0200 Subject: [PATCH 3/5] Moved to dynamic pointer base --- .../theta/xcfa/passes/ReferenceElimination.kt | 364 +++++++++++------- 1 file changed, 231 insertions(+), 133 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index 87f2c9ab3a..51705676df 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -13,15 +13,16 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - 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.* +import hu.bme.mit.theta.core.stmt.Stmts.Assign import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add import hu.bme.mit.theta.core.type.anytype.Dereference import hu.bme.mit.theta.core.type.anytype.Exprs.Dereference import hu.bme.mit.theta.core.type.anytype.RefExpr @@ -33,160 +34,257 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPo import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.references +import org.abego.treelayout.internal.util.Contract -/** - * Removes all references in favor of creating arrays instead. - */ - +/** Removes all references in favor of creating arrays instead. */ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { - companion object { + companion object { - private var cnt = 2 // counts upwards, uses 3k+2 - get() = field.also { field += 3 } - } + private var cnt = 2 // counts upwards, uses 3k+2 + get() = field.also { field += 3 } + } - override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { - val globalReferredVars = builder.parent.metaData.computeIfAbsent("references") { - builder.parent.getProcedures().flatMap { - it.getEdges() - .flatMap { it.label.getFlatLabels().flatMap { it.references } } - } - .map { (it.expr as RefExpr<*>).decl as VarDecl<*> }.toSet() - .filter { builder.parent.getVars().any { global -> global.wrappedVar == it } } - .associateWith { - val ptrType = CPointer(null, CComplexType.getType(it.ref, parseContext), parseContext) - val varDecl = Var(it.name + "*", ptrType.smtType) - val lit = CComplexType.getType(varDecl.ref, parseContext).getValue("$cnt") - builder.parent.addVar(XcfaGlobalVar(varDecl, lit)) - parseContext.metadata.create(varDecl.ref, "cType", ptrType) - val assign = StmtLabel(AssignStmt.of(cast(varDecl, varDecl.type), - cast(lit, varDecl.type))) - Pair(varDecl, assign) + private val XcfaBuilder.pointer: VarDecl<*> by lazy { + Var("__sp", CPointer(null, null, parseContext).smtType) + } + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + val globalReferredVars = + builder.parent.metaData.computeIfAbsent("references") { + builder.parent + .getProcedures() + .flatMap { it.getEdges().flatMap { it.label.getFlatLabels().flatMap { it.references } } } + .map { (it.expr as RefExpr<*>).decl as VarDecl<*> } + .toSet() + .filter { builder.parent.getVars().any { global -> global.wrappedVar == it } } + .associateWith { + val ptrType = CPointer(null, CComplexType.getType(it.ref, parseContext), parseContext) + val varDecl = Var(it.name + "*", ptrType.smtType) + val lit = CComplexType.getType(varDecl.ref, parseContext).getValue("$cnt") + builder.parent.addVar(XcfaGlobalVar(varDecl, lit)) + parseContext.metadata.create(varDecl.ref, "cType", ptrType) + val assign = + StmtLabel(AssignStmt.of(cast(varDecl, varDecl.type), cast(lit, varDecl.type))) + Pair(varDecl, SequenceLabel(listOf(assign))) + } + } + checkState(globalReferredVars is Map<*, *>, "ReferenceElimination needs info on references") + globalReferredVars as Map, Pair, SequenceLabel>> + + val referredVars = + builder + .getEdges() + .flatMap { it.label.getFlatLabels().flatMap { it.references } } + .map { (it.expr as RefExpr<*>).decl as VarDecl<*> } + .toSet() + .filter { !globalReferredVars.containsKey(it) } + .associateWith { + val ptrType = CPointer(null, CComplexType.getType(it.ref, parseContext), parseContext) + + val ptrVar = builder.parent.pointer + if (builder.parent.getVars().none { it.wrappedVar == ptrVar }) { // initial creation + val initVal = ptrType.getValue("$cnt") + builder.parent.addVar(XcfaGlobalVar(ptrVar, initVal)) + val initProc = builder.parent.getInitProcedures().map { it.first } + Contract.checkState(initProc.size == 1, "Multiple start procedure are not handled well") + initProc.forEach { + val initAssign = + StmtLabel(Assign(cast(ptrVar, ptrVar.type), cast(initVal, ptrVar.type))) + val newEdges = + it.initLoc.outgoingEdges.map { + it.withLabel( + SequenceLabel(listOf(initAssign) + it.label.getFlatLabels(), it.label.metadata) + ) } + it.initLoc.outgoingEdges.forEach(it::removeEdge) + newEdges.forEach(it::addEdge) + } + } + val assign1 = + StmtLabel( + AssignStmt.of( + cast(ptrVar, ptrType.smtType), + cast(Add(ptrVar.ref, ptrType.getValue("3")), ptrType.smtType), + ) + ) + val varDecl = Var(it.name + "*", ptrType.smtType) + builder.addVar(varDecl) + parseContext.metadata.create(varDecl.ref, "cType", ptrType) + val assign2 = + StmtLabel(AssignStmt.of(cast(varDecl, varDecl.type), cast(ptrVar.ref, varDecl.type))) + Pair(varDecl, SequenceLabel(listOf(assign1, assign2))) } - checkState(globalReferredVars is Map<*, *>, "ReferenceElimination needs info on references") - globalReferredVars as Map, Pair, StmtLabel>> - - val referredVars = builder.getEdges() - .flatMap { it.label.getFlatLabels().flatMap { it.references } } - .map { (it.expr as RefExpr<*>).decl as VarDecl<*> }.toSet() - .filter { !globalReferredVars.containsKey(it) } - .associateWith { - val ptrType = CPointer(null, CComplexType.getType(it.ref, parseContext), parseContext) - val varDecl = Var(it.name + "*", ptrType.smtType) - builder.addVar(varDecl) - parseContext.metadata.create(varDecl.ref, "cType", ptrType) - val assign = StmtLabel(AssignStmt.of(cast(varDecl, varDecl.type), - cast(CComplexType.getType(varDecl.ref, parseContext).getValue("$cnt"), varDecl.type))) - Pair(varDecl, assign) - } + globalReferredVars - - if (referredVars.isEmpty()) { - return builder + if ( + globalReferredVars.isNotEmpty() && + builder.parent.getInitProcedures().any { it.first == builder } + ) { // we only need this for main + val initLabels = globalReferredVars.values.flatMap { it.second.labels } + val initEdges = builder.initLoc.outgoingEdges + val newInitEdges = + initEdges.map { + it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) } + initEdges.forEach(builder::removeEdge) + newInitEdges.forEach(builder::addEdge) + } - val initLabels = referredVars.values.map { it.second } - val initEdges = builder.initLoc.outgoingEdges - val newInitEdges = initEdges.map { - it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) + if (referredVars.isNotEmpty()) { + val initLabels = referredVars.values.flatMap { it.second.labels } + val initEdges = builder.initLoc.outgoingEdges + val newInitEdges = + initEdges.map { + it.withLabel(SequenceLabel(initLabels + it.label.getFlatLabels(), it.label.metadata)) } - initEdges.forEach(builder::removeEdge) - newInitEdges.forEach(builder::addEdge) + initEdges.forEach(builder::removeEdge) + newInitEdges.forEach(builder::addEdge) - val edges = LinkedHashSet(builder.getEdges()) - for (edge in edges) { - builder.removeEdge(edge) - builder.addEdge(edge.withLabel(edge.label.changeReferredVars(referredVars, parseContext))) - } + val edges = LinkedHashSet(builder.getEdges()) + val allReferredVars = referredVars + globalReferredVars + for (edge in edges) { + builder.removeEdge(edge) + builder.addEdge( + edge.withLabel(edge.label.changeReferredVars(allReferredVars, parseContext)) + ) + } - return DeterministicPass().run(NormalizePass().run(builder)) + return DeterministicPass().run(NormalizePass().run(builder)) } - @JvmOverloads - fun XcfaLabel.changeReferredVars(varLut: Map, Pair, StmtLabel>>, - parseContext: ParseContext? = null): XcfaLabel = - if (varLut.isNotEmpty()) - when (this) { - is InvokeLabel -> InvokeLabel(name, params.map { it.changeReferredVars(varLut, parseContext) }, - metadata = metadata) + return builder + } - is NondetLabel -> NondetLabel(labels.map { it.changeReferredVars(varLut, parseContext) }.toSet(), - metadata = metadata) + @JvmOverloads + fun XcfaLabel.changeReferredVars( + varLut: Map, Pair, SequenceLabel>>, + parseContext: ParseContext? = null, + ): XcfaLabel = + if (varLut.isNotEmpty()) + when (this) { + is InvokeLabel -> + InvokeLabel( + name, + params.map { it.changeReferredVars(varLut, parseContext) }, + metadata = metadata, + ) - is SequenceLabel -> SequenceLabel(labels.map { it.changeReferredVars(varLut, parseContext) }, - metadata = metadata) + is NondetLabel -> + NondetLabel( + labels.map { it.changeReferredVars(varLut, parseContext) }.toSet(), + metadata = metadata, + ) - is StartLabel -> StartLabel(name, params.map { it.changeReferredVars(varLut, parseContext) }, - pidVar, metadata = metadata) + is SequenceLabel -> + SequenceLabel( + labels.map { it.changeReferredVars(varLut, parseContext) }, + metadata = metadata, + ) - is StmtLabel -> SequenceLabel(stmt.changeReferredVars(varLut, parseContext).map { - StmtLabel(it, metadata = metadata, - choiceType = this.choiceType) - }).let { if (it.labels.size == 1) it.labels[0] else it } + is StartLabel -> + StartLabel( + name, + params.map { it.changeReferredVars(varLut, parseContext) }, + pidVar, + metadata = metadata, + ) - else -> this - } - else this - - @JvmOverloads - fun Stmt.changeReferredVars(varLut: Map, Pair, StmtLabel>>, - parseContext: ParseContext? = null): List { - val stmts = when (this) { - is AssignStmt<*> -> if (this.varDecl in varLut.keys) { - val newVar = varLut[this.varDecl]!!.first - listOf( - MemoryAssignStmt.create( - Dereference( - cast(newVar.ref, newVar.type), - cast(CComplexType.getSignedLong(parseContext).nullValue, newVar.type), - this.expr.type), - this.expr.changeReferredVars(varLut, parseContext))) - } else { - listOf(AssignStmt.of(cast(this.varDecl, this.varDecl.type), - cast(this.expr.changeReferredVars(varLut, parseContext), this.varDecl.type))) - } + is StmtLabel -> + SequenceLabel( + stmt.changeReferredVars(varLut, parseContext).map { + StmtLabel(it, metadata = metadata, choiceType = this.choiceType) + } + ) + .let { if (it.labels.size == 1) it.labels[0] else it } - is MemoryAssignStmt<*, *, *> -> listOf( - MemoryAssignStmt.create(deref.changeReferredVars(varLut, parseContext) as Dereference<*, *, *>, - expr.changeReferredVars(varLut, parseContext))) + else -> this + } + else this - is AssumeStmt -> listOf(AssumeStmt.of(cond.changeReferredVars(varLut, parseContext))) - is SequenceStmt -> listOf( - SequenceStmt.of(this.stmts.flatMap { it.changeReferredVars(varLut, parseContext) })) + @JvmOverloads + fun Stmt.changeReferredVars( + varLut: Map, Pair, XcfaLabel>>, + parseContext: ParseContext? = null, + ): List { + val stmts = + when (this) { + is AssignStmt<*> -> + if (this.varDecl in varLut.keys) { + val newVar = varLut[this.varDecl]!!.first + listOf( + MemoryAssignStmt.create( + Dereference( + cast(newVar.ref, newVar.type), + cast(CComplexType.getSignedLong(parseContext).nullValue, newVar.type), + this.expr.type, + ), + this.expr.changeReferredVars(varLut, parseContext), + ) + ) + } else { + listOf( + AssignStmt.of( + cast(this.varDecl, this.varDecl.type), + cast(this.expr.changeReferredVars(varLut, parseContext), this.varDecl.type), + ) + ) + } - is SkipStmt -> listOf(this) - else -> TODO("Not yet implemented ($this)") - } - val metadataValue = parseContext?.metadata?.getMetadataValue(this, "sourceStatement") - if (metadataValue?.isPresent == true) { - for (stmt in stmts) { - parseContext.metadata.create(stmt, "sourceStatement", metadataValue.get()) - } - } - return stmts - } + is MemoryAssignStmt<*, *, *> -> + listOf( + MemoryAssignStmt.create( + deref.changeReferredVars(varLut, parseContext) as Dereference<*, *, *>, + expr.changeReferredVars(varLut, parseContext), + ) + ) - @JvmOverloads - fun Expr.changeReferredVars(varLut: Map, Pair, StmtLabel>>, - parseContext: ParseContext? = null): Expr = - if (this is RefExpr) { - (decl as VarDecl).changeReferredVars(varLut) - } else if (this is Reference<*, *> && this.expr is RefExpr<*> && (this.expr as RefExpr<*>).decl in varLut.keys) { - varLut[(this.expr as RefExpr<*>).decl]?.first?.ref as Expr - } else { - val ret = this.withOps(this.ops.map { it.changeReferredVars(varLut, parseContext) }) - if (parseContext?.metadata?.getMetadataValue(this, "cType")?.isPresent == true) { - parseContext.metadata?.create(ret, "cType", CComplexType.getType(this, parseContext)) - } - ret - } + is AssumeStmt -> listOf(AssumeStmt.of(cond.changeReferredVars(varLut, parseContext))) + is SequenceStmt -> + listOf( + SequenceStmt.of(this.stmts.flatMap { it.changeReferredVars(varLut, parseContext) }) + ) - fun VarDecl.changeReferredVars( - varLut: Map, Pair, StmtLabel>>): Expr = - varLut[this]?.first?.let { - Dereference(cast(it.ref, it.type), cast(CComplexType.getSignedInt(parseContext).nullValue, it.type), - this.type) as Expr - } ?: this.ref + is SkipStmt -> listOf(this) + else -> TODO("Not yet implemented ($this)") + } + val metadataValue = parseContext?.metadata?.getMetadataValue(this, "sourceStatement") + if (metadataValue?.isPresent == true) { + for (stmt in stmts) { + parseContext.metadata.create(stmt, "sourceStatement", metadataValue.get()) + } + } + return stmts + } + + @JvmOverloads + fun Expr.changeReferredVars( + varLut: Map, Pair, XcfaLabel>>, + parseContext: ParseContext? = null, + ): Expr = + if (this is RefExpr) { + (decl as VarDecl).changeReferredVars(varLut) + } else if ( + this is Reference<*, *> && + this.expr is RefExpr<*> && + (this.expr as RefExpr<*>).decl in varLut.keys + ) { + varLut[(this.expr as RefExpr<*>).decl]?.first?.ref as Expr + } else { + val ret = this.withOps(this.ops.map { it.changeReferredVars(varLut, parseContext) }) + if (parseContext?.metadata?.getMetadataValue(this, "cType")?.isPresent == true) { + parseContext.metadata?.create(ret, "cType", CComplexType.getType(this, parseContext)) + } + ret + } -} \ No newline at end of file + fun VarDecl.changeReferredVars( + varLut: Map, Pair, XcfaLabel>> + ): Expr = + varLut[this]?.first?.let { + Dereference( + cast(it.ref, it.type), + cast(CComplexType.getSignedInt(parseContext).nullValue, it.type), + this.type, + ) + as Expr + } ?: this.ref +} From e40acc249e7e85d1f73213198f659e446adce5ab Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Sun, 3 Nov 2024 23:27:28 +0000 Subject: [PATCH 4/5] Version bump --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index e4cbd21501..e57f7daf01 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.6.5" + version = "6.6.6" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } From f699d1b40f17c0d287c128c9af2910b0b61685c8 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 4 Nov 2024 00:37:54 +0100 Subject: [PATCH 5/5] fixed imports --- .../main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 2 +- .../hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt | 2 +- .../java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt | 2 +- .../java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt | 3 +-- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 7c2ac51694..b4a1356e07 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -18,6 +18,7 @@ package hu.bme.mit.theta.c2xcfa import com.google.common.base.Preconditions +import com.google.common.base.Preconditions.checkState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.Decls import hu.bme.mit.theta.core.decl.VarDecl @@ -52,7 +53,6 @@ import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.passes.CPasses import java.math.BigInteger import java.util.stream.Collectors -import org.abego.treelayout.internal.util.Contract.checkState class FrontendXcfaBuilder( val parseContext: ParseContext, 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 a944126ace..90494c4979 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 @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xcfa.cli.checkers +import com.google.common.base.Preconditions.checkState import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.EmptyProof import hu.bme.mit.theta.analysis.algorithm.SafetyChecker @@ -33,7 +34,6 @@ 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.xcfa2chc.toCHC -import org.abego.treelayout.internal.util.Contract.checkState fun getHornChecker( xcfa: XCFA, 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 index 0ee0c65b9d..e655fbfd5d 100644 --- 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,6 +15,7 @@ */ 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 @@ -27,7 +28,6 @@ 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.* -import org.abego.treelayout.internal.util.Contract.checkState /** * Transforms mallocs into address assignments. Requires the ProcedureBuilder be `deterministic`. diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt index 51705676df..9b8cb78acc 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt @@ -34,7 +34,6 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPo import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.references -import org.abego.treelayout.internal.util.Contract /** Removes all references in favor of creating arrays instead. */ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { @@ -87,7 +86,7 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass { val initVal = ptrType.getValue("$cnt") builder.parent.addVar(XcfaGlobalVar(ptrVar, initVal)) val initProc = builder.parent.getInitProcedures().map { it.first } - Contract.checkState(initProc.size == 1, "Multiple start procedure are not handled well") + checkState(initProc.size == 1, "Multiple start procedure are not handled well") initProc.forEach { val initAssign = StmtLabel(Assign(cast(ptrVar, ptrVar.type), cast(initVal, ptrVar.type)))