Extraction test suite and verification pipeline yield different results

[romac]

With my branch in #78, the following benchmark yields different results with the extraction test suite and the verification pipeline that runs when invoking stainless on its own (either from the command-line or through sbt runMain.

object ConstructorArgsBoxing2 {
  case class A()
  case class B()

  sealed abstract class AnyFoo
  case class Foo[T](x: T) extends AnyFoo

  val a: AnyFoo = Foo(A())
  val b: AnyFoo = Foo(B())

  val list0: List[AnyFoo] = List(a, b)
}

I tried performing the extraction in the test suite using VerificationComponent.extract, but am still getting the same error.

Any idea what could be going wrong there?

Extraction test suite

stainless-scala/it:testOnly stainless.ExtractionSuite

(…snip…)

[info]   Extraction of 'extraction/ConstructorArgsBoxing2.scala'
[info]   - should be successful (0 milliseconds)
[info]   - should typecheck (12 milliseconds)
[info]     and transformation
====== ERROR ======
java.util.NoSuchElementException: key not found: apply
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.MapLike$class.apply(MapLike.scala:141)
    at scala.collection.AbstractMap.apply(Map.scala:59)
    at stainless.extraction.oo.TypeEncoding$Scope$2.rewrite(TypeEncoding.scala:724)
    at stainless.extraction.oo.TypeEncoding$Scope$2.transform(TypeEncoding.scala:849)
    at stainless.extraction.oo.TypeEncoding$$anonfun$96.apply(TypeEncoding.scala:1074)
    at stainless.extraction.oo.TypeEncoding$$anonfun$96.apply(TypeEncoding.scala:1074)
    at scala.Option.map(Option.scala:146)
    at stainless.extraction.oo.TypeEncoding$class.transformFunction$1(TypeEncoding.scala:1074)
    at stainless.extraction.oo.TypeEncoding$$anonfun$98.apply(TypeEncoding.scala:1090)
    at stainless.extraction.oo.TypeEncoding$$anonfun$98.apply(TypeEncoding.scala:1090)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at stainless.extraction.oo.TypeEncoding$class.transform(TypeEncoding.scala:1090)
    at stainless.extraction.oo.package$encoding$.transform(package.scala:30)
    at stainless.extraction.oo.package$encoding$.transform(package.scala:30)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.ast.SymbolTransformerComposition$class.transform(TreeOps.scala:307)
    at inox.ast.SymbolTransformer$$anon$2.transform(TreeOps.scala:327)
    at inox.Program$class.transform(Program.scala:77)
    at inox.Program$$anon$1.transform(Program.scala:90)
    at stainless.extraction.package$.extract(package.scala:77)
    at stainless.SimpleComponent$class.extract(Component.scala:41)
    at stainless.verification.VerificationComponent$.extract(VerificationComponent.scala:22)
    at stainless.ExtractionSuite$$anonfun$2.apply(ExtractionSuite.scala:44)
    at stainless.ExtractionSuite$$anonfun$2.apply(ExtractionSuite.scala:44)
    at scala.util.Try$.apply(Try.scala:192)
    at stainless.ExtractionSuite.stainless$ExtractionSuite$$extractOne(ExtractionSuite.scala:44)
    at stainless.ExtractionSuite$$anonfun$testAll$1$$anonfun$apply$mcV$sp$8$$anonfun$apply$1.apply$mcV$sp(ExtractionSuite.scala:78)
    at org.scalatest.SuperEngine.registerNestedBranch(Engine.scala:595)
    at org.scalatest.FunSpecLike$class.describe(FunSpecLike.scala:382)
    at org.scalatest.FunSpec.describe(FunSpec.scala:1630)
    at stainless.ExtractionSuite$$anonfun$testAll$1$$anonfun$apply$mcV$sp$8.apply(ExtractionSuite.scala:77)
    at stainless.ExtractionSuite$$anonfun$testAll$1$$anonfun$apply$mcV$sp$8.apply(ExtractionSuite.scala:76)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at stainless.ExtractionSuite$$anonfun$testAll$1.apply$mcV$sp(ExtractionSuite.scala:76)
    at org.scalatest.SuperEngine.registerNestedBranch(Engine.scala:595)
    at org.scalatest.FunSpecLike$class.describe(FunSpecLike.scala:382)
    at org.scalatest.FunSpec.describe(FunSpec.scala:1630)
    at stainless.ExtractionSuite.testAll(ExtractionSuite.scala:75)
    at stainless.ExtractionSuite.<init>(ExtractionSuite.scala:84)
    at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
    at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
    at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
    at java.lang.reflect.Constructor.newInstance(Constructor.java:423)
    at java.lang.Class.newInstance(Class.java:442)
    at org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:435)
    at sbt.TestRunner.runTest$1(TestFramework.scala:76)
    at sbt.TestRunner.run(TestFramework.scala:85)
    at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
    at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
    at sbt.TestFramework$.sbt$TestFramework$$withContextLoader(TestFramework.scala:185)
    at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
    at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
    at sbt.TestFunction.apply(TestFramework.scala:207)
    at sbt.Tests$.sbt$Tests$$processRunnable$1(Tests.scala:239)
    at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
    at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
    at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
    at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
    at sbt.std.Transform$$anon$4.work(System.scala:63)
    at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
    at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
    at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:17)
    at sbt.Execute.work(Execute.scala:237)
    at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
    at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
    at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:159)
    at sbt.CompletionService$$anon$2.call(CompletionService.scala:28)
    at java.util.concurrent.FutureTask.run(FutureTask.java:266)
    at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
    at java.util.concurrent.FutureTask.run(FutureTask.java:266)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
    at java.lang.Thread.run(Thread.java:748)
