[TS PBT] Project properties and search violations with USVM

usvm-ts-pbt/DESIGN.md

@@ -245,6 +245,21 @@ useful separation is preserved: declarative receiver/argument/result positions a
 values, and condition interpretation is distinct from position resolution. The TypeScript mapper expresses this
 with EtsIR-specific binding and mapping records and has no dependency on `usvm-jvm` or the taint-analysis module.
 
+## USVM projection and property search
+
+The existing projection path configures `TsMachine`'s initial state from exact mapper bindings and declared Kotlin
+domains. The existing search path prepends a mapped synchronous precondition to the predicate entry point. Guard
+completion is explicit in `TsState`: false terminates a rejected path, while an exception or non-boolean result
+terminates an error path. Neither path can reach the predicate target.
+
+Predicate false paths are re-solved on a cloned terminal state before target propagation, so the ordinary terminal
+state is not rewritten. Predicate exceptions reach the same candidate target. Runtime non-boolean entry-point
+results are property errors regardless of their TypeScript return annotation. A residual call that stops a path is
+unsupported, while ordinary unsatisfiable path pruning is not an engine failure. Timeout, solver uncertainty,
+interpreter failure, and candidate-input resolution failure retain separate search outcomes. Candidate extraction
+reads the projected input state with the terminal model, so predicate-local array mutation does not rewrite the
+reported input.
+
 ## Process supervision
 
 `FastCheckProcessTransport` writes stdin and drains stdout and stderr concurrently. This is necessary because each
@@ -284,7 +299,9 @@ classifier because `tsx` depends on a native esbuild package.
 - Backend integration tests execute real uncompiled TypeScript through the packaged adapter, including replay,
   shrinking, explicit examples, preconditions, async predicates, and timeouts.
 - Shared contract fixtures cover precondition admission, discard and errors; predicate violations and errors;
-  special values; aliases; mutation isolation; shrinking; and replay through observable outcomes.
+  special values; aliases; mutation isolation; shrinking; and replay through observable outcomes. One focused JVM
+  conformance test executes the same classification fixture through the real FastCheck and USVM paths, including
+  literal and never return annotations and replay of a pre-mutation USVM candidate.
 - Coverage golden tests assert literal TypeScript statement and branch outcomes for successful and falsified runs,
   cross-property isolation, scope and glob filtering, and source-map/report diagnostics.
 - Mapping golden tests load stable TypeScript fixtures through the native frontend and cover predicate,
@@ -297,5 +314,5 @@ classifier because `tsx` depends on a native esbuild package.
 - Discovering properties by scanning TypeScript source roots.
 - Compiling user TypeScript as part of the PBT workflow.
 - Reimplementing generation, replay, skip accounting, or shrinking in Kotlin.
-- Constructing symbolic inputs or executing mapped properties in USVM.
+- General purity analysis, arbitrary mutable-object projection, and persistent state across property invocations.
 - Combining backend source coverage with future EtsIR replay coverage.

usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md

@@ -85,10 +85,10 @@ was reached within that search.
 - `fast-check-adapter/src/execute-property.ts` applies this contract to generation, explicit examples, replay, and
   shrinking through the existing fast-check invocation.
 - `fast-check-adapter/src/project-domain.ts` projects the declared Kotlin domains for concrete execution.
-- Downstream USVM projection and search implementations consume the same manifest and mapping artifacts and must
-  link to this contract when their dependent changes are integrated.
-- `src/test/resources/properties/contract/PropertyExecutionContract.ts` provides concrete regression coverage;
-  downstream symbolic integration extends the same fixture with symbolic assertions.
+- `UsvmPropertyProjector` and `UsvmPropertySearcher` apply this contract to the existing USVM projection and search
+  paths. `PropertyExecutionConformanceTest` runs the same TypeScript fixture through `FastCheckBackend` and USVM.
+- `src/test/resources/properties/contract/PropertyExecutionContract.ts` is the shared observable fixture for
+  concrete and symbolic contract regressions.
 
 Replay remains ordinary concrete execution with the reported seed and path. It does not introduce a separate
 property runner or alternate callback semantics.

