From 5f44e655ee60fb246be7a17f9d3f0a1410a188b8 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Jul 2024 14:33:39 +0200 Subject: [PATCH 01/18] Remove redundant MonolithicTransFunc interface, adjust converter classes to MonolithicExpr --- .../cfa/analysis/CfaToMonoliticTransFunc.java | 70 ------------------ .../theta/cfa/analysis/CfaToMonoliticExpr.kt | 52 +++++++++++++ .../AbstractMonolithicTransFunc.java | 53 ------------- .../algorithm/bounded/BoundedChecker.kt | 6 +- .../algorithm/bounded/MonolithicExpr.kt | 4 +- .../sts/analysis/StsToMonoliticTransFunc.java | 45 ----------- .../theta/sts/analysis/StsToMonoliticExpr.kt} | 22 ++---- .../analysis/XcfaMonolithicTransFunc.java | 74 ------------------- .../xcfa/analysis/XcfaToMonolithicExpr.kt | 65 ++++++++++++++++ .../cli/checkers/ConfigToBoundedChecker.kt | 5 +- .../analysis/XstsToMonoliticTransFunc.java | 56 -------------- .../src/main/kotlin/XstsToMonolithicExpr.kt | 35 +++++++++ 12 files changed, 164 insertions(+), 323 deletions(-) delete mode 100644 subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticTransFunc.java create mode 100644 subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt delete mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/AbstractMonolithicTransFunc.java delete mode 100644 subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/StsToMonoliticTransFunc.java rename subprojects/{common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java => sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt} (56%) delete mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt delete mode 100644 subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java create mode 100644 subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticTransFunc.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticTransFunc.java deleted file mode 100644 index 7992eb7cfb..0000000000 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticTransFunc.java +++ /dev/null @@ -1,70 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.cfa.analysis; - -import com.google.common.base.Preconditions; -import hu.bme.mit.theta.analysis.algorithm.AbstractMonolithicTransFunc; -import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc; -import hu.bme.mit.theta.cfa.CFA; -import hu.bme.mit.theta.core.decl.Decls; -import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.stmt.AssumeStmt; -import hu.bme.mit.theta.core.stmt.NonDetStmt; -import hu.bme.mit.theta.core.stmt.SequenceStmt; -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.utils.StmtUtils; -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; - -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.stream.Collectors; - -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neq; - -public class CfaToMonoliticTransFunc extends AbstractMonolithicTransFunc { - private CfaToMonoliticTransFunc(CFA cfa) { - Preconditions.checkArgument(cfa.getErrorLoc().isPresent()); - - int i = 0; - final Map map = new HashMap<>(); - for (var x : cfa.getLocs()) { - map.put(x, i++); - } - var locVar = Decls.Var("loc", Int()); - List tranList = cfa.getEdges().stream().map(e -> SequenceStmt.of(List.of( - AssumeStmt.of(Eq(locVar.getRef(), Int(map.get(e.getSource())))), - e.getStmt(), - AssignStmt.of(locVar, Int(map.get(e.getTarget()))) - ))).collect(Collectors.toList()); - var trans = NonDetStmt.of(tranList); - var transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); - transExpr = And(transUnfold.getExprs()); - initExpr = Eq(locVar.getRef(), Int(map.get(cfa.getInitLoc()))); - propExpr = Neq(locVar.getRef(), Int(map.get(cfa.getErrorLoc().get()))); - - firstIndex = VarIndexingFactory.indexing(0); - offsetIndex = transUnfold.getIndexing(); - } - - public static MonolithicTransFunc create(CFA cfa) { - return new CfaToMonoliticTransFunc(cfa); - } -} diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt new file mode 100644 index 0000000000..d0ed3318f7 --- /dev/null +++ b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt @@ -0,0 +1,52 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.cfa.analysis; + +import com.google.common.base.Preconditions; +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.core.decl.Decls; +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.booltype.BoolExprs.And +import hu.bme.mit.theta.core.type.inttype.IntExprs.* +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; + +fun CFA.toMonolithicExpr(): MonolithicExpr { + Preconditions.checkArgument(this.errorLoc.isPresent); + + val map = mutableMapOf() + for ((i, x) in this.locs.withIndex()) { + map[x] = i; + } + val locVar = Decls.Var("loc", Int()) + val tranList = this.edges.map{e -> SequenceStmt.of(listOf( + AssumeStmt.of(Eq(locVar.ref, Int(map[e.source]!!))), + e.stmt, + AssignStmt.of(locVar, Int(map[e.target]!!)) + ))}.toList() + val trans = NonDetStmt.of(tranList); + val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); + val transExpr = And(transUnfold.exprs) + val initExpr = Eq(locVar.ref, Int(map[this.initLoc]!!)) + val propExpr = Neq(locVar.ref, Int(map[this.errorLoc.orElseThrow()]!!)) + + val offsetIndex = transUnfold.indexing + + return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex) + } + diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/AbstractMonolithicTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/AbstractMonolithicTransFunc.java deleted file mode 100644 index dd3fc19264..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/AbstractMonolithicTransFunc.java +++ /dev/null @@ -1,53 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.analysis.algorithm; - -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; - -public abstract class AbstractMonolithicTransFunc implements MonolithicTransFunc { - protected Expr transExpr; - protected Expr initExpr; - protected VarIndexing firstIndex; - protected VarIndexing offsetIndex; - protected Expr propExpr; - - @Override - public Expr getTransExpr() { - return transExpr; - } - - @Override - public Expr getInitExpr() { - return initExpr; - } - - @Override - public Expr getPropExpr() { - return propExpr; - } - - @Override - public VarIndexing getInitIndexing() { - return firstIndex; - } - - @Override - public VarIndexing getOffsetIndexing() { - return offsetIndex; - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index a300cb72a6..7fdbe878c0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -74,9 +74,9 @@ class BoundedChecker @JvmOverloads constructor( ) : SafetyChecker, UnitPrec> { private val vars = monolithicExpr.vars() - private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, 0) + private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0)) private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) } - private val indices = mutableListOf(VarIndexingFactory.indexing(0)) + private val indices = mutableListOf(monolithicExpr.initOffsetIndex) private val exprs = mutableListOf>() private var kindLastIterLookup = 0 @@ -98,7 +98,7 @@ class BoundedChecker @JvmOverloads constructor( exprs.add(PathUtils.unfold(monolithicExpr.transExpr, indices.last())) - indices.add(indices.last().add(monolithicExpr.offsetIndex)) + indices.add(indices.last().add(monolithicExpr.transOffsetIndex)) if (isBmcEnabled) { bmc()?.let { return it } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt index 766b21af6c..65df7dfb65 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt @@ -21,12 +21,14 @@ import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.utils.ExprUtils.getVars import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory data class MonolithicExpr( val initExpr: Expr, val transExpr: Expr, val propExpr: Expr, - val offsetIndex: VarIndexing + val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1), + val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0) ) { fun vars(): Collection> { diff --git a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/StsToMonoliticTransFunc.java b/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/StsToMonoliticTransFunc.java deleted file mode 100644 index 86515307c5..0000000000 --- a/subprojects/sts/sts-analysis/src/main/java/hu/bme/mit/theta/sts/analysis/StsToMonoliticTransFunc.java +++ /dev/null @@ -1,45 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.sts.analysis; - -import hu.bme.mit.theta.analysis.algorithm.AbstractMonolithicTransFunc; -import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc; -import hu.bme.mit.theta.analysis.expl.ExplState; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.sts.STS; - -import java.util.Collection; -import java.util.function.Function; - -public class StsToMonoliticTransFunc extends AbstractMonolithicTransFunc { - private StsToMonoliticTransFunc(STS sts) { - transExpr = sts.getTrans(); - initExpr = sts.getInit(); - propExpr = sts.getProp(); - firstIndex = VarIndexingFactory.indexing(0); - offsetIndex = VarIndexingFactory.indexing(1); - } - - public static MonolithicTransFunc create(STS sts) { - return new StsToMonoliticTransFunc(sts); - } -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt similarity index 56% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java rename to subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt index 883058e1d2..76bab7c228 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFunc.java +++ b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt @@ -13,24 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm; -import com.google.errorprone.annotations.Var; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; -import hu.bme.mit.theta.solver.SolverFactory; - -public interface MonolithicTransFunc { - Expr getTransExpr(); - - Expr getInitExpr(); - - Expr getPropExpr(); - - VarIndexing getInitIndexing(); - - VarIndexing getOffsetIndexing(); +package hu.bme.mit.theta.sts.analysis +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.sts.STS +fun STS.toMonoliticExpr(): MonolithicExpr{ + return MonolithicExpr(this.init, this.trans, this.prop) } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java deleted file mode 100644 index 47e98b7a5b..0000000000 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java +++ /dev/null @@ -1,74 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xcfa.analysis; - -import com.google.common.base.Preconditions; -import hu.bme.mit.theta.analysis.algorithm.AbstractMonolithicTransFunc; -import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc; -import hu.bme.mit.theta.core.decl.Decls; -import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.stmt.AssumeStmt; -import hu.bme.mit.theta.core.stmt.NonDetStmt; -import hu.bme.mit.theta.core.stmt.SequenceStmt; -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.utils.StmtUtils; -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; -import hu.bme.mit.theta.xcfa.UtilsKt; -import hu.bme.mit.theta.xcfa.model.StmtLabel; -import hu.bme.mit.theta.xcfa.model.XCFA; -import hu.bme.mit.theta.xcfa.model.XcfaLocation; - -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.stream.Collectors; - -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neq; - -public class XcfaMonolithicTransFunc extends AbstractMonolithicTransFunc { - private XcfaMonolithicTransFunc(XCFA xcfa) { - Preconditions.checkArgument(xcfa.getInitProcedures().size() == 1); - var proc = xcfa.getInitProcedures().stream().findFirst().orElse(null).getFirst(); - assert proc != null; - Preconditions.checkArgument(proc.getEdges().stream().map(UtilsKt::getFlatLabels).noneMatch(it -> it.stream().anyMatch(i -> !(i instanceof StmtLabel)))); - Preconditions.checkArgument(proc.getErrorLoc().isPresent()); - int i = 0; - final Map map = new HashMap<>(); - for (var x : proc.getLocs()) { - map.put(x, i++); - } - var locVar = Decls.Var("__loc_", Int()); - List tranList = proc.getEdges().stream().map(e -> SequenceStmt.of(List.of( - AssumeStmt.of(Eq(locVar.getRef(), Int(map.get(e.getSource())))), - e.getLabel().toStmt(), - AssignStmt.of(locVar, Int(map.get(e.getTarget()))) - ))).collect(Collectors.toList()); - final var trans = NonDetStmt.of(tranList); - var transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); - transExpr = And(transUnfold.getExprs()); - initExpr = Eq(locVar.getRef(), Int(map.get(proc.getInitLoc()))); - firstIndex = VarIndexingFactory.indexing(0); - offsetIndex = transUnfold.getIndexing(); - propExpr = Neq(locVar.getRef(), Int(map.get(proc.getErrorLoc().get()))); - } - - public static MonolithicTransFunc create(XCFA xcfa) { - return new XcfaMonolithicTransFunc(xcfa); - } -} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt new file mode 100644 index 0000000000..e152fd9f0d --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt @@ -0,0 +1,65 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xcfa.analysis; + +import com.google.common.base.Preconditions; +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.core.decl.Decls; +import hu.bme.mit.theta.core.stmt.AssignStmt; +import hu.bme.mit.theta.core.stmt.AssumeStmt; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; +import hu.bme.mit.theta.core.type.booltype.BoolExprs.And +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntExprs.Eq +import hu.bme.mit.theta.core.type.inttype.IntExprs.Neq +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.xcfa.getFlatLabels +import hu.bme.mit.theta.xcfa.model.StmtLabel; +import hu.bme.mit.theta.xcfa.model.XCFA; +import hu.bme.mit.theta.xcfa.model.XcfaEdge +import hu.bme.mit.theta.xcfa.model.XcfaLocation; + +fun XCFA.toMonolithicExpr(): MonolithicExpr { + Preconditions.checkArgument(this.initProcedures.size == 1) + val proc = this.initProcedures.stream().findFirst().orElse(null).first + Preconditions.checkArgument(proc.edges.map { it.getFlatLabels() }.flatten().none { it !is StmtLabel }) + Preconditions.checkArgument(proc.errorLoc.isPresent) + + val map = mutableMapOf() + for ((i, x) in proc.locs.withIndex()) { + map[x] = i; + } + val locVar = Decls.Var("__loc_", IntExprs.Int()) + val tranList = proc.edges.map { (source, target, label): XcfaEdge -> + SequenceStmt.of(listOf( + AssumeStmt.of(Eq(locVar.ref, IntExprs.Int(map[source]!!))), + label.toStmt(), + AssignStmt.of(locVar, + IntExprs.Int(map[target]!!)) + )) + }.toList() + val trans = NonDetStmt.of(tranList) + val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)) + + return MonolithicExpr( + initExpr = Eq(locVar.ref, IntExprs.Int(map[proc.initLoc]!!)), + transExpr = And(transUnfold.exprs), + propExpr = Neq(locVar.ref, IntExprs.Int(map[proc.errorLoc.get()]!!)), + transOffsetIndex = transUnfold.indexing + ) +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 52194fa0aa..c0f92495dd 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -20,7 +20,6 @@ import com.google.common.base.Preconditions import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.EmptyWitness import hu.bme.mit.theta.analysis.algorithm.SafetyChecker -import hu.bme.mit.theta.analysis.algorithm.arg.ARG import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.analysis.ptr.PtrState @@ -35,8 +34,6 @@ import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.solver.SolverFactory -import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstaller -import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.analysis.XcfaState @@ -111,6 +108,6 @@ private fun getMonolithicExpr(xcfa: XCFA): MonolithicExpr { initExpr = Eq(locVar.ref, IntExprs.Int(map[proc.initLoc]!!)), transExpr = And(transUnfold.exprs), propExpr = Neq(locVar.ref, IntExprs.Int(map[proc.errorLoc.get()]!!)), - offsetIndex = transUnfold.indexing + transOffsetIndex = transUnfold.indexing ) } \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java deleted file mode 100644 index 98e175e869..0000000000 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java +++ /dev/null @@ -1,56 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xsts.analysis; - -import hu.bme.mit.theta.analysis.algorithm.AbstractMonolithicTransFunc; -import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc; -import hu.bme.mit.theta.analysis.expl.ExplState; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.stmt.Stmts; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.StmtUnfoldResult; -import hu.bme.mit.theta.core.utils.StmtUtils; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.xsts.XSTS; - -import java.util.Collection; -import java.util.List; -import java.util.Set; -import java.util.function.Function; - -import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; - -public class XstsToMonoliticTransFunc extends AbstractMonolithicTransFunc { - private XstsToMonoliticTransFunc(XSTS xsts) { - final StmtUnfoldResult initUnfoldResult = StmtUtils.toExpr(xsts.getInit(), VarIndexingFactory.indexing(0)); - initExpr = And(And(initUnfoldResult.getExprs()), xsts.getInitFormula()); - firstIndex = initUnfoldResult.getIndexing(); - final var envTran = Stmts.SequenceStmt(List.of(xsts.getEnv(), xsts.getTran())); - final StmtUnfoldResult envTranUnfoldResult = StmtUtils.toExpr(envTran, VarIndexingFactory.indexing(0)); - transExpr = And(envTranUnfoldResult.getExprs()); - offsetIndex = envTranUnfoldResult.getIndexing(); - propExpr = xsts.getProp(); - - } - - public static MonolithicTransFunc create(XSTS xsts) { - return new XstsToMonoliticTransFunc(xsts); - } -} diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt new file mode 100644 index 0000000000..247ccba3a6 --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt @@ -0,0 +1,35 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.core.stmt.Stmts; +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And +import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import hu.bme.mit.theta.xsts.XSTS; +fun XSTS.toMonolithicExpr(): MonolithicExpr { + + val initUnfoldResult = StmtUtils.toExpr(this.init, VarIndexingFactory.indexing(0)) + val initExpr = And(And(initUnfoldResult.exprs), this.initFormula) + val initOffsetIndex = initUnfoldResult.indexing + val envTran = Stmts.SequenceStmt(listOf(this.env, this.tran)) + val envTranUnfoldResult = StmtUtils.toExpr(envTran, VarIndexingFactory.indexing(0)); + val transExpr = And(envTranUnfoldResult.exprs); + val transOffsetIndex = envTranUnfoldResult.indexing; + val propExpr = this.prop + + return MonolithicExpr(initExpr, transExpr, propExpr, transOffsetIndex, initOffsetIndex) +} From ddb92f99afd961021ee93374519d0459172aca34 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Jul 2024 14:35:31 +0200 Subject: [PATCH 02/18] Fixed typos in filenames --- .../analysis/{CfaToMonoliticExpr.kt => CfaToMonolithicExpr.kt} | 0 .../analysis/{StsToMonoliticExpr.kt => StsToMonolithicExpr.kt} | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/{CfaToMonoliticExpr.kt => CfaToMonolithicExpr.kt} (100%) rename subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/{StsToMonoliticExpr.kt => StsToMonolithicExpr.kt} (95%) diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt similarity index 100% rename from subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonoliticExpr.kt rename to subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt diff --git a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt similarity index 95% rename from subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt rename to subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt index 76bab7c228..e6ab5afa0d 100644 --- a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonoliticExpr.kt +++ b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt @@ -19,6 +19,6 @@ package hu.bme.mit.theta.sts.analysis import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.sts.STS -fun STS.toMonoliticExpr(): MonolithicExpr{ +fun STS.toMonolithicExpr(): MonolithicExpr{ return MonolithicExpr(this.init, this.trans, this.prop) } From 80d508abe4c315a3cbeefb81ba9bf9f3d3e9d48d Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Jul 2024 14:37:18 +0200 Subject: [PATCH 03/18] Remove unused file --- .../algorithm/MonolithicTransFuncStub.java | 73 ------------------- 1 file changed, 73 deletions(-) delete mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFuncStub.java diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFuncStub.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFuncStub.java deleted file mode 100644 index a7a41a4be5..0000000000 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/MonolithicTransFuncStub.java +++ /dev/null @@ -1,73 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.analysis.algorithm; - -import hu.bme.mit.theta.core.stmt.Stmt; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.StmtUtils; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; - -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; - -public final class MonolithicTransFuncStub implements MonolithicTransFunc { - private final Expr transExpr; - private final Expr initExpr; - private final Expr propExpr; - private final VarIndexing initIndexing; - private final VarIndexing offsetIndexing; - - public MonolithicTransFuncStub( - Stmt transStmt, - Expr initExpr, - Expr propExpr - ) { - var result = StmtUtils.toExpr(transStmt, VarIndexingFactory.indexing(0)); - this.transExpr = And(result.getExprs()); - this.initExpr = initExpr; - this.propExpr = propExpr; - this.initIndexing = VarIndexingFactory.indexing(0); - this.offsetIndexing = result.getIndexing(); - } - - @Override - public Expr getTransExpr() { - return transExpr; - } - - @Override - public Expr getInitExpr() { - return initExpr; - } - - @Override - public Expr getPropExpr() { - return propExpr; - } - - @Override - public VarIndexing getInitIndexing() { - return initIndexing; - } - - @Override - public VarIndexing getOffsetIndexing() { - return offsetIndexing; - } - -} From 67c289167cfb958c506dd7f5383f05789f1079d1 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Jul 2024 14:45:39 +0200 Subject: [PATCH 04/18] Reformat code --- .../bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt | 8 +++++--- .../bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt | 2 +- .../mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt | 10 +++++----- .../src/main/kotlin/XstsToMonolithicExpr.kt | 1 + 4 files changed, 12 insertions(+), 9 deletions(-) diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt index d0ed3318f7..2783a8585d 100644 --- a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt +++ b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt @@ -34,11 +34,13 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { map[x] = i; } val locVar = Decls.Var("loc", Int()) - val tranList = this.edges.map{e -> SequenceStmt.of(listOf( + val tranList = this.edges.map { e -> + SequenceStmt.of(listOf( AssumeStmt.of(Eq(locVar.ref, Int(map[e.source]!!))), e.stmt, AssignStmt.of(locVar, Int(map[e.target]!!)) - ))}.toList() + )) + }.toList() val trans = NonDetStmt.of(tranList); val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); val transExpr = And(transUnfold.exprs) @@ -48,5 +50,5 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { val offsetIndex = transUnfold.indexing return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex) - } +} diff --git a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt index e6ab5afa0d..a452ecb065 100644 --- a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt +++ b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt @@ -19,6 +19,6 @@ package hu.bme.mit.theta.sts.analysis import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.sts.STS -fun STS.toMonolithicExpr(): MonolithicExpr{ +fun STS.toMonolithicExpr(): MonolithicExpr { return MonolithicExpr(this.init, this.trans, this.prop) } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt index e152fd9f0d..050b421bdb 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt @@ -46,11 +46,11 @@ fun XCFA.toMonolithicExpr(): MonolithicExpr { } val locVar = Decls.Var("__loc_", IntExprs.Int()) val tranList = proc.edges.map { (source, target, label): XcfaEdge -> - SequenceStmt.of(listOf( - AssumeStmt.of(Eq(locVar.ref, IntExprs.Int(map[source]!!))), - label.toStmt(), - AssignStmt.of(locVar, - IntExprs.Int(map[target]!!)) + SequenceStmt.of(listOf( + AssumeStmt.of(Eq(locVar.ref, IntExprs.Int(map[source]!!))), + label.toStmt(), + AssignStmt.of(locVar, + IntExprs.Int(map[target]!!)) )) }.toList() val trans = NonDetStmt.of(tranList) diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt index 247ccba3a6..fbc9a65c39 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt @@ -20,6 +20,7 @@ import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.xsts.XSTS; + fun XSTS.toMonolithicExpr(): MonolithicExpr { val initUnfoldResult = StmtUtils.toExpr(this.init, VarIndexingFactory.indexing(0)) From 3735869bc3d42f2fa149a3b6565e384b1aa1eaf6 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Jul 2024 14:46:45 +0200 Subject: [PATCH 05/18] Move xcfa to monolithic conversion to match other formalisms --- .../cli/checkers/ConfigToBoundedChecker.kt | 48 +------------------ 1 file changed, 2 insertions(+), 46 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index c0f92495dd..309920680d 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -16,38 +16,24 @@ package hu.bme.mit.theta.xcfa.cli.checkers -import com.google.common.base.Preconditions import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.EmptyWitness import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker -import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.common.logging.Logger -import hu.bme.mit.theta.core.decl.Decls -import hu.bme.mit.theta.core.stmt.* -import hu.bme.mit.theta.core.type.booltype.BoolExprs.And -import hu.bme.mit.theta.core.type.inttype.IntExprs -import hu.bme.mit.theta.core.type.inttype.IntExprs.Eq -import hu.bme.mit.theta.core.type.inttype.IntExprs.Neq -import hu.bme.mit.theta.core.utils.StmtUtils -import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.analysis.XcfaState +import hu.bme.mit.theta.xcfa.analysis.toMonolithicExpr import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.cli.utils.getSolver import hu.bme.mit.theta.xcfa.cli.utils.valToAction import hu.bme.mit.theta.xcfa.cli.utils.valToState -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.model.StmtLabel import hu.bme.mit.theta.xcfa.model.XCFA -import hu.bme.mit.theta.xcfa.model.XcfaEdge -import hu.bme.mit.theta.xcfa.model.XcfaLocation -import java.util.stream.Collectors fun getBoundedChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, @@ -56,7 +42,7 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, val boundedConfig = config.backendConfig.specConfig as BoundedConfig return BoundedChecker( - monolithicExpr = getMonolithicExpr(xcfa), + monolithicExpr = xcfa.toMonolithicExpr(), bmcSolver = tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver)?.createSolver(), bmcEnabled = { !boundedConfig.bmcConfig.disable }, @@ -80,34 +66,4 @@ private fun tryGetSolver(name: String, validate: Boolean): SolverFactory? { } catch (e: Throwable) { return null } -} - -private fun getMonolithicExpr(xcfa: XCFA): MonolithicExpr { - Preconditions.checkArgument(xcfa.initProcedures.size == 1) - val proc = xcfa.initProcedures.stream().findFirst().orElse(null).first - Preconditions.checkArgument(proc.edges.map { it.getFlatLabels() }.flatten().none { it !is StmtLabel }) - Preconditions.checkArgument(proc.errorLoc.isPresent) - var i = 0 - val map: MutableMap = HashMap() - for (x in proc.locs) { - map[x] = i++ - } - val locVar = Decls.Var("__loc_", IntExprs.Int()) - val tranList = proc.edges.stream().map { (source, target, label): XcfaEdge -> - SequenceStmt.of(java.util.List.of( - AssumeStmt.of(IntExprs.Eq(locVar.ref, IntExprs.Int(map[source]!!))), - label.toStmt(), - AssignStmt.of(locVar, - IntExprs.Int(map[target]!!)) - )) - }.collect(Collectors.toList()) - val trans = NonDetStmt.of(tranList as List) - val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)) - - return MonolithicExpr( - initExpr = Eq(locVar.ref, IntExprs.Int(map[proc.initLoc]!!)), - transExpr = And(transUnfold.exprs), - propExpr = Neq(locVar.ref, IntExprs.Int(map[proc.errorLoc.get()]!!)), - transOffsetIndex = transUnfold.indexing - ) } \ No newline at end of file From f1f449212392c2d5ab6e73429a0ffdbdeee65f50 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 15:43:39 +0200 Subject: [PATCH 06/18] Enable Kind and IMC based on the solvers provided --- .../mit/theta/analysis/algorithm/bounded/BoundedChecker.kt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 7fdbe878c0..cb88d4e6b7 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -62,12 +62,12 @@ class BoundedChecker @JvmOverloads constructor( private val monolithicExpr: MonolithicExpr, private val shouldGiveUp: (Int) -> Boolean = { false }, private val bmcSolver: Solver? = null, - private val bmcEnabled: () -> Boolean = { true }, + private val bmcEnabled: () -> Boolean = { bmcSolver != null }, private val lfPathOnly: () -> Boolean = { true }, private val itpSolver: ItpSolver? = null, - private val imcEnabled: (Int) -> Boolean = { true }, + private val imcEnabled: (Int) -> Boolean = { itpSolver != null }, private val indSolver: Solver? = null, - private val kindEnabled: (Int) -> Boolean = { true }, + private val kindEnabled: (Int) -> Boolean = { indSolver != null }, private val valToState: (Valuation) -> S, private val biValToAction: (Valuation, Valuation) -> A, private val logger: Logger, From ae9acb6f9a05637200878e4c59ccb2530c4bd724 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 15:43:58 +0200 Subject: [PATCH 07/18] Add valToState and biValToAction for CFA --- .../theta/cfa/analysis/CfaToMonolithicExpr.kt | 36 ++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt index 2783a8585d..ca6c125314 100644 --- a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt +++ b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt @@ -18,13 +18,19 @@ package hu.bme.mit.theta.cfa.analysis; import com.google.common.base.Preconditions; import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.core.decl.Decls; +import hu.bme.mit.theta.core.model.ImmutableValuation +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.* import hu.bme.mit.theta.core.type.booltype.BoolExprs.And import hu.bme.mit.theta.core.type.inttype.IntExprs.* +import hu.bme.mit.theta.core.type.inttype.IntLitExpr import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; +import java.util.* fun CFA.toMonolithicExpr(): MonolithicExpr { Preconditions.checkArgument(this.errorLoc.isPresent); @@ -33,7 +39,7 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { for ((i, x) in this.locs.withIndex()) { map[x] = i; } - val locVar = Decls.Var("loc", Int()) + val locVar = Decls.Var("__loc__", Int()) val tranList = this.edges.map { e -> SequenceStmt.of(listOf( AssumeStmt.of(Eq(locVar.ref, Int(map[e.source]!!))), @@ -52,3 +58,31 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex) } +fun CFA.valToAction(val1: Valuation, val2: Valuation): CfaAction { + val val1Map = val1.toMap() + val val2Map = val2.toMap() + var i = 0 + val map: MutableMap = mutableMapOf() + for (x in this.locs) { + map[x] = i++ + } + return CfaAction.create( + this.edges.first { edge -> + map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() && + map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() + }) +} + +fun CFA.valToState(val1: Valuation): CfaState { + val valMap = val1.toMap() + var i = 0 + val map: MutableMap = mutableMapOf() + for (x in this.locs) { + map[i++] = x + } + return CfaState.of( + map[(valMap[valMap.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()], + ExplState.of(val1) + ) +} + From d724dfac41ef1f53a0b402e4654afba7fa4cf5ac Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 15:44:17 +0200 Subject: [PATCH 08/18] Add cli bindings for bmc,kind,imc --- .../cfa/analysis/config/CfaConfigBuilder.java | 1 + .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 72 +++++++++++++++++-- 2 files changed, 67 insertions(+), 6 deletions(-) diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index 932f6fe932..7427f38b20 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -145,6 +145,7 @@ public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { public enum Algorithm { CEGAR, + BMC, KINDUCTION, IMC } diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index bb5a27107d..57001fe9c4 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -22,12 +22,17 @@ import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker; +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.CfaToMonolithicExprKt; import hu.bme.mit.theta.cfa.analysis.CfaTraceConcretizer; import hu.bme.mit.theta.cfa.analysis.config.CfaConfig; import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; @@ -233,14 +238,17 @@ private void run() { refinementSolverFactory = SolverManager.resolveSolverFactory(solver); } - final SafetyResult, ? extends Trace> status; + final SafetyResult> status; if (algorithm == Algorithm.CEGAR) { final CfaConfig configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory); status = check(configuration); - sw.stop(); + } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { + final BoundedChecker checker = buildBoundedChecker(cfa, abstractionSolverFactory); + status = checker.check(null); } else { throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); } + sw.stop(); printResult(status, sw.elapsed(TimeUnit.MILLISECONDS)); if (status.isUnsafe() && cexfile != null) { @@ -282,6 +290,52 @@ private CFA loadModel() throws Exception { } } + private BoundedChecker buildBoundedChecker(final CFA cfa, final SolverFactory abstractionSolverFactory) { + final MonolithicExpr monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa); + final BoundedChecker checker; + switch (algorithm) { + case BMC -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger + ); + case KINDUCTION -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + () -> true, + () -> true, + null, + (i) -> false, + abstractionSolverFactory.createSolver(), + (i) -> true, + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger + ); + case IMC -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + () -> true, + () -> true, + abstractionSolverFactory.createItpSolver(), + (i) -> true, + null, + (i) -> false, + val -> CfaToMonolithicExprKt.valToState(cfa, val), + (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), + logger + ); + default -> + throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + } + return checker; + } + private SafetyResult, ? extends Trace> check(CfaConfig configuration) throws Exception { try { return configuration.check(); @@ -293,7 +347,7 @@ private CFA loadModel() throws Exception { } } - private void printResult(final SafetyResult, ? extends Trace> status, final long totalTimeMs) { + private void printResult(final SafetyResult> status, final long totalTimeMs) { final CegarStatistics stats = (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); if (benchmarkMode) { @@ -303,9 +357,15 @@ private void printResult(final SafetyResult, ? extends Trace writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - writer.cell(status.getWitness().size()); - writer.cell(status.getWitness().getDepth()); - writer.cell(status.getWitness().getMeanBranchingFactor()); + if (status.getWitness() instanceof ARG arg) { + writer.cell(arg.size()); + writer.cell(arg.getDepth()); + writer.cell(arg.getMeanBranchingFactor()); + } else { + writer.cell(""); + writer.cell(""); + writer.cell(""); + } if (status.isUnsafe()) { writer.cell(status.asUnsafe().getCex().length() + ""); } else { From ddf4452840b37401c9a7afe18a0470be450f6a11 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 15:58:26 +0200 Subject: [PATCH 09/18] Add valToState and biValToAction for XSTS --- .../src/main/kotlin/XstsToMonolithicExpr.kt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt index fbc9a65c39..b9b7fe3bd5 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt @@ -15,11 +15,15 @@ */ import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.Stmts; import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState fun XSTS.toMonolithicExpr(): MonolithicExpr { @@ -34,3 +38,17 @@ fun XSTS.toMonolithicExpr(): MonolithicExpr { return MonolithicExpr(initExpr, transExpr, propExpr, transOffsetIndex, initOffsetIndex) } + +fun XSTS.valToAction(val1: Valuation, val2: Valuation): XstsAction { + return XstsAction.create( + Stmts.SequenceStmt(listOf(this.env, this.tran)) + ) +} + +fun XSTS.valToState(val1: Valuation): XstsState { + return XstsState.of( + ExplState.of(val1), + false, + true + ) +} \ No newline at end of file From 5caab293a907516dcaf9e54a71d081e60e331557 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 16:11:21 +0200 Subject: [PATCH 10/18] Add sts boundedchecker cli binding --- .../theta/sts/analysis/StsToMonolithicExpr.kt | 10 +++ .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 70 +++++++++++++++++-- 2 files changed, 75 insertions(+), 5 deletions(-) diff --git a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt index a452ecb065..19c7bd5189 100644 --- a/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt +++ b/subprojects/sts/sts-analysis/src/main/kotlin/hu/bme/mit/theta/sts/analysis/StsToMonolithicExpr.kt @@ -17,8 +17,18 @@ package hu.bme.mit.theta.sts.analysis import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.sts.STS fun STS.toMonolithicExpr(): MonolithicExpr { return MonolithicExpr(this.init, this.trans, this.prop) } + +fun STS.valToAction(val1: Valuation, val2: Valuation): StsAction { + return StsAction(this); +} + +fun STS.valToState(val1: Valuation): ExplState { + return ExplState.of(val1); +} diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index dabdb04b79..86b44a43f1 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -22,6 +22,8 @@ import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker; +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; @@ -36,6 +38,7 @@ import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import hu.bme.mit.theta.sts.STS; import hu.bme.mit.theta.sts.StsUtils; @@ -44,6 +47,7 @@ import hu.bme.mit.theta.sts.aiger.elements.AigerSystem; import hu.bme.mit.theta.sts.aiger.utils.AigerCoi; import hu.bme.mit.theta.sts.analysis.StsAction; +import hu.bme.mit.theta.sts.analysis.StsToMonolithicExprKt; import hu.bme.mit.theta.sts.analysis.StsTraceConcretizer; import hu.bme.mit.theta.sts.analysis.config.StsConfig; import hu.bme.mit.theta.sts.analysis.config.StsConfigBuilder; @@ -75,6 +79,7 @@ public class StsCli { enum Algorithm { CEGAR, + BMC, KINDUCTION, IMC } @@ -159,10 +164,13 @@ private void run() { final Stopwatch sw = Stopwatch.createStarted(); final STS sts = loadModel(); - SafetyResult, ? extends Trace> status = null; + SafetyResult> status = null; if (algorithm.equals(Algorithm.CEGAR)) { final StsConfig configuration = buildConfiguration(sts); status = check(configuration); + } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { + final BoundedChecker checker = buildBoundedChecker(sts, Z3LegacySolverFactory.getInstance()); + status = checker.check(null); } else { throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); } @@ -226,7 +234,53 @@ private STS loadModel() throws Exception { } } - private void printResult(final SafetyResult, ? extends Trace> status, final STS sts, + private BoundedChecker buildBoundedChecker(final STS sts, final SolverFactory abstractionSolverFactory) { + final MonolithicExpr monolithicExpr = StsToMonolithicExprKt.toMonolithicExpr(sts); + final BoundedChecker checker; + switch (algorithm) { + case BMC -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger + ); + case KINDUCTION -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + () -> true, + () -> true, + null, + (i) -> false, + abstractionSolverFactory.createSolver(), + (i) -> true, + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger + ); + case IMC -> checker = new BoundedChecker<>( + monolithicExpr, + (i) -> false, + abstractionSolverFactory.createSolver(), + () -> true, + () -> true, + abstractionSolverFactory.createItpSolver(), + (i) -> true, + null, + (i) -> false, + val -> StsToMonolithicExprKt.valToState(sts, val), + (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), + logger + ); + default -> + throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + } + return checker; + } + + private void printResult(final SafetyResult> status, final STS sts, final long totalTimeMs) { final CegarStatistics stats = (CegarStatistics) status.getStats().get(); if (benchmarkMode) { @@ -236,9 +290,15 @@ private void printResult(final SafetyResult, ? extends Trace writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - writer.cell(status.getWitness().size()); - writer.cell(status.getWitness().getDepth()); - writer.cell(status.getWitness().getMeanBranchingFactor()); + if(status.getWitness() instanceof ARG arg) { + writer.cell(arg.size()); + writer.cell(arg.getDepth()); + writer.cell(arg.getMeanBranchingFactor()); + } else { + writer.cell(""); + writer.cell(""); + writer.cell(""); + } if (status.isUnsafe()) { writer.cell(status.asUnsafe().getCex().length() + ""); } else { From 687755fe28a3a38060ed15e2a02048c1002b0545 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 17:05:54 +0200 Subject: [PATCH 11/18] Move XstsToMonolithicExpr.kt --- .../{ => hu/bme/mit/theta/xsts/analysis}/XstsToMonolithicExpr.kt | 1 + 1 file changed, 1 insertion(+) rename subprojects/xsts/xsts-analysis/src/main/kotlin/{ => hu/bme/mit/theta/xsts/analysis}/XstsToMonolithicExpr.kt (96%) diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt similarity index 96% rename from subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt rename to subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt index b9b7fe3bd5..a72c8f79c7 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/XstsToMonolithicExpr.kt @@ -13,6 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ +package hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr import hu.bme.mit.theta.analysis.expl.ExplState From 1d4ab249048009c592a7318ac223f59aa620ec83 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 17:06:11 +0200 Subject: [PATCH 12/18] Add BoundedCheckerBuilder.kt --- .../bounded/BoundedCheckerBuilder.kt | 107 ++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt new file mode 100644 index 0000000000..7ca7a89934 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -0,0 +1,107 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm.bounded + +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.solver.ItpSolver +import hu.bme.mit.theta.solver.Solver + +@JvmOverloads +fun buildBMC( + monolithicExpr: MonolithicExpr, + bmcSolver: Solver, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> A, + logger: Logger, + shouldGiveUp: (Int) -> Boolean = { false }, + bmcEnabled: () -> Boolean = { true }, + lfPathOnly: () -> Boolean = { true }, +): BoundedChecker { + return BoundedChecker( + monolithicExpr, + shouldGiveUp, + bmcSolver, + bmcEnabled, + lfPathOnly, + null, + { false }, + null, + { false }, + valToState, + biValToAction, + logger + ) +} +@JvmOverloads +fun buildKIND( + monolithicExpr: MonolithicExpr, + bmcSolver: Solver, + indSolver: Solver, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> A, + logger: Logger, + shouldGiveUp: (Int) -> Boolean = { false }, + bmcEnabled: () -> Boolean = { true }, + lfPathOnly: () -> Boolean = { true }, + kindEnabled: (Int) -> Boolean = { true }, +): BoundedChecker { + return BoundedChecker( + monolithicExpr, + shouldGiveUp, + bmcSolver, + bmcEnabled, + lfPathOnly, + null, + { false }, + indSolver, + kindEnabled, + valToState, + biValToAction, + logger + ) +} +@JvmOverloads +fun buildIMC( + monolithicExpr: MonolithicExpr, + bmcSolver: Solver, + itpSolver: ItpSolver, + valToState: (Valuation) -> S, + biValToAction: (Valuation, Valuation) -> A, + logger: Logger, + shouldGiveUp: (Int) -> Boolean = { false }, + bmcEnabled: () -> Boolean = { true }, + lfPathOnly: () -> Boolean = { true }, + imcEnabled: (Int) -> Boolean = { true }, +): BoundedChecker { + return BoundedChecker( + monolithicExpr, + shouldGiveUp, + bmcSolver, + bmcEnabled, + lfPathOnly, + itpSolver, + imcEnabled, + null, + { false }, + valToState, + biValToAction, + logger + ) +} \ No newline at end of file From 71fe85e97df5b40671be2d401563d8192e42e758 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 17:06:28 +0200 Subject: [PATCH 13/18] Make cfa-analysis a kotlin project --- subprojects/sts/sts-analysis/build.gradle.kts | 1 + 1 file changed, 1 insertion(+) diff --git a/subprojects/sts/sts-analysis/build.gradle.kts b/subprojects/sts/sts-analysis/build.gradle.kts index de8d888b56..fbb1cbfcc7 100644 --- a/subprojects/sts/sts-analysis/build.gradle.kts +++ b/subprojects/sts/sts-analysis/build.gradle.kts @@ -15,6 +15,7 @@ */ plugins { id("java-common") + id("kotlin-common") } dependencies { From e61b29741afc091bd25f7c060f2a84cd48b20951 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 17:07:15 +0200 Subject: [PATCH 14/18] Add cli bindings for xsts, use bounded builder in all formalisms --- .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 20 +---- .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 20 +---- .../xcfa/analysis/XcfaToMonolithicExpr.kt | 47 ++++++++++ .../cli/checkers/ConfigToBoundedChecker.kt | 11 +-- .../analysis/config/XstsConfigBuilder.java | 2 + .../hu/bme/mit/theta/xsts/cli/XstsCli.java | 85 +++++++++++++++---- 6 files changed, 128 insertions(+), 57 deletions(-) diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 57001fe9c4..024911743e 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -23,6 +23,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedCheckerBuilderKt; import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expl.ExplState; @@ -294,38 +295,25 @@ private CFA loadModel() throws Exception { final MonolithicExpr monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa); final BoundedChecker checker; switch (algorithm) { - case BMC -> checker = new BoundedChecker<>( + case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), val -> CfaToMonolithicExprKt.valToState(cfa, val), (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), logger ); - case KINDUCTION -> checker = new BoundedChecker<>( + case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), - () -> true, - () -> true, - null, - (i) -> false, abstractionSolverFactory.createSolver(), - (i) -> true, val -> CfaToMonolithicExprKt.valToState(cfa, val), (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), logger ); - case IMC -> checker = new BoundedChecker<>( + case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), - () -> true, - () -> true, abstractionSolverFactory.createItpSolver(), - (i) -> true, - null, - (i) -> false, val -> CfaToMonolithicExprKt.valToState(cfa, val), (val1, val2) -> CfaToMonolithicExprKt.valToAction(cfa, val1, val2), logger diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 86b44a43f1..0a04b06bd7 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -23,6 +23,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedCheckerBuilderKt; import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expr.ExprState; @@ -238,38 +239,25 @@ private STS loadModel() throws Exception { final MonolithicExpr monolithicExpr = StsToMonolithicExprKt.toMonolithicExpr(sts); final BoundedChecker checker; switch (algorithm) { - case BMC -> checker = new BoundedChecker<>( + case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), val -> StsToMonolithicExprKt.valToState(sts, val), (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), logger ); - case KINDUCTION -> checker = new BoundedChecker<>( + case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), - () -> true, - () -> true, - null, - (i) -> false, abstractionSolverFactory.createSolver(), - (i) -> true, val -> StsToMonolithicExprKt.valToState(sts, val), (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), logger ); - case IMC -> checker = new BoundedChecker<>( + case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( monolithicExpr, - (i) -> false, abstractionSolverFactory.createSolver(), - () -> true, - () -> true, abstractionSolverFactory.createItpSolver(), - (i) -> true, - null, - (i) -> false, val -> StsToMonolithicExprKt.valToState(sts, val), (val1, val2) -> StsToMonolithicExprKt.valToAction(sts, val1, val2), logger diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt index 050b421bdb..d91174ed82 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt @@ -17,7 +17,11 @@ package hu.bme.mit.theta.xcfa.analysis; import com.google.common.base.Preconditions; import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.core.decl.Decls; +import hu.bme.mit.theta.core.model.ImmutableValuation +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.AssignStmt; import hu.bme.mit.theta.core.stmt.AssumeStmt; import hu.bme.mit.theta.core.stmt.NonDetStmt; @@ -26,6 +30,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.And import hu.bme.mit.theta.core.type.inttype.IntExprs import hu.bme.mit.theta.core.type.inttype.IntExprs.Eq import hu.bme.mit.theta.core.type.inttype.IntExprs.Neq +import hu.bme.mit.theta.core.type.inttype.IntLitExpr import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.xcfa.getFlatLabels @@ -33,6 +38,7 @@ import hu.bme.mit.theta.xcfa.model.StmtLabel; import hu.bme.mit.theta.xcfa.model.XCFA; import hu.bme.mit.theta.xcfa.model.XcfaEdge import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import java.util.* fun XCFA.toMonolithicExpr(): MonolithicExpr { Preconditions.checkArgument(this.initProcedures.size == 1) @@ -63,3 +69,44 @@ fun XCFA.toMonolithicExpr(): MonolithicExpr { transOffsetIndex = transUnfold.indexing ) } + +fun XCFA.valToAction(val1: Valuation, val2: Valuation): XcfaAction { + val val1Map = val1.toMap() + val val2Map = val2.toMap() + var i = 0 + val map: MutableMap = HashMap() + for (x in this.procedures.first { it.name == "main" }.locs) { + map[x] = i++ + } + return XcfaAction( + pid = 0, + edge = this.procedures.first { it.name == "main" }.edges.first { edge -> + map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() && + map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() + }) +} + +fun XCFA.valToState(val1: Valuation): XcfaState> { + val valMap = val1.toMap() + var i = 0 + val map: MutableMap = HashMap() + for (x in this.procedures.first { it.name == "main" }.locs) { + map[i++] = x + } + return XcfaState( + xcfa = this, + processes = mapOf(Pair(0, XcfaProcessState( + locs = LinkedList( + listOf(map[(valMap[valMap.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()])), + varLookup = LinkedList(), + ))), + 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()))), + mutexes = emptyMap(), + threadLookup = emptyMap(), + bottom = false + ) +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index 309920680d..18e0bd82ca 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -24,15 +24,10 @@ import hu.bme.mit.theta.analysis.ptr.PtrState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM import hu.bme.mit.theta.solver.SolverFactory -import hu.bme.mit.theta.xcfa.analysis.XcfaAction -import hu.bme.mit.theta.xcfa.analysis.XcfaPrec -import hu.bme.mit.theta.xcfa.analysis.XcfaState -import hu.bme.mit.theta.xcfa.analysis.toMonolithicExpr +import hu.bme.mit.theta.xcfa.analysis.* import hu.bme.mit.theta.xcfa.cli.params.BoundedConfig import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig import hu.bme.mit.theta.xcfa.cli.utils.getSolver -import hu.bme.mit.theta.xcfa.cli.utils.valToAction -import hu.bme.mit.theta.xcfa.cli.utils.valToState import hu.bme.mit.theta.xcfa.model.XCFA fun getBoundedChecker(xcfa: XCFA, mcm: MCM, @@ -53,8 +48,8 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, indSolver = tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver)?.createSolver(), kindEnabled = { !boundedConfig.indConfig.disable }, - valToState = { valToState(xcfa, it) }, - biValToAction = { val1, val2 -> valToAction(xcfa, val1, val2) }, + valToState = { xcfa.valToState(it) }, + biValToAction = { val1, val2 -> xcfa.valToAction(val1, val2) }, logger = logger ) as SafetyChecker>, XcfaAction>, XcfaPrec<*>> diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index af4b9e7b51..d84d0deee2 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -77,6 +77,8 @@ public class XstsConfigBuilder { public enum Algorithm { CEGAR, + + BMC, KINDUCTION, IMC, MDD diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 1dfb8e356e..33eaea0fff 100644 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -22,7 +22,6 @@ import com.google.common.base.Stopwatch; import com.koloboke.collect.set.hash.HashObjSets; import hu.bme.mit.delta.collections.IntObjCursor; -import hu.bme.mit.delta.collections.impl.RecursiveIntObjMapViews; import hu.bme.mit.delta.java.mdd.*; import hu.bme.mit.delta.mdd.LatticeDefinition; import hu.bme.mit.delta.mdd.MddInterpreter; @@ -32,6 +31,9 @@ import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.arg.ARG; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker; +import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedCheckerBuilderKt; +import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics; import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex; @@ -82,6 +84,7 @@ import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.PredSplit; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.Refinement; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.Search; +import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.XstsToMonolithicExprKt; import hu.bme.mit.theta.xsts.analysis.mdd.XstsMddChecker; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; import hu.bme.mit.theta.frontend.petrinet.xsts.PetriNetToXSTS; @@ -260,7 +263,7 @@ private void run() { try { if (algorithm == Algorithm.CEGAR) { - runCegarAnalysis(); + runCegarOrBoundedAnalysis(); } else if (algorithm == Algorithm.MDD) { if (model.endsWith(".pnml")) { runPetrinetMddAnalysis(); @@ -277,7 +280,7 @@ private void run() { } } - private void runCegarAnalysis() throws Exception { + private void runCegarOrBoundedAnalysis() throws Exception { final Stopwatch sw = Stopwatch.createStarted(); final XSTS xsts = loadXSTSModel(); @@ -287,15 +290,28 @@ private void runCegarAnalysis() throws Exception { return; } - final XstsConfig configuration = buildConfiguration(xsts); - final SafetyResult, ? extends Trace> status = check(configuration); + registerAllSolverManagers(solverHome, logger); + final SolverFactory abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver); + final SolverFactory refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver); + + final SafetyResult> status; + if (algorithm == Algorithm.CEGAR) { + final XstsConfig configuration = buildConfiguration(xsts, abstractionSolverFactory, refinementSolverFactory); + status = check(configuration); + } else if (algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { + final BoundedChecker checker = buildBoundedChecker(xsts, abstractionSolverFactory); + status = checker.check(null); + } else { + throw new UnsupportedOperationException("Algorithm not supported: " + algorithm); + } + sw.stop(); - printCegarResult(status, xsts, sw.elapsed(TimeUnit.MILLISECONDS)); + printCegarOrBoundedResult(status, xsts, sw.elapsed(TimeUnit.MILLISECONDS)); if (status.isUnsafe() && cexfile != null) { writeCex(status.asUnsafe(), xsts); } - if (dotfile != null) { - writeVisualStatus(status, dotfile); + if (dotfile != null && algorithm == Algorithm.CEGAR) { + writeVisualStatus((SafetyResult, ? extends Trace>) status, dotfile); } } @@ -559,7 +575,7 @@ private List loadOrdering(final List petriNets) throws Exceptio return ordering; } - private XstsConfig buildConfiguration(final XSTS xsts) throws Exception { + private XstsConfig buildConfiguration(final XSTS xsts, final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) throws Exception { // set up stopping analysis if it is stuck on same ARGs and precisions //if (noStuckCheck) { //ArgCexCheckHandler.instance.setArgCexCheck(false, false); @@ -567,10 +583,6 @@ private List loadOrdering(final List petriNets) throws Exceptio //ArgCexCheckHandler.instance.setArgCexCheck(true, refinement.equals(Refinement.MULTI_SEQ)); // } - registerAllSolverManagers(solverHome, logger); - SolverFactory abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver); - SolverFactory refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver); - try { return new XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory) .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) @@ -580,7 +592,40 @@ private List loadOrdering(final List petriNets) throws Exceptio } } - private void printCegarResult(final SafetyResult, ? extends Trace> status, final XSTS sts, final long totalTimeMs) { + private BoundedChecker buildBoundedChecker(final XSTS xsts, final SolverFactory abstractionSolverFactory) { + final MonolithicExpr monolithicExpr = XstsToMonolithicExprKt.toMonolithicExpr(xsts); + final BoundedChecker checker; + switch (algorithm) { + case BMC -> checker = BoundedCheckerBuilderKt.buildBMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + val -> XstsToMonolithicExprKt.valToState(xsts, val), + (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), + logger + ); + case KINDUCTION -> checker = BoundedCheckerBuilderKt.buildKIND( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createSolver(), + val -> XstsToMonolithicExprKt.valToState(xsts, val), + (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), + logger + ); + case IMC -> checker = BoundedCheckerBuilderKt.buildIMC( + monolithicExpr, + abstractionSolverFactory.createSolver(), + abstractionSolverFactory.createItpSolver(), + val -> XstsToMonolithicExprKt.valToState(xsts, val), + (val1, val2) -> XstsToMonolithicExprKt.valToAction(xsts, val1, val2), + logger + ); + default -> + throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + } + return checker; + } + + private void printCegarOrBoundedResult(final SafetyResult> status, final XSTS sts, final long totalTimeMs) { final CegarStatistics stats = (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); if (benchmarkMode) { @@ -590,9 +635,15 @@ private void printCegarResult(final SafetyResult, ? extends writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - writer.cell(status.getWitness().size()); - writer.cell(status.getWitness().getDepth()); - writer.cell(status.getWitness().getMeanBranchingFactor()); + if (status.getWitness() instanceof ARG arg) { + writer.cell(arg.size()); + writer.cell(arg.getDepth()); + writer.cell(arg.getMeanBranchingFactor()); + } else { + writer.cell(""); + writer.cell(""); + writer.cell(""); + } if (status.isUnsafe()) { writer.cell(status.asUnsafe().getCex().length() + ""); } else { From 805793f50d4aadfc242eccacfe9ebf84bbde20ed Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 17:07:25 +0200 Subject: [PATCH 15/18] Remove moved functions --- .../mit/theta/xcfa/cli/utils/BMCValToTrace.kt | 71 ------------------- 1 file changed, 71 deletions(-) delete mode 100644 subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt deleted file mode 100644 index 7a04fcb462..0000000000 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt +++ /dev/null @@ -1,71 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.xcfa.cli.utils - -import hu.bme.mit.theta.analysis.expl.ExplState -import hu.bme.mit.theta.analysis.ptr.PtrState -import hu.bme.mit.theta.core.decl.Decls.Var -import hu.bme.mit.theta.core.model.ImmutableValuation -import hu.bme.mit.theta.core.model.Valuation -import hu.bme.mit.theta.core.type.inttype.IntLitExpr -import hu.bme.mit.theta.xcfa.analysis.XcfaAction -import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState -import hu.bme.mit.theta.xcfa.analysis.XcfaState -import hu.bme.mit.theta.xcfa.model.XCFA -import hu.bme.mit.theta.xcfa.model.XcfaLocation -import java.util.* - -fun valToAction(xcfa: XCFA, val1: Valuation, val2: Valuation): XcfaAction { - val val1Map = val1.toMap() - val val2Map = val2.toMap() - var i = 0 - val map: MutableMap = HashMap() - for (x in xcfa.procedures.first { it.name == "main" }.locs) { - map[x] = i++ - } - return XcfaAction( - pid = 0, - edge = xcfa.procedures.first { it.name == "main" }.edges.first { edge -> - map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() && - map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() - }) -} - -fun valToState(xcfa: XCFA, val1: Valuation): XcfaState> { - val valMap = val1.toMap() - var i = 0 - val map: MutableMap = HashMap() - for (x in xcfa.procedures.first { it.name == "main" }.locs) { - map[i++] = x - } - return XcfaState( - xcfa = xcfa, - processes = mapOf(Pair(0, XcfaProcessState( - locs = LinkedList( - listOf(map[(valMap[valMap.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()])), - varLookup = LinkedList(), - ))), - PtrState(ExplState.of( - ImmutableValuation.from( - val1.toMap() - .filter { it.key.name != "__loc_" && !it.key.name.startsWith("__temp_") } - .map { Pair(Var("_" + "_" + it.key.name, it.key.type), it.value) }.toMap()))), - mutexes = emptyMap(), - threadLookup = emptyMap(), - bottom = false - ) -} \ No newline at end of file From efe51937307c7f600bb3e44e2cc150430cd3ff8b Mon Sep 17 00:00:00 2001 From: mondokm Date: Wed, 31 Jul 2024 11:55:49 +0200 Subject: [PATCH 16/18] Fix bugs in sts,xsts bounded cli bindings --- .../sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java | 2 +- .../src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 0a04b06bd7..d817270f99 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -270,7 +270,7 @@ private STS loadModel() throws Exception { private void printResult(final SafetyResult> status, final STS sts, final long totalTimeMs) { - final CegarStatistics stats = (CegarStatistics) status.getStats().get(); + final CegarStatistics stats = (CegarStatistics) status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); if (benchmarkMode) { writer.cell(status.isSafe()); writer.cell(totalTimeMs); diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 33eaea0fff..e123b6e81c 100644 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -262,7 +262,7 @@ private void run() { try { - if (algorithm == Algorithm.CEGAR) { + if (algorithm == Algorithm.CEGAR || algorithm == Algorithm.BMC || algorithm == Algorithm.KINDUCTION || algorithm == Algorithm.IMC) { runCegarOrBoundedAnalysis(); } else if (algorithm == Algorithm.MDD) { if (model.endsWith(".pnml")) { From a927f6a49baa137e299449498335ad92b6f10d30 Mon Sep 17 00:00:00 2001 From: mondokm Date: Wed, 31 Jul 2024 11:56:52 +0200 Subject: [PATCH 17/18] Reformat files --- .../bounded/BoundedCheckerBuilder.kt | 50 +++---------------- .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 2 +- 2 files changed, 9 insertions(+), 43 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt index 7ca7a89934..bfd1aeadf9 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedCheckerBuilder.kt @@ -34,21 +34,10 @@ fun buildBMC( bmcEnabled: () -> Boolean = { true }, lfPathOnly: () -> Boolean = { true }, ): BoundedChecker { - return BoundedChecker( - monolithicExpr, - shouldGiveUp, - bmcSolver, - bmcEnabled, - lfPathOnly, - null, - { false }, - null, - { false }, - valToState, - biValToAction, - logger - ) + return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, null, + { false }, valToState, biValToAction, logger) } + @JvmOverloads fun buildKIND( monolithicExpr: MonolithicExpr, @@ -62,21 +51,10 @@ fun buildKIND( lfPathOnly: () -> Boolean = { true }, kindEnabled: (Int) -> Boolean = { true }, ): BoundedChecker { - return BoundedChecker( - monolithicExpr, - shouldGiveUp, - bmcSolver, - bmcEnabled, - lfPathOnly, - null, - { false }, - indSolver, - kindEnabled, - valToState, - biValToAction, - logger - ) + return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, null, { false }, indSolver, + kindEnabled, valToState, biValToAction, logger) } + @JvmOverloads fun buildIMC( monolithicExpr: MonolithicExpr, @@ -90,18 +68,6 @@ fun buildIMC( lfPathOnly: () -> Boolean = { true }, imcEnabled: (Int) -> Boolean = { true }, ): BoundedChecker { - return BoundedChecker( - monolithicExpr, - shouldGiveUp, - bmcSolver, - bmcEnabled, - lfPathOnly, - itpSolver, - imcEnabled, - null, - { false }, - valToState, - biValToAction, - logger - ) + return BoundedChecker(monolithicExpr, shouldGiveUp, bmcSolver, bmcEnabled, lfPathOnly, itpSolver, imcEnabled, null, + { false }, valToState, biValToAction, logger) } \ No newline at end of file diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index d817270f99..ddb48470eb 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -278,7 +278,7 @@ private void printResult(final SafetyResult> status, fi writer.cell(stats.getAbstractorTimeMs()); writer.cell(stats.getRefinerTimeMs()); writer.cell(stats.getIterations()); - if(status.getWitness() instanceof ARG arg) { + if (status.getWitness() instanceof ARG arg) { writer.cell(arg.size()); writer.cell(arg.getDepth()); writer.cell(arg.getMeanBranchingFactor()); From e407b7ba9ff244fdadae9b1609ed96603703ee13 Mon Sep 17 00:00:00 2001 From: mondokm Date: Wed, 31 Jul 2024 13:30:40 +0200 Subject: [PATCH 18/18] Resolve rebase conflict --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 8bf1134ca8..1a556276e8 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.2.3" + version = "6.3.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) }