search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

Type error when using variant types #379

Closed jad-hamza closed 6 years ago

jad-hamza commented 6 years ago

I don't know if this is an issue of its own, or if this is due to the Container type not being rejected properly. scalac rejects it, but probably in the phases that are not executed by Stainless (see https://github.com/epfl-lara/stainless/issues/327 for similar discussion)

object BigIntContainer {
  case class Container[+T](var x: T)

  def store(box: Container[BigInt], y: BigInt) = {
    box.x = y
  }
}
[Internal] Error: Type error: box.x = y, expected Unit, 
[Internal] found <untyped>
[Internal] 
[Internal] Typing explanation:
[Internal] box.x = y is of type <untyped>
[Internal]   box is of type Object
[Internal]   y is of type BigInt. Trace:
[Internal] - inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:22)
[Internal] - inox.ast.TypeOps$class.typeCheck(TypeOps.scala:93)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.typeCheck(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedFunction(Definitions.scala:215)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedFunction(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
[Internal] - scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:210)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.stainless$extraction$oo$Definitions$AbstractSymbols$$super$ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:133)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply$mcV$sp(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.utils.Lazy.get(Lazy.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormed(Definitions.scala:206)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormed(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.TypeEncoding$class.extractSymbols(TypeEncoding.scala:1182)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1256)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1256)
[Internal] - stainless.extraction.CachingPhase$class.extract(ExtractionPipeline.scala:91)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extract(TypeEncoding.scala:1256)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - stainless.extraction.utils.DebugPipeline$class.extract(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anon$1.extract(DebugPipeline.scala:100)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.ComponentRun$class.extract(Component.scala:75)
[Internal] - stainless.verification.VerificationRun.extract(VerificationComponent.scala:37)
[Internal] - stainless.ComponentRun$class.apply(Component.scala:86)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:37)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:174)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - stainless.frontend.StainlessCallBack.processSymbols(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack.apply(StainlessCallBack.scala:59)
[Internal] - stainless.frontends.scalac.StainlessExtraction$Phase.apply(StainlessExtraction.scala:34)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$applyPhase$1.apply$mcV$sp(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase.withCurrentUnit(Global.scala:431)
[Internal] - scala.tools.nsc.Global$GlobalPhase.applyPhase(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.tools.nsc.Global$GlobalPhase.run(Global.scala:398)
[Internal] - scala.tools.nsc.Global$Run.compileUnitsInternal(Global.scala:1501)
[Internal] - scala.tools.nsc.Global$Run.compileUnits(Global.scala:1486)
[Internal] - scala.tools.nsc.Global$Run.compileSources(Global.scala:1481)
[Internal] - scala.tools.nsc.Global$Run.compile(Global.scala:1582)
[Internal] - stainless.frontends.scalac.ScalaCompiler$Factory$$anon$1.onRun(ScalaCompiler.scala:127)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:31)
[Internal] - java.lang.Thread.run(Thread.java:748)
[Internal] Type error: box.x = y, expected Unit, 
[Internal] found <untyped>
[Internal] 
[Internal] Typing explanation:
[Internal] box.x = y is of type <untyped>
[Internal]   box is of type Object
[Internal]   y is of type BigInt
[Internal] Please inform the authors of Inox about this message
samarion commented 6 years ago

This was indeed due to a bug in type encoding, fixed in https://github.com/epfl-lara/stainless/commit/ba25a3db6cd2ddcd8193b4c91f99d6d4966b98df