Skip to content

[TS] Model collection iterators and array callbacks #625

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
CaelmBleidd wants to merge 1 commit into
base: caelmbleidd/ts-bounded-map-set-models
Choose a base branch
from
Open

[TS] Model collection iterators and array callbacks #625

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package org.usvm.machine.call

import org.jacodb.ets.model.EtsAnyType
import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsClassSignature
import org.jacodb.ets.model.EtsFunctionType
import org.jacodb.ets.model.EtsLocal
Expand All @@ -26,6 +27,7 @@ internal fun hasBuiltinGlobalOwner(
internal fun EtsType.isBuiltinGlobalType(expectedName: String): Boolean = when (expectedName) {
"Math" -> this is EtsUnclearRefType && name == expectedName
"Number" -> this is EtsFunctionType && isBuiltinNumberType()
"Array" -> this is EtsFunctionType && isBuiltinArrayType()
else -> false
}

Expand All @@ -39,6 +41,15 @@ private fun EtsFunctionType.isBuiltinNumberType(): Boolean {
!parameter.isRest
}

private fun EtsFunctionType.isBuiltinArrayType(): Boolean {
val parameter = signature.parameters.singleOrNull() ?: return false
val arrayType = signature.returnType as? EtsArrayType ?: return false
return signature.enclosingClass == EtsClassSignature.UNKNOWN &&
signature.name.isEmpty() &&
arrayType.elementType == EtsAnyType && arrayType.dimensions == 1 &&
parameter.type == EtsNumberType && parameter.isOptional && !parameter.isRest
}

private fun EtsValue.isLegacyBuiltinGlobal(
expectedName: String,
callee: EtsMethodSignature,
Expand Down
19 changes: 18 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,18 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
inputAdapter = TsDenseArrayModelSupport.reduceAdapter,
domainGuard = TsDenseArrayModelSupport.denseReceiverDomain,
),
sourceModel(
id = "ts.array.map",
methodName = "map",
inputAdapter = TsDenseArrayModelSupport.callbackAdapter,
domainGuard = TsArraySlotPrimitives.reverseDomain,
),
sourceModel(
id = "ts.array.forEach",
methodName = "forEach",
inputAdapter = TsDenseArrayModelSupport.callbackAdapter,
domainGuard = TsArraySlotPrimitives.reverseDomain,
),
sourceModel(
id = "ts.array.pop",
methodName = "pop",
Expand Down Expand Up @@ -438,7 +450,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
domainGuard = domainGuard,
inputAdapter = inputAdapter,
requiredModelIds = buildSet {
if (methodName in setOf("reverse", "unshift")) {
if (methodName in setOf("reverse", "unshift", "map", "forEach")) {
add("ts.array.primitive.prepareOwnSlots")
add("ts.array.primitive.hasOwnSlot")
}
Expand All @@ -457,6 +469,9 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
if (methodName in setOf("push", "unshift")) {
add(PRIMITIVE_GROW_ID)
}
if (methodName == "map") {
add(PRIMITIVE_ALLOCATE_ID)
}
if (methodName in setOf("slice", "concat")) {
add(PRIMITIVE_ALLOCATE_LIKE_ID)
}
Expand Down Expand Up @@ -585,6 +600,8 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
sizeSort = sizeSort,
count = length,
)
// Fresh allocations have known holes until the source algorithm writes each own slot.
knownArrayPropertyPresence += result
result
},
)
Expand Down
190 changes: 190 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionEtsIrModelFamily.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,190 @@
package org.usvm.machine.call.intrinsic

import org.jacodb.ets.model.EtsArrayType
import org.jacodb.ets.model.EtsClassSignature
import org.jacodb.ets.model.EtsClassType
import org.jacodb.ets.model.EtsStringType
import org.jacodb.ets.model.EtsType
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
import org.usvm.UConcreteHeapRef
import org.usvm.UExpr
import org.usvm.api.typeStreamOf
import org.usvm.machine.call.TsEtsIrUnknownCallModel
import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact
import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter
import org.usvm.machine.call.TsResidualCallPolicy
import org.usvm.machine.call.TsUnknownCallFailureReason
import org.usvm.machine.call.TsUnknownCallModel
import org.usvm.machine.call.TsUnknownCallModelCompletion
import org.usvm.machine.call.TsUnknownCallModelExecution
import org.usvm.machine.call.TsUnknownCallModelSuccessor
import org.usvm.machine.call.TsUnknownCallTarget
import org.usvm.machine.call.hasBuiltinGlobalOwner
import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact
import org.usvm.machine.expr.TsCollectionKind
import org.usvm.machine.expr.newModeledCollection
import org.usvm.machine.state.TsState
import org.usvm.types.singleOrNull
import org.usvm.util.arrayStorageType

/** Iterable construction executes normal source bodies over modeled native storage. */
internal object TsCollectionEtsIrModelFamily : TsBuiltInUnknownCallModelFamily {
private const val CLASS_NAME = "CollectionModels"
private const val PRIMITIVES_NAME = "CollectionModelPrimitives"
private val baseArtifact by lazy {
loadBundledEtsIrUnknownCallModelArtifact(
resourceName = "/org/usvm/machine/call/models/CollectionModels.ts",
sourceFileName = "CollectionModels.ts",
entryPointClassName = CLASS_NAME,
entryPointMethodName = "arrayFrom",
)
}
private val sourceModelIds by lazy { models.filterIsInstance<TsEtsIrUnknownCallModel>().map { it.id }.toSet() }

override val models: List<TsUnknownCallModel> by lazy {
listOf(
constructor(kind = TsCollectionKind.MAP, name = "Map"),
constructor(kind = TsCollectionKind.SET, name = "Set"),
populate(kind = TsCollectionKind.MAP, name = "Map"),
populate(kind = TsCollectionKind.SET, name = "Set"),
initializer(kind = TsCollectionKind.MAP, name = "initializeMap"),
initializer(kind = TsCollectionKind.SET, name = "initializeSet"),
arrayFromModel(),
)
}

private fun arrayFromModel(): TsUnknownCallModel = TsEtsIrUnknownCallModel(
id = "ts.array.fromIterable",
target = TsUnknownCallTarget(methodName = "from"),
artifact = artifact("arrayFrom"),
inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
val owner = call.receiver?.source ?: return@TsEtsIrUnknownCallModelInputAdapter null
if (!hasBuiltinGlobalOwner(owner, call.callee, expectedName = "Array")) {
return@TsEtsIrUnknownCallModelInputAdapter null
}
val arguments = call.arguments.map {
it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null
}
val input = arguments.firstOrNull() ?: return@TsEtsIrUnknownCallModelInputAdapter null
val mapping = arguments.getOrNull(1) ?: state.ctx.mkUndefinedValue()
val supportedInput = state.supportsIterable(input, call.arguments[0].source.type)
if (mapping != state.ctx.mkUndefinedValue() || !supportedInput) {
return@TsEtsIrUnknownCallModelInputAdapter null
}
listOf(input)
},
requiredModelIds = setOf(
"ts.array.push",
"ts.array.primitive.grow",
TsIteratorModelFamily.COLLECTION_ITERATOR_ID,
),
)


private fun constructor(kind: TsCollectionKind, name: String): TsUnknownCallModel {
val entry = if (kind == TsCollectionKind.MAP) "mapConstructor" else "setConstructor"
val initialize = if (kind == TsCollectionKind.MAP) "initializeMap" else "initializeSet"
val signature = EtsClassSignature.UNKNOWN.copy(name = name)
return TsEtsIrUnknownCallModel(
id = "ts.${name.lowercase()}.constructor",
target = TsUnknownCallTarget(methodName = CONSTRUCTOR_NAME, enclosingClassName = name),
artifact = artifact(entry),
inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
val receiver = call.receiver?.resolved as? UConcreteHeapRef
?: return@TsEtsIrUnknownCallModelInputAdapter null
val runtimeType = state.memory.typeStreamOf(receiver).singleOrNull()
if (call.callee.enclosingClass != signature || runtimeType != EtsClassType(signature)) {
return@TsEtsIrUnknownCallModelInputAdapter null
}
val arguments = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null }
val input = arguments.firstOrNull() ?: state.ctx.mkUndefinedValue()
listOf(receiver, input)
},
requiredModelIds = setOf("ts.collection.primitive.$initialize"),
)
}

