Lookup fails for `toString()`

[saraswat]

stainless fails on:

import stainless.io.StdOut.println
abstract class A
case class B[X  <: A](a:X) {}
case object C extends A
object test {
  def m[X <: A](a:X) = B(a)
  def main(args: Array[String]): Unit = {
      println(m(C).toString())
  }
}

with the trace below. How should a user print out a value, then...?

Trace:

[error] ## Exception when compiling 31 sources to /Users/savija/tmp/test/verified/target/scala-2.12/classes
[error] inox.ast.Definitions$FunctionLookupException: Lookup failed for function with symbol `toString$0`
[error] inox.ast.Definitions$AbstractSymbols.$anonfun$getFunction$1(Definitions.scala:197)
[error] scala.Option.getOrElse(Option.scala:189)
[error] inox.ast.Definitions$AbstractSymbols.getFunction(Definitions.scala:197)
[error] inox.ast.Definitions$AbstractSymbols.getFunction$(Definitions.scala:196)
[error] stainless.extraction.oo.ClassSymbols$ClassSymbols.getFunction(ClassSymbols.scala:18)
[error] stainless.extraction.xlang.TreeSanitizer$IgnoredFields.isFieldAccessor(TreeSanitizer.scala:187)
[error] stainless.extraction.xlang.TreeSanitizer$IgnoredFields.traverse(TreeSanitizer.scala:201)
[error] inox.transformers.TreeTraverser.traverse(Traverser.scala:96)
[error] inox.transformers.TreeTraverser.traverse$(Traverser.scala:96)
[error] stainless.extraction.xlang.TreeSanitizer$IgnoredFields.traverse(TreeSanitizer.scala:175)
[error] stainless.extraction.xlang.TreeSanitizer$IgnoredFields.traverse(TreeSanitizer.scala:175)
[error] inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[error] inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[error] scala.collection.immutable.List.foreach(List.scala:392)
[error] inox.transformers.Traverser.traverse(Traverser.scala:29)
[error] inox.transformers.Traverser.traverse$(Traverser.scala:25)

[jad-hamza]

I opened a pull request to make StdOut.println callable on any value https://github.com/epfl-lara/stainless/pull/761

In the meantime you can define your own println function and annotate it @extern so that Stainless doesn't look at it:

@extern
def println(x: Any): Unit = {
    scala.Predef.println(x)
}

@extern is quite useful to wrap any kind of code that Stainless doesn't support (the code won't be verified but will be compiled normally)

[romac]

@jad-hamza You might want to add a @pure annotation to such a function, to inform Stainless that the function will not mutate its arguments. Stainless will otherwise assume that any field that is either mutable or marked @extern but not @pure will be mutated by the function call.

[jad-hamza]

Good point!

[jad-hamza]

Reopening because we might want to deal with the toString issue as well, independently of printing

[vkuncak]

In general, a function known to Scala (e.g. due to Prelude) but not known to Stainless will make its way all the way to Inox and then cause a crash. For example, this crashes:

object Test {
  def f = assume(false)
}