Skip to content

Commit

Permalink
Server-side Logika report caching.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 1, 2024
1 parent f03a87c commit 5e709bd
Show file tree
Hide file tree
Showing 5 changed files with 80 additions and 119 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 @@ -97,16 +97,16 @@ final class NoTransitionSmt2CacheImpl(val persistentCache: java.util.concurrent.
override def clearTransition(): Unit = {}

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

def setTransition(th: TypeHierarchy, config: Config, transition: Cache.Transition, state: State,
nextStates: ISZ[State], smt2: Smt2): U64 = u64"0"
nextStates: ISZ[State], smt2: Smt2, reporter: Logika.Reporter, numOfReports: Z): Unit = {}

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

def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State,
nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64 = u64"0"
nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2, reporter: Logika.Reporter, numOfReports: Z): Unit = {}

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

Expand Down
87 changes: 37 additions & 50 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, state: State, smt2: Smt2, reporter: Reporter): Option[ISZ[State]]

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, state: State, nextStates: ISZ[State], smt2: Smt2, reporter: Reporter, numOfReports: Z): Unit

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, state: State, smt2: Smt2, reporter: Reporter): Option[ISZ[(State, State.Value)]]

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, state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2, reporter: Reporter, numOfReports: Z): Unit

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

Expand Down Expand Up @@ -154,6 +154,7 @@ object Logika {
def numOfSats: Z
def vcMillis: Z
def satMillis: Z
def numOfReports: Z

def state(plugins: ISZ[logika.plugin.ClaimPlugin], posOpt: Option[Position], context: ISZ[String],
th: TypeHierarchy, s: State, atLinesFresh: B, atRewrite: B): Unit
Expand All @@ -162,10 +163,12 @@ object Logika {

def inform(pos: Position, kind: Reporter.Info.Kind.Type, message: String): Unit

def coverage(setCache: B, cached: U64, pos: Position): Unit
def coverage(pos: Position): Unit

def empty: Reporter

def child: Reporter

def combine(other: Reporter): Reporter

def illFormed(): Unit
Expand Down Expand Up @@ -3748,13 +3751,13 @@ 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 {
case Some((svs, cached)) =>
reporter.coverage(F, cached, e.posOpt.get)
AST.Stmt.Expr(e, AST.TypedAttr(e.posOpt, e.typedOpt)), state, smt2, reporter) match {
case Some(svs) =>
return svs
case _ =>
}
}
val numOfReports = reporter.numOfReports
val svs = expH(state)
def check(): B = {
if (!(svs.size > 0)) {
Expand All @@ -3777,12 +3780,10 @@ import Util._
if (cachedExp) {
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)
reporter.coverage(T, cached, e.posOpt.get)
} else {
reporter.coverage(F, zeroU64, e.posOpt.get)
cache.setAssignExpTransition(th, config, AST.Stmt.Expr(e, AST.TypedAttr(e.posOpt, e.typedOpt)),
state, svs, smt2, reporter, numOfReports)
}
reporter.coverage(e.posOpt.get)
}
return svs
}
Expand Down Expand Up @@ -3936,25 +3937,22 @@ 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 {
case Some((svs, cached)) =>
reporter.coverage(F, cached, pos)
return svs
cache.getAssignExpTransitionAndUpdateSmt2(th, config, ae, s0, smt2, reporter) match {
case Some(svs) => return svs
case _ =>
}
}
val numOfReports = reporter.numOfReports
val r: ISZ[(State, State.Value)] = ae match {
case ae: AST.Stmt.Expr => evalExp(split, smt2, cache, rtCheck, s0, ae.exp, reporter)
case _ =>
val (s1, sym) = s0.freshSym(t, pos)
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)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
cache.setAssignExpTransition(th, config, ae, s0, r, smt2, reporter, numOfReports)
}
reporter.coverage(pos)
return r
}