// Optional populate helpers keep the original constructor model usable without iterable models.
private fun populate(kind: TsCollectionKind, name: String): TsUnknownCallModel {
val entry = if (kind == TsCollectionKind.MAP) "mapFromIterable" else "setFromIterable"
val helper = if (kind == TsCollectionKind.MAP) "populateMap" else "populateSet"
val initialize = if (kind == TsCollectionKind.MAP) "initializeMap" else "initializeSet"
val operation = if (kind == TsCollectionKind.MAP) "set" else "add"
return TsEtsIrUnknownCallModel(
id = "ts.${name.lowercase()}.fromIterable",
target = TsUnknownCallTarget(
methodName = helper,
enclosingClassName = PRIMITIVES_NAME,
failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
),
artifact = artifact(entry),
inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
val sourceFile = baseArtifact.file
val helperSignature = sourceFile.allClasses.single { it.name == PRIMITIVES_NAME }.signature
val caller = call.callSite.location.method
val sourceCaller = caller.signature.enclosingClass
val ownedCall = call.callee.enclosingClass == helperSignature &&
sourceCaller == baseArtifact.entryPoint.signature.enclosingClass &&
state.isUnknownCallModelActive("ts.${name.lowercase()}.constructor")
if (!ownedCall) return@TsEtsIrUnknownCallModelInputAdapter null
val inputs = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null }
if (inputs.size != 2) return@TsEtsIrUnknownCallModelInputAdapter null
val supportedInput = state.supportsIterable(inputs[1], call.arguments[1].source.type)
if (!supportedInput) {
return@TsEtsIrUnknownCallModelInputAdapter null
}
inputs
},
requiredModelIds = setOf(
"ts.collection.primitive.$initialize",
"ts.collection.$operation",
"ts.typeError.constructor",
TsIteratorModelFamily.COLLECTION_ITERATOR_ID,
),
)
}

