Skip to content

Commit 5f9d9b2

Browse files
sergeypospelovsergeypospelov
authored
Restructure packages (#13)
1 parent 5a330c5 commit 5f9d9b2

36 files changed

Lines changed: 359 additions & 83 deletions

‎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

0 commit comments

Comments
 (0)