From 35d5f6b9d6f65476b6147721818471c5d1db4d06 Mon Sep 17 00:00:00 2001 From: RipplB Date: Sat, 30 Mar 2024 16:52:17 +0100 Subject: [PATCH] Kotlinizing --- .../hu/bme/mit/theta/cfa/CFAVarChanger.kt | 3 +- .../analysis/multi/MultiStatePredicate.java | 34 +++++++++++++++++++ .../theta/analysis/multi/MultiOfTwoTest.kt | 5 +-- .../bme/mit/theta/core/utils/StmtUtils.java | 9 +++++ .../{StmtUtils.kt => VarChangerUtils.kt} | 6 ++++ .../mit/theta/xsts/utils/XSTSVarChanger.kt | 9 +++-- 6 files changed, 59 insertions(+), 7 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiStatePredicate.java rename subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/{StmtUtils.kt => VarChangerUtils.kt} (86%) diff --git a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt b/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt index 7f9c92b180..950f9a4d76 100644 --- a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt +++ b/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt @@ -21,8 +21,7 @@ import hu.bme.mit.theta.core.utils.changeVars fun CFA.copyWithReplacingVars(variableMapping: Map>): CFA { val builder = CFA.builder() - val locationMap: Map = mutableMapOf( - *(locs.map { Pair(it.name, builder.createLoc(it.name)) }.toTypedArray())) + val locationMap: Map = locs.associate { it.name to builder.createLoc(it.name) } builder.initLoc = locationMap[initLoc.name] if (errorLoc.isPresent) builder.errorLoc = locationMap[errorLoc.get().name] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiStatePredicate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiStatePredicate.java new file mode 100644 index 0000000000..d7ca8e6cea --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiStatePredicate.java @@ -0,0 +1,34 @@ +/* + * 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.multi; + +import hu.bme.mit.theta.analysis.State; + +import java.util.function.Predicate; + +public class MultiStatePredicate implements Predicate> { + + private final Predicate dataStatePredicate; + + public MultiStatePredicate(Predicate dataStatePredicate) { + this.dataStatePredicate = dataStatePredicate; + } + + @Override + public boolean test(MultiState multiState) { + return dataStatePredicate.test(multiState.getDataState()); + } +} diff --git a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt index 07e71c8309..a96e0d1b8d 100644 --- a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt +++ b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt @@ -95,7 +95,7 @@ class MultiOfTwoTest { FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> originalCfa = CfaDslManager.createCfa(inputStream) } - val cfa = originalCfa.copyWithReplacingVars(mapOf(*(variables.map { Pair(it.name, it) }.toTypedArray()))) + val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) val dataAnalysis = xstsExplBuilder.dataAnalysis val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) val cfaLts: CfaLts = CfaSbeLts.getInstance() @@ -126,7 +126,7 @@ class MultiOfTwoTest { { llts, cls, rlts, crs, dns -> StmtMultiLts.of(llts, cls, rlts, crs, dns) }) val prop = Not(xsts.prop) val dataPredicate = ExplStatePredicate(prop, solver) - val argBuilder = ArgBuilder.create(product.lts, product.analysis) { s -> dataPredicate.test(s.dataState) } + val argBuilder = ArgBuilder.create(product.lts, product.analysis, MultiStatePredicate(dataPredicate)) val abstractor = BasicAbstractor.builder(argBuilder).build() val traceChecker = ExprTraceSeqItpChecker.create(True(), prop, itpSolver) val precRefiner = @@ -168,6 +168,7 @@ class MultiOfTwoTest { FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> cfa = CfaDslManager.createCfa(inputStream) } + cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) val cfaLts: CfaLts = CfaSbeLts.getInstance() val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java index 992a704d96..4fd6c1d4f7 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java @@ -20,7 +20,10 @@ import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; +import java.util.Collection; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.Set; /** @@ -78,4 +81,10 @@ public static StmtUnfoldResult toExpr(final List stmts, return StmtToExprTransformer.toExpr(stmts, indexing); } + public static Stmt changeVars(final Stmt stmt, final Collection> varDecls) { + final Map> map = new HashMap<>(); + varDecls.forEach(varDecl -> map.put(varDecl.getName(), varDecl)); + return VarChangerUtilsKt.changeVars(stmt, map); + } + } diff --git a/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/StmtUtils.kt b/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt similarity index 86% rename from subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/StmtUtils.kt rename to subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt index f88475a214..c1b02d7c4e 100644 --- a/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/StmtUtils.kt +++ b/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt @@ -33,6 +33,12 @@ fun Stmt.changeVars(variableMapping: Map>): Stmt { is SequenceStmt -> SequenceStmt.of(stmts.map { it.changeVars(variableMapping) }) is SkipStmt -> this is NonDetStmt -> NonDetStmt.of(stmts.map { it.changeVars(variableMapping) }) + is LoopStmt -> LoopStmt.of(stmt.changeVars(variableMapping), loopVariable.changeVars(variableMapping), + from.changeVars(variableMapping), to.changeVars(variableMapping)) + + is IfStmt -> IfStmt.of(cond.changeVars(variableMapping), then.changeVars(variableMapping), + elze.changeVars(variableMapping)) + else -> TODO("Not yet implemented") } } diff --git a/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt b/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt index 61c76246de..6a80ea1d76 100644 --- a/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt +++ b/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt @@ -22,9 +22,12 @@ import hu.bme.mit.theta.core.utils.changeVars import hu.bme.mit.theta.xsts.XSTS fun XSTS.copyWithReplacingVars(variableMapping: Map>): XSTS { - val newVarToType = mutableMapOf(*(varToType.map { Pair(it.key, it.value) }.toTypedArray())) + val newVarToType = varToType.toMutableMap() variableMapping.forEach { (name, varDecl) -> newVarToType[varDecl] = varToType[vars.find { it.name == name }] } val matchingCtrlVarNames = ctrlVars.filter { variableMapping.containsKey(it.name) }.map { it.name } - val newCtrlVars = setOf(*(ctrlVars.filter { !variableMapping.containsKey(it.name) }.toTypedArray()), *(variableMapping.filter { it.key in matchingCtrlVarNames }.values.toTypedArray())) - return XSTS(newVarToType, newCtrlVars, init.changeVars(variableMapping) as NonDetStmt, tran.changeVars(variableMapping) as NonDetStmt, env.changeVars(variableMapping) as NonDetStmt, initFormula.changeVars(variableMapping), prop.changeVars(variableMapping)) + val newCtrlVars = ctrlVars.filter { it.name !in variableMapping } + .toSet() + variableMapping.filter { it.key in matchingCtrlVarNames }.values.toSet() + return XSTS(newVarToType, newCtrlVars, init.changeVars(variableMapping) as NonDetStmt, + tran.changeVars(variableMapping) as NonDetStmt, env.changeVars(variableMapping) as NonDetStmt, + initFormula.changeVars(variableMapping), prop.changeVars(variableMapping)) } \ No newline at end of file