Skip to content
Snippets Groups Projects
Commit 75c86e99 authored by Ravi's avatar Ravi
Browse files

Implementing a new induction tactic and adding test cases

parent b4bd39dd
No related branches found
No related tags found
No related merge requests found
...@@ -10,7 +10,7 @@ package object annotation { ...@@ -10,7 +10,7 @@ package object annotation {
@ignore @ignore
class induct extends StaticAnnotation class induct extends StaticAnnotation
@ignore @ignore
class traceInduct extends StaticAnnotation class traceInduct(name: String = "") extends StaticAnnotation
@ignore @ignore
class ignore extends StaticAnnotation class ignore extends StaticAnnotation
@ignore @ignore
......
...@@ -5,34 +5,136 @@ package verification ...@@ -5,34 +5,136 @@ package verification
import purescala.Definitions._ import purescala.Definitions._
import purescala.Expressions._ import purescala.Expressions._
import purescala.Constructors._
import purescala.ExprOps._
import purescala.DefOps._
import purescala.Common._
import purescala.Types._
import purescala.TypeOps._
import purescala.Extractors._
import invariant.util.PredicateUtil._
import leon.utils._
/** /**
* This tactic applies only to non-recursive functions. * This tactic applies only to non-recursive functions.
* Inducts over the recursive calls of the first recursive procedure, in the body of `funDef` * Inducts over the recursive calls of the first recursive procedure in the body of `funDef`
*/ */
class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) { class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) {
val description : String = val description: String = "A tactic that performs induction over the recursions of a function."
val cg = vctx.program.callGraph
val defaultTactic = new DefaultTactic(vctx)
implicit protected val ctx = vctx.context def generatePostconditions(function: FunDef): Seq[VC] = {
assert(!cg.isRecursive(function) && function.body.isDefined)
def generateVCs(fd: FunDef): Seq[VC] = { val inductFunname = function.extAnnotations("traceInduct") match {
generatePostconditions(fd) ++ case Seq(Some(arg: String)) => Some(arg)
generatePreconditions(fd) ++ case a => None
generateCorrectnessConditions(fd)
}
def generatePostconditions(function: FunDef): Seq[VC]
def generatePreconditions(function: FunDef): Seq[VC]
def generateCorrectnessConditions(function: FunDef): Seq[VC]
protected def sizeLimit(s: String, limit: Int) = {
require(limit > 3)
// Crop the call to display it properly
val res = s.takeWhile(_ != '\n').take(limit)
if (res == s) {
res
} else {
res + " ..."
} }
// pritn debug info
if(inductFunname.isDefined)
ctx.reporter.debug("Extracting induction pattern from: "+inductFunname.get)(DebugSectionVerification)
if (function.hasPostcondition) {
// construct post(body)
val prop = application(function.postcondition.get, Seq(function.body.get))
val paramVars = function.paramIds.map(_.toVariable)
// extract the first recursive call when scanning `prop` AST from left to right
var funInv: Option[FunctionInvocation] = None
preTraversal {
case _ if funInv.isDefined =>
// do nothing
case fi @ FunctionInvocation(tfd, args) if cg.isRecursive(tfd.fd) // function is recurisve
&& args.forall(paramVars.contains) // all arguments should be parameters
&& args.toSet.size == args.size => // all arguments are unique
if (inductFunname.isDefined) {
if (inductFunname.get == tfd.fd.id.name)
funInv = Some(fi)
} else
funInv = Some(fi)
case _ =>
}(prop)
funInv match {
case None =>
ctx.reporter.warning("Cannot discover induction pattern! Falling back to normal tactic.")
defaultTactic.generatePostconditions(function)
case Some(finv) =>
// create a new function that realizes the tactic
val tactFun = new FunDef(FreshIdentifier(function.id.name + "-VCTact"), function.tparams,
function.params, BooleanType)
tactFun.precondition = function.precondition
// the body of tactFun is a conjunction of induction pattern of finv, and the property
val callee = finv.tfd.fd
val paramIndex = paramVars.zipWithIndex.toMap
val frame = finv.args.map { case v: Variable => v }
val footprint = paramVars.filterNot(frame.contains)
val indexedFootprint = footprint.map { a => paramIndex(a) -> a }.toMap
// the returned expression will have boolean value
def inductPattern(e: Expr): Expr = {
e match {
case IfExpr(c, th, el) =>
createAnd(Seq(inductPattern(c),
IfExpr(c, inductPattern(th), inductPattern(el))))
case MatchExpr(scr, cases) =>
val scrpat = inductPattern(scr)
val casePats = cases.map{
case MatchCase(pat, optGuard, rhs) =>
val guardPat = optGuard.toSeq.map(inductPattern _)
(guardPat, MatchCase(pat, optGuard, inductPattern(rhs)))
}
val pats = scrpat +: casePats.flatMap(_._1) :+ MatchExpr(scr, casePats.map(_._2))
createAnd(pats)
case Let(i, v, b) =>
createAnd(Seq(inductPattern(v), Let(i, v, inductPattern(b))))
case FunctionInvocation(tfd, args) =>
val argPattern = createAnd(args.map(inductPattern))
if (tfd.fd == callee) { // self recursive call ?
// create a tactFun invocation to mimic the recursion pattern
val indexedArgs = (args zip frame).map {
case (a, f) => paramIndex(f) -> a
}.toMap ++ indexedFootprint
val recArgs = (0 until indexedArgs.size).map(indexedArgs)
val recCall = FunctionInvocation(TypedFunDef(tactFun, tactFun.tparams.map(_.tp)), recArgs)
createAnd(Seq(argPattern, recCall))
} else {
argPattern
}
case Operator(args, op) =>
// conjoin all the expressions and return them
createAnd(args.map(inductPattern))
}
}
val argsMap = callee.params.map(_.id).zip(finv.args).toMap
val tparamMap = callee.tparams.zip(finv.tfd.tps).toMap
val inlinedBody = replaceFromIDs(argsMap,
instantiateType(callee.body.get, tparamMap, Map()))
val inductScheme = inductPattern(inlinedBody)
// add body, pre and post for the tactFun
tactFun.body = Some(createAnd(Seq(inductScheme, prop)))
tactFun.precondition = function.precondition
// postcondition is `holds`
val resid = FreshIdentifier("holds", BooleanType)
tactFun.postcondition = Some(Lambda(Seq(ValDef(resid)), resid.toVariable))
// print debug info if needed
ctx.reporter.debug("Autogenerated tactic fun: "+tactFun)(DebugSectionVerification)
// generate vcs using the tactfun
defaultTactic.generatePostconditions(tactFun) ++
defaultTactic.generatePreconditions(tactFun) ++
defaultTactic.generateCorrectnessConditions(tactFun)
}
} else Seq()
} }
def generatePreconditions(function: FunDef): Seq[VC] =
defaultTactic.generatePreconditions(function)
def generateCorrectnessConditions(function: FunDef): Seq[VC] =
defaultTactic.generateCorrectnessConditions(function)
} }
...@@ -71,12 +71,15 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] { ...@@ -71,12 +71,15 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
def generateVCs(vctx: VerificationContext, toVerify: Seq[FunDef]): Seq[VC] = { def generateVCs(vctx: VerificationContext, toVerify: Seq[FunDef]): Seq[VC] = {
val defaultTactic = new DefaultTactic(vctx) val defaultTactic = new DefaultTactic(vctx)
val inductionTactic = new InductionTactic(vctx) val inductionTactic = new InductionTactic(vctx)
val trInductTactic = new TraceInductionTactic(vctx)
val vcs = for(funDef <- toVerify) yield { val vcs = for(funDef <- toVerify) yield {
val tactic: Tactic = val tactic: Tactic =
if (funDef.annotations.contains("induct")) { if (funDef.annotations.contains("induct")) {
inductionTactic inductionTactic
} else { } else if(funDef.annotations.contains("traceInduct")){
trInductTactic
}else {
defaultTactic defaultTactic
} }
......
import leon.annotation._
import leon.lang._
import leon.collection._
object TraceInductTest {
sealed abstract class IList
case class ICons(head: BigInt, tail: IList) extends IList
case class INil() extends IList
// proved with unrolling=0
def size(l: IList): BigInt = (l match {
case INil() => BigInt(0)
case ICons(_, t) => 1 + size(t)
}) //ensuring(res => res >= 0)
@traceInduct
def nonNegSize(l: IList): Boolean = {
size(l) >= 0
} holds
def reverse0(l1: IList, l2: IList): IList = (l1 match {
case INil() => l2
case ICons(x, xs) => reverse0(xs, ICons(x, l2))
})
def content(l: IList): Set[BigInt] = l match {
case INil() => Set.empty[BigInt]
case ICons(x, xs) => Set(x) ++ content(xs)
}
@traceInduct("reverse0")
def revPreservesContent(l1: IList, l2: IList): Boolean = {
content(l1) ++ content(l2) == content(reverse0(l1, l2))
} holds
def insertAtIndex[T](l: List[T], i: BigInt, y: T): List[T] = {
require(0 <= i && i <= l.size)
l match {
case Nil() =>
Cons[T](y, Nil())
case _ if i == 0 =>
Cons[T](y, l)
case Cons(x, tail) =>
Cons[T](x, insertAtIndex(tail, i - 1, y))
}
}
// A lemma about `append` and `insertAtIndex`
@traceInduct("insertAtIndex")
def appendInsertIndex[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
require(0 <= i && i <= l1.size + l2.size)
(insertAtIndex((l1 ++ l2), i, y) == (
if (i < l1.size) insertAtIndex(l1, i, y) ++ l2
else l1 ++ insertAtIndex(l2, (i - l1.size), y)))
}.holds
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment