diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 34fc1c98c52a9b8d4d165e5e9d5d3d21d0e20e57..23a0a7780463a1ba66809747df5cc9d690463b95 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -185,10 +185,9 @@ object Main {
else if (terminationF) TerminationPhase
else if (isabelleF) IsabellePhase
else if (evalF) EvaluationPhase
- else if (inferInvF) InstrumentationPhase andThen InferInvariantsPhase
+ else if (inferInvF) InferInvariantsPhase
else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
else analysis
-
}
pipeBegin andThen
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index 30ca3fcdebedca181e58ea6929930d3b823aad9e..c724f05b37aa67f0df165af330e37f6b9bb5d9de 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -17,6 +17,7 @@ import transformations._
import verification._
import verification.VCKinds
import leon.purescala.ScalaPrinter
+import leon.purescala.PrettyPrinter
/**
* @author ravi
@@ -44,7 +45,7 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
optDisableInfer)
//TODO provide options for analyzing only selected functions
- def run(ctx: LeonContext)(prog: Program): InferenceReport = {
+ def run(ctx: LeonContext)(program: Program): InferenceReport = {
//control printing of statistics
val dumpStats = true
@@ -67,70 +68,40 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
var autoInference = true
for (opt <- ctx.options) (opt.optionDef.name, opt.value) match {
- case ("wholeprogram", true) => {
- //do not do a modular analysis
- modularlyAnalyze = false
- }
-
- case ("fullunroll", true) => {
- //do not do a modular analysis
- targettedUnroll = false
- }
-
- case ("minbounds", true) => {
- tightBounds = true
- }
-
- case ("withmult", true) => {
- withmult = true
- }
-
- case ("usereals", true) => {
- usereals = true
- }
-
+ case ("wholeprogram", true) =>
+ modularlyAnalyze = false
+ case ("fullunroll", true) =>
+ targettedUnroll = false
+ case ("minbounds", true) =>
+ tightBounds = true
+ case ("withmult", true) =>
+ withmult = true
+ case ("usereals", true) =>
+ usereals = true
case ("disableInfer", true) =>
autoInference = false
-
- case ("inferTemp", true) => {
- inferTemp = true
- var foundStrongest = false
- //go over all post-conditions and pick the strongest relation
- prog.definedFunctions.foreach((fd) => {
- if (!foundStrongest && fd.hasPostcondition) {
- val cond = fd.postcondition.get
- simplePostTransform((e) => e match {
- case Equals(_, _) => {
- enumerationRelation = Equals.apply _
- foundStrongest = true
- e
- }
- case _ => e
- })(cond)
- }
- })
- }
-
- case ("cegis", true) => {
- useCegis = true
- }
-
+ case ("inferTemp", true) =>
+ inferTemp = true
+ case ("cegis", true) =>
+ useCegis = true
case ("timeout", timeOut: Int) =>
timeout = timeOut
-
- case ("stats-suffix", suffix: String) => {
- statsSuff = suffix
- }
-
+ case ("stats-suffix", suffix: String) =>
+ statsSuff = suffix
case _ =>
}
+
+ // (a) first run instrumentation phase
+ val instProg = InstrumentationPhase(ctx, program)
- val funToTmpl = prog.definedFunctions.collect {
+ // (b) convert qmarks to tmpl functions
+ val funToTmpl = instProg.definedFunctions.collect {
case fd if fd.hasTemplate =>
fd -> fd.getTemplate
}.toMap
- val qMarksRemovedProg = Util.assignTemplateAndCojoinPost(funToTmpl, prog, Map())
+ val qMarksRemovedProg = Util.assignTemplateAndCojoinPost(funToTmpl, instProg, Map())
+ // convert nonlinearity to recursive functions
val newprog = if (usereals) {
(new IntToRealProgram())(qMarksRemovedProg)
} else qMarksRemovedProg
@@ -138,13 +109,33 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
val finalprog = nlelim(newprog)
val toVerifyPost = validateAndCollectNotValidated(qMarksRemovedProg, ctx, timeout)
+
+ // collect strongest relation for enumeration if defined
+ var foundStrongest = false
+ //go over all post-conditions and pick the strongest relation
+ instProg.definedFunctions.foreach((fd) => {
+ if (!foundStrongest && fd.hasPostcondition) {
+ val cond = fd.postcondition.get
+ simplePostTransform((e) => e match {
+ case Equals(_, _) => {
+ enumerationRelation = Equals.apply _
+ foundStrongest = true
+ e
+ }
+ case _ => e
+ })(cond)
+ }
+ })
+
//populate the inference context and invoke inferenceEngine
- val inferctx = new InferenceContext(finalprog, toVerifyPost, ctx,
+ val inferctx = new InferenceContext(program, finalprog, toVerifyPost, ctx,
//multiplication operation
(e1, e2) => FunctionInvocation(TypedFunDef(nlelim.multFun, nlelim.multFun.tparams.map(_.tp)), Seq(e1, e2)),
enumerationRelation = LessEquals, modularlyAnalyze, targettedUnroll, autoInference,
dumpStats, tightBounds, withmult, usereals, inferTemp, useCegis, timeout, maxCegisBound, statsSuff)
- (new InferenceEngine(inferctx)).run()
+ val report = (new InferenceEngine(inferctx)).run()
+ println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
+ report
}
def createLeonContext(ctx: LeonContext, opts: String*): LeonContext = {
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index 243cd54801a40ca9d4c2a60dfcb2d24ac3fdf802..bf3d83845b3fcb9b2ecbd3fe108186655dbc26b2 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -9,6 +9,7 @@ import purescala._
* @author ravi
*/
case class InferenceContext(
+ val uninstrumentedProgram : Program,
val program : Program,
val toVerifyPostFor: Set[String],
val leonContext : LeonContext,
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index 067eac087c5267cbc9c7c8eb7a62c90bfac3465f..03202f9dbb3a300a8eca4c2454b295e924dfd1b3 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -72,7 +72,7 @@ class InferenceEngine(ctx: InferenceContext) {
reporter.info("- Dumping statistics")
dumpStats(ctx.statsSuffix)
}
- new InferenceReport(program, results.map(pair => {
+ new InferenceReport(results.map(pair => {
val (fd, ic) = pair
(fd -> List[VC](ic))
}))(ctx)
@@ -141,7 +141,7 @@ class InferenceEngine(ctx: InferenceContext) {
val inv = TemplateInstantiator.getAllInvariants(model.get,
Map(origFd -> origFd.getTemplate))
// record the inferred invariants
- val ic = new InferenceCondition(Some(inv(origFd)), fd)
+ val ic = new InferenceCondition(Some(inv(origFd)), origFd)
ic.time = if (first) Some(funcTime) else Some(0.0)
// update analyzed set
analyzedSet += (origFd -> ic)
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index 21756faac1fb1deae5bd626070f517a935905291..15c1a1ffef4bbbc0d011431c3e915db8e3cf54e9 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -16,53 +16,52 @@ import invariant.structure._
import leon.transformations.InstUtil
import leon.purescala.PrettyPrinter
-
class InferenceCondition(val invariant: Option[Expr], funDef: FunDef)
extends VC(BooleanLiteral(true), funDef, null) {
- var time : Option[Double] = None
+ var time: Option[Double] = None
def status: String = invariant match {
case None => "unknown"
case Some(inv) => {
- val prettyInv = simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv),fd))
+ val prettyInv = simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd))
PrettyPrinter(prettyInv)
}
}
}
-class InferenceReport(p: Program, fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContext)
- extends VerificationReport(p : Program, Map()) {
+class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContext)
+ extends VerificationReport(ctx.program, Map()) {
import scala.math.Ordering.Implicits._
- val conditions : Seq[InferenceCondition] =
+ val conditions: Seq[InferenceCondition] =
fvcs.flatMap(_._2.map(_.asInstanceOf[InferenceCondition])).toSeq.sortBy(vc => vc.fd.id.name)
- private def infoSep(size: Int) : String = "╟" + ("┄" * size) + "╢\n"
- private def infoFooter(size: Int) : String = "╚" + ("═" * size) + "╝"
- private def infoHeader(size: Int) : String = ". ┌─────────┐\n" +
- "╔═╡ Summary ╞" + ("═" * (size - 12)) + "╗\n" +
- "║ └─────────┘" + (" " * (size - 12)) + "║"
+ private def infoSep(size: Int): String = "╟" + ("┄" * size) + "╢\n"
+ private def infoFooter(size: Int): String = "╚" + ("═" * size) + "╝"
+ private def infoHeader(size: Int): String = ". ┌─────────┐\n" +
+ "╔═╡ Summary ╞" + ("═" * (size - 12)) + "╗\n" +
+ "║ └─────────┘" + (" " * (size - 12)) + "║"
- private def infoLine(str: String, size: Int) : String = {
- "║ "+ str + (" " * (size - str.size - 2)) + " ║"
+ private def infoLine(str: String, size: Int): String = {
+ "║ " + str + (" " * (size - str.size - 2)) + " ║"
}
- private def fit(str : String, maxLength : Int) : String = {
- if(str.length <= maxLength) {
+ private def fit(str: String, maxLength: Int): String = {
+ if (str.length <= maxLength) {
str
} else {
str.substring(0, maxLength - 1) + "…"
}
}
- private def funName(fd: FunDef) = InstUtil.userFunctionName(fd)
+ private def funName(fd: FunDef) = InstUtil.userFunctionName(fd)
- override def summaryString : String = if(conditions.size > 0) {
+ override def summaryString: String = if (conditions.size > 0) {
val maxTempSize = (conditions.map(_.status.size).max + 3)
val outputStrs = conditions.map(vc => {
val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
- "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" "*(maxTempSize-vc.status.size)), timeStr)
+ "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" " * (maxTempSize - vc.status.size)), timeStr)
})
val summaryStr = {
val totalTime = conditions.foldLeft(0.0)((a, ic) => a + ic.time.getOrElse(0.0))
@@ -73,12 +72,41 @@ class InferenceReport(p: Program, fvcs: Map[FunDef, List[VC]])(implicit ctx: Inf
val entrySize = (outputStrs :+ summaryStr).map(_.size).max + 2
infoHeader(entrySize) +
- outputStrs.map(str => infoLine(str, entrySize)).mkString("\n", "\n", "\n") +
- infoSep(entrySize) +
- infoLine(summaryStr, entrySize) + "\n" +
- infoFooter(entrySize)
+ outputStrs.map(str => infoLine(str, entrySize)).mkString("\n", "\n", "\n") +
+ infoSep(entrySize) +
+ infoLine(summaryStr, entrySize) + "\n" +
+ infoFooter(entrySize)
} else {
"No user provided templates were solved."
}
+
+ def finalProgram: Program = {
+ val funToTmpl = conditions.collect {
+ case cd if cd.invariant.isDefined =>
+ cd.fd -> cd.invariant.get
+ }.toMap
+ Util.assignTemplateAndCojoinPost(funToTmpl, ctx.program)
+ }
+
+ def finalProgramWoInstrumentation: Program = {
+
+ val funToUninstFun = ctx.program.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
+ case (acc, fd) =>
+ val uninstFunName = InstUtil.userFunctionName(fd)
+ val uninstFdOpt =
+ if (uninstFunName.isEmpty) None
+ else Util.functionByName(uninstFunName, ctx.uninstrumentedProgram)
+ if (uninstFdOpt.isDefined) {
+ acc + (fd -> uninstFdOpt.get)
+ }
+ else acc
+ }
+ val funToPost = conditions.collect {
+ case cd if cd.invariant.isDefined && funToUninstFun.contains(cd.fd) =>
+ funToUninstFun(cd.fd) -> cd.invariant.get
+ }.toMap
+ //println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
+ Util.assignTemplateAndCojoinPost(Map(), ctx.uninstrumentedProgram, funToPost, uniqueIdDisplay = false)
+ }
}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/Util.scala b/src/main/scala/leon/invariant/util/Util.scala
index fdd70bf9a5bb21155d7269279d39be0e0559d5a1..cc9bf2b2c288c4975b832f36202c4343049ff04d 100644
--- a/src/main/scala/leon/invariant/util/Util.scala
+++ b/src/main/scala/leon/invariant/util/Util.scala
@@ -150,13 +150,14 @@ object Util {
})(ine)
}
- def assignTemplateAndCojoinPost(funToTmpl: Map[FunDef, Expr], prog: Program, funToPost: Map[FunDef, Expr] = Map()): Program = {
+ def assignTemplateAndCojoinPost(funToTmpl: Map[FunDef, Expr], prog: Program,
+ funToPost: Map[FunDef, Expr] = Map(), uniqueIdDisplay : Boolean = true): Program = {
val funMap = Util.functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
case (accMap, fd) if fd.isTheoryOperation =>
accMap + (fd -> fd)
case (accMap, fd) => {
- val freshId = FreshIdentifier(fd.id.name, fd.returnType, true)
+ val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
val newfd = new FunDef(freshId, fd.tparams, fd.returnType, fd.params)
accMap.updated(fd, newfd)
}
diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala
index fa35cc3f56cfe1dd37f2b013337373e619a5b086..01ab8f1716c9d5b47f93c6c008ffb022ea4ecba6 100644
--- a/src/main/scala/leon/transformations/InstrumentationUtil.scala
+++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala
@@ -67,7 +67,11 @@ object InstUtil {
mfd
}
- def userFunctionName(fd: FunDef) = fd.id.name.split("-")(0)
+ def userFunctionName(fd: FunDef) = {
+ val splits = fd.id.name.split("-")
+ if(!splits.isEmpty) splits(0)
+ else ""
+ }
def getInstMap(fd: FunDef) = {
val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition