From 32d53a55d219b144c33e7d50b31ea4fea687987c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 18 Dec 2012 20:05:35 +0100
Subject: [PATCH] Implement a new XlangAnalysisPhase
This commit introduces a new XlangAnalysisPhase that run
all the xlang phase as well as the AnalysisPhase. It updates
the Main accordingly.
The reason for this change is to be able to correctly control
the --functions option as well as transforming each VerificationCondition
about function postcondition into loop invariant.
The previous solution was to use some mutable states inside the FunDef object.
Those are cleaned by this commit. To do so, it was necessary to change the
transformation phases signature in order to return along with the modified
program a Set or Map (depending on which phase) of freshly introduced
functions and their correspondance in the original program.
One small change that was necessary was to not print the verification report
in the analysis phase but only in the Main. This allows the XlangAnalysisPhase
to update correctly the verification conditions in the report before it gets
printed. This is also arguably a better design decision to have it printed
in the Main since it was returned by the AnalysisPhase.
---
src/main/scala/leon/LeonOption.scala | 1 +
src/main/scala/leon/Main.scala | 21 ++---
src/main/scala/leon/TypeChecking.scala | 2 -
src/main/scala/leon/UnitElimination.scala | 4 -
.../scala/leon/purescala/Definitions.scala | 5 --
.../leon/verification/AnalysisPhase.scala | 1 -
.../leon/verification/DefaultTactic.scala | 25 +++---
.../verification/VerificationCondition.scala | 1 +
.../leon/xlang/ArrayTransformation.scala | 4 -
.../scala/leon/xlang/FunctionClosure.scala | 27 +++++--
.../xlang/ImperativeCodeElimination.scala | 16 ++--
src/main/scala/leon/xlang/Trees.scala | 16 ----
.../scala/leon/xlang/XlangAnalysisPhase.scala | 80 +++++++++++++++++++
.../XLangVerificationRegression.scala | 7 +-
14 files changed, 130 insertions(+), 80 deletions(-)
create mode 100644 src/main/scala/leon/xlang/XlangAnalysisPhase.scala
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 40cd6c23f..da28a90d5 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -40,5 +40,6 @@ case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: Stri
}
object ListValue {
+ def apply(values: Seq[String]) = values.mkString(":")
def unapply(value: String): Option[Seq[String]] = Some(value.split(':').map(_.trim).filter(!_.isEmpty))
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 26477afd3..56d66e601 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -9,6 +9,7 @@ object Main {
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
xlang.FunctionClosure,
+ xlang.XlangAnalysisPhase,
synthesis.SynthesisPhase,
verification.AnalysisPhase
)
@@ -118,16 +119,6 @@ object Main {
val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase
- val pipeTransforms: Pipeline[Program, Program] =
- if (settings.xlang) {
- xlang.ArrayTransformation andThen
- xlang.EpsilonElimination andThen
- xlang.ImperativeCodeElimination andThen
- xlang.FunctionClosure
- } else {
- NoopPhase()
- }
-
val pipeSynthesis: Pipeline[Program, Program]=
if (settings.synthesis) {
synthesis.SynthesisPhase
@@ -136,14 +127,15 @@ object Main {
}
val pipeVerify: Pipeline[Program, Any] =
- if (settings.verify) {
+ if (settings.xlang) {
+ xlang.XlangAnalysisPhase
+ } else if (settings.verify) {
verification.AnalysisPhase
} else {
NoopPhase()
}
pipeBegin andThen
- pipeTransforms andThen
pipeSynthesis andThen
pipeVerify
}
@@ -159,7 +151,10 @@ object Main {
try {
// Run pipeline
- pipeline.run(ctx)(args.toList)
+ pipeline.run(ctx)(args.toList) match {
+ case (report: verification.VerificationReport) => reporter.info(report.summaryString)
+ case _ =>
+ }
} catch {
case LeonFatalError() => sys.exit(1)
}
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index 08291badc..41cda6b80 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -87,8 +87,6 @@ object TypeChecking extends UnitPhase[Program] {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.precondition = fd.precondition.map(transform)
// freshFunDef.postcondition = fd.postcondition.map(transform)
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 3d56d5377..dc58a24be 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -23,8 +23,6 @@ object UnitElimination extends TransformationPhase {
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
- freshFunDef.fromLoop = fd.fromLoop
- freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
@@ -102,8 +100,6 @@ object UnitElimination extends TransformationPhase {
val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- freshFunDef.parent = fd.parent
- freshFunDef.fromLoop = fd.fromLoop
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 6eee2247c..80f1df984 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -313,11 +313,6 @@ object Definitions {
var precondition: Option[Expr] = None
var postcondition: Option[Expr] = None
- //true if this function has been generated from a while loop
- var fromLoop = false
- //the fundef where the loop was defined (if applies)
- var parent: Option[FunDef] = None
-
def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2e340cac1..146f8bb2d 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -148,7 +148,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
val report = new VerificationReport(vcs)
- reporter.info(report.summaryString)
report
}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 47a2af0d2..cdc752a50 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -44,10 +44,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrec
}
- if(functionDefinition.fromLoop)
- Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
- else
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
@@ -76,13 +73,13 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
val newBody : Expr = replace(substMap, prec)
val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
- if(fd.fromLoop)
- new VerificationCondition(
- withPrecIfDefined(path, newCall),
- fd.parent.get,
- if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
- else
+ //if(fd.fromLoop)
+ // new VerificationCondition(
+ // withPrecIfDefined(path, newCall),
+ // fd.parent.get,
+ // if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
+ // this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
+ //else
new VerificationCondition(
withPrecIfDefined(path, newCall),
function,
@@ -117,7 +114,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function,//if(function.fromLoop) function.parent.get else function,
VCKind.ExhaustiveMatch,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -149,7 +146,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function, //if(function.fromLoop) function.parent.get else function,
VCKind.MapAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -178,7 +175,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function, //if(function.fromLoop) function.parent.get else function,
VCKind.ArrayAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 573bcd699..893fb39b3 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -42,4 +42,5 @@ object VCKind extends Enumeration {
val InvariantInit = Value("inv init.")
val InvariantInd = Value("inv ind.")
val InvariantPost = Value("inv post.")
+ val InvariantPre = Value("inv pre.")
}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 880e870f5..4a9017597 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -142,8 +142,6 @@ object ArrayTransformation extends TransformationPhase {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
// freshFunDef
// } else fd
@@ -272,8 +270,6 @@ object ArrayTransformation extends TransformationPhase {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.precondition = fd.precondition.map(transform)
// freshFunDef.postcondition = fd.postcondition.map(transform)
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 47e0cbeed..c6fc16e1f 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -1,4 +1,5 @@
-package leon.xlang
+package leon
+package xlang
import leon.TransformationPhase
import leon.LeonContext
@@ -10,31 +11,41 @@ import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.xlang.Trees._
-object FunctionClosure extends TransformationPhase{
+object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef], Map[FunDef, FunDef])] {
val name = "Function Closure"
val description = "Closing function with its scoping variables"
+ /* I know, that's a lot of mutable variables */
private var pathConstraints: List[Expr] = Nil
private var enclosingLets: List[(Identifier, Expr)] = Nil
private var newFunDefs: Map[FunDef, FunDef] = Map()
private var topLevelFuns: Set[FunDef] = Set()
+ private var parent: FunDef = null //refers to the current toplevel parent
+ private var parents: Map[FunDef, FunDef] = null //each hoisted function mapped to its original parent
+ private var freshFunDefs: Map[FunDef, FunDef] = null //mapping from original FunDef in LetDef to the fresh ones
+ /* but notice the private keyword */
- def apply(ctx: LeonContext, program: Program): Program = {
+ //return modified program, new funDef to their original parents, old FunDef to freshly introduced FunDef
+ def run(ctx: LeonContext)(program: Program): (Program, Map[FunDef, FunDef], Map[FunDef, FunDef]) = {
pathConstraints = Nil
enclosingLets = Nil
newFunDefs = Map()
topLevelFuns = Set()
+ parent = null
+ parents = Map()
+ freshFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
+ parent = fd
pathConstraints = fd.precondition.toList
fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
val Program(id, ObjectDef(objId, defs, invariants)) = program
val res = Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
- res
+ (res, parents, freshFunDefs)
}
private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
@@ -50,13 +61,13 @@ object FunctionClosure extends TransformationPhase{
val extraVarDecls: Seq[VarDecl] = extraVarDeclFreshIds.map(id => VarDecl(id, id.getType))
val newVarDecls: Seq[VarDecl] = fd.args ++ extraVarDecls
val newBindedVars: Set[Identifier] = bindedVars ++ fd.args.map(_.id)
- val newFunId = FreshIdentifier(fd.id.name)
+ val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
topLevelFuns += newFunDef
- newFunDef.fromLoop = fd.fromLoop
- newFunDef.parent = fd.parent
- newFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
+ parents += (newFunDef -> parent)
+ freshFunDefs += (fd -> newFunDef)
def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index b926893cd..656104b92 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -1,4 +1,5 @@
-package leon.xlang
+package leon
+package xlang
import leon.TransformationPhase
import leon.LeonContext
@@ -10,16 +11,18 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.xlang.Trees._
-object ImperativeCodeElimination extends TransformationPhase {
+object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef])] {
val name = "Imperative Code Elimination"
val description = "Transform imperative constructs into purely functional code"
private var varInScope = Set[Identifier]()
private var parent: FunDef = null //the enclosing fundef
+ private var wasLoop: Set[FunDef] = null //record FunDef that are the transformation of loops
- def apply(ctx: LeonContext, pgm: Program): Program = {
+ def run(ctx: LeonContext)(pgm: Program): (Program, Set[FunDef]) = {
varInScope = Set()
+ wasLoop = Set()
parent = null
val allFuns = pgm.definedFunctions
@@ -28,7 +31,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
}))
- pgm
+ (pgm, wasLoop)
}
//return a "scope" consisting of purely functional code that defines potentially needed
@@ -150,9 +153,8 @@ object ImperativeCodeElimination extends TransformationPhase {
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
- whileFunDef.fromLoop = true
- whileFunDef.parent = Some(parent)
+ val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
+ wasLoop += whileFunDef
val whileFunCond = condRes
val whileFunRecursiveCall = replaceNames(condFun,
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 31c717784..13fded9dc 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -261,8 +261,6 @@ object Trees {
case (None, None) =>
Some((Seq(b, body), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//LetDef(nfd, as(1))
fd.body = Some(as(0))
@@ -271,8 +269,6 @@ object Trees {
case (Some(pre), None) =>
Some((Seq(b, body, pre), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.precondition = Some(as(2))
//LetDef(nfd, as(1))
@@ -283,8 +279,6 @@ object Trees {
case (None, Some(post)) =>
Some((Seq(b, body, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.postcondition = Some(as(2))
//LetDef(nfd, as(1))
@@ -295,8 +289,6 @@ object Trees {
case (Some(pre), Some(post)) =>
Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.precondition = Some(as(2))
//nfd.postcondition = Some(as(3))
@@ -313,16 +305,12 @@ object Trees {
case (None, None) =>
Some((Seq(body), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//LetDef(nfd, as(0))
LetDef(fd, as(0))
}))
case (Some(pre), None) =>
Some((Seq(body, pre), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.precondition = Some(as(1))
//LetDef(nfd, as(0))
fd.precondition = Some(as(1))
@@ -331,8 +319,6 @@ object Trees {
case (None, Some(post)) =>
Some((Seq(body, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.postcondition = Some(as(1))
//LetDef(nfd, as(0))
fd.postcondition = Some(as(1))
@@ -341,8 +327,6 @@ object Trees {
case (Some(pre), Some(post)) =>
Some((Seq(body, pre, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.precondition = Some(as(1))
//nfd.postcondition = Some(as(2))
//LetDef(nfd, as(0))
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
new file mode 100644
index 000000000..4f29e272f
--- /dev/null
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -0,0 +1,80 @@
+package leon
+package xlang
+
+import leon.purescala.Definitions._
+import leon.verification._
+
+object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
+
+ val name = "xlang analysis"
+ val description = "apply analysis on xlang"
+
+ def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
+
+ val pgm1 = ArrayTransformation(ctx, pgm)
+ val pgm2 = EpsilonElimination(ctx, pgm1)
+ val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
+ val (pgm4, parents, freshFunDefs) = FunctionClosure.run(ctx)(pgm3)
+
+ val originalFunDefs = freshFunDefs.map(x => (x._2, x._1))
+
+ def functionWasLoop(fd: FunDef): Boolean = originalFunDefs.get(fd) match {
+ case None => false //meaning, this was a top level function
+ case Some(nested) => wasLoop.contains(nested) //could have been a LetDef originally
+ }
+ def subFunctionsOf(fd: FunDef): Set[FunDef] = parents.flatMap((p: (FunDef, FunDef)) => p match {
+ case (child, parent) => if(parent == fd) List(child) else List()
+ }).toSet
+
+ val newOptions = ctx.options map {
+ case LeonValueOption("functions", ListValue(fs)) => {
+ var freshToAnalyse: Set[String] = Set()
+ fs.foreach((toAnalyse: String) => {
+ pgm.definedFunctions.find(_.id.name == toAnalyse) match {
+ case Some(fd) => {
+ val children = subFunctionsOf(fd)
+ freshToAnalyse ++= children.map(_.id.name)
+ freshToAnalyse += fd.id.name
+ }
+ case None =>
+ }
+ })
+
+ LeonValueOption("functions", ListValue(freshToAnalyse.toList))
+ }
+ case opt => opt
+ }
+ val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
+ val vcs = vr.conditions
+
+ //this is enough to convert invariant postcondition and inductive conditions. However the initial validity
+ //of the invariant (before entering the loop) will still appear as a regular function precondition
+ //To fix this, we need some information in the VCs about which function the precondtion refers to
+ //although we could arguably say that the term precondition is general enough to refer both to a loop invariant
+ //precondition and a function invocation precondition
+ val freshVcs = vcs.map(vc => {
+ val funDef = vc.funDef
+ if(functionWasLoop(funDef)) {
+ val freshVc = new VerificationCondition(
+ vc.condition,
+ parents(funDef),
+ if(vc.kind == VCKind.Postcondition) VCKind.InvariantPost else if(vc.kind == VCKind.Precondition) VCKind.InvariantInd else vc.kind,
+ vc.tactic,
+ vc.info).setPosInfo(funDef)
+ freshVc.value = vc.value
+ freshVc.solvedWith = vc.solvedWith
+ freshVc.time = vc.time
+ freshVc
+ } else vc
+ })
+
+ val sortedFreshVcs = freshVcs.sortWith((vc1, vc2) => {
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ })
+
+ new VerificationReport(sortedFreshVcs)
+ }
+
+}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 4102f5b87..f5b33c3e2 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -19,12 +19,7 @@ class XLangVerificationRegression extends FunSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.plugin.ExtractionPhase andThen
- xlang.ArrayTransformation andThen
- xlang.EpsilonElimination andThen
- xlang.ImperativeCodeElimination andThen
- xlang.FunctionClosure andThen
- leon.verification.AnalysisPhase
+ leon.plugin.ExtractionPhase andThen xlang.XlangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()
--
GitLab