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

Neglecting to specify type arguments in PVL new expression triggers crash #1268

Closed wandernauta closed 1 month ago

wandernauta commented 1 month ago

The following (bogus) PVL program causes VerCors to crash with a seemingly unrelated exception:

class X<T> {
}

void main() {
    new X();
}
[54.7%] VerCors › Transformation › monomorphizeClassException in thread "[VerCors] Block layout updates" hre.progress.ProgressLogicError: The amount of progress (1.1759259259259283) exceeds the range [0; 1] at trail: root > Transformation
    at hre.progress.task.AbstractTask.progress(AbstractTask.scala:37)
    at hre.progress.task.AbstractTask.$anonfun$progress$1(AbstractTask.scala:22)
    at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
    at scala.collection.StrictOptimizedIterableOps.map$(StrictOptimizedIterableOps.scala:87)
    at scala.collection.mutable.ArrayBuffer.map(ArrayBuffer.scala:43)
    at hre.progress.task.AbstractTask.progress(AbstractTask.scala:22)
    at hre.progress.Layout.progressEstimate(Layout.scala:85)
    at hre.progress.Layout.progressBadge(Layout.scala:87)
    at hre.progress.Layout.updateProgressMessage(Layout.scala:119)
    at hre.progress.Layout.update(Layout.scala:135)
    at hre.progress.Layout$.update(Layout.scala:19)
    at hre.progress.Progress$$anon$1.run(Progress.scala:72)
    at java.base/java.util.TimerThread.mainLoop(Timer.java:566)
    at java.base/java.util.TimerThread.run(Timer.java:516)
[ERROR] An error occurred in pass monomorphizeClass
[INFO] Done: VerCors (at 20:27:27, duration: 00:00:03)
hre.debug.TimeTravel$CauseWithBadEffect: This trace causes an error later on: 
======================================
1 
    2 class X T_1606662456> {
         [----------------------
    3     constructor(int tid) {
    4         Object exc;
    5         exc = null;
    6         label BUBBLE;
    7         
    8         assert exc == null;
    9     }
      -----]
   10 }
   11
--------------------------------------
[1/2] A reference to the successor of this declaration was made, ...
--------------------------------------
15     ?brokenref? res1;
   16     exc = null;
         [--------------------------------------------------------------------------------------------------------
   17     ??InvokeConstructor??(Ref(?brokenref?), Nil$(), res1, $colon$colon(tid), Nil$(), Nil$(), Nil$(), Nil$())
          --------------------------------------------------------------------------------------------------------]
   18     res1;
   19     label END;
--------------------------------------
[2/2] ... but it has no successor in this position.
======================================
    at hre.debug.TimeTravel$.cause(TimeTravel.scala:49)
    at vct.col.util.FrozenScopes.$anonfun$succ$1(FrozenScopes.scala:32)
    at vct.result.VerificationError$.withContext(VerificationError.scala:61)
    at vct.col.util.FrozenScopes.succ(FrozenScopes.scala:32)
    at vct.col.ast.AllScopes.succ(AllScopes.scala:184)
    at vct.col.ast.AbstractRewriter.succ(AbstractRewriter.scala:15)
    at vct.col.ast.AbstractRewriter.succ$(AbstractRewriter.scala:15)
    at vct.col.rewrite.NonLatchingRewriter.succ(NonLatchingRewriter.scala:8)
    at vct.col.ast.ops.rewrite.InvokeConstructorRewrite.$anonfun$rewrite$1(InvokeConstructorRewrite.scala:6)
    at scala.Option.getOrElse(Option.scala:201)
    at vct.col.ast.ops.rewrite.InvokeConstructorRewrite.rewrite(InvokeConstructorRewrite.scala:6)
    at vct.col.ast.ops.rewrite.InvokeConstructorRewrite.rewrite$(InvokeConstructorRewrite.scala:4)
    at vct.col.ast.InvokeConstructor.rewrite(Node.scala:493)
    at vct.col.ast.ops.rewrite.InvokeConstructorRewrite.rewriteDefault(InvokeConstructorRewrite.scala:3)
    at vct.col.ast.ops.rewrite.InvokeConstructorRewrite.rewriteDefault$(InvokeConstructorRewrite.scala:3)
    at vct.col.ast.InvokeConstructor.rewriteDefault(Node.scala:493)
    at vct.col.ast.InvokeConstructor.rewriteDefault(Node.scala:493)
    at vct.rewrite.MonomorphizeClass.dispatch(MonomorphizeClass.scala:185)
    at vct.col.ast.ops.rewrite.BlockRewrite.$anonfun$rewrite$1(BlockRewrite.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.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.rewrite.MonomorphizeClass.dispatch(MonomorphizeClass.scala:185)
    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.rewrite.MonomorphizeClass.dispatch(MonomorphizeClass.scala:185)
    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.rewrite.MonomorphizeClass.dispatch(MonomorphizeClass.scala:130)
    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: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.util.ScopedStack.having(ScopedStack.scala:35)
    at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:37)
    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] !*!*!*!*!*!*!*!*!*!*!*!

I would instead expect a type error to be logged. Providing too many type arguments causes VerCors to log a type error, as expected. Providing angle brackets but no type arguments is a syntax error.

Version: https://github.com/utwente-fmt/vercors/commit/33132556d2619e2dd88e55f2a5dadd5aa03869ce (dev branch).

This issue was found by fuzzing.

superaxander commented 1 month ago

Yeah so the successor of a class with type arguments and its methods are declared in an InstantiationContext instead of the normal scope. Since the InvokeConstructor node does not name generic type arguments it is rewritten normally and looks for the successor in the normal scope. We could add a case to check for this case where a constructor does not name any type arguments but the class does. However in Java it's allowed to instantiate a class while omitting the type arguments so if we want to support that. I guess we'd have to make the InvokeConstructor call refer to the version that is always instantiated. (the one with keepBodies=true) We could do that explicitly or make that version the successor of the old class in the normal scope.

bobismijnnaam commented 1 month ago

Or we can choose to not support the Java edge case, and leave it for the person who will finalize the generics support. That might make things easier? It's just one line in the check method of the relevant nodes, right?

superaxander commented 1 month ago

Yes that's also possible, I have no particular preference

bobismijnnaam commented 1 month ago

Related: e90a6745fae3499983e240b2adb11fb903d7b40c