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 981ae31
Show file tree
Hide file tree
Showing 2 changed files with 138 additions and 60 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
193 changes: 133 additions & 60 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 @@ -2,34 +2,8 @@ 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.JcMethod
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.float
import org.jacodb.api.jvm.ext.ifArrayGetElementType
import org.jacodb.api.jvm.ext.int
import org.jacodb.api.jvm.ext.long
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.void
import org.usvm.UBoolExpr
import org.usvm.UBv32Sort
import org.usvm.UBvSort
import org.usvm.UConcreteHeapRef
import org.usvm.UExpr
import org.usvm.UFpSort
import org.usvm.UHeapRef
import org.usvm.api.Engine
import org.usvm.api.SymbolicIdentityMap
import org.usvm.api.SymbolicList
import org.usvm.api.SymbolicMap
import org.jacodb.api.jvm.*
import org.jacodb.api.jvm.cfg.*
import org.usvm.api.collection.ListCollectionApi.ensureListSizeCorrect
import org.usvm.api.collection.ListCollectionApi.mkSymbolicList
import org.usvm.api.collection.ListCollectionApi.symbolicListCopyRange
Expand All @@ -47,20 +21,13 @@ import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapMergeInto
import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapPut
import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapRemove
import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize
import org.usvm.api.makeSymbolicPrimitive
import org.usvm.api.makeSymbolicRef
import org.usvm.api.makeSymbolicRefWithSameType
import org.usvm.api.mapTypeStream
import org.usvm.api.memcpy
import org.usvm.api.objectTypeEquals
import org.usvm.collection.array.length.UArrayLengthLValue
import org.usvm.collection.field.UFieldLValue
import org.usvm.machine.interpreter.JcExprResolver
import org.usvm.machine.interpreter.JcStepScope
import org.usvm.machine.mocks.mockMethod
import org.usvm.machine.state.JcState
import org.usvm.machine.state.skipMethodInvocationWithValue
import org.usvm.sizeSort
import org.usvm.types.first
import org.usvm.types.singleOrNull
import org.usvm.util.allocHeapRef
Expand All @@ -70,6 +37,14 @@ import kotlin.reflect.KFunction0
import kotlin.reflect.KFunction1
import kotlin.reflect.KFunction2
import kotlin.reflect.jvm.javaMethod
import org.jacodb.api.jvm.ext.*
import org.jacodb.impl.features.classpaths.JcUnknownClass
import org.usvm.*
import org.usvm.api.*
import org.usvm.api.util.Reflection.toJavaClass
import org.usvm.machine.state.newStmt
import java.util.*
import kotlin.collections.ArrayList

class JcMethodApproximationResolver(
private val ctx: JcContext,
Expand Down Expand Up @@ -110,66 +85,84 @@ 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
}

if (className == "org.apache.commons.logging.Log") {
if (approximateLoggerMethod(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 +183,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 +258,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 @@ -312,6 +342,35 @@ class JcMethodApproximationResolver(
return false
}

private val loggerLevelCheckMethods = setOf(
"isFatalEnabled", "isErrorEnabled", "isWarnEnabled", "isInfoEnabled", "isDebugEnabled", "isTraceEnabled"
)

private val loggerPrintMethods = setOf(
"fatal", "error", "warn", "info", "debug", "trace"
)

private fun approximateLoggerMethod(methodCall: JcMethodCall): Boolean = with(methodCall) {
val methodName = method.name
if (loggerLevelCheckMethods.contains(methodName)) {
scope.doWithState {
skipMethodInvocationWithValue(methodCall, ctx.falseExpr)
}

return true
}

if (loggerPrintMethods.contains(methodName)) {
scope.doWithState {
skipMethodInvocationWithValue(methodCall, ctx.voidValue)
}

return true
}

return false
}

private fun JcExprResolver.resolveArrayCopy(
methodCall: JcMethodCall,
srcRef: UHeapRef,
Expand Down Expand Up @@ -602,13 +661,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 981ae31

Please sign in to comment.