diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 78121f038e15d1844f15f9ff45cdd807b4660708..94c4adb7de4bcd01a344f4ee01dc5f892f53be09 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -25,4 +25,6 @@ package object annotation {
class axiom extends StaticAnnotation
@ignore
class invstate extends StaticAnnotation
+ @ignore
+ class memoize extends StaticAnnotation
}
\ No newline at end of file
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 71b49841f1c647c6cb851f529da76a1864037c5e..579e1803c770ba740f3c6d915ed6d9ca1579c558 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -57,6 +57,7 @@ object Main {
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the lazy construct", false)
+ //val optMemoize = LeonFlagOptionDef("memoize", "Handles programs that uses memoization", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval)
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 293aff0eab509d90bbccdcfd805d6aa11b1f0e6d..c8121446f28971e9e6a8ba5f63b52346fe941b53 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -57,20 +57,16 @@ object LazinessEliminationPhase extends TransformationPhase {
// options that control behavior
val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
- /**
- * TODO: enforce that the specs do not create lazy closures
- * TODO: we are forced to make an assumption that lazy ops takes as type parameters only those
- * type parameters of their return type and not more. (enforce this)
- * TODO: Check that lazy types are not nested
- * TODO: expose in/out state to the user level, so that they can be used in specs
- * For now using lazyinv annotation
- */
def apply(ctx: LeonContext, prog: Program): Program = {
if (dumpInputProg)
println("Input prog: \n" + ScalaPrinter.apply(prog))
+
+ val (pass, msg) = sanityChecks(prog, ctx)
+ assert(pass, msg)
+
val nprog = liftLazyExpressions(prog)
- if(dumpLiftProg) {
+ if (dumpLiftProg) {
prettyPrintProgramToFile(nprog, ctx, "-lifted")
}
@@ -116,6 +112,57 @@ object LazinessEliminationPhase extends TransformationPhase {
instProg
}
+ /**
+ * TODO: we are forced to make an assumption that lazy ops takes as type parameters only those
+ * type parameters of their return type and not more. (This is checked in the closureFactory,\
+ * but may be check this upfront)
+ */
+ def sanityChecks(p: Program, ctx: LeonContext): (Boolean, String) = {
+ // using a bit of a state here
+ var failMsg = ""
+ val checkres = p.definedFunctions.forall {
+ case fd if !fd.isLibrary =>
+ /**
+ * Fails when the argument to a suspension creation
+ * is either a normal or memoized function depending on the flag
+ * 'argMem' = true implies fail if the argument is a memoized function
+ */
+ def failOnClosures(argMem: Boolean, e: Expr) = e match {
+ case finv: FunctionInvocation if isLazyInvocation(finv)(p) =>
+ finv match {
+ case FunctionInvocation(_, Seq(FunctionInvocation(callee, _))) if isMemoized(callee.fd) => argMem
+ case _ => !argMem
+ }
+ case _ => false
+ }
+ // specs should not create lazy closures, but can refer to memoized functions
+ val specCheckFailed = exists(failOnClosures(false, _))(fd.precOrTrue) || exists(failOnClosures(false, _))(fd.postOrTrue)
+ if (specCheckFailed) {
+ failMsg = "Lazy closure creation in the specification of function: " + fd.id
+ false
+ } else {
+ // cannot suspend a memoized function
+ val bodyCheckFailed = exists(failOnClosures(true, _))(fd.body.getOrElse(Util.tru))
+ if (bodyCheckFailed) {
+ failMsg = "Suspending a memoized function is not supported! in body of: " + fd.id
+ false
+ } else {
+ def nestedSusp(e: Expr) = e match {
+ case finv @ FunctionInvocation(_, Seq(call: FunctionInvocation)) if isLazyInvocation(finv)(p) && isLazyInvocation(call)(p) => true
+ case _ => false
+ }
+ val nestedCheckFailed = exists(nestedSusp)(fd.body.getOrElse(Util.tru))
+ if (nestedCheckFailed) {
+ failMsg = "Nested suspension creation in the body: " + fd.id
+ false
+ } else true
+ }
+ }
+ case _ => true
+ }
+ (checkres, failMsg)
+ }
+
/**
* convert the argument of every lazy constructors to a procedure
*/
@@ -199,7 +246,7 @@ object LazinessEliminationPhase extends TransformationPhase {
val npost = pbody match {
case And(args) =>
createAnd(args.filterNot(hasInstVar))
- case l : Let => // checks if the body of the let can be deconstructed as And
+ case l: Let => // checks if the body of the let can be deconstructed as And
//println(s"Fist let val: ${l.value} body: ${l.body}")
val (letsCons, letsBody) = letStarUnapply(l)
//println("Let* body: "+letsBody)
@@ -218,7 +265,7 @@ object LazinessEliminationPhase extends TransformationPhase {
def contextForChecks(userOptions: LeonContext) = {
val solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre"))
LeonContext(userOptions.reporter, userOptions.interruptManager,
- solverOptions.options ++ userOptions.options)
+ solverOptions.options ++ userOptions.options)
}
def checkSpecifications(prog: Program, checkCtx: LeonContext) {
@@ -227,10 +274,10 @@ object LazinessEliminationPhase extends TransformationPhase {
if (fd.annotations.contains("axiom"))
fd.addFlag(Annotation("library", Seq()))
}
-// val functions = Seq() //Seq("--functions=rotate")
-// val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
-// val unfoldFactor = 3 ,
-// "--unfoldFactor="+unfoldFactor) ++ solverOptions ++ functions
+ // val functions = Seq() //Seq("--functions=rotate")
+ // val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
+ // val unfoldFactor = 3 ,
+ // "--unfoldFactor="+unfoldFactor) ++ solverOptions ++ functions
//val solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre")
val report = VerificationPhase.apply(checkCtx, prog)
println(report.summaryString)
@@ -244,23 +291,23 @@ object LazinessEliminationPhase extends TransformationPhase {
if (fd.annotations.contains("axiom"))
fd.addFlag(Annotation("library", Seq()))
}
-// val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
-// val ctx = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre") ++ solverOptions)
+ // val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
+ // val ctx = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre") ++ solverOptions)
//(a) create vcs
// Note: we only need to check specs involving instvars since others were checked before.
// Moreover, we can add other specs as assumptions since (A => B) ^ ((A ^ B) => C) => A => B ^ C
//checks if the expression uses res._2 which corresponds to instvars after instrumentation
def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
- exists(_ == TupleSelect(resid.toVariable, 2))(e)
+ exists(_ == TupleSelect(resid.toVariable, 2))(e)
val vcs = p.definedFunctions.collect {
// skipping verification of uninterpreted functions
case fd if !fd.isLibrary && InstUtil.isInstrumented(fd) && fd.hasBody &&
- fd.postcondition.exists{post =>
- val Lambda(Seq(resdef), pbody) = post
- accessesSecondRes(pbody, resdef.id)
- } =>
+ fd.postcondition.exists { post =>
+ val Lambda(Seq(resdef), pbody) = post
+ accessesSecondRes(pbody, resdef.id)
+ } =>
val Lambda(Seq(resdef), pbody) = fd.postcondition.get
val (instPost, assumptions) = pbody match {
case And(args) =>
@@ -272,16 +319,16 @@ object LazinessEliminationPhase extends TransformationPhase {
case And(args) =>
val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
(letsCons(createAnd(instSpecs)),
- letsCons(createAnd(rest)))
+ letsCons(createAnd(rest)))
case _ =>
(l, Util.tru)
}
case e => (e, Util.tru)
}
val vc = implies(createAnd(Seq(fd.precOrTrue, assumptions,
- Equals(resdef.id.toVariable, fd.body.get))), instPost)
- if(debugInstVCs)
- println(s"VC for function ${fd.id} : "+vc)
+ Equals(resdef.id.toVariable, fd.body.get))), instPost)
+ if (debugInstVCs)
+ println(s"VC for function ${fd.id} : " + vc)
VC(vc, fd, VCKinds.Postcondition)
}
//(b) create a verification context
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index fe56e5878f15b5a903ff4a08b7939155a228f6ba..7c6a3b45f413c346159dc88e779736e4ddfcc46b 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -28,6 +28,10 @@ import purescala.PrinterOptions
object LazinessUtil {
+ def isMemoized(fd: FunDef) = {
+ fd.flags.contains(Annotation("memoize", Seq()))
+ }
+
def prettyPrintProgramToFile(p: Program, ctx: LeonContext, suffix: String) {
val optOutputDirectory = new LeonOptionDef[String] {
val name = "o"
@@ -192,7 +196,7 @@ object LazinessUtil {
def isEvalFunction(fd: FunDef) = {
fd.id.name.startsWith("eval@")
}
-
+
def isStateParam(id: Identifier) = {
id.name.startsWith("st@")
}
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index 4d98dc89e1f82756ee9616a681206310523b7f86..91a33252161cad2187f75ab24086d039aa9c2aaf 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -34,7 +34,7 @@ class LazyClosureFactory(p: Program) {
implicit val prog = p
/**
* Create a mapping from types to the lazyops that may produce a value of that type
- * TODO: relax that requirement that type parameters of return type of a function
+ * TODO: relax the requirement that type parameters of return type of a function
* lazy evaluated should include all of its type parameters
*/
private val (tpeToADT, opToCaseClass) = {
diff --git a/testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala b/testcases/lazy-datastructures/memoization/FibonacciMemoized.scala
similarity index 100%
rename from testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala
rename to testcases/lazy-datastructures/memoization/FibonacciMemoized.scala