Skip to content

Commit dab6d43

Browse files
authored
Added names for mocks (#339)
1 parent 71cd0e1 commit dab6d43

File tree

3 files changed

+11
-6
lines changed

3 files changed

+11
-6
lines changed

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -366,9 +366,10 @@ open class UContext<USizeSort : USort>(
366366
private var trackedIndex = 0
367367

368368
fun <Sort : USort> mkTrackedSymbol(
369-
sort: Sort
369+
sort: Sort,
370+
name: String? = null,
370371
): UTrackedSymbol<Sort> = trackedSymbols.createIfContextActive {
371-
UTrackedSymbol(this, name = "tracked#${trackedIndex++}", sort)
372+
UTrackedSymbol(this, name = "${name ?: "tracked"}#${trackedIndex++}", sort)
372373
}.cast()
373374

374375
private val isSubtypeExprCache = mkAstInterner<UIsSubtypeExpr<Any>>()

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,9 @@ interface UMockEvaluator {
1414
fun <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort>
1515
}
1616

17-
interface TrackedLiteral
17+
interface TrackedLiteral {
18+
val name: String
19+
}
1820

1921
interface UMocker<Method> : UMockEvaluator {
2022
fun <Sort : USort> call(
@@ -69,7 +71,7 @@ class UIndexedMocker<Method>(
6971
sort: Sort,
7072
ownership: MutabilityOwnership,
7173
): UExpr<Sort> {
72-
val const = sort.uctx.mkTrackedSymbol(sort)
74+
val const = sort.uctx.mkTrackedSymbol(sort, trackedLiteral?.name)
7375

7476
if (trackedLiteral != null) {
7577
trackedSymbols = trackedSymbols.put(trackedLiteral, const, ownership)

usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt

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

33
import org.usvm.StepScope
4+
import org.usvm.TrackedLiteral
45
import org.usvm.UBoolExpr
56
import org.usvm.UExpr
67
import org.usvm.UHeapRef
@@ -12,10 +13,11 @@ import org.usvm.utils.logAssertFailure
1213
// TODO: special mock api for variables
1314

1415
fun <Method, T : USort> UState<*, Method, *, *, *, *>.makeSymbolicPrimitive(
15-
sort: T
16+
sort: T,
17+
trackedLiteral: TrackedLiteral? = null,
1618
): UExpr<T> {
1719
check(sort != sort.uctx.addressSort) { "$sort is not primitive" }
18-
return memory.mocker.createMockSymbol(trackedLiteral = null, sort, ownership)
20+
return memory.mocker.createMockSymbol(trackedLiteral = trackedLiteral, sort, ownership)
1921
}
2022

2123
fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRef(

0 commit comments

Comments
 (0)