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.

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

JRE reflection-based shimming fails for types that contain arrays #1295

Open
wandernauta opened this issue Dec 11, 2024 · 0 comments
Open

JRE reflection-based shimming fails for types that contain arrays #1295

wandernauta opened this issue Dec 11, 2024 · 0 comments
Labels
A-Bug F-Java Frontend: Java Fuzzing Found by fuzzing

Comments

@wandernauta
Copy link
Contributor

wandernauta commented Dec 11, 2024

VerCors can demand-load shims for classes from the current JRE using reflection. However, this seems to fail for classes that use arrays of primitives, for instance:

import java.util.UUID;

class Foo {
    UUID example;
}

gives

[INFO] Start: VerCors (at 17:09:15)
[WARN] Attempting to load a shim of java.util.UUID via reflection.
[WARN] Attempting to load a shim of [B via reflection.
[WARN] Attempting to load a shim of java.lang.[B via reflection.
[INFO] Done: VerCors (at 17:09:16, duration: 00:00:00)
vct.result.VerificationError$Unreachable: Invalid JRE: The type `[B` built in to the JRE could not be loaded.

where [B is byte[].

	at vct.col.resolve.lang.Java$.$anonfun$lazyType$3(Java.scala:221)
	at scala.Option.getOrElse(Option.scala:201)
	at vct.col.resolve.lang.Java$.lazyType(Java.scala:220)
	at vct.col.resolve.lang.Java$.lazyType(Java.scala:205)
	at vct.col.resolve.lang.Java$.lazyType(Java.scala:194)
	at vct.col.resolve.lang.Java$.translateRuntimeType(Java.scala:297)
	at vct.col.resolve.lang.Java$.translateRuntimeParameter(Java.scala:304)
	at vct.col.resolve.lang.Java$.$anonfun$translateRuntimeClass$4(Java.scala:371)
	at scala.collection.immutable.ArraySeq.map(ArraySeq.scala:75)
	at scala.collection.immutable.ArraySeq.map(ArraySeq.scala:35)
	at vct.col.resolve.lang.Java$.$anonfun$translateRuntimeClass$3(Java.scala:370)
	at scala.collection.ArrayOps$.map$extension(ArrayOps.scala:934)
	at vct.col.resolve.lang.Java$.translateRuntimeClass(Java.scala:357)
	at vct.col.resolve.lang.Java$.findRuntimeJavaType(Java.scala:247)
	at vct.col.resolve.lang.Java$.$anonfun$findJavaTypeName$7(Java.scala:534)
	at hre.util.FuncTools$.$anonfun$firstOption$4(FuncTools.scala:13)
	at scala.Option.orElse(Option.scala:477)
	at hre.util.FuncTools$.$anonfun$firstOption$3(FuncTools.scala:13)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at hre.util.FuncTools$.firstOption(FuncTools.scala:13)
	at vct.col.resolve.lang.Java$.$anonfun$findJavaTypeName$6(Java.scala:534)
	at scala.Option.orElse(Option.scala:477)
	at vct.col.resolve.lang.Java$.findJavaTypeName(Java.scala:535)
	at vct.col.resolve.ResolveTypes$.resolveOne(Resolve.scala:213)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:137)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1$adapted(Resolve.scala:136)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1$adapted(Resolve.scala:136)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1$adapted(Resolve.scala:136)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.$anonfun$resolve$1$adapted(Resolve.scala:136)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:136)
	at vct.col.resolve.ResolveTypes$.resolve(Resolve.scala:130)
	at vct.main.stages.Resolution.run(Resolution.scala:143)
	at vct.main.stages.Resolution.run(Resolution.scala:120)
	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: 077f8b9 (dev branch).

This issue was found by fuzzing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-Bug F-Java Frontend: Java Fuzzing Found by fuzzing
Projects
None yet
Development

No branches or pull requests

2 participants