usvm-ts-pbt/README.md

@@ -204,6 +204,31 @@ Stable mapping diagnostics include `mapping.entry-point.unmapped`, `mapping.entr
 separately from mapping provenance and
 backend diagnostics are copied without reinterpretation.
 
+## USVM projection and property search
+
+`UsvmProjectionCapabilityResolver` compares the declared domains with the exact EtsIR parameter bindings.
+Booleans, bounded integers and numbers, supported primitive constants, optionals, bounded tuples, and bounded
+arrays are projected by `UsvmDomainProjector`. Strings are an explicit over-approximation: USVM constrains their
+type and UTF-16 length but not their contents. Nested arrays, incompatible EtsIR types, and collections above
+`UsvmProjectionOptions.maxSymbolicCollectionLength` are unsupported with stable diagnostics.
+
+`UsvmPropertyProjector` executes a mapped synchronous precondition over projected inputs. It reports accepted and
+rejected domains separately; a reachable exception or non-boolean result is `PROPERTY_ERROR`, solver uncertainty is
+`SOLVER_UNKNOWN`, and async, non-exact, or unsupported residual-call execution is `UNSUPPORTED`.
+
+`UsvmPropertySearcher` evaluates the mapped precondition and predicate in one symbolic state. A false precondition
+is `PRECONDITION_REJECTED` when it excludes the complete projected domain. A precondition exception or non-boolean
+result is `PROPERTY_ERROR`. Predicate `false` and escaping predicate exceptions are `VIOLATION_REACHED`, while a
+non-boolean predicate is `PROPERTY_ERROR`. Timeout, solver uncertainty, unsupported execution, engine failure, and
+input-resolution failure retain distinct statuses and are never treated as proof or as violations.
+
+The shared fixture in `src/test/resources/properties/contract/PropertyExecutionContract.ts` is executed by both
+`FastCheckBackend` and the USVM projection/search path. It covers precondition admission, rejection, exception and
+non-boolean results, plus false, throwing, literal-boolean-typed, never-typed, and non-boolean predicates. A shared
+mutation regression also verifies that a USVM candidate is reconstructed from the input before predicate mutation
+and reproduces through fast-check. Special values, alias preservation, mutation isolation, shrinking, and replay
+remain covered at the concrete invocation boundary.
+
 ## Registries and CLI
 
 The CLI loads Kotlin property registries through `ServiceLoader`:

usvm-ts-pbt/build.gradle.kts

@@ -7,6 +7,7 @@ plugins {
 }
 
 dependencies {
+    implementation(project(":usvm-core"))
     implementation(project(":usvm-ts"))
     implementation(Libs.jacodb_ets)
     implementation(Libs.clikt)

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt

@@ -61,6 +61,26 @@ internal object PbtDiagnosticCode {
     const val MAPPING_STATEMENT_AMBIGUOUS = "mapping.statement.ambiguous"
     const val MAPPING_STATEMENT_UNMAPPED = "mapping.statement.unmapped"
 
+    const val USVM_DOMAIN_ARRAY_NESTED_UNSUPPORTED = "usvm.domain.array.nested.unsupported"
+    const val USVM_DOMAIN_COLLECTION_TOO_LARGE = "usvm.domain.collection.too-large"
+    const val USVM_DOMAIN_STRING_APPROXIMATE = "usvm.domain.string.approximate"
+    const val USVM_DOMAIN_TYPE_UNSUPPORTED = "usvm.domain.type.unsupported"
+    const val USVM_ENGINE_FAILURE = "usvm.engine.failure"
+    const val USVM_EXECUTION_UNSUPPORTED = "usvm.execution.unsupported"
+    const val USVM_INPUT_BINDING_UNAVAILABLE = "usvm.input.binding.unavailable"
+    const val USVM_INPUT_RESOLUTION_FAILED = "usvm.input.resolution.failed"
+    const val USVM_MAPPING_PROPERTY_ID_MISMATCH = "usvm.mapping.property-id.mismatch"
+    const val USVM_PRECONDITION_ASYNC = "usvm.precondition.async"
+    const val USVM_PRECONDITION_BINDING_UNAVAILABLE = "usvm.precondition.binding.unavailable"
+    const val USVM_PRECONDITION_MAPPING_NON_EXACT = "usvm.precondition.mapping.non-exact"
+    const val USVM_PRECONDITION_MAPPING_UNAVAILABLE = "usvm.precondition.mapping.unavailable"
+    const val USVM_PRECONDITION_RESULT_NON_BOOLEAN = "usvm.precondition.result.non-boolean"
+    const val USVM_PRECONDITION_THREW = "usvm.precondition.threw"
+    const val USVM_PREDICATE_ASYNC = "usvm.predicate.async"
+    const val USVM_PREDICATE_MAPPING_NON_EXACT = "usvm.predicate.mapping.non-exact"
+    const val USVM_PREDICATE_RESULT_NON_BOOLEAN = "usvm.predicate.result.non-boolean"
+    const val USVM_SOLVER_UNKNOWN = "usvm.solver.unknown"
+
     const val PROTOCOL_REQUEST_INVALID = "protocol.request.invalid"
     const val SOURCE_ROOT_INVALID = "source-root.invalid"
 

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt

@@ -0,0 +1,178 @@
+package org.usvm.ts.pbt.usvm
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsTupleType
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.isTrue
+import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.expr.extractDouble
+import org.usvm.machine.expr.extractInt
+import org.usvm.machine.expr.toConcreteBoolValue
+import org.usvm.machine.state.TsState
+import org.usvm.sizeSort
+import org.usvm.ts.pbt.model.ArrayDomain
+import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ConstantDomain
+import org.usvm.ts.pbt.model.IntegerDomain
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.OptionalDomain
+import org.usvm.ts.pbt.model.PropertyDomain
+import org.usvm.ts.pbt.model.PropertyInput
+import org.usvm.ts.pbt.model.StringDomain
+import org.usvm.ts.pbt.model.TupleDomain
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+
+internal class UsvmCandidateInputResolver {
+    fun resolve(
+        state: TsState,
+        declaredInputs: List<PropertyInput>,
+        projection: UsvmDeclaredDomainProjection,
+    ): List<JsConcreteValue> {
+        require(declaredInputs.size == projection.inputs.size)
+        val initialState = projection.initialState.clone()
+        initialState.models = state.models
+
+        return declaredInputs.zip(projection.inputs).map { (input, projected) ->
+            resolveValue(
+                state = initialState,
+                domain = input.domain,
+                etsType = projected.etsType,
+                value = projected.value,
+            )
+        }
+    }
+
+    private fun resolveValue(
+        state: TsState,
+        domain: PropertyDomain,
+        etsType: EtsType,
+        value: UExpr<out USort>,
+    ): JsConcreteValue = with(state.ctx) {
+        if (value.isFakeObject()) {
+            return@with resolveFakeValue(state, domain, etsType, value)
+        }
+
+        when (domain) {
+            BooleanDomain -> JsConcreteValue.Boolean(
+                state.models.single().eval(value.asExpr(boolSort)).toConcreteBoolValue(),
+            )
+
+            is IntegerDomain, is NumberDomain -> JsConcreteValue.number(
+                state.models.single().eval(value.asExpr(fp64Sort)).extractDouble(),
+            )
+
+            is StringDomain -> resolveString(state, value)
+            is ConstantDomain -> domain.value
+            is OptionalDomain -> resolveOptional(state, domain, etsType, value)
+            is TupleDomain -> resolveTuple(state, domain, etsType, value)
+            is ArrayDomain -> resolveArray(state, domain, etsType as EtsArrayType, value)
+        }
+    }
+
+    private fun resolveFakeValue(
+        state: TsState,
+        domain: PropertyDomain,
+        etsType: EtsType,
+        value: UConcreteHeapRef,
+    ): JsConcreteValue = with(state.ctx) {
+        val model = state.models.single()
+        val fakeType = value.getFakeType(state.memory)
+        val selected = when {
+            model.eval(fakeType.boolTypeExpr).isTrue -> value.extractBool(state.memory)
+            model.eval(fakeType.fpTypeExpr).isTrue -> value.extractFp(state.memory)
+            model.eval(fakeType.refTypeExpr).isTrue -> value.extractRef(state.memory)
+            else -> error("Cannot resolve the selected fake-object type")
+        }
+
+        resolveValue(state, domain, etsType, selected)
+    }
+
+    private fun resolveOptional(
+        state: TsState,
+        domain: OptionalDomain,
+        etsType: EtsType,
+        value: UExpr<out USort>,
+    ): JsConcreteValue = with(state.ctx) {
+        if (value.sort == addressSort) {
+            val ref = value.asExpr(addressSort)
+            val nil = when (domain.nil) {
+                JsConcreteValue.Null -> mkTsNullValue()
+                JsConcreteValue.Undefined -> mkUndefinedValue()
+                else -> error("Optional nil must be null or undefined")
+            }
+            if (state.models.single().eval(mkHeapRefEq(ref, nil)).isTrue) {
+                return@with domain.nil
+            }
+        }
+
+        val nestedType = (etsType as org.jacodb.ets.model.EtsUnionType).types.first { type ->
+            UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type)
+        }
+
+        resolveValue(state, domain.value, nestedType, value)
+    }
+
+    private fun resolveString(state: TsState, value: UExpr<out USort>): JsConcreteValue.String = with(state.ctx) {
+        val ref = state.models.single().eval(value.asExpr(addressSort)) as? UConcreteHeapRef
+            ?: error("Symbolic string reference did not resolve to a concrete heap reference")
+        val concrete = getStringConstantValue(ref)
+            ?: error("Symbolic string contents are unavailable")
+
+        JsConcreteValue.String(concrete)
+    }
+
+    private fun resolveTuple(
+        state: TsState,
+        domain: TupleDomain,
+        etsType: EtsType,
+        value: UExpr<out USort>,
+    ): JsConcreteValue.Array = with(state.ctx) {
+        val ref = state.models.single().eval(value.asExpr(addressSort)) as UConcreteHeapRef
+        val elementTypes = when (etsType) {
+            is EtsTupleType -> etsType.types
+            is EtsArrayType -> List(domain.elements.size) { etsType.elementType }
+            else -> error("Unsupported tuple EtsIR type $etsType")
+        }
+        val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+        val elements = domain.elements.zip(elementTypes).mapIndexed { index, (elementDomain, elementType) ->
+            val lValue = mkArrayIndexLValue(addressSort, ref, mkBv(index), arrayType)
+            val element = state.memory.read(lValue)
+
+            resolveValue(state, elementDomain, elementType, element)
+        }
+
+        JsConcreteValue.Array(elements)
+    }
+
+    private fun resolveArray(
+        state: TsState,
+        domain: ArrayDomain,
+        etsType: EtsArrayType,
+        value: UExpr<out USort>,
+    ): JsConcreteValue.Array = with(state.ctx) {
+        val ref = state.models.single().eval(value.asExpr(addressSort)) as UConcreteHeapRef
+        val lengthLValue = mkArrayLengthLValue(ref, etsType)
+        val length = state.models.single()
+            .eval(state.memory.read(lengthLValue).asExpr(sizeSort))
+            .extractInt()
+        val elementSort = typeToSort(arrayDescriptorOf(etsType).let { it as EtsArrayType }.elementType)
+        val elements = (0 until length).map { index ->
+            val element = if (elementSort is TsUnresolvedSort) {
+                state.memory.read(mkArrayIndexLValue(addressSort, ref, mkBv(index), etsType))
+            } else {
+                state.memory.read(mkArrayIndexLValue(elementSort, ref, mkBv(index), etsType))
+            }
+
+            resolveValue(state, domain.element, etsType.elementType, element)
+        }
+
+        JsConcreteValue.Array(elements)
+    }
+}