Skip to content

Restructure packages #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 25, 2023
Merged

Restructure packages #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3a2b05e
Restructure packages
sergeypospelov Apr 25, 2023
ee33cfd
Fix: RE in tests
sergeypospelov Apr 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/Composition.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
package org.usvm

import org.usvm.memory.UReadOnlySymbolicHeap
import org.usvm.memory.URegionId
import org.usvm.memory.URegistersStackEvaluator

@Suppress("MemberVisibilityCanBePrivate")
open class UComposer<Field, Type>(
ctx: UContext,
Expand Down
5 changes: 5 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/Context.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,11 @@ import org.ksmt.sort.KUninterpretedSort
import org.ksmt.utils.DefaultValueSampler
import org.ksmt.utils.asExpr
import org.ksmt.utils.cast
import org.usvm.memory.UAllocatedArrayRegion
import org.usvm.memory.UInputArrayLengthRegion
import org.usvm.memory.UInputArrayRegion
import org.usvm.memory.UInputFieldRegion
import org.usvm.memory.splitUHeapRef

@Suppress("LeakingThis")
open class UContext(
Expand Down
11 changes: 11 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/Expressions.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,17 @@ import org.ksmt.expr.*
import org.ksmt.expr.printer.ExpressionPrinter
import org.ksmt.expr.transformer.KTransformerBase
import org.ksmt.sort.*
import org.usvm.memory.UAllocatedArrayId
import org.usvm.memory.UAllocatedArrayRegion
import org.usvm.memory.UInputArrayId
import org.usvm.memory.UInputArrayLengthId
import org.usvm.memory.UInputArrayLengthRegion
import org.usvm.memory.UInputArrayRegion
import org.usvm.memory.UInputFieldId
import org.usvm.memory.UInputFieldRegion
import org.usvm.memory.URegionId
import org.usvm.memory.USymbolicArrayIndex
import org.usvm.memory.USymbolicMemoryRegion

//region KSMT aliases

Expand Down
2 changes: 2 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/Merging.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package org.usvm

import org.usvm.memory.URegionHeap

interface UMerger<Entity> {
/**
* @returns Merged entity or null if [left] and [right] are non-mergeable
Expand Down
2 changes: 2 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/State.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ package org.usvm

import kotlinx.collections.immutable.PersistentList
import org.ksmt.expr.KInterpretedValue
import org.usvm.memory.UMemoryBase
import org.usvm.model.UModel

abstract class UState<Type, Field, Method, Statement>(
// TODO: add interpreter-specific information
Expand Down
11 changes: 10 additions & 1 deletion usvm-core/src/main/kotlin/org/usvm/Heap.kt → ...e/src/main/kotlin/org/usvm/memory/Heap.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,17 @@
package org.usvm
package org.usvm.memory

import kotlinx.collections.immutable.PersistentMap
import kotlinx.collections.immutable.persistentMapOf
import org.ksmt.utils.asExpr
import org.usvm.UBoolExpr
import org.usvm.UConcreteHeapAddress
import org.usvm.UConcreteHeapRef
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.USizeExpr
import org.usvm.USort
import org.usvm.sampleUValue

interface UReadOnlyHeap<Ref, Value, SizeT, Field, ArrayType, Guard> {
fun <Sort : USort> readField(ref: Ref, field: Field, sort: Sort): Value
Expand Down
12 changes: 11 additions & 1 deletion .../main/kotlin/org/usvm/HeapRefSplitting.kt → ...otlin/org/usvm/memory/HeapRefSplitting.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,14 @@
package org.usvm
package org.usvm.memory

import org.usvm.UAddressSort
import org.usvm.UBoolExpr
import org.usvm.UConcreteHeapRef
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.UIteExpr
import org.usvm.USort
import org.usvm.USymbolicHeapRef
import org.usvm.isFalse

data class GuardedExpr<out T>(
val expr: T,
Expand Down
16 changes: 15 additions & 1 deletion usvm-core/src/main/kotlin/org/usvm/Memory.kt → ...src/main/kotlin/org/usvm/memory/Memory.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,20 @@
package org.usvm
package org.usvm.memory

import org.ksmt.utils.asExpr
import org.usvm.UArrayIndexRef
import org.usvm.UComposer
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.UFieldRef
import org.usvm.UHeapRef
import org.usvm.UIndexedMocker
import org.usvm.ULValue
import org.usvm.UMocker
import org.usvm.URegisterRef
import org.usvm.USizeExpr
import org.usvm.USort
import org.usvm.UTypeStorage
import org.usvm.UTypeSystem

interface UMemory<LValue, RValue, SizeT, HeapRef, Type> {
/**
Expand Down
21 changes: 19 additions & 2 deletions ...src/main/kotlin/org/usvm/MemoryRegions.kt → ...n/kotlin/org/usvm/memory/MemoryRegions.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,31 @@
package org.usvm
package org.usvm.memory

import org.ksmt.utils.asExpr
import org.usvm.UBoolExpr
import org.usvm.UComposer
import org.usvm.UConcreteHeapAddress
import org.usvm.UConcreteHeapRef
import org.usvm.UConcreteSize
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.UIndexType
import org.usvm.USizeExpr
import org.usvm.USizeSort
import org.usvm.USort
import org.usvm.sampleUValue
import org.usvm.uctx
import org.usvm.util.SetRegion
import org.usvm.util.emptyRegionTree

//region Memory region


interface UMemoryRegion<Key, Sort : USort> {
interface UReadOnlyMemoryRegion<Key, Sort : USort> {
fun read(key: Key): UExpr<Sort>
}


interface UMemoryRegion<Key, Sort : USort> : UReadOnlyMemoryRegion<Key, Sort> {
fun write(key: Key, value: UExpr<Sort>, guard: UBoolExpr): UMemoryRegion<Key, Sort>
}

Expand Down
7 changes: 6 additions & 1 deletion ...src/main/kotlin/org/usvm/MemoryUpdates.kt → ...n/kotlin/org/usvm/memory/MemoryUpdates.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
package org.usvm
package org.usvm.memory

import org.usvm.UBoolExpr
import org.usvm.UComposer
import org.usvm.UExpr
import org.usvm.USort
import org.usvm.isFalse
import org.usvm.util.Region
import org.usvm.util.RegionTree
import org.usvm.util.emptyRegionTree
Expand Down
13 changes: 12 additions & 1 deletion ...ore/src/main/kotlin/org/usvm/RegionIds.kt → .../main/kotlin/org/usvm/memory/RegionIds.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,17 @@
package org.usvm
package org.usvm.memory

import org.ksmt.utils.asExpr
import org.usvm.UBoolExpr
import org.usvm.UComposer
import org.usvm.UConcreteHeapAddress
import org.usvm.UExpr
import org.usvm.UExprTransformer
import org.usvm.UHeapRef
import org.usvm.USizeExpr
import org.usvm.USizeSort
import org.usvm.USort
import org.usvm.isTrue
import org.usvm.uctx

/**
* Represents any possible type of regions that can be used in the memory.
Expand Down
5 changes: 4 additions & 1 deletion ...rc/main/kotlin/org/usvm/RegistersStack.kt → .../kotlin/org/usvm/memory/RegistersStack.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
package org.usvm
package org.usvm.memory

import org.ksmt.expr.KExpr
import org.ksmt.utils.asExpr
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.USort
import java.util.Stack

interface URegistersStackEvaluator {
Expand Down
10 changes: 8 additions & 2 deletions ...e/src/main/kotlin/org/usvm/UpdateNodes.kt → ...ain/kotlin/org/usvm/memory/UpdateNodes.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@
package org.usvm

package org.usvm.memory

import org.usvm.UBoolExpr
import org.usvm.UComposer
import org.usvm.UExpr
import org.usvm.USizeExpr
import org.usvm.USort
import org.usvm.isTrue
import java.util.*

/**
Expand Down
31 changes: 24 additions & 7 deletions ...e/src/main/kotlin/org/usvm/EagerModels.kt → ...main/kotlin/org/usvm/model/EagerModels.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,24 @@
package org.usvm
package org.usvm.model

import org.ksmt.utils.asExpr
import org.ksmt.utils.sampleValue
import org.usvm.UBoolExpr
import org.usvm.UConcreteHeapRef
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.UIndexedMethodReturnValue
import org.usvm.UMockEvaluator
import org.usvm.UMockSymbol
import org.usvm.USizeExpr
import org.usvm.USizeSort
import org.usvm.USort
import org.usvm.memory.UAddressCounter
import org.usvm.memory.UMemoryRegion
import org.usvm.memory.UReadOnlyMemoryRegion
import org.usvm.memory.URegistersStackEvaluator
import org.usvm.memory.USymbolicArrayIndex
import org.usvm.memory.USymbolicHeap
import org.usvm.uctx

/**
* An eager model for registers that stores mapping
Expand Down Expand Up @@ -52,9 +69,9 @@ class UIndexedMockEagerModel<Method>(
*/
class UHeapEagerModel<Field, ArrayType>(
private val nullRef: UConcreteHeapRef,
private val resolvedInputFields: Map<Field, UMemoryRegion<UHeapRef, out USort>>,
private val resolvedInputArrays: Map<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>,
private val resolvedInputLengths: Map<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>,
private val resolvedInputFields: Map<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>,
private val resolvedInputArrays: Map<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>,
private val resolvedInputLengths: Map<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>,
) : USymbolicHeap<Field, ArrayType> {
override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
// All the expressions in the model are interpreted, therefore, they must
Expand All @@ -66,7 +83,7 @@ class UHeapEagerModel<Field, ArrayType>(
val region = resolvedInputFields.getOrElse(field) {
// sampleValue here is important
UMemory1DArray(sort.sampleValue().nullAddress(nullRef))
} as UMemoryRegion<UHeapRef, Sort>
} as UReadOnlyMemoryRegion<UHeapRef, Sort>

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

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

val region = resolvedInputLengths.getOrElse<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
val region = resolvedInputLengths.getOrElse<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
// sampleValue here is important
UMemory1DArray(ref.uctx.sizeSort.sampleValue())
}
Expand Down
18 changes: 15 additions & 3 deletions .../main/kotlin/org/usvm/LazyModelDecoder.kt → ...kotlin/org/usvm/model/LazyModelDecoder.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,22 @@
package org.usvm
package org.usvm.model

import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.sort.KUninterpretedSort
import org.usvm.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
import org.usvm.UAddressCounter.Companion.NULL_ADDRESS
import org.usvm.UAddressSort
import org.usvm.UConcreteHeapRef
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.solver.UExprTranslator
import org.usvm.UHeapRef
import org.usvm.USort
import org.usvm.solver.UTrackingExprTranslator
import org.usvm.UTypeModel
import org.usvm.memory.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
import org.usvm.memory.UAddressCounter.Companion.NULL_ADDRESS
import org.usvm.memory.UMemoryBase
import org.usvm.memory.URegionId
import org.usvm.uctx

interface UModelDecoder<Memory, Model> {
fun decode(memory: Memory, model: KModel): Model
Expand Down
30 changes: 26 additions & 4 deletions ...re/src/main/kotlin/org/usvm/LazyModels.kt → .../main/kotlin/org/usvm/model/LazyModels.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,32 @@
package org.usvm
package org.usvm.model

import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.utils.asExpr
import org.ksmt.utils.cast
import org.ksmt.utils.sampleValue
import org.usvm.UAddressSort
import org.usvm.UBoolExpr
import org.usvm.UConcreteHeapRef
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.UIndexedMethodReturnValue
import org.usvm.UMockEvaluator
import org.usvm.UMockSymbol
import org.usvm.USizeExpr
import org.usvm.USizeSort
import org.usvm.USort
import org.usvm.memory.UAddressCounter
import org.usvm.memory.UInputArrayId
import org.usvm.memory.UInputArrayLengthId
import org.usvm.memory.UInputFieldId
import org.usvm.memory.UMemoryRegion
import org.usvm.memory.UReadOnlyMemoryRegion
import org.usvm.memory.URegionId
import org.usvm.memory.URegistersStackEvaluator
import org.usvm.memory.USymbolicArrayIndex
import org.usvm.memory.USymbolicHeap
import org.usvm.uctx


/**
Expand Down Expand Up @@ -84,9 +106,9 @@ class ULazyHeapModel<Field, ArrayType>(
private val addressesMapping: AddressesMapping,
private val regionIdToInitialValue: Map<URegionId<*, *, *>, KExpr<*>>,
) : USymbolicHeap<Field, ArrayType> {
private val resolvedInputFields = mutableMapOf<Field, UMemoryRegion<UHeapRef, out USort>>()
private val resolvedInputArrays = mutableMapOf<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>()
private val resolvedInputLengths = mutableMapOf<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>()
private val resolvedInputFields = mutableMapOf<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>()
private val resolvedInputArrays = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>()
private val resolvedInputLengths = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>()
override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
// All the expressions in the model are interpreted, therefore, they must
// have concrete addresses. Moreover, the model knows only about input values
Expand Down
10 changes: 9 additions & 1 deletion usvm-core/src/main/kotlin/org/usvm/Model.kt → ...e/src/main/kotlin/org/usvm/model/Model.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,12 @@
package org.usvm
package org.usvm.model

import org.usvm.UComposer
import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.UMockEvaluator
import org.usvm.USort
import org.usvm.UTypeModel
import org.usvm.memory.UReadOnlySymbolicHeap

interface UModel {
fun <Sort: USort> eval(expr: UExpr<Sort>): UExpr<Sort>
Expand Down
Loading