Input arrays support

UnitTestBot · CaelmBleidd · May 29, 2025 · May 29, 2025 · May 30, 2025 · May 30, 2025
commit 545887c50cc60ef7cdf5cb4531de2972668cff7c
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -821,9 +821,7 @@ class TsExprResolver(
                 val fakeRef = if (ref.isFakeObject()) {
                     ref
                 } else {
-                    mkFakeValue(scope, bool, fp, ref).also {
-                        lValuesToAllocatedFakeObjects += refLValue to it
-                    }
+                    mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it }
                 }
 
                 // TODO ambiguous enum fields resolution

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
@@ -100,3 +100,14 @@ fun UExpr<*>.extractInt(): Int {
     }
     error("Cannot extract Int from $this")
 }
+
+/**
+ * Extracts an integer value from [this] expression if possible.
+ * Otherwise, throws an error.
+ */
+fun UExpr<out USort>.extractInt(): Int {
+    if (this@extractInt is KBitVec32Value) {
+        return intValue
+    }
+    error("Cannot extract int from $this")
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -573,6 +573,7 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractBool(scope)
                             lhsType.boolTypeExpr
                         }
+                        }
 
                         fp64Sort -> {
                             lhsValue = lhs.extractFp(scope)
@@ -583,7 +584,6 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractRef(scope)
                             lhsType.refTypeExpr
                         }
-
                         else -> error("Unsupported sort ${rhs.sort}")
                     }
                 }
@@ -595,6 +595,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractBool(scope)
                             rhsType.boolTypeExpr
                         }
+                        }
 
                         fp64Sort -> {
                             rhsValue = rhs.extractFp(scope)
@@ -605,7 +606,6 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractRef(scope)
                             rhsType.refTypeExpr
                         }
-
                         else -> error("Unsupported sort ${lhs.sort}")
                     }
                 }

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -49,6 +49,7 @@ class TsState(
     val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)),
     val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
+    val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,