Minor fixes

UnitTestBot · Oct 3, 2023 · 31f18a3 · 31f18a3
1 parent ec60803
commit 31f18a3
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 30 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
@@ -88,6 +88,11 @@ 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<UExpr<out USort>>,

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
@@ -718,26 +718,25 @@ class JcExprResolver(
             ref = classRef
         )
 
-    private fun resolveArrayAccess(array: JcValue, index: JcValue): UArrayIndexLValue<JcType, *, USizeSort>? =
-        with(ctx) {
-            val arrayRef = resolveJcExpr(array)?.asExpr(addressSort) ?: return null
-            checkNullPointer(arrayRef) ?: return null
+    private fun resolveArrayAccess(array: JcValue, index: JcValue): UArrayIndexLValue<JcType, *, USizeSort>? = with(ctx) {
+        val arrayRef = resolveJcExpr(array)?.asExpr(addressSort) ?: return null
+        checkNullPointer(arrayRef) ?: return null
 
-            val arrayDescriptor = arrayDescriptorOf(array.type as JcArrayType)
+        val arrayDescriptor = arrayDescriptorOf(array.type as JcArrayType)
 
-            val idx = resolveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null
-            val lengthRef = UArrayLengthLValue(arrayRef, arrayDescriptor, sizeSort)
-            val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
+        val idx = resolveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null
+        val lengthRef = UArrayLengthLValue(arrayRef, arrayDescriptor, sizeSort)
+        val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
 
-            assertHardMaxArrayLength(length) ?: return null
+        assertHardMaxArrayLength(length) ?: return null
 
-            checkArrayIndex(idx, length) ?: return null
+        checkArrayIndex(idx, length) ?: return null
 
-            val elementType = requireNotNull(array.type.ifArrayGetElementType)
-            val cellSort = typeToSort(elementType)
+        val elementType = requireNotNull(array.type.ifArrayGetElementType)
+        val cellSort = typeToSort(elementType)
 
-            return UArrayIndexLValue(cellSort, arrayRef, idx, arrayDescriptor)
-        }
+        return UArrayIndexLValue(cellSort, arrayRef, idx, arrayDescriptor)
+    }
 
     // endregion
 
@@ -957,10 +956,8 @@ class JcExprResolver(
         scope.calcOnState {
             with(ctx) {
                 // We can use any sort here as it is not used
-                val staticFieldsMemoryRegionId =
-                    JcStaticFieldRegionId(staticInitializer.enclosingClass.toType(), voidSort)
-                val staticFieldsMemoryRegion =
-                    memory.getRegion(staticFieldsMemoryRegionId) as JcStaticFieldsMemoryRegion
+                val staticFieldsMemoryRegionId = JcStaticFieldRegionId(staticInitializer.enclosingClass.toType(), voidSort)
+                val staticFieldsMemoryRegion = memory.getRegion(staticFieldsMemoryRegionId) as JcStaticFieldsMemoryRegion
                 staticFieldsMemoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(this@calcOnState)
             }
         }

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
@@ -287,12 +287,7 @@ class JcInterpreter(
             val methodResult = scope.calcOnState { methodResult }
 
             when (methodResult) {
-                is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(
-                    exprResolver.simpleValueResolver,
-                    it,
-                    scope
-                )
-
+                is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(exprResolver.simpleValueResolver, it, scope)
                 is JcMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
                 is JcMethodResult.JcException -> error("Exceptions must be processed earlier")
             }
@@ -414,12 +409,7 @@ class JcInterpreter(
         val methodResult = scope.calcOnState { methodResult }
 
         when (methodResult) {
-            is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(
-                exprResolver.simpleValueResolver,
-                callExpr,
-                scope
-            )
-
+            is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(exprResolver.simpleValueResolver, callExpr, scope)
             is JcMethodResult.Success -> observer?.onCallStatement(exprResolver.simpleValueResolver, stmt, scope)
             is JcMethodResult.JcException -> error("Exceptions must be processed earlier")
         }