Generic classes with final fields trigger TransformationCheckError, crash

[wandernauta]

The following PVL program causes the constantFinalFields rewrite to generate an AST that no longer typechecks, which triggers a VerCors crash:

class C <T> {
    final int f;
}

The col file before the rewrite is:

class C<type<any> T_673129458> {
    final int f;
    
    constructor(int tid) {
        
    }
}

The col file after the rewrite is:

requires f != null;
decreases;
pure int f(C<T_1373361892> f);


class C<type<any> T_1373361892> {
    constructor(int tid) {
        
    }
}

vct.main.stages.Transformation$TransformationCheckError: The constantFinalFields rewrite caused the AST to no longer typecheck:
======================================
1 requires f != null;
    2 decreases;
                  [------------
    3 pure int f(C f);
                   ------------]
    4 
    5
--------------------------------------
[1/2] This usage is out of scope,
--------------------------------------
4 
    5 
             [----------------------
    6 class C T_1373361892> {
              ----------------------]
    7     constructor(int tid) {
    8
--------------------------------------
[2/2] since it is declared here.
======================================
	at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:263)
	at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:238)
	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:238)
	at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
	at vct.main.stages.Transformation.run(Transformation.scala:232)
	at vct.main.stages.Transformation.run(Transformation.scala:205)
	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] !*!*!*!*!*!*!*!*!*!*!*!

This issue was found by fuzzing.

[bobismijnnaam]

Looks like the constantFinalFields rewrite is not generics-aware. Post-rewrite f should get a generics argument itself. Since generics support in VerCors is at the moment spotty at best, it would be fine to not support this use case for now, and throw a usererror here whenever a (static) final field occurs in a class. Making the constantFinalFields class generics-aware should also not be too complicated a task.