lock/unlock statement with literal null triggers UnreachableAfterTypeCheck

[wandernauta]

Per the wiki, the lock statement takes an object o "where o can be an arbitrary expression. The only constraint is that o is not null."

This nullness is checked: for the following PVL program, "Lock target may be null" is reported pointing at the offending lock statement, as expected:

class a {
}

void example() {
    a thing = null;
    lock thing;
}

However, passing a literal null causes an UnreachableAfterTypeCheck error:

void example() {
    lock null;
}

Such a program is clearly wrong, and I don't think that users would write this accidentally, but it would perhaps still be nicer to show a similar "Lock target may be null" message here (or even "Lock target is null").

A similar case seems to apply to the unlock, wait, notify and synchronized statements.

[INFO] Start: VerCors (at 09:58:46)
[INFO] Done: VerCors (at 09:58:47, duration: 00:00:01)
vct.col.check.UnreachableAfterTypeCheck: A condition was reached that should have been excluded by the type check. Either a property of a node was queried before the type check, or the type check is missing a condition. The node says: This argument is not a class type.
	at vct.col.rewrite.EncodeIntrinsicLock.getClass(EncodeIntrinsicLock.scala:93)
	at vct.col.rewrite.EncodeIntrinsicLock.needHeld(EncodeIntrinsicLock.scala:98)
	at vct.col.rewrite.EncodeIntrinsicLock.$anonfun$dispatch$1(EncodeIntrinsicLock.scala:104)
	at vct.col.rewrite.EncodeIntrinsicLock.$anonfun$dispatch$1$adapted(EncodeIntrinsicLock.scala:103)
	at vct.col.ast.node.NodeSubnodeOps.visit(NodeSubnodeOps.scala:11)
	at vct.col.ast.node.NodeSubnodeOps.visit$(NodeSubnodeOps.scala:10)
	at vct.col.ast.Lock.visit(Node.scala:424)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1$adapted(NodeSubnodeOps.scala:12)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.ast.node.NodeSubnodeOps.visit(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.visit$(NodeSubnodeOps.scala:10)
	at vct.col.ast.Block.visit(Node.scala:537)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1$adapted(NodeSubnodeOps.scala:12)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.ast.node.NodeSubnodeOps.visit(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.visit$(NodeSubnodeOps.scala:10)
	at vct.col.ast.Scope.visit(Node.scala:546)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1$adapted(NodeSubnodeOps.scala:12)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.ast.node.NodeSubnodeOps.visit(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.visit$(NodeSubnodeOps.scala:10)
	at vct.col.ast.Procedure.visit(Node.scala:702)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.$anonfun$visit$1$adapted(NodeSubnodeOps.scala:12)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.ast.node.NodeSubnodeOps.visit(NodeSubnodeOps.scala:12)
	at vct.col.ast.node.NodeSubnodeOps.visit$(NodeSubnodeOps.scala:10)
	at vct.col.ast.Program.visit(Node.scala:111)
	at vct.col.ast.node.NodeSubnodeOps.foreach(NodeSubnodeOps.scala:15)
	at vct.col.ast.node.NodeSubnodeOps.foreach$(NodeSubnodeOps.scala:15)
	at vct.col.ast.Program.foreach(Node.scala:111)
	at vct.col.rewrite.EncodeIntrinsicLock.dispatch(EncodeIntrinsicLock.scala:103)
	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.