Skip to content

Commit

Permalink
Rewriting system.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 15, 2024
1 parent d571cd6 commit 814520e
Show file tree
Hide file tree
Showing 6 changed files with 88 additions and 22 deletions.
64 changes: 55 additions & 9 deletions jvm/src/test/scala/org/sireum/logika/example/list.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,11 @@ import org.sireum.justification._
case _ => halt("Trying to access tl on an empty list")
}

@strictpure def tlLax: List[T] = this match {
case List.Cons(_, next) => next
case _ => List.Nil()
}

@strictpure def ++(l2: List[T]): List[T] = this match {
case l@List.Cons(_, next) => l(next = next ++ l2)
case _ => l2
Expand Down Expand Up @@ -154,10 +159,10 @@ object List {
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 _))
4 ( p._1 ≡ key2 ) by Premise,
5 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
6 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)),
7 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
//@formatter:on
)
} else {
Expand All @@ -166,10 +171,10 @@ object List {
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 _))
4 ( !(p._1 ≡ key2) ) by Premise,
5 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
6 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)),
7 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
//@formatter:on
)
}
Expand Down Expand Up @@ -212,7 +217,7 @@ object List {

@strictpure def tail: Queue[T] = {
val thiz = this
thiz(buffer = buffer.tl)
thiz(buffer = buffer.tlLax)
}

@strictpure def length: Z = buffer.length
Expand Down Expand Up @@ -301,6 +306,47 @@ object List {
//@formatter:on
)
}

@pure def frameTail[T](q: Queue[T]): Unit = {
Contract(
Ensures(
q.tail.error ≡ q.error,
q.tail.capacity ≡ q.capacity,
q.tail.strategy ≡ q.strategy
)
)
Deduce(
//@formatter:off
1 ( q.tail.error ≡ q.error ) by Simpl,
2 ( q.tail.capacity ≡ q.capacity ) by Simpl,
3 ( q.tail.strategy ≡ q.strategy ) by Simpl
//@formatter:on
)
}

@pure def wfTail[T](q: Queue[T]): Unit = {
Contract(
Requires(q.wellFormed),
Ensures(q.tail.wellFormed)
)

frameTail(q)

Deduce(
//@formatter:off
1 ( q.wellFormed ) by Premise,
2 ( q.tail.error == q.error ) by Premise,
3 ( q.tail.capacity == q.capacity ) by Premise,
4 ( q.tail.strategy == q.strategy ) by Premise,
5 ( q.buffer.length >= q.tail.length ) by Auto,
6 ( 0 < q.capacity &
(q.strategy != Queue.Strategy.Unbounded __>: q.buffer.length <= q.capacity) ) by Rewrite(RS(Queue.$.wellFormed _), 1), // Auto,
7 ( 0 < q.tail.capacity &
(q.tail.strategy != Queue.Strategy.Unbounded __>: q.tail.buffer.length <= q.tail.capacity) ) by Auto,
8 ( q.tail.wellFormed ) by Rewrite(RS(Queue.$.wellFormed _), 7) // Auto,
//@formatter:on
)
}
}