private fun initializer(kind: TsCollectionKind, name: String): TsUnknownCallModel = TsPrimitiveUnknownCallModel(
idPrefix = "ts.collection.primitive",
methodName = name,
enclosingClassName = PRIMITIVES_NAME,
arity = 1,
helperClassSignature = { baseArtifact.file.allClasses.single { it.name == PRIMITIVES_NAME }.signature },
sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass },
owningModelIds = { sourceModelIds },
implementation = { state, inputs ->
val receiver = inputs.single() as? UConcreteHeapRef
if (receiver == null) {
null
} else {
val successor = TsUnknownCallModelSuccessor(
guard = state.ctx.trueExpr,
completion = TsUnknownCallModelCompletion.Normal {
modeledCollections += receiver to newModeledCollection(kind)
ctx.mkUndefinedValue()
},
)
TsUnknownCallModelExecution(successors = listOf(successor))
}
},
unsupportedCallPolicy = TsResidualCallPolicy.STOP_PATH,
)

private fun TsState.supportsIterable(input: UExpr<*>, staticType: EtsType): Boolean {
val reference = input as? UConcreteHeapRef ?: return false
val knownNative = reference in modeledCollections || reference in collectionIterators ||
reference in arrayIterators || reference in stringIterators
if (knownNative) return true
val type = arrayStorageType(reference, staticType)
return type is EtsArrayType || type == EtsStringType
}

private fun artifact(name: String): TsEtsIrUnknownCallModelArtifact {
val artifact = baseArtifact
val method = artifact.file.allClasses
.single { it.name == CLASS_NAME }
.methods
.single { it.name == name }
return artifact.copy(entryPoint = method)
}
}
47 changes: 6 additions & 41 deletions usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,38 +1,30 @@
package org.usvm.machine.call.intrinsic

import org.jacodb.ets.model.EtsClassSignature
import org.jacodb.ets.model.EtsClassType
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
import org.usvm.UConcreteHeapRef
import org.usvm.api.typeStreamOf
import org.usvm.isFalse
import org.usvm.machine.call.TsUnknownCall
import org.usvm.machine.call.TsUnknownCallFailureReason
import org.usvm.machine.call.TsUnknownCallModel
import org.usvm.machine.call.TsUnknownCallModelCompletion
import org.usvm.machine.call.TsUnknownCallModelExecution
import org.usvm.machine.call.TsUnknownCallModelSuccessor
import org.usvm.machine.call.TsUnknownCallTarget
import org.usvm.machine.expr.TsCollectionKind
import org.usvm.machine.expr.collectionClear
import org.usvm.machine.expr.collectionGet
import org.usvm.machine.expr.collectionInsert
import org.usvm.machine.expr.collectionMatches
import org.usvm.machine.expr.collectionPut
import org.usvm.machine.expr.collectionRemove
import org.usvm.machine.expr.collectionUndefined
import org.usvm.machine.expr.collectionValue
import org.usvm.machine.expr.newModeledCollection
import org.usvm.machine.state.TsState
import org.usvm.machine.types.iteUnresolvedValue
import org.usvm.types.singleOrNull

