From 827fcc0e1ede13d68e236ad51ad337155c2614fa Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Mon, 30 Oct 2023 20:29:39 +0300 Subject: [PATCH] Support lambda expressions --- buildSrc/src/main/kotlin/Versions.kt | 2 +- .../main/kotlin/org/usvm/machine/JcContext.kt | 3 + .../org/usvm/machine/JcMethodCallInst.kt | 16 ++++ .../usvm/machine/JcVirtualInvokeResolver.kt | 87 ++++++++++++++++--- .../machine/interpreter/JcCallSiteRegion.kt | 49 +++++++++++ .../machine/interpreter/JcExprResolver.kt | 34 +++++--- .../usvm/machine/interpreter/JcInterpreter.kt | 28 ++++-- .../org/usvm/machine/state/JcStateUtils.kt | 7 +- .../samples/lambda/InvokeDynamicExamples.java | 81 +++++++++++++++++ .../lambda/InvokeDynamicExamplesTest.kt | 61 +++++++++++++ .../samples/wrappers/BooleanWrapperTest.kt | 7 +- 11 files changed, 338 insertions(+), 37 deletions(-) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/lambda/InvokeDynamicExamples.java create mode 100644 usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/InvokeDynamicExamplesTest.kt diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt index 0a2f551ebd..4b6919648b 100644 --- a/buildSrc/src/main/kotlin/Versions.kt +++ b/buildSrc/src/main/kotlin/Versions.kt @@ -4,7 +4,7 @@ object Versions { const val ksmt = "0.5.7" const val collections = "0.3.5" const val coroutines = "1.6.4" - const val jcdb = "1.3.0" + const val jcdb = "1.4.0" const val mockk = "1.13.4" const val junitParams = "5.9.3" const val logback = "1.4.8" diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt index 94eabd9744..1ad83a30d1 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt @@ -23,6 +23,7 @@ import org.jacodb.impl.bytecode.JcFieldImpl import org.jacodb.impl.types.FieldInfo import org.usvm.UBv32Sort import org.usvm.UContext +import org.usvm.machine.interpreter.JcLambdaCallSiteRegionId import org.usvm.util.extractJcRefType internal typealias USizeSort = UBv32Sort @@ -60,6 +61,8 @@ class JcContext( ?: error("No enum type in classpath") } + val lambdaCallSiteRegionId by lazy { JcLambdaCallSiteRegionId(this) } + // TODO store it in JcComponents? Make it mutable? internal val useNegativeAddressesInStaticInitializer: Boolean = false diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt index c905a17a61..d6f25f0ca2 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt @@ -2,6 +2,7 @@ package org.usvm.machine import org.jacodb.api.JcMethod import org.jacodb.api.JcRefType +import org.jacodb.api.cfg.JcDynamicCallExpr import org.jacodb.api.cfg.JcExpr import org.jacodb.api.cfg.JcInst import org.jacodb.api.cfg.JcInstLocation @@ -86,3 +87,18 @@ data class JcVirtualMethodCallInst( override val originalInst: JcInst = returnSite } + +/** + * Invoke dynamic instruction. + * The [dynamicCall] can't be processed and the machine + * must resolve it to some [JcConcreteMethodCallInst] or approximate. + * */ +data class JcDynamicMethodCallInst( + val dynamicCall: JcDynamicCallExpr, + override val arguments: List>, + override val returnSite: JcInst, +) : JcMethodCallBaseInst, JcMethodCall { + override val location: JcInstLocation = returnSite.location + override val method: JcMethod = dynamicCall.method.method + override val originalInst: JcInst = returnSite +} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcVirtualInvokeResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcVirtualInvokeResolver.kt index 998cc3c351..cee150523d 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcVirtualInvokeResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcVirtualInvokeResolver.kt @@ -1,10 +1,8 @@ package org.usvm.machine -import io.ksmt.expr.KExpr import io.ksmt.utils.asExpr import org.jacodb.api.JcType import org.jacodb.api.ext.toType -import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UHeapRef @@ -13,14 +11,16 @@ import org.usvm.api.evalTypeEquals import org.usvm.api.typeStreamOf import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isStaticHeapRef +import org.usvm.machine.interpreter.JcLambdaCallSite +import org.usvm.machine.interpreter.JcLambdaCallSiteMemoryRegion import org.usvm.machine.interpreter.JcStepScope import org.usvm.machine.interpreter.JcTypeSelector import org.usvm.machine.state.JcState import org.usvm.machine.state.newStmt -import org.usvm.memory.foldHeapRefWithStaticAsSymbolic +import org.usvm.memory.foldHeapRef import org.usvm.model.UModelBase import org.usvm.types.UTypeStream -import org.usvm.types.first +import org.usvm.types.single import org.usvm.util.findMethod /** @@ -68,7 +68,13 @@ private fun resolveVirtualInvokeWithModel( val concreteRef = model.eval(instance) as UConcreteHeapRef if (isAllocatedConcreteHeapRef(concreteRef) || isStaticHeapRef(concreteRef)) { - val concreteCall = makeConcreteMethodCall(scope, concreteRef, methodCall) + val callSite = findLambdaCallSite(methodCall, scope, concreteRef) + val concreteCall = if (callSite != null) { + makeLambdaCallSiteCall(callSite) + } else { + makeConcreteMethodCall(scope, concreteRef, methodCall) + } + scope.doWithState { newStmt(concreteCall) } @@ -76,6 +82,7 @@ private fun resolveVirtualInvokeWithModel( return@with } + // Resolved lambda call site can't be an input ref val typeStream = model.typeStreamOf(concreteRef) val typeConstraintsWithBlockOnStates = makeConcreteCallsForPossibleTypes( scope, @@ -100,17 +107,36 @@ private fun resolveVirtualInvokeWithoutModel( val instance = arguments.first().asExpr(ctx.addressSort) val refsWithConditions = mutableListOf>() - foldHeapRefWithStaticAsSymbolic( + val lambdaCallSitesWithConditions = mutableListOf>() + foldHeapRef( instance, - refsWithConditions, + Unit, initialGuard = ctx.trueExpr, ignoreNullRefs = true, collapseHeapRefs = false, - blockOnConcrete = { curRefsWithConditions, (ref, condition) -> curRefsWithConditions.also { it += ref to condition } }, - blockOnSymbolic = { curRefsWithConditions, (ref, condition) -> curRefsWithConditions.also { it += ref to condition } }, + blockOnConcrete = { _, (ref, condition) -> + val lambdaCallSite = findLambdaCallSite(methodCall, scope, ref) + if (lambdaCallSite != null) { + lambdaCallSitesWithConditions += lambdaCallSite to condition + } else { + refsWithConditions += ref to condition + } + }, + blockOnStatic = { _, (ref, condition) -> + val lambdaCallSite = findLambdaCallSite(methodCall, scope, ref) + if (lambdaCallSite != null) { + lambdaCallSitesWithConditions += lambdaCallSite to condition + } else { + refsWithConditions += ref to condition + } + }, + blockOnSymbolic = { _, (ref, condition) -> + // Resolved lambda call site can't be a symbolic ref + refsWithConditions.also { it += ref to condition } + }, ) - val conditionsWithBlocks = refsWithConditions.flatMap { (ref, condition) -> + val conditionsWithBlocks = refsWithConditions.flatMapTo(mutableListOf()) { (ref, condition) -> when { isAllocatedConcreteHeapRef(ref) || isStaticHeapRef(ref) -> { val concreteCall = makeConcreteMethodCall(scope, ref, methodCall) @@ -140,6 +166,11 @@ private fun resolveVirtualInvokeWithoutModel( } } + lambdaCallSitesWithConditions.mapTo(conditionsWithBlocks) { (callSite, condition) -> + val concreteCall = makeLambdaCallSiteCall(callSite) + condition to { state: JcState -> state.newStmt(concreteCall) } + } + scope.forkMulti(conditionsWithBlocks) } @@ -149,7 +180,7 @@ private fun JcVirtualMethodCallInst.makeConcreteMethodCall( methodCall: JcVirtualMethodCallInst, ): JcConcreteMethodCallInst { // We have only one type for allocated and static heap refs - val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.first() + val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.single() val concreteMethod = type.findMethod(method) ?: error("Can't find method $method in type ${type.typeName}") @@ -162,7 +193,7 @@ private fun JcVirtualMethodCallInst.makeConcreteCallsForPossibleTypes( methodCall: JcVirtualMethodCallInst, typeStream: UTypeStream, typeSelector: JcTypeSelector, - instance: KExpr, + instance: UHeapRef, ctx: JcContext, condition: UBoolExpr, forkOnRemainingTypes: Boolean, @@ -196,3 +227,35 @@ private fun JcVirtualMethodCallInst.makeConcreteCallsForPossibleTypes( return typeConstraintsWithBlockOnStates } + +private fun findLambdaCallSite( + methodCall: JcVirtualMethodCallInst, + scope: JcStepScope, + ref: UConcreteHeapRef, +): JcLambdaCallSite? = with(methodCall) { + val callSites = scope.calcOnState { memory.getRegion(ctx.lambdaCallSiteRegionId) as JcLambdaCallSiteMemoryRegion } + val callSite = callSites.findCallSite(ref) ?: return null + + val lambdaMethodType = callSite.lambda.dynamicMethodType + + // Match function signature + when { + method.name != callSite.lambda.callSiteMethodName -> return null + method.returnType != lambdaMethodType.returnType -> return null + lambdaMethodType.argumentTypes != method.parameters.map { it.type } -> return null + } + + return callSite +} + +private fun JcVirtualMethodCallInst.makeLambdaCallSiteCall( + callSite: JcLambdaCallSite, +): JcConcreteMethodCallInst { + val lambdaMethod = callSite.lambda.actualMethod.method + + // Instance was already resolved to the call site + val callArgsWithoutInstance = this.arguments.drop(1) + val lambdaMethodArgs = callSite.callSiteArgs + callArgsWithoutInstance + + return JcConcreteMethodCallInst(location, lambdaMethod.method, lambdaMethodArgs, returnSite) +} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt new file mode 100644 index 0000000000..6c991a1752 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt @@ -0,0 +1,49 @@ +package org.usvm.machine.interpreter + +import kotlinx.collections.immutable.PersistentMap +import kotlinx.collections.immutable.persistentHashMapOf +import org.jacodb.api.cfg.JcLambdaExpr +import org.usvm.UAddressSort +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapAddress +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.machine.JcContext +import org.usvm.memory.UMemoryRegion +import org.usvm.memory.UMemoryRegionId + +class JcLambdaCallSiteRegionId(private val ctx: JcContext) : UMemoryRegionId { + override val sort: UAddressSort + get() = ctx.addressSort + + override fun emptyRegion(): UMemoryRegion = + JcLambdaCallSiteMemoryRegion(ctx) +} + +internal class JcLambdaCallSiteMemoryRegion( + private val ctx: JcContext, + private val callSites: PersistentMap = persistentHashMapOf() +) : UMemoryRegion { + fun writeCallSite(callSite: JcLambdaCallSite) = + JcLambdaCallSiteMemoryRegion(ctx, callSites.put(callSite.ref.address, callSite)) + + fun findCallSite(ref: UConcreteHeapRef): JcLambdaCallSite? = callSites[ref.address] + + override fun read(key: Nothing): UExpr { + error("Unsupported operation for call site region") + } + + override fun write( + key: Nothing, + value: UExpr, + guard: UBoolExpr + ): UMemoryRegion { + error("Unsupported operation for call site region") + } +} + +data class JcLambdaCallSite( + val ref: UConcreteHeapRef, + val lambda: JcLambdaExpr, + val callSiteArgs: List> +) 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 af8261460f..be41f05b64 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 @@ -107,10 +107,12 @@ import org.usvm.machine.operator.wideTo32BitsIfNeeded import org.usvm.machine.state.JcMethodResult import org.usvm.machine.state.JcState import org.usvm.machine.state.addConcreteMethodCallStmt +import org.usvm.machine.state.addDynamicCall import org.usvm.machine.state.addVirtualMethodCallStmt import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop import org.usvm.memory.ULValue import org.usvm.memory.URegisterStackLValue +import org.usvm.memory.UWritableMemory import org.usvm.mkSizeExpr import org.usvm.sizeSort import org.usvm.util.allocHeapRef @@ -390,22 +392,30 @@ class JcExprResolver( resolveInvoke( expr.method, instanceExpr = null, - argumentExprs = expr::args, - argumentTypes = expr::callSiteArgTypes - ) { arguments -> - TODO("Dynamic invoke: ${expr.method.method} $arguments") + argumentExprs = { expr.callSiteArgs }, + argumentTypes = { expr.callSiteArgTypes } + ) { callSiteArguments -> + scope.doWithState { addDynamicCall(expr, callSiteArguments) } } - override fun visitJcLambdaExpr(expr: JcLambdaExpr): UExpr? = - resolveInvoke( - expr.method, - instanceExpr = null, - argumentExprs = expr::args, - argumentTypes = { expr.method.parameters.map { it.type } } - ) { arguments -> - scope.doWithState { addConcreteMethodCallStmt(expr.method.method, arguments) } + override fun visitJcLambdaExpr(expr: JcLambdaExpr): UExpr? { + val callSiteArgs = expr.callSiteArgs.zip(expr.callSiteArgTypes) { arg, type -> + resolveJcExpr(arg, type) ?: return null } + val callSiteRef = scope.calcOnState { memory.allocConcrete(expr.callSiteReturnType) } + val callSite = JcLambdaCallSite(callSiteRef, expr, callSiteArgs) + scope.doWithState { memory.writeCallSite(callSite) } + + return callSiteRef + } + + private fun UWritableMemory.writeCallSite(callSite: JcLambdaCallSite) { + val callSiteRegion = getRegion(ctx.lambdaCallSiteRegionId) as JcLambdaCallSiteMemoryRegion + val updatedRegion = callSiteRegion.writeCallSite(callSite) + setRegion(ctx.lambdaCallSiteRegionId, updatedRegion) + } + private inline fun resolveInvoke( method: JcTypedMethod, instanceExpr: JcValue?, 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 56a1304490..aed0708409 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 @@ -44,6 +44,7 @@ import org.usvm.forkblacklists.UForkBlackList import org.usvm.machine.JcApplicationGraph import org.usvm.machine.JcConcreteMethodCallInst import org.usvm.machine.JcContext +import org.usvm.machine.JcDynamicMethodCallInst import org.usvm.machine.JcInterpreterObserver import org.usvm.machine.JcMethodApproximationResolver import org.usvm.machine.JcMethodCall @@ -240,7 +241,7 @@ class JcInterpreter( } if (stmt.method.isNative) { - mockNativeMethod(scope, stmt) + mockMethod(scope, stmt) return } @@ -256,7 +257,17 @@ class JcInterpreter( return } - resolveVirtualInvoke(stmt, scope, typeSelector, forkOnRemainingTypes = false) + resolveVirtualInvoke(stmt, scope, forkOnRemainingTypes = false) + } + + is JcDynamicMethodCallInst -> { + observer?.onMethodCallWithResolvedArguments(simpleValueResolver, stmt, scope) + + if (approximateMethod(scope, stmt)) { + return + } + + mockMethod(scope, stmt, stmt.dynamicCall.callSiteReturnType) } } } @@ -504,7 +515,6 @@ class JcInterpreter( private fun resolveVirtualInvoke( methodCall: JcVirtualMethodCallInst, scope: JcStepScope, - typeSelector: JcTypeSelector, forkOnRemainingTypes: Boolean, ): Unit = resolveVirtualInvoke(ctx, methodCall, scope, typeSelector, forkOnRemainingTypes) @@ -515,13 +525,13 @@ class JcInterpreter( return approximationResolver.approximate(scope, exprResolver, methodCall) } - private fun mockNativeMethod( - scope: JcStepScope, - methodCall: JcConcreteMethodCallInst, - ) = with(methodCall) { - logger.warn { "Mocked: ${method.enclosingClass.name}::${method.name}" } + private fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall) { + val returnType = with(applicationGraph) { methodCall.method.typed }.returnType + mockMethod(scope, methodCall, returnType) + } - val returnType = with(applicationGraph) { method.typed }.returnType + private fun mockMethod(scope: JcStepScope, methodCall: JcMethodCall, returnType: JcType) = with(methodCall) { + logger.warn { "Mocked: ${method.enclosingClass.name}::${method.name}" } if (returnType == ctx.cp.void) { scope.doWithState { skipMethodInvocationWithValue(methodCall, ctx.voidValue) } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt index 4dafd26f58..b9918456ad 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt @@ -3,6 +3,7 @@ package org.usvm.machine.state import org.jacodb.api.JcMethod import org.jacodb.api.JcType import org.jacodb.api.cfg.JcArgument +import org.jacodb.api.cfg.JcDynamicCallExpr import org.jacodb.api.cfg.JcInst import org.jacodb.api.ext.cfg.locals import org.usvm.UExpr @@ -10,8 +11,8 @@ import org.usvm.UHeapRef import org.usvm.USort import org.usvm.machine.JcApplicationGraph import org.usvm.machine.JcConcreteMethodCallInst +import org.usvm.machine.JcDynamicMethodCallInst import org.usvm.machine.JcMethodCall -import org.usvm.machine.JcMethodEntrypointInst import org.usvm.machine.JcVirtualMethodCallInst val JcState.lastStmt get() = pathLocation.statement @@ -77,6 +78,10 @@ fun JcState.addVirtualMethodCallStmt(method: JcMethod, arguments: List>) { + newStmt(JcDynamicMethodCallInst(dynamicCall, arguments, lastStmt)) +} + fun JcMethod.localIdx(idx: Int) = if (isStatic) idx else idx + 1 // TODO: cache it with JacoDB cache diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/lambda/InvokeDynamicExamples.java b/usvm-jvm/src/samples/java/org/usvm/samples/lambda/InvokeDynamicExamples.java new file mode 100644 index 0000000000..e203ed3dbe --- /dev/null +++ b/usvm-jvm/src/samples/java/org/usvm/samples/lambda/InvokeDynamicExamples.java @@ -0,0 +1,81 @@ +package org.usvm.samples.lambda; + +import java.util.function.Function; + +public class InvokeDynamicExamples { + private static class IntWrapper { + final int value; + + private IntWrapper(int value) { + this.value = value; + } + + IntWrapper add(int other) { + return new IntWrapper(value + other); + } + } + + private static int runUnaryFunction(int data, Function f) { + int result = f.apply(new IntWrapper(data)).value; + return result + 17; + } + + private static int runSamFunction(int data, SamBase f) { + int result = f.samFunction(new IntWrapper(data)).value; + return result + 17; + } + + private static int runDefaultFunction(int data, SamBase f) { + int result = f.defaultFunction(new IntWrapper(data)); + return result + 17; + } + + public interface SamBase { + IntWrapper samFunction(IntWrapper data); + + default int defaultFunction(IntWrapper data) { + if (data == null) { + return -2; + } + return samFunction(data).value + 31; + } + } + + private static IntWrapper add(IntWrapper a, int b) { + return a.add(b); + } + + private static IntWrapper addTwo(IntWrapper x) { + return x.add(2); + } + + public static int testUnaryFunction(int in) { + return runUnaryFunction(in, d -> d.add(2)); + } + + public static int testMethodRefUnaryFunction(int in) { + return runUnaryFunction(in, InvokeDynamicExamples::addTwo); + } + + public static int testCurryingFunction(int in) { + Function add42 = x -> add(x, 42); + return runUnaryFunction(in, d -> add42.apply(d.add(2))); + } + + public static int testSamFunction(int in) { + return runSamFunction(in, d -> d.add(2)); + } + + public static int testSamWithDefaultFunction(int in) { + return runDefaultFunction(in, d -> d.add(2)); + } + + private static String runComplexStringConcat(String str, int v) { + return str + v + 'x' + str + 17 + str; + } + + public static int testComplexInvokeDynamic(Object unused) { + String concatenated = runComplexStringConcat("abc", 42); + return concatenated != null ? 0 : -1; + } +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/InvokeDynamicExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/InvokeDynamicExamplesTest.kt new file mode 100644 index 0000000000..7c99cea6d8 --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/lambda/InvokeDynamicExamplesTest.kt @@ -0,0 +1,61 @@ +package org.usvm.samples.lambda + +import org.usvm.samples.JavaMethodTestRunner +import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults +import kotlin.test.Test + +class InvokeDynamicExamplesTest : JavaMethodTestRunner() { + @Test + fun testSimpleUnaryFunction() { + checkDiscoveredProperties( + InvokeDynamicExamples::testUnaryFunction, + eq(1), + { data, res -> res == data + 2 + 17 } + ) + } + + @Test + fun testMethodRefUnaryFunction() { + checkDiscoveredProperties( + InvokeDynamicExamples::testMethodRefUnaryFunction, + eq(1), + { data, res -> res == data + 2 + 17 } + ) + } + + @Test + fun testSimpleCurryingFunction() { + checkDiscoveredProperties( + InvokeDynamicExamples::testCurryingFunction, + eq(1), + { data, res -> res == data + 2 + 42 + 17 } + ) + } + + @Test + fun testSimpleSamFunction() { + checkDiscoveredProperties( + InvokeDynamicExamples::testSamFunction, + eq(1), + { data, res -> res == data + 2 + 17 } + ) + } + + @Test + fun testSamWithDefaultFunction() { + checkDiscoveredProperties( + InvokeDynamicExamples::testSamWithDefaultFunction, + eq(1), + { data, res -> res == data + 2 + 31 + 17 } + ) + } + + @Test + fun testComplexInvokeDynamic() { + checkDiscoveredProperties( + InvokeDynamicExamples::testComplexInvokeDynamic, + ignoreNumberOfAnalysisResults + ) + } +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt index c0efa82e9a..a9b62cddd8 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt @@ -3,6 +3,7 @@ package org.usvm.samples.wrappers import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq +import org.usvm.test.util.checkers.ge internal class BooleanWrapperTest : JavaMethodTestRunner() { @@ -31,9 +32,11 @@ internal class BooleanWrapperTest : JavaMethodTestRunner() { fun equalityTest() { checkDiscoveredProperties( BooleanWrapper::equality, - eq(2), + ge(2), { _, a, b, result -> a == b && result == 1 }, - { _, a, b, result -> a != b && result == 4 }, // method under test has unreachable branches because of caching + { _, a, b, result -> a != b && result == 4 }, + // method under test has unreachable branches because of caching + invariants = arrayOf({ _, _, _, result -> result != 2 && result != 3 }), ) } } \ No newline at end of file