Skip to content

Commit 76ddc87

Browse files
DamtevDamtev
authored
Introduced static refs, supported enums (#61)
1 parent 956cdd3 commit 76ddc87

61 files changed

Lines changed: 1400 additions & 452 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

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

Lines changed: 44 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -114,38 +114,54 @@ open class UContext(
114114
}
115115

116116
fun mkHeapRefEq(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr =
117-
when {
118-
// fast checks
119-
lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
120-
lhs is UConcreteHeapRef && rhs is UConcreteHeapRef -> mkBool(lhs == rhs)
117+
mkHeapEqWithFastChecks(lhs, rhs) {
121118
// unfolding
122-
else -> {
123-
val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
124-
val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
125-
126-
val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
127-
128-
val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
129-
130-
concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
131-
val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
132-
// mkAnd instead of mkAnd with flat=false here is OK
133-
val conjunct = mkAnd(guardLhs, guardRhs)
134-
conjuncts += conjunct
135-
}
136-
137-
if (symbolicRefLhs != null && symbolicRefRhs != null) {
138-
val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
139-
// mkAnd instead of mkAnd with flat=false here is OK
140-
val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
141-
conjuncts += conjunct
142-
}
143-
144-
// it's safe to use mkOr here
145-
mkOr(conjuncts)
119+
val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
120+
val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
121+
122+
val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
123+
124+
val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
125+
126+
concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
127+
val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
128+
// mkAnd instead of mkAnd with flat=false here is OK
129+
val conjunct = mkAnd(guardLhs, guardRhs)
130+
conjuncts += conjunct
146131
}
132+
133+
if (symbolicRefLhs != null && symbolicRefRhs != null) {
134+
val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
135+
// mkAnd instead of mkAnd with flat=false here is OK
136+
val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
137+
conjuncts += conjunct
138+
}
139+
140+
// it's safe to use mkOr here
141+
mkOr(conjuncts)
147142
}
148143

144+
private inline fun mkHeapEqWithFastChecks(
145+
lhs: UHeapRef,
146+
rhs: UHeapRef,
147+
blockOnFailedFastChecks: () -> UBoolExpr,
148+
): UBoolExpr = when {
149+
lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
150+
isAllocatedConcreteHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> mkBool(lhs == rhs)
151+
isStaticHeapRef(lhs) && isStaticHeapRef(rhs) -> mkBool(lhs == rhs)
152+
153+
isAllocatedConcreteHeapRef(lhs) && isStaticHeapRef(rhs) -> falseExpr
154+
isStaticHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> falseExpr
155+
156+
isStaticHeapRef(lhs) && rhs is UNullRef -> falseExpr
157+
lhs is UNullRef && isStaticHeapRef(rhs) -> falseExpr
158+
159+
lhs is USymbolicHeapRef && isStaticHeapRef(rhs) -> super.mkEq(lhs, rhs, order = true)
160+
isStaticHeapRef(lhs) && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
161+
162+
else -> blockOnFailedFastChecks()
163+
}
164+
149165
private val uConcreteHeapRefCache = mkAstInterner<UConcreteHeapRef>()
150166
fun mkConcreteHeapRef(address: UConcreteHeapAddress): UConcreteHeapRef =
151167
uConcreteHeapRefCache.createIfContextActive {

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

Lines changed: 41 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ import io.ksmt.sort.KSort
2626
import io.ksmt.sort.KUninterpretedSort
2727
import org.usvm.memory.USymbolicCollection
2828
import org.usvm.memory.USymbolicCollectionId
29+
import kotlin.contracts.ExperimentalContracts
30+
import kotlin.contracts.contract
2931

3032
//region KSMT aliases
3133

@@ -76,8 +78,35 @@ typealias UHeapRef = UExpr<UAddressSort>
7678
typealias USymbolicHeapRef = USymbol<UAddressSort>
7779
typealias UConcreteHeapAddress = Int
7880

79-
fun isSymbolicHeapRef(expr: UExpr<*>) =
80-
expr.sort == expr.uctx.addressSort && expr is USymbol<*>
81+
@OptIn(ExperimentalContracts::class)
82+
fun isSymbolicHeapRef(expr: UExpr<*>): Boolean {
83+
contract {
84+
returns(true) implies (expr is USymbol<*>)
85+
}
86+
87+
return expr.sort == expr.uctx.addressSort && expr is USymbol<*>
88+
}
89+
90+
@OptIn(ExperimentalContracts::class)
91+
fun isAllocatedConcreteHeapRef(expr: UExpr<*>): Boolean {
92+
contract {
93+
returns(true) implies (expr is UConcreteHeapRef)
94+
}
95+
96+
return expr is UConcreteHeapRef && expr.isAllocated
97+
}
98+
99+
@OptIn(ExperimentalContracts::class)
100+
fun isStaticHeapRef(expr: UExpr<*>): Boolean {
101+
contract {
102+
returns(true) implies (expr is UConcreteHeapRef)
103+
}
104+
105+
return expr is UConcreteHeapRef && expr.isStatic
106+
}
107+
108+
val UConcreteHeapRef.isAllocated: Boolean get() = address >= INITIAL_CONCRETE_ADDRESS
109+
val UConcreteHeapRef.isStatic: Boolean get() = address <= INITIAL_STATIC_ADDRESS
81110

82111
class UConcreteHeapRefDecl internal constructor(
83112
ctx: UContext,
@@ -129,8 +158,9 @@ class UNullRef internal constructor(
129158
}
130159
}
131160

132-
// We split all addresses into three parts:
133-
// * input values: [Int.MIN_VALUE..0),
161+
// We split all addresses into four parts:
162+
// * static values (represented as allocated but interpreted as input): [Int.MIN_VALUE..INITIAL_STATIC_ADDRESS]
163+
// * input values: (INITIAL_STATIC_ADDRESS..0),
134164
// * null value: [0]
135165
// * allocated values: (0..[Int.MAX_VALUE]
136166

@@ -147,10 +177,16 @@ const val INITIAL_INPUT_ADDRESS = NULL_ADDRESS - 1
147177

148178
/**
149179
* A constant corresponding to the first allocated address in any symbolic memory.
150-
* Input addresses takes this semi-interval: (0..[Int.MAX_VALUE])
180+
* Allocated addresses takes this semi-interval: (0..[Int.MAX_VALUE])
151181
*/
152182
const val INITIAL_CONCRETE_ADDRESS = NULL_ADDRESS + 1
153183

184+
/**
185+
* A constant corresponding to the first static address in any symbolic memory.
186+
* Static addresses takes this segment: [[Int.MIN_VALUE]..[INITIAL_STATIC_ADDRESS]]
187+
*/
188+
const val INITIAL_STATIC_ADDRESS = -(1 shl 20) // Use value not less than UNINTERPRETED_SORT_MIN_ALLOWED_VALUE in ksmt
189+
154190

155191
//endregion
156192

‎usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@ import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitia
2222
fun <Type> UReadOnlyMemory<Type>.typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
2323
types.getTypeStream(ref)
2424

25-
fun UMemory<*, *>.allocate() = ctx.mkConcreteHeapRef(addressCounter.freshAddress())
25+
fun UMemory<*, *>.allocateConcreteRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshAllocatedAddress())
26+
fun UMemory<*, *>.allocateStaticRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshStaticAddress())
2627

2728
fun <Field, Sort : USort> UReadOnlyMemory<*>.readField(
2829
ref: UHeapRef, field: Field, sort: Sort

‎usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,14 @@ import org.usvm.api.readArrayIndex
1111
import org.usvm.api.readArrayLength
1212
import org.usvm.api.writeArrayIndex
1313
import org.usvm.api.writeArrayLength
14-
import org.usvm.memory.map
14+
import org.usvm.memory.mapWithStaticAsConcrete
1515
import org.usvm.uctx
1616

1717
object ListCollectionApi {
1818
fun <ListType> UState<ListType, *, *, *, *, *>.mkSymbolicList(
1919
listType: ListType,
2020
): UHeapRef = with(memory.ctx) {
21-
val ref = memory.alloc(listType)
21+
val ref = memory.allocConcrete(listType)
2222
memory.writeArrayLength(ref, mkSizeExpr(0), listType)
2323
ref
2424
}
@@ -36,7 +36,7 @@ object ListCollectionApi {
3636
listRef: UHeapRef,
3737
listType: ListType,
3838
): Unit? {
39-
listRef.map(
39+
listRef.mapWithStaticAsConcrete(
4040
concreteMapper = {
4141
// Concrete list size is always correct
4242
it

‎usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,14 +13,14 @@ import org.usvm.collection.map.ref.refMapMerge
1313
import org.usvm.collection.set.ref.URefSetEntryLValue
1414
import org.usvm.collection.set.ref.URefSetRegionId
1515
import org.usvm.collection.set.ref.refSetUnion
16-
import org.usvm.memory.map
16+
import org.usvm.memory.mapWithStaticAsConcrete
1717
import org.usvm.uctx
1818

1919
object ObjectMapCollectionApi {
2020
fun <MapType> UState<MapType, *, *, *, *, *>.mkSymbolicObjectMap(
2121
mapType: MapType,
2222
): UHeapRef = with(memory.ctx) {
23-
val ref = memory.alloc(mapType)
23+
val ref = memory.allocConcrete(mapType)
2424
val length = UMapLengthLValue(ref, mapType)
2525
memory.write(length, mkSizeExpr(0), trueExpr)
2626
ref
@@ -40,7 +40,7 @@ object ObjectMapCollectionApi {
4040
mapRef: UHeapRef,
4141
mapType: MapType,
4242
): Unit? {
43-
mapRef.map(
43+
mapRef.mapWithStaticAsConcrete(
4444
concreteMapper = {
4545
// Concrete map size is always correct
4646
it

‎usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt‎

Lines changed: 21 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ import org.usvm.memory.ULValue
1212
import org.usvm.memory.UMemoryRegion
1313
import org.usvm.memory.UMemoryRegionId
1414
import org.usvm.memory.USymbolicCollection
15-
import org.usvm.memory.foldHeapRef
1615
import org.usvm.memory.foldHeapRef2
16+
import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
1717
import org.usvm.memory.key.USizeExprKeyInfo
18-
import org.usvm.memory.map
18+
import org.usvm.memory.mapWithStaticAsSymbolic
1919

2020
data class UArrayIndexLValue<ArrayType, Sort : USort>(
2121
override val sort: Sort,
@@ -92,32 +92,30 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort>(
9292
private fun updateInput(updated: UInputArray<ArrayType, Sort>) =
9393
UArrayMemoryRegion(allocatedArrays, updated)
9494

95-
override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> =
96-
key.ref.map(
97-
{ concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
98-
{ symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
99-
)
95+
override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
96+
concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
97+
symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
98+
)
10099

101100
override fun write(
102101
key: UArrayIndexLValue<ArrayType, Sort>,
103102
value: UExpr<Sort>,
104103
guard: UBoolExpr
105-
): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> =
106-
foldHeapRef(
107-
key.ref,
108-
initial = this,
109-
initialGuard = guard,
110-
blockOnConcrete = { region, (concreteRef, innerGuard) ->
111-
val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
112-
val newRegion = oldRegion.write(key.index, value, innerGuard)
113-
region.updateAllocatedArray(concreteRef.address, newRegion)
114-
},
115-
blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
116-
val oldRegion = region.getInputArray(key.arrayType, key.sort)
117-
val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
118-
region.updateInput(newRegion)
119-
}
120-
)
104+
): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
105+
key.ref,
106+
initial = this,
107+
initialGuard = guard,
108+
blockOnConcrete = { region, (concreteRef, innerGuard) ->
109+
val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
110+
val newRegion = oldRegion.write(key.index, value, innerGuard)
111+
region.updateAllocatedArray(concreteRef.address, newRegion)
112+
},
113+
blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
114+
val oldRegion = region.getInputArray(key.arrayType, key.sort)
115+
val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
116+
region.updateInput(newRegion)
117+
}
118+
)
121119

122120
override fun memcpy(
123121
srcRef: UHeapRef,

‎usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ internal fun <ArrayType> UWritableMemory<ArrayType>.allocateArray(
6060
type: ArrayType,
6161
length: USizeExpr
6262
): UConcreteHeapRef {
63-
val address = alloc(type)
63+
val address = allocConcrete(type)
6464

6565
val lengthRegionRef = UArrayLengthLValue(address, type)
6666
write(lengthRegionRef, length, guard = length.uctx.trueExpr)

‎usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
1111
import org.usvm.memory.UMemoryRegion
1212
import org.usvm.memory.UMemoryRegionId
1313
import org.usvm.memory.USymbolicCollection
14-
import org.usvm.memory.foldHeapRef
14+
import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
1515
import org.usvm.memory.guardedWrite
16-
import org.usvm.memory.map
16+
import org.usvm.memory.mapWithStaticAsSymbolic
1717
import org.usvm.sampleUValue
1818
import org.usvm.uctx
1919

@@ -60,17 +60,16 @@ internal class UArrayLengthsMemoryRegion<ArrayType>(
6060
private fun updatedInput(updated: UInputArrayLengths<ArrayType>) =
6161
UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated)
6262

63-
override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr =
64-
key.ref.map(
65-
{ concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
66-
{ symbolicRef -> getInputLength(key).read(symbolicRef) }
67-
)
63+
override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr = key.ref.mapWithStaticAsSymbolic(
64+
concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
65+
symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
66+
)
6867

6968
override fun write(
7069
key: UArrayLengthLValue<ArrayType>,
7170
value: USizeExpr,
7271
guard: UBoolExpr
73-
) = foldHeapRef(
72+
) = foldHeapRefWithStaticAsSymbolic(
7473
key.ref,
7574
initial = this,
7675
initialGuard = guard,

‎usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt‎

Lines changed: 21 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
1111
import org.usvm.memory.UMemoryRegion
1212
import org.usvm.memory.UMemoryRegionId
1313
import org.usvm.memory.USymbolicCollection
14-
import org.usvm.memory.foldHeapRef
14+
import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
1515
import org.usvm.memory.guardedWrite
16-
import org.usvm.memory.map
16+
import org.usvm.memory.mapWithStaticAsSymbolic
1717
import org.usvm.sampleUValue
1818

1919
data class UFieldLValue<Field, Sort : USort>(override val sort: Sort, val ref: UHeapRef, val field: Field) :
@@ -55,31 +55,29 @@ internal class UFieldsMemoryRegion<Field, Sort : USort>(
5555
private fun updateInput(updated: UInputFields<Field, Sort>) =
5656
UFieldsMemoryRegion(sort, field, allocatedFields, updated)
5757

58-
override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> =
59-
key.ref.map(
60-
{ concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
61-
{ symbolicRef -> getInputFields(key).read(symbolicRef) }
62-
)
58+
override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
59+
concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
60+
symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef) }
61+
)
6362

6463
override fun write(
6564
key: UFieldLValue<Field, Sort>,
6665
value: UExpr<Sort>,
6766
guard: UBoolExpr
68-
): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> =
69-
foldHeapRef(
70-
key.ref,
71-
initial = this,
72-
initialGuard = guard,
73-
blockOnConcrete = { region, (concreteRef, innerGuard) ->
74-
val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
75-
sort.sampleUValue()
76-
}
77-
region.updateAllocated(newRegion)
78-
},
79-
blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
80-
val oldRegion = region.getInputFields(key)
81-
val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
82-
region.updateInput(newRegion)
67+
): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
68+
key.ref,
69+
initial = this,
70+
initialGuard = guard,
71+
blockOnConcrete = { region, (concreteRef, innerGuard) ->
72+
val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
73+
sort.sampleUValue()
8374
}
84-
)
75+
region.updateAllocated(newRegion)
76+
},
77+
blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
78+
val oldRegion = region.getInputFields(key)
79+
val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
80+
region.updateInput(newRegion)
81+
}
82+
)
8583
}

0 commit comments

Comments
 (0)