From 36238c6609f98f95af211bd3839fde161c8ba813 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Fri, 12 Apr 2024 11:20:23 +0200 Subject: [PATCH] oc checker refactor --- .../analysis/algorithm/oc/BasicOcChecker.kt | 24 +++--- .../theta/analysis/algorithm/oc/OcChecker.kt | 18 ++++- .../algorithm/oc/UserPropagatorOcChecker.kt | 79 ++++++++++--------- .../theta/xcfa/analysis/oc/XcfaOcChecker.kt | 2 + 4 files changed, 68 insertions(+), 55 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/BasicOcChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/BasicOcChecker.kt index ce54797b4c..b9e2e5b6ba 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/BasicOcChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/BasicOcChecker.kt @@ -23,7 +23,7 @@ import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.SolverStatus import java.util.* -class BasicOcChecker : OcCheckerBase { +class BasicOcChecker : OcCheckerBase() { override val solver: Solver = SolverManager.resolveSolverFactory("Z3:4.13").createSolver() private var relations: Array>? = null @@ -58,19 +58,13 @@ class BasicOcChecker : OcCheckerBase { val decision = OcAssignment(decisionStack.peek().rels, rf) decisionStack.push(decision) val reason0 = setAndClose(decision.rels, rf) - if (reason0 != null) { - solver.add(BoolExprs.Not(reason0.expr)) - continue@dpllLoop - } + if (propagate(reason0)) continue@dpllLoop val writes = events[rf.from.const.varDecl]!!.values.flatten() .filter { it.type == EventType.WRITE && it.enabled == true } for (w in writes) { val reason = derive(decision.rels, rf, w) - if (reason != null) { - solver.add(BoolExprs.Not(reason.expr)) - continue@dpllLoop - } + if (propagate(reason)) continue@dpllLoop } } @@ -79,10 +73,7 @@ class BasicOcChecker : OcCheckerBase { decisionStack.push(decision) for (rf in rfs[w.const.varDecl]!!.filter { it.enabled == true }) { val reason = derive(decision.rels, rf, w) - if (reason != null) { - solver.add(BoolExprs.Not(reason.expr)) - continue@dpllLoop - } + if (propagate(reason)) continue@dpllLoop } } @@ -96,6 +87,13 @@ class BasicOcChecker : OcCheckerBase { override fun getRelations(): Array>? = relations?.copy() + override fun propagate(reason: Reason?): Boolean { + reason ?: return false + propagated.add(reason) + solver.add(BoolExprs.Not(reason.expr)) + return true + } + /** * Returns true if obj is not on the stack (in other words, if the value of obj is changed in the new model) */ diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt index e3c116674b..0934027471 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcChecker.kt @@ -58,15 +58,26 @@ interface OcChecker { * blocks, see Event::clkId) */ fun getRelations(): Array>? + + /** + * Get the list of propagated clauses in the form of reasons. + */ + fun getPropagatedClauses(): List } /** * This interface implements basic utilities for an ordering consistency checker such as derivation rules and * transitive closure operations. */ -internal interface OcCheckerBase : OcChecker { +abstract class OcCheckerBase : OcChecker { + + protected val propagated: MutableList = mutableListOf() - fun derive(rels: Array>, rf: Relation, w: E): Reason? = when { + override fun getPropagatedClauses() = propagated.toList() + + protected abstract fun propagate(reason: Reason?): Boolean + + protected fun derive(rels: Array>, rf: Relation, w: E): Reason? = when { rf.from.clkId == rf.to.clkId -> null // rf within an atomic block w.clkId == rf.from.clkId || w.clkId == rf.to.clkId -> null // w within an atomic block with one of the rf ends @@ -83,7 +94,7 @@ internal interface OcCheckerBase : OcChecker { else -> null } - fun setAndClose(rels: Array>, rel: Relation): Reason? { + protected fun setAndClose(rels: Array>, rel: Relation): Reason? { if (rel.from.clkId == rel.to.clkId) return null // within an atomic block return setAndClose(rels, rel.from.clkId, rel.to.clkId, if (rel.type == RelationType.PO) PoReason else RelationReason(rel)) @@ -118,7 +129,6 @@ internal interface OcCheckerBase : OcChecker { } } - /** * Reason(s) of an enabled relation. */ diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/UserPropagatorOcChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/UserPropagatorOcChecker.kt index 458d5f69ae..8faf0ffd32 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/UserPropagatorOcChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/UserPropagatorOcChecker.kt @@ -26,17 +26,42 @@ import hu.bme.mit.theta.solver.javasmt.JavaSMTUserPropagator import org.sosy_lab.java_smt.SolverContextFactory.Solvers.Z3 import java.util.* -class UserPropagatorOcChecker : OcCheckerBase, JavaSMTUserPropagator() { +class UserPropagatorOcChecker : OcCheckerBase() { private val partialAssignment = Stack>() - override val solver: Solver = JavaSMTSolverFactory.create(Z3, arrayOf()).createSolverWithPropagators(this) - private var solverLevel: Int = 0 - private lateinit var writes: Map, Map>> private lateinit var flatWrites: List private lateinit var rfs: Map, List>> private lateinit var flatRfs: List> + private val userPropagator: JavaSMTUserPropagator = object : JavaSMTUserPropagator() { + override fun onKnownValue(expr: Expr, value: Boolean) { + if (value) { + flatRfs.find { it.declRef == expr }?.let { rf -> propagate(rf) } + ?: flatWrites.filter { it.guardExpr == expr }.forEach { w -> propagate(w) } + } + } + + override fun onFinalCheck() = + flatWrites.filter { w -> w.guard.isEmpty() || partialAssignment.any { it.event == w } }.forEach { w -> + propagate(w) + } + + override fun onPush() { + solverLevel++ + } + + override fun onPop(levels: Int) { + solverLevel -= levels + while (partialAssignment.isNotEmpty() && partialAssignment.peek().solverLevel > solverLevel) { + partialAssignment.pop() + } + } + } + + override val solver: Solver = JavaSMTSolverFactory.create(Z3, arrayOf()).createSolverWithPropagators(userPropagator) + private var solverLevel: Int = 0 + override fun check( events: Map, Map>>, pos: List>, @@ -52,53 +77,26 @@ class UserPropagatorOcChecker : OcCheckerBase, JavaSMTUserPropagat pos.forEach { setAndClose(initialRels, it) } partialAssignment.push(OcAssignment(rels = initialRels)) - flatRfs.forEach { rf -> registerExpression(rf.declRef) } - flatWrites.forEach { w -> if (w.guard.isNotEmpty()) registerExpression(w.guardExpr) } + flatRfs.forEach { rf -> userPropagator.registerExpression(rf.declRef) } + flatWrites.forEach { w -> if (w.guard.isNotEmpty()) userPropagator.registerExpression(w.guardExpr) } return solver.check() } override fun getRelations(): Array>? = partialAssignment.lastOrNull()?.rels?.copy() - override fun onKnownValue(expr: Expr, value: Boolean) { - if (value) { - flatRfs.find { it.declRef == expr }?.let { rf -> propagate(rf) } - ?: flatWrites.filter { it.guardExpr == expr }.forEach { w -> propagate(w) } - } - } - - override fun onFinalCheck() = - flatWrites.filter { w -> w.guard.isEmpty() || partialAssignment.any { it.event == w } }.forEach { w -> - propagate(w) - } - - override fun onPush() { - solverLevel++ - } - - override fun onPop(levels: Int) { - solverLevel -= levels - while (partialAssignment.isNotEmpty() && partialAssignment.peek().solverLevel > solverLevel) { - partialAssignment.pop() - } - } - private fun propagate(rf: Relation) { check(rf.type == RelationType.RFI || rf.type == RelationType.RFE) val assignement = OcAssignment(partialAssignment.peek().rels, rf, solverLevel) partialAssignment.push(assignement) val reason0 = setAndClose(assignement.rels, rf) - if (reason0 != null) { - propagateConflict(reason0.exprs) - } + propagate(reason0) val writes = writes[rf.from.const.varDecl]!!.values.flatten() .filter { w -> w.guard.isEmpty() || partialAssignment.any { it.event == w } } for (w in writes) { val reason = derive(assignement.rels, rf, w) - if (reason != null) { - propagateConflict(reason.exprs) - } + propagate(reason) } } @@ -109,10 +107,15 @@ class UserPropagatorOcChecker : OcCheckerBase, JavaSMTUserPropagat partialAssignment.push(assignment) for (rf in rfs) { val reason = derive(assignment.rels, rf, w) - if (reason != null) { - propagateConflict(reason.exprs) - } + propagate(reason) } } } + + override fun propagate(reason: Reason?): Boolean { + reason ?: return false + propagated.add(reason) + userPropagator.propagateConflict(reason.exprs) + return true + } } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index ac77dee4d3..47cb95b35f 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -341,6 +341,8 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv return true } + // Extract counterexample trace from model + private fun getTrace(model: Valuation): Trace, XcfaAction> { val stateList = mutableListOf>() val actionList = mutableListOf()