Skip to content

Commit cd073a9

Browse files
sergeypospelovsergeypospelov
authored
Restructure packages (#13)
1 parent d828594 commit cd073a9

36 files changed

+359
-83
lines changed

‎usvm-core/src/main/kotlin/org/usvm/Composition.kt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
package org.usvm
22

3+
import org.usvm.memory.UReadOnlySymbolicHeap
4+
import org.usvm.memory.URegionId
5+
import org.usvm.memory.URegistersStackEvaluator
6+
37
@Suppress("MemberVisibilityCanBePrivate")
48
open class UComposer<Field, Type>(
59
ctx: UContext,

‎usvm-core/src/main/kotlin/org/usvm/Context.kt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,11 @@ import org.ksmt.sort.KUninterpretedSort
1111
import org.ksmt.utils.DefaultValueSampler
1212
import org.ksmt.utils.asExpr
1313
import org.ksmt.utils.cast
14+
import org.usvm.memory.UAllocatedArrayRegion
15+
import org.usvm.memory.UInputArrayLengthRegion
16+
import org.usvm.memory.UInputArrayRegion
17+
import org.usvm.memory.UInputFieldRegion
18+
import org.usvm.memory.splitUHeapRef
1419

1520
@Suppress("LeakingThis")
1621
open class UContext(

‎usvm-core/src/main/kotlin/org/usvm/Expressions.kt

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,17 @@ import org.ksmt.expr.*
66
import org.ksmt.expr.printer.ExpressionPrinter
77
import org.ksmt.expr.transformer.KTransformerBase
88
import org.ksmt.sort.*
9+
import org.usvm.memory.UAllocatedArrayId
10+
import org.usvm.memory.UAllocatedArrayRegion
11+
import org.usvm.memory.UInputArrayId
12+
import org.usvm.memory.UInputArrayLengthId
13+
import org.usvm.memory.UInputArrayLengthRegion
14+
import org.usvm.memory.UInputArrayRegion
15+
import org.usvm.memory.UInputFieldId
16+
import org.usvm.memory.UInputFieldRegion
17+
import org.usvm.memory.URegionId
18+
import org.usvm.memory.USymbolicArrayIndex
19+
import org.usvm.memory.USymbolicMemoryRegion
920

1021
//region KSMT aliases
1122

‎usvm-core/src/main/kotlin/org/usvm/Merging.kt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
package org.usvm
22

3+
import org.usvm.memory.URegionHeap
4+
35
interface UMerger<Entity> {
46
/**
57
* @returns Merged entity or null if [left] and [right] are non-mergeable

‎usvm-core/src/main/kotlin/org/usvm/State.kt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ package org.usvm
22

33
import kotlinx.collections.immutable.PersistentList
44
import org.ksmt.expr.KInterpretedValue
5+
import org.usvm.memory.UMemoryBase
6+
import org.usvm.model.UModel
57

68
abstract class UState<Type, Field, Method, Statement>(
79
// TODO: add interpreter-specific information

‎usvm-core/src/main/kotlin/org/usvm/Heap.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/Heap.kt

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,17 @@
1-
package org.usvm
1+
package org.usvm.memory
22

33
import kotlinx.collections.immutable.PersistentMap
44
import kotlinx.collections.immutable.persistentMapOf
55
import org.ksmt.utils.asExpr
6+
import org.usvm.UBoolExpr
7+
import org.usvm.UConcreteHeapAddress
8+
import org.usvm.UConcreteHeapRef
9+
import org.usvm.UContext
10+
import org.usvm.UExpr
11+
import org.usvm.UHeapRef
12+
import org.usvm.USizeExpr
13+
import org.usvm.USort
14+
import org.usvm.sampleUValue
615

716
interface UReadOnlyHeap<Ref, Value, SizeT, Field, ArrayType, Guard> {
817
fun <Sort : USort> readField(ref: Ref, field: Field, sort: Sort): Value

‎usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,14 @@
1-
package org.usvm
1+
package org.usvm.memory
2+
3+
import org.usvm.UAddressSort
4+
import org.usvm.UBoolExpr
5+
import org.usvm.UConcreteHeapRef
6+
import org.usvm.UExpr
7+
import org.usvm.UHeapRef
8+
import org.usvm.UIteExpr
9+
import org.usvm.USort
10+
import org.usvm.USymbolicHeapRef
11+
import org.usvm.isFalse
212

313
data class GuardedExpr<out T>(
414
val expr: T,

‎usvm-core/src/main/kotlin/org/usvm/Memory.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
1-
package org.usvm
1+
package org.usvm.memory
22

33
import org.ksmt.utils.asExpr
4+
import org.usvm.UArrayIndexRef
5+
import org.usvm.UComposer
6+
import org.usvm.UContext
7+
import org.usvm.UExpr
8+
import org.usvm.UFieldRef
9+
import org.usvm.UHeapRef
10+
import org.usvm.UIndexedMocker
11+
import org.usvm.ULValue
12+
import org.usvm.UMocker
13+
import org.usvm.URegisterRef
14+
import org.usvm.USizeExpr
15+
import org.usvm.USort
16+
import org.usvm.UTypeStorage
17+
import org.usvm.UTypeSystem
418

519
interface UMemory<LValue, RValue, SizeT, HeapRef, Type> {
620
/**

‎usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,31 @@
1-
package org.usvm
1+
package org.usvm.memory
22

33
import org.ksmt.utils.asExpr
4+
import org.usvm.UBoolExpr
5+
import org.usvm.UComposer
6+
import org.usvm.UConcreteHeapAddress
7+
import org.usvm.UConcreteHeapRef
8+
import org.usvm.UConcreteSize
9+
import org.usvm.UExpr
10+
import org.usvm.UHeapRef
11+
import org.usvm.UIndexType
12+
import org.usvm.USizeExpr
13+
import org.usvm.USizeSort
14+
import org.usvm.USort
15+
import org.usvm.sampleUValue
16+
import org.usvm.uctx
417
import org.usvm.util.SetRegion
518
import org.usvm.util.emptyRegionTree
619

720
//region Memory region
821

922

10-
interface UMemoryRegion<Key, Sort : USort> {
23+
interface UReadOnlyMemoryRegion<Key, Sort : USort> {
1124
fun read(key: Key): UExpr<Sort>
25+
}
26+
27+
28+
interface UMemoryRegion<Key, Sort : USort> : UReadOnlyMemoryRegion<Key, Sort> {
1229
fun write(key: Key, value: UExpr<Sort>, guard: UBoolExpr): UMemoryRegion<Key, Sort>
1330
}
1431

‎usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
1-
package org.usvm
1+
package org.usvm.memory
22

3+
import org.usvm.UBoolExpr
4+
import org.usvm.UComposer
5+
import org.usvm.UExpr
6+
import org.usvm.USort
7+
import org.usvm.isFalse
38
import org.usvm.util.Region
49
import org.usvm.util.RegionTree
510
import org.usvm.util.emptyRegionTree

‎usvm-core/src/main/kotlin/org/usvm/RegionIds.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/RegionIds.kt

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,17 @@
1-
package org.usvm
1+
package org.usvm.memory
22

33
import org.ksmt.utils.asExpr
4+
import org.usvm.UBoolExpr
5+
import org.usvm.UComposer
6+
import org.usvm.UConcreteHeapAddress
7+
import org.usvm.UExpr
8+
import org.usvm.UExprTransformer
9+
import org.usvm.UHeapRef
10+
import org.usvm.USizeExpr
11+
import org.usvm.USizeSort
12+
import org.usvm.USort
13+
import org.usvm.isTrue
14+
import org.usvm.uctx
415

516
/**
617
* Represents any possible type of regions that can be used in the memory.

‎usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
1-
package org.usvm
1+
package org.usvm.memory
22

33
import org.ksmt.expr.KExpr
44
import org.ksmt.utils.asExpr
5+
import org.usvm.UContext
6+
import org.usvm.UExpr
7+
import org.usvm.USort
58
import java.util.Stack
69

710
interface URegistersStackEvaluator {

‎usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
1-
package org.usvm
2-
1+
package org.usvm.memory
2+
3+
import org.usvm.UBoolExpr
4+
import org.usvm.UComposer
5+
import org.usvm.UExpr
6+
import org.usvm.USizeExpr
7+
import org.usvm.USort
8+
import org.usvm.isTrue
39
import java.util.*
410

511
/**

‎usvm-core/src/main/kotlin/org/usvm/EagerModels.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/model/EagerModels.kt

Lines changed: 24 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,24 @@
1-
package org.usvm
1+
package org.usvm.model
22

33
import org.ksmt.utils.asExpr
44
import org.ksmt.utils.sampleValue
5+
import org.usvm.UBoolExpr
6+
import org.usvm.UConcreteHeapRef
7+
import org.usvm.UExpr
8+
import org.usvm.UHeapRef
9+
import org.usvm.UIndexedMethodReturnValue
10+
import org.usvm.UMockEvaluator
11+
import org.usvm.UMockSymbol
12+
import org.usvm.USizeExpr
13+
import org.usvm.USizeSort
14+
import org.usvm.USort
15+
import org.usvm.memory.UAddressCounter
16+
import org.usvm.memory.UMemoryRegion
17+
import org.usvm.memory.UReadOnlyMemoryRegion
18+
import org.usvm.memory.URegistersStackEvaluator
19+
import org.usvm.memory.USymbolicArrayIndex
20+
import org.usvm.memory.USymbolicHeap
21+
import org.usvm.uctx
522

623
/**
724
* An eager model for registers that stores mapping
@@ -52,9 +69,9 @@ class UIndexedMockEagerModel<Method>(
5269
*/
5370
class UHeapEagerModel<Field, ArrayType>(
5471
private val nullRef: UConcreteHeapRef,
55-
private val resolvedInputFields: Map<Field, UMemoryRegion<UHeapRef, out USort>>,
56-
private val resolvedInputArrays: Map<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>,
57-
private val resolvedInputLengths: Map<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>,
72+
private val resolvedInputFields: Map<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>,
73+
private val resolvedInputArrays: Map<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>,
74+
private val resolvedInputLengths: Map<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>,
5875
) : USymbolicHeap<Field, ArrayType> {
5976
override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
6077
// All the expressions in the model are interpreted, therefore, they must
@@ -66,7 +83,7 @@ class UHeapEagerModel<Field, ArrayType>(
6683
val region = resolvedInputFields.getOrElse(field) {
6784
// sampleValue here is important
6885
UMemory1DArray(sort.sampleValue().nullAddress(nullRef))
69-
} as UMemoryRegion<UHeapRef, Sort>
86+
} as UReadOnlyMemoryRegion<UHeapRef, Sort>
7087

7188
return region.read(ref)
7289
}
@@ -88,7 +105,7 @@ class UHeapEagerModel<Field, ArrayType>(
88105
val region = resolvedInputArrays.getOrElse(arrayType) {
89106
// sampleValue here is important
90107
UMemory2DArray(sort.sampleValue().nullAddress(nullRef))
91-
} as UMemoryRegion<USymbolicArrayIndex, Sort>
108+
} as UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>
92109

93110
return region.read(key)
94111
}
@@ -99,7 +116,7 @@ class UHeapEagerModel<Field, ArrayType>(
99116
// which have addresses less or equal than INITIAL_INPUT_ADDRESS
100117
require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS)
101118

102-
val region = resolvedInputLengths.getOrElse<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
119+
val region = resolvedInputLengths.getOrElse<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
103120
// sampleValue here is important
104121
UMemory1DArray(ref.uctx.sizeSort.sampleValue())
105122
}

‎usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,22 @@
1-
package org.usvm
1+
package org.usvm.model
22

33
import org.ksmt.expr.KExpr
44
import org.ksmt.solver.KModel
55
import org.ksmt.sort.KUninterpretedSort
6-
import org.usvm.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
7-
import org.usvm.UAddressCounter.Companion.NULL_ADDRESS
6+
import org.usvm.UAddressSort
7+
import org.usvm.UConcreteHeapRef
8+
import org.usvm.UContext
9+
import org.usvm.UExpr
10+
import org.usvm.solver.UExprTranslator
11+
import org.usvm.UHeapRef
12+
import org.usvm.USort
13+
import org.usvm.solver.UTrackingExprTranslator
14+
import org.usvm.UTypeModel
15+
import org.usvm.memory.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
16+
import org.usvm.memory.UAddressCounter.Companion.NULL_ADDRESS
17+
import org.usvm.memory.UMemoryBase
18+
import org.usvm.memory.URegionId
19+
import org.usvm.uctx
820

921
interface UModelDecoder<Memory, Model> {
1022
fun decode(memory: Memory, model: KModel): Model

‎usvm-core/src/main/kotlin/org/usvm/LazyModels.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt

Lines changed: 26 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,32 @@
1-
package org.usvm
1+
package org.usvm.model
22

33
import org.ksmt.expr.KExpr
44
import org.ksmt.solver.KModel
55
import org.ksmt.utils.asExpr
66
import org.ksmt.utils.cast
77
import org.ksmt.utils.sampleValue
8+
import org.usvm.UAddressSort
9+
import org.usvm.UBoolExpr
10+
import org.usvm.UConcreteHeapRef
11+
import org.usvm.UExpr
12+
import org.usvm.UHeapRef
13+
import org.usvm.UIndexedMethodReturnValue
14+
import org.usvm.UMockEvaluator
15+
import org.usvm.UMockSymbol
16+
import org.usvm.USizeExpr
17+
import org.usvm.USizeSort
18+
import org.usvm.USort
19+
import org.usvm.memory.UAddressCounter
20+
import org.usvm.memory.UInputArrayId
21+
import org.usvm.memory.UInputArrayLengthId
22+
import org.usvm.memory.UInputFieldId
23+
import org.usvm.memory.UMemoryRegion
24+
import org.usvm.memory.UReadOnlyMemoryRegion
25+
import org.usvm.memory.URegionId
26+
import org.usvm.memory.URegistersStackEvaluator
27+
import org.usvm.memory.USymbolicArrayIndex
28+
import org.usvm.memory.USymbolicHeap
29+
import org.usvm.uctx
830

931

1032
/**
@@ -84,9 +106,9 @@ class ULazyHeapModel<Field, ArrayType>(
84106
private val addressesMapping: AddressesMapping,
85107
private val regionIdToInitialValue: Map<URegionId<*, *, *>, KExpr<*>>,
86108
) : USymbolicHeap<Field, ArrayType> {
87-
private val resolvedInputFields = mutableMapOf<Field, UMemoryRegion<UHeapRef, out USort>>()
88-
private val resolvedInputArrays = mutableMapOf<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>()
89-
private val resolvedInputLengths = mutableMapOf<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>()
109+
private val resolvedInputFields = mutableMapOf<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>()
110+
private val resolvedInputArrays = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>()
111+
private val resolvedInputLengths = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>()
90112
override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
91113
// All the expressions in the model are interpreted, therefore, they must
92114
// have concrete addresses. Moreover, the model knows only about input values

‎usvm-core/src/main/kotlin/org/usvm/Model.kt renamed to ‎usvm-core/src/main/kotlin/org/usvm/model/Model.kt

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,12 @@
1-
package org.usvm
1+
package org.usvm.model
2+
3+
import org.usvm.UComposer
4+
import org.usvm.UContext
5+
import org.usvm.UExpr
6+
import org.usvm.UMockEvaluator
7+
import org.usvm.USort
8+
import org.usvm.UTypeModel
9+
import org.usvm.memory.UReadOnlySymbolicHeap
210

311
interface UModel {
412
fun <Sort: USort> eval(expr: UExpr<Sort>): UExpr<Sort>

0 commit comments

Comments
 (0)