search

epfl-lara / stainless

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

Crash in Inox type checker when using freshCopy #1474

Closed vkuncak closed 9 months ago

vkuncak commented 9 months ago

The Scla program with stainless version

[  Info  ] Version: 0.9.8.1-17-gd38a2ba
[  Info  ] Built at: 2023-11-02 17:14:54.153+0100

crashes with the error message shown below.

object TailList {
  import stainless.lang.*
  import stainless.lang.StaticChecks.*
  import stainless.annotation.*

  @mutable
  sealed abstract class Opt[@mutable T]
  case class NONE[@mutable T]() extends Opt[T]
  case class SOME[@mutable T](value: T) extends Opt[T]

  @ignore
  class pointer extends scala.annotation.Annotation

  final case class Node(var head: Int, var next: Cell[Opt[Node]])

  @extern
  def getLast(n: Node): Node =    
    n.next.v match
      case NONE() => n
      case SOME(next) => getLast(next)

  final case class TList(var first: Node,
                         @pointer var last: Node) {
    require(last == getLast(first))

    def isEmpty: Boolean =
      first.next.v == NONE()

    def popFirst: Int =
      require(!isEmpty)
      n.next.v match
        case SOME(n1) => 
          n1.head
          n.next = Cell(NONE())

    def addToEnd(x: Int): Unit =
      updateLast(last, mkEnd(x))
  }

  def updateLast(last: Node, newOne: Node): Unit =
    last.next.v = SOME(newOne)

  def mkEnd(head: Int): Node = Node(head, Cell(NONE[Node]()))

  @main
  def test =
    val n1: Node = mkEnd(5)
    val l: TList = TList(n1, freshCopy(n1))
    ()
}

[ Info ] Finished compiling
[ Info ] Preprocessing finished
[ Info ] Finished lowering the symbols
[ Info ] Finished generating VCs
[ Info ] Starting verification... [ Info ] Verified: 0 / 1 [Internal] Error: Type error: !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] }, expected Boolean, [Internal] found [Internal] [Internal] Typing explanation: [Internal] !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] } is of type [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] mkEnd(5) is of type Node [Internal] 5 is of type Int because mkEnd was instantiated with with type (Int) => Node [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] TList(n1, n1) is of type TList [Internal] n1 is of type Node [Internal] n1 is of type Node because TList was instantiated with with fields (Node,Node) because inv was instantiated with with type (TList) => (Boolean, TList). Trace: [Internal] - inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:29) [Internal] - inox.ast.TypeOps.typeCheck(TypeOps.scala:89) [Internal] - inox.ast.TypeOps.typeCheck$(TypeOps.scala:11) [Internal] - inox.ast.SimpleSymbols$SimpleSymbols.typeCheck(SimpleSymbols.scala:12) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr$$anonfun$1$$anonfun$1(UnrollingSolver.scala:214) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr$$anonfun$1$$anonfun$adapted$1(UnrollingSolver.scala:215) [Internal] - scala.util.Try$.apply(Try.scala:210) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:84) [Internal] - inox.utils.TimerStorage.run(Timer.scala:78) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr$$anonfun$1(UnrollingSolver.scala:215) [Internal] - scala.util.Try$.apply(Try.scala:210) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:84) [Internal] - inox.utils.TimerStorage.run(Timer.scala:78) [Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr(UnrollingSolver.scala:242) [Internal] - inox.solvers.SolverFactory$NativeZ3Impl$1.inox$tip$TipDebugger$$super$assertCnstr(SolverFactory.scala:185) [Internal] - inox.tip.TipDebugger.assertCnstr(TipDebugger.scala:91) [Internal] - inox.tip.TipDebugger.assertCnstr$(TipDebugger.scala:11) [Internal] - inox.solvers.SolverFactory$NativeZ3Impl$1.assertCnstr(SolverFactory.scala:185) [Internal] - inox.solvers.SolverFactory$NativeZ3Impl$1.assertCnstr(SolverFactory.scala:185) [Internal] - stainless.verification.VerificationChecker.$anonfun$10(VerificationChecker.scala:299) [Internal] - scala.util.Try$.apply(Try.scala:210) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:84) [Internal] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:302) [Internal] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$$anon$3.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:445) [Internal] - stainless.verification.VerificationCache.$anonfun$1(VerificationCache.scala:85) [Internal] - scala.util.Try$.apply(Try.scala:210) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:84) [Internal] - stainless.verification.VerificationCache.checkVC(VerificationCache.scala:92) [Internal] - stainless.verification.VerificationCache.checkVC$(VerificationCache.scala:27) [Internal] - stainless.verification.VerificationChecker$$anon$3.checkVC(VerificationChecker.scala:445) [Internal] - stainless.verification.VerificationChecker.processVC$1(VerificationChecker.scala:155) [Internal] - stainless.verification.VerificationChecker.$anonfun$4(VerificationChecker.scala:183) [Internal] - scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:861) [Internal] - scala.collection.IterableOnceOps.foldLeft(IterableOnce.scala:675) [Internal] - scala.collection.IterableOnceOps.foldLeft$(IterableOnce.scala:669) [Internal] - scala.collection.AbstractIterator.foldLeft(Iterator.scala:1300) [Internal] - scala.concurrent.Future$.traverse(Future.scala:861) [Internal] - stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:184) [Internal] - stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:436) [Internal] - stainless.verification.VerificationChecker.verify(VerificationChecker.scala:113) [Internal] - stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:436) [Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:450) [Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:121) [Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:75) [Internal] - stainless.ComponentRun.apply(Component.scala:88) [Internal] - stainless.ComponentRun.apply$(Component.scala:35) [Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:48) [Internal] - stainless.frontend.SplitCallBack.$anonfun$10(SplitCallBack.scala:201) [Internal] - scala.collection.immutable.List.map(List.scala:246) [Internal] - scala.collection.immutable.List.map(List.scala:79) [Internal] - stainless.frontend.SplitCallBack.processFunctionsSymbols(SplitCallBack.scala:203) [Internal] - stainless.frontend.SplitCallBack.$anonfun$9(SplitCallBack.scala:174) [Internal] - stainless.extraction.utils.ConcurrentCache.getOrElseUpdate(ConcurrentCaches.scala:15) [Internal] - stainless.frontend.SplitCallBack.processFunctions(SplitCallBack.scala:174) [Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:160) [Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:82) [Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:36) [Internal] - java.base/java.lang.Thread.run(Thread.java:833) [Internal] Type error: !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] }, expected Boolean, [Internal] found [Internal] [Internal] Typing explanation: [Internal] !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] } is of type [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] mkEnd(5) is of type Node [Internal] 5 is of type Int because mkEnd was instantiated with with type (Int) => Node [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] TList(n1, n1) is of type TList [Internal] n1 is of type Node [Internal] n1 is of type Node because TList was instantiated with with fields (Node,Node) because inv was instantiated with with type (TList) => (Boolean, TList) [Internal] Please inform the authors of Inox about this message [Internal] Error: Type error: !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] }, expected Boolean, [Internal] found [Internal] [Internal] Typing explanation: [Internal] !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] } is of type [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] mkEnd(5) is of type Node [Internal] 5 is of type Int because mkEnd was instantiated with with type (Int) => Node [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] TList(n1, n1) is of type TList [Internal] n1 is of type Node [Internal] n1 is of type Node because TList was instantiated with with fields (Node,Node) because inv was instantiated with with type (TList) => (Boolean, TList). Trace: [Internal] - inox.package$FatalError$.apply(package.scala:24) [Internal] - inox.Reporter.onFatal(Reporter.scala:47) [Internal] - inox.Reporter.internalError(Reporter.scala:63) [Internal] - inox.Reporter.internalError(Reporter.scala:115) [Internal] - inox.Reporter.internalError(Reporter.scala:118) [Internal] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:346) [Internal] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$$anon$3.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:445) [Internal] - stainless.verification.VerificationCache.$anonfun$1(VerificationCache.scala:85) [Internal] - scala.util.Try$.apply(Try.scala:210) [Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:84) [Internal] - stainless.verification.VerificationCache.checkVC(VerificationCache.scala:92) [Internal] - stainless.verification.VerificationCache.checkVC$(VerificationCache.scala:27) [Internal] - stainless.verification.VerificationChecker$$anon$3.checkVC(VerificationChecker.scala:445) [Internal] - stainless.verification.VerificationChecker.processVC$1(VerificationChecker.scala:155) [Internal] - stainless.verification.VerificationChecker.$anonfun$4(VerificationChecker.scala:183) [Internal] - scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:861) [Internal] - scala.collection.IterableOnceOps.foldLeft(IterableOnce.scala:675) [Internal] - scala.collection.IterableOnceOps.foldLeft$(IterableOnce.scala:669) [Internal] - scala.collection.AbstractIterator.foldLeft(Iterator.scala:1300) [Internal] - scala.concurrent.Future$.traverse(Future.scala:861) [Internal] - stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:184) [Internal] - stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:436) [Internal] - stainless.verification.VerificationChecker.verify(VerificationChecker.scala:113) [Internal] - stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:53) [Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:436) [Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:450) [Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:121) [Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:75) [Internal] - stainless.ComponentRun.apply(Component.scala:88) [Internal] - stainless.ComponentRun.apply$(Component.scala:35) [Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:48) [Internal] - stainless.frontend.SplitCallBack.$anonfun$10(SplitCallBack.scala:201) [Internal] - scala.collection.immutable.List.map(List.scala:246) [Internal] - scala.collection.immutable.List.map(List.scala:79) [Internal] - stainless.frontend.SplitCallBack.processFunctionsSymbols(SplitCallBack.scala:203) [Internal] - stainless.frontend.SplitCallBack.$anonfun$9(SplitCallBack.scala:174) [Internal] - stainless.extraction.utils.ConcurrentCache.getOrElseUpdate(ConcurrentCaches.scala:15) [Internal] - stainless.frontend.SplitCallBack.processFunctions(SplitCallBack.scala:174) [Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:160) [Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:82) [Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:36) [Internal] - java.base/java.lang.Thread.run(Thread.java:833) [Internal] Type error: !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] }, expected Boolean, [Internal] found [Internal] [Internal] Typing explanation: [Internal] !{ [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) [Internal] } is of type [Internal] val n1: Node = mkEnd(5) [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] mkEnd(5) is of type Node [Internal] 5 is of type Int because mkEnd was instantiated with with type (Int) => Node [Internal] inv(TList(n1, n1)) is of type (Boolean, TList) [Internal] TList(n1, n1) is of type TList [Internal] n1 is of type Node [Internal] n1 is of type Node because TList was instantiated with with fields (Node,Node) because inv was instantiated with with type (TList) => (Boolean, TList) [Internal] Please inform the authors of Inox about this message [ Error ] Stainless terminated with an error. [ Error ] Debug output is available in the file stainless-stack-trace.txt. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues [ Error ] You may use --debug=stack to have the stack trace displayed in the output.

mario-bucev commented 9 months ago

Inox is right here, the problem comes from the invariant being impure (due to getLast being @extern, taking a mutable parameter and not marked as @pure), and is transformed into a function returning an updated copy of TList, alongside the expected Boolean. Can we transfer this issue to Stainless?