Skip to content

Commit

Permalink
Distinguished transition caching by method name context.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 17, 2024
1 parent 48e9803 commit 7d4555b
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 30 deletions.
8 changes: 4 additions & 4 deletions jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,16 +96,16 @@ final class NoTransitionSmt2CacheImpl(val persistentCache: java.util.concurrent.

override def clearTransition(): Unit = {}

def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Cache.Transition, state: State,
def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Cache.Transition, context: ISZ[String], state: State,
smt2: Smt2): Option[(ISZ[State], U64)] = None()

def setTransition(th: TypeHierarchy, config: Config, transition: Cache.Transition, state: State,
def setTransition(th: TypeHierarchy, config: Config, transition: Cache.Transition, context: ISZ[String], state: State,
nextStates: ISZ[State], smt2: Smt2): U64 = u64"0"

def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State,
def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State,
smt2: Smt2): Option[(ISZ[(State, State.Value)], U64)] = None()

def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State,
def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State,
nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64 = u64"0"

def getSmt2(isSat: B, th: TypeHierarchy, config: Config, timeoutInMs: Z, claims: ISZ[State.Claim]): Option[Smt2Query.Result] = None()
Expand Down
28 changes: 14 additions & 14 deletions shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,13 @@ object Logika {
@msig trait Cache {
def clearTransition(): Unit

def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Cache.Transition, state: State, smt2: Smt2): Option[(ISZ[State], U64)]
def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Cache.Transition, context: ISZ[String], state: State, smt2: Smt2): Option[(ISZ[State], U64)]

def setTransition(th: TypeHierarchy, config: Config, transition: Cache.Transition, state: State, nextStates: ISZ[State], smt2: Smt2): U64
def setTransition(th: TypeHierarchy, config: Config, transition: Cache.Transition, context: ISZ[String], state: State, nextStates: ISZ[State], smt2: Smt2): U64

def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, smt2: Smt2): Option[(ISZ[(State, State.Value)], U64)]
def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State, smt2: Smt2): Option[(ISZ[(State, State.Value)], U64)]

def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64
def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64

def getSmt2(isSat: B, th: TypeHierarchy, config: Config, timeoutInMs: Z, claims: ISZ[State.Claim]): Option[Smt2Query.Result]

