epfl-lara / leon

The Leon system for verification, synthesis, repair

Leon 3.0

Getting Started

To build Leon you will need JDK, scala, sbt, and some external solver binaries. On Linux, it should already work out of the box.

To get started, see the documentation chapters, such as

• Getting Started
• Installation
• Introduction to Leon

For change log, see CHANGELOG.md

The Stainless/Inox Stack

Leon verification has recently been split off into

• Inox a backend solving layer, and
• Stainless a Scala frontend that supports contract-checking and termination proving.

Leon remains (for now) the main project for synthesis and repair as well as resource bounds inference. However, developpment of verification-related features will most likely be confined to the Stainless/Inox front.

leon's Issues

ListSpecs.reverseIndex does not terminate

In the body, there's the recursive call reverseIndex[T](l,i) which is identical to the initial invocation. --termination confirms that there is a counterexample. I tried fixing it, but to no avail so far.

Counter-example not well typed in presence of lambdas

Sorry for the long file, but it is hard to reproduce the problem.when removing lines in the code.
When running with --solvers=smt-cvc4 or --solvers=smt-z3, we obtain a counter-example

[Warning ] net -> VerifiedNetwork(MMap[BigInt, BigInt](VerifiedNetwork%28MMap[BigInt, BigInt]%28%28x$399 : BigInt%29 => None[BigInt]%28%29%29%29))

which is not well-typed (VerifiedNetwork is not recursive, and MMap should take a lambda as a parameter, not a VerifiedNetwork)

Note that there are quantifiers in "instantiate".

import leon.lang._
import leon.collection._
import leon.proof._
import leon.annotation._

import scala.language.postfixOps


object Networking {

  case class MMap[A,B](f: A => Option[B]) {

    def contains(k: A): Boolean = f(k) != None[B]()


    def getOrElse(k: A, v: B) = {
      if (contains(k)) f(k).get
      else v
    }
  }
  case class VerifiedNetwork(states: MMap[BigInt,BigInt]) 

  abstract class ActorId
  case class UID(uid: BigInt) extends ActorId


  abstract class Message
  case class Elected(i: BigInt) extends Message


  abstract class Actor {
    val myId: ActorId

  }
  case class PP(myId: ActorId) extends Actor


  def instantiate(n: BigInt, p: BigInt => Boolean): Boolean = {
    require(forall ((i: BigInt) => p(i)))

    true
  }


  def receivePre(n: BigInt, a: Actor, m: Message, net: VerifiedNetwork) = {

    val UID(myuid) = a.myId

    myuid < n && {
      val dummyVar = 0

      (instantiate(n, (i: BigInt) => net.states.contains(i)))  && (
        m match {
          case Elected(uid) => false
        })
    }
  }




  def applyMessage(
    messages: MMap[(ActorId,ActorId), List[Message]], 
    param: BigInt, 
    getActor: Actor, 
    sender: ActorId, 
    receiver: ActorId, 
    m: Message, 
    net: VerifiedNetwork): Boolean = {

    val sms = messages.getOrElse((sender,receiver), Nil())

    sms match {
      case Cons(x, xs) if (x == m) => 
        check(receivePre(param, getActor,m, net))

      case _ => 
        false
    }

  }

}

CallGraph doesn't track function calls in patterns

Consider this small program:

import leon.collection._
import leon.lang._

object Unapply {

  def check[A](xs: List[A]) = {
    xs match {
      case Nil() => true
      case _ :: _ => true
    }
  }.holds

}

The call graph does not contain the call from Unapply.check to ::.unapply, although it is being called through the pattern match. This problem didn't come up before because 75fc27a appears to be the first commit using an unapply pattern in the library.

Using TailRecursive printer in scala-smtlib

There is currently no simple option to switch to the TailRecursive printer in scala-smtlib when dealing with large smt specs (this should potentially be done automatically). Also changing the printer in SMTLIBSolver is not sufficient as the printers are hard-coded inside the interpreters in scala-smtlib.

Leon fails to verify simple list filtering

While doing SAV course project, we found Leon failed to verify following code:

  def test(list: List[BigInt], f: BigInt => Boolean): List[BigInt] = {
    list.filter(f)
  } ensuring { res =>
    res.forall(f) && list.forall(e => res.contains(e) == f(e))
  }

This may not necessarily be a bug, we report here just to let you know it.

Pure Scala

I know this is going to very tough and resource intensive.

Perhaps you could make this and ScalaZ3 functionality pure Scala without Z3 by porting or an alternative improved implementation.

Also perhaps provide IDE integration and keep it compatible with the main Scala release than a sub set. Since Scala can use classes not written in Scala perhaps a way to reason over Java bytecode. (Keep this generic as possible)

Perhaps this can at some point be part of the main Scala tool chain.

Pretty printing doesn't print annotation (arguments)

Since 3e4281d and #132, richer annotations are supported in Leon. The pretty printer hasn't caught up yet.

(Creating this issue to remind me that I should probably implement that.)

Use cla-assistant to manage CLAs

I see there is CLA.txt residing in the repository. I'm not aware how this is submitted.
https://cla-assistant.io/ helps easy management of CLAs and verifies CLA of contributor when a PR lands to the repository.

State#forever doesn't terminate

(... as the name already indicates)

The problem is that this function can't be defined in Isabelle

My personal opinion is that as long as Leon doesn't support codata, there probably shouldn't be any non-terminating functions in the library.

[Leon server] Missing 404 handler in leon.epfl.ch

