From a5a7ae548ee64c2b0d30e065e426bf21c09d6d52 Mon Sep 17 00:00:00 2001
From: Aleksei Menshutin <a.menshutin@vkteam.ru>
Date: Sun, 20 Sep 2026 17:26:03 +0300
Subject: [PATCH] Support parameterized EtsIR model families

---
 .../call/TsBuiltInUnknownCallModels.kt        | 11 +++++++++-
 .../machine/call/TsEtsIrUnknownCallModel.kt   | 22 ++++++++++++++++++-
 .../intrinsic/TsBuiltInUnknownCallModel.kt    |  5 +++++
 3 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt
index 935d768c3e..5db429b4d2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt
@@ -1,15 +1,24 @@
 package org.usvm.machine.call
 
 import org.usvm.machine.call.intrinsic.TsBuiltInUnknownCallModel
+import org.usvm.machine.call.intrinsic.TsBuiltInUnknownCallModelFamily
 
 /** Discovers built-in model objects from the sealed hierarchy. */
 object TsBuiltInUnknownCallModels {
     private val models by lazy {
-        TsBuiltInUnknownCallModel::class.sealedSubclasses.map { modelClass ->
+        val individualModels = TsBuiltInUnknownCallModel::class.sealedSubclasses.map { modelClass ->
             requireNotNull(modelClass.objectInstance) {
                 "Built-in semantic model must be an object: ${modelClass.qualifiedName}"
             }
         }
+        val modelFamilies = TsBuiltInUnknownCallModelFamily::class.sealedSubclasses.flatMap { familyClass ->
+            val family = requireNotNull(familyClass.objectInstance) {
+                "Built-in semantic model family must be an object: ${familyClass.qualifiedName}"
+            }
+            family.models
+        }
+
+        individualModels + modelFamilies
     }
     private val allModels by lazy { TsUnknownCallModelCatalog(models) }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt
index c0b11f8be2..304ee16335 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt
@@ -111,11 +111,17 @@ class TsEtsIrUnknownCallModel(
     override val target: TsUnknownCallTarget,
     val artifact: TsEtsIrUnknownCallModelArtifact,
     val domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS,
+    val inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY,
 ) : TsUnknownCallModel, TsMachineLocalUnknownCallModel {
     override val additionalSceneFiles: List<EtsFile> = listOf(artifact.file)
 
     override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? {
-        val inputs = call.resolvedInputs() ?: return null
+        val resolvedInputs = call.resolvedInputs() ?: return null
+        val inputs = inputAdapter.adapt(
+            state = state,
+            call = call,
+            resolvedInputs = resolvedInputs,
+        ) ?: return null
         if (inputs.size != artifact.entryPoint.parameters.size) {
             return null
         }
@@ -154,10 +160,24 @@ class TsEtsIrUnknownCallModel(
             target = target,
             artifact = materializedArtifact,
             domainGuard = domainGuard,
+            inputAdapter = inputAdapter,
         )
     }
 }
 
+/** Adapts resolved call inputs to the parameters of a TypeScript model entry point. */
+fun interface TsEtsIrUnknownCallModelInputAdapter {
+    fun adapt(
+        state: TsState,
+        call: TsUnknownCall,
+        resolvedInputs: List<UExpr<*>>,
+    ): List<UExpr<*>>?
+
+    companion object {
+        val IDENTITY = TsEtsIrUnknownCallModelInputAdapter { _, _, resolvedInputs -> resolvedInputs }
+    }
+}
+
 /** Builds the symbolic input guard for one TypeScript model body. */
 fun interface TsEtsIrUnknownCallModelDomainGuard {
     fun evaluate(
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt
index ce29d46e5b..7edace4767 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt
@@ -4,3 +4,8 @@ import org.usvm.machine.call.TsUnknownCallModel
 
 /** Implement as an object in this package; the sealed hierarchy registers every built-in automatically. */
 internal sealed interface TsBuiltInUnknownCallModel : TsUnknownCallModel
+
+/** Supplies a parameterized family of built-in semantic models from one object. */
+internal sealed interface TsBuiltInUnknownCallModelFamily {
+    val models: List<TsUnknownCallModel>
+}