Improvements to the termination checker

library/collection/List.scala

@@ -126,19 +126,22 @@ sealed abstract class List[T] {
     )
   }
 
-  private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = l match {
-    case Nil() =>
-      if (acc.size > 0) {
-        res :+ acc
-      } else {
-        res
-      }
-    case Cons(h, t) =>
-      if (s0 == BigInt(0)) {
-        chunk0(s, l, Nil(), res :+ acc, s)
-      } else {
-        chunk0(s, t, acc :+ h, res, s0-1)
-      }
+  private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = {
+    require(s > 0 && s0 >= 0)
+    l match {
+      case Nil() =>
+        if (acc.size > 0) {
+          res :+ acc
+        } else {
+          res
+        }
+      case Cons(h, t) =>
+        if (s0 == BigInt(0)) {
+          chunk0(s, t, Cons(h, Nil()), res :+ acc, s-1)
+        } else {
+          chunk0(s, t, acc :+ h, res, s0-1)
+        }
+    }
   }
 
   def chunks(s: BigInt): List[List[T]] = {
@@ -296,57 +299,75 @@ sealed abstract class List[T] {
     }
   }
 
-  def insertAt(pos: BigInt, l: List[T]): List[T] = (this match {
-    case Nil() => l
-    case Cons(h, t) =>
-      if (pos < 0) {
-        insertAt(size + pos, l)
-      } else if (pos == BigInt(0)) {
-        l ++ this
-      } else {
-        Cons(h, t.insertAt(pos - 1, l))
+  private def insertAtImpl(pos: BigInt, l: List[T]): List[T] = {
+    require(0 <= pos && pos <= size)
+    if(pos == BigInt(0)) {
+      l ++ this
+    } else {
+      this match {
+        case Cons(h, t) =>
+          Cons(h, t.insertAtImpl(pos-1, l))
+        case Nil() =>
+          l
       }
-  }) ensuring { res =>
+    }
+  } ensuring { res =>
     res.size == this.size + l.size &&
     res.content == this.content ++ l.content
   }
 
-  def insertAt(pos: BigInt, e: T): List[T] = (this match {
-    case Nil() => Cons[T](e, Nil())
-    case Cons(h, t) =>
-      if (pos < 0) {
-        insertAt(size + pos, e)
-      } else if (pos == BigInt(0)) {
-        Cons(e, this)
-      } else {
-        Cons(h, t.insertAt(pos - 1, e))
-      }
-  }) ensuring { res =>
+  def insertAt(pos: BigInt, l: List[T]): List[T] = {
+    require(-pos <= size && pos <= size)
+    if(pos < 0) {
+      insertAtImpl(size + pos, l)
+    } else {
+      insertAtImpl(pos, l)
+    }
+  } ensuring { res =>
+    res.size == this.size + l.size &&
+    res.content == this.content ++ l.content
+  }
+
+  def insertAt(pos: BigInt, e: T): List[T] = {
+    require(-pos <= size && pos <= size)
+    insertAt(pos, Cons[T](e, Nil()))
+  } ensuring { res =>
     res.size == this.size + 1 &&
     res.content == this.content ++ Set(e)
   }
 
-  def replaceAt(pos: BigInt, l: List[T]): List[T] = (this match {
-    case Nil() => l
-    case Cons(h, t) =>
-      if (pos < 0) {
-        replaceAt(size + pos, l)
-      } else if (pos == BigInt(0)) {
-        l ++ this.drop(l.size)
-      } else {
-        Cons(h, t.replaceAt(pos - 1, l))
+  private def replaceAtImpl(pos: BigInt, l: List[T]): List[T] = {
+    require(0 <= pos && pos <= size)
+    if (pos == BigInt(0)) {
+      l ++ this.drop(l.size)
+    } else {
+      this match {
+        case Cons(h, t) =>
+          Cons(h, t.replaceAtImpl(pos-1, l))
+        case Nil() =>
+          l
       }
-  }) ensuring { res =>
+    }
+  } ensuring { res =>
+    res.content.subsetOf(l.content ++ this.content)
+  }
+
+  def replaceAt(pos: BigInt, l: List[T]): List[T] = {
+    require(-pos <= size && pos <= size)
+    if(pos < 0) {
+      replaceAtImpl(size + pos, l)
+    } else {
+      replaceAtImpl(pos, l)
+    }
+  } ensuring { res =>
     res.content.subsetOf(l.content ++ this.content)
   }
 
   def rotate(s: BigInt): List[T] = {
     if (isEmpty) {
       Nil()
-    } else if (s < 0) {
-      rotate(size+s)
     } else {
-      drop(s) ++ take(s)
+      drop(s mod size) ++ take(s mod size)
     }
   } ensuring { res =>
     res.size == this.size

src/main/scala/leon/Main.scala

@@ -148,6 +148,7 @@ object Main {
     val synthesisF   = ctx.findOptionOrDefault(optSynthesis)
     val xlangF       = ctx.findOptionOrDefault(optXLang)
     val repairF      = ctx.findOptionOrDefault(optRepair)
+    val analysisF    = ctx.findOption(optVerify).isDefined && ctx.findOption(optTermination).isDefined
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
     val evalF        = ctx.findOption(SharedOptions.optEval)
@@ -181,6 +182,7 @@ object Main {
         if (noopF) RestoreMethods andThen FileOutputPhase
         else if (synthesisF) SynthesisPhase
         else if (repairF) RepairPhase
+        else if (analysisF) Pipeline.both(FunctionClosure andThen AnalysisPhase, TerminationPhase)
         else if (terminationF) TerminationPhase
         else if (xlangF) XLangAnalysisPhase
         else if (evalF.isDefined) EvaluationPhase
@@ -245,6 +247,10 @@ object Main {
 
       // Run pipeline
       pipeline.run(ctx)(args.toList) match {
+        case (vReport: verification.VerificationReport, tReport: termination.TerminationReport) =>
+          ctx.reporter.info(vReport.summaryString)
+          ctx.reporter.info(tReport.summaryString)
+
         case report: verification.VerificationReport =>
           ctx.reporter.info(report.summaryString)
 

src/main/scala/leon/Pipeline.scala

@@ -15,3 +15,16 @@ abstract class Pipeline[-F, +T] {
 
   def run(ctx: LeonContext)(v: F): T
 }
+
+object Pipeline {
+
+  def both[T, R1, R2](f1: Pipeline[T, R1], f2: Pipeline[T, R2]): Pipeline[T, (R1, R2)] = new Pipeline[T, (R1, R2)] {
+    def run(ctx : LeonContext)(t : T): (R1, R2) = {
+      val r1 = f1.run(ctx)(t)
+      // don't check for SharedOptions.optStrictPhases because f2 does not depend on the result of f1
+      val r2 = f2.run(ctx)(t)
+      (r1, r2)
+    }
+  }
+
+}

src/main/scala/leon/termination/ChainBuilder.scala

@@ -113,12 +113,12 @@ final case class Chain(relations: List[Relation]) {
   lazy val inlined: Seq[Expr] = inlining.map(_._2)
 }
 
-trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Strengthener with RelationComparator =>
+trait ChainBuilder extends RelationBuilder { self: Strengthener with RelationComparator =>
 
   protected type ChainSignature = (FunDef, Set[RelationSignature])
 
   protected def funDefChainSignature(funDef: FunDef): ChainSignature = {
-    funDef -> (self.program.callGraph.transitiveCallees(funDef) + funDef).map(funDefRelationSignature)
+    funDef -> (checker.program.callGraph.transitiveCallees(funDef) + funDef).map(funDefRelationSignature)
   }
 
   private val chainCache : MutableMap[FunDef, (Set[FunDef], Set[Chain], ChainSignature)] = MutableMap.empty
@@ -131,9 +131,9 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
       def decreasing(relations: List[Relation]): Boolean = {
         val constraints = relations.map(relation => relationConstraints.getOrElse(relation, {
           val Relation(funDef, path, FunctionInvocation(_, args), _) = relation
-          val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
-          val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(e1, e2)))) {
-            if (solver.definitiveALL(implies(andJoin(path), self.sizeDecreasing(e1, e2)))) {
+          val args0 = funDef.params.map(_.toVariable)
+          val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(args0, args)))) {
+            if (solver.definitiveALL(implies(andJoin(path), self.sizeDecreasing(args0, args)))) {
               StrongDecreasing
             } else {
               WeakDecreasing
@@ -153,7 +153,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
         val Relation(_, _, FunctionInvocation(tfd, _), _) :: _ = chain
         val fd = tfd.fd
 
-        if (!self.program.callGraph.transitivelyCalls(fd, funDef)) {
+        if (!checker.program.callGraph.transitivelyCalls(fd, funDef)) {
           Set.empty[FunDef] -> Set.empty[Chain]
         } else if (fd == funDef) {
           Set.empty[FunDef] -> Set(Chain(chain.reverse))

src/main/scala/leon/termination/ChainComparator.scala

@@ -10,7 +10,8 @@ import purescala.TypeOps._
 import purescala.Constructors._
 import purescala.Common._
 
-trait ChainComparator { self : StructuralSize with TerminationChecker =>
+trait ChainComparator { self : StructuralSize =>
+  val checker: TerminationChecker
 
   private object ContainerType {
     def unapply(c: ClassType): Option[(CaseClassType, Seq[(Identifier, TypeTree)])] = c match {
@@ -175,8 +176,8 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
         case NoEndpoint =>
           endpoint(thenn) min endpoint(elze)
         case ep =>
-          val terminatingThen = functionCallsOf(thenn).forall(fi => self.terminates(fi.tfd.fd).isGuaranteed)
-          val terminatingElze = functionCallsOf(elze).forall(fi => self.terminates(fi.tfd.fd).isGuaranteed)
+          val terminatingThen = functionCallsOf(thenn).forall(fi => checker.terminates(fi.tfd.fd).isGuaranteed)
+          val terminatingElze = functionCallsOf(elze).forall(fi => checker.terminates(fi.tfd.fd).isGuaranteed)
           val thenEndpoint = if (terminatingThen) ep max endpoint(thenn) else endpoint(thenn)
           val elzeEndpoint = if (terminatingElze) ep.inverse max endpoint(elze) else endpoint(elze)
           thenEndpoint max elzeEndpoint

src/main/scala/leon/termination/ChainProcessor.scala

@@ -8,20 +8,23 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors.tupleWrap
 
-class ChainProcessor(val checker: TerminationChecker with ChainBuilder with ChainComparator with Strengthener with StructuralSize) extends Processor with Solvable {
+class ChainProcessor(
+    val checker: TerminationChecker,
+    val modules: ChainBuilder with ChainComparator with Strengthener with StructuralSize
+) extends Processor with Solvable {
 
   val name: String = "Chain Processor"
 
   def run(problem: Problem) = {
     reporter.debug("- Strengthening postconditions")
-    checker.strengthenPostconditions(problem.funSet)(this)
+    modules.strengthenPostconditions(problem.funSet)(this)
 
     reporter.debug("- Strengthening applications")
-    checker.strengthenApplications(problem.funSet)(this)
+    modules.strengthenApplications(problem.funSet)(this)
 
     reporter.debug("- Running ChainBuilder")
     val chainsMap : Map[FunDef, (Set[FunDef], Set[Chain])] = problem.funSet.map { funDef =>
-      funDef -> checker.getChains(funDef)(this)
+      funDef -> modules.getChains(funDef)(this)
     }.toMap
 
     val loopPoints = chainsMap.foldLeft(Set.empty[FunDef]) { case (set, (fd, (fds, chains))) => set ++ fds }
@@ -48,15 +51,15 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
       reporter.debug("-+> Searching for structural size decrease")
 
       val (se1, se2s, _) = exprs(funDefs.head)
-      val structuralFormulas = checker.structuralDecreasing(se1, se2s)
+      val structuralFormulas = modules.structuralDecreasing(se1, se2s)
       val structuralDecreasing = structuralFormulas.exists(formula => definitiveALL(formula))
 
       reporter.debug("-+> Searching for numerical converging")
 
       // worth checking multiple funDefs as the endpoint discovery can be context sensitive
       val numericDecreasing = funDefs.exists { fd =>
         val (ne1, ne2s, fdChains) = exprs(fd)
-        val numericFormulas = checker.numericConverging(ne1, ne2s, fdChains)
+        val numericFormulas = modules.numericConverging(ne1, ne2s, fdChains)
         numericFormulas.exists(formula => definitiveALL(formula))
       }
 

src/main/scala/leon/termination/ComplexTerminationChecker.scala

@@ -8,23 +8,53 @@ import purescala.Expressions._
 
 import scala.collection.mutable.{Map => MutableMap}
 
-class ComplexTerminationChecker(context: LeonContext, program: Program)
-       extends ProcessingPipeline(context, program)
-          with StructuralSize
-          with RelationComparator
-          with ChainComparator
-          with Strengthener
-          with RelationBuilder
-          with ChainBuilder {
+class ComplexTerminationChecker(context: LeonContext, program: Program) extends ProcessingPipeline(context, program) {
 
   val name = "Complex Termination Checker"
   val description = "A modular termination checker with a few basic modules™"
 
+  val modules =
+        new StructuralSize
+       with ArgsSizeSumRelationComparator
+       with ChainComparator
+       with Strengthener
+       with RelationBuilder
+       with ChainBuilder 
+  {
+    val checker = ComplexTerminationChecker.this
+  }
+
+  val modulesLexicographic =
+        new StructuralSize
+       with LexicographicRelationComparator
+       with ChainComparator
+       with Strengthener
+       with RelationBuilder
+       with ChainBuilder 
+  {
+    val checker = ComplexTerminationChecker.this
+  }
+
+  val modulesBV =
+        new StructuralSize
+       with BVRelationComparator
+       with ChainComparator
+       with Strengthener
+       with RelationBuilder
+       with ChainBuilder 
+  {
+    val checker = ComplexTerminationChecker.this
+  }
+
   def processors = List(
-    new RecursionProcessor(this),
-    new RelationProcessor(this),
-    new ChainProcessor(this),
-    new LoopProcessor(this)
+    new RecursionProcessor(this, modules),
+    // RelationProcessor is the only Processor which benefits from trying a different RelationComparator
+    new RelationProcessor(this, modulesBV),
+    new RelationProcessor(this, modules),
+    new RelationProcessor(this, modulesLexicographic),
+    new ChainProcessor(this, modules),
+    new SelfCallsProcessor(this),
+    new LoopProcessor(this, modules)
   )
 
 }

src/main/scala/leon/termination/LoopProcessor.scala

@@ -10,16 +10,16 @@ import purescala.Constructors._
 
 import scala.collection.mutable.{Map => MutableMap}
 
-class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Strengthener with StructuralSize, k: Int = 10) extends Processor with Solvable {
+class LoopProcessor(val checker: TerminationChecker, val modules: ChainBuilder with Strengthener with StructuralSize, k: Int = 10) extends Processor with Solvable {
 
   val name: String = "Loop Processor"
 
   def run(problem: Problem) = {
     reporter.debug("- Strengthening applications")
-    checker.strengthenApplications(problem.funSet)(this)
+    modules.strengthenApplications(problem.funSet)(this)
 
     reporter.debug("- Running ChainBuilder")
-    val chains : Set[Chain] = problem.funSet.flatMap(fd => checker.getChains(fd)(this)._2)
+    val chains : Set[Chain] = problem.funSet.flatMap(fd => modules.getChains(fd)(this)._2)
 
     reporter.debug("- Searching for loops")
     val nonTerminating: MutableMap[FunDef, Result] = MutableMap.empty

src/main/scala/leon/termination/Processor.scala

@@ -26,16 +26,16 @@ trait Processor {
 
 trait Solvable extends Processor {
 
-  val checker : TerminationChecker with Strengthener with StructuralSize
+  val modules: Strengthener with StructuralSize
 
   private val solver: SolverFactory[Solver] = {
     val program     : Program     = checker.program
     val context     : LeonContext = checker.context
-    val sizeModule  : ModuleDef   = ModuleDef(FreshIdentifier("$size"), checker.defs.toSeq, false)
+    val sizeModule  : ModuleDef   = ModuleDef(FreshIdentifier("$size"), modules.defs.toSeq, false)
     val sizeUnit    : UnitDef     = UnitDef(FreshIdentifier("$size"),Seq(sizeModule)) 
     val newProgram  : Program     = program.copy( units = sizeUnit :: program.units)
 
-    SolverFactory.default(context, newProgram).withTimeout(500.millisecond)
+    SolverFactory.getFromSettings(context, newProgram).withTimeout(500.millisecond)
   }
 
   type Solution = (Option[Boolean], Map[Identifier, Expr])