From 55492d7e0dce9dff13bc179fc55489ae54eb4980 Mon Sep 17 00:00:00 2001 From: RipplB Date: Thu, 7 Mar 2024 14:09:32 +0100 Subject: [PATCH] Refactoring for conventions --- .../theta/analysis/multi/MultiAnalysis.java | 4 +- .../multi/MultiAnalysisBuilderFunc.java | 37 ------ .../theta/analysis/multi/MultiBuilder.java | 25 +++++ .../mit/theta/analysis/multi/MultiLts.java | 6 +- .../analysis/multi/MultiLtsBuilderFunc.java | 34 ------ .../multi/{ => stmt}/ExprMultiState.java | 4 +- .../multi/{ => stmt}/StmtMultiAction.java | 3 +- .../StmtMultiAnalysis.java} | 16 +-- .../StmtMultiLts.java} | 16 +-- ...{ProductOfTwoTest.kt => MultiOfTwoTest.kt} | 105 +++++++++++++++++- 10 files changed, 152 insertions(+), 98 deletions(-) delete mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java delete mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/{ => stmt}/ExprMultiState.java (93%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/{ => stmt}/StmtMultiAction.java (95%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/{ExprMultiAnalysis.java => stmt/StmtMultiAnalysis.java} (79%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/{ExprMultiLts.java => stmt/StmtMultiLts.java} (78%) rename subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/{ProductOfTwoTest.kt => MultiOfTwoTest.kt} (55%) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java index 2fb9277978..d07e393e21 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java @@ -62,9 +62,9 @@ protected MultiAnalysis(Function defineNextSide, Side getPartialOrd() { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java deleted file mode 100644 index 82c1f08ba8..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java +++ /dev/null @@ -1,37 +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.multi; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.InitFunc; -import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.State; - -import java.util.function.Function; - -@FunctionalInterface -public interface MultiAnalysisBuilderFunc, MAction extends MultiAction, - MAnalysis extends MultiAnalysis> { - - MAnalysis build(MultiAnalysis.Side leftSide, - MultiAnalysis.Side rightSide, - Function defineNextSide, - InitFunc dataInitFunc); - -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java index 542dece37c..29e6910677 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java @@ -92,4 +92,29 @@ public static class BothSidesDone, MAction extends MultiAction, + MAnalysis extends MultiAnalysis> { + + MAnalysis build(MultiAnalysis.Side leftSide, + MultiAnalysis.Side rightSide, + Function defineNextSide, + InitFunc dataInitFunc); + + } + + @FunctionalInterface + public interface MultiLtsBuilderFunc, MAction extends MultiAction, + MLts extends MultiLts> { + + MLts build(LTS leftLts, BiFunction combineLeftState, + LTS rightLts, BiFunction combineRightState, + Function defineNextSide); + + } + } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java index de3354c9d0..120dd8f833 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java @@ -37,9 +37,9 @@ protected MultiLts(Function defineNextSide, Side getEnabledActionsFor(MState state) { @@ -61,7 +61,7 @@ public Function getDefineNextSide() { return defineNextSide; } - protected record Side( + public record Side( LTS lts, BiFunction combineStates) { } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java deleted file mode 100644 index b9153c6226..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java +++ /dev/null @@ -1,34 +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.multi; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.State; - -import java.util.function.BiFunction; -import java.util.function.Function; - -@FunctionalInterface -public interface MultiLtsBuilderFunc, MAction extends MultiAction, - MLts extends MultiLts> { - - MLts build(LTS leftLts, BiFunction combineLeftState, - LTS rightLts, BiFunction combineRightState, - Function defineNextSide); - -} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/ExprMultiState.java similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/ExprMultiState.java index 86bb87be05..fd99266be4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/ExprMultiState.java @@ -13,9 +13,11 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.multi; +package hu.bme.mit.theta.analysis.multi.stmt; import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.analysis.multi.MultiSourceSide; +import hu.bme.mit.theta.analysis.multi.MultiState; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAction.java similarity index 95% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAction.java index f781e4633d..8c7c3ca4cd 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAction.java @@ -13,9 +13,10 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.multi; +package hu.bme.mit.theta.analysis.multi.stmt; import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.analysis.multi.MultiAction; import hu.bme.mit.theta.core.stmt.Stmt; import java.util.List; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAnalysis.java similarity index 79% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAnalysis.java index e3f574019c..bfbc154380 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiAnalysis.java @@ -13,41 +13,43 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.multi; +package hu.bme.mit.theta.analysis.multi.stmt; import hu.bme.mit.theta.analysis.InitFunc; import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.analysis.multi.MultiAnalysis; +import hu.bme.mit.theta.analysis.multi.MultiSourceSide; import java.util.function.Function; -public final class ExprMultiAnalysis extends MultiAnalysis, StmtMultiAction> { - private ExprMultiAnalysis(Function, MultiSourceSide> defineNextSide, Side leftSide, Side rightSide, InitFunc dataInitFunc) { + private StmtMultiAnalysis(Function, MultiSourceSide> defineNextSide, Side leftSide, Side rightSide, InitFunc dataInitFunc) { super(defineNextSide, leftSide, rightSide, dataInitFunc); } public static - ExprMultiAnalysis + StmtMultiAnalysis of(Side leftSide, Side rightSide, Function, MultiSourceSide> defineNextSide, InitFunc dataInitFunc) { - return new ExprMultiAnalysis<>(defineNextSide, leftSide, rightSide, dataInitFunc); + return new StmtMultiAnalysis<>(defineNextSide, leftSide, rightSide, dataInitFunc); } @Override - ExprMultiState createInitialState(LBlank leftState, RBlank rightState, DataState dataState) { + public ExprMultiState createInitialState(LBlank leftState, RBlank rightState, DataState dataState) { return ExprMultiState.createInitial(leftState, rightState, dataState); } @Override - ExprMultiState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide) { + public ExprMultiState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide) { return ExprMultiState.create(leftState, rightState, dataState, sourceSide, true); } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiLts.java similarity index 78% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiLts.java index b6228dfe24..aa7a691a02 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/stmt/StmtMultiLts.java @@ -13,37 +13,39 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.multi; +package hu.bme.mit.theta.analysis.multi.stmt; import hu.bme.mit.theta.analysis.LTS; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.analysis.multi.MultiLts; +import hu.bme.mit.theta.analysis.multi.MultiSourceSide; import java.util.function.BiFunction; import java.util.function.Function; -public final class ExprMultiLts +public final class StmtMultiLts extends MultiLts, StmtMultiAction> { - private ExprMultiLts(Function, MultiSourceSide> defineNextSide, Side left, Side right) { + private StmtMultiLts(Function, MultiSourceSide> defineNextSide, Side left, Side right) { super(defineNextSide, left, right); } public static - ExprMultiLts of( + StmtMultiLts of( LTS leftLts, BiFunction wrapLeftState, LTS rightLts, BiFunction wrapRightState, Function, MultiSourceSide> defineNextSide) { - return new ExprMultiLts<>(defineNextSide, new Side<>(leftLts, wrapLeftState), new Side<>(rightLts, wrapRightState)); + return new StmtMultiLts<>(defineNextSide, new Side<>(leftLts, wrapLeftState), new Side<>(rightLts, wrapRightState)); } @Override - StmtMultiAction wrapLeftAction(LAction action) { + protected StmtMultiAction wrapLeftAction(LAction action) { return StmtMultiAction.ofLeftStmtAction(action); } @Override - StmtMultiAction wrapRightAction(RAction action) { + protected StmtMultiAction wrapRightAction(RAction action) { return StmtMultiAction.ofRightStmtAction(action); } } diff --git a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/ProductOfTwoTest.kt b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt similarity index 55% rename from subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/ProductOfTwoTest.kt rename to subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt index 4241725dde..ff8d3a1c93 100644 --- a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/ProductOfTwoTest.kt +++ b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt @@ -19,12 +19,19 @@ import hu.bme.mit.theta.analysis.algorithm.ArgBuilder import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker import hu.bme.mit.theta.analysis.expl.* +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate import hu.bme.mit.theta.analysis.expr.refinement.* +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAnalysis +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiLts +import hu.bme.mit.theta.analysis.pred.* import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer import hu.bme.mit.theta.analysis.unit.UnitState import hu.bme.mit.theta.cfa.CFA import hu.bme.mit.theta.cfa.analysis.CfaAction -import hu.bme.mit.theta.cfa.analysis.CfaAnalysis.create +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis import hu.bme.mit.theta.cfa.analysis.CfaPrec import hu.bme.mit.theta.cfa.analysis.CfaState import hu.bme.mit.theta.cfa.analysis.lts.CfaLts @@ -47,14 +54,14 @@ import java.io.FileInputStream import java.io.IOException import java.io.SequenceInputStream -class ProductOfTwoTest { +class MultiOfTwoTest { val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) val solver: Solver = Z3SolverFactory.getInstance().createSolver() val itpSolver = Z3SolverFactory.getInstance().createItpSolver() @Test - fun test() { + fun testExplPrec() { var xsts: XSTS try { SequenceInputStream( @@ -84,7 +91,7 @@ class ProductOfTwoTest { FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> cfa = CfaDslManager.createCfa(inputStream) } - val cfaAnalysis = create(cfa.initLoc, dataAnalysis) + val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) val cfaLts: CfaLts = CfaSbeLts.getInstance() val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) val cfaInitFunc = @@ -117,8 +124,8 @@ class ProductOfTwoTest { .build, XstsState, ExplState>, StmtMultiAction>( NextSideFunctions::alternating, dataAnalysis.initFunc, - { ls, rs, dns, dif -> ExprMultiAnalysis.of(ls, rs, dns, dif) }, - { llts, cls, rlts, crs, dns -> ExprMultiLts.of(llts, cls, rlts, crs, dns) }) + { ls, rs, dns, dif -> StmtMultiAnalysis.of(ls, rs, dns, dif) }, + { 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) } @@ -130,7 +137,93 @@ class ProductOfTwoTest { ) val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, PruneStrategy.FULL, logger) val checker = CegarChecker.create(abstractor, refiner) + val result = checker.check(MultiPrec(cfaInitPrec, dataInitPrec, dataInitPrec)) + + assertTrue(result.isUnsafe) + } + + @Test + fun testPredPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop") + ).use { inputStream -> + xsts = XstsDslManager.createXsts(inputStream) + } + } catch (e: IOException) { + throw RuntimeException(e) + } + val dataAnalysis = PredAnalysis.create( + solver, + PredAbstractors.booleanAbstractor(solver), + xsts.initFormula + ) + val xstsAnalysis = XstsAnalysis.create(dataAnalysis) + val xstsLts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())) + val xstsInitFunc = XstsInitFunc.create { _: PredPrec -> listOf(UnitState.getInstance()) } + val xstsCombineStates = { x: XstsState, d: PredState -> XstsState.of(d, x.lastActionWasEnv(), true) } + val xstsStripState = + { x: XstsState -> XstsState.of(UnitState.getInstance(), x.lastActionWasEnv(), true) } + val xstsExtractFromState = { x: XstsState -> x.state } + val xstsStripPrec = { p: PredPrec -> p } + + var cfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + cfa = CfaDslManager.createCfa(inputStream) + } + val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) + val cfaLts: CfaLts = CfaSbeLts.getInstance() + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val cfaInitFunc = + { _: CfaPrec -> listOf>(CfaState.of(cfa.initLoc, UnitState.getInstance())) } + val dataInitPrec = PredPrec.of() + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val cfaCombineStates = { c: CfaState, d: PredState -> CfaState.of(c.loc, d) } + val cfaStripState = { c: CfaState -> CfaState.of(c.loc, UnitState.getInstance()) } + val cfaExtractFromState = { c: CfaState -> c.state } + val cfaStripPrec = { p: CfaPrec -> p } + + val product = MultiBuilder.initWithLeftSide( + cfaAnalysis, + cfaLts, + cfaCombineStates, + cfaStripState, + cfaExtractFromState, + cfaInitFunc, + cfaStripPrec + ) + .addRightSide( + xstsAnalysis, + xstsLts, + xstsCombineStates, + xstsStripState, + xstsExtractFromState, + xstsInitFunc, + xstsStripPrec + ) + .build, XstsState, PredState>, StmtMultiAction>( + NextSideFunctions::alternating, + dataAnalysis.initFunc, + { ls, rs, dns, dif -> StmtMultiAnalysis.of(ls, rs, dns, dif) }, + { llts, cls, rlts, crs, dns -> StmtMultiLts.of(llts, cls, rlts, crs, dns) }) + val prop = Not(xsts.prop) + val dataPredicate = ExprStatePredicate(prop, solver) + val argBuilder = ArgBuilder.create(product.lts, product.analysis) { s -> dataPredicate.test(s.dataState) } + val abstractor = BasicAbstractor.builder(argBuilder).build() + val traceChecker = ExprTraceSeqItpChecker.create(True(), prop, itpSolver) + val precRefiner = + JoiningPrecRefiner.create, XstsState, PredState>, StmtMultiAction, MultiPrec?, PredPrec, PredPrec>, ItpRefutation>( + RefToMultiPrec(cfaRefToPrec, ItpRefToPredPrec(ExprSplitters.atoms()), + ItpRefToPredPrec(ExprSplitters.atoms())) + ) + val refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, PruneStrategy.FULL, logger) + val checker = CegarChecker.create(abstractor, refiner) + + val result = checker.check(MultiPrec(cfaInitPrec, dataInitPrec, dataInitPrec)) + assertTrue(result.isUnsafe) }