search

utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
56 stars 26 forks source link

Crash report: Viper has crashed: java.util.NoSuchElementException: None.get #1275

Open etiennebirling opened 1 month ago

etiennebirling commented 1 month ago

Crash Message

Viper has crashed: java.util.NoSuchElementException: None.get
  at viper.api.backend.SilverBackend.processError(SilverBackend.scala:376)
  at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:172)
  at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34)
  at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:164)
  at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:164)
  at scala.collection.immutable.List.foreach(List.scala:333)
  at viper.api.backend.SilverBackend.submit(SilverBackend.scala:164)
  at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:143)
  at viper.api.backend.silicon.Silicon.submit(Silicon.scala:34)
  at vct.main.stages.SilverBackend.verify(Backend.scala:201)
  at vct.main.stages.Backend.$anonfun$run$6(Backend.scala:166)
  at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:106)
  ...
  at vct.main.Main$.main(Main.scala:50)
  at vct.main.Main.main(Main.scala)

Version Information

Arguments

forperm.c

File Inputs

forperm.c ```c struct t {int val;}; struct f {int cac;}; /*@ requires \pointer(this, 10, write); requires Perm(this->val, 1); ensures \pointer(this, 10, write); ensures \polarity_dependent(true, (\forperm struct f * this \in this->cac; false)); ensures Perm(this->val, 1); @*/ void incr(struct t* this, int n) { this->val = this->val + n; } ```

Full Log

``` 17:15:02.719 [INFO] Start: VerCors (at 17:15:02) 17:15:07.230 [WARN] Possible viper bug: silver AST does not reparse when printing as text 17:15:07.230 [WARN] Quantified arguments can only be used directly (vercors-267072219603548256.sil@238.31--238.70) 17:15:08.109 [INFO] Done: VerCors (at 17:15:08, duration: 00:00:05) 17:15:08.114 [ERROR] viper.api.backend.SilverBackend$ViperCrashed: Viper has crashed: java.util.NoSuchElementException: None.get at viper.api.backend.SilverBackend.processError(SilverBackend.scala:376) at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:172) at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34) at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:164) at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:164) at scala.collection.immutable.List.foreach(List.scala:333) at viper.api.backend.SilverBackend.submit(SilverBackend.scala:164) at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:143) at viper.api.backend.silicon.Silicon.submit(Silicon.scala:34) at vct.main.stages.SilverBackend.verify(Backend.scala:201) at vct.main.stages.Backend.$anonfun$run$6(Backend.scala:166) at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:106) at scala.Option.getOrElse(Option.scala:201) at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:104) at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate$(Backend.scala:100) at vct.main.stages.SilverBackend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:184) at vct.main.stages.Backend.$anonfun$run$5(Backend.scala:166) at vct.main.stages.Backend.$anonfun$run$5$adapted(Backend.scala:163) at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:25) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18) at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166) at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:25) at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:24) at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576) at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574) at scala.collection.AbstractIterator.foreach(Iterator.scala:1300) at hre.progress.Progress$.foreach(Progress.scala:24) at vct.main.stages.Backend.$anonfun$run$1(Backend.scala:163) at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16) at hre.progress.Progress$.stages(Progress.scala:47) at vct.main.stages.Backend.run(Backend.scala:145) at vct.main.stages.Backend.run$(Backend.scala:137) at vct.main.stages.SilverBackend.run(Backend.scala:184) at vct.main.stages.SilverBackend.run(Backend.scala:184) at hre.stages.Stages.$anonfun$run$3(Stages.scala:104) at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101) at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576) at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574) at scala.collection.AbstractIterable.foreach(Iterable.scala:933) at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903) at hre.stages.Stages.$anonfun$run$1(Stages.scala:101) at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16) at hre.progress.Progress$.stages(Progress.scala:47) at hre.stages.Stages.run(Stages.scala:98) at hre.stages.Stages.run$(Stages.scala:95) at hre.stages.StagesPair.run(Stages.scala:145) at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64) at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.util.Time$.logTime(Time.scala:23) at vct.main.modes.Verify$.runOptions(Verify.scala:99) at vct.main.Main$.runMode(Main.scala:107) at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.middleware.Middleware$.using(Middleware.scala:78) at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.io.Watch$.booleanWithWatch(Watch.scala:58) at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100) at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17) at hre.middleware.Middleware$.using(Middleware.scala:78) at vct.main.Main$.runOptions(Main.scala:95) at vct.main.Main$.main(Main.scala:50) at vct.main.Main.main(Main.scala) 17:15:08.114 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 17:15:08.114 [ERROR] ! VerCors has crashed ! 17:15:08.114 [ERROR] !*!*!*!*!*!*!*!*!*!*!*! 17:15:08.115 [ERROR] Please report this as a bug here: ```
etiennebirling commented 1 month ago

Note that this also seems to occur when reversing the polarity

superaxander commented 4 weeks ago

This crash occurs because we ignore Viper's checks that happen after parsing. In your output log you can see the line:

[WARN] Quantified arguments can only be used directly (vercors-267072219603548256.sil@238.31--238.70)

Which notifies us of the actual problem which is that you can only put a direct expression in between \in and ;.

If I'm understanding correctly what you're trying to do, you could write this as:

\polarity_dependent(true, (\forperm struct f r \in r.cac; r != *this));

Note that this will stop working in a future version of VerCors since the way we encode C structs has changed quite a lot. (and I didn't consider the use of forperm with C structs while making these changes)

etiennebirling commented 4 weeks ago

Thanks for your answer. Do you call the value this a direct expression because it refers to an argument? I tried to replace it with r as you suggested but the thing still crashes (same bug report).

Regarding the formula itself, no I think you did not get correctly what I mean. What I am trying to phrase is "No permission to any cac field of a struct t instance is held" (meaning no permission overall, not just forbidding to hold the cac field of this specifically). That is not what your suggested formula describes, right?

superaxander commented 4 weeks ago

I'm not 100% sure what they mean by direct expression in Viper but I guess basically anything of the form a.b is a direct expression of a, but most other things (such as the pointer dereferences that happen in your example) aren't.

I guess because the only things with a field cac will be the struct f you could just do \forperm struct f r \in r.cac; false. (note if there are multiple structs with fields with the name cac this will still work since VerCors will give them different names internally)

etiennebirling commented 4 weeks ago

Ok, I understand. You suggestion worked to fix the problem. Thanks for the help.