Expand Down Expand Up @@ -3747,7 +3747,7 @@ import Util._
}
if (config.transitionCache && cachedExp && state.ok) {
cache.getAssignExpTransitionAndUpdateSmt2(th, config,
AST.Stmt.Expr(e, AST.TypedAttr(e.posOpt, e.typedOpt)), state, smt2) match {
AST.Stmt.Expr(e, AST.TypedAttr(e.posOpt, e.typedOpt)), context.methodName, state, smt2) match {
case Some((svs, cached)) =>
reporter.coverage(F, cached, e.posOpt.get)
return svs
Expand Down Expand Up @@ -3777,7 +3777,7 @@ import Util._
if (config.transitionCache && ops.ISZOps(svs).
forall((p: (State, State.Value)) => p._1.status != State.Status.Error)) {
val cached = cache.setAssignExpTransition(th, config, AST.Stmt.Expr(e, AST.TypedAttr(e.posOpt, e.typedOpt)),
state, svs, smt2)
context.methodName, state, svs, smt2)
reporter.coverage(T, cached, e.posOpt.get)
} else {
reporter.coverage(F, zeroU64, e.posOpt.get)
Expand Down Expand Up @@ -3935,7 +3935,7 @@ import Util._
ae: AST.AssignExp, reporter: Reporter): ISZ[(State, State.Value)] = {
val pos = ae.asStmt.posOpt.get
if (config.transitionCache && s0.ok) {
cache.getAssignExpTransitionAndUpdateSmt2(th, config, ae, s0, smt2) match {
cache.getAssignExpTransitionAndUpdateSmt2(th, config, ae, context.methodName, s0, smt2) match {
case Some((svs, cached)) =>
reporter.coverage(F, cached, pos)
return svs
Expand All @@ -3949,7 +3949,7 @@ import Util._
for (s2 <- evalAssignExp(split, smt2, cache, Some(sym), rtCheck, s1, ae, reporter)) yield (s2, sym)
}
if (config.transitionCache && ops.ISZOps(r).forall((p: (State, State.Value)) => p._1.status != State.Status.Error)) {
val cached = cache.setAssignExpTransition(th, config, ae, s0, r, smt2)
val cached = cache.setAssignExpTransition(th, config, ae, context.methodName, s0, r, smt2)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
Expand Down Expand Up @@ -4712,7 +4712,7 @@ import Util._
case step: AST.ProofAst.Step.Regular =>
val pos = step.claim.posOpt.get
if (config.transitionCache) {
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.ProofStep(step, m.values), s0, smt2) match {
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.ProofStep(step, m.values), context.methodName, s0, smt2) match {
case Some((ISZ(nextState), cached)) =>
reporter.coverage(F, cached, pos)
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
Expand Down Expand Up @@ -4766,7 +4766,7 @@ import Util._
}
val nextState = plugin.handle(this, smt2, cache, m, s0, normStep, reporter)
if (config.transitionCache && nextState.ok && !reporter.hasError) {
val cached = cache.setTransition(th, config, Cache.Transition.ProofStep(step, m.values), s0, ISZ(nextState), smt2)
val cached = cache.setTransition(th, config, Cache.Transition.ProofStep(step, m.values), context.methodName, s0, ISZ(nextState), smt2)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
Expand Down Expand Up @@ -5241,7 +5241,7 @@ import Util._
val pos = sequent.attr.posOpt.get
var cacheHit = F
if (config.transitionCache) {
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.Sequent(sequent), st0, smt2) match {
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.Sequent(sequent), context.methodName, st0, smt2) match {
case Some((ISZ(nextState), cached)) =>
cacheHit = T
reporter.coverage(F, cached, pos)
Expand All @@ -5261,7 +5261,7 @@ import Util._
ISZ(), reporter)._1
}
if (config.transitionCache && st0.ok) {
val cached = cache.setTransition(th, config, Cache.Transition.Sequent(sequent), st00, ISZ(st0), smt2)
val cached = cache.setTransition(th, config, Cache.Transition.Sequent(sequent), context.methodName, st00, ISZ(st0), smt2)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
Expand Down Expand Up @@ -5505,7 +5505,7 @@ import Util._
def checkExps(split: Split.Type, smt2: Smt2, cache: Logika.Cache, rtCheck: B, title: String, titleSuffix: String,
s0: State, exps: ISZ[AST.Exp], reporter: Reporter): ISZ[State] = {
if (config.transitionCache && s0.ok) {
cache.getTransitionAndUpdateSmt2(th, config, Logika.Cache.Transition.Exps(exps), s0, smt2) match {
cache.getTransitionAndUpdateSmt2(th, config, Logika.Cache.Transition.Exps(exps), context.methodName, s0, smt2) match {
case Some((nextStates, cached)) =>
for (exp <- exps) {
reporter.coverage(F, cached, exp.posOpt.get)
Expand All @@ -5529,7 +5529,7 @@ import Util._
}
val r = currents ++ done
if (config.transitionCache && !reporter.hasError) {
val cached = cache.setTransition(th, config, Logika.Cache.Transition.Exps(exps), s0, r, smt2)
val cached = cache.setTransition(th, config, Logika.Cache.Transition.Exps(exps), context.methodName, s0, r, smt2)
for (exp <- exps) {
reporter.coverage(T, cached, exp.posOpt.get)
}
Expand Down
8 changes: 4 additions & 4 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1112,18 +1112,18 @@ object RewritingSystem {
@record class NoCache extends Logika.Cache {

override def clearTransition(): Unit = {}
override def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, state: State, smt2: Smt2): Option[(ISZ[State], U64)] = {
override def getTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, context: ISZ[String], state: State, smt2: Smt2): Option[(ISZ[State], U64)] = {
return None()
}
override def setTransition(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, state: State, nextStates: ISZ[State], smt2: Smt2): U64 = {
override def setTransition(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, context: ISZ[String], state: State, nextStates: ISZ[State], smt2: Smt2): U64 = {
return U64.fromZ(0)
}

override def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, smt2: Smt2): Option[(ISZ[(State, State.Value)], U64)] = {
override def getAssignExpTransitionAndUpdateSmt2(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State, smt2: Smt2): Option[(ISZ[(State, State.Value)], U64)] = {
return None()
}

override def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64 = {
override def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, context: ISZ[String], state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64 = {
return U64.fromZ(0)
}

Expand Down
16 changes: 8 additions & 8 deletions shared/src/main/scala/org/sireum/logika/Util.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1914,7 +1914,7 @@ object Util {
for (r <- requires if s.ok) {
var cacheHit = F
if (logika.config.transitionCache) {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(r), s, smt2) match {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(r), logika.context.methodName, s, smt2) match {
case Some((ISZ(nextState), cached)) =>
cacheHit = T
reporter.coverage(F, cached, r.posOpt.get)
Expand All @@ -1926,7 +1926,7 @@ object Util {
val s0 = s
s = logika.evalAssume(smt2, cache, T, "Precondition", s, r, r.posOpt, reporter)._1
if (logika.config.transitionCache && s.ok) {
val cached = cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(r), s0, ISZ(s), smt2)
val cached = cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(r), logika.context.methodName, s0, ISZ(s), smt2)
reporter.coverage(T, cached, r.posOpt.get)
} else {
reporter.coverage(F, Logika.zeroU64, r.posOpt.get)
Expand Down Expand Up @@ -1958,7 +1958,7 @@ object Util {
for (e <- ensures if s.ok) {
var cacheHit = F
if (logika.config.transitionCache) {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(e), s, smt2) match {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(e), logika.context.methodName, s, smt2) match {
case Some((ISZ(nextState), cached)) =>
cacheHit = T
reporter.coverage(F, cached, e.posOpt.get)
Expand All @@ -1970,7 +1970,7 @@ object Util {
val s0 = s
s = logika.evalAssert(smt2, cache, T, "Postcondition", s, e, e.posOpt, rwLocals, reporter)._1
if (logika.config.transitionCache && s.ok) {
val cached = cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(e), s0, ISZ(s), smt2)
val cached = cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(e), logika.context.methodName, s0, ISZ(s), smt2)
reporter.coverage(T, cached, e.posOpt.get)
} else {
reporter.coverage(F, Logika.zeroU64, e.posOpt.get)
Expand Down Expand Up @@ -2651,7 +2651,7 @@ object Util {
}
if (logika.config.transitionCache) {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config,
Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), s0, smt2) match {
Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), logika.context.methodName, s0, smt2) match {
case Some((ISZ(nextState), cached)) =>
for (inv <- invs) {
reporter.coverage(F, cached, inv.posOpt.get)
Expand Down Expand Up @@ -2701,7 +2701,7 @@ object Util {
}
if (logika.config.transitionCache && s4.ok) {
val cached = cache.setTransition(logika.th, logika.config,
Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), s0, ISZ(s4), smt2)
Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), logika.context.methodName, s0, ISZ(s4), smt2)
for (inv <- invs) {
reporter.coverage(T, cached, inv.posOpt.get)
}
Expand Down Expand Up @@ -2951,7 +2951,7 @@ object Util {
val transition: Logika.Cache.Transition = if (stmt.hasReturnMemoized && ensures.nonEmpty)
Logika.Cache.Transition.StmtExps(stmt, context.methodOpt.get.ensures)
else Logika.Cache.Transition.Stmt(stmt)
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, transition, currentNoOld, smt2) match {
cache.getTransitionAndUpdateSmt2(logika.th, logika.config, transition, logika.context.methodName, currentNoOld, smt2) match {
case Some((ss, cached)) =>
if (stmt.isInstruction) {
reporter.coverage(F, cached, stmt.posOpt.get)
Expand All @@ -2969,7 +2969,7 @@ object Util {
val (l2, ss) = logika.evalStmt(split, smt2, cache, rtCheck, currentNoOld, stmts(i), reporter)
logika = l2
if (!reporter.hasError && ops.ISZOps(ss).forall((s: State) => s.status != State.Status.Error)) {
val cached = cache.setTransition(logika.th, logika.config, transition, currentNoOld, ss, smt2)
val cached = cache.setTransition(logika.th, logika.config, transition, logika.context.methodName, currentNoOld, ss, smt2)
if (stmt.isInstruction) {
reporter.coverage(T, cached, stmt.posOpt.get)
if (stmt.isInstanceOf[AST.Stmt.Return]) {
Expand Down

0 comments on commit 7d4555b

Please sign in to comment.