Format

Author: Lipen

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -52,7 +52,6 @@ class TsContext(
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
-
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -657,7 +657,6 @@ class TsExprResolver(
 
                     fakeObj
                 }
-
             }
         } else {
             val lValue = mkArrayIndexLValue(
@@ -754,7 +753,9 @@ 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
+                    }
                 }
                 memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
 

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt

@@ -73,26 +73,30 @@ class TsVoidSort(ctx: TsContext) : USort(ctx) {
     }
 }
 
-fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
+fun UExpr<*>.toConcreteBoolValue(): Boolean = when (this) {
     ctx.trueExpr -> true
     ctx.falseExpr -> false
-    else -> error("Cannot extract boolean from $this")
+    else -> error("Cannot extract Boolean from $this")
 }
 
-fun UExpr<out USort>.extractDouble(): Double {
+/**
+ * Extracts a double value from [this] expression if possible.
+ * Otherwise, throws an error.
+ */
+fun UExpr<*>.extractDouble(): Double {
     if (this@extractDouble is KFp64Value) {
         return value
     }
-    error("Cannot extract double from $this")
+    error("Cannot extract Double from $this")
 }
 
 /**
  * Extracts an integer value from [this] expression if possible.
  * Otherwise, throws an error.
  */
-fun UExpr<out USort>.extractInt(): Int {
+fun UExpr<*>.extractInt(): Int {
     if (this@extractInt is KBitVec32Value) {
         return intValue
     }
-    error("Cannot extract int from $this")
+    error("Cannot extract Int from $this")
 }

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)
                             lhsType.fpTypeExpr
@@ -582,6 +583,7 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractRef(scope)
                             lhsType.refTypeExpr
                         }
+
                         else -> error("Unsupported sort ${rhs.sort}")
                     }
                 }
@@ -593,6 +595,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractBool(scope)
                             rhsType.boolTypeExpr
                         }
+
                         fp64Sort -> {
                             rhsValue = rhs.extractFp(scope)
                             rhsType.fpTypeExpr
@@ -602,6 +605,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractRef(scope)
                             rhsType.refTypeExpr
                         }
+
                         else -> error("Unsupported sort ${lhs.sort}")
                     }
                 }

usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt

@@ -47,7 +47,7 @@ class TsState(
     val localToSortStack: MutableList<UPersistentHashMap<Int, USort>> = mutableListOf(persistentHashMapOf()),
     var staticStorage: UPersistentHashMap<EtsClass, UConcreteHeapRef> = persistentHashMapOf(),
     val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)),
-    val addedArtificialLocals: MutableSet<String> = hashSetOf<String>(),
+    val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,

usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt

@@ -328,4 +328,4 @@ fun EtsClassType.toAuxiliaryType(hierarchy: EtsHierarchy): EtsAuxiliaryType? {
     return EtsAuxiliaryType(
         properties = fieldsIntersection + methodsIntersection
     )
-}
+}

usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt

@@ -108,7 +108,6 @@ class EtsHierarchy(private val scene: EtsScene) {
         return suitableClasses.values
     }
 
-
     companion object {
         // TODO use real one
         val OBJECT_CLASS = EtsClassType(
@@ -135,4 +134,4 @@ fun ClassName.removeTrashFromTheName(): ClassName {
     } else {
         nameWithoutGenerics().removePrefixWithDots()
     }
-}
+}

usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt

@@ -41,7 +41,7 @@ fun EtsType.isResolved(): Boolean =
     this !is EtsUnclearRefType && (this as? EtsClassType)?.signature?.file != EtsFileSignature.UNKNOWN
 
 fun EtsType.getClassesForType(
-    scene: EtsScene
+    scene: EtsScene,
 ): List<EtsClass> = if (isResolved()) {
     scene
         .projectAndSdkClasses
@@ -74,4 +74,4 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe
     }
 
     return fakeObject
-}
+}

usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt

@@ -92,21 +92,21 @@ class TsTestResolver {
             when (lValue) {
                 is UFieldLValue<*, *> -> {
                     val resolvedRef = state.models.first().eval(lValue.ref)
-                    resolvedLValuesToFakeObjects += UFieldLValue(lValue.sort, resolvedRef, lValue.field) to fakeObject
+                    val fieldLValue = UFieldLValue(lValue.sort, resolvedRef, lValue.field)
+                    resolvedLValuesToFakeObjects += fieldLValue to fakeObject
                 }
 
                 is UArrayIndexLValue<*, *, *> -> {
                     val model = state.models.first()
                     val resolvedRef = model.eval(lValue.ref)
                     val resolvedIndex = model.eval(lValue.index)
-
-                    val uArrayIndexLValue = UArrayIndexLValue(
+                    val arrayIndexLValue = UArrayIndexLValue(
                         lValue.sort,
                         resolvedRef,
                         resolvedIndex,
                         lValue.arrayType,
                     )
-                    resolvedLValuesToFakeObjects += uArrayIndexLValue to fakeObject
+                    resolvedLValuesToFakeObjects += arrayIndexLValue to fakeObject
                 }
 
                 else -> error("Unexpected lValue type: ${lValue::class.java.name}")
@@ -235,8 +235,8 @@ open class TsTestStateResolver(
         val arrayLength = mkArrayLengthLValue(heapRef, type)
         val length = resolveLValue(arrayLength) as TsTestValue.TsNumber
 
-        val values = (0 until length.number.toInt()).map {
-            val index = mkSizeExpr(it)
+        val values = (0 until length.number.toInt()).map { i ->
+            val index = mkSizeExpr(i)
             val sort = typeToSort(type.elementType)
 
             if (sort is TsUnresolvedSort) {