From b4ff5e659941d81cb9a46a4f2458dea87a849c12 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Wed, 7 Aug 2024 17:07:35 +0300 Subject: [PATCH] updated approximations --- .../src/main/kotlin/org/usvm/api/MockApi.kt | 5 + .../org/usvm/machine/JcApproximations.kt | 122 ++++++++++++++---- 2 files changed, 102 insertions(+), 25 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt index 790fdba5dc..33e1f2de20 100644 --- a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt @@ -28,6 +28,11 @@ fun StepScope.makeSymbolicRefWithSameTy ): UHeapRef? where State : UState = mockSymbolicRef { objectTypeEquals(it, representative) } +fun StepScope.makeNullableSymbolicRefWithSameType( + representative: UHeapRef +): UHeapRef? where State : UState = + mockSymbolicRef { ctx.mkOr(objectTypeEquals(it, representative), ctx.mkEq(it, ctx.nullRef)) } + fun UState<*, Method, *, *, *, *>.makeSymbolicRefUntyped(): UHeapRef = memory.mocker.createMockSymbol(trackedLiteral = null, ctx.addressSort) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt index 71f834b32b..f8f351b081 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt @@ -3,13 +3,16 @@ package org.usvm.machine import io.ksmt.utils.asExpr import io.ksmt.utils.uncheckedCast import org.jacodb.api.jvm.JcArrayType +import org.jacodb.api.jvm.JcClassType import org.jacodb.api.jvm.JcMethod +import org.jacodb.api.jvm.JcPrimitiveType import org.jacodb.api.jvm.JcType import org.jacodb.api.jvm.ext.boolean import org.jacodb.api.jvm.ext.byte import org.jacodb.api.jvm.ext.char import org.jacodb.api.jvm.ext.double import org.jacodb.api.jvm.ext.findClassOrNull +import org.jacodb.api.jvm.ext.findTypeOrNull import org.jacodb.api.jvm.ext.float import org.jacodb.api.jvm.ext.ifArrayGetElementType import org.jacodb.api.jvm.ext.int @@ -18,6 +21,7 @@ import org.jacodb.api.jvm.ext.objectClass import org.jacodb.api.jvm.ext.objectType import org.jacodb.api.jvm.ext.short import org.jacodb.api.jvm.ext.toType +import org.jacodb.api.jvm.ext.unboxIfNeeded import org.jacodb.api.jvm.ext.void import org.usvm.UBoolExpr import org.usvm.UBv32Sort @@ -70,6 +74,9 @@ import kotlin.reflect.KFunction0 import kotlin.reflect.KFunction1 import kotlin.reflect.KFunction2 import kotlin.reflect.jvm.javaMethod +import org.usvm.USort +import org.usvm.api.makeNullableSymbolicRefWithSameType +import org.usvm.api.writeField class JcMethodApproximationResolver( private val ctx: JcContext, @@ -110,34 +117,37 @@ class JcMethodApproximationResolver( } private fun approximateRegularMethod(methodCall: JcMethodCall): Boolean = with(methodCall) { - if (method.enclosingClass == usvmApiSymbolicList) { + val enclosingClass = method.enclosingClass + val className = enclosingClass.name + + if (enclosingClass == usvmApiSymbolicList) { approximateUsvmSymbolicListMethod(methodCall) return true } - if (method.enclosingClass == usvmApiSymbolicMap) { + if (enclosingClass == usvmApiSymbolicMap) { approximateUsvmSymbolicMapMethod(methodCall) return true } - if (method.enclosingClass == usvmApiSymbolicIdentityMap) { + if (enclosingClass == usvmApiSymbolicIdentityMap) { approximateUsvmSymbolicIdMapMethod(methodCall) return true } - if (method.enclosingClass == ctx.cp.objectClass) { + if (enclosingClass == ctx.cp.objectClass) { if (approximateObjectVirtualMethod(methodCall)) return true } - if (method.enclosingClass == ctx.classType.jcClass) { + if (enclosingClass == ctx.classType.jcClass) { if (approximateClassVirtualMethod(methodCall)) return true } - if (method.enclosingClass.name == "jdk.internal.misc.Unsafe") { + if (className == "jdk.internal.misc.Unsafe") { if (approximateUnsafeVirtualMethod(methodCall)) return true } - if (method.name == "clone" && method.enclosingClass == ctx.cp.objectClass) { + if (method.name == "clone" && enclosingClass == ctx.cp.objectClass) { if (approximateArrayClone(methodCall)) return true } @@ -145,31 +155,42 @@ class JcMethodApproximationResolver( } private fun approximateStaticMethod(methodCall: JcMethodCall): Boolean = with(methodCall) { - if (method.enclosingClass == usvmApiEngine) { + val enclosingClass = method.enclosingClass + val className = enclosingClass.name + if (enclosingClass == usvmApiEngine) { approximateUsvmApiEngineStaticMethod(methodCall) return true } - if (method.enclosingClass == ctx.classType.jcClass) { + if (enclosingClass == ctx.classType.jcClass) { if (approximateClassStaticMethod(methodCall)) return true } - if (method.enclosingClass.name == "java.lang.System") { + if (className == "generated.java.lang.PrimitiveTypeUtils") { + if (approximatePrimitiveTypeUtilsStaticMethod(methodCall)) return true + } + + if (className == "java.lang.System") { if (approximateSystemStaticMethod(methodCall)) return true } - if (method.enclosingClass.name == "java.lang.StringUTF16") { + if (className == "java.lang.StringUTF16") { if (approximateStringUtf16StaticMethod(methodCall)) return true } - if (method.enclosingClass.name == "java.lang.Float") { + if (className == "java.lang.Float") { if (approximateFloatStaticMethod(methodCall)) return true } - if (method.enclosingClass.name == "java.lang.Double") { + if (className == "java.lang.Double") { if (approximateDoubleStaticMethod(methodCall)) return true } + val type = enclosingClass.toType() + if (type.unboxIfNeeded() is JcPrimitiveType) { + if (approximateBoxedPrimitiveTypeStaticMethod(methodCall, type)) return true + } + return approximateEmptyNativeMethod(methodCall) } @@ -190,25 +211,41 @@ class JcMethodApproximationResolver( return false } + private fun approximateGetPrimitiveClass(methodCall: JcMethodCall): Boolean = with(methodCall) { + val classNameRef = arguments.single() + + val predefinedTypeNames = ctx.primitiveTypes.associateBy { + exprResolver.simpleValueResolver.resolveStringConstant(it.typeName) + } + + val primitive = predefinedTypeNames[classNameRef] ?: return false + + val classRef = exprResolver.simpleValueResolver.resolveClassRef(primitive) + + scope.doWithState { + skipMethodInvocationWithValue(methodCall, classRef) + } + + return true + } + private fun approximateClassStaticMethod(methodCall: JcMethodCall): Boolean = with(methodCall) { /** * Approximate retrieval of class instance for primitives. * */ if (method.name == "getPrimitiveClass") { - val classNameRef = arguments.single() - - val predefinedTypeNames = ctx.primitiveTypes.associateBy { - exprResolver.simpleValueResolver.resolveStringConstant(it.typeName) - } - - val primitive = predefinedTypeNames[classNameRef] ?: return false + return approximateGetPrimitiveClass(methodCall) + } - val classRef = exprResolver.simpleValueResolver.resolveClassRef(primitive) + return false + } - scope.doWithState { - skipMethodInvocationWithValue(methodCall, classRef) - } - return true + private fun approximatePrimitiveTypeUtilsStaticMethod(methodCall: JcMethodCall): Boolean = with(methodCall) { + /** + * Approximate retrieval of class instance for primitives. + * */ + if (method.name == "getPrimitiveClass") { + return approximateGetPrimitiveClass(methodCall) } return false @@ -249,6 +286,27 @@ class JcMethodApproximationResolver( return false } + @Suppress("UNCHECKED_CAST") + private fun approximateBoxedPrimitiveTypeStaticMethod(methodCall: JcMethodCall, boxedType: JcClassType): Boolean = with(methodCall) { + val parameters = method.parameters + val unboxedType = boxedType.unboxIfNeeded() as JcPrimitiveType + val name = method.name + if (name == "valueOf" && parameters.count() == 1 && parameters.single().type.let { ctx.cp.findTypeOrNull(it) == unboxedType }) { + scope.doWithState { + val boxRef = memory.allocConcrete(boxedType) + val valueField = boxedType.declaredFields.find { it.name == "value" }!! + val sort = ctx.typeToSort(unboxedType) + val value = arguments.single() as UExpr + memory.writeField(boxRef, valueField.field, sort, value, ctx.trueExpr) + skipMethodInvocationWithValue(methodCall, boxRef) + } + + return true + } + + return false + } + private fun approximateUnsafeVirtualMethod(methodCall: JcMethodCall): Boolean = with(methodCall) { // Array offset is usually the same on various JVM if (method.name == "arrayBaseOffset0") { @@ -602,6 +660,13 @@ class JcMethodApproximationResolver( val (ref0, ref1) = it.arguments.map { it.asExpr(ctx.addressSort) } scope.calcOnState { objectTypeEquals(ref0, ref1) } } + dispatchUsvmApiMethod(Engine::typeIs) { + val (ref, classRef) = it.arguments.map { it.asExpr(ctx.addressSort) } + val classRefTypeRepresentative = scope.calcOnState { + memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField)) + } + scope.calcOnState { objectTypeEquals(ref, classRefTypeRepresentative) } + } dispatchMkRef(Engine::makeSymbolic) { val classRef = it.arguments.single().asExpr(ctx.addressSort) val classRefTypeRepresentative = scope.calcOnState { @@ -609,6 +674,13 @@ class JcMethodApproximationResolver( } scope.makeSymbolicRefWithSameType(classRefTypeRepresentative) } + dispatchMkRef(Engine::makeNullableSymbolic) { + val classRef = it.arguments.single().asExpr(ctx.addressSort) + val classRefTypeRepresentative = scope.calcOnState { + memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField)) + } + scope.makeNullableSymbolicRefWithSameType(classRefTypeRepresentative) + } dispatchMkRef2(Engine::makeSymbolicArray) { val (elementClassRefExpr, sizeExpr) = it.arguments val elementClassRef = elementClassRefExpr.asExpr(ctx.addressSort)