From 5d94917c1b67e90ae41c8e9e3d0fbb6fc7efc8cb Mon Sep 17 00:00:00 2001 From: tochilinak Date: Wed, 1 Apr 2026 12:57:54 +0300 Subject: [PATCH] Added names for mocks --- usvm-core/src/main/kotlin/org/usvm/Context.kt | 5 +++-- usvm-core/src/main/kotlin/org/usvm/Mocks.kt | 6 ++++-- usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt | 6 ++++-- 3 files changed, 11 insertions(+), 6 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index 8ddaa88a80..64e0bb82d8 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -366,9 +366,10 @@ open class UContext( private var trackedIndex = 0 fun mkTrackedSymbol( - sort: Sort + sort: Sort, + name: String? = null, ): UTrackedSymbol = trackedSymbols.createIfContextActive { - UTrackedSymbol(this, name = "tracked#${trackedIndex++}", sort) + UTrackedSymbol(this, name = "${name ?: "tracked"}#${trackedIndex++}", sort) }.cast() private val isSubtypeExprCache = mkAstInterner>() diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt index 599bb0c3a4..3631453f2d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt @@ -14,7 +14,9 @@ interface UMockEvaluator { fun eval(symbol: UMockSymbol): UExpr } -interface TrackedLiteral +interface TrackedLiteral { + val name: String +} interface UMocker : UMockEvaluator { fun call( @@ -69,7 +71,7 @@ class UIndexedMocker( sort: Sort, ownership: MutabilityOwnership, ): UExpr { - val const = sort.uctx.mkTrackedSymbol(sort) + val const = sort.uctx.mkTrackedSymbol(sort, trackedLiteral?.name) if (trackedLiteral != null) { trackedSymbols = trackedSymbols.put(trackedLiteral, const, ownership) diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt index 69d78fd905..fc0d674ebe 100644 --- a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt @@ -1,6 +1,7 @@ package org.usvm.api import org.usvm.StepScope +import org.usvm.TrackedLiteral import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef @@ -12,10 +13,11 @@ import org.usvm.utils.logAssertFailure // TODO: special mock api for variables fun UState<*, Method, *, *, *, *>.makeSymbolicPrimitive( - sort: T + sort: T, + trackedLiteral: TrackedLiteral? = null, ): UExpr { check(sort != sort.uctx.addressSort) { "$sort is not primitive" } - return memory.mocker.createMockSymbol(trackedLiteral = null, sort, ownership) + return memory.mocker.createMockSymbol(trackedLiteral = trackedLiteral, sort, ownership) } fun StepScope.makeSymbolicRef(