Call by name arguments unsound #1395
Assignees
Labels
Comments
|
The issue also arises in Scala 3. Here is a version of the example along with a test case that crashes in Note that the ADT does not seem the simple algebraic one because C case is defined in terms of B. import stainless.lang._
import stainless.collection._
sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Trait
object Bug{
def foo2(t: Trait, arg: => BigInt): List[BigInt] = {
decreases(t)
t match {
case A() => Nil[BigInt]()
case B(v, sub) => foo2(sub, arg)
case C(l, r) => Cons(((foo2(l, arg) ++ (foo2(r, arg) :+ BigInt(1))) - BigInt(1)).head, Nil[BigInt]())
}
}
val b: B = B(0, A())
def test = foo2(C(b, b), 42)
} |
|
Removing the recursion bouncing in the ADT using a pair makes Stainless detect it and correctly report an error: import stainless.lang._
import stainless.collection._
sealed trait Trait
case class A() extends Trait
case class C(left: (BigInt, Trait), right: (BigInt, Trait)) extends Trait
object Bug{
def foo2(t: Trait, arg: => BigInt): List[BigInt] = {
decreases(t)
t match {
case A() => Nil[BigInt]()
case C(l, r) => Cons(((foo2(l._2, arg) ++ (foo2(r._2, arg) :+ BigInt(1))) - BigInt(1)).head, Nil[BigInt]())
}
}
}gives In the original example, however, the counterexample is masked! It looks like something is off with the way ADTs are encoded in this case, even though there's no ADT encoding. @samarion have you seen anything like this? |
|
Another point that may be worth pointing out: if we replace the call-by-name parameter |
|
Very strange. Maybe if someone grabs some solver debug logs of the failing case I can try to make a guess. |
|
Another variant, this is correctly rejected: import stainless.lang._
import stainless.collection._
object i1395b {
sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Trait
def foo2(t: Trait, arg: BigInt => BigInt): List[BigInt] = {
decreases(t)
t match {
case A() => Nil[BigInt]()
case B(v, sub) => foo2(sub, x => arg(x))
case C(l, r) =>
val h = foo2(l, x => arg(x)).head
Cons(h, Nil[BigInt]())
}
}
}but this incorrectly verifies: import stainless.lang._
import stainless.collection._
object i1395b {
sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Trait
def foo2(t: Trait, arg: () => BigInt): List[BigInt] = {
decreases(t)
t match {
case A() => Nil[BigInt]()
case B(v, sub) => foo2(sub, () => arg())
case C(l, r) =>
val h = foo2(l, () => arg()).head
Cons(h, Nil[BigInt]())
}
}
} |
|
This might be an instance of this issue: epfl-lara/inox#139 |
|
The solver debug log for the precondition VC (for the variant #1395 (comment)): Click to expandThere is an ADT invariant on |
|
Yeah that looks like the Inox issue I mentioned. I expect that the example using a pair instead of the I gave some pointers about how to fix the underlying issue in epfl-lara/inox#139, but it's unfortunately a bit involved. |
|
At a first glance, all ingredients seems to be present for the fix. I'll give it a try :) Thanks again for looking at this issue! |
|
How did it go @mario-bucev ? |
|
@sankalpgambhir to illustrate the consequence of SMT-style ADT restrictions, even a very mild departure from recursion going over top-level data type definition, as in the present example: sealed trait Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Trait
case class C(left: B, right: B) extends Traitrequires Stainless to transform the ADT to make call inside @invariant(inv)
abstract class Trait
case class C(left: Trait, right: Trait) extends Trait
case class A() extends Trait
case class B(value: BigInt, sub: Trait) extends Traitwith the definition of def inv(thiss: Trait): Boolean = thiss.isInstanceOf[C] ==> ({
assert(thiss.isInstanceOf[C], "Cast error")
thiss.left
}.isInstanceOf[B] && {
assert(thiss.isInstanceOf[C], "Cast error")
thiss.right
}.isInstanceOf[B]) |
|
This and the underlying Inox issue should not be forgotten |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When running the following example, stainless times out as expected on
foobecause I useheadon an empty list. Stainless however verifiesfoo2which is exactlyfoobut with an additional call by value argument that is never used.The issues arises with timeouts, if the example is simplified and stainless is able to find a counterexample, then both will be invalid.
I am using the latest version of stainless-scalac.
The text was updated successfully, but these errors were encountered: