Extract a separate translator for TS (#247)

UnitTestBot · Feb 7, 2025 · 54d248a · 54d248a
1 parent 62b17f8
commit 54d248a
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 0 deletions.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TSComponents.kt
@@ -7,9 +7,14 @@ import org.jacodb.ets.base.EtsType
 import org.usvm.SolverType
 import org.usvm.UBv32SizeExprProvider
 import org.usvm.UComponents
+import org.usvm.UComposer
 import org.usvm.UContext
 import org.usvm.UMachineOptions
 import org.usvm.USizeExprProvider
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.memory.UReadOnlyMemory
+import org.usvm.model.ULazyModelDecoder
+import org.usvm.solver.UExprTranslator
 import org.usvm.solver.USolverBase
 import org.usvm.solver.UTypeSolver
 import org.usvm.types.UTypeSystem
@@ -23,10 +28,26 @@ class TSComponents(
     override val useSolverForForks: Boolean
         get() = options.useSolverForForks
 
+    override fun <Context : UContext<TSSizeSort>> buildTranslatorAndLazyDecoder(
+        ctx: Context,
+    ): Pair<UExprTranslator<EtsType, TSSizeSort>, ULazyModelDecoder<EtsType>> {
+        val translator = TSExprTranslator(ctx)
+        val decoder = ULazyModelDecoder(translator)
+
+        return translator to decoder
+    }
+
     override fun <Context : UContext<TSSizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<TSSizeSort> {
         return UBv32SizeExprProvider(ctx)
     }
 
+    override fun <Context : UContext<TSSizeSort>> mkComposer(
+        ctx: Context,
+    ): (UReadOnlyMemory<EtsType>, MutabilityOwnership) -> UComposer<EtsType, TSSizeSort> =
+        { memory: UReadOnlyMemory<EtsType>, ownership: MutabilityOwnership ->
+            TSComposer(ctx, memory, ownership)
+        }
+
     override fun mkTypeSystem(
         ctx: UContext<TSSizeSort>,
     ): UTypeSystem<EtsType> = typeSystem

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TSTransformer.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TSTransformer.kt
@@ -0,0 +1,20 @@
+package org.usvm.machine
+
+import org.jacodb.ets.base.EtsType
+import org.usvm.UComposer
+import org.usvm.UContext
+import org.usvm.UTransformer
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.memory.UReadOnlyMemory
+import org.usvm.solver.UExprTranslator
+
+interface TSTransformer : UTransformer<EtsType, TSSizeSort>
+
+class TSComposer(
+    ctx: UContext<TSSizeSort>,
+    memory: UReadOnlyMemory<EtsType>,
+    ownership: MutabilityOwnership,
+) : UComposer<EtsType, TSSizeSort>(ctx, memory, ownership), TSTransformer
+
+class TSExprTranslator(ctx: UContext<TSSizeSort>) : UExprTranslator<EtsType, TSSizeSort>(ctx), TSTransformer
+