From c6e45741ed7f79c769248759adafc3bf0a61417d Mon Sep 17 00:00:00 2001 From: RipplB Date: Fri, 21 Jun 2024 00:00:22 +0200 Subject: [PATCH] Add variable swapping algorithms Create extension functions for Xsts and CFA which create a copy of a model by replacing the variables in the parameter. --- subprojects/cfa/cfa/build.gradle.kts | 1 + .../hu/bme/mit/theta/cfa/CFAVarChanger.kt | 41 ++++++++++++ .../mit/theta/cfa/CFAVarChangerUnitTest.kt | 40 +++++++++++ subprojects/common/core/build.gradle.kts | 1 + .../bme/mit/theta/core/utils/StmtUtils.java | 8 +++ .../mit/theta/core/utils/VarChangerUtils.kt | 66 +++++++++++++++++++ subprojects/xsts/xsts/build.gradle.kts | 1 + .../mit/theta/xsts/utils/XSTSVarChanger.kt | 33 ++++++++++ .../xsts/utils/XSTSVarChangerUnitTest.kt | 56 ++++++++++++++++ .../xsts/src/test/resources/incrementors.xsts | 16 +++++ 10 files changed, 263 insertions(+) create mode 100644 subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt create mode 100644 subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt create mode 100644 subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt create mode 100644 subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt create mode 100644 subprojects/xsts/xsts/src/test/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChangerUnitTest.kt create mode 100644 subprojects/xsts/xsts/src/test/resources/incrementors.xsts diff --git a/subprojects/cfa/cfa/build.gradle.kts b/subprojects/cfa/cfa/build.gradle.kts index 195f997dbe..25854d3935 100644 --- a/subprojects/cfa/cfa/build.gradle.kts +++ b/subprojects/cfa/cfa/build.gradle.kts @@ -16,6 +16,7 @@ plugins { id("java-common") id("antlr-grammar") + id("kotlin-common") } dependencies { 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 new file mode 100644 index 0000000000..e3260c6bce --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt @@ -0,0 +1,41 @@ +/* + * 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 + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.utils.changeVars + +/** + * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable whose name is present in + * the parameter gets replaced to the associated instance. + */ +fun CFA.copyWithReplacingVars(variableMapping: Map>): CFA { + val builder = CFA.builder() + 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] + if (finalLoc.isPresent) + builder.finalLoc = locationMap[finalLoc.get().name] + edges.forEach { + builder.createEdge( + locationMap[it.source.name], locationMap[it.target.name], + it.stmt.changeVars(variableMapping) + ) + } + return builder.build() +} diff --git a/subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt b/subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt new file mode 100644 index 0000000000..5bacc3fda3 --- /dev/null +++ b/subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt @@ -0,0 +1,40 @@ +/* + * 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 + +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.type.inttype.IntType +import org.junit.jupiter.api.Test +import java.io.FileInputStream + +class CFAVarChangerUnitTest { + + @Test + fun `single variable changing`() { + var origCfa: CFA + FileInputStream("src/test/resources/counter5_true.cfa").use { inputStream -> + origCfa = CfaDslManager.createCfa(inputStream) + } + val newVar = Decls.Var("x", IntType.getInstance()) + val newCfa = origCfa.copyWithReplacingVars(listOf(newVar).associateBy { it.name }) + + assert(!newCfa.vars.any { + origCfa.vars.contains(it) + }) + assert(origCfa.vars.iterator().next() != newCfa.vars.iterator().next()) + } +} \ No newline at end of file diff --git a/subprojects/common/core/build.gradle.kts b/subprojects/common/core/build.gradle.kts index 5a0f56f8d1..1ba5923b5f 100644 --- a/subprojects/common/core/build.gradle.kts +++ b/subprojects/common/core/build.gradle.kts @@ -17,6 +17,7 @@ plugins { id("java-common") id("antlr-grammar") id("java-test-fixtures") + id("kotlin-common") } dependencies { 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..a136c44d94 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,9 @@ import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.Set; /** @@ -78,4 +80,10 @@ public static StmtUnfoldResult toExpr(final List stmts, return StmtToExprTransformer.toExpr(stmts, indexing); } + public static Stmt changeVars(final Stmt stmt, final Iterable> 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/VarChangerUtils.kt b/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt new file mode 100644 index 0000000000..31838601b9 --- /dev/null +++ b/subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt @@ -0,0 +1,66 @@ +/* + * 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.core.utils + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.utils.TypeUtils.cast + +fun Stmt.changeVars(variableMapping: Map>): Stmt { + return when (this) { + is AssignStmt<*> -> AssignStmt.of( + cast(varDecl.changeVars(variableMapping), varDecl.type), + cast(expr.changeVars(variableMapping), varDecl.type) + ) + + is HavocStmt<*> -> HavocStmt.of(varDecl.changeVars(variableMapping)) + is AssumeStmt -> AssumeStmt.of(cond.changeVars(variableMapping)) + 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") + } +} + +fun Expr.changeVars(variableMapping: Map>): Expr = + if (this is RefExpr) { + when (this.decl) { + is VarDecl -> (this.decl as VarDecl).changeVars(variableMapping).ref + else -> this + } + } else this.withOps(this.ops.map { it.changeVars(variableMapping) }) + +@SuppressWarnings("kotlin:S6530") +fun VarDecl.changeVars(variableMapping: Map>): VarDecl { + val swap = variableMapping[this.name] ?: return this + if (swap.type != this.type) + throw RuntimeException("Can't change variable to different type") + return swap as VarDecl +} \ No newline at end of file diff --git a/subprojects/xsts/xsts/build.gradle.kts b/subprojects/xsts/xsts/build.gradle.kts index 195f997dbe..25854d3935 100644 --- a/subprojects/xsts/xsts/build.gradle.kts +++ b/subprojects/xsts/xsts/build.gradle.kts @@ -16,6 +16,7 @@ plugins { id("java-common") id("antlr-grammar") + id("kotlin-common") } dependencies { 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 new file mode 100644 index 0000000000..6a80ea1d76 --- /dev/null +++ b/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt @@ -0,0 +1,33 @@ +/* + * 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.utils + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.NonDetStmt +import hu.bme.mit.theta.core.utils.changeVars +import hu.bme.mit.theta.xsts.XSTS + +fun XSTS.copyWithReplacingVars(variableMapping: Map>): XSTS { + 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 = 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 diff --git a/subprojects/xsts/xsts/src/test/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChangerUnitTest.kt b/subprojects/xsts/xsts/src/test/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChangerUnitTest.kt new file mode 100644 index 0000000000..af7af05863 --- /dev/null +++ b/subprojects/xsts/xsts/src/test/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChangerUnitTest.kt @@ -0,0 +1,56 @@ +/* + * 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.utils + +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.core.utils.StmtUtils +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import org.junit.jupiter.api.Test +import java.io.FileInputStream + +class XSTSVarChangerUnitTest { + + @Test + fun `xsts variable changing`() { + var origXsts: XSTS + FileInputStream("src/test/resources/incrementors.xsts").use { inputStream -> + origXsts = XstsDslManager.createXsts(inputStream) + } + val newX = Decls.Var("x", IntType.getInstance()) + val newY = Decls.Var("y", IntType.getInstance()) + val newXsts = origXsts.copyWithReplacingVars( + listOf(newX, newY) + .associateBy { it.name } + ) + + val origVars = setOf( + StmtUtils.getVars(origXsts.init), + StmtUtils.getVars(origXsts.tran), + StmtUtils.getVars(origXsts.env) + ) + val newVars = setOf( + StmtUtils.getVars(newXsts.init), + StmtUtils.getVars(newXsts.tran), + StmtUtils.getVars(newXsts.env) + ) + + assert(!newVars.any { + origVars.contains(it) + }) + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts/src/test/resources/incrementors.xsts b/subprojects/xsts/xsts/src/test/resources/incrementors.xsts new file mode 100644 index 0000000000..d96e0da425 --- /dev/null +++ b/subprojects/xsts/xsts/src/test/resources/incrementors.xsts @@ -0,0 +1,16 @@ +var x: integer = 0 +ctrl var y: integer + +trans { + x:=x+1; +} + +init { + y:=0; +} + +env { + x:=x+1; +} + +prop {true} \ No newline at end of file