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

fork/join statement with literal null triggers ClassCastException #1300

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

fork/join statement with literal null triggers ClassCastException #1300

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 fork statement expects an object-typed expression of a class that has a run method, but the grammar also allows a literal null:

void spork() {
    fork null;
}

This passes at least some type checks, but then causes a "java.lang.ClassCastException: class vct.col.ast.TNull cannot be cast to class vct.col.ast.TClass" in the code that checks whether the expression is a runnable.

If, instead of a literal null, a reference is passed to an object that may be null, the issue does not appear; this is in some ways similar to #1298.

[INFO] Start: VerCors (at 19:29:41)
[INFO] Done: VerCors (at 19:29:43, 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.ClassCastException: class vct.col.ast.TNull cannot be cast to class vct.col.ast.TClass (vct.col.ast.TNull and vct.col.ast.TClass are in unnamed module of loader 'app')
	at vct.col.rewrite.EncodeForkJoin.getRunnableClass(EncodeForkJoin.scala:278)
	at vct.col.rewrite.EncodeForkJoin.dispatch(EncodeForkJoin.scala:81)
	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.EncodeForkJoin.dispatch(EncodeForkJoin.scala:104)
	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.EncodeForkJoin.dispatch(EncodeForkJoin.scala:104)
	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.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:7)
	at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:7)
	at vct.col.rewrite.NonLatchingRewriter.rewriteDefault(NonLatchingRewriter.scala:8)
	at vct.col.rewrite.EncodeForkJoin.dispatch(EncodeForkJoin.scala:264)
	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