Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Empty sequential block triggers error in ParBlockEncoder.check #1299

Open
wandernauta opened this issue Jan 5, 2025 · 0 comments
Open

Empty sequential block triggers error in ParBlockEncoder.check #1299

wandernauta opened this issue Jan 5, 2025 · 0 comments
Labels
A-Bug F-PVL Frontend: PVL Fuzzing Found by fuzzing

Comments

@wandernauta
Copy link
Contributor

The PVL grammar allows a sequential block to be empty, for example:

void x() {
    sequential {
    }
}

The intended meaning would perhaps be to do nothing sequentially. However, ParBlockEncoder.check assumes that there is always at least one region, since it calls regions.tail, which triggers an UnsupportedOperationException in this case.

[INFO] Start: VerCors (at 18:31:24)
[INFO] Done: VerCors (at 18:31:25, duration: 00:00:01)
vct.result.VerificationError$Crash: VerCors crashed near this position. Cause follows:
	at vct.result.VerificationError$.withContext(VerificationError.scala:68)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:12)
	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:267)
	at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:267)
	at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:259)
	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:259)
	at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
	at vct.main.stages.Transformation.run(Transformation.scala:253)
	at vct.main.stages.Transformation.run(Transformation.scala:226)
	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)
Caused by: java.lang.UnsupportedOperationException: tail of empty list
	at scala.collection.immutable.Nil$.tail(List.scala:664)
	at scala.collection.immutable.Nil$.tail(List.scala:661)
	at vct.col.rewrite.ParBlockEncoder.check(ParBlockEncoder.scala:283)
	at vct.col.rewrite.ParBlockEncoder.$anonfun$dispatch$2(ParBlockEncoder.scala:352)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.rewrite.ParBlockEncoder.dispatch(ParBlockEncoder.scala:349)
	at vct.col.ast.ops.rewrite.BlockRewrite.$anonfun$rewrite$1(BlockRewrite.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.BlockRewrite.rewrite(BlockRewrite.scala:6)
	at vct.col.ast.ops.rewrite.BlockRewrite.rewrite$(BlockRewrite.scala:4)
	at vct.col.ast.Block.rewrite(Node.scala:537)
	at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault(BlockRewrite.scala:3)
	at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault$(BlockRewrite.scala:3)
	at vct.col.ast.Block.rewriteDefault(Node.scala:537)
	at vct.col.ast.Block.rewriteDefault(Node.scala:537)
	at vct.col.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:116)
	at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:116)
	at vct.col.rewrite.NonLatchingRewriter.rewriteDefault(NonLatchingRewriter.scala:8)
	at vct.col.rewrite.ParBlockEncoder.dispatch(ParBlockEncoder.scala:433)
	at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$5(ScopeRewrite.scala:14)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$4(ScopeRewrite.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.ScopeRewrite.$anonfun$rewrite$3(ScopeRewrite.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.ScopeRewrite.$anonfun$rewrite$2(ScopeRewrite.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.ScopeRewrite.$anonfun$rewrite$1(ScopeRewrite.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.ScopeRewrite.rewrite(ScopeRewrite.scala:5)
	at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite$(ScopeRewrite.scala:4)
	at vct.col.ast.Scope.rewrite(Node.scala:546)
	at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault(ScopeRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault$(ScopeRewrite.scala:3)
	at vct.col.ast.Scope.rewriteDefault(Node.scala:546)
	at vct.col.ast.Scope.rewriteDefault(Node.scala:546)
	at vct.col.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:116)
	at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:116)
	at vct.col.rewrite.NonLatchingRewriter.rewriteDefault(NonLatchingRewriter.scala:8)
	at vct.col.rewrite.ParBlockEncoder.dispatch(ParBlockEncoder.scala:433)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$2(ProcedureRewrite.scala:19)
	at scala.Option.map(Option.scala:242)
	at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:19)
	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.rewrite.NonLatchingRewriter.$anonfun$dispatch$1(NonLatchingRewriter.scala:12)
	at vct.result.VerificationError$.withContext(VerificationError.scala:61)
	... 68 more
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

Version: 2bd3bca (dev branch).

This issue was found by fuzzing.
@superaxander superaxander added A-Bug F-PVL Frontend: PVL Fuzzing Found by fuzzing labels Jan 6, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
A-Bug F-PVL Frontend: PVL Fuzzing Found by fuzzing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@wandernauta @superaxander