From d571cd69a2b7d31853fabf6dcf7a2c6375a7bc08 Mon Sep 17 00:00:00 2001 From: Robby Date: Fri, 15 Mar 2024 10:32:22 -0500 Subject: [PATCH] Rewriting system. --- .../scala/org/sireum/logika/example/list.sc | 51 +++++++++++++++---- .../org/sireum/logika/RewritingSystem.scala | 45 ++++------------ .../sireum/logika/plugin/RewritePlugin.scala | 25 +++++---- 3 files changed, 64 insertions(+), 57 deletions(-) diff --git a/jvm/src/test/scala/org/sireum/logika/example/list.sc b/jvm/src/test/scala/org/sireum/logika/example/list.sc index 825701bc..439af22f 100644 --- a/jvm/src/test/scala/org/sireum/logika/example/list.sc +++ b/jvm/src/test/scala/org/sireum/logika/example/list.sc @@ -99,7 +99,8 @@ object List { 3 ( update(map, key, value) ≡ Cons(p, update(next, key, value)) ) by RSimpl(RS(update _)), //Auto, 4 ( lookup(Cons(p, update(next, key, value)), key) ≡ lookup(update(next, key, value), key) ) by RSimpl(RS(lookup _)), - 5 ( lookup(update(map, key, value), key) ≡ value ) by Rewrite(RS(lookupUpdateEq _), 4) + 5 ( lookup(Cons(p, update(next, key, value)), key) ≡ value ) by Rewrite(RS(lookupUpdateEq _), 4), + 6 ( lookup(update(next, key, value), key) ≡ value ) by Rewrite(RS(lookup _), 5) //@formatter:on ) return @@ -147,16 +148,31 @@ object List { //lookupUpdateNe(next, key1, key2, value) - Deduce( - //@formatter:off - 1 ( key1 ≢ key2 ) by Premise, - 2 ( map ≡ Cons(p, next) ) by Auto, - 3 ( !(p._1 ≡ key1) ) by Premise, - 4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)), - 5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)), - 6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) - //@formatter:on - ) + if (p._1 ≡ key2) { + Deduce( + //@formatter:off + 1 ( key1 ≢ key2 ) by Premise, + 2 ( map ≡ Cons(p, next) ) by Auto, + 3 ( !(p._1 ≡ key1) ) by Premise, + 7 ( p._1 ≡ key2 ) by Premise, + 4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)), + 5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)), + 6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) + //@formatter:on + ) + } else { + Deduce( + //@formatter:off + 1 ( key1 ≢ key2 ) by Premise, + 2 ( map ≡ Cons(p, next) ) by Auto, + 3 ( !(p._1 ≡ key1) ) by Premise, + 7 ( !(p._1 ≡ key2) ) by Premise, + 4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)), + 5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)), + 6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) + //@formatter:on + ) + } return } @@ -272,6 +288,19 @@ object List { //@formatter:on ) } + + @pure def singleQueueHead[T](q: Queue[T], a: T): Unit = { + Contract( + Requires(q.buffer ≡ Cons[T](a, Nil())), + Ensures(q.head ≡ a) + ) + Deduce( + //@formatter:off + 1 ( q.buffer ≡ List.Cons[T](a, List.Nil[T]()) ) by Premise, + 2 ( q.head ≡ a ) by Simpl // Auto + //@formatter:on + ) + } } diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index 2c703a07..5d49a790 100644 --- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala +++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala @@ -235,11 +235,12 @@ object RewritingSystem { val fromStepOpt: Option[(AST.CoreExp.Base, AST.ProofAst.StepId)], val shouldTrace: B, val shouldTraceEval: B, + val maxUnfolding: Z, var labeledOnly: B, var inLabel: B, var done: B, var trace: ISZ[Trace]) { - val unfoldingMap: MBox[UnfoldingNumMap] = MBox(HashSMap.empty) + @strictpure def unfoldingMap: MBox[UnfoldingNumMap] = MBox(HashSMap.empty) @memoize def provenClaimStepIdMapEval: HashSMap[AST.CoreExp.Base, AST.ProofAst.StepId] = { fromStepOpt match { case Some((e, fromStepId)) => return provenClaimStepIdMap - (e, fromStepId) @@ -455,7 +456,7 @@ object RewritingSystem { } case _ => if (r0.isEmpty && labeledOnly) { - evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1, + evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 0, provenClaimStepIdMapEval, o, F, shouldTraceEval) match { case Some((r1, t)) => trace = trace ++ t @@ -492,7 +493,7 @@ object RewritingSystem { } case _ => F } - if (shouldUnfold) { + if (shouldUnfold && (!labeledOnly || inLabel)) { evalBase(th, EvalConfig.none, cache, methodPatterns, unfoldingMap, 1, HashSMap.empty, o2, F, shouldTraceEval) match { case Some((o3, t)) => trace = trace ++ t @@ -545,13 +546,13 @@ object RewritingSystem { if (patterns2.isEmpty) { o } else { - Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, F, F, F, ISZ()). - transformCoreExpBase(cache, o).getOrElse(o) + Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, maxUnfolding, + F, F, F, ISZ()).transformCoreExpBase(cache, o).getOrElse(o) } } } val (o3Opt, t): (Option[AST.CoreExp.Base], ISZ[Trace]) = - evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1, + evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 0, provenClaimStepIdMapEval, o2, F, shouldTraceEval) match { case Some((o3o, t)) => (Some(o3o), t) case _ => (None(), ISZ()) @@ -598,8 +599,8 @@ object RewritingSystem { (for (k <- 0 until apcs.size; apc <- toCondEquiv(th, apcs(k)._2)) yield r2l(Rewriter.Pattern.Claim(pattern.name :+ s"Assumption$k", F, isPermutative(apc), HashSSet.empty, apc))) ++ patterns - val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, F, F, F, ISZ()). - transformCoreExpBase(cache, o).getOrElse(o) + val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, + maxUnfolding, F, F, F, ISZ()).transformCoreExpBase(cache, o).getOrElse(o) val m = unifyExp(T, th, pattern.localPatternSet, from, o2, map, pas, sm, ems) if (ems.value.isEmpty) { unifyPendingApplications(T, th, pattern.localPatternSet, m, pas, sm, ems) match { @@ -1768,11 +1769,7 @@ object RewritingSystem { if (right < left) AST.CoreExp.Binary(right, AST.Exp.BinaryOp.InequivUni, left, AST.Typed.b) else AST.CoreExp.Binary(left, AST.Exp.BinaryOp.InequivUni, right, AST.Typed.b) - var unfoldDisabled = F def shouldUnfold(info: Info.Method): B = { - if (unfoldDisabled) { - return F - } val r = !info.ast.hasContract && info.ast.isStrictPure && ((info.ast.purity == AST.Purity.Abs) ->: methodPatterns.contains((info.name, info.isInObject))) if (!r) { @@ -1888,8 +1885,6 @@ object RewritingSystem { } case _ => } - val oldUnfoldDisabled = unfoldDisabled - unfoldDisabled = T var done = rOpt.isEmpty while (!done) { rOpt match { @@ -1903,7 +1898,6 @@ object RewritingSystem { case _ => done = T } } - unfoldDisabled = oldUnfoldDisabled return rOpt } @@ -2517,26 +2511,7 @@ object RewritingSystem { } return Some(r) } - var tExp = e.tExp - var fExp = e.fExp - if (config.iteBranches) { - val oldUnfoldDisabled = unfoldDisabled - unfoldDisabled = T - evalBaseH(e.tExp) match { - case Some(t) => - changed = T - tExp = t - case _ => - } - evalBaseH(e.fExp) match { - case Some(f) => - changed = T - fExp = f - case _ => - } - unfoldDisabled = oldUnfoldDisabled - } - return if (changed) Some(e(cond = cond, tExp = tExp, fExp = fExp)) else None() + return if (changed) Some(e(cond = cond)) else None() } def evalApply(e: AST.CoreExp.Apply): Option[AST.CoreExp.Base] = { diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala index 3987ade0..6c14047b 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala @@ -135,7 +135,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext val rwPc = Rewriter(if (logika.config.rwPar) logika.config.parCores else 1, logika.th, provenClaims, patterns, methodPatterns, if (fromOpt.isEmpty) None() else Some((fromCoreClaim, fromOpt.get)), - logika.config.rwTrace, logika.config.rwEvalTrace, F, F, F, ISZ()) + logika.config.rwTrace, logika.config.rwEvalTrace, logika.config.rwMax, F, F, F, ISZ()) if (logika.config.rwEvalTrace) { rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("simplifying", stepClaim) } @@ -204,7 +204,10 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext ld.transformCoreExpBase(rwClaim) rwPc.labeledOnly = ld.found var changed = F - while (!done && i < logika.config.rwMax && (if (isRSimpl) rwClaim != AST.CoreExp.True else rwClaim != stepClaim)) { + def continu: B = { + return if (isRSimpl) rwClaim != AST.CoreExp.True else rwClaim != stepClaim + } + while (!done && i < logika.config.rwMax && continu) { rwPc.done = F if (logika.config.rwTrace) { rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("rewriting", rwClaim) @@ -218,18 +221,18 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext done = T rwClaim } + if (continu && !rwPc.labeledOnly) { + rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns, + MBox(HashSMap.empty), 0, rwPc.provenClaimStepIdMapEval, rwClaim, T, T) match { + case Some((r, t)) => + rwPc.trace = rwPc.trace ++ t + r + case _ => rwClaim + } + } i = i + 1 } rwClaim = RewritingSystem.LabeledRemover().transformCoreExpBase(rwClaim).getOrElse(rwClaim) - if (!rwPc.labeledOnly) { - rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns, - rwPc.unfoldingMap, 1, rwPc.provenClaimStepIdMapEval, rwClaim, T, T) match { - case Some((r, t)) => - rwPc.trace = rwPc.trace ++ t - r - case _ => rwClaim - } - } } @strictpure def fromCoreClaimST: Option[ST] = if (fromOpt.isEmpty) None() else Some( st"""After ${if (isEval) "evaluating" else "rewriting"}${if (fromOpt.isEmpty) st"" else st" ${fromOpt.get}"}: