diff --git a/src/main/scala/leon/laziness/FreeVariableFactory.scala b/src/main/scala/leon/laziness/FreeVariableFactory.scala
index fe07ea8b9a2ed30b0c727a84342fc168c83018d9..9e93edb5e92e7d8b49a2dbab7346260867d1bc17 100644
--- a/src/main/scala/leon/laziness/FreeVariableFactory.scala
+++ b/src/main/scala/leon/laziness/FreeVariableFactory.scala
@@ -33,42 +33,50 @@ import invariant.util.ProgramUtil._
* All free variables are of type `FreeVar` which can be mapped
* to a required type by applying uninterpreted functions.
*/
-class FreeVariableFactory() {
+object FreeVariableFactory {
- val absClass = AbstractClassDef(FreshIdentifier("FreeVar@"), Seq(), None)
- val absType = AbstractClassType(absClass, Seq())
+ val fvClass = AbstractClassDef(FreshIdentifier("FreeVar@"), Seq(), None)
+ val fvType = AbstractClassType(fvClass, Seq())
val varCase = {
- val cdef = CaseClassDef(FreshIdentifier("Var@"), Seq(), Some(absType), false)
- cdef.setFields(Seq(ValDef(FreshIdentifier("fl", absType))))
- absClass.registerChild(cdef)
+ val cdef = CaseClassDef(FreshIdentifier("Var@"), Seq(), Some(fvType), false)
+ cdef.setFields(Seq(ValDef(FreshIdentifier("fl", fvType))))
+ fvClass.registerChild(cdef)
cdef
}
val nextCase = {
- val cdef = CaseClassDef(FreshIdentifier("NextVar@"), Seq(), Some(absType), false)
- cdef.setFields(Seq(ValDef(FreshIdentifier("fl", absType))))
- absClass.registerChild(cdef)
+ val cdef = CaseClassDef(FreshIdentifier("NextVar@"), Seq(), Some(fvType), false)
+ cdef.setFields(Seq(ValDef(FreshIdentifier("fl", fvType))))
+ fvClass.registerChild(cdef)
cdef
}
val nilCase = {
- val cdef = CaseClassDef(FreshIdentifier("NilVar@"), Seq(), Some(absType), false)
- absClass.registerChild(cdef)
+ val cdef = CaseClassDef(FreshIdentifier("NilVar@"), Seq(), Some(fvType), false)
+ fvClass.registerChild(cdef)
cdef
}
class FreeVarListIterator(initRef: Variable) {
- require(initRef.getType == absType)
+ require(initRef.getType == fvType)
var refExpr : Expr = initRef
def current = CaseClass(varCase.typed, Seq(refExpr)) // Var(refExpr)
def next {
refExpr = CaseClass(nextCase.typed, Seq(refExpr)) // Next(refExpr)
}
+ // returns the current expressions and increments state
+ def nextExpr = {
+ val e = current
+ next
+ e
+ }
}
+ def getFreeListIterator(initRef: Variable) = new FreeVarListIterator(initRef)
+
var uifuns = Map[TypeTree, FunDef]()
def getOrCreateUF(t: TypeTree) = {
uifuns.getOrElse(t, {
val funName = "uop@" + TypeUtil.typeNameWOParams(t)
- val param = ValDef(FreshIdentifier("a", absType))
+ val param = ValDef(FreshIdentifier("a", fvType))
val tparams = TypeUtil.getTypeParameters(t) map TypeParameterDef.apply _
val uop = new FunDef(FreshIdentifier(funName), tparams, Seq(param), t)
uifuns += (t -> uop)
@@ -80,8 +88,9 @@ class FreeVariableFactory() {
val flIter = new FreeVarListIterator(initRef)
/**
- * Free variables are not guaranteed to be unique.
- * They are operations over unique references.
+ * Free operations are not guaranteed to be unique: They are
+ * uninterpreted functions of the form: f(ref).
+ * f(res_1) could be equal to f(res_2).
*/
def nextFV(t: TypeTree) = {
val uop = getOrCreateUF(t)
@@ -102,7 +111,7 @@ class FreeVariableFactory() {
def getFreeVarGenerator(initRef: Variable) = new FreeVariableGenerator(initRef)
- def createdClasses = Seq(absClass, varCase, nextCase, nilCase)
+ def fvClasses = Seq(fvClass, varCase, nextCase, nilCase)
- def createdFunctions = uifuns.keys.toSeq
+ def fvFunctions = uifuns.keys.toSeq
}
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index d20a741385d22f4111948b68fd278cbb646ebb75..867ba31ab448e8648ae4cfa69fc1aa97ec84fa8c 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -36,14 +36,14 @@ import purescala.Constructors._
import leon.verification._
import PredicateUtil._
import leon.invariant.engine._
-
+import LazyVerificationPhase._
/**
* TODO: Function names are assumed to be small case. Fix this!!
*/
object LazinessEliminationPhase extends TransformationPhase {
val debugLifting = false
val dumpInputProg = false
- val dumpLiftProg = false
+ val dumpLiftProg = true
val dumpProgramWithClosures = true
val dumpTypeCorrectProg = false
val dumpProgWithPreAsserts = true
@@ -52,7 +52,6 @@ object LazinessEliminationPhase extends TransformationPhase {
val debugSolvers = false
val skipStateVerification = false
val skipResourceVerification = false
- val debugInstVCs = false
val name = "Laziness Elimination Phase"
val description = "Coverts a program that uses lazy construct" +
@@ -62,7 +61,7 @@ object LazinessEliminationPhase extends TransformationPhase {
val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
val optUseOrb = LeonFlagOptionDef("useOrb", "Use Orb to infer constants", false)
- override val definedOptions: Set[LeonOptionDef[Any]] = Set(optUseOrb)
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optUseOrb, optRefEquality)
/**
* TODO: add inlining annotations for optimization.
@@ -75,7 +74,8 @@ object LazinessEliminationPhase extends TransformationPhase {
val (pass, msg) = sanityChecks(prog, ctx)
assert(pass, msg)
- val nprog = liftLazyExpressions(prog)
+ // refEq is by default false
+ val nprog = LazyExpressionLifter.liftLazyExpressions(prog, ctx.findOption(optRefEquality).getOrElse(false))
if (dumpLiftProg) {
prettyPrintProgramToFile(nprog, ctx, "-lifted")
}
@@ -184,379 +184,4 @@ object LazinessEliminationPhase extends TransformationPhase {
}
(checkres, failMsg)
}
-
- /**
- * convert the argument of every lazy constructors to a procedure
- */
- var globalId = 0
- def freshFunctionNameForArg = {
- globalId += 1
- "lazyarg" + globalId
- }
-
- /**
- * (a) The functions lifts arguments of '$' to functions
- * (b) lifts eager computations to lazy computations if necessary
- * (c) converts memoization to lazy evaluation
- */
- def liftLazyExpressions(prog: Program): Program = {
- var newfuns = Map[ExprStructure, (FunDef, ModuleDef)]()
- val fdmap = prog.definedFunctions.collect {
- case fd if !fd.isLibrary =>
- val nfd = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.params, fd.returnType)
- fd.flags.foreach(nfd.addFlag(_))
- (fd -> nfd)
- }.toMap
-
- lazy val lazyFun = ProgramUtil.functionByFullName("leon.lazyeval.$.apply", prog).get
- lazy val valueFun = ProgramUtil.functionByFullName("leon.lazyeval.$.value", prog).get
-
- prog.modules.foreach { md =>
- def exprLifter(inmem: Boolean)(expr: Expr) = expr match {
- // is the arugment of lazy invocation not a function ?
- case finv @ FunctionInvocation(lazytfd, Seq(arg)) if isLazyInvocation(finv)(prog) && !arg.isInstanceOf[FunctionInvocation] =>
- val freevars = variablesOf(arg).toList
- val tparams = freevars.map(_.getType).flatMap(getTypeParameters).distinct
- val argstruc = new ExprStructure(arg)
- val argfun =
- if (newfuns.contains(argstruc)) {
- newfuns(argstruc)._1
- } else {
- //construct type parameters for the function
- // note: we should make the base type of arg as the return type
- val nfun = new FunDef(FreshIdentifier(freshFunctionNameForArg, Untyped, true), tparams map TypeParameterDef.apply,
- freevars.map(ValDef(_)), bestRealType(arg.getType))
- nfun.body = Some(arg)
- newfuns += (argstruc -> (nfun, md))
- nfun
- }
- FunctionInvocation(lazytfd, Seq(FunctionInvocation(TypedFunDef(argfun, tparams),
- freevars.map(_.toVariable))))
-
- // is the argument of eager invocation not a variable ?
- case finv @ FunctionInvocation(TypedFunDef(fd, _), Seq(arg)) if isEagerInvocation(finv)(prog) && !arg.isInstanceOf[Variable] =>
- val rootType = bestRealType(arg.getType)
- val freshid = FreshIdentifier("t", rootType)
- Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, Seq(rootType)), Seq(freshid.toVariable)))
-
- case FunctionInvocation(TypedFunDef(fd, targs), args) if isMemoized(fd) && !inmem =>
- // calling a memoized function is modeled as creating a lazy closure and forcing it
- val tfd = TypedFunDef(fdmap.getOrElse(fd, fd), targs)
- val finv = FunctionInvocation(tfd, args)
- // enclose the call within the $ and force it
- val susp = FunctionInvocation(TypedFunDef(lazyFun, Seq(tfd.returnType)), Seq(finv))
- FunctionInvocation(TypedFunDef(valueFun, Seq(tfd.returnType)), Seq(susp))
-
- case FunctionInvocation(TypedFunDef(fd, targs), args) if fdmap.contains(fd) =>
- FunctionInvocation(TypedFunDef(fdmap(fd), targs), args)
- case e => e
- }
- md.definedFunctions.foreach {
- case fd if fd.hasBody && !fd.isLibrary =>
- def rec(inmem: Boolean)(e: Expr): Expr = e match {
- case Operator(args, op) =>
- val nargs = args map rec(inmem || isMemCons(e)(prog))
- exprLifter(inmem)(op(nargs))
- }
- val nfd = fdmap(fd)
- nfd.fullBody = rec(false)(fd.fullBody)
- /*val nbody = simplePostTransform(exprLifter(false))(fd.body.get)
- val npre = fd.precondition.map(simplePostTransform(exprLifter(true)))
- val npost = fd.postcondition.map(simplePostTransform(exprLifter(true)))*/
- //println(s"New body of $fd: $nbody")
- /*nfd.body = Some(nbody)
- nfd.precondition = npre
- nfd.postcondition = npost*/
- case _ => ;
- }
- }
- val repProg = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
- case fd: FunDef => fdmap.getOrElse(fd, fd)
- case d => d
- })
- val nprog =
- if (!newfuns.isEmpty) {
- val modToNewDefs = newfuns.values.groupBy(_._2).map { case (k, v) => (k, v.map(_._1)) }.toMap
- appendDefsToModules(repProg, modToNewDefs)
- } else
- repProg
- if (debugLifting)
- println("After lifiting arguments of lazy constructors: \n" + ScalaPrinter.apply(nprog))
- nprog
- }
-
- def removeInstrumentationSpecs(p: Program): Program = {
- def hasInstVar(e: Expr) = {
- exists { e => InstUtil.InstTypes.exists(i => i.isInstVariable(e)) }(e)
- }
- val newPosts = p.definedFunctions.collect {
- case fd if fd.postcondition.exists { exists(hasInstVar) } =>
- // remove the conjuncts that use instrumentation vars
- val Lambda(resdef, pbody) = fd.postcondition.get
- 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
- //println(s"Fist let val: ${l.value} body: ${l.body}")
- val (letsCons, letsBody) = letStarUnapply(l)
- //println("Let* body: "+letsBody)
- letsBody match {
- case And(args) =>
- letsCons(createAnd(args.filterNot(hasInstVar)))
- case _ => Util.tru
- }
- case e => Util.tru
- }
- (fd -> Lambda(resdef, npost))
- }.toMap
- ProgramUtil.updatePost(newPosts, p) //note: this will not update libraries
- }
-
- def contextForChecks(userOptions: LeonContext) = {
- val solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre"))
- LeonContext(userOptions.reporter, userOptions.interruptManager,
- solverOptions.options ++ userOptions.options)
- }
-
- // cumulative stats
- var totalTime = 0L
- var totalVCs = 0
- var solvedWithZ3 = 0
- var solvedWithCVC4 = 0
- var z3Time = 0L
- var cvc4Time = 0L
-
- def collectCumulativeStats(rep: VerificationReport) {
- totalTime += rep.totalTime
- totalVCs += rep.totalConditions
- val (withz3, withcvc) = rep.vrs.partition{
- case (vc, vr) =>
- vr.solvedWith.map(s => s.name.contains("smt-z3")).get
- }
- solvedWithZ3 += withz3.size
- solvedWithCVC4 += withcvc.size
- z3Time += withz3.map(_._2.timeMs.getOrElse(0L)).sum
- cvc4Time += withcvc.map(_._2.timeMs.getOrElse(0L)).sum
- }
-
- def dumpStats() {
- println("totalTime: "+f"${totalTime/1000d}%-3.3f")
- println("totalVCs: "+totalVCs)
- println("solvedWithZ3: "+ solvedWithZ3)
- println("solvedWithCVC4: "+ solvedWithCVC4)
- println("z3Time: "+f"${z3Time/1000d}%-3.3f")
- println("cvc4Time: "+f"${cvc4Time/1000d}%-3.3f")
- }
-
- def checkSpecifications(prog: Program, checkCtx: LeonContext) {
- // convert 'axiom annotation to library
- prog.definedFunctions.foreach { fd =>
- 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 solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre")
- val report = VerificationPhase.apply(checkCtx, prog)
- // collect stats
- collectCumulativeStats(report)
- println(report.summaryString)
- /*ctx.reporter.whenDebug(leon.utils.DebugSectionTimers) { debug =>
- ctx.timers.outputTable(debug)
- }*/
- }
-
- def checkInstrumentationSpecs(p: Program, checkCtx: LeonContext) = {
- p.definedFunctions.foreach { fd =>
- if (fd.annotations.contains("axiom"))
- fd.addFlag(Annotation("library", Seq()))
- }
- val funsToCheck = p.definedFunctions.filter(shouldGenerateVC)
- if (checkCtx.findOption(optUseOrb).getOrElse(false)) {
- // create an inference context
- val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds"))
- val ctxForInf = LeonContext(checkCtx.reporter, checkCtx.interruptManager,
- inferOpts.options ++ checkCtx.options)
- val inferctx = new InferenceContext(p, ctxForInf)
- val vcSolver = (funDef: FunDef, prog: Program) => new VCSolver(inferctx, prog, funDef)
- prettyPrintProgramToFile(inferctx.inferProgram, checkCtx, "-inferProg", true)
- (new InferenceEngine(inferctx)).analyseProgram(inferctx.inferProgram, funsToCheck, vcSolver, None)
- } else {
- val vcs = funsToCheck.map { fd =>
- val (ants, post, tmpl) = createVC(fd)
- if (tmpl.isDefined)
- throw new IllegalStateException("Postcondition has holes! Run with --useOrb option")
- val vc = implies(ants, post)
- if (debugInstVCs)
- println(s"VC for function ${fd.id} : " + vc)
- VC(vc, fd, VCKinds.Postcondition)
- }
- val rep = checkVCs(vcs, checkCtx, p)
- // record some stats
- collectCumulativeStats(rep)
- println("Resource Verification Results: \n" + rep.summaryString)
- }
- }
-
- def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
- exists(_ == TupleSelect(resid.toVariable, 2))(e)
-
- /**
- * Note: we also skip verification of uninterpreted functions
- */
- def shouldGenerateVC(fd: FunDef) = {
- !fd.isLibrary && InstUtil.isInstrumented(fd) && fd.hasBody &&
- fd.postcondition.exists { post =>
- val Lambda(Seq(resdef), pbody) = post
- accessesSecondRes(pbody, resdef.id)
- }
- }
-
- /**
- * creates 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 createVC(fd: FunDef) = {
- val Lambda(Seq(resdef), _) = fd.postcondition.get
- val (pbody, tmpl) = (fd.getPostWoTemplate, fd.template)
- val (instPost, assumptions) = pbody match {
- case And(args) =>
- val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
- (createAnd(instSpecs), createAnd(rest))
- case l: Let =>
- val (letsCons, letsBody) = letStarUnapply(l)
- letsBody match {
- case And(args) =>
- val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
- (letsCons(createAnd(instSpecs)),
- letsCons(createAnd(rest)))
- case _ =>
- (l, Util.tru)
- }
- case e => (e, Util.tru)
- }
- val ants = createAnd(Seq(fd.precOrTrue, assumptions, Equals(resdef.id.toVariable, fd.body.get)))
- (ants, instPost, tmpl)
- }
-
- def checkVCs(vcs: List[VC], checkCtx: LeonContext, p: Program) = {
- val timeout: Option[Long] = None
- val reporter = checkCtx.reporter
- // Solvers selection and validation
- val baseSolverF = SolverFactory.getFromSettings(checkCtx, p)
- val solverF = timeout match {
- case Some(sec) =>
- baseSolverF.withTimeout(sec / 1000)
- case None =>
- baseSolverF
- }
- val vctx = VerificationContext(checkCtx, p, solverF, reporter)
- try {
- VerificationPhase.checkVCs(vctx, vcs)
- //println("Resource Verification Results: \n" + veriRep.summaryString)
- } finally {
- solverF.shutdown()
- }
- }
-
- class VCSolver(ctx: InferenceContext, p: Program, rootFd: FunDef) extends
- UnfoldingTemplateSolver(ctx, p, rootFd) {
- override def constructVC(fd: FunDef): (Expr, Expr) = {
- val (ants, post, tmpl) = createVC(fd)
- val conseq = matchToIfThenElse(createAnd(Seq(post, tmpl.getOrElse(Util.tru))))
- (matchToIfThenElse(ants), conseq)
- }
-
- /**
- * TODO: fix this!!
- */
- override def verifyInvariant(newposts: Map[FunDef, Expr]) = (Some(false), Model.empty)
- }
-
- /**
- * NOT USED CURRENTLY
- * Lift the specifications on functions to the invariants corresponding
- * case classes.
- * Ideally we should class invariants here, but it is not currently supported
- * so we create a functions that can be assume in the pre and post of functions.
- * TODO: can this be optimized
- */
- /* def liftSpecsToClosures(opToAdt: Map[FunDef, CaseClassDef]) = {
- val invariants = opToAdt.collect {
- case (fd, ccd) if fd.hasPrecondition =>
- val transFun = (args: Seq[Identifier]) => {
- val argmap: Map[Expr, Expr] = (fd.params.map(_.id.toVariable) zip args.map(_.toVariable)).toMap
- replace(argmap, fd.precondition.get)
- }
- (ccd -> transFun)
- }.toMap
- val absTypes = opToAdt.values.collect {
- case cd if cd.parent.isDefined => cd.parent.get.classDef
- }
- val invFuns = absTypes.collect {
- case abs if abs.knownCCDescendents.exists(invariants.contains) =>
- val absType = AbstractClassType(abs, abs.tparams.map(_.tp))
- val param = ValDef(FreshIdentifier("$this", absType))
- val tparams = abs.tparams
- val invfun = new FunDef(FreshIdentifier(abs.id.name + "$Inv", Untyped),
- tparams, BooleanType, Seq(param))
- (abs -> invfun)
- }.toMap
- // assign bodies for the 'invfuns'
- invFuns.foreach {
- case (abs, fd) =>
- val bodyCases = abs.knownCCDescendents.collect {
- case ccd if invariants.contains(ccd) =>
- val ctype = CaseClassType(ccd, fd.tparams.map(_.tp))
- val cvar = FreshIdentifier("t", ctype)
- val fldids = ctype.fields.map {
- case ValDef(fid, Some(fldtpe)) =>
- FreshIdentifier(fid.name, fldtpe)
- }
- val pattern = CaseClassPattern(Some(cvar), ctype,
- fldids.map(fid => WildcardPattern(Some(fid))))
- val rhsInv = invariants(ccd)(fldids)
- // assert the validity of substructures
- val rhsValids = fldids.flatMap {
- case fid if fid.getType.isInstanceOf[ClassType] =>
- val t = fid.getType.asInstanceOf[ClassType]
- val rootDef = t match {
- case absT: AbstractClassType => absT.classDef
- case _ if t.parent.isDefined =>
- t.parent.get.classDef
- }
- if (invFuns.contains(rootDef)) {
- List(FunctionInvocation(TypedFunDef(invFuns(rootDef), t.tps),
- Seq(fid.toVariable)))
- } else
- List()
- case _ => List()
- }
- val rhs = Util.createAnd(rhsInv +: rhsValids)
- MatchCase(pattern, None, rhs)
- }
- // create a default case
- val defCase = MatchCase(WildcardPattern(None), None, Util.tru)
- val matchExpr = MatchExpr(fd.params.head.id.toVariable, bodyCases :+ defCase)
- fd.body = Some(matchExpr)
- }
- invFuns
- }*/
- // Expressions for testing solvers
- // a test expression
- /*val tparam =
- val dummyFunDef = new FunDef(FreshIdentifier("i"),Seq(), Seq(), IntegerType)
- val eq = Equals(FunctionInvocation(TypedFunDef(dummyFunDef, Seq()), Seq()), InfiniteIntegerLiteral(0))
- import solvers._
- val solver = SimpleSolverAPI(SolverFactory(() => new solvers.smtlib.SMTLIBCVC4Solver(ctx, prog)))
- solver.solveSAT(eq) match {
- case (Some(true), m) =>
- println("Model: "+m.toMap)
- case _ => println("Formula is unsat")
- }
- System.exit(0)*/
}
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index c587a330283e3899edb77937ff729420c6be3803..365babd1b91326356e15d1f591ea5358e4cc999f 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -46,9 +46,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val funsNeedStates = funsManager.funsNeedStates
val funsRetStates = funsManager.funsRetStates
- val consCallers = funsManager.callersOfLazyCons // transitive constructors of closures
val starCallers = funsManager.funsNeedStateTps
- val fvFactory = new FreeVariableFactory()
val lazyTnames = closureFactory.lazyTypeNames
val lazyops = closureFactory.lazyops
diff --git a/src/main/scala/leon/laziness/LazyExpressionLifter.scala b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9cdceceb76a69f473263cc544f36c8b5fff47fff
--- /dev/null
+++ b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
@@ -0,0 +1,263 @@
+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 purescala.TypeOps._
+import leon.invariant.util.TypeUtil._
+import leon.invariant.util.LetTupleSimplification._
+import leon.verification.VerificationPhase
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+import scala.util.matching.Regex
+import leon.purescala.PrettyPrinter
+import leon.solvers._
+import leon.solvers.z3._
+import leon.transformations._
+import leon.LeonContext
+import leon.LeonOptionDef
+import leon.Main
+import leon.TransformationPhase
+import LazinessUtil._
+import invariant.datastructure._
+import invariant.util.ProgramUtil._
+import purescala.Constructors._
+import leon.verification._
+import PredicateUtil._
+import leon.invariant.engine._
+import FreeVariableFactory._
+
+object LazyExpressionLifter {
+
+ /**
+ * convert the argument of every lazy constructors to a procedure
+ */
+ var globalId = 0
+ def freshFunctionNameForArg = {
+ globalId += 1
+ "lazyarg" + globalId
+ }
+
+ /**
+ * (a) The functions lifts arguments of '$' to functions
+ * (b) lifts eager computations to lazy computations if necessary
+ * (c) converts memoization to lazy evaluation
+ * (d) Adds unique references to programs that create lazy closures.
+ */
+ def liftLazyExpressions(prog: Program, createUniqueIds: Boolean = false): Program = {
+
+ lazy val funsMan = new LazyFunctionsManager(prog)
+ lazy val needsId = funsMan.callersnTargetOfLazyCons
+
+ var newfuns = Map[ExprStructure, (FunDef, ModuleDef)]()
+ val fdmap = prog.definedFunctions.collect {
+ case fd if !fd.isLibrary =>
+ val nname = FreshIdentifier(fd.id.name)
+ val nfd =
+ if (createUniqueIds && needsId(fd)) {
+ val idparam = ValDef(FreshIdentifier("id@", fvType))
+ new FunDef(nname, fd.tparams, fd.params :+ idparam, fd.returnType)
+ } else
+ new FunDef(nname, fd.tparams, fd.params, fd.returnType)
+ fd.flags.foreach(nfd.addFlag(_))
+ (fd -> nfd)
+ }.toMap
+
+ lazy val lazyFun = ProgramUtil.functionByFullName("leon.lazyeval.$.apply", prog).get
+ lazy val valueFun = ProgramUtil.functionByFullName("leon.lazyeval.$.value", prog).get
+
+ var anchorDef: Option[FunDef] = None // a hack to find anchors
+ prog.modules.foreach { md =>
+ def exprLifter(inmem: Boolean)(fl: Option[FreeVarListIterator])(expr: Expr) = expr match {
+ // is this $(e) where e is not a funtion
+ case finv @ FunctionInvocation(lazytfd, Seq(arg)) if isLazyInvocation(finv)(prog) =>
+ arg match {
+ case _: FunctionInvocation =>
+ finv // subexpressions have already been evaluated
+ case _ =>
+ val freevars = variablesOf(arg).toList
+ val tparams = freevars.map(_.getType).flatMap(getTypeParameters).distinct
+ val argstruc = new ExprStructure(arg)
+ val argfun =
+ if (newfuns.contains(argstruc)) {
+ newfuns(argstruc)._1
+ } else {
+ //construct type parameters for the function
+ // note: we should make the base type of arg as the return type
+ val nname = FreshIdentifier(freshFunctionNameForArg, Untyped, true)
+ val tparamDefs = tparams map TypeParameterDef.apply
+ val params = freevars.map(ValDef(_))
+ val retType = bestRealType(arg.getType)
+ val nfun =
+ if (createUniqueIds) {
+ val idparam = ValDef(FreshIdentifier("id@", fvType))
+ new FunDef(nname, tparamDefs, params :+ idparam, retType)
+ } else
+ new FunDef(nname, tparamDefs, params, retType)
+ nfun.body = Some(arg)
+ newfuns += (argstruc -> (nfun, md))
+ nfun
+ }
+ val fvVars = freevars.map(_.toVariable)
+ val params =
+ if (createUniqueIds)
+ fvVars :+ fl.get.nextExpr
+ else fvVars
+ FunctionInvocation(lazytfd, Seq(FunctionInvocation(TypedFunDef(argfun, tparams), params)))
+ }
+
+ // is the argument of eager invocation not a variable ?
+ case finv @ FunctionInvocation(TypedFunDef(fd, _), Seq(arg)) if isEagerInvocation(finv)(prog) && !arg.isInstanceOf[Variable] =>
+ val rootType = bestRealType(arg.getType)
+ val freshid = FreshIdentifier("t", rootType)
+ Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, Seq(rootType)), Seq(freshid.toVariable)))
+
+ // is this an invocation of a memoized function ?
+ case FunctionInvocation(TypedFunDef(fd, targs), args) if isMemoized(fd) && !inmem =>
+ // calling a memoized function is modeled as creating a lazy closure and forcing it
+ val tfd = TypedFunDef(fdmap.getOrElse(fd, fd), targs)
+ val finv = FunctionInvocation(tfd, args)
+ // enclose the call within the $ and force it
+ val susp = FunctionInvocation(TypedFunDef(lazyFun, Seq(tfd.returnType)), Seq(finv))
+ FunctionInvocation(TypedFunDef(valueFun, Seq(tfd.returnType)), Seq(susp))
+
+ // every other function calls ?
+ case FunctionInvocation(TypedFunDef(fd, targs), args) if fdmap.contains(fd) =>
+ val nargs =
+ if (createUniqueIds && needsId(fd))
+ args :+ fl.get.nextExpr
+ else args
+ FunctionInvocation(TypedFunDef(fdmap(fd), targs), nargs)
+
+ case e => e
+ }
+ md.definedFunctions.foreach {
+ case fd if fd.hasBody && !fd.isLibrary =>
+ // create a free list iterator
+ val nfd = fdmap(fd)
+ val fliter =
+ if (createUniqueIds && needsId(fd)) {
+ if (!anchorDef.isDefined)
+ anchorDef = Some(nfd)
+ val initRef = nfd.params.last.id.toVariable
+ Some(getFreeListIterator(initRef))
+ } else
+ None
+
+ def rec(inmem: Boolean)(e: Expr): Expr = e match {
+ case Operator(args, op) =>
+ val nargs = args map rec(inmem || isMemCons(e)(prog))
+ exprLifter(inmem)(fliter)(op(nargs))
+ }
+ nfd.fullBody = rec(false)(fd.fullBody)
+ case _ => ;
+ }
+ }
+ val progWithFuns = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
+ case fd: FunDef => fdmap.getOrElse(fd, fd)
+ case d => d
+ })
+ val progWithClasses =
+ if (createUniqueIds) addDefs(progWithFuns, fvClasses, anchorDef.get)
+ else progWithFuns
+ if (!newfuns.isEmpty) {
+ val modToNewDefs = newfuns.values.groupBy(_._2).map { case (k, v) => (k, v.map(_._1)) }.toMap
+ appendDefsToModules(progWithClasses, modToNewDefs)
+ } else
+ progWithClasses
+ }
+
+ /**
+ * NOT USED CURRENTLY
+ * Lift the specifications on functions to the invariants corresponding
+ * case classes.
+ * Ideally we should class invariants here, but it is not currently supported
+ * so we create a functions that can be assume in the pre and post of functions.
+ * TODO: can this be optimized
+ */
+ /* def liftSpecsToClosures(opToAdt: Map[FunDef, CaseClassDef]) = {
+ val invariants = opToAdt.collect {
+ case (fd, ccd) if fd.hasPrecondition =>
+ val transFun = (args: Seq[Identifier]) => {
+ val argmap: Map[Expr, Expr] = (fd.params.map(_.id.toVariable) zip args.map(_.toVariable)).toMap
+ replace(argmap, fd.precondition.get)
+ }
+ (ccd -> transFun)
+ }.toMap
+ val absTypes = opToAdt.values.collect {
+ case cd if cd.parent.isDefined => cd.parent.get.classDef
+ }
+ val invFuns = absTypes.collect {
+ case abs if abs.knownCCDescendents.exists(invariants.contains) =>
+ val absType = AbstractClassType(abs, abs.tparams.map(_.tp))
+ val param = ValDef(FreshIdentifier("$this", absType))
+ val tparams = abs.tparams
+ val invfun = new FunDef(FreshIdentifier(abs.id.name + "$Inv", Untyped),
+ tparams, BooleanType, Seq(param))
+ (abs -> invfun)
+ }.toMap
+ // assign bodies for the 'invfuns'
+ invFuns.foreach {
+ case (abs, fd) =>
+ val bodyCases = abs.knownCCDescendents.collect {
+ case ccd if invariants.contains(ccd) =>
+ val ctype = CaseClassType(ccd, fd.tparams.map(_.tp))
+ val cvar = FreshIdentifier("t", ctype)
+ val fldids = ctype.fields.map {
+ case ValDef(fid, Some(fldtpe)) =>
+ FreshIdentifier(fid.name, fldtpe)
+ }
+ val pattern = CaseClassPattern(Some(cvar), ctype,
+ fldids.map(fid => WildcardPattern(Some(fid))))
+ val rhsInv = invariants(ccd)(fldids)
+ // assert the validity of substructures
+ val rhsValids = fldids.flatMap {
+ case fid if fid.getType.isInstanceOf[ClassType] =>
+ val t = fid.getType.asInstanceOf[ClassType]
+ val rootDef = t match {
+ case absT: AbstractClassType => absT.classDef
+ case _ if t.parent.isDefined =>
+ t.parent.get.classDef
+ }
+ if (invFuns.contains(rootDef)) {
+ List(FunctionInvocation(TypedFunDef(invFuns(rootDef), t.tps),
+ Seq(fid.toVariable)))
+ } else
+ List()
+ case _ => List()
+ }
+ val rhs = Util.createAnd(rhsInv +: rhsValids)
+ MatchCase(pattern, None, rhs)
+ }
+ // create a default case
+ val defCase = MatchCase(WildcardPattern(None), None, Util.tru)
+ val matchExpr = MatchExpr(fd.params.head.id.toVariable, bodyCases :+ defCase)
+ fd.body = Some(matchExpr)
+ }
+ invFuns
+ }*/
+ // Expressions for testing solvers
+ // a test expression
+ /*val tparam =
+ val dummyFunDef = new FunDef(FreshIdentifier("i"),Seq(), Seq(), IntegerType)
+ val eq = Equals(FunctionInvocation(TypedFunDef(dummyFunDef, Seq()), Seq()), InfiniteIntegerLiteral(0))
+ import solvers._
+ val solver = SimpleSolverAPI(SolverFactory(() => new solvers.smtlib.SMTLIBCVC4Solver(ctx, prog)))
+ solver.solveSAT(eq) match {
+ case (Some(true), m) =>
+ println("Model: "+m.toMap)
+ case _ => println("Formula is unsat")
+ }
+ System.exit(0)*/
+}
diff --git a/src/main/scala/leon/laziness/LazyFunctionsManager.scala b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
index f0e9462b33c117c9d340cbae7bc3e9646c0bdf7a..b5197ac4ca2d5ec6dacdd9a320e51a6b5cdd5795 100644
--- a/src/main/scala/leon/laziness/LazyFunctionsManager.scala
+++ b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
@@ -79,19 +79,21 @@ class LazyFunctionsManager(p: Program) {
(readfuns ++ valCallers, valCallers, starCallers ++ readfuns ++ valCallers)
}
- lazy val callersOfLazyCons = {
+ lazy val callersnTargetOfLazyCons = {
var consRoots = Set[FunDef]()
+ var targets = Set[FunDef]()
funsNeedStates.foreach {
case fd if fd.hasBody =>
postTraversal {
case finv: FunctionInvocation if isLazyInvocation(finv)(p) => // this is the lazy invocation constructor
consRoots += fd
+ targets += finv.tfd.fd
case _ =>
;
}(fd.body.get)
case _ => ;
}
- cg.transitiveCallers(consRoots.toSeq)
+ cg.transitiveCallers(consRoots.toSeq) ++ targets
}
lazy val cgWithoutSpecs = CallGraphUtil.constructCallGraph(p, true, false)
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..41375996956a49d5f3d61fe74add146d04266440
--- /dev/null
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -0,0 +1,237 @@
+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 purescala.TypeOps._
+import leon.invariant.util.TypeUtil._
+import leon.invariant.util.LetTupleSimplification._
+import leon.verification.VerificationPhase
+import java.io.File
+import java.io.FileWriter
+import java.io.BufferedWriter
+import scala.util.matching.Regex
+import leon.purescala.PrettyPrinter
+import leon.solvers._
+import leon.solvers.z3._
+import leon.transformations._
+import leon.LeonContext
+import leon.LeonOptionDef
+import leon.Main
+import leon.TransformationPhase
+import LazinessUtil._
+import invariant.datastructure._
+import invariant.util.ProgramUtil._
+import purescala.Constructors._
+import leon.verification._
+import PredicateUtil._
+import leon.invariant.engine._
+
+object LazyVerificationPhase {
+
+ val debugInstVCs = false
+
+ def removeInstrumentationSpecs(p: Program): Program = {
+ def hasInstVar(e: Expr) = {
+ exists { e => InstUtil.InstTypes.exists(i => i.isInstVariable(e)) }(e)
+ }
+ val newPosts = p.definedFunctions.collect {
+ case fd if fd.postcondition.exists { exists(hasInstVar) } =>
+ // remove the conjuncts that use instrumentation vars
+ val Lambda(resdef, pbody) = fd.postcondition.get
+ 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
+ //println(s"Fist let val: ${l.value} body: ${l.body}")
+ val (letsCons, letsBody) = letStarUnapply(l)
+ //println("Let* body: "+letsBody)
+ letsBody match {
+ case And(args) =>
+ letsCons(createAnd(args.filterNot(hasInstVar)))
+ case _ => Util.tru
+ }
+ case e => Util.tru
+ }
+ (fd -> Lambda(resdef, npost))
+ }.toMap
+ ProgramUtil.updatePost(newPosts, p) //note: this will not update libraries
+ }
+
+ def contextForChecks(userOptions: LeonContext) = {
+ val solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre"))
+ LeonContext(userOptions.reporter, userOptions.interruptManager,
+ solverOptions.options ++ userOptions.options)
+ }
+
+ // cumulative stats
+ var totalTime = 0L
+ var totalVCs = 0
+ var solvedWithZ3 = 0
+ var solvedWithCVC4 = 0
+ var z3Time = 0L
+ var cvc4Time = 0L
+
+ def collectCumulativeStats(rep: VerificationReport) {
+ totalTime += rep.totalTime
+ totalVCs += rep.totalConditions
+ val (withz3, withcvc) = rep.vrs.partition{
+ case (vc, vr) =>
+ vr.solvedWith.map(s => s.name.contains("smt-z3")).get
+ }
+ solvedWithZ3 += withz3.size
+ solvedWithCVC4 += withcvc.size
+ z3Time += withz3.map(_._2.timeMs.getOrElse(0L)).sum
+ cvc4Time += withcvc.map(_._2.timeMs.getOrElse(0L)).sum
+ }
+
+ def dumpStats() {
+ println("totalTime: "+f"${totalTime/1000d}%-3.3f")
+ println("totalVCs: "+totalVCs)
+ println("solvedWithZ3: "+ solvedWithZ3)
+ println("solvedWithCVC4: "+ solvedWithCVC4)
+ println("z3Time: "+f"${z3Time/1000d}%-3.3f")
+ println("cvc4Time: "+f"${cvc4Time/1000d}%-3.3f")
+ }
+
+ def checkSpecifications(prog: Program, checkCtx: LeonContext) {
+ // convert 'axiom annotation to library
+ prog.definedFunctions.foreach { fd =>
+ 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 solverOptions = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre")
+ val report = VerificationPhase.apply(checkCtx, prog)
+ // collect stats
+ collectCumulativeStats(report)
+ println(report.summaryString)
+ /*ctx.reporter.whenDebug(leon.utils.DebugSectionTimers) { debug =>
+ ctx.timers.outputTable(debug)
+ }*/
+ }
+
+ def checkInstrumentationSpecs(p: Program, checkCtx: LeonContext) = {
+
+ val useOrb = checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false)
+ p.definedFunctions.foreach { fd =>
+ if (fd.annotations.contains("axiom"))
+ fd.addFlag(Annotation("library", Seq()))
+ }
+ val funsToCheck = p.definedFunctions.filter(shouldGenerateVC)
+ if (useOrb) {
+ // create an inference context
+ val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds"))
+ val ctxForInf = LeonContext(checkCtx.reporter, checkCtx.interruptManager,
+ inferOpts.options ++ checkCtx.options)
+ val inferctx = new InferenceContext(p, ctxForInf)
+ val vcSolver = (funDef: FunDef, prog: Program) => new VCSolver(inferctx, prog, funDef)
+ prettyPrintProgramToFile(inferctx.inferProgram, checkCtx, "-inferProg", true)
+ (new InferenceEngine(inferctx)).analyseProgram(inferctx.inferProgram, funsToCheck, vcSolver, None)
+ } else {
+ val vcs = funsToCheck.map { fd =>
+ val (ants, post, tmpl) = createVC(fd)
+ if (tmpl.isDefined)
+ throw new IllegalStateException("Postcondition has holes! Run with --useOrb option")
+ val vc = implies(ants, post)
+ if (debugInstVCs)
+ println(s"VC for function ${fd.id} : " + vc)
+ VC(vc, fd, VCKinds.Postcondition)
+ }
+ val rep = checkVCs(vcs, checkCtx, p)
+ // record some stats
+ collectCumulativeStats(rep)
+ println("Resource Verification Results: \n" + rep.summaryString)
+ }
+ }
+
+ def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
+ exists(_ == TupleSelect(resid.toVariable, 2))(e)
+
+ /**
+ * Note: we also skip verification of uninterpreted functions
+ */
+ def shouldGenerateVC(fd: FunDef) = {
+ !fd.isLibrary && InstUtil.isInstrumented(fd) && fd.hasBody &&
+ fd.postcondition.exists { post =>
+ val Lambda(Seq(resdef), pbody) = post
+ accessesSecondRes(pbody, resdef.id)
+ }
+ }
+
+ /**
+ * creates 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 createVC(fd: FunDef) = {
+ val Lambda(Seq(resdef), _) = fd.postcondition.get
+ val (pbody, tmpl) = (fd.getPostWoTemplate, fd.template)
+ val (instPost, assumptions) = pbody match {
+ case And(args) =>
+ val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
+ (createAnd(instSpecs), createAnd(rest))
+ case l: Let =>
+ val (letsCons, letsBody) = letStarUnapply(l)
+ letsBody match {
+ case And(args) =>
+ val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
+ (letsCons(createAnd(instSpecs)),
+ letsCons(createAnd(rest)))
+ case _ =>
+ (l, Util.tru)
+ }
+ case e => (e, Util.tru)
+ }
+ val ants = createAnd(Seq(fd.precOrTrue, assumptions, Equals(resdef.id.toVariable, fd.body.get)))
+ (ants, instPost, tmpl)
+ }
+
+ def checkVCs(vcs: List[VC], checkCtx: LeonContext, p: Program) = {
+ val timeout: Option[Long] = None
+ val reporter = checkCtx.reporter
+ // Solvers selection and validation
+ val baseSolverF = SolverFactory.getFromSettings(checkCtx, p)
+ val solverF = timeout match {
+ case Some(sec) =>
+ baseSolverF.withTimeout(sec / 1000)
+ case None =>
+ baseSolverF
+ }
+ val vctx = VerificationContext(checkCtx, p, solverF, reporter)
+ try {
+ VerificationPhase.checkVCs(vctx, vcs)
+ //println("Resource Verification Results: \n" + veriRep.summaryString)
+ } finally {
+ solverF.shutdown()
+ }
+ }
+
+ class VCSolver(ctx: InferenceContext, p: Program, rootFd: FunDef) extends
+ UnfoldingTemplateSolver(ctx, p, rootFd) {
+ override def constructVC(fd: FunDef): (Expr, Expr) = {
+ val (ants, post, tmpl) = createVC(fd)
+ val conseq = matchToIfThenElse(createAnd(Seq(post, tmpl.getOrElse(Util.tru))))
+ (matchToIfThenElse(ants), conseq)
+ }
+
+ /**
+ * TODO: fix this!!
+ */
+ override def verifyInvariant(newposts: Map[FunDef, Expr]) = (Some(false), Model.empty)
+ }
+}
diff --git a/testcases/lazy-datastructures/ManualnOutdated/Concat.scala b/testcases/lazy-datastructures/ManualnOutdated/Concat.scala
index 3d3969956b2b27c96646cd9b0a3f9267a28663c0..8a881fc0177518b673ee1ce62a4bdecc338d5fb3 100644
--- a/testcases/lazy-datastructures/ManualnOutdated/Concat.scala
+++ b/testcases/lazy-datastructures/ManualnOutdated/Concat.scala
@@ -24,7 +24,7 @@ object Concat {
case Cons(x, xs) => SCons(x, $(concat(xs, l2)))
case Nil() => SNil[T]()
}
- } ensuring(_ => time <= ?)
+ } ensuring(_ => time <= 20)
def kthElem[T](l: $[LList[T]], k: BigInt): Option[T] = {
require(k >= 1)
@@ -35,10 +35,10 @@ object Concat {
kthElem(xs, k - 1)
case SNil() => None[T]
}
- } ensuring (_ => time <= ? * k)
+ } //ensuring (_ => time <= ? * k)
def concatnSelect[T](l1: List[T], l2: List[T], k: BigInt) : Option[T] = {
require(k >= 1)
kthElem($(concat(l1, l2)), k)
- } ensuring (_ => time <= ? * k)
+ } //ensuring (_ => time <= ? * k)
}