Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit d777277

Browse files
sergeypospelovsergeypospelov
committedJul 19, 2023
A first attempt to implement element and array types connection
1 parent d0b4b15 commit d777277

File tree

17 files changed

+265
-92
lines changed

17 files changed

+265
-92
lines changed
 

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

Lines changed: 64 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,14 @@ interface UTypeEvaluator<Type> {
3030
* Manages allocated objects separately from input ones. Indeed, we know the type of an allocated object
3131
* precisely, thus we can evaluate the subtyping constraints for them concretely (modulo generic type variables).
3232
*/
33-
class UTypeConstraints<Type>(
33+
open class UTypeConstraints<Type>(
3434
private val typeSystem: UTypeSystem<Type>,
3535
private val equalityConstraints: UEqualityConstraints,
36-
private val concreteRefToType: MutableMap<UConcreteHeapAddress, Type> = mutableMapOf(),
36+
protected val concreteRefToType: MutableMap<UConcreteHeapAddress, Type> = mutableMapOf(),
3737
symbolicRefToTypeRegion: MutableMap<USymbolicHeapRef, UTypeRegion<Type>> = mutableMapOf(),
3838
) : UTypeEvaluator<Type> {
3939
init {
40-
equalityConstraints.subscribe(::intersectConstraints)
40+
equalityConstraints.subscribe(::intersectRegions)
4141
}
4242

4343
val symbolicRefToTypeRegion get(): Map<USymbolicHeapRef, UTypeRegion<Type>> = _symbolicRefToTypeRegion
@@ -57,7 +57,7 @@ class UTypeConstraints<Type>(
5757
)
5858
}
5959

60-
private fun contradiction() {
60+
protected fun contradiction() {
6161
isContradicting = true
6262
}
6363

@@ -68,11 +68,13 @@ class UTypeConstraints<Type>(
6868
concreteRefToType[ref] = type
6969
}
7070

71-
private fun getRegion(symbolicRef: USymbolicHeapRef) =
72-
_symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] ?: topTypeRegion
71+
fun getTypeRegion(symbolicRef: USymbolicHeapRef, useRepresentative: Boolean = false): UTypeRegion<Type> {
72+
val representative = if (useRepresentative) equalityConstraints.equalReferences.find(symbolicRef) else symbolicRef
73+
return _symbolicRefToTypeRegion[representative] ?: topTypeRegion
74+
}
7375

7476

75-
private fun setRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion<Type>) {
77+
private fun setTypeRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion<Type>) {
7678
_symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] = value
7779
}
7880

@@ -96,23 +98,7 @@ class UTypeConstraints<Type>(
9698
}
9799

98100
is USymbolicHeapRef -> {
99-
val constraints = getRegion(ref)
100-
val newConstraints = constraints.addSupertype(type)
101-
if (newConstraints.isContradicting) {
102-
// the only left option here is to be equal to null
103-
equalityConstraints.makeEqual(ref, ref.uctx.nullRef)
104-
} else {
105-
// Inferring new symbolic disequalities here
106-
for ((key, value) in _symbolicRefToTypeRegion.entries) {
107-
// TODO: cache intersections?
108-
if (key != ref && value.intersect(newConstraints).isEmpty) {
109-
// If we have two inputs of incomparable reference types, then they are either non equal,
110-
// or both nulls
111-
equalityConstraints.makeNonEqualOrBothNull(ref, key)
112-
}
113-
}
114-
setRegion(ref, newConstraints)
115-
}
101+
updateRegionCanBeEqualNull(ref) { it.addSupertype(type) }
116102
}
117103

118104
else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref")
@@ -139,23 +125,7 @@ class UTypeConstraints<Type>(
139125
}
140126