/** Empty native constructors and a bounded coherent subset of Map/Set operations. */
/** A bounded coherent subset of native Map/Set operations. */
internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily {
private const val MAX_ENTRIES = 16

override val models: List<TsUnknownCallModel> = listOf(
ConstructorModel(kind = TsCollectionKind.MAP, name = "Map"),
ConstructorModel(kind = TsCollectionKind.SET, name = "Set"),
OperationModel(operation = "get"),
OperationModel(operation = "set"),
OperationModel(operation = "add"),
Expand All @@ -41,35 +33,6 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily {
OperationModel(operation = "clear"),
)

private class ConstructorModel(private val kind: TsCollectionKind, name: String) : TsUnknownCallModel {
private val signature = EtsClassSignature.UNKNOWN.copy(name = name)
override val id = "ts.${name.lowercase()}.constructor"
override val target = TsUnknownCallTarget(
methodName = CONSTRUCTOR_NAME,
enclosingClassName = name,
failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND,
)

override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) {
val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return null
if (call.callee.enclosingClass != signature) return null
val runtimeType = state.memory.typeStreamOf(receiver).singleOrNull()
val nativeType = EtsClassType(signature)
if (runtimeType != nativeType) return null
val arguments = call.arguments.map { it.resolved ?: return null }
val emptyInput = arguments.isEmpty() || arguments.first() == mkUndefinedValue() ||
arguments.first() == mkTsNullValue()
if (!emptyInput) return null

val successor = TsUnknownCallModelSuccessor(
guard = trueExpr,
completion = TsUnknownCallModelCompletion.Normal { receiver },
applyStateChanges = { modeledCollections += receiver to newModeledCollection(kind = kind) },
)
TsUnknownCallModelExecution(successors = listOf(successor))
}
}

private class OperationModel(private val operation: String) : TsUnknownCallModel {
override val id = "ts.collection.$operation"
override val target = TsUnknownCallTarget(methodName = operation)
Expand All @@ -86,7 +49,7 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily {
guard = trueExpr,
completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
applyStateChanges = {
modeledCollections += receiver to newModeledCollection(kind = collection.kind)
collectionClear(receiver, collection)
},
)
return TsUnknownCallModelExecution(successors = listOf(successor))
Expand Down Expand Up @@ -135,7 +98,9 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily {
TsUnknownCallModelSuccessor(
guard = match.guard,
completion = TsUnknownCallModelCompletion.Normal { receiver },
applyStateChanges = { collectionPut(collection, match.key, value) },
applyStateChanges = {
if (collection.kind == TsCollectionKind.MAP) collectionPut(collection, match.key, value)
},
)
}.toMutableList()
val canInsert = collection.keys.size < MAX_ENTRIES
Expand Down
13 changes: 13 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,19 @@ internal object TsDenseArrayModelSupport {
}
}

// A non-undefined thisArg requires the callback invocation machinery to bind `this` explicitly.
val callbackAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null
val arguments = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null }
val callback = arguments.firstOrNull() as? UConcreteHeapRef
?: return@TsEtsIrUnknownCallModelInputAdapter null
if (callback !in state.associatedFunction) return@TsEtsIrUnknownCallModelInputAdapter null
val thisArgument = arguments.getOrNull(1) ?: state.ctx.mkUndefinedValue()
if (thisArgument != state.ctx.mkUndefinedValue()) return@TsEtsIrUnknownCallModelInputAdapter null

listOf(receiver, callback)
}

val reduceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call ->
val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2)
?: return@TsEtsIrUnknownCallModelInputAdapter null
Expand Down
Loading
Loading