Visit a random url, e.g. leon.epfl.ch/docs, and you get an error page

I suppose there's missing a onHandlerNotFound definition in the Global object.

Evaluation of passes fails to record positions of patterns, guards, scrutinees

The counter-example is not well displayed within the passes:

package leon.custom

import leon._
import leon.lang._
import leon.collection._
import leon.annotation._

sealed abstract class List[T] {  
  def count(e: T): BigInt = { this match {
    case Cons(h, t) =>
      if (h == e) {
        t.count(e)
      } else {
        t.count(e)
      }
    case Nil() =>
      BigInt(0)
  }} ensuring { res => 
    (((this, e), res) passes {
      case (Cons(a1, Cons(a2, Cons(a3, Cons(a4, Nil())))), v) if a1 == v && a2 == v && a3 != v && a4 == v => 3
      case (Cons(a1, Cons(a2, Nil())), v) if a1 != v && a2 != v => 0
    })
  }

}


case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]

PortfolioSolver with incremental smtlib solvers

Portfolio solvers cannot be used incrementally if the underlying solvers are smt-lib based.

The issue is that whenever portfolio runs check() it waits until the first solver finishes and then interrupts all other solvers (to make sure there is no out-of-order messages, e.g. assert while check). Since interrupt is implement in smt-lib solvers by killing the smt process, solvers become unusable for subsequent commands and thus cannot be used incrementally.

Add doc for @traceInduct

leon.collection.List.foldRight inconsistent with scala.collection.immutable.List.foldRight

The signature of scala.collection.immutable.List.foldRight is

  override def foldRight[B](z: B)(op: (A, B) => B): B

while for leon.collection.List.foldRight it's

  def foldRight[R](f: (T,R) => R)(z: R): R

It would be nice to have the two consistent with each other.

leon.lang.Map.getOrElse missing

The method Map.getOrElse is missing in leon.lang.Map.

Fatal error with class invariants

import leon.lang._

object Test  {

  case class DefinedAtZero(m: Map[BigInt,BigInt])  {
    require(m.contains(0))

  }

  def receive(m: DefinedAtZero) = {
    m 
  } ensuring(res => res.m(0) == 5)
}

I obtain the empty map as a counter-example to function "receive" (not a valid counter-example, because it's not defined at zero)
Using option --checkmodels produces a fatal error

[Warning ] - Model leads to evaluation error: Stack overflow
[ Error ] Something went wrong. The model should have been valid, yet we got this: Model(
[ Error ] m -> DefinedAtZero(MapBigInt,BigInt)
[ Error ] ) for formula m.m(BigInt(0)) != BigInt(5)
[Warning ] => UNKNOWN
[ Fatal ] There were errors.

Is this a known issue?
Thanks

evaluation and verification don't agree on modulo

Consider this:

import leon.lang._

object Test {
  def m = BigInt(-1) % 3

  def claim1 = {
    m == 2
  }.holds

  def claim2 = {
    m == -1
  }.holds
}

Verification says that claim1 is invalid and claim2 is valid. That's what I'd expect, because as mentioned here, leon follows Scala/Java and treats '%' as remainder, not modulo.

But running with --eval, I get

[  Info  ]  - Evaluating m
[  Info  ]   => 2

which contradicts the verification results.

Tested on latest commit on master (0699558).

Analyze division by zero-bitvector, modulo/remainder by zero

In this example, Leon tells us that in b1, no division by zero will occur. But it could also analyze the other cases for division or modulo by zero.

object Test {
  def b1: BigInt = BigInt(5) / BigInt(2)
  def b2: BigInt = BigInt(5) % BigInt(2)
  def b3: BigInt = BigInt(5) mod BigInt(2)

  def i1: Int = 5 / 2
  def i2: Int = 5 % 2
}

[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ b1     division by zero                       3:20       valid        Z3-f           0.025 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 1      valid: 1      invalid: 0      unknown 0                                0.025 ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝

[Not so important, just a little enhancement ;-)]

No guard against circular logic proofs

Ensuring clauses that create circular logic should be disallowed at some point during verification.
For example:

def commutative(x: Int, y: Int): Int = {
  if (x > y) x else 0
} ensuring { res => res == commutative(y, x) }

will be proved valid by Leon!

Termination issue

It seems that Leon incorrectly proves the termination of testEvolution in the following example:

import leon.collection._
import leon.lang._
import leon.annotation._

import scala.language.postfixOps

object Termination {

  case class Task(tick: BigInt) {
    require(tick >= 0)
    // removing the ADT invariant makes Leon correctly prove non-termination
    // of testEvolution
  }

  case class Core(tasks: Task, current: Option[BigInt]) 


  def insertBack(): Core = Core(Task(0), None())


  def testEvolution(c: Core): Core = {
    c.current match {
      case Some(_) => testEvolution(c)
      case None() => insertBack()
    }
  }

  @ignore
  def main(args: Array[String]) {
    testEvolution(Core(Task(0), Some(0)))
  }

}

leon --termination Term.scala
testEvolution  ✓ Terminates (Relation Processor comparing outer structural sizes of argument types)

(Infinite loop may occur if c.current is defined, which might be the case.)

The issue seems to come from the "require(tick >= 0)" in class Task.

Thanks :)

Counterexample does not violate precondition of lambda passed to HOF

In this example

import leon.collection._

object Test {

  def id(x: BigInt): BigInt = {
    require(x >= 2)
    x
  }