Expand Down Expand Up @@ -4713,13 +4711,13 @@ 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 {
case Some((ISZ(nextState), cached)) =>
reporter.coverage(F, cached, pos)
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.ProofStep(step, m.values), s0, smt2, reporter) match {
case Some(ISZ(nextState)) =>
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
case _ =>
}
}
val numOfReports = reporter.numOfReports
val normStep: AST.ProofAst.Step.Regular = step.just match {
case j: AST.ProofAst.Step.Justification.Apply =>
j.invokeIdent.attr.resOpt.get match {
Expand Down Expand Up @@ -4767,11 +4765,9 @@ 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)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
cache.setTransition(th, config, Cache.Transition.ProofStep(step, m.values), s0, ISZ(nextState), smt2, reporter, numOfReports)
}
reporter.coverage(pos)
return (nextState, m + stepNo ~> StepProofContext.Regular(th, stepNo, step.claim))
}
reporter.error(step.just.posOpt, Logika.kind, "Could not recognize justification form")
Expand Down Expand Up @@ -5242,14 +5238,14 @@ 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 {
case Some((ISZ(nextState), cached)) =>
cache.getTransitionAndUpdateSmt2(th, config, Cache.Transition.Sequent(sequent), st0, smt2, reporter) match {
case Some(ISZ(nextState)) =>
cacheHit = T
reporter.coverage(F, cached, pos)
st0 = nextState
case _ =>
}
}
val numOfReports = reporter.numOfReports
if (!cacheHit) {
var i = 0
val st00 = st0
Expand All @@ -5262,11 +5258,9 @@ import Util._
ISZ(), reporter)._1
}
if (config.transitionCache && st0.ok) {
val cached = cache.setTransition(th, config, Cache.Transition.Sequent(sequent), st00, ISZ(st0), smt2)
reporter.coverage(T, cached, pos)
} else {
reporter.coverage(F, zeroU64, pos)
cache.setTransition(th, config, Cache.Transition.Sequent(sequent), st00, ISZ(st0), smt2, reporter, numOfReports)
}
reporter.coverage(pos)
}
} else {
var p = premises(st0, sequent)
Expand Down Expand Up @@ -5447,7 +5441,7 @@ import Util._
|Split statement evaluation does not maintain nextFresh invariant for: ${stmt.prettyST}
|${(for (s <- ss) yield st"* ${s.toST}", "\n")}""".render)
if (stmt.isInstruction) {
reporter.coverage(F, zeroU64, stmt.posOpt.get)
reporter.coverage(stmt.posOpt.get)
}
return p
}
Expand Down Expand Up @@ -5506,15 +5500,12 @@ 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 {
case Some((nextStates, cached)) =>
for (exp <- exps) {
reporter.coverage(F, cached, exp.posOpt.get)
}
return nextStates
cache.getTransitionAndUpdateSmt2(th, config, Logika.Cache.Transition.Exps(exps), s0, smt2, reporter) match {
case Some(nextStates) => return nextStates
case _ =>
}
}
val numOfReports = reporter.numOfReports
var currents = ISZ(s0)
var done = ISZ[State]()
for (exp <- exps) {
Expand All @@ -5530,14 +5521,10 @@ 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)
for (exp <- exps) {
reporter.coverage(T, cached, exp.posOpt.get)
}
} else {
for (exp <- exps) {
reporter.coverage(F, zeroU64, exp.posOpt.get)
}
cache.setTransition(th, config, Logika.Cache.Transition.Exps(exps), s0, r, smt2, reporter, numOfReports)
}
for (exp <- exps) {
reporter.coverage(exp.posOpt.get)
}
return r
}
Expand Down
5 changes: 4 additions & 1 deletion shared/src/main/scala/org/sireum/logika/ReporterImpl.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ final class ReporterImpl(val logPc: B,
override def numOfSats: Z = _numOfSats.get
override def vcMillis: Z = _vcMillis.get
override def satMillis: Z = _satMillis.get
override def numOfReports: Z = _messages.size

override def $clonable: Boolean = clonable

Expand Down Expand Up @@ -120,14 +121,16 @@ final class ReporterImpl(val logPc: B,
override def illFormed(): Unit = {
}

override def coverage(setCache: B, cached: U64, pos: Position): Unit = {
override def coverage(pos: Position): Unit = {
}

override def empty: Logika.Reporter = {
return new ReporterImpl(logPc, logPcRaw, logVc, logDetailedInfo, F, ISZ(), collectStats, _numOfVCs, _numOfSats,
_vcMillis, _satMillis)
}

override def child: Logika.Reporter = this

override def messages: ISZ[Message] = {
return _messages
}
Expand Down
10 changes: 4 additions & 6 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -987,19 +987,17 @@ 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, state: State, smt2: Smt2, reporter: Logika.Reporter): Option[ISZ[State]] = {
return None()
}
override def setTransition(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, state: State, nextStates: ISZ[State], smt2: Smt2): U64 = {
return U64.fromZ(0)
override def setTransition(th: TypeHierarchy, config: Config, transition: Logika.Cache.Transition, state: State, nextStates: ISZ[State], smt2: Smt2, reporter: Logika.Reporter, numOfReports: Z): Unit = {
}

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, state: State, smt2: Smt2, reporter: Logika.Reporter): Option[ISZ[(State, State.Value)]] = {
return None()
}

override def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2): U64 = {
return U64.fromZ(0)
override def setAssignExpTransition(th: TypeHierarchy, config: Config, exp: AST.AssignExp, state: State, nextStatesValues: ISZ[(State, State.Value)], smt2: Smt2, reporter: Logika.Reporter, numOfReports: Z): Unit = {
}

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

0 comments on commit 5e709bd

Please sign in to comment.