From c7719514498b76a561e6f628456f28c34fc7e5cc Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Thu, 4 Feb 2016 18:29:50 +0100
Subject: [PATCH] Changing some parameters and minor changes
---
library/annotation/package.scala | 6 +++
.../invariant/engine/InferenceContext.scala | 2 +-
.../invariant/engine/RefinementEngine.scala | 45 ++++++++++---------
.../invariant/structure/FunctionUtils.scala | 1 +
.../templateSolvers/NLTemplateSolver.scala | 4 +-
.../laziness/LazinessEliminationPhase.scala | 7 +--
.../leon/laziness/LazyClosureConverter.scala | 6 +--
.../leon/laziness/LazyClosureFactory.scala | 3 +-
.../withOrb/RealTimeQueue.scala | 15 +++----
9 files changed, 49 insertions(+), 40 deletions(-)
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 94c4adb7d..14a770b4d 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -17,6 +17,8 @@ package object annotation {
class extern extends StaticAnnotation
@ignore
class inline extends StaticAnnotation
+
+ // Orb annotations
@ignore
class monotonic extends StaticAnnotation
@ignore
@@ -27,4 +29,8 @@ package object annotation {
class invstate extends StaticAnnotation
@ignore
class memoize extends StaticAnnotation
+ @ignore
+ class invisibleBody extends StaticAnnotation // do not unfold the body of the function
+ @ignore
+ class unfoldFactor(f: Int=0) extends StaticAnnotation // 0 implies no bound on unfolding
}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index 966a79dc6..96603581a 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -36,7 +36,7 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
val dumpStats = false
// the following options have default values
- val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
+ val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(30L) // in secs
val nlTimeout = leonContext.findOption(optNLTimeout).getOrElse(15L)
val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
diff --git a/src/main/scala/leon/invariant/engine/RefinementEngine.scala b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
index 4175ef57a..786a66b25 100644
--- a/src/main/scala/leon/invariant/engine/RefinementEngine.scala
+++ b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
@@ -70,7 +70,6 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
//unroll each call in the head pointers and in toRefineCalls
val callsToProcess = if (toRefineCalls.isDefined) {
-
//pick only those calls that have been least unrolled
val relevCalls = allheads.intersect(toRefineCalls.get)
var minCalls = Set[Call]()
@@ -86,14 +85,12 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
}
})
minCalls
-
} else allheads
if (verbose)
reporter.info("Unrolling: " + callsToProcess.size + "/" + allheads.size)
val unrolls = callsToProcess.foldLeft(Set[Call]())((acc, call) => {
-
val calldata = formula.callData(call)
val recInvokes = calldata.parents.count(_ == call.fi.tfd.fd)
//if the call is not a recursive call, unroll it unconditionally
@@ -110,7 +107,7 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
acc
}
}
- //TODO: are there better ways of unrolling ??
+ //TODO: are there better ways of unrolling ?? Yes. Akask Lal "dag Inlining". Implement that!
})
//update the head functions
@@ -189,25 +186,29 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
}
def inilineCall(call: Call, formula: Formula) = {
- //here inline the body and conjoin it with the guard
val tfd = call.fi.tfd
val callee = tfd.fd
-
- //Important: make sure we use a fresh body expression here, and freshenlocals
- val tparamMap = (callee.tparams zip tfd.tps).toMap
- val newbody = freshenLocals(matchToIfThenElse(callee.body.get))
- val freshBody = instantiateType(newbody, tparamMap, Map())
- val calleeSummary =
- Equals(getFunctionReturnVariable(callee), freshBody)
- val argmap1 = formalToActual(call)
- val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
-
- if (this.dumpInlinedSummary)
- println("Inlined Summary: " + inlinedSummary)
-
- //conjoin the summary with the disjunct corresponding to the 'guard'
- //note: the parents of the summary are the parents of the call plus the callee function
- val calldata = formula.callData(call)
- formula.conjoinWithDisjunct(calldata.guard, inlinedSummary, (callee +: calldata.parents))
+ if (callee.isBodyVisible) {
+ //here inline the body and conjoin it with the guard
+ //Important: make sure we use a fresh body expression here, and freshenlocals
+ val tparamMap = (callee.tparams zip tfd.tps).toMap
+ val newbody = freshenLocals(matchToIfThenElse(callee.body.get))
+ val freshBody = instantiateType(newbody, tparamMap, Map())
+ val calleeSummary =
+ Equals(getFunctionReturnVariable(callee), freshBody)
+ val argmap1 = formalToActual(call)
+ val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
+
+ if (this.dumpInlinedSummary)
+ println("Inlined Summary: " + inlinedSummary)
+
+ //conjoin the summary with the disjunct corresponding to the 'guard'
+ //note: the parents of the summary are the parents of the call plus the callee function
+ val calldata = formula.callData(call)
+ formula.conjoinWithDisjunct(calldata.guard, inlinedSummary, (callee +: calldata.parents))
+ } else {
+ if (verbose)
+ reporter.info(s"Not inlining ${call.fi}: body invisible!")
+ }
}
}
diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
index dc77b9447..fa9597e70 100644
--- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala
+++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
@@ -27,6 +27,7 @@ object FunctionUtils {
lazy val compose = fd.annotations.contains("compose")
lazy val isLibrary = fd.annotations.contains("library")
lazy val isExtern = fd.annotations.contains("extern")
+ lazy val isBodyVisible = !fd.annotations.contains("invisibleBody")
lazy val hasFieldFlag = fd.flags.contains(IsField(false))
lazy val hasLazyFieldFlag = fd.flags.contains(IsField(true))
lazy val isUserFunction = !hasFieldFlag && !hasLazyFieldFlag
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index f4e63e0c0..1194695b9 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -45,7 +45,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val trackUnpackedVCCTime = false
//print flags
- val verbose = true
+ val verbose = false
val printCounterExample = false
val printPathToConsole = false
val dumpPathAsSMTLIB = false
@@ -59,7 +59,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
private val farkasSolver = new FarkasLemmaSolver(ctx, program)
private val startFromEarlierModel = true
private val disableCegis = true
- private val useIncrementalSolvingForVCs = true
+ private val useIncrementalSolvingForVCs = false
private val useCVCToCheckVCs = true
private val usePortfolio = false // portfolio has a bug in incremental solving
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index c40e38a9c..ef1a5415e 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -37,6 +37,7 @@ import leon.verification._
import PredicateUtil._
import leon.invariant.engine._
import LazyVerificationPhase._
+import utils._
/**
* TODO: Function names are assumed to be small case. Fix this!!
*/
@@ -93,14 +94,14 @@ object LazinessEliminationPhase extends TransformationPhase {
if (dumpTypeCorrectProg)
println("After rectifying types: \n" + ScalaPrinter.apply(typeCorrectProg))
- val progWithPre = (new ClosurePreAsserter(typeCorrectProg)).apply
+ val progWithPre = (new ClosurePreAsserter(typeCorrectProg)).apply
if (dumpProgWithPreAsserts) {
//println("After asserting closure preconditions: \n" + ScalaPrinter.apply(progWithPre))
prettyPrintProgramToFile(progWithPre, ctx, "-withpre", uniqueIds = true)
}
// verify the contracts that do not use resources
- val progWOInstSpecs = removeInstrumentationSpecs(progWithPre)
+ val progWOInstSpecs = InliningPhase.apply(ctx, removeInstrumentationSpecs(progWithPre))
if (dumpProgWOInstSpecs) {
//println("After removing instrumentation specs: \n" + ScalaPrinter.apply(progWOInstSpecs))
prettyPrintProgramToFile(progWOInstSpecs, ctx, "-woinst")
@@ -110,7 +111,7 @@ object LazinessEliminationPhase extends TransformationPhase {
checkSpecifications(progWOInstSpecs, checkCtx)
// instrument the program for resources (note: we avoid checking preconditions again here)
- val instrumenter = new LazyInstrumenter(typeCorrectProg, closureFactory)
+ val instrumenter = new LazyInstrumenter(InliningPhase.apply(ctx, typeCorrectProg), closureFactory)
val instProg = instrumenter.apply
if (dumpInstrumentedProgram) {
//println("After instrumentation: \n" + ScalaPrinter.apply(instProg))
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index 365babd1b..404f968f6 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -251,8 +251,6 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
/**
* These are evalFunctions that do not affect the state.
- * TODO: here we can avoid creating two calls to the function one
- * with uninterpreted state and other with input state (since here both are equal)
*/
val computeFunctions = evalFunctions.map {
case (tname, evalfd) =>
@@ -267,6 +265,7 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val invoke = FunctionInvocation(TypedFunDef(evalfd, evalfd.tparams.map(_.tp)),
Seq(param1.id.toVariable, uiState))
fun.body = Some(TupleSelect(invoke, 1))
+ fun.addFlag(IsInlined)
(tname -> fun)
}.toMap
@@ -286,7 +285,8 @@ class LazyClosureConverter(p: Program, ctx: LeonContext,
val fun = new FunDef(FreshIdentifier(closureConsName(tname)), tparamdefs,
Seq(ValDef(param1), ValDef(param2)), param1Type)
fun.body = Some(param1.toVariable)
- // assert that the closure in unevaluated if useRefEquality is enabled
+ fun.addFlag(IsInlined)
+ // assert that the closure in unevaluated if useRefEquality is enabled! is this needed ?
// not supported as of now
/*if (refEq) {
val resid = FreshIdentifier("res", param1Type)
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index 49151ed15..921119154 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -207,7 +207,6 @@ class LazyClosureFactory(p: Program) {
val SetType(baseT) = stType.classDef.fields.find { fld => fld.id.name == fldname }.get.getType
val param2 = FreshIdentifier("cl", baseT)
- // TODO: as an optimization we can mark all these functions as inline and inline them at their callees
val updateFun = new FunDef(FreshIdentifier("updState" + tn),
state.tparams, Seq(ValDef(param1), ValDef(param2)), stType)
// create a body for the updateFun:
@@ -221,6 +220,8 @@ class LazyClosureFactory(p: Program) {
}
val nst = CaseClass(stType, nargs)
updateFun.body = Some(nst)
+ // add inline annotation of optimization
+ updateFun.addFlag(IsInlined)
(tn -> updateFun)
}.toMap
}
diff --git a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
index 7a3b07008..f0a78b4f2 100644
--- a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
@@ -28,15 +28,13 @@ object RealTimeQueue {
def size: BigInt = {
this match {
case SNil() => BigInt(0)
- case SCons(x, t) => 1 + ssize(t)
+ case SCons(x, t) => 1 + (t*).size
}
} ensuring (_ >= 0)
}
case class SCons[T](x: T, tail: $[Stream[T]]) extends Stream[T]
case class SNil[T]() extends Stream[T]
- def ssize[T](l: $[Stream[T]]): BigInt = (l*).size
-
def isConcrete[T](l: $[Stream[T]]): Boolean = {
l.isEvaluated && (l* match {
case SCons(_, tail) =>
@@ -45,9 +43,10 @@ object RealTimeQueue {
})
}
- @invstate
+ @invisibleBody
+ @invstate
def rotate[T](f: $[Stream[T]], r: List[T], a: $[Stream[T]]): Stream[T] = { // doesn't change state
- require(r.size == ssize(f) + 1 && isConcrete(f))
+ require(r.size == (f*).size + 1 && isConcrete(f))
(f.value, r) match {
case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
SCons[T](y, a)
@@ -82,7 +81,7 @@ object RealTimeQueue {
def isEmpty = (f*).isEmpty
def valid = {
(firstUnevaluated(f) == firstUnevaluated(s)) &&
- ssize(s) == ssize(f) - r.size //invariant: |s| = |f| - |r|
+ (s*).size == (f*).size - r.size //invariant: |s| = |f| - |r|
}
}
@@ -102,11 +101,11 @@ object RealTimeQueue {
createQ(q.f, Cons(x, q.r), q.s)
} ensuring (res => res.valid && time <= ?)
- /*def dequeue[T](q: Queue[T]): Queue[T] = {
+ def dequeue[T](q: Queue[T]): Queue[T] = {
require(!q.isEmpty && q.valid)
q.f.value match {
case SCons(x, nf) =>
createQ(nf, q.r, q.s)
}
- } ensuring (res => res.valid && time <= ?)*/
+ } ensuring (res => res.valid && time <= ?)
}
--
GitLab