  def go(start: BigInt): List[BigInt] = {
    require(start >= 2)
    Cons(start, Nil()).map(id)
  }

  // let's --eval this:
  def c1 = go(2)
}

Leon says it found a counter-example:

[  Info  ]  - Now considering 'precond. (call id(x))' VC for go @15:28...
[ Error  ]  => INVALID
[ Error  ] Found counter-example:
[ Error  ]   start -> 2
[ Error  ]   x     -> 0
[  Info  ]  - Now considering 'precond. (call go(2))' VC for c1 @19:12...
[  Info  ]  => VALID
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ c1    precond. (call go(2))                   19:12      valid          Z3-f         0.004 ║
[  Info  ] ║ go    precond. (call id(x))                   15:28      invalid        Z3-f         0.023 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2      valid: 1      invalid: 1      unknown 0                                0.027 ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝

If I understand correctly, it says that the call to id in Cons(start, Nil()).map(id) does not respect the precondition of id. But it does, because start is required to be >= 2.

Missing import statement in documentation example

In the Induction section of Proving Theorems, the below example does not make a reference to leon.proof:

import leon.collection._ // for List
import leon.lang._       // for holds

object Example {
  def reverseReverse[T](l: List[T]): Boolean = {
    l.reverse.reverse == l
  }.holds
}

Which is then needed in the following steps (for because, check and trivial calls):

def reverseReverse[T](l: List[T]): Boolean = {
  l.reverse.reverse == l because {
    l match {
      case Nil()       => check {  Nil[T]().reverse.reverse == Nil[T]()  }
      case Cons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
    }
  }
}.holds

def reverseReverse[T](l: List[T]): Boolean = {
  l.reverse.reverse == l because {
    l match {
      case Nil()       => trivial
      case Cons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
    }
  }
}.holds

ADTLongInduction fails on Church.Add

ADTLongInduction generates non-sense on Church.Add

./leon --synthesis --manual src/test/resources/regression/synthesis/Church/Add.scala

7

should rewrite and generalize to K-induction at the same time, recorded as an issue so we don't forget.

Fails to produce a list of alternatives to synthesize

./leon --synthesis --manual 

fails to quickly produce a list of applicable rules, maybe due to the amount of Num variables, on the following input:

/* Copyright 2009-2014 EPFL, Lausanne */

import leon.lang._
import leon.lang.synthesis._

object ChurchNumerals {
  sealed abstract class Num
  case object Z extends Num
  case class  S(pred: Num) extends Num

  def value(n:Num) : Int = {
    n match {
      case Z => 0
      case S(p) => 1 + value(p)
    }
  } ensuring (_ >= 0)

  // def add(x : Num, y : Num) : Num = (x match {
  //   case Z => y
  //   case S(p) => add(p, S(y))
  // }) ensuring (value(_) == value(x) + value(y))

  def rec(y: Num, x: Num, y2: Num, x2: Num): Num = {
    y match {
      case S(pred) =>
        val r = rec(pred, x, y2, x2);
        choose((r: Num) => (value(r) == value(x) + value(S(pred))))
      case _ =>
         Z
    }
  } ensuring {
    (res: Num) => value(res) == value(x) + value(y)
  }
  def add(x: Num, y: Num): Num = {
    rec(y, x, y, x)
  }
}

Map#get vs. Map#apply

From the library:

case class Map[A, B] (theMap: scala.collection.immutable.Map[A,B]) {
  def apply(k: A): B = ...
  def get(k: A): Option[B] = ...
}

From the AST:

/** $encodingof `map.get(key)` */
case class MapGet(map: Expr, key: Expr) extends Expr {
  val getType = map.getType match {
    case MapType(from, to) if isSubtypeOf(key.getType, from) =>
      to
    case _ => Untyped
  }
}

From code extraction:

case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
  MapGet(a1, a2)

It appears to me that this is actually the encoding of map.apply(key). I would suggest changing the comment and the name of the class.

Termination checker is unsound in handling streams

Given a variable v having case class type that has a field f of function type say Unit => A.
The termination checker assumes that v.f() is a structurally smaller term than v. This basically stems from the assumption of well-founded types.

Feature Request: Class State Invariant

I'm not sure if this is the right place to ask for a feature. The problem I encountered is that I want to impose a constraint on all instances of a class. For example, in the following I'd like isValid to hold for all instances of GoSet.

case class GoSet[T](elements: List[T]) {
  def isValid: Boolean = {
    if (isEmpty) true
    else !GoSet(elements.tail).contains(elements.head) && GoSet(elements.tail).isValid
  }
}

As far as I know currently Leon doesn't support specifying an invariant on a class, so I have to duplicate require(isValid) at the beginning of each member method. With the support of class state invariant, it not only helps save duplicate code, but also enables programmers to think about verification at a higher abstraction level.

From the functional point of view, the class invariant are actually the post-condition of the constructor of the class(assume immutable objects). It seems this is theoretically possible for immutable objects, but I'm not sure about the details.

Thanks.

Missing filename from compiler errors/warnings

The compiler error messages do not include the filename, which can be tiring when debugging an issue. For instance, compare the message from scalac:

[warn] /leon-go/src/main/scala/go/core/CaptureLogic.scala:97: a pure expression does nothing in statement position; you may be omitting necessary parentheses
[warn]       "which file???"
[warn]       ^
[warn] one warning found

and leon:

[Warning ] 97:7: warning: a pure expression does nothing in statement position; you may be omitting necessary parentheses
                 "which file???"
                 ^
