UnitTestBot · Saloed · Feb 22, 2024 · Feb 21, 2024
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt
@@ -43,7 +43,7 @@ class JcCheckerRunner(val cp: JcClasspath) {
     ) {
         val checkersObserver = JcCheckerObserver(checkersVisitor, apiImpl)
 
-        JcMachine(cp, options, checkersObserver).use { machine ->
+        JcMachine(cp, options, interpreterObserver = checkersObserver).use { machine ->
             machine.analyze(entryPoint, targets)
         }
     }

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
@@ -43,6 +43,7 @@ val logger = object : KLogging() {}.logger
 class JcMachine(
     cp: JcClasspath,
     private val options: UMachineOptions,
+    private val jcMachineOptions: JcMachineOptions = JcMachineOptions(),
     private val interpreterObserver: JcInterpreterObserver? = null,
 ) : UMachine<JcState>() {
     private val applicationGraph = JcApplicationGraph(cp)
@@ -51,7 +52,7 @@ class JcMachine(
     private val components = JcComponents(typeSystem, options)
     private val ctx = JcContext(cp, components)
 
-    private val interpreter = JcInterpreter(ctx, applicationGraph, interpreterObserver)
+    private val interpreter = JcInterpreter(ctx, applicationGraph, jcMachineOptions, interpreterObserver)
 
     private val cfgStatistics = CfgStatisticsImpl(applicationGraph)
 

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt
@@ -0,0 +1,22 @@
+package org.usvm.machine
+
+/**
+ * JcMachine specific options.
+ * */
+data class JcMachineOptions(
+    /**
+     * During virtual call resolution the machine should consider all possible call implementations.
+     * By default, the machine forks on few concrete implementation and ignore remaining.
+     * */
+    val forkOnRemainingTypes: Boolean = false,
+
+    /**
+     * Controls, whether the machine should analyze states with implicit exceptions (e.g. NPE).
+     * */
+    val forkOnImplicitExceptions: Boolean = true,
+
+    /**
+     * Hard constraint for maximal array size.
+     * */
+    val arrayMaxSize: Int = 1_500,
+)
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
@@ -99,6 +99,7 @@ import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.isTrue
 import org.usvm.machine.JcContext
+import org.usvm.machine.JcMachineOptions
 import org.usvm.machine.USizeSort
 import org.usvm.machine.operator.JcBinaryOperator
 import org.usvm.machine.operator.JcUnaryOperator
@@ -128,11 +129,11 @@ import org.usvm.utils.logAssertFailure
 class JcExprResolver(
     private val ctx: JcContext,
     private val scope: JcStepScope,
+    private val options: JcMachineOptions,
     localToIdx: (JcMethod, JcLocal) -> Int,
     mkTypeRef: (JcType) -> UConcreteHeapRef,
     mkStringConstRef: (String) -> UConcreteHeapRef,
     private val classInitializerAnalysisAlwaysRequiredForType: (JcRefType) -> Boolean,
-    private val hardMaxArrayLength: Int = 1_500, // TODO: move to options
 ) : JcExprVisitor<UExpr<out USort>?> {
     val simpleValueResolver: JcSimpleValueResolver = JcSimpleValueResolver(
         ctx,
@@ -768,21 +769,29 @@ class JcExprResolver(
     fun checkArrayIndex(idx: UExpr<USizeSort>, length: UExpr<USizeSort>) = with(ctx) {
         val inside = (mkBvSignedLessOrEqualExpr(mkBv(0), idx)) and (mkBvSignedLessExpr(idx, length))
 
-        scope.fork(
-            inside,
-            blockOnFalseState = allocateException(arrayIndexOutOfBoundsExceptionType)
-        )
+        if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                inside,
+                blockOnFalseState = allocateException(arrayIndexOutOfBoundsExceptionType)
+            )
+        } else {
+            scope.assert(inside).logAssertFailure { "Jc implicit exception: Check index out of bound" }
+        }
     }
 
     fun checkNewArrayLength(length: UExpr<USizeSort>) = with(ctx) {
         assertHardMaxArrayLength(length) ?: return null
 
         val lengthIsNonNegative = mkBvSignedLessOrEqualExpr(mkBv(0), length)
 
-        scope.fork(
-            lengthIsNonNegative,
-            blockOnFalseState = allocateException(negativeArraySizeExceptionType)
-        )
+        if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                lengthIsNonNegative,
+                blockOnFalseState = allocateException(negativeArraySizeExceptionType)
+            )
+        } else {
+            scope.assert(lengthIsNonNegative).logAssertFailure { "Jc implicit exception: Check new array length" }
+        }
     }
 
     fun checkDivisionByZero(expr: UExpr<out USort>) = with(ctx) {
@@ -791,26 +800,47 @@ class JcExprResolver(
             return Unit
         }
         val neqZero = mkEq(expr.cast(), mkBv(0, sort)).not()
-        scope.fork(
-            neqZero,
-            blockOnFalseState = allocateException(arithmeticExceptionType)
-        )
+        if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                neqZero,
+                blockOnFalseState = allocateException(arithmeticExceptionType)
+            )
+        } else {
+            scope.assert(neqZero).logAssertFailure { "Jc implicit exception: Check division by zero" }
+        }
     }
 
     fun checkNullPointer(ref: UHeapRef) = with(ctx) {
         val neqNull = mkHeapRefEq(ref, nullRef).not()
-        scope.fork(
-            neqNull,
-            blockOnFalseState = allocateException(nullPointerExceptionType)
-        )
+        if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                neqNull,
+                blockOnFalseState = allocateException(nullPointerExceptionType)
+            )
+        } else {
+            scope.assert(neqNull).logAssertFailure { "Jc implicit exception: Check NPE" }
+        }
+    }
+
+    fun checkClassCast(expr: UHeapRef, type: JcType) = with(ctx) {
+        val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr, type) }
+
+        if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                isExpr,
+                blockOnFalseState = allocateException(ctx.classCastExceptionType)
+            )
+        } else {
+            scope.assert(isExpr).logAssertFailure { "Jc implicit exception: Check class cast" }
+        }
     }
 
     // endregion
 
     // region hard assertions
 
     private fun assertHardMaxArrayLength(length: UExpr<USizeSort>): Unit? = with(ctx) {
-        val lengthLeThanMaxLength = mkBvSignedLessOrEqualExpr(length, mkBv(hardMaxArrayLength))
+        val lengthLeThanMaxLength = mkBvSignedLessOrEqualExpr(length, mkBv(options.arrayMaxSize))
         scope.assert(lengthLeThanMaxLength)
             .logAssertFailure { "JcExprResolver: array length max" }
     }
@@ -881,17 +911,11 @@ class JcExprResolver(
             "Unexpected type variable $type"
         }
 
-        return if (!ctx.typeSystem<JcType>().isSupertype(type, typeBefore)) {
-            val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr, type) }
-
-            scope.fork(
-                isExpr,
-                blockOnFalseState = allocateException(ctx.classCastExceptionType)
-            ) ?: return null
-            expr
-        } else {
-            expr
+        if (!ctx.typeSystem<JcType>().isSupertype(type, typeBefore)) {
+            checkClassCast(expr, type) ?: return null
         }
+
+        return expr
     }
 
     private fun resolvePrimitiveCast(

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
@@ -53,6 +53,7 @@ import org.usvm.machine.JcConcreteMethodCallInst
 import org.usvm.machine.JcContext
 import org.usvm.machine.JcDynamicMethodCallInst
 import org.usvm.machine.JcInterpreterObserver
+import org.usvm.machine.JcMachineOptions
 import org.usvm.machine.JcMethodApproximationResolver
 import org.usvm.machine.JcMethodCall
 import org.usvm.machine.JcMethodCallBaseInst
@@ -78,6 +79,7 @@ import org.usvm.types.singleOrNull
 import org.usvm.util.name
 import org.usvm.util.outerClassInstanceField
 import org.usvm.util.write
+import org.usvm.utils.logAssertFailure
 import org.usvm.utils.onStateDeath
 
 typealias JcStepScope = StepScope<JcState, JcType, JcInst, JcContext>
@@ -88,6 +90,7 @@ typealias JcStepScope = StepScope<JcState, JcType, JcInst, JcContext>
 class JcInterpreter(
     private val ctx: JcContext,
     private val applicationGraph: JcApplicationGraph,
+    private val options: JcMachineOptions,
     private val observer: JcInterpreterObserver? = null,
     var forkBlackList: UForkBlackList<JcState, JcInst> = UForkBlackList.createDefault(),
 ) : UInterpreter<JcState>() {
@@ -303,7 +306,7 @@ class JcInterpreter(
                     return
                 }
 
-                resolveVirtualInvoke(stmt, scope, forkOnRemainingTypes = false)
+                resolveVirtualInvoke(stmt, scope)
             }
 
             is JcDynamicMethodCallInst -> {
@@ -399,32 +402,29 @@ class JcInterpreter(
         val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return
         val expr = exprResolver.resolveJcExpr(stmt.rhv, stmt.lhv.type) ?: return
 
-        val noArrayStoreException = checkArrayStoreException(lvalue, expr, scope)
+        checkArrayStoreException(lvalue, expr, exprResolver, scope) ?: return
 
-        scope.fork(
-            noArrayStoreException,
-            blockOnTrueState = {
-                val nextStmt = stmt.nextStmt
-                memory.write(lvalue, expr)
-                newStmt(nextStmt)
-            },
-            blockOnFalseState = exprResolver.allocateException(ctx.arrayStoreExceptionType)
-        )
+        scope.doWithState {
+            val nextStmt = stmt.nextStmt
+            memory.write(lvalue, expr)
+            newStmt(nextStmt)
+        }
     }
 
     // Returns `trueExpr` if ArrayStoreException is impossible
     private fun checkArrayStoreException(
         lvalue: ULValue<*, *>,
         rvalue: UExpr<out USort>,
+        exprResolver: JcExprResolver,
         scope: JcStepScope
-    ): UBoolExpr {
+    ): Unit? {
         if (lvalue !is UArrayIndexLValue<*, *, *>) {
-            return ctx.trueExpr
+            return Unit
         }
 
         // ArrayStoreException is possible only for references
         if (rvalue.sort != ctx.addressSort) {
-            return ctx.trueExpr
+            return Unit
         }
 
         check(lvalue.sort == rvalue.sort) {
@@ -462,7 +462,15 @@ class JcInterpreter(
             ctx.mkAnd(elementTypeConstraints, arrayTypeConstraints)
         }
 
-        return isRvalueSubtypeOf
+        return if (options.forkOnImplicitExceptions) {
+            scope.fork(
+                isRvalueSubtypeOf,
+                blockOnFalseState = exprResolver.allocateException(ctx.arrayStoreExceptionType)
+            )
+        } else {
+            scope.assert(isRvalueSubtypeOf)
+                .logAssertFailure { "Jc implicit exception: Check ArrayStoreException" }
+        }
     }
 
     private fun visitIfStmt(scope: JcStepScope, stmt: JcIfInst) {
@@ -624,6 +632,7 @@ class JcInterpreter(
         JcExprResolver(
             ctx,
             scope,
+            options,
             ::mapLocalToIdxMapper,
             ::typeInstanceAllocator,
             ::stringConstantAllocator,
@@ -697,8 +706,7 @@ class JcInterpreter(
     private fun resolveVirtualInvoke(
         methodCall: JcVirtualMethodCallInst,
         scope: JcStepScope,
-        forkOnRemainingTypes: Boolean,
-    ): Unit = resolveVirtualInvoke(ctx, methodCall, scope, typeSelector, forkOnRemainingTypes)
+    ): Unit = resolveVirtualInvoke(ctx, methodCall, scope, typeSelector, options.forkOnRemainingTypes)
 
     private val approximationResolver = JcMethodApproximationResolver(ctx, applicationGraph)
 

diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
@@ -780,7 +780,7 @@ open class JavaMethodTestRunner : TestRunner<JcTest, KFunction<*>, KClass<*>?, J
     override val runner: (KFunction<*>, UMachineOptions) -> List<JcTest> = { method, options ->
         val jcMethod = cp.getJcMethodByName(method)
 
-        JcMachine(cp, options, interpreterObserver).use { machine ->
+        JcMachine(cp, options, interpreterObserver = interpreterObserver).use { machine ->
             val states = machine.analyze(jcMethod.method, targets)
             states.map { testResolver.resolve(jcMethod, it, machine.stringConstants) }
         }