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 compileLambda in CodeGeneration #1182

Open jad-hamza opened 2 years ago

jad-hamza commented 2 years ago

This files (a minimized version of GodelNumbering) crashes on the assertion here: https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/core/src/main/scala/stainless/codegen/CodeGeneration.scala#L355

stainless Test.scala --solvers=smt-z3 --batched --vc-cache=false --codegen --debug=stack --feeling-lucky
import stainless.lang._
import stainless.equations._
import stainless.annotation._
import stainless.proof.check

object Test {
  sealed abstract class Nat {
    def +(that: Nat): Nat = {
      decreases(this)
      this match {
        case Zero => that
        case Succ(n) => Succ(n + that)
      }
    }
  }

  case object Zero extends Nat
  case class Succ(n: Nat) extends Nat

  val One = Succ(Zero)
  val Two = Succ(One)

  @opaque @inlineOnce
  def associative_plus(@induct n1: Nat, n2: Nat, n3: Nat): Unit = {
    ()
  }.ensuring(_ => (n1 + n2) + n3 == n1 + (n2 + n3))

  @opaque @inlineOnce
  def plus_succ(@induct n1: Nat, n2: Nat): Unit = {
    ()
  }.ensuring(_ => n1 + Succ(n2) == Succ(n1 + n2))

  @induct @opaque @inlineOnce
  def plus_zero(n: Nat): Unit = {
    ()
  }.ensuring(_ => n + Zero == n)

  @opaque @inlineOnce
  def commutative_plus(n1: Nat, n2: Nat): Unit = {
    decreases(n1, n2)
    n1 match {
      case Zero =>
        plus_zero(n2)
      case Succ(p1) => {
        n1 + n2               ==:| trivial   |:
        Succ(p1) + n2         ==:| trivial   |:
        (Succ(p1 + n2): Nat)  ==:| commutative_plus(p1, n2) |:
        (Succ(n2 + p1): Nat)  ==:| plus_succ(n2, p1) |:
        n2 + n1
      }.qed
    }
  }.ensuring(_ => n1 + n2 == n2 + n1)
}

Stack trace:

[  Info  ] Starting verification...
[  Info  ] Verified: 0 / 28
[Internal] Error: assertion failed. Trace:
[Internal] - scala.Predef$.assert(Predef.scala:264)
[Internal] - stainless.codegen.CodeGeneration.compileLambda(CodeGeneration.scala:355)
[Internal] - stainless.codegen.CodeGeneration.compileLambda$(CodeGeneration.scala:353)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.compileLambda(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkLambda(CodeGeneration.scala:1253)
[Internal] - stainless.codegen.CodeGeneration.mkLambda$(CodeGeneration.scala:1244)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkLambda(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:903)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:642)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:642)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:642)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:860)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:862)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:642)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:1223)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:625)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:634)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.mkExpr(CodeGeneration.scala:619)
[Internal] - stainless.codegen.CodeGeneration.mkExpr$(CodeGeneration.scala:607)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.mkExpr(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.compileFunDef(CodeGeneration.scala:333)
[Internal] - stainless.codegen.CodeGeneration.compileFunDef$(CodeGeneration.scala:270)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.compileFunDef(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CodeGeneration.$anonfun$compile$3(CodeGeneration.scala:151)
[Internal] - stainless.codegen.CodeGeneration.$anonfun$compile$3$adapted(CodeGeneration.scala:150)
[Internal] - scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
[Internal] - scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
[Internal] - scala.collection.AbstractIterable.foreach(Iterable.scala:919)
[Internal] - stainless.codegen.CodeGeneration.compile(CodeGeneration.scala:150)
[Internal] - stainless.codegen.CodeGeneration.compile$(CodeGeneration.scala:144)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.compile(CodeGenEvaluator.scala:187)
[Internal] - stainless.codegen.CompilationUnit.$init$(CompilationUnit.scala:470)
[Internal] - stainless.evaluators.CodeGenEvaluator$$anon$1.<init>(CodeGenEvaluator.scala:190)
[Internal] - stainless.evaluators.CodeGenEvaluator$.apply(CodeGenEvaluator.scala:187)
[Internal] - stainless.evaluators.Evaluator$.apply(Evaluator.scala:13)
[Internal] - stainless.package$$anon$1$$anon$2.createEvaluator(package.scala:72)
[Internal] - inox.Semantics.$anonfun$getEvaluator$1(Semantics.scala:35)
[Internal] - inox.utils.Cache.cached(Caches.scala:14)
[Internal] - inox.utils.Cache.cached$(Caches.scala:11)
[Internal] - inox.utils.LruCache.cached(Caches.scala:20)
[Internal] - inox.Semantics.getEvaluator(Semantics.scala:35)
[Internal] - inox.Semantics.getEvaluator$(Semantics.scala:33)
[Internal] - stainless.package$$anon$1$$anon$2.getEvaluator(package.scala:59)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.validateModel(UnrollingSolver.scala:326)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$23(UnrollingSolver.scala:780)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$23$adapted(UnrollingSolver.scala:780)
[Internal] - scala.Option.filter(Option.scala:319)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.luckyModel$lzycompute$1(UnrollingSolver.scala:780)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.luckyModel$1(UnrollingSolver.scala:778)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$2(UnrollingSolver.scala:783)
[Internal] - scala.util.Try$.apply(Try.scala:210)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$1(UnrollingSolver.scala:554)
[Internal] - scala.util.Try$.apply(Try.scala:210)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions(UnrollingSolver.scala:836)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions$(UnrollingSolver.scala:553)
[Internal] - inox.solvers.SolverFactory$$anon$9.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:292)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions(TimeoutSolver.scala:47)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions$(TimeoutSolver.scala:39)
[Internal] - inox.solvers.SolverFactory$$anon$9.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:292)
[Internal] - inox.tip.TipDebugger.checkAssumptions(TipDebugger.scala:101)
[Internal] - inox.tip.TipDebugger.checkAssumptions$(TipDebugger.scala:99)
[Internal] - inox.solvers.SolverFactory$$anon$9.checkAssumptions(SolverFactory.scala:292)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check$(UnrollingSolver.scala:87)
[Internal] - inox.solvers.SolverFactory$$anon$9.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:292)
[Internal] - inox.solvers.combinators.TimeoutSolver.check(TimeoutSolver.scala:35)
[Internal] - inox.solvers.combinators.TimeoutSolver.check$(TimeoutSolver.scala:28)
[Internal] - inox.solvers.SolverFactory$$anon$9.inox$tip$TipDebugger$$super$check(SolverFactory.scala:292)
[Internal] - inox.tip.TipDebugger.check(TipDebugger.scala:96)
[Internal] - inox.tip.TipDebugger.check$(TipDebugger.scala:94)
[Internal] - inox.solvers.SolverFactory$$anon$9.check(SolverFactory.scala:292)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVC$3(VerificationChecker.scala:241)
[Internal] - scala.util.Try$.apply(Try.scala:210)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:236)
[Internal] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:222)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVC(VerificationChecker.scala:369)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVCs$2(VerificationChecker.scala:111)
[Internal] - scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:855)
[Internal] - scala.collection.IterableOnceOps.foldLeft(IterableOnce.scala:646)
[Internal] - scala.collection.IterableOnceOps.foldLeft$(IterableOnce.scala:642)
[Internal] - scala.collection.AbstractIterator.foldLeft(Iterator.scala:1288)
[Internal] - scala.concurrent.Future$.traverse(Future.scala:855)
[Internal] - stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:101)
[Internal] - stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:88)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:369)
[Internal] - stainless.verification.VerificationChecker.verify(VerificationChecker.scala:79)
[Internal] - stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:77)
[Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:369)
[Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:383)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:116)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:53)
[Internal] - stainless.ComponentRun.apply(Component.scala:101)
[Internal] - stainless.ComponentRun.apply$(Component.scala:98)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:53)
[Internal] - stainless.frontend.BatchedCallBack.$anonfun$endExtractions$3(BatchedCallBack.scala:111)
[Internal] - scala.collection.immutable.List.map(List.scala:246)
[Internal] - scala.collection.immutable.List.map(List.scala:79)
[Internal] - stainless.frontend.BatchedCallBack.endExtractions(BatchedCallBack.scala:109)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:33)
[Internal] - java.lang.Thread.run(Thread.java:748)
[Internal] assertion failed
[Internal] Please inform the authors of Inox about this message
jad-hamza commented 2 years ago

When this is fixed, we should unignore these benchmarks:

https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala#L96 https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala#L121

vkuncak commented 2 years ago

Is this happening because counterexample validation attempt crashes?

jad-hamza commented 2 years ago

It's with --feeling-lucky (I don't really know how this works, but the description is: "Use evaluator to find counter-examples early"), so maybe it's even before that. (Also there shouldn't be counterexamples in this file, which is accepted with the --feeling-lucky --codegen options).

vkuncak commented 2 years ago

I believe --feeling-lucky opportunistically tests satisfiable queries that over-approximate the expression truth value. A satisfiable answer to such query is inconclusive and requires further unfolding. The idea is that we do obtain some counterexample from it, so we might as well try to execute function on it. If we are "lucky" and this execution triggers a crash, then we managed to find a counterexample. If there is no real counterexample then, if --feeling-lucky is not used to guide unfolding strategy (I am not sure if any solver uses such guidance, @samarion ?) then these checks normally should not trigger any failures. But if the solver was to return some huge counterexamples, it could cause even codegen evaluator to run very long or even stack overflow. Why do we even need to use --feeling-lucky here?

vkuncak commented 2 years ago

In any case, even if --feeling-lucky can cause a crash, it does not look like it should crash in compilation of lambdas.

samarion commented 2 years ago

We don't need --feeling-lucky but using it with --codegen gives us the best regression suite we have for the codegen evaluator.

@jad-hamza if you add some debugging around the assertion I can try to guess what's going wrong.

vkuncak commented 2 years ago

Confirmed as still crashing with stainless-dotty as of today.

samarion commented 2 years ago

If someone adds some debugging lines around the offending assertion and pastes the output here I can try to guestimate what's going wrong.