[info]     - should be successful *** FAILED *** (55 milliseconds)
[info]       org.scalatest.exceptions.TestFailedException was thrown. (ExtractionSuite.scala:19)
[info]       org.scalatest.exceptions.TestFailedException:
[info]       at org.scalatest.Assertions$class.newAssertionFailedException(Assertions.scala:528)
[info]       at org.scalatest.FunSpec.newAssertionFailedException(FunSpec.scala:1630)
[info]       at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:501)
[info]       at stainless.ExtractionSuite.stainless$ExtractionSuite$$assertSuccess(ExtractionSuite.scala:19)

(…snip…)

Verification pipeline

runMain ConstructorArgsBoxing2.scala

[  Info  ]  - Now solving 'postcondition' VC for a @?:?...
[  Info  ]  - Result for 'postcondition' VC for a @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for a @?:?...
[  Info  ]  - Result for 'cast correctness' VC for a @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for a @?:?...
[  Info  ]  - Result for 'cast correctness' VC for a @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for a @?:?...
[  Info  ]  - Result for 'cast correctness' VC for a @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'postcondition' VC for b @?:?...
[  Info  ]  - Result for 'postcondition' VC for b @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for b @?:?...
[  Info  ]  - Result for 'cast correctness' VC for b @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for b @?:?...
[  Info  ]  - Result for 'cast correctness' VC for b @?:?:
[  Info  ]  => VALID
[  Info  ]  - Now solving 'cast correctness' VC for b @?:?...
[  Info  ]  - Result for 'cast correctness' VC for b @?:?:
[  Info  ]  => VALID
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ verification summary ╞══════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                          ║
[  Info  ] ║ a   cast correctness                     ?:?:?        valid        U:smt-z3           0.027       ║
[  Info  ] ║ a   cast correctness                     ?:?:?        valid        U:smt-z3           0.020       ║
[  Info  ] ║ a   cast correctness                     ?:?:?        valid        U:smt-z3           0.031       ║
[  Info  ] ║ a   postcondition                        ?:?:?        valid        U:smt-z3           0.352       ║
[  Info  ] ║ b   cast correctness                     ?:?:?        valid        U:smt-z3           0.034       ║
[  Info  ] ║ b   cast correctness                     ?:?:?        valid        U:smt-z3           0.023       ║
[  Info  ] ║ b   cast correctness                     ?:?:?        valid        U:smt-z3           0.033       ║
[  Info  ] ║ b   postcondition                        ?:?:?        valid        U:smt-z3           0.056       ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 8      valid: 8    (0 from cache)   invalid: 0      unknown: 0     time:   0.576           ║
[  Info  ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Shutting down executor service.

[romac]

@samarion @mantognini @jad-hamza Any idea what might be going wrong there?

[romac]

My bad, the testcases are actually missing some imports. Everything runs fine now.

[mantognini]

If the issue was simply a missing import, we should probably fire a nicer error than this monstrosity into the user's face.

[romac]

Agreed. Here the problem was that the List.apply method that was resolved was the one from the scala.collection instead of stainless.collection.List.

Maybe we can even figure out a way to override the standard prelude with our own, which would put stainless.lang. and stainless.collection. in scope.

I know there is an option to do that with the Typelevel Scala programmer but I don’t whether that’s the case for Lightbend Scala as well.

On 27 Oct 2017, at 10:43, Marco Antognini notifications@github.com wrote:

If the issue was simply a missing import, we should probably fire a nicer error than this monstrosity into the user's face.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub, or mute the thread.