141127
is USymbolicHeapRef -> {
142-
val constraints = getRegion(ref)
143-
val newConstraints = constraints.excludeSupertype(type)
144-
equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef)
145-
if (newConstraints.isContradicting || equalityConstraints.isContradicting) {
146-
// the [ref] can't be equal to null
147-
contradiction()
148-
} else {
149-
// Inferring new symbolic disequalities here
150-
for ((key, value) in _symbolicRefToTypeRegion.entries) {
151-
// TODO: cache intersections?
152-
if (key != ref && value.intersect(newConstraints).isEmpty) {
153-
// If we have two inputs of incomparable reference types, then they are non equal
154-
equalityConstraints.makeNonEqual(ref, key)
155-
}
156-
}
157-
setRegion(ref, newConstraints)
158-
}
128+
updateRegionCannotBeEqualNull(ref) { it.excludeSupertype(type) }
159129
}
160130

161131
else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref")
@@ -165,7 +135,7 @@ class UTypeConstraints<Type>(
165135
/**
166136
* @return a type stream corresponding to the [ref].
167137
*/
168-
internal fun readTypeStream(ref: UHeapRef): UTypeStream<Type> =
138+
internal fun getTypeStream(ref: UHeapRef): UTypeStream<Type> =
169139
when (ref) {
170140
is UConcreteHeapRef -> {
171141
val concreteType = concreteRefToType[ref.address]
@@ -180,15 +150,61 @@ class UTypeConstraints<Type>(
180150
is UNullRef -> error("Null ref should be handled explicitly earlier")
181151

182152
is USymbolicHeapRef -> {
183-
getRegion(ref).typeStream
153+
getTypeRegion(ref).typeStream
184154
}
185155

186156
else -> error("Unexpected ref: $ref")
187157
}
188158

189-
private fun intersectConstraints(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
190-
val newRegion = getRegion(ref1).intersect(getRegion(ref2))
191-
setRegion(ref1, newRegion)
159+
private fun intersectRegions(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
160+
val region = getTypeRegion(ref2)
161+
updateRegionCanBeEqualNull(ref1, region::intersect)
162+
}
163+
164+
protected fun updateRegionCannotBeEqualNull(
165+
ref: USymbolicHeapRef,
166+
regionMapper: (UTypeRegion<Type>) -> UTypeRegion<Type>,
167+
) {
168+
val region = getTypeRegion(ref)
169+
val newRegion = regionMapper(region)
170+
if (newRegion == region) {
171+
return
172+
}
173+
equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef)
174+
if (newRegion.isEmpty || equalityConstraints.isContradicting) {
175+
contradiction()
176+
return
177+
}
178+
for ((key, value) in _symbolicRefToTypeRegion.entries) {
179+
// TODO: cache intersections?
180+
if (key != ref && value.intersect(newRegion).isEmpty) {
181+
// If we have two inputs of incomparable reference types, then they are non equal
182+
equalityConstraints.makeNonEqual(ref, key)
183+
}
184+
}
185+
setTypeRegion(ref, newRegion)
186+
}
187+
188+
protected fun updateRegionCanBeEqualNull(
189+
ref: USymbolicHeapRef,
190+
regionMapper: (UTypeRegion<Type>) -> UTypeRegion<Type>,
191+
) {
192+
val region = getTypeRegion(ref)
193+
val newRegion = regionMapper(region)
194+
if (newRegion == region) {
195+
return
196+
}
197+
if (newRegion.isEmpty) {
198+
equalityConstraints.makeEqual(ref, ref.uctx.nullRef)
199+
}
200+
for ((key, value) in _symbolicRefToTypeRegion.entries) {
201+
// TODO: cache intersections?
202+
if (key != ref && value.intersect(newRegion).isEmpty) {
203+
// If we have two inputs of incomparable reference types, then they are non equal
204+
equalityConstraints.makeNonEqualOrBothNull(ref, key)
205+
}
206+
}
207+
setTypeRegion(ref, newRegion)
192208
}
193209

194210
/**
@@ -209,9 +225,9 @@ class UTypeConstraints<Type>(
209225
// accordingly to the [UIsExpr] specification, [nullRef] always satisfies the [type]
210226
return@mapper symbolicRef.ctx.trueExpr
211227
}
212-
val typeRegion = getRegion(symbolicRef)
228+
val typeRegion = getTypeRegion(symbolicRef)
213229

214-
if (typeRegion.addSupertype(type).isContradicting) {
230+
if (typeRegion.addSupertype(type).isEmpty) {
215231
symbolicRef.ctx.falseExpr
216232
} else {
217233
symbolicRef.uctx.mkIsExpr(symbolicRef, type)

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ infix fun <T> GuardedExpr<T>.withAlso(guard: UBoolExpr) = GuardedExpr(expr, guar
2626
* @param symbolicHeapRef an ite made of all [USymbolicHeapRef]s with its guard, the single [USymbolicHeapRef] if it's
2727
* the single [USymbolicHeapRef] in the base expression or `null` if there are no [USymbolicHeapRef]s at all.
2828
*/
29-
internal data class SplitHeapRefs(
29+
data class SplitHeapRefs(
3030
val concreteHeapRefs: List<GuardedExpr<UConcreteHeapRef>>,
3131
val symbolicHeapRef: GuardedExpr<UHeapRef>?,
3232
)
@@ -43,7 +43,7 @@ internal data class SplitHeapRefs(
4343
* @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
4444
* considered unsatisfiable, so we assume their guards equal to false, and they won't be added to the result.
4545
*/
46-
internal fun splitUHeapRef(
46+
fun splitUHeapRef(
4747
ref: UHeapRef,
4848
initialGuard: UBoolExpr = ref.ctx.trueExpr,
4949
ignoreNullRefs: Boolean = true,
@@ -75,7 +75,7 @@ internal fun splitUHeapRef(
7575
* @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
7676
* considered unsatisfiable, so we assume their guards equal to false.
7777
*/
78-
internal inline fun withHeapRef(
78+
inline fun withHeapRef(
7979
ref: UHeapRef,
8080
initialGuard: UBoolExpr,
8181
crossinline blockOnConcrete: (GuardedExpr<UConcreteHeapRef>) -> Unit,
@@ -104,9 +104,9 @@ internal inline fun withHeapRef(
104104
}
105105
}
106106

107-
private const val LEFT_CHILD = 0
108-
private const val RIGHT_CHILD = 1
109-
private const val DONE = 2
107+
const val LEFT_CHILD = 0
108+
const val RIGHT_CHILD = 1
109+
const val DONE = 2
110110

111111

112112
/**
@@ -118,7 +118,7 @@ private const val DONE = 2
118118
* considered unsatisfiable, so we assume their guards equal to false. If [ignoreNullRefs] is true and [this] is
119119
* [UNullRef], throws an [IllegalArgumentException].
120120
*/
121-
internal inline fun <Sort : USort> UHeapRef.map(
121+
inline fun <Sort : USort> UHeapRef.map(
122122
crossinline concreteMapper: (UConcreteHeapRef) -> UExpr<Sort>,
123123
crossinline symbolicMapper: (USymbolicHeapRef) -> UExpr<Sort>,
124124
ignoreNullRefs: Boolean = true,

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,5 +162,5 @@ open class UMemoryBase<Field, Type, Method>(
162162
UMemoryBase(ctx, typeConstraints, stack.clone(), heap.toMutableHeap(), mocker)
163163

164164
override fun typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
165-
types.readTypeStream(ref)
165+
types.getTypeStream(ref)
166166
}

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ class ULazyHeapModel<Field, ArrayType>(
117117
// All the expressions in the model are interpreted, therefore, they must
118118
// have concrete addresses. Moreover, the model knows only about input values
119119
// which have addresses less or equal than INITIAL_INPUT_ADDRESS
120-
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
120+
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
121121

122122
val resolvedRegion = resolvedInputFields[field]
123123
val regionId = UInputFieldId(field, sort, contextHeap = null)
@@ -142,7 +142,7 @@ class ULazyHeapModel<Field, ArrayType>(
142142
// All the expressions in the model are interpreted, therefore, they must
143143
// have concrete addresses. Moreover, the model knows only about input values
144144
// which have addresses less or equal than INITIAL_INPUT_ADDRESS
145-
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
145+
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
146146

147147
val key = ref to index
148148

@@ -164,7 +164,7 @@ class ULazyHeapModel<Field, ArrayType>(
164164
// All the expressions in the model are interpreted, therefore, they must
165165
// have concrete addresses. Moreover, the model knows only about input values
166166
// which have addresses less or equal than INITIAL_INPUT_ADDRESS
167-
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
167+
require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
168168

169169
val resolvedRegion = resolvedInputLengths[arrayType]
170170
val regionId = UInputArrayLengthId(arrayType, ref.uctx.sizeSort, contextHeap = null)

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ class USoftConstraintsProvider<Field, Type>(override val ctx: UContext) : UTrans
5252
fun provide(initialExpr: UExpr<*>): Set<UBoolExpr> =
5353
caches.getOrElse(initialExpr) {
5454
apply(initialExpr)
55-
provide(initialExpr)
55+
caches.getValue(initialExpr)
5656
}
5757

5858
// region The most common methods
@@ -97,10 +97,9 @@ class USoftConstraintsProvider<Field, Type>(override val ctx: UContext) : UTrans
9797
expr: UConcreteHeapRef,
9898
): UExpr<UAddressSort> = error("Illegal operation since UConcreteHeapRef must not be translated into a solver")
9999

100-
override fun transform(expr: UNullRef): UExpr<UAddressSort> = expr
100+
override fun transform(expr: UNullRef): UExpr<UAddressSort> = transformExpr(expr)
101101

102-
override fun transform(expr: UIsExpr<Type>): UBoolExpr =
103-
error("Illegal operation since UIsExpr should not be translated into a SMT solver")
102+
override fun transform(expr: UIsExpr<Type>): UBoolExpr = transformExpr(expr)
104103

105104
override fun transform(
106105
expr: UInputArrayLengthReading<Type>,

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

Lines changed: 16 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,6 @@ open class UTypeRegion<Type>(
1616
val subtypes: PersistentSet<Type> = persistentSetOf(),
1717
val notSubtypes: PersistentSet<Type> = persistentSetOf(),
1818
) : Region<UTypeRegion<Type>> {
19-
val isContradicting get() = typeStream.isEmpty
20-
2119
/**
2220
* Returns region that represents empty set of types. Called when type
2321
* constraints contradict, for example if X <: Y and X </: Y.
@@ -37,7 +35,7 @@ open class UTypeRegion<Type>(
3735
* - t is final && t </: X && X <: t
3836
*/
3937
open fun addSupertype(supertype: Type): UTypeRegion<Type> {
40-
if (isContradicting || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
38+
if (isEmpty || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
4139
return this
4240
}
4341

@@ -84,7 +82,7 @@ open class UTypeRegion<Type>(
8482
* X <: u && u <: t && X </: t, i.e. if [supertypes] contains subtype of [notSupertype]
8583
*/
8684
open fun excludeSupertype(notSupertype: Type): UTypeRegion<Type> {
87-
if (isContradicting || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) {
85+
if (isEmpty || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) {
8886
return this
8987
}
9088

@@ -108,8 +106,8 @@ open class UTypeRegion<Type>(
108106
* - t <: X && u <: t && u </: X, i.e. if [notSubtypes] contains subtype of [subtype]
109107
* - t <: X && X <: u && t </: u
110108
*/
111-
protected open fun addSubtype(subtype: Type): UTypeRegion<Type> {
112-
if (isContradicting || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
109+
open fun addSubtype(subtype: Type): UTypeRegion<Type> {
110+
if (isEmpty || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
113111
return this
114112
}
115113

@@ -134,8 +132,8 @@ open class UTypeRegion<Type>(
134132
* - u <: X && t <: u && t </: X, i.e. if [subtypes] contains supertype of [notSubtype]
135133
* - t is final && t </: X && X <: t
136134
*/
137-
protected open fun excludeSubtype(notSubtype: Type): UTypeRegion<Type> {
138-
if (isContradicting || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) {
135+
open fun excludeSubtype(notSubtype: Type): UTypeRegion<Type> {
136+
if (isEmpty || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) {
139137
return this
140138
}
141139

@@ -153,9 +151,12 @@ open class UTypeRegion<Type>(
153151
return UTypeRegion(typeSystem, newTypeStream, notSubtypes = newNotSubtypes)
154152
}
155153

156-
override val isEmpty: Boolean = isContradicting
154+
override val isEmpty: Boolean = typeStream.isEmpty
157155

158156
override fun intersect(other: UTypeRegion<Type>): UTypeRegion<Type> {
157+
if (this == other) {
158+
return this
159+
}
159160
// TODO: optimize things up by not re-allocating type regions after each operation
160161
val otherSize = other.size
161162
val thisSize = this.size
@@ -164,6 +165,9 @@ open class UTypeRegion<Type>(
164165
} else {
165166
this to other
166167
}
168+
if (smallRegion.isEmpty) {
169+
return smallRegion
170+
}
167171

168172
val result1 = smallRegion.supertypes.fold(largeRegion) { acc, t -> acc.addSupertype(t) }
169173
val result2 = smallRegion.notSupertypes.fold(result1) { acc, t -> acc.excludeSupertype(t) }
@@ -172,6 +176,9 @@ open class UTypeRegion<Type>(
172176
}
173177

174178
override fun subtract(other: UTypeRegion<Type>): UTypeRegion<Type> {
179+
if (isEmpty || other.isEmpty) {
180+
return this
181+
}
175182
if (other.notSupertypes.isNotEmpty() || other.notSubtypes.isEmpty() || other.supertypes.size + other.subtypes.size != 1) {
176183
TODO("For now, we are able to subtract only positive singleton type constraints")
177184
}

‎usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,29 @@ class TypeSolverTest {
148148
assertIs<UUnsatResult<UModelBase<Field, TestType>>>(resultWithEqConstraint)
149149
}
150150

151+
@Test
152+
fun `Test symbolic ref -- different types 3 refs`(): Unit = with(ctx) {
153+
val ref0 = ctx.mkRegisterReading(0, addressSort)
154+
val ref1 = ctx.mkRegisterReading(1, addressSort)
155+
val ref2 = ctx.mkRegisterReading(2, addressSort)
156+
157+
pc += mkIsExpr(ref0, interfaceAB)
158+
pc += mkIsExpr(ref1, interfaceBC1)
159+
pc += mkIsExpr(ref2, interfaceAC)
160+
pc += mkHeapRefEq(ref0, nullRef).not()
161+
pc += mkHeapRefEq(ref1, nullRef).not()
162+
pc += mkHeapRefEq(ref2, nullRef).not()
163+
164+
val resultWithoutEqConstraint = solver.check(pc)
165+
val model = assertIs<USatResult<UModelBase<Field, TestType>>>(resultWithoutEqConstraint).model
166+
assertNotEquals(model.eval(ref0), model.eval(ref1))
167+
168+
pc += mkHeapRefEq(ref0, ref1)
169+
pc += mkHeapRefEq(ref1, ref2)
170+
171+
assertTrue(pc.isFalse)
172+
}
173+
151174
@Test
152175
fun `Test symbolic ref -- different interface types but same base type`(): Unit = with(ctx) {
153176
val ref0 = ctx.mkRegisterReading(0, addressSort)

‎usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import org.jacodb.api.JcRefType
88
import org.jacodb.api.JcType
99
import org.jacodb.api.ext.isAssignable
1010
import org.jacodb.api.ext.objectType
11+
import org.jacodb.api.ext.packageName
1112
import org.jacodb.api.ext.toType
1213
import org.jacodb.impl.features.HierarchyExtensionImpl
1314
import org.usvm.types.USupportTypeStream
@@ -43,6 +44,17 @@ class JcTypeSystem(
4344
else -> error("Unknown type $t")
4445
}
4546

47+
fun isArrayElemType(elemType: JcType, arrayType: JcType): Boolean {
48+
if (arrayType !is JcArrayType) {
49+
return false
50+
}
51+
return isSupertype(arrayType.elementType, elemType)
52+
}
53+
54+
fun arrayTypeOf(type: JcType): JcType {
55+
return type.classpath.arrayTypeOf(type)
56+
}
57+
4658
private val topTypeStream by lazy { USupportTypeStream.from(this, cp.objectType) }
4759

4860
override fun topTypeStream(): UTypeStream<JcType> =

‎usvm-jvm/src/main/kotlin/org/usvm/machine/constraints/JcTypeConstraints.kt‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
//package org.usvm.machine.constraints
2+
//
3+
//import org.jacodb.api.JcArrayType
4+
//import org.jacodb.api.JcType
5+
//import org.usvm.UBoolExpr
6+
//import org.usvm.UConcreteHeapRef
7+
//import org.usvm.UHeapRef
8+
//import org.usvm.UNullRef
9+
//import org.usvm.USymbolicHeapRef
10+
//import org.usvm.constraints.UEqualityConstraints
11+
//import org.usvm.constraints.UTypeConstraints
12+
//import org.usvm.machine.JcTypeSystem
13+
//import org.usvm.machine.jctx
14+
//import org.usvm.memory.map
15+
//
16+
//class JcTypeConstraints(
17+
// private val typeSystem: JcTypeSystem,
18+
// private val equalityConstraints: UEqualityConstraints,
19+
//) : UTypeConstraints<JcType>(typeSystem, equalityConstraints) {
20+
//
21+
// fun evalIsElementOfArray(elemRef: UHeapRef, arrayRef: UHeapRef): UBoolExpr {
22+
// val ctx = elemRef.jctx
23+
// return elemRef.map(
24+
// concreteMapper = { concreteElemRef ->
25+
// val elemType = concreteRefToType.getValue(concreteElemRef.address)
26+
// arrayRef.map(
27+
// concreteMapper = { concreteArrayRef ->
28+
// val arrayType = concreteRefToType.getValue(concreteArrayRef.address)
29+
// if (typeSystem.isArrayElemType(elemType, arrayType)) {
30+
// ctx.trueExpr
31+
// } else {
32+
// ctx.falseExpr
33+
// }
34+
// },
35+
// symbolicMapper = { symbolicArrayRef ->
36+
// val arrayTypeRegion = getTypeRegion(symbolicArrayRef)
37+
// val arrayTypeOfElement = typeSystem.arrayTypeOf(elemType)
38+
// val newArrayTypeRegion = arrayTypeRegion.addSubtype(arrayTypeOfElement)
39+
// if (newArrayTypeRegion.isEmpty) {
40+
// ctx.falseExpr
41+
// } else {
42+
// evalIsSupertype(arrayRef, arrayTypeOfElement)
43+
// }
44+
// },
45+
// ignoreNullRefs = true
46+
// )
47+
// },
48+
// symbolicMapper = mapper@{ symbolicElemRef ->
49+
// if (symbolicElemRef == ctx.nullRef) {
50+
// return@mapper ctx.trueExpr
51+
// }
52+
//
53+
// val elemTypeRegion = getTypeRegion(symbolicElemRef)
54+
// arrayRef.map(
55+
// concreteMapper = { concreteArrayRef ->
56+
// val concreteArrayType = concreteRefToType.getValue(concreteArrayRef.address) as JcArrayType
57+
// evalIs(symbolicElemRef, concreteArrayType.elementType)
58+
// },
59+
// symbolicMapper = { symbolicArrayRef ->
60+
// val arrayTypeRegion = getTypeRegion(symbolicArrayRef)
61+
// // actually, we need to map type region here
62+
// val newArrayTypeRegion = arrayTypeRegion.intersect(elemTypeRegion)
63+
// if (newArrayTypeRegion.isEmpty) {
64+
// ctx.falseExpr
65+
// } else {
66+
// ctx.mkElementOfArrayTypeExpr(elemRef, arrayRef)
67+
// }
68+
// },
69+
// ignoreNullRefs = true
70+
// )
71+
// },
72+
// ignoreNullRefs = false
73+
// )
74+
// }
75+
//
76+
// fun addIsElementOfArray(elemRef: UHeapRef, arrayRef: UHeapRef) {
77+
// when (elemRef) {
78+
// is UConcreteHeapRef -> {
79+
// val elemType = concreteRefToType.getValue(elemRef.address)
80+
// when (arrayRef) {
81+
// is UConcreteHeapRef -> {
82+
// val arrayType = concreteRefToType.getValue(arrayRef.address) as JcArrayType
83+
// if (typeSystem.isArrayElemType(elemType, arrayType)) {
84+
// contradiction()
85+
// }
86+
// }
87+
//
88+
// is UNullRef -> error("Null ref should be handled explicitly earlier")
89+
// is USymbolicHeapRef -> {
90+
// val arrayTypeOfElement = typeSystem.arrayTypeOf(elemType)
91+
// updateRegionCannotBeEqualNull(arrayRef) { it.addSubtype(arrayTypeOfElement) }
92+
// }
93+
//
94+
// else -> error("Unexpected ref: $arrayRef")
95+
// }
96+
// }
97+
//
98+
// is UNullRef -> return
99+
// is USymbolicHeapRef -> {
100+
// when (arrayRef) {
101+
// is UConcreteHeapRef -> {
102+
// val arrayType = concreteRefToType.getValue(arrayRef.address) as JcArrayType
103+
// updateRegionCanBeEqualNull(elemRef) { it.addSupertype(arrayType) }
104+
// }
105+
//
106+
// is UNullRef -> error("Null ref should be handled explicitly earlier")
107+
// is USymbolicHeapRef -> {
108+
// val elemTypeRegion = getTypeRegion(elemRef)
109+
// val arrayTypeRegion = getTypeRegion(arrayRef)
110+
// // actually, we need to map type regions here
111+
// updateRegionCanBeEqualNull(elemRef) { it.intersect(arrayTypeRegion) }
112+
// // actually, we need to map type regions here
113+
// updateRegionCannotBeEqualNull(arrayRef) { it.intersect(elemTypeRegion) }
114+
// }
115+
//
116+
// else -> error("Unexpected ref: $arrayRef")
117+
// }
118+
// }
119+
//
120+
// else -> error("Unexpected ref: $arrayRef")
121+
// }
122+
// }
123+
//}

‎usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ import org.usvm.UCallStack
1010
import org.usvm.UContext
1111
import org.usvm.UState
1212
import org.usvm.constraints.UPathConstraints
13-
import org.usvm.machine.JcContext
1413
import org.usvm.memory.UMemoryBase
1514
import org.usvm.model.UModelBase
1615

‎usvm-jvm/src/samples/java/org/usvm/samples/objects/HiddenFieldExample.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
package org.usvm.samples.objects;
22

3-
import static org.usvm.api.mock.UMockKt.assume;
4-
53
public class HiddenFieldExample {
64
public int checkHiddenField(HiddenFieldSuperClass o) {
7-
assume(!(o instanceof HiddenFieldSuccClass));
5+
if (o instanceof HiddenFieldSuccClass) {
6+
return 0;
7+
}
88

99
if (o.a == 1 && o.b == 2) {
1010
return 1;

‎usvm-jvm/src/samples/java/org/usvm/samples/types/PathDependentGenericsExample.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,11 @@ private <T, K extends Number> void functionWithSeveralGenerics(List<K> firstValu
4242
}
4343

4444
private <T> void functionWithOneGeneric(ClassWithOneGeneric<T> value) {
45-
System.out.println();
45+
4646
}
4747

4848
private <T, K> void functionWithTwoGenerics(ClassWithTwoGenerics<T, K> value) {
49-
System.out.println();
49+
5050
}
5151
}
5252

‎usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import org.usvm.test.util.checkers.eq
99

1010
internal class CastClassTest : JavaMethodTestRunner() {
1111
@Test
12-
@Disabled("Support instanceof")
12+
@Disabled("Support assumptions")
1313
fun testThisTypeChoice() {
1414
checkDiscoveredProperties(
1515
CastClass::castToInheritor,

‎usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt‎

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

3-
import org.junit.jupiter.api.Disabled
43
import org.junit.jupiter.api.Test
54
import org.usvm.samples.JavaMethodTestRunner
65
import org.usvm.test.util.checkers.eq
76
import org.usvm.test.util.checkers.ge
87
import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
98

10-
11-
@Disabled("Support instanceof")
129
internal class InstanceOfExampleTest : JavaMethodTestRunner() {
1310
@Test
1411
fun testSimpleInstanceOf() {
@@ -234,7 +231,6 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
234231
}
235232

236233
@Test
237-
@Disabled("Unexpected lvalue org.usvm.machine.JcStaticFieldRef@74414a78")
238234
fun testInstanceOfAsInternalExpressionsMap() {
239235
checkDiscoveredProperties(
240236
InstanceOfExample::instanceOfAsInternalExpressionsMap,
@@ -247,9 +243,8 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
247243
fun testSymbolicInstanceOf() {
248244
checkDiscoveredProperties(
249245
InstanceOfExample::symbolicInstanceOf,
250-
eq(6),
251-
{ _, _, i, r -> i < 1 && r == null },
252-
{ _, _, i, r -> i > 3 && r == null },
246+
eq(5),
247+
{ _, _, i, r -> (i < 1 || i > 3) && r == null },
253248
{ _, o, _, _ -> o == null },
254249
{ _, o, i, _ -> o != null && i > o.lastIndex },
255250
{ _, o, i, r -> o != null && o[i] is CastClassFirstSucc && r is CastClassFirstSucc },

‎usvm-jvm/src/test/kotlin/org/usvm/samples/objects/HiddenFieldExampleTest.kt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@ import org.usvm.test.util.checkers.eq
88

99
internal class HiddenFieldExampleTest : JavaMethodTestRunner() {
1010
@Test
11-
@Disabled("Support instanceof")
1211
fun testCheckHiddenField() {
1312
checkDiscoveredProperties(
1413
HiddenFieldExample::checkHiddenField,
15-
eq(4),
14+
eq(5),
1615
{ _, o, _ -> o == null },
16+
{ _, o, r -> o is HiddenFieldSuccClass && r == 0 },
1717
{ _, o, r -> o != null && o.a != 1 && r == 2 },
1818
{ _, o, r -> o != null && o.a == 1 && o.b != 2 && r == 2 },
1919
{ _, o, r -> o != null && o.a == 1 && o.b == 2 && r == 1 },

‎usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import java.util.TreeMap
99

1010
internal class StandardStructuresTest : JavaMethodTestRunner() {
1111
@Test
12-
@Disabled("Support instanceof")
12+
@Disabled("Support creation of collections")
1313
fun testGetList() {
1414
checkDiscoveredProperties(
1515
StandardStructures::getList,
@@ -24,7 +24,7 @@ internal class StandardStructuresTest : JavaMethodTestRunner() {
2424
}
2525

2626
@Test
27-
@Disabled("Support instanceof")
27+
@Disabled("Support creation of collections")
2828
fun testGetMap() {
2929
checkDiscoveredProperties(
3030
StandardStructures::getMap,
@@ -36,7 +36,7 @@ internal class StandardStructuresTest : JavaMethodTestRunner() {
3636
}
3737

3838
@Test
39-
@Disabled("Support instanceof")
39+
@Disabled("Support creation of collections")
4040
fun testGetDeque() {
4141
checkDiscoveredProperties(
4242
StandardStructures::getDeque,

‎usvm-jvm/src/test/kotlin/org/usvm/samples/types/PathDependentGenericsExampleTest.kt‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ import org.usvm.test.util.checkers.eq
88

99
internal class PathDependentGenericsExampleTest : JavaMethodTestRunner() {
1010
@Test
11-
@Disabled("Support instanceof")
1211
fun testPathDependentGenerics() {
1312
checkDiscoveredProperties(
1413
PathDependentGenericsExample::pathDependentGenerics,

0 commit comments

Comments
 (0)
Please sign in to comment.