Open vkuncak opened 1 year ago
mario-bucev
commented
1 year ago Minimized:
object Test {
def app(x: Int) = {
require(x > 0)
x + x
}.ensuring(_ > 0)
}Apparently, this stems from
https://github.com/uuverifiers/princess/blob/b8280e70269a554c20b52dccb735af80e4bf1ab0/src/ap/theories/bitvectors/ModuloArithmetic.scala#L306-L312
Maybe there is a case SignedBVSort missing?
vkuncak
commented
1 year ago @mario-bucev what is the status of this including the potential fix to Princess?
mario-bucev
commented
1 year ago The small typo fix has been merged https://github.com/uuverifiers/princess/pull/3 this issue can be resumed
vkuncak
commented
1 year ago Great! This would be indeed of value for having some checks on Scala idomatic code, done for Scala and in Scala :)
mario-bucev
commented
1 year ago Running the fix on the minimized example works but not on the ScalaList:
This error should not be too hard to fix, it's just about indexing into a Stream with something bigger than an Int.
mario-bucev
commented
1 year ago Actually, the problem may be on our side. Minimized example:
import stainless.lang._
object ScalaListMin {
sealed abstract class List[+A] {
def :: [B >: A](elem: B): List[B] = Cons(elem, this)
}
case object Nil extends List[Nothing]
final case class Cons[+A](first: A, next: List[A]) extends List[A]
def listOfCons(n: Int): List[List[Int]] = {
if (n <= 0) Nil
else Cons(42, Nil) :: listOfCons(n-1)
}
}The crash happens during measure inference for listOfCons. Having an invariant list makes the error go away.
vkuncak
commented
1 year ago @mario-bucev this seems resolved?
mario-bucev
commented
1 year ago It does not crash anymore, however two VCs timeout for zipWith, namely match exhaustiveness and the precondition of the recursive call.
mario-bucev
commented
1 year ago @samarion We were wondering whether you could shed some light (if possible!) on this snippet that does not verify with Princess:
import stainless.lang._
object ScalaList {
sealed abstract class List[+A] {
def :: [B >: A](elem: B): List[B] = Cons(elem, this)
def length: Long = {
this match {
case Nil => 0
case Cons(h, t) =>
val tLen = t.length
if (tLen == Long.MaxValue) tLen
else 1 + tLen
}
} ensuring(_ >= 0)
}
case object Nil extends List[Nothing]
final case class Cons[+A](first: A, next: List[A]) extends List[A]
def zipWith[A,B,C](f: (A,B) => C)(l1: List[A], l2: List[B]): List[C] = {
decreases(l1)
require(l1.length == l2.length && l1.length < Int.MaxValue)
/*
Match exhaustiveness:
!isList$0(l1$29, A$147) || !isList$0(l2$27, B$83) || length$1(A$147, l1$29) != length$1(B$83, l2$27)
|| length$1(A$147, l1$29) >= 2147483647.toLong || l1$29.isInstanceOf[Nil$2] && l2$27.isInstanceOf[Nil$2]
|| !l1$29.isInstanceOf[Cons$2] || !l2$27.isInstanceOf[Cons$2] || {
val l1$32: { x$115: Object$0 | (isList$0(x$115, A$147)): @dropConjunct } = l1$29.next$1
length$1(A$147, l1$32) == length$1(B$83, l2$27.next$1) && length$1(A$147, l1$32) < 2147483647.toLong
}
*/
(l1, l2) match {
case (Nil, Nil) => Nil
case (Cons(a,as), Cons(b,bs)) =>
/*
Precondition of recursive call:
!isList$0(l1$29, A$147) || !isList$0(l2$27, B$83) || length$1(A$147, l1$29) != length$1(B$83, l2$27)
|| length$1(A$147, l1$29) >= 2147483647.toLong || l1$29.isInstanceOf[Nil$2] && l2$27.isInstanceOf[Nil$2]
|| l1$29.isInstanceOf[Cons$2] && l2$27.isInstanceOf[Cons$2]
*/
Cons[C](f(a,b), zipWith(f)(as, bs))
}
}
}
Running Stainless https://github.com/epfl-lara/stainless/commit/bcc5b4d4e2fe0cc975345e7244ad24ecc3b2585b on the bolts ScalaList https://github.com/epfl-lara/bolts/commit/3f4df349a45a7e62c020f55eaedaaeb626c2b41d using command line args
--no-colors --timeout=5 ScalaList.scala --vc-cache=no --solvers=princessproduceswith Princess trace