Skip to content

Commit

Permalink
updated approximations
Browse files Browse the repository at this point in the history
  • Loading branch information
@MchKosticyn
MchKosticyn committed Aug 7, 2024
1 parent c81dc1f commit b4ff5e6
Show file tree
Hide file tree
Showing 2 changed files with 102 additions and 25 deletions.
5 changes: 5 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,11 @@ fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefWithSameTy
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
mockSymbolicRef { objectTypeEquals(it, representative) }

fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefWithSameType(
representative: UHeapRef
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
mockSymbolicRef { ctx.mkOr(objectTypeEquals(it, representative), ctx.mkEq(it, ctx.nullRef)) }

fun <Method> UState<*, Method, *, *, *, *>.makeSymbolicRefUntyped(): UHeapRef =
memory.mocker.createMockSymbol(trackedLiteral = null, ctx.addressSort)

Expand Down
122 changes: 97 additions & 25 deletions usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -110,66 +117,80 @@ 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
}

return approximateEmptyNativeMethod(methodCall)
}

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)
}

Expand All @@ -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
Expand Down Expand Up @@ -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<USort>
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") {
Expand Down Expand Up @@ -602,13 +660,27 @@ 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 {
memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
}
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)
Expand Down

0 comments on commit b4ff5e6

Please sign in to comment.