@pure function with inner functions causes a crash #1273
Description
The following causes a MatchError on IsPure
import stainless._
import stainless.lang._
import stainless.annotation._
object PureFnWithInnerFn {
@pure
def outer: Unit = {
def inner: Unit = ()
}
}(seems to be a minor oversight in ImperativeCodeElimination which should filter out the IsPure flags on transformed inner functions)
Stacktrace
scala.MatchError: IsPure (of class stainless.extraction.imperative.Trees$IsPure$)
at inox.ast.TreeDeconstructor.deconstruct(Deconstructors.scala:526)
at inox.ast.TreeDeconstructor.deconstruct$(Deconstructors.scala:21)
at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$ast$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
at stainless.ast.TreeDeconstructor.deconstruct(Deconstructors.scala:231)
at stainless.ast.TreeDeconstructor.deconstruct$(Deconstructors.scala:6)
at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$termination$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
at stainless.extraction.termination.TreeDeconstructor.deconstruct(Trees.scala:37)
at stainless.extraction.termination.TreeDeconstructor.deconstruct$(Trees.scala:31)
at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$trace$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
at stainless.extraction.trace.TreeDeconstructor.deconstruct(Trees.scala:35)
at stainless.extraction.trace.TreeDeconstructor.deconstruct$(Trees.scala:29)
at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$inlining$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
at stainless.extraction.inlining.TreeDeconstructor.deconstruct(Trees.scala:38)
at stainless.extraction.inlining.TreeDeconstructor.deconstruct$(Trees.scala:31)
at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$oo$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
at stainless.extraction.oo.TreeDeconstructor.deconstruct(Trees.scala:482)
at stainless.extraction.oo.TreeDeconstructor.deconstruct$(Trees.scala:426)
at stainless.extraction.oo.ConcreteTreeDeconstructor.deconstruct(Trees.scala:486)
at inox.transformers.Transformer.transform(Transformer.scala:141)
at inox.transformers.Transformer.transform$(Transformer.scala:6)
at stainless.extraction.oo.ConcreteTreeTransformer.inox$transformers$TreeTransformer$$super$transform(Trees.scala:518)
at inox.transformers.TreeTransformer.transform(Transformer.scala:226)
at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at inox.transformers.TreeTransformer.transform(Transformer.scala:227)
at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at inox.transformers.Transformer.$anonfun$6(Transformer.scala:82)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at inox.transformers.Transformer.transform(Transformer.scala:85)
at inox.transformers.Transformer.transform$(Transformer.scala:6)
at stainless.extraction.oo.ConcreteTreeTransformer.stainless$transformers$Transformer$$super$transform(Trees.scala:518)
at stainless.extraction.oo.ConcreteTreeTransformer.stainless$transformers$Transformer$$super$transform(Trees.scala:518)
at stainless.transformers.Transformer.transform(Transformer.scala:63)
at stainless.transformers.Transformer.transform$(Transformer.scala:8)
at stainless.extraction.oo.ConcreteTreeTransformer.inox$transformers$TreeTransformer$$super$transform(Trees.scala:518)
at inox.transformers.TreeTransformer.transform(Transformer.scala:220)
at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
at stainless.extraction.imperative.ImperativeCleanup$TransformerContext.transform(ImperativeCleanup.scala:98)
at inox.transformers.TreeTransformer.transform(Transformer.scala:221)
at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at inox.transformers.DefinitionTransformer.transform(Transformer.scala:181)
at inox.transformers.DefinitionTransformer.transform$(Transformer.scala:170)
at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
at stainless.extraction.SimplePhase.extractFunction(ExtractionPipeline.scala:153)
at stainless.extraction.SimplePhase.extractFunction$(ExtractionPipeline.scala:147)
at stainless.extraction.imperative.ImperativeCleanup.extractFunction(ImperativeCleanup.scala:140)
at stainless.extraction.imperative.ImperativeCleanup.extractFunction(ImperativeCleanup.scala:126)
at stainless.extraction.CachingPhase.$anonfun$3$$anonfun$1(ExtractionPipeline.scala:102)
at stainless.extraction.utils.ConcurrentCache.cached(ConcurrentCaches.scala:26)
at stainless.extraction.ExtractionCaches$ExtractionCache.cached(ExtractionCaches.scala:165)
at stainless.extraction.CachingPhase.$anonfun$1(ExtractionPipeline.scala:102)
at scala.collection.Iterator$$anon$9.next(Iterator.scala:575)
at scala.collection.immutable.List.prependedAll(List.scala:153)
at scala.collection.immutable.List$.from(List.scala:684)
at scala.collection.immutable.List$.from(List.scala:681)
at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
at scala.collection.immutable.Iterable$.from(Iterable.scala:35)
at scala.collection.immutable.Iterable$.from(Iterable.scala:32)
at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
at scala.collection.IterableOps.map(Iterable.scala:671)
at scala.collection.IterableOps.map$(Iterable.scala:671)
at scala.collection.AbstractIterable.map(Iterable.scala:919)
at stainless.extraction.CachingPhase.extractSymbols(ExtractionPipeline.scala:102)
at stainless.extraction.CachingPhase.extractSymbols$(ExtractionPipeline.scala:82)
at stainless.extraction.imperative.ImperativeCleanup.stainless$extraction$oo$CachingPhase$$super$extractSymbols(ImperativeCleanup.scala:17)
at stainless.extraction.imperative.ImperativeCleanup.stainless$extraction$oo$CachingPhase$$super$extractSymbols(ImperativeCleanup.scala:17)
at stainless.extraction.oo.CachingPhase.extractSymbols(ExtractionPipeline.scala:28)
at stainless.extraction.oo.CachingPhase.extractSymbols$(ExtractionPipeline.scala:13)
at stainless.extraction.imperative.ImperativeCleanup.extractSymbols(ImperativeCleanup.scala:17)
at stainless.extraction.imperative.ImperativeCleanup.extractSymbols(ImperativeCleanup.scala:17)
at stainless.extraction.CachingPhase.extract(ExtractionPipeline.scala:97)
at stainless.extraction.CachingPhase.extract$(ExtractionPipeline.scala:82)
at stainless.extraction.imperative.ImperativeCleanup.extract(ImperativeCleanup.scala:17)
at stainless.extraction.utils.DebugPipeline.extract$$anonfun$2$$anonfun$1(DebugPipeline.scala:136)
at scala.util.Try$.apply(Try.scala:210)
at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
at inox.utils.TimerStorage.run(Timer.scala:88)
at stainless.extraction.utils.DebugPipeline.extract$$anonfun$1(DebugPipeline.scala:136)
at stainless.extraction.utils.DebugSymbols.debug(DebugPipeline.scala:64)
at stainless.extraction.utils.DebugSymbols.debug$(DebugPipeline.scala:29)
at stainless.extraction.utils.DebugPipeline.debug(DebugPipeline.scala:124)
at stainless.extraction.utils.DebugPipeline.extract(DebugPipeline.scala:137)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
at stainless.ComponentRun.extract(Component.scala:87)
at stainless.ComponentRun.extract$(Component.scala:47)
at stainless.verification.VerificationRun.extract(VerificationComponent.scala:53)
at stainless.ComponentRun.apply(Component.scala:97)
at stainless.ComponentRun.apply$(Component.scala:47)
at stainless.verification.VerificationRun.apply(VerificationComponent.scala:53)
at stainless.frontend.BatchedCallBack.$anonfun$3(BatchedCallBack.scala:109)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at stainless.frontend.BatchedCallBack.endExtractions(BatchedCallBack.scala:110)
at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:34)
at java.lang.Thread.run(Thread.java:748)