search

utwente-fmt / vercors

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

Attempting to return a resource in PVL triggers NoSuchElementException #1267

Open wandernauta opened 3 days ago

wandernauta commented 3 days ago

In the wiki, the type resource is described as a "Boolean-like type" in the specification language, noting that...

In PVL, the specification types above can also be used in the regular program.

And indeed the following PVL program verifies:

void foo() {
    resource a = true;
    assert a;
}

The following program also verifies (note that bar is not pure):

requires x;
void bar(resource x) {
}

void foo() {
    bar(true);
}

However, the following program causes VerCors to crash with a NoSuchElementException:

resource bar() {
    return true;
}

void foo() {
    assert bar();
}
java.util.NoSuchElementException: head of empty Stack
    at scala.collection.IndexedSeqOps.head(IndexedSeq.scala:99)
    at scala.collection.IndexedSeqOps.head$(IndexedSeq.scala:94)
    at scala.collection.mutable.ArrayDeque.head(ArrayDeque.scala:39)
    at scala.collection.mutable.Stack.top(Stack.scala:115)
    at hre.util.ScopedStack.top(ScopedStack.scala:25)
    at vct.rewrite.EncodeResourceValues.dispatch(EncodeResourceValues.scala:458)
    at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:7)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
    at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
    at vct.col.ast.Procedure.rewrite(Node.scala:702)
    at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
    at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
    at vct.col.ast.Procedure.rewriteDefault(Node.scala:702)
    at vct.col.ast.Procedure.rewriteDefault(Node.scala:702)
    at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:16)
    at vct.col.util.Scopes.$anonfun$dispatch$3(Scopes.scala:137)
    at vct.col.util.Scopes.$anonfun$dispatch$3$adapted(Scopes.scala:136)
    at scala.collection.immutable.List.foreach(List.scala:333)
    at vct.col.util.Scopes.$anonfun$dispatch$2(Scopes.scala:136)
    at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.collect(Scopes.scala:92)
    at vct.col.util.Scopes.dispatch(Scopes.scala:136)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$7(ProgramRewrite.scala:13)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.col.util.Scopes.scope(Scopes.scala:84)
    at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
    at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
    at vct.col.ast.Program.rewrite(Node.scala:111)
    at vct.col.ast.ops.rewrite.ProgramRewrite.rewriteDefault(ProgramRewrite.scala:3)
    at vct.col.ast.ops.rewrite.ProgramRewrite.rewriteDefault$(ProgramRewrite.scala:3)
    at vct.col.ast.Program.rewriteDefault(Node.scala:111)
    at vct.col.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:109)
    at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:109)
    at vct.col.rewrite.NonLatchingRewriter.rewriteDefault(NonLatchingRewriter.scala:8)
    at vct.rewrite.EncodeResourceValues.$anonfun$dispatch$1(EncodeResourceValues.scala:150)
    at hre.util.ScopedStack.having(ScopedStack.scala:35)
    at vct.rewrite.EncodeResourceValues.dispatch(EncodeResourceValues.scala:150)
    at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
    at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
    at vct.col.ast.VerificationContext.rewrite(Node.scala:100)
    at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
    at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
    at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:100)
    at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:4)
    at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:4)
    at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
    at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
    at scala.collection.immutable.List.map(List.scala:246)
    at scala.collection.immutable.List.map(List.scala:79)
    at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
    at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
    at vct.col.ast.Verification.rewrite(Node.scala:94)
    at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
    at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
    at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
    at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:3)
    at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:3)
    at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
    at vct.main.stages.Transformation.liftedTree1$1(Transformation.scala:239)
    at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:239)
    at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:233)
    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.Transformation.$anonfun$run$2(Transformation.scala:233)
    at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
    at vct.main.stages.Transformation.run(Transformation.scala:227)
    at vct.main.stages.Transformation.run(Transformation.scala:200)
    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)
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

If bar is marked pure, the error goes away.

Version: 3313255 (dev branch).

This issue was found by fuzzing.

bobismijnnaam commented 2 days ago

@wandernauta For context, VerCors supports some degree of first class permissions:

class C {
    int x;
}

void m(C c) {
  resource a = Perm(c.x, 1);
  exhale a;
}

Currently it's not the case because of some other bug but that's an easy fix.

I'll have a quick look to see if it's worth fixing this because the support is quite experimental, so I might just put a try/catch wrapper around it for a friendly message.

bobismijnnaam commented 2 days ago

To fix this, we need to make sure Return is actually typechecked. This can be done by adding an intermediate AmbiguousReturn(Expr), which is transformed into a Return(Expr, Ref[AbstractMethod]) after the resolution phase. Typechecking then needs to be added here:

https://github.com/utwente-fmt/vercors/blob/33132556d2619e2dd88e55f2a5dadd5aa03869ce/src/col/vct/col/typerules/CoercingRewriter.scala#L2274)

This is a bit of a bigger project because, while the AST changes are logical and straightforward, it's not really clear how many passes require extra bookkeeping to construct a proper back pointer to the successor of the current method being rewritten. For now I'm just adding a proper error that resource values as method return types are not supported with a link to this issue.