From a59cd852f2a8536ae4e0358506595ea391821620 Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Tue, 6 Oct 2015 18:25:17 +0200
Subject: [PATCH] Supporting resource verification of lazy programs
---
.../util/LetTupleSimplifications.scala | 12 +-
.../laziness/LazinessEliminationPhase.scala | 43 +-
.../scala/leon/laziness/LazinessUtil.scala | 11 +-
.../leon/laziness/LazyClosureConverter.scala | 3 +-
.../leon/laziness/LazyInstrumenter.scala | 62 +++
.../solvers/templates/TemplateGenerator.scala | 2 +-
.../SerialInstrumentationPhase.scala | 499 +++++++++---------
.../RealTimeQueue-transformed.scala | 265 +++++-----
.../lazy-datastructures/RealTimeQueue.scala | 28 +-
9 files changed, 496 insertions(+), 429 deletions(-)
create mode 100644 src/main/scala/leon/laziness/LazyInstrumenter.scala
diff --git a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala b/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
index c89eae941..c62437405 100644
--- a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
+++ b/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
@@ -99,13 +99,10 @@ object LetTupleSimplification {
postMap(replaceMap.lift, true)(e) //perform recursive replacements to handle nested tuple selects
//replaceMap(ts) //replace tuple-selects in the map with the new identifier
- case t: Terminal => t
-
- /*case UnaryOperator(sube, op) =>
- op(recSimplify(sube, replaceMap))
+ case ts @ TupleSelect(Tuple(subes), i) =>
+ subes(i - 1)
- case BinaryOperator(e1, e2, op) =>
- op(recSimplify(e1, replaceMap), recSimplify(e2, replaceMap))*/
+ case t: Terminal => t
case Operator(subes, op) =>
op(subes.map(recSimplify(_, replaceMap)))
@@ -383,6 +380,9 @@ object LetTupleSimplification {
}
}
}
+ // also perform a tuple simplification
+ case ts @ TupleSelect(Tuple(subes), i) =>
+ Some(subes(i - 1))
case _ => None
}
res
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index defad548c..39d2e95ce 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -32,12 +32,13 @@ object LazinessEliminationPhase extends TransformationPhase {
val debugLifting = false
val dumpProgramWithClosures = false
val dumpTypeCorrectProg = false
- val dumpFinalProg = false
+ val dumpProgWithPreAsserts = false
+ val dumpInstrumentedProgram = false
val debugSolvers = false
-
+
val skipVerification = false
val prettyPrint = true
-
+
val name = "Laziness Elimination Phase"
val description = "Coverts a program that uses lazy construct" +
" to a program that does not use lazy constructs"
@@ -50,28 +51,33 @@ object LazinessEliminationPhase extends TransformationPhase {
*/
def apply(ctx: LeonContext, prog: Program): Program = {
- val nprog = liftLazyExpressions(prog)
+ val nprog = liftLazyExpressions(prog)
val progWithClosures = (new LazyClosureConverter(nprog, new LazyClosureFactory(nprog))).apply
if (dumpProgramWithClosures)
- println("After closure conversion: \n" + ScalaPrinter.apply(progWithClosures))
-
- //Rectify type parameters and local types
+ println("After closure conversion: \n" + ScalaPrinter.apply(progWithClosures))
+
+ //Rectify type parameters and local types
val typeCorrectProg = (new TypeRectifier(progWithClosures, tp => tp.id.name.endsWith("@"))).apply
if (dumpTypeCorrectProg)
println("After rectifying types: \n" + ScalaPrinter.apply(typeCorrectProg))
-
- val transProg = (new ClosurePreAsserter(typeCorrectProg)).apply
- if (dumpFinalProg)
- println("After asserting closure preconditions: \n" + ScalaPrinter.apply(transProg))
-
+
+ val progWithPre = (new ClosurePreAsserter(typeCorrectProg)).apply
+ if (dumpProgWithPreAsserts)
+ println("After asserting closure preconditions: \n" + ScalaPrinter.apply(progWithPre))
+
+ // instrument the program for resources
+ val instProg = (new LazyInstrumenter(progWithPre)).apply
+ if(dumpInstrumentedProgram)
+ println("After instrumentation: \n" + ScalaPrinter.apply(instProg))
+
// check specifications (to be moved to a different phase)
if (!skipVerification)
- checkSpecifications(transProg)
+ checkSpecifications(instProg)
if (prettyPrint)
- prettyPrintProgramToFile(transProg, ctx)
- transProg
- }
-
+ prettyPrintProgramToFile(instProg, ctx)
+ instProg
+ }
+
/**
* convert the argument of every lazy constructors to a procedure
*/
@@ -128,7 +134,7 @@ object LazinessEliminationPhase extends TransformationPhase {
prog.definedFunctions.foreach { fd =>
if (fd.annotations.contains("axiom"))
fd.addFlag(Annotation("library", Seq()))
- }
+ }
val functions = Seq() // Seq("--functions=Rotate@rotateLem")
val solverOptions = if(debugSolvers) Seq("--debug=solver") else Seq()
val ctx = Main.processOptions(Seq("--solvers=smt-cvc4") ++ solverOptions ++ functions)
@@ -232,4 +238,3 @@ object LazinessEliminationPhase extends TransformationPhase {
invFuns
}*/
}
-
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index dd65f2df4..eb32ac937 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -57,7 +57,7 @@ object LazinessUtil {
}
}
ctx.reporter.info("Output written on " + outputFolder)
- }
+ }
def isLazyInvocation(e: Expr)(implicit p: Program): Boolean = e match {
case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
@@ -134,6 +134,14 @@ object LazinessUtil {
fd.id.name.startsWith("new@")
}
+ def evalFunctionName(absTypeName: String) = {
+ "eval@" + absTypeName
+ }
+
+ def isEvalFunction(fd: FunDef) = {
+ fd.id.name.startsWith("eval@")
+ }
+
/**
* Returns all functions that 'need' states to be passed in
* and those that return a new state.
@@ -163,4 +171,3 @@ object LazinessUtil {
(funsNeedStates, funsRetStates)
}
}
-
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index 6b11c654c..a54835407 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -134,7 +134,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
val retType = TupleType(Seq(tpe, stType))
// create a eval function
- val dfun = new FunDef(FreshIdentifier("eval" + absdef.id.name, Untyped),
+ val dfun = new FunDef(FreshIdentifier(evalFunctionName(absdef.id.name), Untyped),
tparamDefs, retType, Seq(ValDef(param1), ValDef(param2)))
// assign body of the eval fucntion
@@ -523,4 +523,3 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
evalFunctions.values ++ computeFunctions.values, anchor)
}
}
-
diff --git a/src/main/scala/leon/laziness/LazyInstrumenter.scala b/src/main/scala/leon/laziness/LazyInstrumenter.scala
new file mode 100644
index 000000000..65bff6d22
--- /dev/null
+++ b/src/main/scala/leon/laziness/LazyInstrumenter.scala
@@ -0,0 +1,62 @@
+package leon
+package laziness
+
+import invariant.factories._
+import invariant.util.Util._
+import invariant.util._
+import invariant.structure.FunctionUtils._
+import purescala.ScalaPrinter
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.DefOps._
+import purescala.Extractors._
+import purescala.Types._
+import leon.invariant.util.TypeUtil._
+import leon.invariant.util.LetTupleSimplification._
+import leon.verification.AnalysisPhase
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+import scala.util.matching.Regex
+import leon.purescala.PrettyPrinter
+import leon.LeonContext
+import leon.LeonOptionDef
+import leon.Main
+import leon.transformations._
+import LazinessUtil._
+
+class LazyInstrumenter(p: Program) {
+
+ def apply: Program = {
+ val exprInstFactory = (x: Map[FunDef, FunDef], y: SerialInstrumenter, z: FunDef) =>
+ new LazyExprInstrumenter(x, y)(z)
+ (new SerialInstrumenter(p, Some(exprInstFactory))).apply
+ }
+
+ class LazyExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrumenter)(implicit currFun: FunDef)
+ extends ExprInstrumenter(funMap, serialInst)(currFun) {
+
+ val costOfMemoization: Map[Instrumentation, Int] =
+ Map(Time -> 1, Stack -> 1, Rec -> 1, TPR -> 1, Depth -> 1)
+
+ override def apply(e: Expr): Expr = {
+ if (isEvalFunction(currFun)) {
+ val closureParam = currFun.params(0).id.toVariable
+ val stateParam = currFun.params(1).id.toVariable
+ val nbody = super.apply(e)
+ val bodyId = FreshIdentifier("bd", nbody.getType, true)
+ val instExprs = instrumenters map { m =>
+ IfExpr(ElementOfSet(closureParam, stateParam),
+ //SubsetOf(FiniteSet(Set(closureParam), closureParam.getType), stateParam),
+ InfiniteIntegerLiteral(costOfMemoization(m.inst)),
+ selectInst(bodyId.toVariable, m.inst))
+ }
+ Let(bodyId, nbody,
+ Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
+
+ } else super.apply(e)
+ }
+ }
+}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index f6484ff7b..1ecc2c9cd 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -95,7 +95,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
val (postConds, postExprs, postGuarded, postLambdas, postQuantifications) = mkClauses(start, postHolds, substMap)
- val allGuarded = (bodyGuarded.keys ++ postGuarded.keys).map { k =>
+ val allGuarded = (bodyGuarded.keys ++ postGuarded.keys).map { k =>
k -> (bodyGuarded.getOrElse(k, Seq.empty) ++ postGuarded.getOrElse(k, Seq.empty))
}.toMap
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index 20e3aa0e2..fba97a85b 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -12,7 +12,7 @@ import leon.utils._
import invariant.util._
import invariant.util.CallGraphUtil
import invariant.structure.FunctionUtils._
-import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{ Map => MutableMap }
/**
* An instrumentation phase that performs a sequence of instrumentations
@@ -23,14 +23,16 @@ object InstrumentationPhase extends TransformationPhase {
val description = "Instruments the program for all counters needed"
def apply(ctx: LeonContext, program: Program): Program = {
- val instprog = new SerialInstrumenter(ctx, program)
+ val instprog = new SerialInstrumenter(program)
instprog.apply
}
}
-class SerialInstrumenter(ctx: LeonContext, program: Program) {
+class SerialInstrumenter(program: Program,
+ exprInstOpt : Option[(Map[FunDef, FunDef], SerialInstrumenter, FunDef) => ExprInstrumenter] = None) {
val debugInstrumentation = false
+ val exprInstFactory = exprInstOpt.getOrElse((x: Map[FunDef, FunDef], y : SerialInstrumenter, z: FunDef) => new ExprInstrumenter(x, y)(z))
val instToInstrumenter: Map[Instrumentation, Instrumenter] =
Map(Time -> new TimeInstrumenter(program, this),
Depth -> new DepthInstrumenter(program, this),
@@ -40,15 +42,17 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
// a map from functions to the list of instrumentations to be performed for the function
lazy val funcInsts = {
- var emap = MutableMap[FunDef,List[Instrumentation]]()
+ var emap = MutableMap[FunDef, List[Instrumentation]]()
def update(fd: FunDef, inst: Instrumentation) {
if (emap.contains(fd))
emap(fd) = (emap(fd) :+ inst).distinct
else emap.update(fd, List(inst))
}
- instToInstrumenter.values.foreach{ m =>
- m.functionsToInstrument.foreach({ case (fd, instsToPerform) =>
- instsToPerform.foreach(instToPerform => update(fd, instToPerform)) })
+ instToInstrumenter.values.foreach { m =>
+ m.functionsToInstrument.foreach({
+ case (fd, instsToPerform) =>
+ instsToPerform.foreach(instToPerform => update(fd, instToPerform))
+ })
}
emap.toMap
}
@@ -100,7 +104,8 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
def mapBody(body: Expr, from: FunDef, to: FunDef) = {
val res = if (instFuncs.contains(from)) {
- (new ExprInstrumenter(funMap)(from)(body))
+ //(new ExprInstrumenter(funMap, this)(from)(body))
+ exprInstFactory(funMap, this, from)(body)
} else
mapExpr(body)
res
@@ -154,16 +159,17 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
}
}
- val additionalFuncs = funMap.flatMap{ case (k, _) =>
- if (instFuncs(k))
- instrumenters(k).flatMap(_.additionalfunctionsToAdd)
- else List()
+ val additionalFuncs = funMap.flatMap {
+ case (k, _) =>
+ if (instFuncs(k))
+ instrumenters(k).flatMap(_.additionalfunctionsToAdd)
+ else List()
}.toList.distinct
val newprog = Util.copyProgram(program, (defs: Seq[Definition]) =>
defs.map {
case fd: FunDef if funMap.contains(fd) =>
- funMap(fd)
+ funMap(fd)
case d => d
} ++ additionalFuncs)
if (debugInstrumentation)
@@ -172,269 +178,269 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
ProgramSimplifier(newprog)
}
- class ExprInstrumenter(funMap: Map[FunDef, FunDef])(implicit currFun: FunDef) {
- val retainMatches = true
-
- val insts = funcInsts(currFun)
- val instrumenters = SerialInstrumenter.this.instrumenters(currFun)
- val instIndex = SerialInstrumenter.this.instIndex(currFun) _
- val selectInst = SerialInstrumenter.this.selectInst(currFun) _
- val instTypes = SerialInstrumenter.this.instTypes(currFun)
-
- // Should be called only if 'expr' has to be instrumented
- // Returned Expr is always an expr of type tuple (Expr, Int)
- def tupleify(e: Expr, subs: Seq[Expr], recons: Seq[Expr] => Expr)(implicit letIdMap: Map[Identifier, Identifier]): Expr = {
- // When called for:
- // Op(n1,n2,n3)
- // e = Op(n1,n2,n3)
- // subs = Seq(n1,n2,n3)
- // recons = { Seq(newn1,newn2,newn3) => Op(newn1, newn2, newn3) }
- //
- // This transformation should return, informally:
- //
- // LetTuple((e1,t1), transform(n1),
- // LetTuple((e2,t2), transform(n2),
- // ...
- // Tuple(recons(e1, e2, ...), t1 + t2 + ... costOfExpr(Op)
- // ...
- // )
- // )
- //
- // You will have to handle FunctionInvocation specially here!
- tupleifyRecur(e, subs, recons, List(), Map())
- }
+}
- def tupleifyRecur(e: Expr, subs: Seq[Expr], recons: Seq[Expr] => Expr, subeVals: List[Expr],
- subeInsts: Map[Instrumentation, List[Expr]])(implicit letIdMap: Map[Identifier, Identifier]): Expr = {
- //note: subs.size should be zero if e is a terminal
- if (subs.size == 0) {
- e match {
- case v @ Variable(id) =>
- val valPart = if (letIdMap.contains(id)) {
- TupleSelect(letIdMap(id).toVariable, 1) //this takes care of replacement
- } else v
- val instPart = instrumenters map (_.instrument(v, Seq()))
- Tuple(valPart +: instPart)
-
- case t: Terminal =>
- val instPart = instrumenters map (_.instrument(t, Seq()))
- val finalRes = Tuple(t +: instPart)
- finalRes
-
- case f @ FunctionInvocation(tfd, args) if tfd.fd.isRealFunction =>
- val newfd = funMap(tfd.fd)
- val newFunInv = FunctionInvocation(TypedFunDef(newfd, tfd.tps), subeVals)
- //create a variables to store the result of function invocation
- if (instFuncs(tfd.fd)) {
- //this function is also instrumented
- val resvar = Variable(FreshIdentifier("e", newfd.returnType, true))
- val valexpr = TupleSelect(resvar, 1)
- val instexprs = instrumenters.map { m =>
- val calleeInst = if (funcInsts(tfd.fd).contains(m.inst)) {
- List(SerialInstrumenter.this.selectInst(tfd.fd)(resvar, m.inst))
- } else List()
- //Note we need to ensure that the last element of list is the instval of the finv
- m.instrument(e, subeInsts.getOrElse(m.inst, List()) ++ calleeInst, Some(resvar))
- }
- Let(resvar.id, newFunInv, Tuple(valexpr +: instexprs))
- } else {
- val resvar = Variable(FreshIdentifier("e", tfd.fd.returnType, true))
- val instexprs = instrumenters.map { m =>
- m.instrument(e, subeInsts.getOrElse(m.inst, List()))
- }
- Let(resvar.id, newFunInv, Tuple(resvar +: instexprs))
- }
+class ExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrumenter)(implicit currFun: FunDef) {
+ val retainMatches = true
+
+ val insts = serialInst.funcInsts(currFun)
+ val instrumenters = serialInst.instrumenters(currFun)
+ val instIndex = serialInst.instIndex(currFun) _
+ val selectInst = serialInst.selectInst(currFun) _
+ val instTypes = serialInst.instTypes(currFun)
+
+ // Should be called only if 'expr' has to be instrumented
+ // Returned Expr is always an expr of type tuple (Expr, Int)
+ def tupleify(e: Expr, subs: Seq[Expr], recons: Seq[Expr] => Expr)(implicit letIdMap: Map[Identifier, Identifier]): Expr = {
+ // When called for:
+ // Op(n1,n2,n3)
+ // e = Op(n1,n2,n3)
+ // subs = Seq(n1,n2,n3)
+ // recons = { Seq(newn1,newn2,newn3) => Op(newn1, newn2, newn3) }
+ //
+ // This transformation should return, informally:
+ //
+ // LetTuple((e1,t1), transform(n1),
+ // LetTuple((e2,t2), transform(n2),
+ // ...
+ // Tuple(recons(e1, e2, ...), t1 + t2 + ... costOfExpr(Op)
+ // ...
+ // )
+ // )
+ //
+ // You will have to handle FunctionInvocation specially here!
+ tupleifyRecur(e, subs, recons, List(), Map())
+ }
- // This case will be taken if the function invocation is actually a val (lazy or otherwise) in the class
- case f @ FunctionInvocation(tfd, args) =>
- val resvar = Variable(FreshIdentifier("e", tfd.fd.returnType, true))
- val instPart = instrumenters map (_.instrument(f, Seq()))
- val finalRes = Tuple(f +: instPart)
- finalRes
-
- case _ =>
- val exprPart = recons(subeVals)
- val instexprs = instrumenters.zipWithIndex.map {
- case (menter, i) => menter.instrument(e, subeInsts.getOrElse(menter.inst, List()))
+ def tupleifyRecur(e: Expr, subs: Seq[Expr], recons: Seq[Expr] => Expr, subeVals: List[Expr],
+ subeInsts: Map[Instrumentation, List[Expr]])(implicit letIdMap: Map[Identifier, Identifier]): Expr = {
+ //note: subs.size should be zero if e is a terminal
+ if (subs.size == 0) {
+ e match {
+ case v @ Variable(id) =>
+ val valPart = if (letIdMap.contains(id)) {
+ TupleSelect(letIdMap(id).toVariable, 1) //this takes care of replacement
+ } else v
+ val instPart = instrumenters map (_.instrument(v, Seq()))
+ Tuple(valPart +: instPart)
+
+ case t: Terminal =>
+ val instPart = instrumenters map (_.instrument(t, Seq()))
+ val finalRes = Tuple(t +: instPart)
+ finalRes
+
+ case f @ FunctionInvocation(tfd, args) if tfd.fd.isRealFunction =>
+ val newfd = TypedFunDef(funMap(tfd.fd), tfd.tps)
+ val newFunInv = FunctionInvocation(newfd, subeVals)
+ //create a variables to store the result of function invocation
+ if (serialInst.instFuncs(tfd.fd)) {
+ //this function is also instrumented
+ val resvar = Variable(FreshIdentifier("e", newfd.returnType, true))
+ val valexpr = TupleSelect(resvar, 1)
+ val instexprs = instrumenters.map { m =>
+ val calleeInst = if (serialInst.funcInsts(tfd.fd).contains(m.inst)) {
+ List(serialInst.selectInst(tfd.fd)(resvar, m.inst))
+ } else List()
+ //Note we need to ensure that the last element of list is the instval of the finv
+ m.instrument(e, subeInsts.getOrElse(m.inst, List()) ++ calleeInst, Some(resvar))
}
- Tuple(exprPart +: instexprs)
- }
- } else {
- val currExp = subs.head
- val resvar = Variable(FreshIdentifier("e", TupleType(currExp.getType +: instTypes), true))
- val eval = TupleSelect(resvar, 1)
- val instMap = insts.map { inst =>
- (inst -> (subeInsts.getOrElse(inst, List()) :+ selectInst(resvar, inst)))
- }.toMap
- //process the remaining arguments
- val recRes = tupleifyRecur(e, subs.tail, recons, subeVals :+ eval, instMap)
- //transform the current expression
- val newCurrExpr = transform(currExp)
- Let(resvar.id, newCurrExpr, recRes)
+ Let(resvar.id, newFunInv, Tuple(valexpr +: instexprs))
+ } else {
+ val resvar = Variable(FreshIdentifier("e", newFunInv.getType, true))
+ val instexprs = instrumenters.map { m =>
+ m.instrument(e, subeInsts.getOrElse(m.inst, List()))
+ }
+ Let(resvar.id, newFunInv, Tuple(resvar +: instexprs))
+ }
+
+ // This case will be taken if the function invocation is actually a val (lazy or otherwise) in the class
+ case f @ FunctionInvocation(tfd, args) =>
+ val resvar = Variable(FreshIdentifier("e", tfd.fd.returnType, true))
+ val instPart = instrumenters map (_.instrument(f, Seq()))
+ val finalRes = Tuple(f +: instPart)
+ finalRes
+
+ case _ =>
+ val exprPart = recons(subeVals)
+ val instexprs = instrumenters.zipWithIndex.map {
+ case (menter, i) => menter.instrument(e, subeInsts.getOrElse(menter.inst, List()))
+ }
+ Tuple(exprPart +: instexprs)
}
+ } else {
+ val currExp = subs.head
+ val resvar = Variable(FreshIdentifier("e", TupleType(currExp.getType +: instTypes), true))
+ val eval = TupleSelect(resvar, 1)
+ val instMap = insts.map { inst =>
+ (inst -> (subeInsts.getOrElse(inst, List()) :+ selectInst(resvar, inst)))
+ }.toMap
+ //process the remaining arguments
+ val recRes = tupleifyRecur(e, subs.tail, recons, subeVals :+ eval, instMap)
+ //transform the current expression
+ val newCurrExpr = transform(currExp)
+ Let(resvar.id, newCurrExpr, recRes)
}
+ }
- /**
- * TODO: need to handle new expression trees
- * Match statements without guards are now instrumented directly
- */
- def transform(e: Expr)(implicit letIdMap: Map[Identifier, Identifier]): Expr = e match {
- // Assume that none of the matchcases has a guard. It has already been converted into an if then else
- case me @ MatchExpr(scrutinee, matchCases) =>
- val containsGuard = matchCases.exists(currCase => currCase.optGuard.isDefined)
- if (containsGuard) {
- def rewritePM(me: MatchExpr): Option[Expr] = {
- val MatchExpr(scrut, cases) = me
- val condsAndRhs = for (cse <- cases) yield {
- val map = mapForPattern(scrut, cse.pattern)
- val patCond = conditionForPattern(scrut, cse.pattern, includeBinders = false)
- val realCond = cse.optGuard match {
- case Some(g) => And(patCond, replaceFromIDs(map, g))
- case None => patCond
- }
- val newRhs = replaceFromIDs(map, cse.rhs)
- (realCond, newRhs)
+ /**
+ * TODO: need to handle new expression trees
+ * Match statements without guards are now instrumented directly
+ */
+ def transform(e: Expr)(implicit letIdMap: Map[Identifier, Identifier]): Expr = e match {
+ // Assume that none of the matchcases has a guard. It has already been converted into an if then else
+ case me @ MatchExpr(scrutinee, matchCases) =>
+ val containsGuard = matchCases.exists(currCase => currCase.optGuard.isDefined)
+ if (containsGuard) {
+ def rewritePM(me: MatchExpr): Option[Expr] = {
+ val MatchExpr(scrut, cases) = me
+ val condsAndRhs = for (cse <- cases) yield {
+ val map = mapForPattern(scrut, cse.pattern)
+ val patCond = conditionForPattern(scrut, cse.pattern, includeBinders = false)
+ val realCond = cse.optGuard match {
+ case Some(g) => And(patCond, replaceFromIDs(map, g))
+ case None => patCond
}
- val bigIte = condsAndRhs.foldRight[Expr](
- Error(me.getType, "Match is non-exhaustive").copiedFrom(me))((p1, ex) => {
- if (p1._1 == BooleanLiteral(true)) {
- p1._2
- } else {
- IfExpr(p1._1, p1._2, ex)
- }
- })
- Some(bigIte)
+ val newRhs = replaceFromIDs(map, cse.rhs)
+ (realCond, newRhs)
}
- transform(rewritePM(me).get)
- } else {
- val instScrutinee =
- Variable(FreshIdentifier("scr", TupleType(scrutinee.getType +: instTypes), true))
-
- def transformMatchCaseList(mCases: Seq[MatchCase]): Seq[MatchCase] = {
- def transformMatchCase(mCase: MatchCase) = {
- val MatchCase(pattern, guard, expr) = mCase
- val newExpr = {
- val exprVal =
- Variable(FreshIdentifier("expr", TupleType(expr.getType +: instTypes), true))
- val newExpr = transform(expr)
- val instExprs = instrumenters map { m =>
- m.instrumentMatchCase(me, mCase, selectInst(exprVal, m.inst),
- selectInst(instScrutinee, m.inst))
- }
- val letBody = Tuple(TupleSelect(exprVal, 1) +: instExprs)
- Let(exprVal.id, newExpr, letBody)
+ val bigIte = condsAndRhs.foldRight[Expr](
+ Error(me.getType, "Match is non-exhaustive").copiedFrom(me))((p1, ex) => {
+ if (p1._1 == BooleanLiteral(true)) {
+ p1._2
+ } else {
+ IfExpr(p1._1, p1._2, ex)
}
- MatchCase(pattern, guard, newExpr)
- }
- if (mCases.length == 0) Seq[MatchCase]()
- else {
- transformMatchCase(mCases.head) +: transformMatchCaseList(mCases.tail)
+ })
+ Some(bigIte)
+ }
+ transform(rewritePM(me).get)
+ } else {
+ val instScrutinee =
+ Variable(FreshIdentifier("scr", TupleType(scrutinee.getType +: instTypes), true))
+
+ def transformMatchCaseList(mCases: Seq[MatchCase]): Seq[MatchCase] = {
+ def transformMatchCase(mCase: MatchCase) = {
+ val MatchCase(pattern, guard, expr) = mCase
+ val newExpr = {
+ val exprVal =
+ Variable(FreshIdentifier("expr", TupleType(expr.getType +: instTypes), true))
+ val newExpr = transform(expr)
+ val instExprs = instrumenters map { m =>
+ m.instrumentMatchCase(me, mCase, selectInst(exprVal, m.inst),
+ selectInst(instScrutinee, m.inst))
+ }
+ val letBody = Tuple(TupleSelect(exprVal, 1) +: instExprs)
+ Let(exprVal.id, newExpr, letBody)
}
+ MatchCase(pattern, guard, newExpr)
+ }
+ if (mCases.length == 0) Seq[MatchCase]()
+ else {
+ transformMatchCase(mCases.head) +: transformMatchCaseList(mCases.tail)
}
- val matchExpr = MatchExpr(TupleSelect(instScrutinee, 1),
- transformMatchCaseList(matchCases))
- Let(instScrutinee.id, transform(scrutinee), matchExpr)
}
+ val matchExpr = MatchExpr(TupleSelect(instScrutinee, 1),
+ transformMatchCaseList(matchCases))
+ Let(instScrutinee.id, transform(scrutinee), matchExpr)
+ }
- case Let(i, v, b) => {
- val (ni, nv) = {
- val ir = Variable(FreshIdentifier("ir", TupleType(v.getType +: instTypes), true))
- val transv = transform(v)
- (ir, transv)
- }
- val r = Variable(FreshIdentifier("r", TupleType(b.getType +: instTypes), true))
- val transformedBody = transform(b)(letIdMap + (i -> ni.id))
- val instexprs = instrumenters map { m =>
- m.instrument(e, List(selectInst(ni, m.inst), selectInst(r, m.inst)))
- }
- Let(ni.id, nv,
- Let(r.id, transformedBody, Tuple(TupleSelect(r, 1) +: instexprs)))
+ case Let(i, v, b) => {
+ val (ni, nv) = {
+ val ir = Variable(FreshIdentifier("ir", TupleType(v.getType +: instTypes), true))
+ val transv = transform(v)
+ (ir, transv)
+ }
+ val r = Variable(FreshIdentifier("r", TupleType(b.getType +: instTypes), true))
+ val transformedBody = transform(b)(letIdMap + (i -> ni.id))
+ val instexprs = instrumenters map { m =>
+ m.instrument(e, List(selectInst(ni, m.inst), selectInst(r, m.inst)))
}
+ Let(ni.id, nv,
+ Let(r.id, transformedBody, Tuple(TupleSelect(r, 1) +: instexprs)))
+ }
- case ife @ IfExpr(cond, th, elze) => {
- val (nifCons, condInsts) = {
- val rescond = Variable(FreshIdentifier("c", TupleType(cond.getType +: instTypes), true))
- val condInstPart = insts.map { inst => (inst -> selectInst(rescond, inst)) }.toMap
- val recons = (e1: Expr, e2: Expr) => {
- Let(rescond.id, transform(cond), IfExpr(TupleSelect(rescond, 1), e1, e2))
- }
- (recons, condInstPart)
- }
- val (nthenCons, thenInsts) = {
- val resthen = Variable(FreshIdentifier("th", TupleType(th.getType +: instTypes), true))
- val thInstPart = insts.map { inst => (inst -> selectInst(resthen, inst)) }.toMap
- val recons = (theninsts: List[Expr]) => {
- Let(resthen.id, transform(th), Tuple(TupleSelect(resthen, 1) +: theninsts))
- }
- (recons, thInstPart)
+ case ife @ IfExpr(cond, th, elze) => {
+ val (nifCons, condInsts) = {
+ val rescond = Variable(FreshIdentifier("c", TupleType(cond.getType +: instTypes), true))
+ val condInstPart = insts.map { inst => (inst -> selectInst(rescond, inst)) }.toMap
+ val recons = (e1: Expr, e2: Expr) => {
+ Let(rescond.id, transform(cond), IfExpr(TupleSelect(rescond, 1), e1, e2))
}
- val (nelseCons, elseInsts) = {
- val reselse = Variable(FreshIdentifier("el", TupleType(elze.getType +: instTypes), true))
- val elInstPart = insts.map { inst => (inst -> selectInst(reselse, inst)) }.toMap
- val recons = (einsts: List[Expr]) => {
- Let(reselse.id, transform(elze), Tuple(TupleSelect(reselse, 1) +: einsts))
- }
- (recons, elInstPart)
+ (recons, condInstPart)
+ }
+ val (nthenCons, thenInsts) = {
+ val resthen = Variable(FreshIdentifier("th", TupleType(th.getType +: instTypes), true))
+ val thInstPart = insts.map { inst => (inst -> selectInst(resthen, inst)) }.toMap
+ val recons = (theninsts: List[Expr]) => {
+ Let(resthen.id, transform(th), Tuple(TupleSelect(resthen, 1) +: theninsts))
}
- val (finalThInsts, finalElInsts) = instrumenters.foldLeft((List[Expr](), List[Expr]())) {
- case ((thinsts, elinsts), menter) =>
- val inst = menter.inst
- val (thinst, elinst) = menter.instrumentIfThenElseExpr(ife,
- Some(condInsts(inst)), Some(thenInsts(inst)), Some(elseInsts(inst)))
- (thinsts :+ thinst, elinsts :+ elinst)
+ (recons, thInstPart)
+ }
+ val (nelseCons, elseInsts) = {
+ val reselse = Variable(FreshIdentifier("el", TupleType(elze.getType +: instTypes), true))
+ val elInstPart = insts.map { inst => (inst -> selectInst(reselse, inst)) }.toMap
+ val recons = (einsts: List[Expr]) => {
+ Let(reselse.id, transform(elze), Tuple(TupleSelect(reselse, 1) +: einsts))
}
- val nthen = nthenCons(finalThInsts)
- val nelse = nelseCons(finalElInsts)
- nifCons(nthen, nelse)
+ (recons, elInstPart)
}
+ val (finalThInsts, finalElInsts) = instrumenters.foldLeft((List[Expr](), List[Expr]())) {
+ case ((thinsts, elinsts), menter) =>
+ val inst = menter.inst
+ val (thinst, elinst) = menter.instrumentIfThenElseExpr(ife,
+ Some(condInsts(inst)), Some(thenInsts(inst)), Some(elseInsts(inst)))
+ (thinsts :+ thinst, elinsts :+ elinst)
+ }
+ val nthen = nthenCons(finalThInsts)
+ val nelse = nelseCons(finalElInsts)
+ nifCons(nthen, nelse)
+ }
- // For all other operations, we go through a common tupleifier.
- case n @ Operator(ss, recons) =>
- tupleify(e, ss, recons)
+ // For all other operations, we go through a common tupleifier.
+ case n @ Operator(ss, recons) =>
+ tupleify(e, ss, recons)
-/* case b @ BinaryOperator(s1, s2, recons) =>
+ /* case b @ BinaryOperator(s1, s2, recons) =>
tupleify(e, Seq(s1, s2), { case Seq(s1, s2) => recons(s1, s2) })
case u @ UnaryOperator(s, recons) =>
tupleify(e, Seq(s), { case Seq(s) => recons(s) })
*/
- case t: Terminal =>
- tupleify(e, Seq(), { case Seq() => t })
- }
-
- def apply(e: Expr): Expr = {
- // Apply transformations
- val newe =
- if (retainMatches) e
- else matchToIfThenElse(liftExprInMatch(e))
- val transformed = transform(newe)(Map())
- val bodyId = FreshIdentifier("bd", transformed.getType, true)
- val instExprs = instrumenters map { m =>
- m.instrumentBody(newe,
- selectInst(bodyId.toVariable, m.inst))
+ case t: Terminal =>
+ tupleify(e, Seq(), { case Seq() => t })
+ }
- }
- Let(bodyId, transformed,
- Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
+ def apply(e: Expr): Expr = {
+ // Apply transformations
+ val newe =
+ if (retainMatches) e
+ else matchToIfThenElse(liftExprInMatch(e))
+ val transformed = transform(newe)(Map())
+ val bodyId = FreshIdentifier("bd", transformed.getType, true)
+ val instExprs = instrumenters map { m =>
+ m.instrumentBody(newe,
+ selectInst(bodyId.toVariable, m.inst))
}
+ Let(bodyId, transformed,
+ Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
+ }
- def liftExprInMatch(ine: Expr): Expr = {
- def helper(e: Expr): Expr = {
- e match {
- case MatchExpr(strut, cases) => strut match {
- case t: Terminal => e
- case _ => {
- val freshid = FreshIdentifier("m", strut.getType, true)
- Let(freshid, strut, MatchExpr(freshid.toVariable, cases))
- }
+ def liftExprInMatch(ine: Expr): Expr = {
+ def helper(e: Expr): Expr = {
+ e match {
+ case MatchExpr(strut, cases) => strut match {
+ case t: Terminal => e
+ case _ => {
+ val freshid = FreshIdentifier("m", strut.getType, true)
+ Let(freshid, strut, MatchExpr(freshid.toVariable, cases))
}
- case _ => e
}
+ case _ => e
}
-
- if (retainMatches) helper(ine)
- else simplePostTransform(helper)(ine)
}
+
+ if (retainMatches) helper(ine)
+ else simplePostTransform(helper)(ine)
}
}
@@ -467,14 +473,13 @@ abstract class Instrumenter(program: Program, si: SerialInstrumenter) {
* by Expression Extractors.
* fd is the function containing the expression `e`
*/
- def instrument(e: Expr, subInsts: Seq[Expr], funInvResVar: Option[Variable] = None)
- (implicit fd: FunDef, letIdMap: Map[Identifier, Identifier]): Expr
+ def instrument(e: Expr, subInsts: Seq[Expr], funInvResVar: Option[Variable] = None)(implicit fd: FunDef, letIdMap: Map[Identifier, Identifier]): Expr
/**
* Instrument procedure specialized for if-then-else
*/
def instrumentIfThenElseExpr(e: IfExpr, condInst: Option[Expr],
- thenInst: Option[Expr], elzeInst: Option[Expr]): (Expr, Expr)
+ thenInst: Option[Expr], elzeInst: Option[Expr]): (Expr, Expr)
/**
* This function is expected to combine the cost of the scrutinee,
@@ -485,5 +490,5 @@ abstract class Instrumenter(program: Program, si: SerialInstrumenter) {
* matching across match statements and ifThenElse statements is consistent
*/
def instrumentMatchCase(me: MatchExpr, mc: MatchCase,
- caseExprCost: Expr, scrutineeCost: Expr): Expr
+ caseExprCost: Expr, scrutineeCost: Expr): Expr
}
\ No newline at end of file
diff --git a/testcases/lazy-datastructures/RealTimeQueue-transformed.scala b/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
index d416dacb0..f690cc86b 100644
--- a/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
+++ b/testcases/lazy-datastructures/RealTimeQueue-transformed.scala
@@ -1,12 +1,13 @@
//import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.collection._
+package leon
+import lang._
+import annotation._
+import collection._
object RealTimeQueue {
abstract class LList[T]
-
- def LList$isEmpty[T]($this : LList[T]): Boolean = {
+
+ def LList$isEmpty[T]($this: LList[T]): Boolean = {
$this match {
case SNil() =>
true
@@ -14,8 +15,8 @@ object RealTimeQueue {
false
}
}
-
- def LList$isCons[T]($this : LList[T]): Boolean = {
+
+ def LList$isCons[T]($this: LList[T]): Boolean = {
$this match {
case SCons(_, _) =>
true
@@ -23,8 +24,8 @@ object RealTimeQueue {
false
}
}
-
- def LList$size[T]($this : LList[T]): BigInt = {
+
+ def LList$size[T]($this: LList[T]): BigInt = {
$this match {
case SNil() =>
BigInt(0)
@@ -32,31 +33,30 @@ object RealTimeQueue {
BigInt(1) + ssize[T](t)
}
} ensuring {
- (x$1 : BigInt) => (x$1 >= BigInt(0))
+ (x$1: BigInt) => (x$1 >= BigInt(0))
}
-
- case class SCons[T](x : T, tail : LazyLList[T]) extends LList[T]
-
+
+ case class SCons[T](x: T, tail: LazyLList[T]) extends LList[T]
+
case class SNil[T]() extends LList[T]
-
+
// TODO: closures are not ADTs since two closures with same arguments are not necessarily equal but
// ADTs are equal. This creates a bit of problem in checking if a closure belongs to a set or not.
// However, currently we are assuming that such problems do not happen.
// A solution is to pass around a dummy id that is unique for each closure.
abstract class LazyLList[T]
-
- case class Rotate[T](f : LazyLList[T], r : List[T], a : LazyLList[T], res: LList[T]) extends LazyLList[T]
-
- case class Lazyarg[T](newa : LList[T]) extends LazyLList[T]
+ case class Rotate[T](f: LazyLList[T], r: List[T], a: LazyLList[T], res: LList[T]) extends LazyLList[T]
+
+ case class Lazyarg[T](newa: LList[T]) extends LazyLList[T]
- def ssize[T](l : LazyLList[T]): BigInt = {
+ def ssize[T](l: LazyLList[T]): BigInt = {
val clist = evalLazyLList[T](l, Set[LazyLList[T]]())._1
LList$size[T](clist)
- } ensuring(res => res >= 0)
+ } ensuring (res => res >= 0)
- def isConcrete[T](l : LazyLList[T], st : Set[LazyLList[T]]): Boolean = {
+ def isConcrete[T](l: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
Set[LazyLList[T]](l).subsetOf(st) && (evalLazyLList[T](l, st)._1 match {
case SCons(_, tail) =>
isConcrete[T](tail, st)
@@ -64,28 +64,20 @@ object RealTimeQueue {
true
}) || LList$isEmpty[T](evalLazyLList[T](l, st)._1)
}
-
- // an assertion: closures created by evaluating a closure will result in unevaluated closure
+
+ // an assertion: closures created by evaluating a closure will result in unevaluated closure
@library
- def lemmaLazy[T](l : LazyLList[T], st : Set[LazyLList[T]]) : Boolean = {
- Set[LazyLList[T]](l).subsetOf(st) || {
+ def lemmaLazy[T](l: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
+ Set[LazyLList[T]](l).subsetOf(st) || {
evalLazyLList[T](l, Set[LazyLList[T]]())._1 match {
- case SCons(_, tail) =>
- l != tail && !Set[LazyLList[T]](tail).subsetOf(st)
- case _ => true
+ case SCons(_, tail) =>
+ l != tail && !Set[LazyLList[T]](tail).subsetOf(st)
+ case _ => true
}
}
-// Set[LazyLList[T]](l).subsetOf(st) || {
-// val (nval, nst, _) = evalLazyLList[T](l, st)
-// nval match {
-// case SCons(_, tail) =>
-// !Set[LazyLList[T]](tail).subsetOf(nst)
-// case _ => true
-// }
-// }
} holds
-
- def firstUnevaluated[T](l : LazyLList[T], st : Set[LazyLList[T]]): LazyLList[T] = {
+
+ def firstUnevaluated[T](l: LazyLList[T], st: Set[LazyLList[T]]): LazyLList[T] = {
if (Set[LazyLList[T]](l).subsetOf(st)) {
evalLazyLList[T](l, st)._1 match {
case SCons(_, tail) =>
@@ -96,71 +88,70 @@ object RealTimeQueue {
} else {
l
}
- } ensuring(res => (!LList$isEmpty[T](evalLazyLList[T](res, st)._1) || isConcrete[T](l, st)) &&
- (LList$isEmpty[T](evalLazyLList[T](res, st)._1) || !Set[LazyLList[T]](res).subsetOf(st)) &&
- { val (nval, nst, _) = evalLazyLList[T](res, st)
- nval match {
- case SCons(_, tail) =>
- firstUnevaluated(l, nst) == tail
- case _ => true
- }
- } &&
- lemmaLazy(res, st)
- )
-
+ } ensuring (res => (!LList$isEmpty[T](evalLazyLList[T](res, st)._1) || isConcrete[T](l, st)) &&
+ (LList$isEmpty[T](evalLazyLList[T](res, st)._1) || !Set[LazyLList[T]](res).subsetOf(st)) &&
+ {
+ val (nval, nst, _) = evalLazyLList[T](res, st)
+ nval match {
+ case SCons(_, tail) =>
+ firstUnevaluated(l, nst) == tail
+ case _ => true
+ }
+ } &&
+ lemmaLazy(res, st))
+
@library
- def evalLazyLList[T](cl : LazyLList[T], st : Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = {
+ def evalLazyLList[T](cl: LazyLList[T], st: Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = {
cl match {
- case t : Rotate[T] =>
+ case t: Rotate[T] =>
val (rres, _, rtime) = rotate(t.f, t.r, t.a, st)
val tset = Set[LazyLList[T]](t)
- val tme =
- if(tset.subsetOf(st))
- BigInt(1)
- else // time of rotate
- rtime
+ val tme =
+ if (tset.subsetOf(st))
+ BigInt(1)
+ else // time of rotate
+ rtime
(rotate(t.f, t.r, t.a, Set[LazyLList[T]]())._1, st ++ tset, tme)
- case t : Lazyarg[T] =>
+ case t: Lazyarg[T] =>
(lazyarg(t.newa), st ++ Set[LazyLList[T]](t), BigInt(1))
}
- } ensuring(res => (cl match {
- case t : Rotate[T] =>
- LList$size(res._1) == ssize(t.f) + t.r.size + ssize(t.a) &&
- res._1 != SNil[T]() &&
- res._3 <= 4
- case _ => true
- })
- // &&
- // (res._1 match {
- // case SCons(_, tail) =>
- // Set[LazyLList[T]](cl).subsetOf(st) || !Set[LazyLList[T]](tail).subsetOf(res._2)
- // case _ => true
- // })
- )
-
+ } ensuring (res => (cl match {
+ case t: Rotate[T] =>
+ LList$size(res._1) == ssize(t.f) + t.r.size + ssize(t.a) &&
+ res._1 != SNil[T]() &&
+ res._3 <= 4
+ case _ => true
+ }) // &&
+ // (res._1 match {
+ // case SCons(_, tail) =>
+ // Set[LazyLList[T]](cl).subsetOf(st) || !Set[LazyLList[T]](tail).subsetOf(res._2)
+ // case _ => true
+ // })
+ )
+
@extern
- def rotate2[T](f : LazyLList[T], r : List[T], a : LazyLList[T], st : Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = ???
-
- def lazyarg[T](newa : LList[T]): LList[T] = {
+ def rotate2[T](f: LazyLList[T], r: List[T], a: LazyLList[T], st: Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = ???
+
+ def lazyarg[T](newa: LList[T]): LList[T] = {
newa
- }
-
- def streamScheduleProperty[T](s : LazyLList[T], sch : LazyLList[T], st : Set[LazyLList[T]]): Boolean = {
+ }
+
+ def streamScheduleProperty[T](s: LazyLList[T], sch: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
firstUnevaluated[T](s, st) == sch
}
-
- case class Queue[T](f : LazyLList[T], r : List[T], s : LazyLList[T])
-
- def Queue$isEmpty[T]($this : Queue[T], st : Set[LazyLList[T]]): Boolean = {
+
+ case class Queue[T](f: LazyLList[T], r: List[T], s: LazyLList[T])
+
+ def Queue$isEmpty[T]($this: Queue[T], st: Set[LazyLList[T]]): Boolean = {
LList$isEmpty[T](evalLazyLList[T]($this.f, st)._1)
}
-
- def Queue$valid[T]($this : Queue[T], st : Set[LazyLList[T]]): Boolean = {
- streamScheduleProperty[T]($this.f, $this.s, st) &&
+
+ def Queue$valid[T]($this: Queue[T], st: Set[LazyLList[T]]): Boolean = {
+ streamScheduleProperty[T]($this.f, $this.s, st) &&
ssize[T]($this.s) == ssize[T]($this.f) - $this.r.size
}
-
+
// things to prove:
// (a0) prove that pre implies post for 'rotate' (this depends on the assumption on eval)
// (a) Rotate closure creations satisfy the preconditions of 'rotate' (or)
@@ -172,66 +163,67 @@ object RealTimeQueue {
// Note: using both captured and calling context is possible but is more involved
// (c) Assume that 'eval' ensures the postcondition of 'rotate'
// (d) Moreover we can also assume that the preconditons of rotate hold whenever we use a closure
-
+
// proof of (a)
// (i) for stateless invariants this can be proven by treating lazy eager,
// so not doing this here
-
+
// monotonicity of isConcrete
- def lemmaConcreteMonotone[T](f : LazyLList[T], st1 : Set[LazyLList[T]], st2 : Set[LazyLList[T]]) : Boolean = {
+ def lemmaConcreteMonotone[T](f: LazyLList[T], st1: Set[LazyLList[T]], st2: Set[LazyLList[T]]): Boolean = {
(evalLazyLList[T](f, st1)._1 match {
case SCons(_, tail) =>
- lemmaConcreteMonotone(tail, st1, st2)
+ lemmaConcreteMonotone(tail, st1, st2)
case _ =>
true
- }) &&
+ }) &&
!(st1.subsetOf(st2) && isConcrete(f, st1)) || isConcrete(f, st2)
} holds
-
+
// proof that the precondition isConcrete(f, st) holds for closure creation in 'rotate' function
- def rotateClosureLemma1[T](f : LazyLList[T], st : Set[LazyLList[T]]): Boolean = {
- require(isConcrete(f, st))
+ def rotateClosureLemma1[T](f: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
+ require(isConcrete(f, st))
val dres = evalLazyLList[T](f, st);
- dres._1 match {
- case SCons(x, tail) =>
+ dres._1 match {
+ case SCons(x, tail) =>
isConcrete(tail, st)
case _ => true
}
} holds
-
+
// proof that the precondition isConcrete(f, st) holds for closure creation in 'createQueue' function
- def rotateClosureLemma2[T](f : LazyLList[T], sch : LazyLList[T], st : Set[LazyLList[T]]): Boolean = {
+ // @ important use and instantiate monotonicity of
+ def rotateClosureLemma2[T](f: LazyLList[T], sch: LazyLList[T], st: Set[LazyLList[T]]): Boolean = {
require(streamScheduleProperty[T](f, sch, st)) // && ssize[T](sch) == (ssize[T](f) - r.size) + BigInt(1))
val dres4 = evalLazyLList[T](sch, st);
- dres4._1 match {
+ dres4._1 match {
case SNil() =>
//isConcrete(f, dres4._2)
- isConcrete(f, st) // the above is implied by the monotonicity of 'isConcrete'
- case _ => true
- }
+ isConcrete(f, st) // the above is implied by the monotonicity of 'isConcrete'
+ case _ => true
+ }
} holds
-
+
// proof that the precondition isConcrete(f, st) holds for closure creation in 'dequeue' function
- def rotateClosureLemma3[T](q : Queue[T], st : Set[LazyLList[T]]): Boolean = {
- require(!Queue$isEmpty[T](q, st) && Queue$valid[T](q, st))
+ def rotateClosureLemma3[T](q: Queue[T], st: Set[LazyLList[T]]): Boolean = {
+ require(!Queue$isEmpty[T](q, st) && Queue$valid[T](q, st))
val dres7 = evalLazyLList[T](q.f, st);
- val SCons(x, nf) = dres7._1
+ val SCons(x, nf) = dres7._1
val dres8 = evalLazyLList[T](q.s, dres7._2);
- dres8._1 match {
+ dres8._1 match {
case SNil() =>
- isConcrete(nf, st)
- // the above would imply: isConcrete(nf, dres8._2) by monotonicity
+ isConcrete(nf, st)
+ // the above would imply: isConcrete(nf, dres8._2) by monotonicity
case _ => true
}
} holds
-
+
// part(c) assume postconditon of 'rotate' in closure invocation time and also
// the preconditions of 'rotate' if necesssary, and prove the properties of the
// methods that invoke closures
-
+
// proving specifications of 'rotate' (only state specifications are interesting)
- def rotate[T](f : LazyLList[T], r : List[T], a : LazyLList[T], st : Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = {
- require(r.size == ssize[T](f) + BigInt(1) && isConcrete(f, st))
+ def rotate[T](f: LazyLList[T], r: List[T], a: LazyLList[T], st: Set[LazyLList[T]]): (LList[T], Set[LazyLList[T]], BigInt) = {
+ require(r.size == ssize[T](f) + BigInt(1) && isConcrete(f, st))
val dres = evalLazyLList[T](f, st);
(dres._1, r) match {
case (SNil(), Cons(y, _)) =>
@@ -240,45 +232,44 @@ object RealTimeQueue {
val na = Lazyarg[T](SCons[T](y, a))
(SCons[T](x, Rotate[T](tail, r1, na, SNil[T]())), dres._2, dres._3 + 3)
}
- } ensuring(res => LList$size(res._1) == ssize(f) + r.size + ssize(a) &&
- res._1 != SNil[T]() &&
- res._3 <= 4)
-
-
+ } ensuring (res => LList$size(res._1) == ssize(f) + r.size + ssize(a) &&
+ res._1 != SNil[T]() &&
+ res._3 <= 4)
+
// a stub for creating new closure (ensures that the new closures do not belong to the old state)
// Note: this could result in inconsistency since we are associating unique ids with closures
@library
- def newclosure[T](rt: Rotate[T], st: Set[LazyLList[T]]) = {
+ def newclosure[T](rt: Rotate[T], st: Set[LazyLList[T]]) = {
(rt, st)
- } ensuring(res => !Set[LazyLList[T]](res._1).subsetOf(st))
-
+ } ensuring (res => !Set[LazyLList[T]](res._1).subsetOf(st))
+
// proving specifications of 'createQueue' (only state specifications are interesting)
- def createQueue[T](f : LazyLList[T], r : List[T], sch : LazyLList[T], st : Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
- require(streamScheduleProperty[T](f, sch, st) &&
+ def createQueue[T](f: LazyLList[T], r: List[T], sch: LazyLList[T], st: Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
+ require(streamScheduleProperty[T](f, sch, st) &&
ssize[T](sch) == (ssize[T](f) - r.size) + BigInt(1))
val dres4 = evalLazyLList[T](sch, st);
dres4._1 match {
case SCons(_, tail) =>
(Queue[T](f, r, tail), dres4._2, dres4._3 + 2)
- case SNil() =>
+ case SNil() =>
val rotres1 = newclosure(Rotate[T](f, r, Lazyarg[T](SNil[T]()), SNil[T]()), dres4._2); // can also directly call rotate here
(Queue[T](rotres1._1, List[T](), rotres1._1), dres4._2, dres4._3 + 3)
}
- } ensuring(res => Queue$valid[T](res._1, res._2) &&
- res._3 <= 7)
-
+ } ensuring (res => Queue$valid[T](res._1, res._2) &&
+ res._3 <= 7)
+
// proving specifications of 'enqueue'
- def enqueue[T](x : T, q : Queue[T], st : Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
+ def enqueue[T](x: T, q: Queue[T], st: Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
require(Queue$valid[T](q, st))
createQueue[T](q.f, Cons[T](x, q.r), q.s, st)
- } ensuring (res => Queue$valid[T](res._1, res._2) &&
- res._3 <= 7)
-
+ } ensuring (res => Queue$valid[T](res._1, res._2) &&
+ res._3 <= 7)
+
// proving specifications of 'dequeue'
- def dequeue[T](q : Queue[T], st : Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
- require(!Queue$isEmpty[T](q, st) && Queue$valid[T](q, st))
+ def dequeue[T](q: Queue[T], st: Set[LazyLList[T]]): (Queue[T], Set[LazyLList[T]], BigInt) = {
+ require(!Queue$isEmpty[T](q, st) && Queue$valid[T](q, st))
val dres7 = evalLazyLList[T](q.f, st);
- val SCons(x, nf) = dres7._1
+ val SCons(x, nf) = dres7._1
val dres8 = evalLazyLList[T](q.s, dres7._2);
dres8._1 match {
case SCons(_, nsch) =>
@@ -287,6 +278,6 @@ object RealTimeQueue {
val rotres3 = newclosure(Rotate[T](nf, q.r, Lazyarg[T](SNil[T]()), SNil[T]()), dres8._2);
(Queue[T](rotres3._1, List[T](), rotres3._1), dres8._2, dres7._3 + dres8._3 + 4)
}
- } ensuring(res => Queue$valid[T](res._1, res._2) &&
- res._3 <= 12)
+ } ensuring (res => Queue$valid[T](res._1, res._2) &&
+ res._3 <= 12)
}
diff --git a/testcases/lazy-datastructures/RealTimeQueue.scala b/testcases/lazy-datastructures/RealTimeQueue.scala
index a058163be..e3f4618cf 100644
--- a/testcases/lazy-datastructures/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/RealTimeQueue.scala
@@ -2,6 +2,7 @@ import leon.lazyeval._
import leon.lang._
import leon.annotation._
import leon.collection._
+import leon.instrumentation._
object RealTimeQueue {
@@ -9,20 +10,20 @@ object RealTimeQueue {
def isEmpty: Boolean = {
this match {
case SNil() => true
- case _ => false
+ case _ => false
}
}
def isCons: Boolean = {
this match {
case SCons(_, _) => true
- case _ => false
+ case _ => false
}
}
def size: BigInt = {
this match {
- case SNil() => BigInt(0)
+ case SNil() => BigInt(0)
case SCons(x, t) => 1 + ssize(t)
}
} ensuring (_ >= 0)
@@ -64,11 +65,10 @@ object RealTimeQueue {
((res*).isEmpty || !res.isEvaluated) && // if the return value is not a Nil closure then it would not have been evaluated
streamLemma(res) &&
(res.value match {
- case SCons(_, tail) =>
+ case SCons(_, tail) =>
firstUnevaluated(l) == tail // after evaluating the firstUnevaluated closure in 'l' we get the next unevaluated closure
case _ => true
- })
- )
+ }))
def streamScheduleProperty[T](s: $[LList[T]], sch: $[LList[T]]) = {
firstUnevaluated(s) == sch
@@ -82,9 +82,8 @@ object RealTimeQueue {
}
}
- //@lazyproc
def rotate[T](f: $[LList[T]], r: List[T], a: $[LList[T]]): LList[T] = {
- require(r.size == ssize(f) + 1) // isConcrete(f) // size invariant between 'f' and 'r' holds
+ require(r.size == ssize(f) + 1 && isConcrete(f)) // size invariant between 'f' and 'r' holds
(f.value, r) match {
case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
SCons[T](y, a)
@@ -93,13 +92,13 @@ object RealTimeQueue {
val rot = $(rotate(tail, r1, $(newa))) //this creates a lazy rotate operation
SCons[T](x, rot)
}
- } ensuring (res => res.size == ssize(f) + r.size + ssize(a) && res.isCons)
- //&& res._2 <= O(1) //time bound)
+ } ensuring (res => res.size == ssize(f) + r.size + ssize(a) && res.isCons &&
+ time <= 30)
// TODO: make newa into sch to avoid a different closure category
def createQueue[T](f: $[LList[T]], r: List[T], sch: $[LList[T]]): Queue[T] = {
require(streamScheduleProperty(f, sch) &&
- ssize(sch) == ssize(f) - r.size + 1) //size invariant holds
+ ssize(sch) == ssize(f) - r.size + 1) //size invariant holds
sch.value match { // evaluate the schedule if it is not evaluated
case SCons(_, tail) =>
Queue(f, r, tail)
@@ -108,12 +107,12 @@ object RealTimeQueue {
val rotres = $(rotate(f, r, $(newa)))
Queue(rotres, Nil[T](), rotres)
}
- } ensuring (res => res.valid)
+ } ensuring (res => res.valid && time <= 50)
def enqueue[T](x: T, q: Queue[T]): Queue[T] = {
require(q.valid)
createQueue(q.f, Cons[T](x, q.r), q.s)
- } ensuring (res => res.valid)
+ } ensuring (res => res.valid && time <= 60)
def dequeue[T](q: Queue[T]): Queue[T] = {
require(!q.isEmpty && q.valid)
@@ -128,6 +127,5 @@ object RealTimeQueue {
Queue(rotres, Nil[T](), rotres)
}
}
- } ensuring (res => res.valid)
+ } ensuring (res => time <= 120) //res.valid && )
}
-
\ No newline at end of file
--
GitLab