Option-less extractors result in "Lookup failure" exceptions

[Ant-28]

Versions

0.9.9.2

Problem

Extractor patterns that do not return Option[T] result in

MWE

//> using jar stainless-library.jar
//> using jar stainless-library-sources.jar
import stainless.annotation.ignore

case class Singleton(x: BigInt)

def unapply(u: Singleton): (BigInt) = {
    u match
        case Singleton(x) => (x)             
}

def testValidate(u: Singleton): Singleton = {
    require(u == Singleton(2))
    u match
        case Singleton(x) => Singleton(x + 1) 
}.ensuring(res => res == Singleton(3))

@ignore 
@main def main() = 
    println(testValidate(Singleton(2)))

The inclusion of main has no effect on the result. It should be noted that changing the signature of unapply to Option[BigInt] results in a successful verification pipeline.

//> using jar stainless-library.jar
//> using jar stainless-library-sources.jar
import stainless.annotation.ignore
import stainless.lang.*

case class Singleton(x: BigInt)

def unapply(u: Singleton): Option[BigInt] = {
    u match
        case Singleton(x) => Some(x)        
    
}

// rest unchanged

Stacktrace

inox.ast.Definitions$FunctionLookupException: Lookup failed for function with symbol `<none>$0`
	at inox.ast.Definitions$FunctionLookupException$.apply(Definitions.scala:32)
	at inox.ast.Definitions$AbstractSymbols.getFunction$$anonfun$1(Definitions.scala:194)
	at scala.Option.getOrElse(Option.scala:201)
	at inox.ast.Definitions$AbstractSymbols.getFunction(Definitions.scala:194)
	at inox.ast.Definitions$AbstractSymbols.getFunction$(Definitions.scala:119)
	at stainless.extraction.oo.ClassSymbols$ClassSymbols.getFunction(ClassSymbols.scala:18)
	at inox.ast.CallGraph.transitiveCallees$$anonfun$1(CallGraph.scala:112)
	at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
	at scala.collection.StrictOptimizedIterableOps.map$(StrictOptimizedIterableOps.scala:87)
	at scala.collection.immutable.Set$Set1.map(Set.scala:165)
	at inox.ast.CallGraph.transitiveCallees(CallGraph.scala:112)
	at inox.ast.CallGraph.transitiveCallees$(CallGraph.scala:9)
	at stainless.extraction.oo.ClassSymbols$ClassSymbols.transitiveCallees(ClassSymbols.scala:18)
	at stainless.extraction.imperative.EffectsAnalyzer$EffectsAnalysis.$init$$$anonfun$2(EffectsAnalyzer.scala:106)
	at scala.collection.IterableOnceOps.foldLeft(IterableOnce.scala:727)
	at scala.collection.IterableOnceOps.foldLeft$(IterableOnce.scala:721)
	at scala.collection.AbstractIterable.foldLeft(Iterable.scala:935)
	at stainless.extraction.imperative.EffectsAnalyzer$EffectsAnalysis.$init$(EffectsAnalyzer.scala:104)
	at stainless.extraction.imperative.AntiAliasing$SymbolsAnalysis.<init>(AntiAliasing.scala:44)
	at stainless.extraction.imperative.AntiAliasing$SymbolsAnalysis$.apply(AntiAliasing.scala:44)
	at stainless.extraction.imperative.AntiAliasing.getContext(AntiAliasing.scala:83)
	at stainless.extraction.imperative.AntiAliasing.getContext(AntiAliasing.scala:83)
	at stainless.extraction.CachingPhase.extract(ExtractionPipeline.scala:125)
	at stainless.extraction.CachingPhase.extract$(ExtractionPipeline.scala:105)
	at stainless.extraction.imperative.AntiAliasing.extract(AntiAliasing.scala:11)
	at stainless.extraction.utils.NamedPipeline.extract$$anonfun$1$$anonfun$1(NamedPipeline.scala:141)
	at scala.util.Try$.apply(Try.scala:217)
	at inox.utils.TimerStorage.runAndGetTime(Timer.scala:84)
	at inox.utils.TimerStorage.run(Timer.scala:78)
	at stainless.extraction.utils.NamedPipeline.extract$$anonfun$1(NamedPipeline.scala:141)
	at stainless.extraction.utils.DebugSymbols.debug(NamedPipeline.scala:64)
	at stainless.extraction.utils.DebugSymbols.debug$(NamedPipeline.scala:29)
	at stainless.extraction.utils.NamedPipeline.debug(NamedPipeline.scala:127)
	at stainless.extraction.utils.NamedPipeline.extract(NamedPipeline.scala:142)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:48)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:48)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:47)
	at stainless.ComponentRun.extract(Component.scala:75)
	at stainless.ComponentRun.extract$(Component.scala:35)
	at stainless.verification.VerificationRun.extract(VerificationComponent.scala:48)
	at stainless.ComponentRun.apply(Component.scala:85)
	at stainless.ComponentRun.apply$(Component.scala:35)
	at stainless.verification.VerificationRun.apply(VerificationComponent.scala:48)
	at stainless.frontend.BatchedCallBack.$anonfun$3(BatchedCallBack.scala:116)
	at scala.collection.immutable.List.map(List.scala:247)
	at scala.collection.immutable.List.map(List.scala:79)
	at stainless.frontend.BatchedCallBack.endExtractions(BatchedCallBack.scala:114)
	at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:36)
	at java.base/java.lang.Thread.run(Thread.java:1583)

Result from scala-cli

scala-cli test.scala
Compiling project (Scala 3.7.4, JVM (17))
Compiled project (Scala 3.7.4, JVM (17))
Singleton(3)

[sankalpgambhir]

So the issue seems to be with the existence of a user-defined irrefutable pattern match. In the case of the optional match, an annotation is applied to the function which seems to be a pair of check and get functions:

@final
@unapply(isEmpty, get)
def unapply(u: T): Option[Int] = u match {

But in the case of an irrefutable match, this annotation does not (need to) contain any data:

@final
@unapply(<none>, <none>)
def unapply(u: T): Int = u match {

The <none> cannot be resolved while collecting symbols later.

Note: I believe in general this should be written with return type Some[Int], which works fine. Edit: apparently the compiler does auto generate these without the Some as well, but these autogenerated unapplies don't seem to exist in the extracted trees printed via debug=trees.

I have not been able to find the code that introduces this annotation, or as yet find if it comes from the Stainless frontend or the Scala compiler.

These trees are printed under Symbols before Preprocessing already, so it is likely either from the compiler or early in the frontend?

@mbovel any ideas on where this @unapply comes from?

Aside:

This is not quite an example of an unapply method on Singleton, since it is outside the function.

Further, there is an auto generated unapply for case classes (which Stainless will pick up by default). In both your cases, that is the method being used in the pattern match when you actually perform the match.