[ Error  ] 97:7: Block expressions require xlang desugaring
                 "which file???"
                 ^^^^^^^^^^^^^^^...
[ Fatal  ] There were errors.

I prefer the message from scalac.

List.find(lambda) is of type <untyped>

Maybe related to #203 .

Small example:

  import leon.collection._
  import leon.lang._

  object Scheduler {
    case class Core(var tasks: List[BigInt], var current: Option[BigInt]) {
    }

    def willBeScheduled(c: Core, j: BigInt, i: BigInt) : Unit = {
       require(!c.tasks.isEmpty)
       require(c.tasks.find(j) == Some(i))

       while(c.current != Some(j)) {
          c.current = c.tasks.find((i:BigInt) => i == j);
       }
    }
  }

==>

  java.lang.AssertionError: assertion failed: lt$28 == lt$27.tasks.find(lambda$0) is not of type Boolean. lt$28 == lt$27.tasks$0.find$3(lambda$0) is of type <untyped>
        lt$28 is of type Option$0[Task$0]
        lt$27.tasks$0.find$3(lambda$0) is of type <untyped>
          lt$27.tasks$0 is of type List$0[Task$0]
            lt$27 is of type Core$0

leon.codegen.CompilationException: Unsupported expr. : a.updated(0, 2)

I get the above error with the following benchmark:

import leon.Utils._
object Test {
  def test(a: Array[Int]): Int = {
    val a2 = a.updated(0, 2)
    12
  }
}

and the following command:

./leon --codegen --evalground --feelinglucky Test.scala

CodeGeneration does not seem to implement functional update to arrays.

java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path

I built leon on my machine (MacOSX Yosemite, 10.10.3)
I see that the leon script includes in the SCALACLASSPATH.
To make it easier to see what's going on, I edited the leon script like this:

#!/bin/bash --posix

LEON=/Users/rouquett/git.leon/leon
IVY_CACHE=/Users/rouquett/.ivy2/cache

SCALACLASSPATH="$LEON/src/main/resources"
SCALACLASSPATH="$SCALACLASSPATH:$LEON/target/scala-2.11/classes"
SCALACLASSPATH="$SCALACLASSPATH:/Users/rouquett/.sbt/0.13/staging/572f4374f25249fa2000/bonsai/target/scala-2.11/classes"
SCALACLASSPATH="$SCALACLASSPATH:/Users/rouquett/.sbt/0.13/staging/4b46b695466923d859a4/scala-smtlib/target/scala-2.11/classes" 
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/cafebabe_2.11-1.2.jar" 
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/scalaz3-unix-64b-2.1.jar"
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/vanuatoo_2.11-0.1.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-compiler/jars/scala-compiler-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-library/jars/scala-library-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-reflect/jars/scala-reflect-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang.modules/scala-xml_2.11/bundles/scala-xml_2.11-1.0.3.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang.modules/scala-parser-combinators_2.11/bundles/scala-parser-combinators_2.11-1.0.3.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/com.typesafe.akka/akka-actor_2.11/jars/akka-actor_2.11-2.3.4.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/com.typesafe/config/bundles/config-1.2.1.jar"

java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} leon.Main $@ 2>&1 | tee -i last.log

Then I get this:

[504] $ ./leon.sh  ./testcases/verification/sas2011-testcases/RedBlackTree.scala
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
    at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at leon.solvers.z3.FairZ3Solver.<init>(FairZ3Solver.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1$$anon$1.<init>(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anon$12.getNewSolver(SolverFactory.scala:18)
    at leon.verification.AnalysisPhase$.checkVC(AnalysisPhase.scala:129)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:111)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:110)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at leon.verification.AnalysisPhase$.checkVCs(AnalysisPhase.scala:110)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:45)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:15)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:236)
    at leon.Main$.main(Main.scala:220)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

Suggestions?

• Nicolas.

Not-so-transitive call-graph

lazy val (transitiveCallGraph, transitiveCallers, transitiveCallees) = {
      var resSet : Set[(FunDef,FunDef)] = callGraph
      var change = true

      while(change) {
        change = false
        for(f1 <- definedFunctions; f2 <- callers(f1); f3 <- callees(f1)) {
          if(!resSet(f2,f3)) {
            change = true
            resSet = resSet + ((f2,f3))
          }
        }
      }
//...

Given a call-graph A->B->C->D, only A,C and B,D will be added to the original callgraph.
Since callers/callees do not change, this is actually no fix-point.

Termination checker unable to prove termination of mutually recursive functions

I get ✗ NoGuarantee for both the functions below:

  @invstate
  def maxValue(items: IList, w: BigInt, currList: IList): BigInt = {
    require((w ==0 || (w > 0 && deps(w - 1, items))) &&
      // lemma inst
      (currList match {
        case Cons((wi, vi), _) =>
          if (wi <= w && wi > 0) depsLem(w - wi, w - 1, items)
          else true
        case Nil() => true
      }))
    currList match {
      case Cons((wi, vi), tail) =>
        val oldMax = maxValue(items, w, tail)
        if (wi <= w && wi > 0) {
          val choiceVal = vi + knapSack(w - wi, items)
          if (choiceVal >= oldMax)
            choiceVal
          else
            oldMax
        } else oldMax
      case Nil() => BigInt(0)
    }
  } ensuring(_ => time <= ? * currList.size + ?) 

  @memoize
  def knapSack(w: BigInt, items: IList): BigInt = {
    require(w >= 0 && (w == 0 || deps(w - 1, items)))
    if (w == 0) BigInt(0)
    else {
      maxValue(items, w, items)
    }
  } ensuring(_ => time <= ? * items.size + ?)

Any help?

Both are in fact terminating and the times bounds are also inferred.

Termination -- java.lang.IllegalArgumentException

Tested with 9566dcf

With Order.scala (the file is not minimal, but hopefully not too hard to debug :) ) The problem is raised by the termination verification of testEvolutionSimple.

