From 7d4555b25461868195e3b15d820375d63268a7d8 Mon Sep 17 00:00:00 2001 From: Robby Date: Sun, 17 Mar 2024 14:11:21 -0500 Subject: [PATCH] Distinguished transition caching by method name context. --- .../logika/NoTransitionSmt2Cache_Ext.scala | 8 +++--- .../main/scala/org/sireum/logika/Logika.scala | 28 +++++++++---------- .../org/sireum/logika/RewritingSystem.scala | 8 +++--- .../main/scala/org/sireum/logika/Util.scala | 16 +++++------ 4 files changed, 30 insertions(+), 30 deletions(-) diff --git a/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala b/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala index 3f73c912..1ae05f27 100644 --- a/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala +++ b/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala @@ -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() diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index eb963fd0..c5ba044f 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -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] @@ -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 @@ -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) @@ -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 @@ -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) @@ -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)) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) } diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index 2bf47d7d..a06135cb 100644 --- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala +++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala @@ -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) } diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala index 6d1d06c1..14b56efe 100644 --- a/shared/src/main/scala/org/sireum/logika/Util.scala +++ b/shared/src/main/scala/org/sireum/logika/Util.scala @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) } @@ -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) @@ -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]) {