From 327755ec8a9ce2031cf6d32bcce5d0b49a649767 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Wed, 20 Sep 2023 13:57:01 +0300 Subject: [PATCH] Fixed ensuring enum correctness for Java 17 (#68) --- .../machine/interpreter/JcExprResolver.kt | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt index 7fd0043522..2d1a5510bd 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt @@ -985,16 +985,25 @@ class JcExprResolver( } /** - * Always use negative addresses in enum static initializers, - * for static initializers of other classes depends on [JcContext.useNegativeAddressesInStaticInitializer]. + * Always use negative addresses in enum static initializers and enum methods + * that were reached from the corresponding static initializer, for static initializers of other classes + * depends on [JcContext.useNegativeAddressesInStaticInitializer]. */ fun JcState.useStaticAddressForAllocation(): Boolean { - val isEnumStaticInitializer = lastEnteredMethod.let { it.isClassInitializer && it.enclosingClass.isEnum } - if (isEnumStaticInitializer) { + val staticInitializers = callStack.filter { it.method.isClassInitializer } + + // Enum's static initializer may contain invocations of other methods – from this enum or from other classes. + // In case of enum methods, we need to consider all refs allocated in these methods as static too. It is important + // because these refs may be assigned to enum's static fields – $VALUES, for example. + val currentClass = lastEnteredMethod.enclosingClass + val inEnumMethodFromEnumStaticInitializer = + currentClass.isEnum && staticInitializers.any { it.method.enclosingClass == currentClass } + + if (inEnumMethodFromEnumStaticInitializer) { return true } - return ctx.useNegativeAddressesInStaticInitializer && callStack.any { it.method.isClassInitializer } + return ctx.useNegativeAddressesInStaticInitializer && staticInitializers.isNotEmpty() } /**