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..b376e643 100644 --- a/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala +++ b/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala @@ -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() diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index 351a0baf..e12bf256 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, 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] @@ -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 @@ -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 @@ -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)) { @@ -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 } @@ -3936,13 +3937,12 @@ 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 _ => @@ -3950,11 +3950,9 @@ 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) - 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 } @@ -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 { @@ -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") @@ -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 @@ -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) @@ -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 } @@ -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) { @@ -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 } diff --git a/shared/src/main/scala/org/sireum/logika/ReporterImpl.scala b/shared/src/main/scala/org/sireum/logika/ReporterImpl.scala index 37de48ee..fbe0ad4f 100644 --- a/shared/src/main/scala/org/sireum/logika/ReporterImpl.scala +++ b/shared/src/main/scala/org/sireum/logika/ReporterImpl.scala @@ -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 @@ -120,7 +121,7 @@ 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 = { @@ -128,6 +129,8 @@ final class ReporterImpl(val logPc: B, _vcMillis, _satMillis) } + override def child: Logika.Reporter = this + override def messages: ISZ[Message] = { return _messages } diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index 9eefd3e6..8a00ae62 100644 --- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala +++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala @@ -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] = { diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala index d129d116..0ecca3c4 100644 --- a/shared/src/main/scala/org/sireum/logika/Util.scala +++ b/shared/src/main/scala/org/sireum/logika/Util.scala @@ -1904,23 +1904,21 @@ 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 { - case Some((ISZ(nextState), cached)) => + cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(r), s, smt2, reporter) match { + case Some(ISZ(nextState)) => cacheHit = T - reporter.coverage(F, cached, r.posOpt.get) s = nextState case _ => } } + val numOfReports = reporter.numOfReports if (!cacheHit) { 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) - reporter.coverage(T, cached, r.posOpt.get) - } else { - reporter.coverage(F, Logika.zeroU64, r.posOpt.get) + cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(r), s0, ISZ(s), smt2, reporter, numOfReports) } + reporter.coverage(r.posOpt.get) } } return s @@ -1948,23 +1946,21 @@ 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 { - case Some((ISZ(nextState), cached)) => + cache.getTransitionAndUpdateSmt2(logika.th, logika.config, Logika.Cache.Transition.Exp(e), s, smt2, reporter) match { + case Some(ISZ(nextState)) => cacheHit = T - reporter.coverage(F, cached, e.posOpt.get) s = nextState case _ => } } + val numOfReports = reporter.numOfReports if (!cacheHit) { 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) - reporter.coverage(T, cached, e.posOpt.get) - } else { - reporter.coverage(F, Logika.zeroU64, e.posOpt.get) + cache.setTransition(logika.th, logika.config, Logika.Cache.Transition.Exp(e), s0, ISZ(s), smt2, reporter, numOfReports) } + reporter.coverage(e.posOpt.get) } } if (postPosOpt.nonEmpty && s.ok) { @@ -2641,15 +2637,12 @@ 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 { - case Some((ISZ(nextState), cached)) => - for (inv <- invs) { - reporter.coverage(F, cached, inv.posOpt.get) - } - return nextState + Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), s0, smt2, reporter) match { + case Some(ISZ(nextState)) => return nextState case _ => } } + val numOfReports = reporter.numOfReports val pos = posOpt.get def spInv(): Option[State] = { val claim: AST.Exp = logika.invs2exp(invs, substMap) match { @@ -2690,15 +2683,11 @@ object Util { s4 = logika.evalInv(posOpt, isAssume, title, smt2, cache, rtCheck, s4, inv.ast, substMap, reporter) } 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) - for (inv <- invs) { - reporter.coverage(T, cached, inv.posOpt.get) - } - } else { - for (inv <- invs) { - reporter.coverage(F, Logika.zeroU64, inv.posOpt.get) - } + cache.setTransition(logika.th, logika.config, + Logika.Cache.Transition.Stmts(for (inv <- invs) yield inv.ast), s0, ISZ(s4), smt2, reporter, numOfReports) + } + for (inv <- invs) { + reporter.coverage(inv.posOpt.get) } return s4 } @@ -2882,12 +2871,13 @@ object Util { } def evalStmtsLogika(l: Logika, split: Split.Type, smt2: Smt2, cache: Logika.Cache, rOpt: Option[State.Value.Sym], - rtCheck: B, state: State, stmts: ISZ[AST.Stmt], reporter: Reporter): (Logika, ISZ[State]) = { + rtCheck: B, state: State, stmts: ISZ[AST.Stmt], rep: Reporter): (Logika, ISZ[State]) = { var logika = l val initConfig = logika.config val context = logika.context var currents = ISZ(state) var done = ISZ[State]() + val reporter = rep.child val size: Z = if (rOpt.nonEmpty) stmts.size - 1 else stmts.size for (i <- 0 until size) { @@ -2911,7 +2901,7 @@ object Util { OptionsUtil.toConfig(initConfig, l.context.maxCores, LibUtil.setOptions, l.context.nameExePathMap, value) match { case Either.Left(c) => logika = logika(config = c) - reporter.coverage(F, org.sireum.U64.fromZ(0), stmt.posOpt.get) + reporter.coverage(stmt.posOpt.get) currents = currents :+ currentNoOld case Either.Right(msgs) => for (msg <- msgs) { @@ -2941,40 +2931,23 @@ 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 { - case Some((ss, cached)) => - if (stmt.isInstruction) { - reporter.coverage(F, cached, stmt.posOpt.get) - if (stmt.isInstanceOf[AST.Stmt.Return]) { - for (e <- ensures) { - reporter.coverage(F, cached, e.posOpt.get) - } - } - } - ss + cache.getTransitionAndUpdateSmt2(logika.th, logika.config, transition, currentNoOld, smt2, reporter) match { + case Some(ss) => ss case _ => + val numOfReports = reporter.numOfReports if (stmt.isInstruction) { logika.logPc(current, reporter, stmt.posOpt) } 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) - if (stmt.isInstruction) { - reporter.coverage(T, cached, stmt.posOpt.get) - if (stmt.isInstanceOf[AST.Stmt.Return]) { - for (e <- ensures) { - reporter.coverage(T, cached, e.posOpt.get) - } - } - } - } else { - if (stmt.isInstruction) { - reporter.coverage(F, Logika.zeroU64, stmt.posOpt.get) - if (stmt.isInstanceOf[AST.Stmt.Return]) { - for (e <- ensures) { - reporter.coverage(F, Logika.zeroU64, e.posOpt.get) - } + cache.setTransition(logika.th, logika.config, transition, currentNoOld, ss, smt2, reporter, numOfReports) + } + if (stmt.isInstruction) { + reporter.coverage(stmt.posOpt.get) + if (stmt.isInstanceOf[AST.Stmt.Return]) { + for (e <- ensures) { + reporter.coverage(e.posOpt.get) } } }