Expand Down
4 changes: 2 additions & 2 deletions shared/src/main/scala/org/sireum/logika/Logika.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3084,7 +3084,7 @@ import Util._
}
def randomSeed(tpe: AST.Typed.Name): Option[ISZ[(State, State.Value)]] = {
var r = ISZ[(State, State.Value)]()
val pf = State.ProofFun(None(), tpe.ids, "randomSeed", ISZ("seed"), ISZ(AST.Typed.z), tpe)
val pf = State.ProofFun(None(), tpe.ids, "randomSeed", F, ISZ("seed"), ISZ(AST.Typed.z), tpe)
for (p <- evalArgs(split, smt2, cache, rtCheck, s0, 1, eargs, reporter)) {
val s1 = p._1
val args: ISZ[State.Value] = for (argOpt <- p._2) yield argOpt.get
Expand Down Expand Up @@ -3121,7 +3121,7 @@ import Util._
def randomSeedBetween(tpe: AST.Typed.Name): Option[ISZ[(State, State.Value)]] = {
var r = ISZ[(State, State.Value)]()
val posOpt = Option.some(pos)
val pf = State.ProofFun(None(), tpe.ids, "randomSeedBetween", ISZ("seed", "min", "max"),
val pf = State.ProofFun(None(), tpe.ids, "randomSeedBetween", F, ISZ("seed", "min", "max"),
ISZ(AST.Typed.z, tpe, tpe), tpe)
for (p <- evalArgs(split, smt2, cache, rtCheck, s0, 3, eargs, reporter)) {
val s1 = p._1
Expand Down
6 changes: 3 additions & 3 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ object RewritingSystem {
val provenClaims: HashSMap[AST.ProofAst.StepId, AST.CoreExp.Base],
val patterns: ISZ[Rewriter.Pattern.Claim],
val methodPatterns: MethodPatternMap,
val fromStepOpt: Option[(AST.CoreExp.Base, AST.ProofAst.StepId)],
val fromStepOpt: Option[AST.ProofAst.StepId],
val shouldTrace: B,
val shouldTraceEval: B,
val maxUnfolding: Z,
Expand All @@ -243,7 +243,7 @@ object RewritingSystem {
@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)
case Some(fromStepId) => return HashSMap ++ (for (p <- provenClaimStepIdMap.entries if p._2 != fromStepId) yield p)
case _ => return provenClaimStepIdMap
}
}
Expand Down Expand Up @@ -705,7 +705,7 @@ object RewritingSystem {
@pure def translateBody(body: AST.Body, funStack: FunStack, localMap: LocalMap): AST.CoreExp.Base = {
val stmts = body.stmts
var m = localMap
for (i <- 0 until stmts.size - 2) {
for (i <- 0 until stmts.size - 1) {
m = translateStmt(stmts(i), funStack, m)._2
}
return translateAssignExp(stmts(stmts.size - 1).asAssignExp, funStack, m)
Expand Down
1 change: 1 addition & 0 deletions shared/src/main/scala/org/sireum/logika/State.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1109,6 +1109,7 @@ object State {
@datatype class ProofFun(val receiverTypeOpt: Option[AST.Typed],
val context: ISZ[String],
val id: String,
val isByName: B,
val paramIds: ISZ[String],
val paramTypes: ISZ[AST.Typed],
val returnType: AST.Typed)
Expand Down
24 changes: 17 additions & 7 deletions shared/src/main/scala/org/sireum/logika/Util.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1447,9 +1447,14 @@ object Util {
if (resOpt.isEmpty) {
return None()
}
return Some(AST.Exp.Invoke(Some(o), AST.Exp.Ident(AST.Id(let.pf.id, AST.Attr(symPosOpt)),
AST.ResolvedAttr(symPosOpt, resOpt, typedOpt)), ISZ(), es, AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
if (let.pf.isByName) {
return Some(AST.Exp.Select(Some(o), AST.Id(let.pf.id, AST.Attr(symPosOpt)), ISZ(), AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
} else {
return Some(AST.Exp.Invoke(Some(o), AST.Exp.Ident(AST.Id(let.pf.id, AST.Attr(symPosOpt)),
AST.ResolvedAttr(symPosOpt, resOpt, typedOpt)), ISZ(), es, AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
}
case _ => return None()
}
} else {
Expand Down Expand Up @@ -1492,9 +1497,14 @@ object Util {
if (resOpt.isEmpty) {
return None()
}
return Some(AST.Exp.Invoke(rcvOpt, AST.Exp.Ident(AST.Id(let.pf.id, AST.Attr(symPosOpt)),
AST.ResolvedAttr(symPosOpt, resOpt, typedOpt)), ISZ(), es, AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
if (let.pf.isByName) {
return Some(AST.Exp.Select(rcvOpt, AST.Id(let.pf.id, AST.Attr(symPosOpt)), ISZ(), AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
} else {
return Some(AST.Exp.Invoke(rcvOpt, AST.Exp.Ident(AST.Id(let.pf.id, AST.Attr(symPosOpt)),
AST.ResolvedAttr(symPosOpt, resOpt, typedOpt)), ISZ(), es, AST.ResolvedAttr(symPosOpt, resOpt,
Some(sym.tipe))))
}
}
case let: State.Claim.Let.Apply =>
var es = ISZ[AST.Exp]()
Expand Down Expand Up @@ -2285,7 +2295,7 @@ object Util {
receiverTypeOpt: Option[AST.Typed], funType: AST.Typed.Fun, owner: ISZ[String], id: String,
isHelper: B, isStrictPure: B, paramIds: ISZ[AST.Id], body: AST.AssignExp, reporter: Reporter,
implicitContextOpt: Option[(String, Position)]): (State, State.ProofFun) = {
val pf = State.ProofFun(receiverTypeOpt, owner, id, for (id <- paramIds) yield id.value, funType.args, Util.normType(funType.ret))
val pf = State.ProofFun(receiverTypeOpt, owner, id, funType.isByName, for (id <- paramIds) yield id.value, funType.args, Util.normType(funType.ret))
if (smt2.pureFuns.contains(pf)) {
return (state, pf)
} else {
Expand Down
11 changes: 10 additions & 1 deletion shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,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)),
if (fromOpt.isEmpty) None() else Some(fromOpt.get),
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)
Expand Down Expand Up @@ -232,6 +232,15 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
}
i = i + 1
}
if (continu && !rwPc.labeledOnly) {
rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns,
MBox(HashSMap.empty), logika.config.rwMax, rwPc.provenClaimStepIdMapEval, rwClaim, T, T) match {
case Some((r, t)) =>
rwPc.trace = rwPc.trace ++ t
r
case _ => rwClaim
}
}
rwClaim = RewritingSystem.LabeledRemover().transformCoreExpBase(rwClaim).getOrElse(rwClaim)
}
@strictpure def fromCoreClaimST: Option[ST] = if (fromOpt.isEmpty) None() else Some(
Expand Down

0 comments on commit 814520e

Please sign in to comment.