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")) } 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 e06e7ce39f..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 @@ -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 @@ -34,161 +35,255 @@ import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.references -/** - * 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 } + 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) + } - 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) + 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) - 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 +}