diff --git a/src/main/scala/leon/purescala/CallGraph.scala b/src/main/scala/leon/purescala/CallGraph.scala
index 9247f0071b4e87fa65f4f173c30256898ae73b46..63886dfd27c2eaf8af28bd993ab26de98cc9e873 100644
--- a/src/main/scala/leon/purescala/CallGraph.scala
+++ b/src/main/scala/leon/purescala/CallGraph.scala
@@ -37,6 +37,21 @@ class CallGraph(p: Program) {
def transitiveCallees(from: Set[FunDef]): Set[FunDef] = from.flatMap(transitiveCallees)
def transitiveCallers(to: Set[FunDef]): Set[FunDef] = to.flatMap(transitiveCallers)
+ lazy val stronglyConnectedComponents: Seq[Set[FunDef]] = {
+ def rec(funs: Set[FunDef]): Seq[Set[FunDef]] = {
+ if (funs.isEmpty) Seq()
+ else {
+ val h = funs.head
+ val component = transitiveCallees(h).filter{ transitivelyCalls(_, h) } + h
+ component +: rec(funs -- component)
+ }
+ }
+ rec(p.definedFunctions.toSet)
+ }
+
+ def stronglyConnectedComponent(fd: FunDef) =
+ stronglyConnectedComponents.find{ _.contains(fd) }.getOrElse(Set(fd))
+
private def init() {
_calls = Set()
_callers = Map()
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 3703464cf25e36c329203ffd39f5558825e4778b..daf7b84999f46bd6ebcd647e86477d5e383f18ff 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -4,9 +4,9 @@ package leon
package solvers
import utils.DebugSectionSolver
-import purescala.Expressions.Expr
+import purescala.Expressions._
import purescala.Common.Identifier
-
+import verification.VC
trait Solver {
def name: String
@@ -15,6 +15,9 @@ trait Solver {
implicit lazy val leonContext = context
def assertCnstr(expression: Expr): Unit
+ def assertVC(vc: VC) = {
+ assertCnstr(Not(vc.condition))
+ }
def check: Option[Boolean]
def getModel: Map[Identifier, Expr]
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 3bdc59d2556c528f74715d78b806d0118939a3b2..53239581b267bd8fce175541202e744809c2e4c0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -5,10 +5,11 @@ package solvers.smtlib
import purescala._
import Expressions._
-import Definitions.{Program, TypedFunDef}
+import Definitions._
import Constructors.{application, implies}
import DefOps.typedTransitiveCallees
-import smtlib.parser.Commands.{Assert => SMTAssert, _}
+import verification.VC
+import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
import smtlib.parser.Terms._
import smtlib.theories.Core.Equals
@@ -17,6 +18,13 @@ import smtlib.theories.Core.Equals
abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
override def targetName = "cvc4-quantified"
+
+ private var currentFunDef: Option[FunDef] = None
+ def refersToCurrent(fd: FunDef) = {
+ (currentFunDef contains fd) || (currentFunDef exists {
+ program.callGraph.transitivelyCalls(fd, _)
+ })
+ }
private val typedFunDefExplorationLimit = 10000
@@ -54,9 +62,9 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
}
}
- val seen = withParams filterNot functions.containsA
+ val notSeen = withParams filterNot functions.containsA
- val smtFunDecls = seen map { tfd =>
+ val smtFunDecls = notSeen map { tfd =>
val id = if (tfd.tps.isEmpty) {
tfd.id
} else {
@@ -85,12 +93,17 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
}
if (smtFunDecls.nonEmpty) {
+ //println("smtFuns: ")
+ //println(smtFunDecls map { _.name.name} mkString ", ")
+ //println(s"current: ${currentFunDef.get.id}")
sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
// Assert contracts for defined functions
for {
- tfd <- seen
+ // Exclude contracts of functions that refer to current to avoid unsoundness
+ tfd <- notSeen if !refersToCurrent(tfd.fd)
post <- tfd.postcondition
} {
+ //println(s"${tfd.id.uniqueName} does not refer to ${currentFunDef.get.id.uniqueName}")
val term = implies(
tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
@@ -119,4 +132,12 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
addError()
}
+ // We need to know the function context.
+ // The reason is we do not want to assume postconditions of functions referring to
+ // the current function, as this may make the proof unsound
+ override def assertVC(vc: VC) = {
+ currentFunDef = Some(vc.fd)
+ super.assertVC(vc)
+ }
+
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index c6a39924c7f5d289878f7403c346eb88e9ec3966..ce65a93bfe16269bb91b382429cc9197343cdb60 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -4,12 +4,12 @@ package leon
package verification
import purescala.Definitions._
-import purescala.Expressions._
import purescala.ExprOps._
import scala.concurrent.duration._
import solvers._
+import solvers.smtlib.SMTLIBCVC4QuantifiedSolver
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
@@ -38,7 +38,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
reporter.debug("Generating Verification Conditions...")
try {
- val vcs = generateVCs(vctx, filterFuns)
+ val vcs = generateVCs(vctx, filterFuns, forceGrouped = baseSolverF.getNewSolver.isInstanceOf[SMTLIBCVC4QuantifiedSolver])
reporter.debug("Checking Verification Conditions...")
@@ -48,13 +48,14 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
}
- def generateVCs(vctx: VerificationContext, filterFuns: Option[Seq[String]]): Seq[VC] = {
+ def generateVCs(vctx: VerificationContext, filterFuns: Option[Seq[String]], forceGrouped: Boolean = false): Seq[VC] = {
import vctx.reporter
import vctx.program
val defaultTactic = new DefaultTactic(vctx)
val inductionTactic = new InductionTactic(vctx)
+ val groupedTactic = new GroupedTactic(vctx)
def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
@@ -72,7 +73,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
val tactic: Tactic =
- if(funDef.annotations.contains("induct")) {
+ if (forceGrouped) {
+ groupedTactic
+ } else if(funDef.annotations.contains("induct")) {
inductionTactic
} else {
defaultTactic
@@ -138,7 +141,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val tStart = System.currentTimeMillis
- s.assertCnstr(Not(vcCond))
+ s.assertVC(vc)
val satResult = s.check
diff --git a/src/main/scala/leon/verification/GroupedTactic.scala b/src/main/scala/leon/verification/GroupedTactic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6ef63a8f8cdc4e9a21171e06e501387f8e684e52
--- /dev/null
+++ b/src/main/scala/leon/verification/GroupedTactic.scala
@@ -0,0 +1,90 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package verification
+
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Definitions._
+import purescala.Constructors._
+
+class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
+ val description = "Default verification condition generation approach"
+
+ def generatePostconditions(fd: FunDef): Seq[VC] = {
+ fd.postcondition map { post =>
+ val perFunc = for {
+ inComp <- vctx.program.callGraph.stronglyConnectedComponent(fd)
+ p <- inComp.postcondition
+ b <- inComp.body
+ } yield {
+ implies(
+ precOrTrue(inComp),
+ application(p, Seq(b))
+ )
+ }
+
+ VC(andJoin(perFunc.toSeq), fd, VCKinds.Postcondition, this).setPos(post)
+ }
+ }.toSeq
+
+ def generatePreconditions(fd: FunDef): Seq[VC] = {
+ fd.body match {
+ case Some(body) =>
+ val calls = collectWithPC {
+ case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get)
+ }(body)
+
+ calls.map {
+ case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
+ val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
+ val vc = implies(and(precOrTrue(fd), path), pre2)
+ val fiS = exprToShortString(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
+ }
+
+ case None =>
+ Nil
+ }
+ }
+
+ def generateCorrectnessConditions(fd: FunDef): Seq[VC] = {
+ fd.body match {
+ case Some(body) =>
+ val calls = collectWithPC {
+ case e @ Error(_, "Match is non-exhaustive") =>
+ (e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
+
+
+ case e @ Error(_, _) =>
+ (e, VCKinds.Assert, BooleanLiteral(false))
+
+ case a @ Assert(cond, Some(err), _) =>
+ val kind = if (err.startsWith("Map ")) {
+ VCKinds.MapUsage
+ } else if (err.startsWith("Array ")) {
+ VCKinds.ArrayUsage
+ } else if (err.startsWith("Division ")) {
+ VCKinds.DivisionByZero
+ } else {
+ VCKinds.Assert
+ }
+
+ (a, kind, cond)
+ case a @ Assert(cond, None, _) => (a, VCKinds.Assert, cond)
+ // Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
+ case a @ Ensuring(body, post) => (a, VCKinds.Assert, application(post, Seq(body)))
+ }(body)
+
+ calls.map {
+ case ((e, kind, errorCond), path) =>
+ val vc = implies(and(precOrTrue(fd), path), errorCond)
+
+ VC(vc, fd, kind, this).setPos(e)
+ }
+
+ case None =>
+ Nil
+ }
+ }
+}