diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt index 9cea22608a..3597d10f80 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt @@ -19,7 +19,6 @@ import org.usvm.machine.interpreter.statics.JcStaticFieldRegionId import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.mapAddress -import org.usvm.sampleUValue import org.usvm.solver.UExprTranslator import org.usvm.solver.URegionDecoder import org.usvm.solver.USoftConstraintsProvider @@ -39,12 +38,13 @@ class JcComposer( class JcExprTranslator(ctx: UContext) : UExprTranslator(ctx), JcTransformer { override fun transform(expr: JcStaticFieldReading): UExpr = getOrPutRegionDecoder(expr.regionId) { - JcStaticFieldDecoder(expr.regionId) + JcStaticFieldDecoder(expr.regionId, this) }.translate(expr) } class JcStaticFieldDecoder( private val regionId: JcStaticFieldRegionId, + private val translator: UExprTranslator<*, *>, ) : URegionDecoder, Sort> { private val translated = mutableMapOf>() @@ -58,16 +58,20 @@ class JcStaticFieldDecoder( mapping: Map, assertions: List>, ): UReadOnlyMemoryRegion, Sort> = - JcStaticFieldModel(model, mapping, translated) + JcStaticFieldModel(model, mapping, translated, translator) } class JcStaticFieldModel( private val model: KModel, private val mapping: Map, private val translatedFields: Map>, + private val translator: UExprTranslator<*, *> ) : UReadOnlyMemoryRegion, Sort> { override fun read(key: JcStaticFieldLValue): UExpr { - val translated = translatedFields[key.field] ?: return key.sort.sampleUValue().mapAddress(mapping) + val translated = translatedFields[key.field] + ?: translator.translate( + key.sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, key.field, key.sort) + ) return model.eval(translated, isComplete = true).mapAddress(mapping) } }