From 191b5c012282e2dbf015398510134dbdcb459091 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Wed, 21 Feb 2024 13:33:01 +0300 Subject: [PATCH] JcMachineOptions and implicit exceptions --- .../kotlin/org/usvm/api/checkers/JcChecker.kt | 2 +- .../main/kotlin/org/usvm/machine/JcMachine.kt | 3 +- .../org/usvm/machine/JcMachineOptions.kt | 22 +++++ .../machine/interpreter/JcExprResolver.kt | 80 ++++++++++++------- .../usvm/machine/interpreter/JcInterpreter.kt | 42 ++++++---- .../org/usvm/samples/JavaMethodTestRunner.kt | 2 +- 6 files changed, 103 insertions(+), 48 deletions(-) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt 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 index 29226cfac7..7acd4920d5 100644 --- 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 index 9b7d89211b..c5f128ffd3 100644 --- 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() { 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 new file mode 100644 index 0000000000..623503d786 --- /dev/null +++ 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 index 985313ebdd..307565a7ef 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 @@ -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?> { val simpleValueResolver: JcSimpleValueResolver = JcSimpleValueResolver( ctx, @@ -768,10 +769,14 @@ class JcExprResolver( fun checkArrayIndex(idx: UExpr, length: UExpr) = 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) = with(ctx) { @@ -779,10 +784,14 @@ class JcExprResolver( 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) = with(ctx) { @@ -791,18 +800,39 @@ 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 @@ -810,7 +840,7 @@ class JcExprResolver( // region hard assertions private fun assertHardMaxArrayLength(length: UExpr): 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().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().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 index 7cb7574d82..45f8c372cf 100644 --- 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 @@ -88,6 +90,7 @@ typealias JcStepScope = StepScope class JcInterpreter( private val ctx: JcContext, private val applicationGraph: JcApplicationGraph, + private val options: JcMachineOptions, private val observer: JcInterpreterObserver? = null, var forkBlackList: UForkBlackList = UForkBlackList.createDefault(), ) : UInterpreter() { @@ -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, + 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 index be8bd13d69..adee1187c9 100644 --- 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, KClass<*>?, J override val runner: (KFunction<*>, UMachineOptions) -> List = { 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) } }