From 22522f32d2517e97ea635de432d79bcc2e6817d2 Mon Sep 17 00:00:00 2001
From: Sergey Pospelov <sergeypospelov59@gmail.com>
Date: Fri, 23 Jun 2023 11:23:34 +0300
Subject: [PATCH] Fix: exact method types resolving

---
 .../kotlin/org/usvm/machine/JcExprResolver.kt | 25 ++++++++++++++++---
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
index fcf7cfc950..b07ec3e982 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
@@ -308,7 +308,12 @@ class JcExprResolver(
             val instance = resolveJcExpr(expr.instance)?.asExpr(ctx.addressSort) ?: return@resolveInvoke null
             checkNullPointer(instance) ?: return@resolveInvoke null
             val arguments = mutableListOf<UExpr<out USort>>(instance)
-            expr.args.mapTo(arguments) { resolveJcExpr(it) ?: return@resolveInvoke null }
+
+            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
+
+            argsWithTypes.mapTo(arguments) { (expr, type) ->
+                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+            }
             arguments
         }
 
@@ -318,13 +323,21 @@ class JcExprResolver(
             val instance = resolveJcExpr(expr.instance)?.asExpr(ctx.addressSort) ?: return@resolveInvoke null
             checkNullPointer(instance) ?: return@resolveInvoke null
             val arguments = mutableListOf<UExpr<out USort>>(instance)
-            expr.args.mapTo(arguments) { resolveJcExpr(it) ?: return@resolveInvoke null }
+            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
+
+            argsWithTypes.mapTo(arguments) { (expr, type) ->
+                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+            }
             arguments
         }
 
     override fun visitJcStaticCallExpr(expr: JcStaticCallExpr): UExpr<out USort>? =
         resolveInvoke(expr.method) {
-            expr.args.map { resolveJcExpr(it) ?: return@resolveInvoke null }
+            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
+
+            argsWithTypes.map { (expr, type) ->
+                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+            }
         }
 
     override fun visitJcDynamicCallExpr(expr: JcDynamicCallExpr): UExpr<out USort> = with(ctx) {
@@ -333,7 +346,11 @@ class JcExprResolver(
 
     override fun visitJcLambdaExpr(expr: JcLambdaExpr): UExpr<out USort>? =
         resolveInvoke(expr.method) {
-            expr.args.map { resolveJcExpr(it) ?: return@resolveInvoke null }
+            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
+
+            argsWithTypes.map { (expr, type) ->
+                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+            }
         }
 
     private fun resolveInvoke(