../leon/leon --termination Order.scala 
java.lang.IllegalArgumentException: Comparison method violates its general contract!
    at java.util.TimSort.mergeHi(TimSort.java:899)
    at java.util.TimSort.mergeAt(TimSort.java:516)
    at java.util.TimSort.mergeForceCollapse(TimSort.java:457)
    at java.util.TimSort.sort(TimSort.java:254)
    at java.util.Arrays.sort(Arrays.java:1438)
    at scala.collection.SeqLike$class.sorted(SeqLike.scala:648)
    at scala.collection.AbstractSeq.sorted(Seq.scala:41)
    at scala.collection.SeqLike$class.sortWith(SeqLike.scala:601)
    at scala.collection.AbstractSeq.sortWith(Seq.scala:41)
    at leon.termination.Strengthener$class.strengthenPostconditions(Strengthener.scala:25)
    at leon.termination.ComplexTerminationChecker$$anon$3.strengthenPostconditions(ComplexTerminationChecker.scala:34)
    at leon.termination.RelationProcessor.run(RelationProcessor.scala:21)
    at leon.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:189)
    at leon.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:182)
    at scala.collection.Iterator$$anon$13.hasNext(Iterator.scala:462)
    at scala.collection.Iterator$class.foreach(Iterator.scala:893)
    at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
    at leon.termination.ProcessingPipeline.verifyTermination(ProcessingPipeline.scala:216)
    at leon.termination.ProcessingPipeline$$anonfun$5$$anonfun$apply$4.apply(ProcessingPipeline.scala:144)
    at leon.termination.ProcessingPipeline$$anonfun$5$$anonfun$apply$4.apply(ProcessingPipeline.scala:143)
    at scala.Option.getOrElse(Option.scala:121)
    at leon.termination.ProcessingPipeline$$anonfun$5.apply(ProcessingPipeline.scala:142)
    at leon.termination.ProcessingPipeline$$anonfun$5.apply(ProcessingPipeline.scala:133)
    at scala.Option.getOrElse(Option.scala:121)
    at leon.termination.ProcessingPipeline.terminates(ProcessingPipeline.scala:133)
    at leon.termination.TerminationPhase$$anonfun$4.apply(TerminationPhase.scala:29)
    at leon.termination.TerminationPhase$$anonfun$4.apply(TerminationPhase.scala:28)
    at scala.collection.immutable.List.map(List.scala:277)
    at leon.termination.TerminationPhase$.apply(TerminationPhase.scala:28)
    at leon.termination.TerminationPhase$.apply(TerminationPhase.scala:8)
    at leon.SimpleLeonPhase$class.run(LeonPhase.scala:14)
    at leon.termination.TerminationPhase$.run(TerminationPhase.scala:8)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:267)
    at leon.Main$.main(Main.scala:251)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

Closures inside case classes

The theorem in this example https://leon.epfl.ch#link/97f9f0f73378d23ca2eee6f7806dbfb7-1 is Invalid according to leon (github version), while it should be valid.

Defining the variable client as given in the commentary makes leon say (correctly) that the theorem is valid.

For some reason, on leon-web, this issue doesn't appear (github version, or online version).

Adding ensuring(rec < ...) in a function prevents other functions from being verified

Strange issue :)

   def insertBack(c: Core, t: Task): Core = {
      require(!contains(c.tasks, t))
      if(containsEquivLemma(c.tasks, t, tick(t))) {
         Core(c.id, sortedIns(c.tasks, tick(t)), None[Task]())
      } else {
         error[Core]("Tick changes task id\n");
      }
   }

   def test(c: Core): Core = {
      c
   } ensuring(rec < 5);

Without the "test" function insertBack is successfully verified by Leon. Adding test prevents insertBack from being verified. The issue is due to the "rec < 5".

Here is a more complete example:
Scheduler-simple.txt
(If you comment the "test" function, the code verifies.)

I've tried comparing the --instrument output with and without the test function. The layout is different, but I haven't spotted any significant change (might be worth double-checking though).

git bisect blames 0ba77a2 for the problem.

leon with isabelle, undefined session, documentation

Dear All,

I am trying to use leon to generate Isabelle thy files from some scala source. Compilation is fine. I can run leon using cvc4 on Addresses.scala and it seems to work. Now I want to run Isabelle.

• There doesn't seem to be much documentation on how to do this

I try the following, and get an error:

