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

Referring to sibling par in barrier inside 'sequential' or 'parallel' fails #1307

Open
wandernauta opened this issue Feb 10, 2025 · 0 comments
Open

Referring to sibling par in barrier inside 'sequential' or 'parallel' fails #1307

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

Comments

@wandernauta
Copy link
Contributor

Attempting to verify the following (faulty) PVL input fails with a time travel exception:

void x() {
    sequential {
        par ty {}
        par barrier(ty) {}
    }
}

A reference to the successor of this declaration was made, but it has no successor.

The outer sequential block can also be a parallel block (but not a par block). If the par barrier(ty) block is moved inside the par ty block, verification succeeds. The other way around, an error message is printed, as expected.

hre.debug.TimeTravel$RepeatUntilCause: ======================================
--------------------------------------
    1  void x() {
    2      sequential {
              [---------
    3          par ty {}
               ---------]
    4          par barrier(ty) {}
    5      }
--------------------------------------
A reference to the successor of this declaration was made, but it has no successor.
======================================
	at hre.debug.TimeTravel$.badEffect(TimeTravel.scala:55)
	at vct.col.util.FrozenScopes.$anonfun$succ$4(FrozenScopes.scala:35)
	at scala.Option.getOrElse(Option.scala:201)
	at vct.col.util.FrozenScopes.$anonfun$succ$3(FrozenScopes.scala:35)
	at vct.col.ref.LazyRef.decl$lzycompute(LazyRef.scala:27)
	at vct.col.ref.LazyRef.decl(LazyRef.scala:26)
	at vct.col.ast.ops.rewrite.ParBarrierRewrite.$anonfun$rewrite$1(ParBarrierRewrite.scala:6)
	at scala.Option.getOrElse(Option.scala:201)
	at vct.col.ast.ops.rewrite.ParBarrierRewrite.rewrite(ParBarrierRewrite.scala:6)
	at vct.col.ast.ops.rewrite.ParBarrierRewrite.rewrite$(ParBarrierRewrite.scala:4)
	at vct.col.ast.ParBarrier.rewrite(Node.scala:618)
	at vct.col.ast.ops.rewrite.ParBarrierRewrite.rewriteDefault(ParBarrierRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ParBarrierRewrite.rewriteDefault$(ParBarrierRewrite.scala:3)
	at vct.col.ast.ParBarrier.rewriteDefault(Node.scala:618)
	at vct.col.ast.ParBarrier.rewriteDefault(Node.scala:618)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:11)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:11)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	at vct.col.ast.ops.rewrite.ParBlockRewrite.$anonfun$rewrite$4(ParBlockRewrite.scala:25)
	at hre.util.ScopedStack.having(ScopedStack.scala:35)
	at vct.col.util.Scopes.scope(Scopes.scala:84)
	at vct.col.ast.ops.rewrite.ParBlockRewrite.$anonfun$rewrite$3(ParBlockRewrite.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.ParBlockRewrite.$anonfun$rewrite$2(ParBlockRewrite.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.ParBlockRewrite.$anonfun$rewrite$1(ParBlockRewrite.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.ParBlockRewrite.rewrite(ParBlockRewrite.scala:5)
	at vct.col.ast.ops.rewrite.ParBlockRewrite.rewrite$(ParBlockRewrite.scala:4)
	at vct.col.ast.ParBlock.rewrite(Node.scala:267)
	at vct.col.ast.ops.rewrite.ParBlockRewrite.rewriteDefault(ParBlockRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ParBlockRewrite.rewriteDefault$(ParBlockRewrite.scala:3)
	at vct.col.ast.ParBlock.rewriteDefault(Node.scala:267)
	at vct.col.ast.ParBlock.rewriteDefault(Node.scala:267)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:7)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:7)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	at vct.col.ast.ops.rewrite.ParSequentialRewrite.$anonfun$rewrite$1(ParSequentialRewrite.scala:6)
	at scala.collection.immutable.List.map(List.scala:250)
	at scala.collection.immutable.List.map(List.scala:79)
	at vct.col.ast.ops.rewrite.ParSequentialRewrite.rewrite(ParSequentialRewrite.scala:6)
	at vct.col.ast.ops.rewrite.ParSequentialRewrite.rewrite$(ParSequentialRewrite.scala:4)
	at vct.col.ast.ParSequential.rewrite(Node.scala:259)
	at vct.col.ast.ops.rewrite.ParSequentialRewrite.rewriteDefault(ParSequentialRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ParSequentialRewrite.rewriteDefault$(ParSequentialRewrite.scala:3)
	at vct.col.ast.ParSequential.rewriteDefault(Node.scala:259)
	at vct.col.ast.ParSequential.rewriteDefault(Node.scala:259)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:7)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:7)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	at vct.col.ast.ops.rewrite.ParStatementRewrite.rewrite(ParStatementRewrite.scala:6)
	at vct.col.ast.ops.rewrite.ParStatementRewrite.rewrite$(ParStatementRewrite.scala:4)
	at vct.col.ast.ParStatement.rewrite(Node.scala:628)
	at vct.col.ast.ops.rewrite.ParStatementRewrite.rewriteDefault(ParStatementRewrite.scala:3)
	at vct.col.ast.ops.rewrite.ParStatementRewrite.rewriteDefault$(ParStatementRewrite.scala:3)
	at vct.col.ast.ParStatement.rewriteDefault(Node.scala:628)
	at vct.col.ast.ParStatement.rewriteDefault(Node.scala:628)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:11)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:11)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	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.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:11)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:11)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	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.rewrite.BaseNonLatchingRewriter.dispatch(BaseNonLatchingRewriter.scala:11)
	at vct.col.ast.rewrite.BaseNonLatchingRewriter.dispatch$(BaseNonLatchingRewriter.scala:11)
	at vct.col.rewrite.NonLatchingRewriter.dispatch(NonLatchingRewriter.scala:8)
	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)
	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)
[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 Feb 10, 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