Basic USVM TS type system with type coercion (#215)

UnitTestBot · Jan 29, 2025 · 3b6a01d · 3b6a01d
1 parent 8c87d76
commit 3b6a01d
Show file tree

Hide file tree

Showing 49 changed files with 3,374 additions and 931 deletions.
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "983d3538a9"
+    const val jacodb = "8a588e71e7"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -5,6 +5,9 @@ import org.usvm.StepScope.StepScopeState.CAN_BE_PROCESSED
 import org.usvm.StepScope.StepScopeState.DEAD
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.utils.checkSat
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.InvocationKind
+import kotlin.contracts.contract
 
 /**
  * An auxiliary class, which carefully maintains forks and asserts via [forkWithBlackList] and [assert].
@@ -48,7 +51,11 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      *
      * @return `null` if the underlying state is `null`.
      */
+    @OptIn(ExperimentalContracts::class)
     fun doWithState(block: T.() -> Unit) {
+        contract {
+            callsInPlace(block, InvocationKind.EXACTLY_ONCE)
+        }
         check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
         return originalState.block()
     }
@@ -58,7 +65,11 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      *
      * @return `null` if the underlying state is `null`, otherwise returns result of calling [block].
      */
+    @OptIn(ExperimentalContracts::class)
     fun <R> calcOnState(block: T.() -> R): R {
+        contract {
+            callsInPlace(block, InvocationKind.EXACTLY_ONCE)
+        }
         check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
         return originalState.block()
     }

diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CyclesTest.kt
@@ -89,13 +89,21 @@ internal class CyclesTest : JavaMethodTestRunner() {
             stopOnCoverage = -1
         ),
     ){
-        checkDiscoveredProperties(
-            Cycles::innerLoop,
-            ignoreNumberOfAnalysisResults,
-            { _, x, r -> x in 1..3 && r == 0 },
-            { _, x, r -> x == 4 && r == 1 },
-            { _, x, r -> x >= 5 && r == 0 }
-        )
+        withOptions(
+            options.copy(
+                stopOnCoverage = 0,
+                stateCollectionStrategy = StateCollectionStrategy.ALL,
+                collectedStatesLimit = 100,
+            )
+        ) {
+            checkDiscoveredProperties(
+                Cycles::innerLoop,
+                ignoreNumberOfAnalysisResults,
+                { _, x, r -> x in 1..3 && r == 0 },
+                { _, x, r -> x == 4 && r == 1 },
+                { _, x, r -> x >= 5 && r == 0 }
+            )
+        }
     }
 
     @Test

diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
@@ -17,16 +17,12 @@
 package org.usvm.dataflow.ts.infer.dto
 
 import org.jacodb.ets.base.EtsAliasType
-import org.jacodb.ets.base.EtsAnnotationNamespaceType
-import org.jacodb.ets.base.EtsAnnotationTypeQueryType
 import org.jacodb.ets.base.EtsAnyType
-import org.jacodb.ets.base.EtsArrayObjectType
 import org.jacodb.ets.base.EtsArrayType
 import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsClassType
 import org.jacodb.ets.base.EtsFunctionType
 import org.jacodb.ets.base.EtsGenericType
-import org.jacodb.ets.base.EtsLexicalEnvType
 import org.jacodb.ets.base.EtsLiteralType
 import org.jacodb.ets.base.EtsNeverType
 import org.jacodb.ets.base.EtsNullType
@@ -40,15 +36,12 @@ import org.jacodb.ets.base.EtsUnionType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsVoidType
 import org.jacodb.ets.dto.AliasTypeDto
-import org.jacodb.ets.dto.AnnotationNamespaceTypeDto
-import org.jacodb.ets.dto.AnnotationTypeQueryTypeDto
 import org.jacodb.ets.dto.AnyTypeDto
 import org.jacodb.ets.dto.ArrayTypeDto
 import org.jacodb.ets.dto.BooleanTypeDto
 import org.jacodb.ets.dto.ClassTypeDto
 import org.jacodb.ets.dto.FunctionTypeDto
 import org.jacodb.ets.dto.GenericTypeDto
-import org.jacodb.ets.dto.LexicalEnvTypeDto
 import org.jacodb.ets.dto.LiteralTypeDto
 import org.jacodb.ets.dto.LocalDto
 import org.jacodb.ets.dto.LocalSignatureDto
@@ -155,10 +148,6 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
         )
     }
 
-    override fun visit(type: EtsArrayObjectType): TypeDto {
-        TODO("Not yet implemented")
-    }
-
     override fun visit(type: EtsUnclearRefType): TypeDto {
         return UnclearReferenceTypeDto(
             name = type.typeName,
@@ -184,24 +173,4 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
             ),
         )
     }
-
-    override fun visit(type: EtsAnnotationNamespaceType): TypeDto {
-        return AnnotationNamespaceTypeDto(
-            originType = type.originType,
-            namespaceSignature = type.namespaceSignature.toDto(),
-        )
-    }
-
-    override fun visit(type: EtsAnnotationTypeQueryType): TypeDto {
-        return AnnotationTypeQueryTypeDto(
-            originType = type.originType,
-        )
-    }
-
-    override fun visit(type: EtsLexicalEnvType): TypeDto {
-        return LexicalEnvTypeDto(
-            nestedMethod = type.nestedMethod.toDto(),
-            closures = type.closures.map { it.toDto() as LocalDto }, // safe cast
-        )
-    }
 }
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt
@@ -18,9 +18,6 @@ package org.usvm.dataflow.ts.infer.dto
 
 import org.jacodb.ets.base.EtsArrayAccess
 import org.jacodb.ets.base.EtsBooleanConstant
-import org.jacodb.ets.base.EtsCaughtExceptionRef
-import org.jacodb.ets.base.EtsClosureFieldRef
-import org.jacodb.ets.base.EtsGlobalRef
 import org.jacodb.ets.base.EtsInstanceFieldRef
 import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsNullConstant
@@ -33,10 +30,7 @@ import org.jacodb.ets.base.EtsUndefinedConstant
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.dto.ArrayRefDto
 import org.jacodb.ets.dto.BooleanTypeDto
-import org.jacodb.ets.dto.CaughtExceptionRefDto
-import org.jacodb.ets.dto.ClosureFieldRefDto
 import org.jacodb.ets.dto.ConstantDto
-import org.jacodb.ets.dto.GlobalRefDto
 import org.jacodb.ets.dto.InstanceFieldRefDto
 import org.jacodb.ets.dto.LocalDto
 import org.jacodb.ets.dto.NullTypeDto
@@ -106,27 +100,6 @@ private object EtsValueToDto : EtsValue.Visitor<ValueDto> {
         )
     }
 
-    override fun visit(value: EtsCaughtExceptionRef): ValueDto {
-        return CaughtExceptionRefDto(
-            type = value.type.toDto(),
-        )
-    }
-
-    override fun visit(value: EtsGlobalRef): ValueDto {
-        return GlobalRefDto(
-            name = value.name,
-            ref = value.ref?.toDto(),
-        )
-    }
-
-    override fun visit(value: EtsClosureFieldRef): ValueDto {
-        return ClosureFieldRefDto(
-            base = value.base.toDto() as LocalDto, // safe cast
-            fieldName = value.fieldName,
-            type = value.type.toDto(),
-        )
-    }
-
     override fun visit(value: EtsArrayAccess): ValueDto {
         return ArrayRefDto(
             array = value.array.toDto(),

diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt
diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt b/usvm-ts/src/main/kotlin/org/usvm/TSContext.kt