tr61@pc1177:/tmp/l/git/github/other/leon$ ./leon --solvers=isabelle testcases/verification/Addresses.scala 
./leon --solvers=isabelle testcases/verification/Addresses.scala 
[Warning ] warning: there were two feature warnings; re-run with -feature for details
[  Info  ] Preparing Isabelle setup (this might take a while) ...
[  Info  ] Building session ...
ERROR(Undefined session(s): "Leon")
    at isabelle.Library$ERROR$.apply(library.scala:33)
    at isabelle.Library$.error(library.scala:37)
    at isabelle.Basic_Library$$anonfun$2.apply(library.scala:223)
    at isabelle.Basic_Library$$anonfun$2.apply(library.scala:223)
    at isabelle.Build$Session_Tree.selection(build.scala:149)
    at isabelle.Build$.build_results(build.scala:758)
    at isabelle.Build$.build(build.scala:1001)
    at edu.tum.cs.isabelle.impl.Environment.build(Environment.scala:46)
    at edu.tum.cs.isabelle.System$.build(System.scala:38)
    at leon.solvers.isabelle.IsabelleEnvironment$$anonfun$4$$anonfun$apply$1.apply(IsabelleEnvironment.scala:69)
    at leon.solvers.isabelle.IsabelleEnvironment$$anonfun$4$$anonfun$apply$1.apply(IsabelleEnvironment.scala:67)
    at scala.concurrent.Future$$anonfun$flatMap$1.apply(Future.scala:253)
    at scala.concurrent.Future$$anonfun$flatMap$1.apply(Future.scala:251)
    at scala.concurrent.impl.CallbackRunnable.run(Promise.scala:32)
    at scala.concurrent.impl.ExecutionContextImpl$AdaptedForkJoinTask.exec(ExecutionContextImpl.scala:121)
    at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
    at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.pollAndExecAll(ForkJoinPool.java:1253)
    at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1346)
    at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
    at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)

• What am I doing wrong?

Merge request for list library methods and lemmas

I have added some methods and lemmas to list library. I do not use a fork of Leon (because I already have a fork that uses a older version of leon), so I cannot give a pull request.
But, the following can be merged easily merged with leon (it is made on top of the recent leon commit).
ravimad/leon2015@73289a8

Cryptic error message: "Don't know what to do with this. Not purescala?"

The following code produces the error message: "Don't know what to do with this. Not purescala?"

import leon.lang._
import leon.annotation._

sealed abstract class Cell
case object WhiteCell extends Cell

Moving the class definition into a module

import leon.lang._
import leon.annotation._

object Foo {
  sealed abstract class Cell
  case object WhiteCell extends Cell
}

fixes the issue.

CodeGenPhase is dead code

leon.codegen.CodeGenPhase appears to be unused and untested; no mention of it anywhere in the source code.

--eval crashes with lambdas

Verification accepts the following program:

import leon.lang._

object Test {
  val foo = (x: BigInt) => x

  def lemma1(x: BigInt) = {
    foo(x) == x
  }.holds
}

But with --eval, I get an error:

[  Info  ]  - Evaluating foo
leon.codegen.CompilationException: Unsupported return value : class Leon$CodeGen$Lambda$5 while expecting (BigInt) => BigInt
    at leon.codegen.CompilationUnit.jvmToExpr(CompilationUnit.scala:247)
    at leon.codegen.CompiledExpression.evalFromJVM(CompiledExpression.scala:48)
    at leon.codegen.CompiledExpression.eval(CompiledExpression.scala:58)
    at leon.evaluators.CodeGenEvaluator$$anonfun$compile$1.apply(CodeGenEvaluator.scala:43)
    at leon.evaluators.CodeGenEvaluator$$anonfun$compile$1.apply(CodeGenEvaluator.scala:41)
    at leon.evaluators.CodeGenEvaluator$$anonfun$eval$2.apply(CodeGenEvaluator.scala:27)
    at leon.evaluators.CodeGenEvaluator$$anonfun$eval$2.apply(CodeGenEvaluator.scala:24)
    at scala.Option.map(Option.scala:146)
    at leon.evaluators.CodeGenEvaluator.eval(CodeGenEvaluator.scala:24)
    at leon.evaluators.Evaluator.eval(Evaluator.scala:18)
    at leon.evaluators.EvaluationPhase$$anonfun$run$1.apply(EvaluationPhase.scala:36)
    at leon.evaluators.EvaluationPhase$$anonfun$run$1.apply(EvaluationPhase.scala:33)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at leon.evaluators.EvaluationPhase$.run(EvaluationPhase.scala:33)
    at leon.evaluators.EvaluationPhase$.run(EvaluationPhase.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:248)
    at leon.Main$.main(Main.scala:232)
    at leon.Main.main(Main.scala)

Forget setting type after reconstructing exprs

I got an error (when trying to call simplifyLets function in the test case src/test/resources/regression/verification/xlang/valid/Epsilon4.scala )

I edited file leon / src / main / scala / leon / purescala / TreeOps.scala by setting type for builder constructor (you can search with builder keyword)

I just sure that it fixed the error in my cases :)

TODO exception with Map's and class Invariants

import leon.lang._

object TODO {

  def contains(m: Map[BigInt,Actor], id: BigInt) = {
    m.contains(id)
  } holds

  case class Actor(myId: BigInt) {
    require(myId == 0)
  }

}

The problem seems to be in DatatypeManager.scala in the typeUnroller function (missing Map case).
What does this function do?

ensuring(rec <= ...) -- big verification time variation

Using 624e5a7

I am trying to prove that a function terminates by ensuring that "rec <= someValue". The time to check the postcondition varies a lot : checking the exact same file, it might take between 30s and 700s to validate the property (I might also have had some runs in which the validator never ends).

I know that this is a pretty vague issue, but if you have any idea on how to report more precise data, I can try it :)

Scheduler.txt

leon Scheduler.scala --functions=testEvolutionSimpleProofRec

