From 925173a629ff545ecc7f027210b147c7177e67eb Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Mon, 12 Feb 2024 13:28:51 +0100 Subject: [PATCH] Fixed push-pop order --- .../algorithm/bounded/BoundedChecker.kt | 46 ++++++++++--------- .../theta/analysis/algorithm/BoundedTest.kt | 37 ++++++++++++--- 2 files changed, 56 insertions(+), 27 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 10f29e21e4..c9b1fffc2f 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 @@ -33,6 +33,7 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.solver.ItpSolver import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.SolverBase import java.util.* class BoundedChecker @JvmOverloads constructor( @@ -63,6 +64,14 @@ class BoundedChecker @JvmOverloads constructor( check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" } } + private fun SolverBase.pushPop(func: () -> T): T { + push() + val ret = func() + pop() + return ret + } + + override fun check(prec: UnitPrec?): SafetyResult { var iteration = 0 @@ -114,23 +123,20 @@ class BoundedChecker @JvmOverloads constructor( } if (bmcSolver.check().isUnsat) { - bmcSolver.pop() logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n") - return SafetyResult.safe() + return SafetyResult.safe() } } - bmcSolver.push() - bmcSolver.add(Not(unfoldedPropExpr(indices.last()))) - - val ret = if (bmcSolver.check().isSat) { - val trace = getTrace(bmcSolver.model) - logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n") - SafetyResult.unsafe(trace) - } else null + return bmcSolver.pushPop { + bmcSolver.add(Not(unfoldedPropExpr(indices.last()))) - bmcSolver.pop() - return ret + if (bmcSolver.check().isSat) { + val trace = getTrace(bmcSolver.model) + logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n") + SafetyResult.unsafe(trace) + } else null + } } private fun kind(): SafetyResult? { @@ -140,16 +146,14 @@ class BoundedChecker @JvmOverloads constructor( exprs.subList(lastIterLookup.first + 1, exprs.size).forEach { indSolver.add(it) } - indSolver.push() - indSolver.add(Not(unfoldedPropExpr(indices.last()))) - - val ret = if (indSolver.check().isUnsat) { - logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") - SafetyResult.safe() - } else null + return indSolver.pushPop { + indSolver.add(Not(unfoldedPropExpr(indices.last()))) - indSolver.pop() - return ret + if (indSolver.check().isUnsat) { + logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") + SafetyResult.safe() + } else null + } } private fun itp(): SafetyResult? { diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt index fd2c6caa99..00d7e416de 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt @@ -17,7 +17,8 @@ package hu.bme.mit.theta.analysis.algorithm import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedChecker import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr -import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.Decls import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.Stmts.Assign @@ -35,7 +36,8 @@ class BoundedTest { companion object { - private var monolithicExpr: MonolithicExpr? = null + private var unsafeMonolithicExpr: MonolithicExpr? = null + private var safeMonolithicExpr: MonolithicExpr? = null private val valToState = { valuation: Valuation -> ExprStateStub(valuation.toExpr()) } @@ -47,29 +49,52 @@ class BoundedTest { init { val x = Decls.Var("x", Int()) val unfoldResult = StmtUtils.toExpr(Assign(x, IntExprs.Add(x.ref, Int(1))), VarIndexingFactory.indexing(0)) - monolithicExpr = MonolithicExpr( + unsafeMonolithicExpr = MonolithicExpr( AbstractExprs.Eq(x.ref, Int(0)), And(unfoldResult.exprs), AbstractExprs.Neq(x.ref, Int(5)), unfoldResult.indexing ) + safeMonolithicExpr = MonolithicExpr( + AbstractExprs.Eq(x.ref, Int(0)), + And(unfoldResult.exprs), + AbstractExprs.Neq(x.ref, Int(-5)), + unfoldResult.indexing + ) } } @Test - fun testBounded() { + fun testBoundedUnsafe() { val solver = Z3SolverFactory.getInstance().createSolver() val itpSolver = Z3SolverFactory.getInstance().createItpSolver() val indSolver = Z3SolverFactory.getInstance().createSolver() val checker: BoundedChecker<*, *> = BoundedChecker( - monolithicExpr = monolithicExpr!!, + monolithicExpr = unsafeMonolithicExpr!!, bmcSolver = solver, itpSolver = itpSolver, indSolver = indSolver, valToState = valToState, biValToAction = biValToAction, - logger = NullLogger.getInstance()) + logger = ConsoleLogger(Logger.Level.VERBOSE)) val safetyResult: SafetyResult<*, *> = checker.check() Assert.assertTrue(safetyResult.isUnsafe()) } + + @Test + fun testBoundedSafe() { + val solver = Z3SolverFactory.getInstance().createSolver() + val itpSolver = Z3SolverFactory.getInstance().createItpSolver() + val indSolver = Z3SolverFactory.getInstance().createSolver() + val checker: BoundedChecker<*, *> = BoundedChecker( + monolithicExpr = safeMonolithicExpr!!, + bmcSolver = solver, + itpSolver = itpSolver, + indSolver = indSolver, + valToState = valToState, + biValToAction = biValToAction, + logger = ConsoleLogger(Logger.Level.VERBOSE)) + val safetyResult: SafetyResult<*, *> = checker.check() + Assert.assertTrue(safetyResult.isSafe()) + } }