Fixed reading by null ref during ensuring enum correctness (#105)

UnitTestBot · Nov 16, 2023 · 7990696 · 7990696
1 parent 39f1845
commit 7990696
Show file tree

Hide file tree

Showing 3 changed files with 50 additions and 0 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
@@ -91,6 +91,7 @@ import org.usvm.UBvSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UNullRef
 import org.usvm.USort
 import org.usvm.api.allocateArrayInitialized
 import org.usvm.collection.array.UArrayIndexLValue
@@ -569,6 +570,11 @@ class JcExprResolver(
             return Unit
         }
 
+        // For null enum values, we do not need any correctness constraints
+        if (enumInstance is UNullRef) {
+            return Unit
+        }
+
         val enumValues = type.enumValues
 
         val maxOrdinalValue = enumValues!!.size.toBv()

diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnumField.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnumField.java
@@ -0,0 +1,23 @@
+package org.usvm.samples.enums;
+
+import org.usvm.samples.enums.ClassWithEnum.StatusEnum;
+
+public class ClassWithEnumField {
+    // Make it public for simpler extracting in tests
+    public StatusEnum statusEnum = null;
+
+    public void setStatusEnum(StatusEnum statusEnum) {
+        this.statusEnum = statusEnum;
+    }
+
+    public int getStatusCode(int initField) {
+        ClassWithEnumField classWithEnumField = new ClassWithEnumField();
+        if (initField == -1) {
+            classWithEnumField.setStatusEnum(StatusEnum.READY);
+        } else if (initField == 1) {
+            classWithEnumField.setStatusEnum(StatusEnum.ERROR);
+        }
+
+        return classWithEnumField.statusEnum.code;
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumFieldTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumFieldTest.kt
@@ -0,0 +1,21 @@
+package org.usvm.samples.enums
+
+import org.junit.jupiter.api.Test
+import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.samples.enums.ClassWithEnum.StatusEnum
+import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
+import org.usvm.util.isException
+import kotlin.math.abs
+
+class ClassWithEnumFieldTest : JavaMethodTestRunner() {
+    @Test
+    fun testEnumFieldCode() {
+        checkDiscoveredPropertiesWithExceptions(
+            ClassWithEnumField::getStatusCode,
+            ignoreNumberOfAnalysisResults,
+            { _, i, r -> abs(i) != 1 && r.isException<NullPointerException>() },
+            { _, i, r -> i == -1 && r.getOrThrow() == StatusEnum.READY.code },
+            { _, i, r -> i == 1 && r.getOrThrow() == StatusEnum.ERROR.code },
+        )
+    }
+}