Run1: [  Info  ] ║ Scheduler.testEvolutionSimpleProofRec  postcondition                                         348:14  valid      Z3-f  701.587 ║
Run2: [  Info  ] ║ Scheduler.testEvolutionSimpleProofRec  postcondition                                         348:14  valid  Z3-f  139.560 ║

Some timings also surprise me:

def testEvolutionSimple(...) {
   if(timer(c).current == Some(e)) {
      c
    } else if (find(doubleTimer(c,e).tasks, e).get == find(c.tasks, e).get - 1) {
      doubleTimer(c,e)
    } else if(rec <= maxSumBeforeSorted(c.tasks, e)) {
       testEvolutionSimple(c2, e);
    } else {
       error[Core]("Cannot happen :)"); 
    }
} ensuring(rec <= maxSumBeforeSorted(c.tasks, e) + 1)

On that code, the body assertion is always much faster than checking the postcondition, while the postcondition seems easier to check (it derives directly from the ifs). Any insight on why this is the case?

All tests are done on a fairly recent desktop machine with 8 cores.

Use SMTLIB solvers in Orb to prevent solver handups and JVM crashes

smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file

To reproduce: Change the following definition from the List library:

   def contains(v: T): Boolean = (this match {
-    case Cons(h, t) if h == v => true
-    case Cons(_, t) => t.contains(v)
+    case Cons(h, t) => h == v || t.contains(v)
     case Nil() => false
   }) ensuring { _ == (content contains v) }

Then run regression:test. test and integration:test are fine. @vkuncak suggested this change.

(reproducible under fcac011)

Compilation issue

The following file results in a java.util.NoSuchElementException:

import leon.collection._
import leon.lang._
import scala.Any
import leon.annotation._
import leon.proof._
import leon.instrumentation._
import leon.invariant._
import leon.util.Random

object Test {
   val seed:Random.State = Random.State(0);
   val t:T = T(Random.nextBigInt(seed));

   case class T(n:BigInt) {
      require(n >= 0);
   }
}

$ leon test.scala 
java.util.NoSuchElementException: None.get
    at scala.None$.get(Option.scala:347)
    at scala.None$.get(Option.scala:345)
    at leon.xlang.AntiAliasingPhase$$anonfun$24.apply(AntiAliasingPhase.scala:271)
    at leon.xlang.AntiAliasingPhase$$anonfun$24.apply(AntiAliasingPhase.scala:269)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at leon.xlang.AntiAliasingPhase$.leon$xlang$AntiAliasingPhase$$mapApplication$1(AntiAliasingPhase.scala:269)
    at leon.xlang.AntiAliasingPhase$$anonfun$leon$xlang$AntiAliasingPhase$$makeSideEffectsExplicit$1.apply(AntiAliasingPhase.scala:410)
    at leon.xlang.AntiAliasingPhase$$anonfun$leon$xlang$AntiAliasingPhase$$makeSideEffectsExplicit$1.apply(AntiAliasingPhase.scala:300)
    at leon.purescala.GenTreeOps$class.rec$2(GenTreeOps.scala:329)
    at leon.purescala.GenTreeOps$$anonfun$15.apply(GenTreeOps.scala:335)
    at leon.purescala.GenTreeOps$$anonfun$15.apply(GenTreeOps.scala:335)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at leon.purescala.GenTreeOps$class.rec$2(GenTreeOps.scala:335)
    at leon.purescala.GenTreeOps$class.preMapWithContext(GenTreeOps.scala:345)
    at leon.purescala.ExprOps$.preMapWithContext(ExprOps.scala:35)
    at leon.xlang.AntiAliasingPhase$.leon$xlang$AntiAliasingPhase$$makeSideEffectsExplicit(AntiAliasingPhase.scala:475)
    at leon.xlang.AntiAliasingPhase$$anonfun$13.apply(AntiAliasingPhase.scala:203)
    at leon.xlang.AntiAliasingPhase$$anonfun$13.apply(AntiAliasingPhase.scala:202)
    at scala.Option.map(Option.scala:146)
    at leon.xlang.AntiAliasingPhase$.leon$xlang$AntiAliasingPhase$$updateBody(AntiAliasingPhase.scala:202)
    at leon.xlang.AntiAliasingPhase$$anonfun$apply$3.apply(AntiAliasingPhase.scala:93)
    at leon.xlang.AntiAliasingPhase$$anonfun$apply$3.apply(AntiAliasingPhase.scala:91)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at leon.xlang.AntiAliasingPhase$.apply(AntiAliasingPhase.scala:91)
    at leon.TransformationPhase.run(LeonPhase.scala:22)
    at leon.TransformationPhase.run(LeonPhase.scala:17)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.xlang.XLangDesugaringPhase$.run(XLangDesugaringPhase.scala:28)
    at leon.xlang.XLangDesugaringPhase$.run(XLangDesugaringPhase.scala:9)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.utils.PreprocessingPhase.run(PreprocessingPhase.scala:48)
    at leon.utils.PreprocessingPhase.run(PreprocessingPhase.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:10)
    at leon.Main$.execute(Main.scala:267)
    at leon.Main$.main(Main.scala:251)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

Thanks,

Prover error in operation functions: ERROR "Type unification failed: Clash of types \"<markup>\" and \"<markup>\"\n\nType error in application: incompatible operand type\n\n<markup>\n<markup>\n\n<markup>"

Any idea about the following?

