Skip to content

Commit 7209949

Browse files
sergeypospelovsergeypospelov
committed
Fix review comments
1 parent cf0bc7f commit 7209949

File tree

11 files changed

+123
-73
lines changed

11 files changed

+123
-73
lines changed

‎usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt

Lines changed: 19 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -1,60 +1,27 @@
11
package org.usvm.constraints
22

3-
import org.usvm.INITIAL_CONCRETE_ADDRESS
4-
import org.usvm.INITIAL_INPUT_ADDRESS
53
import org.usvm.NULL_ADDRESS
64
import org.usvm.UBoolExpr
75
import org.usvm.UConcreteHeapAddress
86
import org.usvm.UConcreteHeapRef
97
import org.usvm.UHeapRef
108
import org.usvm.UNullRef
119
import org.usvm.memory.map
12-
import org.usvm.types.UTypeSystem
1310
import org.usvm.model.UModel
11+
import org.usvm.model.UTypeModel
1412
import org.usvm.solver.USatResult
1513
import org.usvm.solver.USolverResult
1614
import org.usvm.solver.UUnsatResult
1715
import org.usvm.types.USingleTypeStream
1816
import org.usvm.types.UTypeRegion
1917
import org.usvm.types.UTypeStream
18+
import org.usvm.types.UTypeSystem
2019
import org.usvm.uctx
2120

2221
interface UTypeEvaluator<Type> {
2322
fun evalIs(ref: UHeapRef, type: Type): UBoolExpr
2423
}
2524

