Merge branch 'main' into caelmbleidd/mocks_and_statics

UnitTestBot · Feb 19, 2024 · 0ee649d · 0ee649d
2 parents 4f7ee87 + 1d00c9b
commit 0ee649d
Show file tree

Hide file tree

Showing 49 changed files with 662 additions and 389 deletions.
diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt
@@ -1,7 +1,7 @@
 object Versions {
     const val klogging = "1.8.3"
     const val slf4j = "1.6.1"
-    const val ksmt = "0.5.13"
+    const val ksmt = "0.5.21"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
     const val jcdb = "1.4.1"

diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -41,6 +41,8 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
      */
     fun stepResult() = StepResult(forkedStates.asSequence(), alive)
 
+    val isDead: Boolean get() = stepScopeState === DEAD
+
     /**
      * Executes [block] on a state.
      *

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
@@ -7,6 +7,7 @@ import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.uctx
+import org.usvm.utils.logAssertFailure
 
 // TODO: special mock api for variables
 
@@ -39,7 +40,9 @@ private inline fun <Type, Method, State> StepScope<State, Type, *, *>.mockSymbol
         mkTypeConstraint(ref)
     }
 
-    assert(typeConstraint) ?: return null
+    assert(typeConstraint)
+        .logAssertFailure { "Constraint violation: Type constraint in mockSymbolicRef" }
+        ?: return null
 
     return ref
 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
@@ -17,6 +17,7 @@ import org.usvm.mkSizeExpr
 import org.usvm.mkSizeGeExpr
 import org.usvm.mkSizeSubExpr
 import org.usvm.sizeSort
+import org.usvm.utils.logAssertFailure
 
 object ListCollectionApi {
     fun <ListType, USizeSort : USort, Ctx: UContext<USizeSort>> UState<ListType, *, *, Ctx, *, *>.mkSymbolicList(
@@ -51,7 +52,9 @@ object ListCollectionApi {
                 with(ctx) {
                     val boundConstraint = mkSizeGeExpr(length, mkSizeExpr(0))
                     // List size must be correct regardless of guard
-                    assert(boundConstraint) ?: return null
+                    assert(boundConstraint)
+                        .logAssertFailure { "Constraint violation: SymbolicList size correctness constraint" }
+                        ?: return null
                 }
                 symbolicListRef
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
@@ -25,6 +25,7 @@ import org.usvm.mkSizeGeExpr
 import org.usvm.mkSizeSubExpr
 import org.usvm.sizeSort
 import org.usvm.uctx
+import org.usvm.utils.logAssertFailure
 
 object ObjectMapCollectionApi {
     fun <MapType, USizeSort : USort, Ctx: UContext<USizeSort>> UState<MapType, *, *, Ctx, *, *>.mkSymbolicObjectMap(
@@ -61,7 +62,9 @@ object ObjectMapCollectionApi {
                 with(ctx) {
                     val boundConstraint = mkSizeGeExpr(length, mkSizeExpr(0))
                     // Map size must be correct regardless of guard
-                    assert(boundConstraint) ?: return null
+                    assert(boundConstraint)
+                        .logAssertFailure { "Constraint violation: SymbolicMap size correctness constraint" }
+                        ?: return null
                 }
                 symbolicMapRef
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt
@@ -2,22 +2,19 @@ package org.usvm.collection.array
 
 import io.ksmt.KContext
 import io.ksmt.expr.KExpr
-import io.ksmt.solver.KModel
 import io.ksmt.sort.KArray2Sort
 import io.ksmt.sort.KArraySort
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.mkConst
 import org.usvm.UAddressSort
 import org.usvm.UConcreteHeapAddress
-import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
-import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.URangedUpdateNode
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
-import org.usvm.model.UMemory2DArray
+import org.usvm.model.UModelEvaluator
 import org.usvm.sizeSort
 import org.usvm.solver.U1DUpdatesTranslator
 import org.usvm.solver.U2DUpdatesTranslator
@@ -54,10 +51,9 @@ class UArrayRegionDecoder<ArrayType, Sort : USort, USizeSort : USort>(
     }
 
     override fun decodeLazyRegion(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>,
+        model: UModelEvaluator<*>,
         assertions: List<KExpr<KBoolSort>>
-    ) = inputRegionTranslator?.let { UArrayLazyModelRegion(regionId, model, mapping, it) }
+    ) = inputRegionTranslator?.let { UArrayLazyModelRegion(regionId, model, it) }
 }
 
 private class UAllocatedArrayRegionTranslator<ArrayType, Sort : USort, USizeSort : USort>(
@@ -103,10 +99,9 @@ private class UInputArrayRegionTranslator<ArrayType, Sort : USort, USizeSort : U
     }
 
     override fun decodeCollection(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>
+        model: UModelEvaluator<*>
     ): UReadOnlyMemoryRegion<USymbolicArrayIndex<USizeSort>, Sort> =
-        UMemory2DArray(initialValue, model, mapping)
+        model.evalAndCompleteArray2DMemoryRegion(initialValue.decl)
 }
 
 private class UAllocatedArrayUpdatesTranslator<Sort : USort, USizeSort : USort>(

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt
@@ -1,10 +1,9 @@
 package org.usvm.collection.array
 
-import io.ksmt.solver.KModel
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.model.AddressesMapping
+import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
 import org.usvm.solver.UCollectionDecoder
 
@@ -21,12 +20,11 @@ abstract class UArrayModelRegion<ArrayType, Sort : USort, USizeSort : USort>(
 
 class UArrayLazyModelRegion<ArrayType, Sort : USort, USizeSort : USort>(
     regionId: UArrayRegionId<ArrayType, Sort, USizeSort>,
-    private val model: KModel,
-    private val addressesMapping: AddressesMapping,
+    private val model: UModelEvaluator<*>,
     private val inputArrayDecoder: UCollectionDecoder<USymbolicArrayIndex<USizeSort>, Sort>
 ) : UArrayModelRegion<ArrayType, Sort, USizeSort>(regionId) {
     override val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex<USizeSort>, Sort> by lazy {
-        inputArrayDecoder.decodeCollection(model, addressesMapping)
+        inputArrayDecoder.decodeCollection(model)
     }
 }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt
@@ -1,7 +1,7 @@
 package org.usvm.collection.array.length
 
 import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentMapOf
+import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
@@ -42,7 +42,7 @@ interface UArrayLengthsRegion<ArrayType, USizeSort : USort> : UMemoryRegion<UArr
 internal class UArrayLengthsMemoryRegion<ArrayType, USizeSort : USort>(
     private val sort: USizeSort,
     private val arrayType: ArrayType,
-    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentMapOf(),
+    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
     private var inputLengths: UInputArrayLengths<ArrayType, USizeSort>? = null
 ) : UArrayLengthsRegion<ArrayType, USizeSort> {
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt
@@ -2,18 +2,16 @@ package org.usvm.collection.array.length
 
 import io.ksmt.KContext
 import io.ksmt.expr.KExpr
-import io.ksmt.solver.KModel
 import io.ksmt.sort.KArraySort
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.mkConst
 import org.usvm.UAddressSort
-import org.usvm.UConcreteHeapRef
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.URangedUpdateNode
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.memory.USymbolicCollection
-import org.usvm.model.UMemory1DArray
+import org.usvm.model.UModelEvaluator
 import org.usvm.sizeSort
 import org.usvm.solver.U1DUpdatesTranslator
 import org.usvm.solver.UCollectionDecoder
@@ -39,10 +37,9 @@ class UArrayLengthRegionDecoder<ArrayType, USizeSort : USort>(
     }
 
     override fun decodeLazyRegion(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>,
+        model: UModelEvaluator<*>,
         assertions: List<KExpr<KBoolSort>>
-    ) = inputArrayLengthTranslator?.let { UArrayLengthLazyModelRegion(regionId, model, mapping, it) }
+    ) = inputArrayLengthTranslator?.let { UArrayLengthLazyModelRegion(regionId, model, it) }
 }
 
 private class UInputArrayLengthRegionTranslator<ArrayType, USizeSort : USort>(
@@ -66,10 +63,9 @@ private class UInputArrayLengthRegionTranslator<ArrayType, USizeSort : USort>(
     }
 
     override fun decodeCollection(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>
+        model: UModelEvaluator<*>
     ): UReadOnlyMemoryRegion<UHeapRef, USizeSort> =
-        UMemory1DArray(initialValue, model, mapping)
+        model.evalAndCompleteArray1DMemoryRegion(initialValue.decl)
 }
 
 private class UInputArrayLengthUpdateTranslator<USizeSort : USort>(

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt
@@ -1,11 +1,10 @@
 package org.usvm.collection.array.length
 
-import io.ksmt.solver.KModel
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.model.AddressesMapping
+import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
 import org.usvm.solver.UCollectionDecoder
 
@@ -22,12 +21,11 @@ abstract class UArrayLengthModelRegion<ArrayType, USizeSort : USort>(
 
 class UArrayLengthLazyModelRegion<ArrayType, USizeSort : USort>(
     regionId: UArrayLengthsRegionId<ArrayType, USizeSort>,
-    private val model: KModel,
-    private val addressesMapping: AddressesMapping,
+    private val model: UModelEvaluator<*>,
     private val inputArrayLengthDecoder: UCollectionDecoder<UHeapRef, USizeSort>,
 ) : UArrayLengthModelRegion<ArrayType, USizeSort>(regionId) {
     override val inputArrayLength: UReadOnlyMemoryRegion<UHeapRef, USizeSort> by lazy {
-        inputArrayLengthDecoder.decodeCollection(model, addressesMapping)
+        inputArrayLengthDecoder.decodeCollection(model)
     }
 }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt
@@ -2,18 +2,16 @@ package org.usvm.collection.field
 
 import io.ksmt.KContext
 import io.ksmt.expr.KExpr
-import io.ksmt.solver.KModel
 import io.ksmt.sort.KArraySort
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.mkConst
 import org.usvm.UAddressSort
-import org.usvm.UConcreteHeapRef
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.URangedUpdateNode
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.memory.USymbolicCollection
-import org.usvm.model.UMemory1DArray
+import org.usvm.model.UModelEvaluator
 import org.usvm.solver.U1DUpdatesTranslator
 import org.usvm.solver.UCollectionDecoder
 import org.usvm.solver.UExprTranslator
@@ -38,10 +36,9 @@ class UFieldRegionDecoder<Field, Sort : USort>(
     }
 
     override fun decodeLazyRegion(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>,
+        model: UModelEvaluator<*>,
         assertions: List<KExpr<KBoolSort>>
-    ) = inputRegionTranslator?.let { UFieldsLazyModelRegion(regionId, model, mapping, it) }
+    ) = inputRegionTranslator?.let { UFieldsLazyModelRegion(regionId, model, it) }
 }
 
 private class UInputFieldRegionTranslator<Field, Sort : USort>(
@@ -64,10 +61,9 @@ private class UInputFieldRegionTranslator<Field, Sort : USort>(
     }
 
     override fun decodeCollection(
-        model: KModel,
-        mapping: Map<UHeapRef, UConcreteHeapRef>
+        model: UModelEvaluator<*>
     ): UReadOnlyMemoryRegion<UHeapRef, Sort> =
-        UMemory1DArray(initialValue, model, mapping)
+        model.evalAndCompleteArray1DMemoryRegion(initialValue.decl)
 }
 
 private class UInputFieldUpdateTranslator<Sort : USort>(

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt
@@ -1,7 +1,7 @@
 package org.usvm.collection.field
 
 import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentMapOf
+import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
@@ -39,7 +39,7 @@ interface UFieldsRegion<Field, Sort : USort> : UMemoryRegion<UFieldLValue<Field,
 internal class UFieldsMemoryRegion<Field, Sort : USort>(
     private val sort: Sort,
     private val field: Field,
-    private val allocatedFields: PersistentMap<UConcreteHeapAddress, UExpr<Sort>> = persistentMapOf(),
+    private val allocatedFields: PersistentMap<UConcreteHeapAddress, UExpr<Sort>> = persistentHashMapOf(),
     private var inputFields: UInputFields<Field, Sort>? = null
 ) : UFieldsRegion<Field, Sort> {
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt
@@ -1,13 +1,11 @@
 package org.usvm.collection.field
 
-import io.ksmt.solver.KModel
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.model.AddressesMapping
+import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
-import org.usvm.sampleUValue
 import org.usvm.solver.UCollectionDecoder
 
 abstract class UFieldsModelRegion<Field, Sort : USort>(
@@ -23,12 +21,11 @@ abstract class UFieldsModelRegion<Field, Sort : USort>(
 
 class UFieldsLazyModelRegion<Field, Sort : USort>(
     regionId: UFieldsRegionId<Field, Sort>,
-    private val model: KModel,
-    private val addressesMapping: AddressesMapping,
+    private val model: UModelEvaluator<*>,
     private val inputFieldsDecoder: UCollectionDecoder<UHeapRef, Sort>
 ) : UFieldsModelRegion<Field, Sort>(regionId) {
     override val inputFields: UReadOnlyMemoryRegion<UHeapRef, Sort> by lazy {
-        inputFieldsDecoder.decodeCollection(model, addressesMapping)
+        inputFieldsDecoder.decodeCollection(model)
     }
 }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt
@@ -1,11 +1,10 @@
 package org.usvm.collection.map.length
 
-import io.ksmt.solver.KModel
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.model.AddressesMapping
+import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
 import org.usvm.solver.UCollectionDecoder
 
@@ -22,12 +21,11 @@ abstract class UMapLengthModelRegion<MapType, USizeSort : USort>(
 
 class UMapLengthLazyModelRegion<MapType, USizeSort : USort>(
     regionId: UMapLengthRegionId<MapType, USizeSort>,
-    private val model: KModel,
-    private val addressesMapping: AddressesMapping,
+    private val model: UModelEvaluator<*>,
     private val inputLengthDecoder: UCollectionDecoder<UHeapRef, USizeSort>
 ) : UMapLengthModelRegion<MapType, USizeSort>(regionId) {
     override val inputMapLength: UReadOnlyMemoryRegion<UHeapRef, USizeSort> by lazy {
-        inputLengthDecoder.decodeCollection(model, addressesMapping)
+        inputLengthDecoder.decodeCollection(model)
     }
 }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt
@@ -1,7 +1,7 @@
 package org.usvm.collection.map.length
 
 import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentMapOf
+import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
@@ -43,7 +43,7 @@ interface UMapLengthRegion<MapType, USizeSort : USort> : UMemoryRegion<UMapLengt
 internal class UMapLengthMemoryRegion<MapType, USizeSort : USort>(
     private val sort: USizeSort,
     private val mapType: MapType,
-    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentMapOf(),
+    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
     private var inputLengths: UInputMapLength<MapType, USizeSort>? = null
 ) : UMapLengthRegion<MapType, USizeSort> {
-Original file line number
+Diff line change
@@ Expand Up @@
          */
         fun stepResult() = StepResult(forkedStates.asSequence(), alive)
+        val isDead: Boolean get() = stepScopeState === DEAD
         /**
          * Executes [block] on a state.
          *
@@ Expand Down @@