Skip to content

Commit

Permalink
Fixed push-pop order
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Feb 12, 2024
1 parent 664e083 commit 925173a
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 27 deletions.
46 changes: 25 additions & 21 deletions ...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<S : ExprState, A : StmtAction> @JvmOverloads constructor(
Expand Down Expand Up @@ -63,6 +64,14 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" }
}

private fun <T> SolverBase.pushPop(func: () -> T): T {
push()
val ret = func()
pop()
return ret
}


override fun check(prec: UnitPrec?): SafetyResult<S, A> {
var iteration = 0

Expand Down Expand Up @@ -114,23 +123,20 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
}

if (bmcSolver.check().isUnsat) {
bmcSolver.pop()
logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n")
return SafetyResult.safe<S, A>()
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<S, A>? {
Expand All @@ -140,16 +146,14 @@ class BoundedChecker<S : ExprState, A : StmtAction> @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<S, A>()
} 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<S, A>()
} else null
}
}

private fun itp(): SafetyResult<S, A>? {
Expand Down
37 changes: 31 additions & 6 deletions subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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())
}
Expand All @@ -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())
}
}

0 comments on commit 925173a

Please sign in to comment.