26-
class UTypeModel<Type>(
27-
val typeSystem: UTypeSystem<Type>,
28-
typeStreamByAddr: Map<UConcreteHeapAddress, UTypeStream<Type>>,
29-
) : UTypeEvaluator<Type> {
30-
private val typeStreamByAddr = typeStreamByAddr.toMutableMap()
31-
32-
fun typeStream(ref: UConcreteHeapRef): UTypeStream<Type> =
33-
typeStreamByAddr[ref.address] ?: typeSystem.topTypeStream()
34-
35-
override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr =
36-
when (ref) {
37-
is UConcreteHeapRef -> {
38-
if (ref.address == NULL_ADDRESS) {
39-
ref.ctx.trueExpr
40-
} else {
41-
require(ref.address <= INITIAL_INPUT_ADDRESS)
42-
43-
val evaluatedTypeStream = typeStream(ref)
44-
val typeStream = evaluatedTypeStream.filterBySupertype(type)
45-
if (!typeStream.isEmpty) {
46-
typeStreamByAddr[ref.address] = typeStream
47-
ref.ctx.trueExpr
48-
} else {
49-
ref.ctx.falseExpr
50-
}
51-
}
52-
}
53-
54-
else -> error("Expecting concrete ref, but got $ref")
55-
}
56-
}
57-
5825
/**
5926
* A mutable collection of type constraints. Represents a conjunction of constraints of four kinds:
6027
* 1. x <: T, i.e. object referenced in x inherits T (supertype constraints for x)
@@ -79,7 +46,7 @@ class UTypeConstraints<Type>(
7946
}
8047

8148
/**
82-
* Returns if current type and equality constraints are unsatisfiable (syntactically).
49+
* Returns true if the current type and equality constraints are unsatisfiable (syntactically).
8350
*/
8451
var isContradicting = false
8552
private set
@@ -117,16 +84,15 @@ class UTypeConstraints<Type>(
11784
*/
11885
fun addSupertype(ref: UHeapRef, type: Type) {
11986
when (ref) {
87+
is UNullRef -> return
88+
12089
is UConcreteHeapRef -> {
121-
require(ref.address >= INITIAL_CONCRETE_ADDRESS)
12290
val concreteType = concreteRefToType.getValue(ref.address)
12391
if (!typeSystem.isSupertype(type, concreteType)) {
12492
contradiction()
12593
}
12694
}
12795

128-
is UNullRef -> return
129-
13096
else -> {
13197
val constraints = this[ref]
13298
val newConstraints = constraints.addSupertype(type)
@@ -156,16 +122,15 @@ class UTypeConstraints<Type>(
156122
*/
157123
fun excludeSupertype(ref: UHeapRef, type: Type) {
158124
when (ref) {
125+
is UNullRef -> contradiction() // the [ref] can't be equal to null
126+
159127
is UConcreteHeapRef -> {
160-
require(ref.address >= INITIAL_CONCRETE_ADDRESS)
161128
val concreteType = concreteRefToType.getValue(ref.address)
162129
if (typeSystem.isSupertype(type, concreteType)) {
163130
contradiction()
164131
}
165132
}
166133

167-
is UNullRef -> contradiction() // the [ref] can't be equal to null
168-
169134
else -> {
170135
val constraints = this[ref]
171136
val newConstraints = constraints.excludeSupertype(type)
@@ -178,8 +143,7 @@ class UTypeConstraints<Type>(
178143
for ((key, value) in symbolicRefToTypeRegion.entries) {
179144
// TODO: cache intersections?
180145
if (key != ref && value.intersect(newConstraints).isEmpty) {
181-
// If we have two inputs of incomparable reference types, then they are either non equal,
182-
// or both nulls
146+
// If we have two inputs of incomparable reference types, then they are non equal
183147
equalityConstraints.makeNonEqual(ref, key)
184148
}
185149
}
@@ -195,7 +159,6 @@ class UTypeConstraints<Type>(
195159
internal fun readTypeStream(ref: UHeapRef): UTypeStream<Type> =
196160
when (ref) {
197161
is UConcreteHeapRef -> {
198-
require(ref.address >= INITIAL_CONCRETE_ADDRESS)
199162
val concreteType = concreteRefToType[ref.address]
200163
val typeStream = if (concreteType == null) {
201164
typeSystem.topTypeStream()
@@ -310,24 +273,25 @@ class UTypeConstraints<Type>(
310273
// to have the common type with [heapRef], therefore they can't be equal or
311274
// some of them equals null
312275
val disjunct = mutableListOf<UBoolExpr>()
313-
potentialConflictingRefs.mapTo(disjunct) { ref ->
314-
with(ref.uctx) { ref.neq(heapRef) }
315-
}
316-
potentialConflictingRefs.mapTo(disjunct) { ref ->
317-
with(ref.uctx) { ref.eq(nullRef) }
276+
with(heapRef.uctx) {
277+
// can't be equal to heapRef
278+
potentialConflictingRefs.mapTo(disjunct) { it.neq(heapRef) }
279+
// some of them is null
280+
potentialConflictingRefs.mapTo(disjunct) { it.eq(nullRef) }
281+
disjunct += heapRef.eq(nullRef)
318282
}
319283
bannedRefEqualities += heapRef.ctx.mkOr(disjunct)
320284

321285
// start a new group
322286
nextRegion = region
323287
potentialConflictingRefs.clear()
324288
potentialConflictingRefs.add(heapRef)
325-
} else if (nextRegion === region) {
289+
} else if (nextRegion == region) {
326290
// the current [heapRef] gives the same region as the potentialConflictingRefs, so it's better
327291
// to keep only the [heapRef] to minimize the disequalities amount in the result disjunction
328292
potentialConflictingRefs.clear()
329293
potentialConflictingRefs.add(heapRef)
330-
} else if (nextRegion !== currentRegion) {
294+
} else if (nextRegion != currentRegion) {
331295
// no conflict detected, but the current region became smaller
332296
potentialConflictingRefs.add(heapRef)
333297
}
@@ -354,9 +318,9 @@ class UTypeConstraints<Type>(
354318
// because if the cluster is bigger, then we called region.isEmpty previously at least once
355319
check(cluster.size == 1)
356320
return UUnsatResult()
357-
} else {
358-
typeStream
359321
}
322+
323+
typeStream
360324
}
361325

362326
val typeModel = UTypeModel(typeSystem, allConcreteRefToType)
@@ -365,5 +329,5 @@ class UTypeConstraints<Type>(
365329
}
366330

367331
class UTypeUnsatResult<Type>(
368-
val expressionsToAssert: List<UBoolExpr>,
332+
val referenceDisequalitiesDisjuncts: List<UBoolExpr>,
369333
) : UUnsatResult<UTypeModel<Type>>()

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,8 @@ internal data class SplitHeapRefs(
4040
* leafs in the [ref] ite. Otherwise, it will contain an ite with the guard protecting from bubbled up concrete refs.
4141
*
4242
* @param initialGuard an initial value for the accumulated guard.
43+
* @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
44+
* considered unsatisfiable, so we assume their guards equal to false, and they won't be added to the result.
4345
*/
4446
internal fun splitUHeapRef(
4547
ref: UHeapRef,
@@ -291,7 +293,10 @@ internal inline fun filter(
291293

292294
completelyMapped.single()?.withAlso(initialGuard)
293295
}
294-
295-
else -> (ref with initialGuard).takeIf(predicate)
296+
else -> if (ref != ref.uctx.nullRef || !ignoreNullRefs) {
297+
(ref with initialGuard).takeIf(predicate)
298+
} else {
299+
null
300+
}
296301
}
297302
}

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ import org.usvm.UAddressSort
99
import org.usvm.UConcreteHeapRef
1010
import org.usvm.UContext
1111
import org.usvm.UExpr
12-
import org.usvm.constraints.UTypeModel
1312
import org.usvm.memory.UMemoryBase
1413
import org.usvm.solver.UExprTranslator
1514

@@ -52,20 +51,18 @@ open class ULazyModelDecoder<Field, Type, Method>(
5251
* equivalence classes of addresses and work with their number in the future.
5352
*/
5453
private fun buildMapping(model: KModel): AddressesMapping {
55-
// Translated null has to be equal to evaluated null, because it is of KUninterpretedSort and translatedNullRef
56-
// defined as mkUninterpretedSortValue(addressSort, 0).
57-
val evaluatedNullRef = model.eval(translatedNullRef, isComplete = true)
54+
val interpreterdNullRef = model.eval(translatedNullRef, isComplete = true)
5855

5956
val result = mutableMapOf<KExpr<KUninterpretedSort>, UConcreteHeapRef>()
60-
// Except the null value, it has the NULL_ADDRESS
61-
result[evaluatedNullRef] = ctx.mkConcreteHeapRef(NULL_ADDRESS)
57+
// The null value has the NULL_ADDRESS
58+
result[interpreterdNullRef] = ctx.mkConcreteHeapRef(NULL_ADDRESS)
6259

6360
val universe = model.uninterpretedSortUniverse(ctx.addressSort) ?: return result
6461
// All the numbers are enumerated from the INITIAL_INPUT_ADDRESS to the Int.MIN_VALUE
6562
var counter = INITIAL_INPUT_ADDRESS
6663

6764
for (interpretedAddress in universe) {
68-
if (interpretedAddress == evaluatedNullRef) {
65+
if (interpretedAddress == interpreterdNullRef) {
6966
continue
7067
}
7168
result[interpretedAddress] = ctx.mkConcreteHeapRef(counter--)

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ import io.ksmt.solver.KModel
44
import io.ksmt.utils.asExpr
55
import io.ksmt.utils.cast
66
import org.usvm.INITIAL_INPUT_ADDRESS
7+
import org.usvm.NULL_ADDRESS
78
import org.usvm.UBoolExpr
89
import org.usvm.UComposer
910
import org.usvm.UConcreteHeapRef
@@ -96,10 +97,22 @@ class ULazyHeapModel<Field, ArrayType>(
9697
private val resolvedInputArrays = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>()
9798
private val resolvedInputLengths = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>()
9899

100+
/**
101+
* To resolve nullRef, we need to:
102+
* * translate it
103+
* * evaluate the translated value in the [model]
104+
* * map the evaluated value with the [addressesMapping]
105+
*
106+
* Actually, its address should always be equal 0.
107+
*/
99108
private val nullRef = model
100109
.eval(translator.translate(translator.ctx.nullRef))
101110
.mapAddress(addressesMapping) as UConcreteHeapRef
102111

112+
init {
113+
check(nullRef.address == NULL_ADDRESS)
114+
}
115+
103116
override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
104117
// All the expressions in the model are interpreted, therefore, they must
105118
// have concrete addresses. Moreover, the model knows only about input values

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ import org.usvm.ULValue
1313
import org.usvm.UMockEvaluator
1414
import org.usvm.URegisterLValue
1515
import org.usvm.USort
16-
import org.usvm.constraints.UTypeModel
1716
import org.usvm.memory.UReadOnlySymbolicHeap
1817
import org.usvm.memory.UReadOnlySymbolicMemory
1918
import org.usvm.types.UTypeStream

‎usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
package org.usvm.model
2+
3+
import org.usvm.INITIAL_INPUT_ADDRESS
4+
import org.usvm.NULL_ADDRESS
5+
import org.usvm.UBoolExpr
6+
import org.usvm.UConcreteHeapAddress
7+
import org.usvm.UConcreteHeapRef
8+
import org.usvm.UHeapRef
9+
import org.usvm.constraints.UTypeEvaluator
10+
import org.usvm.types.UTypeStream
11+
import org.usvm.types.UTypeSystem
12+
13+
class UTypeModel<Type>(
14+
val typeSystem: UTypeSystem<Type>,
15+
typeStreamByAddr: Map<UConcreteHeapAddress, UTypeStream<Type>>,
16+
) : UTypeEvaluator<Type> {
17+
private val typeStreamByAddr = typeStreamByAddr.toMutableMap()
18+
19+
fun typeStream(ref: UConcreteHeapRef): UTypeStream<Type> =
20+
typeStreamByAddr[ref.address] ?: typeSystem.topTypeStream()
21+
22+
override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr =
23+
when {
24+
ref is UConcreteHeapRef && ref.address == NULL_ADDRESS -> ref.ctx.trueExpr
25+
26+
ref is UConcreteHeapRef -> {
27+
// All the expressions in the model are interpreted, therefore, they must
28+
// have concrete addresses. Moreover, the model knows only about input values
29+
// which have addresses less or equal than INITIAL_INPUT_ADDRESS
30+
require(ref.address <= INITIAL_INPUT_ADDRESS)
31+
32+
val evaluatedTypeStream = typeStream(ref)
33+
val typeStream = evaluatedTypeStream.filterBySupertype(type)
34+
if (!typeStream.isEmpty) {
35+
typeStreamByAddr[ref.address] = typeStream
36+
ref.ctx.trueExpr
37+
} else {
38+
ref.ctx.falseExpr
39+
}
40+
}
41+
42+
else -> error("Expecting concrete ref, but got $ref")
43+
}
44+
}

‎usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ open class USolverBase<Field, Type, Method>(
149149
)
150150

151151
// in case of failure, assert reference disequality expressions
152-
is UTypeUnsatResult<Type> -> typeResult.expressionsToAssert
152+
is UTypeUnsatResult<Type> -> typeResult.referenceDisequalitiesDisjuncts
153153
.map(translator::translate)
154154
.forEach(smtSolver::assert)
155155

‎usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ class USupportTypeStream<Type> private constructor(
9292
}
9393
}
9494

95-
override fun take(n: Int): Collection<Type> =
95+
override fun take(n: Int): List<Type> =
9696
cachingSequence.take(n).toList()
9797

9898
override val isEmpty: Boolean

‎usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ interface UTypeStream<Type> {
5353
/**
5454
* An empty type stream.
5555
*/
56-
class UEmptyTypeStream<Type> : UTypeStream<Type> {
56+
class UEmptyTypeStream<Type> private constructor() : UTypeStream<Type> {
5757
override fun filterBySupertype(type: Type): UTypeStream<Type> = this
5858

5959
override fun filterBySubtype(type: Type): UTypeStream<Type> = this
@@ -66,6 +66,13 @@ class UEmptyTypeStream<Type> : UTypeStream<Type> {
6666

6767
override val isEmpty: Boolean
6868
get() = true
69+
70+
companion object {
71+
@Suppress("UNCHECKED_CAST")
72+
operator fun <Type> invoke() = instance as UEmptyTypeStream<Type>
73+
74+
val instance = UEmptyTypeStream<Nothing>()
75+
}
6976
}
7077

7178
fun <Type> UTypeStream<Type>.takeFirst(): Type = take(1).single()

‎usvm-core/src/test/kotlin/org/usvm/TestUtil.kt

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

3-
import org.usvm.types.USingleTypeStream
4-
import org.usvm.types.UTypeStream
5-
import org.usvm.types.UTypeSystem
6-
73
typealias Field = java.lang.reflect.Field
84
typealias Type = kotlin.reflect.KClass<*>
95
typealias Method = kotlin.reflect.KFunction<*>

0 commit comments

Comments
 (0)