[nix-shell:/tmp/l/git/github/other/leon]$ ./leon --solvers=isabelle testcases/verification/Addresses.scala 
./leon --solvers=isabelle testcases/verification/Addresses.scala 
[Warning ] warning: there were two feature warnings; re-run with -feature for details
[  Info  ] Preparing Isabelle setup (this might take a while) ...
[  Info  ] Building session ...
[  Info  ] Starting <Isabelle2016> instance ...
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Strings are not yet supported, translating to unspecified type
[Warning ] Match uses unsupported features; translating to if-then-else
[Internal] Prover error in operation functions: ERROR "Type unification failed: Clash of types \"<markup>\" and \"<markup>\"\n\nType error in application: incompatible operand type\n\n<markup>\n<markup>\n\n<markup>"
[Internal] Offending input: List((collectA'37,List((x'35,Type(Int.int,List())), (l'36,Type(Leon_Runtime.List'2,List()))),(App(App(App(Const(HOL.If,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dNil'8,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(App(Const(Product_Type.Pair,Type(dummy,List())),Const(Groups.zero_class.zero,Type(Int.int,List()))),App(App(Const(Product_Type.Pair,Type(dummy,List())),Const(Groups.zero_class.zero,Type(Int.int,List()))),Const(Leon_Runtime.List'2.cNil'8,Type(dummy,List()))))),App(App(App(Const(HOL.If,Type(dummy,List())),App(App(Const(HOL.conj,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dCons'3,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(App(Const(HOL.eq,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Free(x'35,Type(Int.int,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))))),Abs(x'd'1'1223,Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(0))),Abs(b2'1227,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(1)))),Abs(c2'1228,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),Bound(2)))),Abs(l2'1229,Type(Leon_Runtime.List'2,List()),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(App(Const(Leon_Runtime.max'34,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Int.int,List()), Type(Int.int,List())))))),App(Const(Leon_Runtime.List'2.sb'5,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(2))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(App(Const(Leon_Runtime.max'34,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Int.int,List()), Type(Int.int,List())))))),App(Const(Leon_Runtime.List'2.sc'6,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(1))),Bound(0)))))))))))),App(App(App(Const(HOL.If,Type(dummy,List())),App(App(Const(HOL.conj,Type(dummy,List())),App(Const(Leon_Runtime.List'2.dCons'3,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(HOL.Not,Type(dummy,List())),App(App(Const(HOL.eq,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Free(x'35,Type(Int.int,List())))))),App(App(Const(HOL.Let,Type(dummy,List())),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))))),App(App(Const(Product_Type.Pair,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(App(Free(collectA'37,Type(fun,List(Type(Int.int,List()), Type(fun,List(Type(Leon_Runtime.List'2,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))))),Free(x'35,Type(Int.int,List()))),App(Const(Leon_Runtime.List'2.stail'7,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List()))))))))),Abs(x'd'2'1234,Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(0))),Abs(b2'1238,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.fst,Type(dummy,List())),Bound(1)))),Abs(c2'1239,Type(Int.int,List()),App(App(Const(HOL.Let,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),App(Const(Product_Type.prod.snd,Type(dummy,List())),Bound(2)))),Abs(l2'1240,Type(Leon_Runtime.List'2,List()),App(App(Const(Product_Type.Pair,Type(dummy,List())),Bound(2)),App(App(Const(Product_Type.Pair,Type(dummy,List())),Bound(1)),App(App(App(App(Const(Leon_Runtime.List'2.cCons'3,Type(dummy,List())),App(Const(Leon_Runtime.List'2.sa'4,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(Leon_Runtime.List'2.sb'5,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),App(Const(Leon_Runtime.List'2.sc'6,Type(dummy,List())),Free(l'36,Type(Leon_Runtime.List'2,List())))),Bound(0))))))))))))),App(Const(Leon_Library.error,Type(fun,List(Type(dummy,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List())))))))),App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Nat.nat,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),App(Const(Num.num.Bit0,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),Const(Num.num.One,Type(Num.num,List()))))))))))))))))))))))))))),Type(Product_Type.prod,List(Type(Int.int,List()), Type(Product_Type.prod,List(Type(Int.int,List()), Type(Leon_Runtime.List'2,List()))))))))
[Internal] Please inform the authors of Leon about this message

Simple use of lemmas for preconditions (feature request?)

Imagine I have the following lemma:

def lemma(l:List[A], e1:A, e2:A) = {
   e1.prop == e2.prop ==> cond(l, e1) == cond(l, e2)
}.holds;

and the following code:

case class B(l:List[A], e:A) {
   require(cond(l, e))
}

def f(b:B):B = {
   B(
        l,
        A(... with same .prop as b.e ...)
    ) // leon cannot prove that B can be built without the lemma
}

What is the best way to make sure that Leon can prove that the new B can be built ? (The precondition for creating B holds because of the lemma.)

if(lemma(l, b.e, A(...))) B(...) else error[]("...") // works but messes up postconditions

check(lemma(...)) //ok
B(...) // ko, lemma has been forgotten

I was wondering if it would be possible to write something such as:

B(...) because lemma(...) // or any better syntax

(Or have Leon remember what it "check(...)'ed" before.)

Sorry if a method already exists in Leon to do that or if the issue has already been raised! :)

Improving the code for declaring ADTs.

The code in the file ADTManager is somewhat hard to follow with too many nested recursion. It has also been a source of other bugs. In principle, we can separate the algorithm into 3 parts: (a) constructing a dependency graph between ADTs, (b) computing SCC DAG, and (c) traversing them in the bottom up order and declaring the ADTs.