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

Crash with simple pattern match when using the princess solver #249

Closed dragos closed 6 years ago

dragos commented 6 years ago

While working on the lambda interpreter example, I wanted to make the pattern match exhaustivity checker to fail (find a missing case), but instead I got this crash. The code in question looks like this:

  def lift(op: (Int, Int) => Int) : Value = FunctionValue((v1: Value) => v1 match {
    case IntegerValue(c1) => FunctionValue((v2: Value) => v2 match {
      case IntegerValue(c2) => IntegerValue(op(c1, c2))
      case _ => Err("Plus given a non-integer value as second argument.")
    })
    // before it was `case _ =>` and everything worked fine
    case Err(_) => Err("Plus given a non-integer value as first argument.")
  })

Result:

[  Info  ]  - Now solving 'match exhaustiveness' VC for lift @78:71...
[info]  - Now solving 'match exhaustiveness' VC for lift @78:71...
[Internal] Error: None.get. Trace:
[error] Error: None.get. Trace:
[Internal] - scala.None$.get(Option.scala:347)
[error] - scala.None$.get(Option.scala:347)
[Internal] - scala.None$.get(Option.scala:345)
[error] - scala.None$.get(Option.scala:345)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractFunction$1$2.apply(UnrollingSolver.scala:380)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractFunction$1$2.apply(UnrollingSolver.scala:380)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractFunction$1$2.apply(UnrollingSolver.scala:378)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractFunction$1$2.apply(UnrollingSolver.scala:378)
[Internal] - scala.Option.getOrElse(Option.scala:121)
[error] - scala.Option.getOrElse(Option.scala:121)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.extractFunction$1(UnrollingSolver.scala:378)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$class.extractFunction$1(UnrollingSolver.scala:378)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractValue$1$1.apply(UnrollingSolver.scala:336)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractValue$1$1.apply(UnrollingSolver.scala:336)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractValue$1$1.apply(UnrollingSolver.scala:335)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$extractValue$1$1.apply(UnrollingSolver.scala:335)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[error] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[error] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.extractValue$1(UnrollingSolver.scala:335)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$class.extractValue$1(UnrollingSolver.scala:335)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:453)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:453)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:453)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:453)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Map$Map1.foreach(Map.scala:116)
[error] - scala.collection.immutable.Map$Map1.foreach(Map.scala:116)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[error] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[error] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:179)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:179)
[Internal] - inox.solvers.princess.PrincessSolver$ModelWrapper.getModel(PrincessSolver.scala:93)
[error] - inox.solvers.princess.PrincessSolver$ModelWrapper.getModel(PrincessSolver.scala:93)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:453)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:453)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:583)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:583)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:464)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:464)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[error] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[error] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[error] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:464)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:464)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:277)
[error] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:277)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
[error] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.checkAssumptions(SolverFactory.scala:277)
[error] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.checkAssumptions(SolverFactory.scala:277)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:88)
[error] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:277)
[error] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:277)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
[error] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.check(SolverFactory.scala:277)
[error] - inox.solvers.SolverFactory$$anonfun$getFromName$7$$anon$10.check(SolverFactory.scala:277)
[Internal] - stainless.verification.VerificationChecker$$anonfun$4.apply(VerificationChecker.scala:112)
[error] - stainless.verification.VerificationChecker$$anonfun$4.apply(VerificationChecker.scala:112)
[Internal] - stainless.verification.VerificationChecker$$anonfun$4.apply(VerificationChecker.scala:107)
[error] - stainless.verification.VerificationChecker$$anonfun$4.apply(VerificationChecker.scala:107)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[error] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[error] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:106)
[error] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:106)
[Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:191)
[error] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:191)
[Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:83)
[error] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:83)
[Internal] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:49)
[error] - stainless.verification.VerificationCache$$anonfun$1.apply(VerificationCache.scala:49)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[error] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[error] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:49)
[error] - stainless.verification.VerificationCache$class.checkVC(VerificationCache.scala:49)
[Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:191)
[error] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:191)
[Internal] - stainless.verification.VerificationChecker$$anonfun$2$$anonfun$apply$1.apply(VerificationChecker.scala:76)
[error] - stainless.verification.VerificationChecker$$anonfun$2$$anonfun$apply$1.apply(VerificationChecker.scala:76)
[Internal] - stainless.verification.VerificationChecker$$anonfun$2$$anonfun$apply$1.apply(VerificationChecker.scala:75)
[error] - stainless.verification.VerificationChecker$$anonfun$2$$anonfun$apply$1.apply(VerificationChecker.scala:75)
[Internal] - scala.concurrent.impl.Future$PromiseCompletingRunnable.liftedTree1$1(Future.scala:24)
[error] - scala.concurrent.impl.Future$PromiseCompletingRunnable.liftedTree1$1(Future.scala:24)
[Internal] - scala.concurrent.impl.Future$PromiseCompletingRunnable.run(Future.scala:24)
[error] - scala.concurrent.impl.Future$PromiseCompletingRunnable.run(Future.scala:24)
[Internal] - stainless.package$$anon$5.execute(package.scala:116)
[error] - stainless.package$$anon$5.execute(package.scala:116)
[Internal] - scala.concurrent.impl.ExecutionContextImpl.execute(ExecutionContextImpl.scala:109)
[error] - scala.concurrent.impl.ExecutionContextImpl.execute(ExecutionContextImpl.scala:109)
[Internal] - scala.concurrent.impl.Future$.apply(Future.scala:31)
[error] - scala.concurrent.impl.Future$.apply(Future.scala:31)
[Internal] - scala.concurrent.Future$.apply(Future.scala:494)
[error] - scala.concurrent.Future$.apply(Future.scala:494)
[Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:74)
[error] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:74)
[Internal] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:74)
[error] - stainless.verification.VerificationChecker$$anonfun$2.apply(VerificationChecker.scala:74)
[Internal] - scala.concurrent.Future$$anonfun$traverse$1.apply(Future.scala:576)
[error] - scala.concurrent.Future$$anonfun$traverse$1.apply(Future.scala:576)
[Internal] - scala.concurrent.Future$$anonfun$traverse$1.apply(Future.scala:575)
[error] - scala.concurrent.Future$$anonfun$traverse$1.apply(Future.scala:575)
[Internal] - scala.collection.immutable.Stream.foldLeft(Stream.scala:610)
[error] - scala.collection.immutable.Stream.foldLeft(Stream.scala:610)
[Internal] - scala.concurrent.Future$.traverse(Future.scala:575)
[error] - scala.concurrent.Future$.traverse(Future.scala:575)
[Internal] - stainless.verification.VerificationChecker$class.checkVCs(VerificationChecker.scala:74)
[error] - stainless.verification.VerificationChecker$class.checkVCs(VerificationChecker.scala:74)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:183)
[error] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:183)
[Internal] - stainless.verification.VerificationChecker$class.verify(VerificationChecker.scala:58)
[error] - stainless.verification.VerificationChecker$class.verify(VerificationChecker.scala:58)
[Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:183)
[error] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:183)
[Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:196)
[error] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:196)
[Internal] - stainless.verification.VerificationComponent$.apply(VerificationComponent.scala:45)
[error] - stainless.verification.VerificationComponent$.apply(VerificationComponent.scala:45)
dragos commented 6 years ago

This is only a problem with the princess solver (which is the one that the Sbt plugin uses, I think). It fails in the same way on the command line when passing --solvers=princess, but it works with nativez3.

vkuncak commented 6 years ago

@samarion , shouldn't all solver activities for a given VC, including pre-processing, be encapsulated in some try catch-all to report that error came up during theorem proving?

samarion commented 6 years ago

Fixed in https://github.com/epfl-lara/inox/commit/525e430808b57dd37c925b419352d88ca0ceb191

@vkuncak On one hand I agree from a user perspective, but it makes fixing bugs that are hard to reproduce so much harder that I'm a bit reluctant...