Skip to content

Commit a453cbc

Browse files
DamtevDamtev
authored
Configurable size sort (#71)
1 parent 103191f commit a453cbc

File tree

105 files changed

+1239
-1017
lines changed

Some content is hidden

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

105 files changed

+1239
-1017
lines changed

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,10 @@ import org.usvm.memory.USymbolicCollectionId
2020
import org.usvm.regions.Region
2121

2222
@Suppress("MemberVisibilityCanBePrivate")
23-
open class UComposer<Type>(
24-
ctx: UContext,
23+
open class UComposer<Type, USizeSort : USort>(
24+
ctx: UContext<USizeSort>,
2525
internal val memory: UReadOnlyMemory<Type>
26-
) : UExprTransformer<Type>(ctx) {
26+
) : UExprTransformer<Type, USizeSort>(ctx) {
2727
open fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort> = apply(expr)
2828

2929
override fun <T : USort> transform(expr: UIteExpr<T>): UExpr<T> =
@@ -61,13 +61,13 @@ open class UComposer<Type>(
6161
return collection.read(mappedKey, this@UComposer)
6262
}
6363

64-
override fun transform(expr: UInputArrayLengthReading<Type>): USizeExpr =
64+
override fun transform(expr: UInputArrayLengthReading<Type, USizeSort>): UExpr<USizeSort> =
6565
transformCollectionReading(expr, expr.address)
6666

67-
override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort> =
67+
override fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort, USizeSort>): UExpr<Sort> =
6868
transformCollectionReading(expr, expr.address to expr.index)
6969

70-
override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort> =
70+
override fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort, USizeSort>): UExpr<Sort> =
7171
transformCollectionReading(expr, expr.index)
7272

7373
override fun <Field, Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort> =
@@ -93,7 +93,7 @@ open class UComposer<Type>(
9393
expr: UInputRefMapWithInputKeysReading<Type, Sort>
9494
): UExpr<Sort> = transformCollectionReading(expr, expr.mapRef to expr.keyRef)
9595

96-
override fun transform(expr: UInputMapLengthReading<Type>): USizeExpr =
96+
override fun transform(expr: UInputMapLengthReading<Type, USizeSort>): UExpr<USizeSort> =
9797
transformCollectionReading(expr, expr.address)
9898

9999
override fun <ElemSort : USort, Reg : Region<Reg>> transform(
@@ -119,4 +119,4 @@ open class UComposer<Type>(
119119
}
120120

121121
@Suppress("NOTHING_TO_INLINE")
122-
inline fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr
122+
inline fun <T : USort> UComposer<*, *>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr

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

Lines changed: 42 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -48,15 +48,16 @@ import org.usvm.solver.USolverBase
4848
import org.usvm.types.UTypeSystem
4949

5050
@Suppress("LeakingThis")
51-
open class UContext(
52-
components: UComponents<*>,
51+
open class UContext<USizeSort : USort>(
52+
components: UComponents<*, USizeSort>,
5353
operationMode: OperationMode = OperationMode.CONCURRENT,
5454
astManagementMode: AstManagementMode = AstManagementMode.GC,
5555
simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY,
5656
) : KContext(operationMode, astManagementMode, simplificationMode) {
5757

5858
private val solver by lazy { components.mkSolver(this) }
5959
private val typeSystem by lazy { components.mkTypeSystem(this) }
60+
val sizeExprs by lazy { components.mkSizeExprProvider(this) }
6061

6162
private var currentStateId = 0u
6263

@@ -74,10 +75,6 @@ open class UContext(
7475
this.typeSystem as UTypeSystem<Type>
7576

7677
val addressSort: UAddressSort = mkUninterpretedSort("Address")
77-
val sizeSort: USizeSort = bv32Sort
78-
79-
fun mkSizeExpr(size: Int): USizeExpr = mkBv(size)
80-
8178
val nullRef: UNullRef = UNullRef(this)
8279

8380
fun mkNullRef(): USymbolicHeapRef {
@@ -179,31 +176,31 @@ open class UContext(
179176
UInputFieldReading(this, region, address)
180177
}.cast()
181178

182-
private val allocatedArrayReadingCache = mkAstInterner<UAllocatedArrayReading<*, out USort>>()
179+
private val allocatedArrayReadingCache = mkAstInterner<UAllocatedArrayReading<*, out USort, USizeSort>>()
183180

184181
fun <ArrayType, Sort : USort> mkAllocatedArrayReading(
185-
region: UAllocatedArray<ArrayType, Sort>,
186-
index: USizeExpr,
187-
): UAllocatedArrayReading<ArrayType, Sort> = allocatedArrayReadingCache.createIfContextActive {
182+
region: UAllocatedArray<ArrayType, Sort, USizeSort>,
183+
index: UExpr<USizeSort>,
184+
): UAllocatedArrayReading<ArrayType, Sort, USizeSort> = allocatedArrayReadingCache.createIfContextActive {
188185
UAllocatedArrayReading(this, region, index)
189186
}.cast()
190187

191-
private val inputArrayReadingCache = mkAstInterner<UInputArrayReading<*, out USort>>()
188+
private val inputArrayReadingCache = mkAstInterner<UInputArrayReading<*, out USort, USizeSort>>()
192189

193190
fun <ArrayType, Sort : USort> mkInputArrayReading(
194-
region: UInputArray<ArrayType, Sort>,
191+
region: UInputArray<ArrayType, Sort, USizeSort>,
195192
address: UHeapRef,
196-
index: USizeExpr,
197-
): UInputArrayReading<ArrayType, Sort> = inputArrayReadingCache.createIfContextActive {
193+
index: UExpr<USizeSort>,
194+
): UInputArrayReading<ArrayType, Sort, USizeSort> = inputArrayReadingCache.createIfContextActive {
198195
UInputArrayReading(this, region, address, index)
199196
}.cast()
200197

201-
private val inputArrayLengthReadingCache = mkAstInterner<UInputArrayLengthReading<*>>()
198+
private val inputArrayLengthReadingCache = mkAstInterner<UInputArrayLengthReading<*, USizeSort>>()
202199

203200
fun <ArrayType> mkInputArrayLengthReading(
204-
region: UInputArrayLengths<ArrayType>,
201+
region: UInputArrayLengths<ArrayType, USizeSort>,
205202
address: UHeapRef,
206-
): UInputArrayLengthReading<ArrayType> = inputArrayLengthReadingCache.createIfContextActive {
203+
): UInputArrayLengthReading<ArrayType, USizeSort> = inputArrayLengthReadingCache.createIfContextActive {
207204
UInputArrayLengthReading(this, region, address)
208205
}.cast()
209206

@@ -262,14 +259,14 @@ open class UContext(
262259
UInputRefMapWithInputKeysReading(this, region, mapRef, keyRef)
263260
}.cast()
264261

265-
private val inputSymbolicMapLengthReadingCache = mkAstInterner<UInputMapLengthReading<*>>()
262+
private val inputSymbolicMapLengthReadingCache = mkAstInterner<UInputMapLengthReading<*, USizeSort>>()
266263

267264
fun <MapType> mkInputMapLengthReading(
268-
region: UInputMapLengthCollection<MapType>,
265+
region: UInputMapLengthCollection<MapType, USizeSort>,
269266
address: UHeapRef
270-
): UInputMapLengthReading<MapType> =
267+
): UInputMapLengthReading<MapType, USizeSort> =
271268
inputSymbolicMapLengthReadingCache.createIfContextActive {
272-
UInputMapLengthReading<MapType>(this, region, address)
269+
UInputMapLengthReading(this, region, address)
273270
}.cast()
274271

275272

@@ -371,7 +368,7 @@ open class UContext(
371368

372369
val uValueSampler: KSortVisitor<KExpr<*>> by lazy { mkUValueSampler() }
373370

374-
class UValueSampler(val uctx: UContext) : DefaultValueSampler(uctx) {
371+
class UValueSampler(val uctx: UContext<*>) : DefaultValueSampler(uctx) {
375372
override fun visit(sort: KUninterpretedSort): KExpr<*> =
376373
if (sort == uctx.addressSort) {
377374
uctx.nullRef
@@ -392,9 +389,31 @@ open class UContext(
392389
}
393390
}
394391

392+
val <USizeSort : USort> UContext<USizeSort>.sizeSort: USizeSort get() = sizeExprs.sizeSort
393+
394+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeExpr(size: Int): UExpr<USizeSort> =
395+
sizeExprs.mkSizeExpr(size)
396+
fun <USizeSort : USort> UContext<USizeSort>.getIntValue(expr: UExpr<USizeSort>): Int? =
397+
sizeExprs.getIntValue(expr)
398+
399+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeSubExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UExpr<USizeSort> =
400+
sizeExprs.mkSizeSubExpr(lhs, rhs)
401+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeLeExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UBoolExpr =
402+
sizeExprs.mkSizeLeExpr(lhs, rhs)
403+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeAddExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UExpr<USizeSort> =
404+
sizeExprs.mkSizeAddExpr(lhs, rhs)
405+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeGtExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UBoolExpr =
406+
sizeExprs.mkSizeGtExpr(lhs, rhs)
407+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeGeExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UBoolExpr =
408+
sizeExprs.mkSizeGeExpr(lhs, rhs)
409+
fun <USizeSort : USort> UContext<USizeSort>.mkSizeLtExpr(lhs: UExpr<USizeSort>, rhs: UExpr<USizeSort>): UBoolExpr =
410+
sizeExprs.mkSizeLtExpr(lhs, rhs)
395411

396412
fun <T : KSort> T.sampleUValue(): KExpr<T> =
397413
accept(uctx.uValueSampler).asExpr(this)
398414

399415
val KAst.uctx
400-
get() = ctx as UContext
416+
get() = ctx as UContext<*>
417+
418+
fun <USizeSort : USort> UContext<*>.withSizeSort(): UContext<USizeSort> = cast()
419+
inline fun <USizeSort : USort, R> UContext<*>.withSizeSort(block: UContext<USizeSort>.() -> R): R = block(withSizeSort())

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

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -19,16 +19,16 @@ import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
1919
import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
2020
import org.usvm.regions.Region
2121

22-
interface UTransformer<Type> : KTransformer {
22+
interface UTransformer<Type, USizeSort : USort> : KTransformer {
2323
fun <Sort : USort> transform(expr: URegisterReading<Sort>): UExpr<Sort>
2424

2525
fun <Field, Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort>
2626

27-
fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort>
27+
fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort, USizeSort>): UExpr<Sort>
2828

29-
fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort>): UExpr<Sort>
29+
fun <Sort : USort> transform(expr: UInputArrayReading<Type, Sort, USizeSort>): UExpr<Sort>
3030

31-
fun transform(expr: UInputArrayLengthReading<Type>): USizeExpr
31+
fun transform(expr: UInputArrayLengthReading<Type, USizeSort>): UExpr<USizeSort>
3232

3333
fun <KeySort : USort, Sort : USort, Reg : Region<Reg>> transform(
3434
expr: UAllocatedMapReading<Type, KeySort, Sort, Reg>
@@ -44,7 +44,7 @@ interface UTransformer<Type> : KTransformer {
4444

4545
fun <Sort : USort> transform(expr: UInputRefMapWithInputKeysReading<Type, Sort>): UExpr<Sort>
4646

47-
fun transform(expr: UInputMapLengthReading<Type>): USizeExpr
47+
fun transform(expr: UInputMapLengthReading<Type, USizeSort>): UExpr<USizeSort>
4848

4949
fun <ElemSort : USort, Reg : Region<Reg>> transform(expr: UAllocatedSetReading<Type, ElemSort, Reg>): UBoolExpr
5050

@@ -67,12 +67,13 @@ interface UTransformer<Type> : KTransformer {
6767
fun transform(expr: UNullRef): UExpr<UAddressSort>
6868
}
6969

70-
abstract class UExprTransformer<Type>(
71-
ctx: UContext
72-
) : KNonRecursiveTransformer(ctx), UTransformer<Type>
70+
abstract class UExprTransformer<Type, USizeSort : USort>(
71+
ctx: UContext<USizeSort>
72+
) : KNonRecursiveTransformer(ctx), UTransformer<Type, USizeSort>
7373

7474
@Suppress("UNCHECKED_CAST")
75-
fun <Type> UTransformer<*>.asTypedTransformer() = this as UTransformer<Type>
75+
fun <Type, USizeSort : USort> UTransformer<*, *>.asTypedTransformer(): UTransformer<Type, USizeSort> =
76+
this as UTransformer<Type, USizeSort>
7677

7778
@Suppress("NOTHING_TO_INLINE")
78-
inline fun <T : USort> UTransformer<*>?.apply(expr: UExpr<T>) = this?.apply(expr) ?: expr
79+
inline fun <T : USort> UTransformer<*, *>?.apply(expr: UExpr<T>) = this?.apply(expr) ?: expr

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

Lines changed: 19 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -35,12 +35,10 @@ typealias USort = KSort
3535
typealias UBoolSort = KBoolSort
3636
typealias UBvSort = KBvSort
3737
typealias UBv32Sort = KBv32Sort
38-
typealias USizeSort = KBv32Sort
3938
typealias UFpSort = KFpSort
4039

4140
typealias UExpr<Sort> = KExpr<Sort>
4241
typealias UBoolExpr = UExpr<UBoolSort>
43-
typealias USizeExpr = UExpr<USizeSort>
4442
typealias UTrue = KTrue
4543
typealias UFalse = KFalse
4644
typealias UAndExpr = KAndExpr
@@ -60,7 +58,7 @@ typealias USizeType = Int
6058

6159
//endregion
6260

63-
abstract class USymbol<Sort : USort>(ctx: UContext) : UExpr<Sort>(ctx)
61+
abstract class USymbol<Sort : USort>(ctx: UContext<*>) : UExpr<Sort>(ctx)
6462

6563
//region Object References
6664

@@ -109,14 +107,14 @@ val UConcreteHeapRef.isAllocated: Boolean get() = address >= INITIAL_CONCRETE_AD
109107
val UConcreteHeapRef.isStatic: Boolean get() = address <= INITIAL_STATIC_ADDRESS
110108

111109
class UConcreteHeapRefDecl internal constructor(
112-
ctx: UContext,
110+
ctx: UContext<*>,
113111
val address: UConcreteHeapAddress,
114112
) : KConstDecl<UAddressSort>(ctx, "0x$address", ctx.addressSort) {
115113
override fun apply(args: List<KExpr<*>>): KApp<UAddressSort, *> = uctx.mkConcreteHeapRef(address)
116114
}
117115

118116
class UConcreteHeapRef internal constructor(
119-
ctx: UContext,
117+
ctx: UContext<*>,
120118
val address: UConcreteHeapAddress,
121119
) : UIntepretedValue<UAddressSort>(ctx) {
122120

@@ -125,7 +123,7 @@ class UConcreteHeapRef internal constructor(
125123
override val sort: UAddressSort = ctx.addressSort
126124

127125
override fun accept(transformer: KTransformerBase): KExpr<UAddressSort> {
128-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
126+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
129127
return transformer.transform(this)
130128
}
131129

@@ -139,13 +137,13 @@ class UConcreteHeapRef internal constructor(
139137
}
140138

141139
class UNullRef internal constructor(
142-
ctx: UContext,
140+
ctx: UContext<*>,
143141
) : USymbolicHeapRef(ctx) {
144142
override val sort: UAddressSort
145143
get() = uctx.addressSort
146144

147145
override fun accept(transformer: KTransformerBase): KExpr<UAddressSort> {
148-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
146+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
149147
return transformer.transform(this)
150148
}
151149

@@ -193,12 +191,12 @@ const val INITIAL_STATIC_ADDRESS = -(1 shl 20) // Use value not less than UNINTE
193191
//region Read Expressions
194192

195193
class URegisterReading<Sort : USort> internal constructor(
196-
ctx: UContext,
194+
ctx: UContext<*>,
197195
val idx: Int,
198196
override val sort: Sort,
199197
) : USymbol<Sort>(ctx) {
200198
override fun accept(transformer: KTransformerBase): KExpr<Sort> {
201-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
199+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
202200
return transformer.transform(this)
203201
}
204202

@@ -212,7 +210,7 @@ class URegisterReading<Sort : USort> internal constructor(
212210
}
213211

214212
abstract class UCollectionReading<CollectionId : USymbolicCollectionId<Key, Sort, CollectionId>, Key, Sort : USort>(
215-
ctx: UContext,
213+
ctx: UContext<*>,
216214
val collection: USymbolicCollection<CollectionId, Key, Sort>
217215
) : USymbol<Sort>(ctx) {
218216
override val sort: Sort get() = collection.sort
@@ -222,17 +220,17 @@ abstract class UCollectionReading<CollectionId : USymbolicCollectionId<Key, Sort
222220

223221
//region Mocked Expressions
224222

225-
abstract class UMockSymbol<Sort : USort>(ctx: UContext, override val sort: Sort) : USymbol<Sort>(ctx)
223+
abstract class UMockSymbol<Sort : USort>(ctx: UContext<*>, override val sort: Sort) : USymbol<Sort>(ctx)
226224

227225
// TODO: make indices compositional!
228226
class UIndexedMethodReturnValue<Method, Sort : USort> internal constructor(
229-
ctx: UContext,
227+
ctx: UContext<*>,
230228
val method: Method,
231229
val callIndex: Int,
232230
override val sort: Sort,
233231
) : UMockSymbol<Sort>(ctx, sort) {
234232
override fun accept(transformer: KTransformerBase): KExpr<Sort> {
235-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
233+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
236234
return transformer.transform(this)
237235
}
238236

@@ -250,7 +248,7 @@ class UIndexedMethodReturnValue<Method, Sort : USort> internal constructor(
250248
//region Subtyping Expressions
251249

252250
abstract class UIsExpr<Type> internal constructor(
253-
ctx: UContext,
251+
ctx: UContext<*>,
254252
val ref: UHeapRef,
255253
) : USymbol<UBoolSort>(ctx) {
256254
final override val sort = ctx.boolSort
@@ -261,13 +259,13 @@ abstract class UIsExpr<Type> internal constructor(
261259
* inheritance is checked only on non-null refs.
262260
*/
263261
class UIsSubtypeExpr<Type> internal constructor(
264-
ctx: UContext,
262+
ctx: UContext<*>,
265263
ref: UHeapRef,
266264
val supertype: Type,
267265
) : UIsExpr<Type>(ctx, ref) {
268266
override fun accept(transformer: KTransformerBase): UBoolExpr {
269-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
270-
return transformer.asTypedTransformer<Type>().transform(this)
267+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
268+
return transformer.asTypedTransformer<Type, USort>().transform(this)
271269
}
272270

273271
override fun print(printer: ExpressionPrinter) {
@@ -284,13 +282,13 @@ class UIsSubtypeExpr<Type> internal constructor(
284282
* inheritance is checked only on non-null refs.
285283
*/
286284
class UIsSupertypeExpr<Type> internal constructor(
287-
ctx: UContext,
285+
ctx: UContext<*>,
288286
ref: UHeapRef,
289287
val subtype: Type,
290288
) : UIsExpr<Type>(ctx, ref) {
291289
override fun accept(transformer: KTransformerBase): UBoolExpr {
292-
require(transformer is UTransformer<*>) { "Expected a UTransformer, but got: $transformer" }
293-
return transformer.asTypedTransformer<Type>().transform(this)
290+
require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" }
291+
return transformer.asTypedTransformer<Type, USort>().transform(this)
294292
}
295293

296294
override fun print(printer: ExpressionPrinter) {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ interface UMocker<Method> : UMockEvaluator {
1818
}
1919

2020
class UIndexedMocker<Method>(
21-
private val ctx: UContext,
21+
private val ctx: UContext<*>,
2222
private val clauses: PersistentMap<Method, PersistentList<UMockSymbol<out USort>>> = persistentMapOf()
2323
) : UMocker<Method> {
2424
override fun <Sort : USort> call(

0 commit comments

Comments
 (0)