Skip to content
Snippets Groups Projects
Commit 2011bc04 authored by Philippe Suter's avatar Philippe Suter
Browse files

now with unrolling

parent a1119315
No related branches found
No related tags found
No related merge requests found
...@@ -23,6 +23,7 @@ class FunCheckPlugin(val global: Global) extends Plugin { ...@@ -23,6 +23,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" + " -P:funcheck:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
" -P:funcheck:nodefaults Runs only the analyses provided by the extensions" + "\n" + " -P:funcheck:nodefaults Runs only the analyses provided by the extensions" + "\n" +
" -P:funcheck:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" + " -P:funcheck:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
" -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" + " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" " -P:funcheck:quiet No info and warning messages from the extensions"
) )
...@@ -38,6 +39,7 @@ class FunCheckPlugin(val global: Global) extends Plugin { ...@@ -38,6 +39,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "tolerant" => silentlyTolerateNonPureBodies = true case "tolerant" => silentlyTolerateNonPureBodies = true
case "quiet" => purescala.Settings.quietExtensions = true case "quiet" => purescala.Settings.quietExtensions = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*) case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length)) case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
case _ => error("Invalid option: " + option) case _ => error("Invalid option: " + option)
......
...@@ -72,8 +72,9 @@ class Analysis(val program: Program) { ...@@ -72,8 +72,9 @@ class Analysis(val program: Program) {
reporter.info(vc) reporter.info(vc)
// reporter.info("Negated:") // reporter.info("Negated:")
// reporter.info(negate(vc)) // reporter.info(negate(vc))
reporter.info("Negated, expanded:") // reporter.info("Negated, expanded:")
reporter.info(expandLets(negate(vc))) // val exp = expandLets(negate(vc))
// reporter.info(exp)
// try all solvers until one returns a meaningful answer // try all solvers until one returns a meaningful answer
solverExtensions.find(se => { solverExtensions.find(se => {
...@@ -107,14 +108,15 @@ class Analysis(val program: Program) { ...@@ -107,14 +108,15 @@ class Analysis(val program: Program) {
} else { } else {
val resFresh = FreshIdentifier("result", true).setType(body.getType) val resFresh = FreshIdentifier("result", true).setType(body.getType)
val bodyAndPost = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), post.get)) val bodyAndPost = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), post.get))
val newExpr = if(prec.isEmpty) { val withPrec = if(prec.isEmpty) {
bodyAndPost bodyAndPost
} else { } else {
Implies(prec.get, bodyAndPost) Implies(prec.get, bodyAndPost)
} }
import Analysis._ import Analysis._
val (newExpr1, sideExprs1) = rewriteSimplePatternMatching(newExpr) val newExpr0 = unrollRecursiveFunctions(program, withPrec, Settings.unrollingLevel)
val (newExpr1, sideExprs1) = rewriteSimplePatternMatching(newExpr0)
val (newExpr2, sideExprs2) = inlineFunctionsAndContracts(program, newExpr1) val (newExpr2, sideExprs2) = inlineFunctionsAndContracts(program, newExpr1)
if(sideExprs1.isEmpty && sideExprs2.isEmpty) { if(sideExprs1.isEmpty && sideExprs2.isEmpty) {
...@@ -162,12 +164,37 @@ object Analysis { ...@@ -162,12 +164,37 @@ object Analysis {
(searchAndApply(isFunCall, applyToCall, expr), extras.reverse) (searchAndApply(isFunCall, applyToCall, expr), extras.reverse)
} }
def unrollRecursiveFunctions(program: Program, expr: Expr, times: Int) : Expr = {
def isRecursiveCall(e: Expr) = e match {
case f @ FunctionInvocation(fd, _) if fd.hasImplementation && program.isRecursive(fd) => true
case _ => false
}
def unrollCall(t: Int)(e: Expr) = e match {
case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
val newLetIDs = fd.args.map(a => FreshIdentifier(a.id.name, true).setType(a.tpe))
val newLetVars = newLetIDs.map(Variable(_))
val substs: Map[Expr,Expr] = Map((fd.args.map(_.toVariable) zip newLetVars) :_*)
val bodyWithLetVars: Expr = replace(substs, fd.body.get)
val bigLet = (newLetIDs zip args).foldLeft(bodyWithLetVars)((e,p) => Let(p._1, p._2, e))
unrollRecursiveFunctions(program, bigLet, t - 1)
}
case o => o
}
if(times > 0)
searchAndApply(isRecursiveCall, unrollCall(times), expr, false)
else
expr
}
// Rewrites pattern matching expressions where the cases simply correspond to // Rewrites pattern matching expressions where the cases simply correspond to
// the list of constructors // the list of constructors
def rewriteSimplePatternMatching(expr: Expr) : (Expr, Seq[Expr]) = { def rewriteSimplePatternMatching(expr: Expr) : (Expr, Seq[Expr]) = {
var extras : List[Expr] = Nil var extras : List[Expr] = Nil
def isPMExpr(e: Expr) : Boolean = e.isInstanceOf[MatchExpr] def isPMExpr(e: Expr) : Boolean = {
e.isInstanceOf[MatchExpr]
}
def rewritePM(e: Expr) : Expr = { def rewritePM(e: Expr) : Expr = {
val MatchExpr(scrutinee, cases) = e.asInstanceOf[MatchExpr] val MatchExpr(scrutinee, cases) = e.asInstanceOf[MatchExpr]
...@@ -194,7 +221,8 @@ object Analysis { ...@@ -194,7 +221,8 @@ object Analysis {
} else { } else {
Variable(FreshIdentifier("pat", true)).setType(p._1.tpe) Variable(FreshIdentifier("pat", true)).setType(p._1.tpe)
}) })
(newPVar, List(Equals(newPVar, CaseClass(ccd, argVars)), Implies(Equals(Variable(scrutAsLetID), newPVar), Equals(newVar, rhs)))) val (rewrittenRHS, moreExtras) = rewriteSimplePatternMatching(rhs)
(newPVar, List(Equals(newPVar, CaseClass(ccd, argVars)), Implies(Equals(Variable(scrutAsLetID), newPVar), Equals(newVar, rewrittenRHS))) ::: moreExtras.toList)
} }
case _ => (null,Nil) case _ => (null,Nil)
}).toList }).toList
...@@ -219,13 +247,19 @@ object Analysis { ...@@ -219,13 +247,19 @@ object Analysis {
} }
} }
// this gets us "extras", but we will still need to clean these up. val cleanerTree = searchAndApply(isPMExpr, rewritePM, expr)
val cleanerTree = searchAndApply(isPMExpr, rewritePM, expr) // println("******************")
val theExtras = extras.reverse // println("rewrote: " + expr)
val onExtras: Seq[(Expr,Seq[Expr])] = theExtras.map(rewriteSimplePatternMatching(_)) // println(" *** to ***")
// the "moreExtras" should be cleaned up due to the recursive call.. // println(cleanerTree)
val (rewrittenExtras, moreExtras) = onExtras.unzip // println(" ** with side conds ** ")
// println(extras.reverse)
(cleanerTree, rewrittenExtras ++ moreExtras.flatten) // println("******************")
(cleanerTree, extras.reverse)
// val theExtras = extras.reverse
// val onExtras: Seq[(Expr,Seq[Expr])] = theExtras.map(rewriteSimplePatternMatching(_))
// // the "moreExtras" should be cleaned up due to the recursive call..
// val (rewrittenExtras, moreExtras) = onExtras.unzip
// (cleanerTree, rewrittenExtras ++ moreExtras.flatten)
} }
} }
...@@ -9,4 +9,5 @@ object Settings { ...@@ -9,4 +9,5 @@ object Settings {
var reporter: Reporter = new DefaultReporter var reporter: Reporter = new DefaultReporter
var quietReporter: Reporter = new QuietReporter var quietReporter: Reporter = new QuietReporter
var runDefaultExtensions: Boolean = true var runDefaultExtensions: Boolean = true
var unrollingLevel: Int = 0
} }
...@@ -103,7 +103,6 @@ object Trees { ...@@ -103,7 +103,6 @@ object Trees {
val fixedType = BooleanType val fixedType = BooleanType
} }
/* Literals */
case class Variable(id: Identifier) extends Expr { case class Variable(id: Identifier) extends Expr {
override def getType = id.getType override def getType = id.getType
override def setType(tt: TypeTree) = { id.setType(tt); this } override def setType(tt: TypeTree) = { id.setType(tt); this }
...@@ -112,6 +111,7 @@ object Trees { ...@@ -112,6 +111,7 @@ object Trees {
// represents the result in post-conditions // represents the result in post-conditions
case class ResultVariable() extends Expr case class ResultVariable() extends Expr
/* Literals */
sealed abstract class Literal[T] extends Expr { sealed abstract class Literal[T] extends Expr {
val value: T val value: T
} }
...@@ -275,7 +275,9 @@ object Trees { ...@@ -275,7 +275,9 @@ object Trees {
// the replacement map should be understood as follows: // the replacement map should be understood as follows:
// - on each subexpression, checkFun checks whether it should be replaced // - on each subexpression, checkFun checks whether it should be replaced
// - repFun is applied is checkFun succeeded // - repFun is applied is checkFun succeeded
def searchAndApply(checkFun: Expr=>Boolean, repFun: Expr=>Expr, expr: Expr) : Expr = { // - if the result of repFun is different from its argument and recursive
// is set to true, search/replace is reapplied on the result.
def searchAndApply(checkFun: Expr=>Boolean, repFun: Expr=>Expr, expr: Expr, recursive: Boolean=true) : Expr = {
def rec(ex: Expr, skip: Expr = null) : Expr = ex match { def rec(ex: Expr, skip: Expr = null) : Expr = ex match {
case _ if (ex != skip && checkFun(ex)) => { case _ if (ex != skip && checkFun(ex)) => {
val newExpr = repFun(ex) val newExpr = repFun(ex)
...@@ -283,9 +285,9 @@ object Trees { ...@@ -283,9 +285,9 @@ object Trees {
Settings.reporter.warning("REPLACING IN EXPRESSION WITH AN UNTYPED TREE ! " + ex + " --to--> " + newExpr) Settings.reporter.warning("REPLACING IN EXPRESSION WITH AN UNTYPED TREE ! " + ex + " --to--> " + newExpr)
} }
if(ex == newExpr) if(ex == newExpr)
rec(ex, ex) if(recursive) rec(ex, ex) else ex
else else
rec(newExpr) if(recursive) rec(newExpr) else newExpr
} }
case l @ Let(i,e,b) => { case l @ Let(i,e,b) => {
val re = rec(e) val re = rec(e)
...@@ -361,16 +363,17 @@ object Trees { ...@@ -361,16 +363,17 @@ object Trees {
def simplifyLets(expr: Expr) : Expr = { def simplifyLets(expr: Expr) : Expr = {
val isLet = ((t: Expr) => t.isInstanceOf[Let]) val isLet = ((t: Expr) => t.isInstanceOf[Let])
def simplerLet(t: Expr) : Expr = t match { def simplerLet(t: Expr) : Expr = t match {
case letExpr @ Let(_, Variable(_), _) => expandLets(letExpr) case letExpr @ Let(i, Variable(v), b) => replace(Map((Variable(i) -> Variable(v))), b)
case letExpr @ Let(i, l: Literal[_], b) => replace(Map((Variable(i) -> l)), b)
case letExpr @ Let(i,e,b) => { case letExpr @ Let(i,e,b) => {
var occurences = 0 var occurences = 0
def isOcc(tr: Expr) = (occurences < 2 && tr.isInstanceOf[Variable] && tr.asInstanceOf[Variable].id == i) def isOcc(tr: Expr) = (occurences < 2 && tr == Variable(i))
def incCount(tr: Expr) = { occurences = occurences + 1; tr } def incCount(tr: Expr) = { occurences = occurences + 1; tr }
searchAndApply(isOcc,incCount,b) searchAndApply(isOcc, incCount, b, false)
if(occurences == 0) { if(occurences == 0) {
b b
} else if(occurences == 1) { } else if(occurences == 1) {
expandLets(letExpr) replace(Map((Variable(i) -> e)), b)
} else { } else {
t t
} }
......
...@@ -150,7 +150,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) { ...@@ -150,7 +150,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
Equals(fOfX, funDef.body.get) Equals(fOfX, funDef.body.get)
} }
val (newExpr1, sideExprs1) = Analysis.rewriteSimplePatternMatching(toConvert) val (newExpr1, sideExprs1) = Analysis.rewriteSimplePatternMatching(toConvert)
val (newExpr2, sideExprs2) = Analysis.inlineFunctionsAndContracts(program, newExpr1) val (newExpr2, sideExprs2) = (newExpr1, Nil) // Analysis.inlineFunctionsAndContracts(program, newExpr1)
val finalToConvert = if(sideExprs1.isEmpty && sideExprs2.isEmpty) { val finalToConvert = if(sideExprs1.isEmpty && sideExprs2.isEmpty) {
newExpr2 newExpr2
} else { } else {
...@@ -165,6 +165,9 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) { ...@@ -165,6 +165,9 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
} }
case None => { case None => {
reporter.warning("Could not generate forall axiom for " + funDef.id.name) reporter.warning("Could not generate forall axiom for " + funDef.id.name)
reporter.warning(toConvert)
reporter.warning(newExpr1)
reporter.warning(newExpr2)
reporter.warning(finalToConvert) reporter.warning(finalToConvert)
} }
} }
......
...@@ -5,8 +5,8 @@ object ExprComp { ...@@ -5,8 +5,8 @@ object ExprComp {
// Operations // Operations
sealed abstract class BinOp sealed abstract class BinOp
case class Plus extends BinOp case class Plus() extends BinOp
case class Times extends BinOp case class Times() extends BinOp
// Expressions // Expressions
sealed abstract class Expr sealed abstract class Expr
...@@ -34,20 +34,20 @@ object ExprComp { ...@@ -34,20 +34,20 @@ object ExprComp {
// Programs // Programs
sealed abstract class Program sealed abstract class Program
case class EProgram extends Program case class EProgram() extends Program
case class NProgram(first : Instruction, rest : Program) extends Program case class NProgram(first : Instruction, rest : Program) extends Program
// Value stack // Value stack
sealed abstract class ValueStack sealed abstract class ValueStack
case class EStack extends ValueStack case class EStack() extends ValueStack
case class NStack(v : Value, rest : ValueStack) extends ValueStack case class NStack(v : Value, rest : ValueStack) extends ValueStack
// Outcomes of running the program // Outcomes of running the program
sealed abstract class Outcome sealed abstract class Outcome
case class Ok(v : ValueStack) extends Outcome case class Ok(v : ValueStack) extends Outcome
case class Fail extends Outcome case class Fail() extends Outcome
// Running programs on a given initial stack // Running programs on a given initial stack
def run(p : Program, vs : ValueStack) : Outcome = p match { def run(p : Program, vs : ValueStack) : Outcome = p match {
......
object Fibonacci {
def fib(x: Int) : Int = {
require(x >= 0)
if(x < 2) {
x
} else {
fib(x - 1) + fib(x - 2)
}
}
// requires that fib is universally quantified to work...
def check() : Boolean = {
fib(5) == 5
} ensuring(_ == true)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment