From 4e0fe891244b9a3fb14c9083ee8ac6c9101a7497 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 09:51:30 +0300 Subject: [PATCH 1/2] [TS PBT] Integrate USVM property execution contract --- usvm-ts-pbt/DESIGN.md | 21 +- usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md | 8 +- usvm-ts-pbt/README.md | 25 + usvm-ts-pbt/build.gradle.kts | 1 + .../org/usvm/ts/pbt/PbtDiagnosticCode.kt | 20 + .../ts/pbt/usvm/UsvmCandidateInputResolver.kt | 178 +++++++ .../usvm/ts/pbt/usvm/UsvmDomainProjector.kt | 393 ++++++++++++++++ .../usvm/UsvmProjectionCapabilityResolver.kt | 352 ++++++++++++++ .../usvm/ts/pbt/usvm/UsvmProjectionModel.kt | 30 ++ .../usvm/ts/pbt/usvm/UsvmPropertyProjector.kt | 310 ++++++++++++ .../ts/pbt/usvm/UsvmPropertySearchModel.kt | 54 +++ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 441 ++++++++++++++++++ .../usvm/PropertyExecutionConformanceTest.kt | 263 +++++++++++ .../usvm/UsvmCollectionDomainProjectorTest.kt | 175 +++++++ .../usvm/UsvmInitialStateConfigurationTest.kt | 110 +++++ .../usvm/UsvmPreconditionProjectionTest.kt | 124 +++++ .../pbt/usvm/UsvmProjectionCapabilityTest.kt | 208 +++++++++ .../pbt/usvm/UsvmProjectionConformanceTest.kt | 48 ++ .../ts/pbt/usvm/UsvmPropertySearcherTest.kt | 231 +++++++++ .../pbt/usvm/UsvmScalarDomainProjectorTest.kt | 245 ++++++++++ .../contract/PropertyExecutionContract.ts | 12 + .../resources/usvm/UsvmCapabilityFixture.ts | 31 ++ .../resources/usvm/UsvmPreconditionFixture.ts | 27 ++ .../usvm/UsvmPropertySearchFixture.ts | 71 +++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 72 ++- .../kotlin/org/usvm/machine/TsMethodCall.kt | 14 + .../usvm/machine/interpreter/TsInterpreter.kt | 109 ++++- .../kotlin/org/usvm/machine/state/TsState.kt | 15 + .../org/usvm/machine/state/TsStateUtils.kt | 23 + 29 files changed, 3578 insertions(+), 33 deletions(-) create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt create mode 100644 usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt create mode 100644 usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts create mode 100644 usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts diff --git a/usvm-ts-pbt/DESIGN.md b/usvm-ts-pbt/DESIGN.md index 72ef500643..f4c18201ee 100644 --- a/usvm-ts-pbt/DESIGN.md +++ b/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. diff --git a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md b/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md index e91f20c26b..83aa9c856a 100644 --- a/usvm-ts-pbt/PROPERTY_EXECUTION_CONTRACT.md +++ b/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. diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 6219768fd5..fdd4bc0997 100644 --- a/usvm-ts-pbt/README.md +++ b/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`: diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts index afc82d9f47..a76e672747 100644 --- a/usvm-ts-pbt/build.gradle.kts +++ b/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) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt index 65dbf5170d..a31d8463a9 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt +++ b/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" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt new file mode 100644 index 0000000000..1e7a584632 --- /dev/null +++ b/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, + projection: UsvmDeclaredDomainProjection, + ): List { + 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, + ): 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, + ): 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): 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, + ): 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, + ): 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) + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt new file mode 100644 index 0000000000..3f70b7b6e5 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -0,0 +1,393 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UAddressSort +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.api.initializeArrayLength +import org.usvm.api.makeSymbolicPrimitive +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.machine.types.mkFakeValue +import org.usvm.sizeSort +import org.usvm.ts.pbt.mapping.EtsInputBinding +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.mkRegisterStackLValue + +/** One symbolic input written to the mapped EtsIR stack slot. */ +data class UsvmProjectedInput( + val inputName: String, + val path: String, + val stackSlot: Int, + val etsType: EtsType, + val value: UExpr, +) + +/** Constraints created exclusively from declared Kotlin property domains. */ +data class UsvmDeclaredDomainProjection( + val inputs: List, + val initialState: TsState, +) + +/** Materializes declared property domains in a real USVM TypeScript initial state. */ +class UsvmDomainProjector( + private val options: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + fun configure( + state: TsState, + inputs: List, + bindings: List, + ): UsvmDeclaredDomainProjection { + require(inputs.size == bindings.size) { + "Property input count ${inputs.size} does not match EtsIR binding count ${bindings.size}" + } + + val preparedInputs = inputs.zip(bindings).mapIndexed { index, (input, binding) -> + require(input.name == binding.propertyInputName) { + "Property input ${input.name} does not match EtsIR binding ${binding.propertyInputName}" + } + + val path = "inputs[$index].domain" + val capability = UsvmProjectionCapabilityResolver().domainCapabilityForProjector( + domain = input.domain, + etsType = binding.parameter.type, + path = path, + options = options, + ) + + PreparedInput(input, binding, path, capability) + } + preparedInputs.forEach { prepared -> + require(prepared.capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { + prepared.capability.diagnostics.joinToString { diagnostic -> diagnostic.message } + } + } + + val projectedInputs = preparedInputs.map { prepared -> + val input = prepared.input + val binding = prepared.binding + val path = prepared.path + + val value = Materializer(state).materialize(input.domain, binding.parameter.type) + writeStackValue(state, binding.stackSlot, value) + + UsvmProjectedInput( + inputName = input.name, + path = path, + stackSlot = binding.stackSlot, + etsType = binding.parameter.type, + value = value, + ) + } + + return UsvmDeclaredDomainProjection( + inputs = projectedInputs, + initialState = state.clone(), + ) + } + + private data class PreparedInput( + val input: PropertyInput, + val binding: EtsInputBinding, + val path: String, + val capability: org.usvm.ts.pbt.backend.ProjectionCapability, + ) + + private inner class Materializer(private val state: TsState) { + fun materialize(domain: PropertyDomain, etsType: EtsType): UExpr = when (domain) { + BooleanDomain -> state.makeSymbolicPrimitive(state.ctx.boolSort) + is IntegerDomain -> materializeInteger(domain) + is NumberDomain -> materializeNumber(domain) + is StringDomain -> materializeString(domain) + is ConstantDomain -> materializeConstant(domain.value) + is OptionalDomain -> materializeOptional(domain, etsType) + is TupleDomain -> materializeTuple(domain, etsType) + is ArrayDomain -> materializeArray(domain, etsType as EtsArrayType) + } + + private fun materializeInteger(domain: IntegerDomain): UExpr = with(state.ctx) { + val value = state.makeSymbolicPrimitive(fp64Sort) + val rounded = mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = value, + ) + val negativeZero = mkAnd(mkFpIsZeroExpr(value), mkFpIsNegativeExpr(value)) + val minimum = mkFp(domain.min.toDouble(), fp64Sort) + val maximum = mkFp(domain.max.toDouble(), fp64Sort) + val isNumber = mkFpIsNaNExpr(value).not() + val isIntegral = mkFpEqualExpr(value, rounded) + val meetsMinimum = mkFpGreaterOrEqualExpr(value, minimum) + val meetsMaximum = mkFpLessOrEqualExpr(value, maximum) + + state.pathConstraints += mkAnd( + isNumber, + isIntegral, + negativeZero.not(), + meetsMinimum, + meetsMaximum, + ) + + value + } + + private fun materializeNumber(domain: NumberDomain): UExpr = with(state.ctx) { + val value = state.makeSymbolicPrimitive(fp64Sort) + val minimum = mkFp(domain.min.toDouble(), fp64Sort) + val maximum = mkFp(domain.max.toDouble(), fp64Sort) + val meetsMinimum = mkFpGreaterOrEqualExpr(value, minimum) + val meetsMaximum = mkFpLessOrEqualExpr(value, maximum) + val insideBounds = mkAnd(meetsMinimum, meetsMaximum) + val constraint = if (domain.allowNaN) { + mkOr(mkFpIsNaNExpr(value), insideBounds) + } else { + insideBounds + } + + state.pathConstraints += constraint + + value + } + + private fun materializeString(domain: StringDomain): UConcreteHeapRef = with(state.ctx) { + val value = state.memory.allocConcrete(EtsStringType) + val stringArrayType = EtsArrayType(EtsStringType, dimensions = 1) + val descriptor = arrayDescriptorOf(stringArrayType) + val length = state.makeSymbolicPrimitive(sizeSort) + val minimumLength = mkBv(domain.minLength) + val maximumLength = mkBv(domain.maxLength) + val meetsMinimum = mkBvSignedGreaterOrEqualExpr(length, minimumLength) + val meetsMaximum = mkBvSignedLessOrEqualExpr(length, maximumLength) + + state.memory.initializeArrayLength(value, descriptor, sizeSort, length) + state.pathConstraints += mkAnd(meetsMinimum, meetsMaximum) + + value + } + + private fun materializeConstant(value: JsConcreteValue): UExpr = with(state.ctx) { + when (value) { + is JsConcreteValue.Boolean -> mkBool(value.value) + is JsConcreteValue.Number -> mkFp(value.toDouble(), fp64Sort) + is JsConcreteValue.String -> state.mkInitializedStringConstant(value.value) + JsConcreteValue.Null -> mkTsNullValue() + JsConcreteValue.Undefined -> mkUndefinedValue() + is JsConcreteValue.Array -> error("Array constants are not valid property-domain primitives") + } + } + + private fun materializeOptional( + domain: OptionalDomain, + etsType: EtsType, + ): UExpr = with(state.ctx) { + val unionType = etsType as EtsUnionType + val nestedType = unionType.types.first { type -> + UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type) + } + val nestedValue = materialize(domain.value, nestedType) + val nilValue = materializeConstant(domain.nil) + val chooseValue = state.makeSymbolicPrimitive(boolSort) + + if (nestedValue.sort == nilValue.sort) { + return@with sameSortIte(chooseValue, nestedValue, nilValue) + } + + val fakeValue = state.mkFakeValue( + scope = null, + boolValue = nestedValue.asOptionalBool(), + fpValue = nestedValue.asOptionalFp(), + refValue = (nestedValue.asOptionalRef() ?: nilValue.asOptionalRef()), + ) + val fakeType = fakeValue.getFakeType(state.memory) + val nestedTypeExpr = when (nestedValue.sort) { + boolSort -> fakeType.boolTypeExpr + fp64Sort -> fakeType.fpTypeExpr + addressSort -> fakeType.refTypeExpr + else -> error("Unsupported optional value sort ${nestedValue.sort}") + } + val nilTypeExpr = when (nilValue.sort) { + boolSort -> fakeType.boolTypeExpr + fp64Sort -> fakeType.fpTypeExpr + addressSort -> fakeType.refTypeExpr + else -> error("Unsupported optional nil sort ${nilValue.sort}") + } + + state.pathConstraints += mkEq(nestedTypeExpr, chooseValue) + state.pathConstraints += mkEq(nilTypeExpr, chooseValue.not()) + + fakeValue + } + + private fun materializeTuple( + domain: TupleDomain, + etsType: EtsType, + ): UConcreteHeapRef = with(state.ctx) { + 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 descriptor = arrayDescriptorOf(arrayType) + val array = state.memory.allocConcrete(descriptor) + + state.memory.initializeArrayLength(array, descriptor, sizeSort, mkBv(domain.elements.size)) + domain.elements.zip(elementTypes).forEachIndexed { index, (elementDomain, elementType) -> + val element = box(materialize(elementDomain, elementType)) + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = mkBv(index), + type = arrayType, + ) + + state.memory.write(lValue, element, guard = trueExpr) + } + + array + } + + private fun materializeArray( + domain: ArrayDomain, + etsType: EtsArrayType, + ): UConcreteHeapRef = with(state.ctx) { + val descriptor = arrayDescriptorOf(etsType) + val array = state.memory.allocConcrete(descriptor) + val length = state.makeSymbolicPrimitive(sizeSort) + val minimumLength = mkBv(domain.minLength) + val maximumLength = mkBv(domain.maxLength) + val meetsMinimum = mkBvSignedGreaterOrEqualExpr(length, minimumLength) + val meetsMaximum = mkBvSignedLessOrEqualExpr(length, maximumLength) + + state.memory.initializeArrayLength(array, descriptor, sizeSort, length) + state.pathConstraints += mkAnd(meetsMinimum, meetsMaximum) + + repeat(domain.maxLength) { index -> + val element = materialize(domain.element, etsType.elementType) + val guard = mkBvSignedLessExpr(mkBv(index), length) + + writeArrayElement(array, etsType, index, element, guard) + } + + array + } + + private fun writeArrayElement( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + index: Int, + value: UExpr, + guard: UBoolExpr, + ) = with(state.ctx) { + val descriptor = arrayDescriptorOf(arrayType) as EtsArrayType + val elementSort = typeToSort(descriptor.elementType) + if (elementSort is TsUnresolvedSort) { + val lValue = mkArrayIndexLValue( + sort = addressSort, + ref = array, + index = mkBv(index), + type = arrayType, + ) + + state.memory.write(lValue, box(value), guard) + } else { + writeArrayElementWithKnownSort(array, arrayType, index, value, guard, elementSort) + } + } + + private fun writeArrayElementWithKnownSort( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + index: Int, + value: UExpr, + guard: UBoolExpr, + sort: USort, + ) = with(state.ctx) { + when (sort) { + boolSort -> { + val lValue = mkArrayIndexLValue(boolSort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(boolSort), guard) + } + + fp64Sort -> { + val lValue = mkArrayIndexLValue(fp64Sort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(fp64Sort), guard) + } + + addressSort -> { + val lValue = mkArrayIndexLValue(addressSort, array, mkBv(index), arrayType) + + state.memory.write(lValue, value.asExpr(addressSort), guard) + } + + else -> error("Unsupported projected array element sort $sort") + } + } + + private fun box(value: UExpr): UConcreteHeapRef = with(state.ctx) { + if (value is UConcreteHeapRef && value.isFakeObject()) return@with value + + state.mkFakeValue( + scope = null, + boolValue = value.asOptionalBool(), + fpValue = value.asOptionalFp(), + refValue = value.asOptionalRef(), + ) + } + + private fun UExpr.asOptionalBool(): UExpr? = + takeIf { sort == state.ctx.boolSort }?.asExpr(state.ctx.boolSort) + + private fun UExpr.asOptionalFp(): UExpr? = + takeIf { sort == state.ctx.fp64Sort }?.asExpr(state.ctx.fp64Sort) + + private fun UExpr.asOptionalRef(): UExpr? = + takeIf { sort == state.ctx.addressSort }?.asExpr(state.ctx.addressSort) + + @Suppress("UNCHECKED_CAST") + private fun sameSortIte( + condition: UBoolExpr, + trueValue: UExpr, + falseValue: UExpr, + ): UExpr = state.ctx.mkIte( + condition, + trueValue as UExpr, + falseValue as UExpr, + ) + } +} + +private fun writeStackValue(state: TsState, stackSlot: Int, value: UExpr): Unit = with(state.ctx) { + require(value.sort == boolSort || value.sort == fp64Sort || value.sort == addressSort) { + "Unsupported projected stack sort ${value.sort}" + } + + val lValue = mkRegisterStackLValue(value.sort, stackSlot) + + state.memory.write(lValue, value.cast(), guard = trueExpr) + state.saveSortForLocal(stackSlot, value.sort) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt new file mode 100644 index 0000000000..1e183a0d35 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt @@ -0,0 +1,352 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanLiteralType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberLiteralType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringLiteralType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.aggregateProjectionCapabilities +import org.usvm.ts.pbt.backend.classifyPropertyCapability +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +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.ExecutionKind +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.StringDomain +import org.usvm.ts.pbt.model.TupleDomain + +/** Calculates USVM fidelity without constructing or mutating a symbolic state. */ +class UsvmProjectionCapabilityResolver { + fun resolve( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + options: UsvmProjectionOptions = UsvmProjectionOptions(), + ): UsvmPropertyProjectionCapability { + val predicateCapability = entryPointCapability( + mapping = mapping.predicate, + path = "predicate", + nonExactCode = PbtDiagnosticCode.USVM_PREDICATE_MAPPING_NON_EXACT, + ) + val predicateTarget = mapping.predicate.exactTargetOrNull() + val predicateExecutionCapability = if (manifest.predicate.executionKind == ExecutionKind.SYNC) { + exact() + } else { + unsupported( + code = PbtDiagnosticCode.USVM_PREDICATE_ASYNC, + message = "Asynchronous TypeScript predicates are not supported by USVM search", + path = "predicate", + ) + } + val inputCapabilities = manifest.inputs.mapIndexed { index, input -> + val path = "inputs[$index].domain" + val parameterType = predicateTarget + ?.bindings + ?.inputs + ?.getOrNull(index) + ?.parameter + ?.type + val capability = if (parameterType == null) { + unsupported( + code = PbtDiagnosticCode.USVM_INPUT_BINDING_UNAVAILABLE, + message = "An exact EtsIR input binding is required", + path = path, + ) + } else { + domainCapabilityForProjector(input.domain, parameterType, path, options) + } + + UsvmInputProjectionCapability( + inputName = input.name, + path = path, + capability = capability, + ) + } + val preconditionCapability = preconditionCapability(manifest, mapping, options) + val propertyIdCapability = if (mapping.propertyId.value == manifest.propertyId) { + exact() + } else { + unsupported( + code = PbtDiagnosticCode.USVM_MAPPING_PROPERTY_ID_MISMATCH, + message = "The property manifest and EtsIR mapping artifact have different IDs", + path = "propertyId", + ) + } + val symbolicComponents = buildList { + add(propertyIdCapability) + add(predicateCapability) + add(predicateExecutionCapability) + addAll(inputCapabilities.map { it.capability }) + add(preconditionCapability) + } + val symbolicCapability = aggregateProjectionCapabilities(symbolicComponents) + + return UsvmPropertyProjectionCapability( + inputs = inputCapabilities, + precondition = preconditionCapability, + symbolic = symbolicCapability, + property = classifyPropertyCapability(concreteCapability, symbolicCapability), + ) + } + + private fun preconditionCapability( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + options: UsvmProjectionOptions, + ): ProjectionCapability { + val declaredPrecondition = manifest.precondition ?: return exact() + if (declaredPrecondition.executionKind == ExecutionKind.ASYNC) { + return unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_ASYNC, + message = "Asynchronous TypeScript preconditions are not supported by USVM projection", + path = "precondition", + ) + } + + val mappedPrecondition = mapping.precondition + ?: return unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_MAPPING_UNAVAILABLE, + message = "The declared precondition has no EtsIR mapping", + path = "precondition", + ) + val mappingCapability = entryPointCapability( + mapping = mappedPrecondition, + path = "precondition", + nonExactCode = PbtDiagnosticCode.USVM_PRECONDITION_MAPPING_NON_EXACT, + ) + val target = mappedPrecondition.exactTargetOrNull() + ?: return mappingCapability + val inputCapabilities = manifest.inputs.mapIndexed { index, input -> + val parameterType = target.bindings.inputs + .getOrNull(index) + ?.parameter + ?.type + + if (parameterType == null) { + unsupported( + code = PbtDiagnosticCode.USVM_PRECONDITION_BINDING_UNAVAILABLE, + message = "An exact EtsIR precondition input binding is required", + path = "precondition", + ) + } else { + domainCapabilityForProjector(input.domain, parameterType, "inputs[$index].domain", options) + } + } + + return aggregateProjectionCapabilities(listOf(mappingCapability) + inputCapabilities) + } + + private fun entryPointCapability( + mapping: EtsMappingResult, + path: String, + nonExactCode: String, + ): ProjectionCapability = if (mapping.status == EtsMappingStatus.EXACT && mapping.targets.size == 1) { + exact() + } else { + unsupported( + code = nonExactCode, + message = "USVM projection requires exactly one EtsIR target, got ${mapping.status}", + path = path, + ) + } + + internal fun domainCapabilityForProjector( + domain: PropertyDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (!domainCompatibilityForProjector(domain, etsType)) { + return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED, + message = "Domain ${domain::class.simpleName} cannot be projected into EtsIR type $etsType", + path = path, + ) + } + + return when (domain) { + BooleanDomain, is IntegerDomain, is NumberDomain -> exact() + is StringDomain -> approximateString(path) + is ConstantDomain -> constantCapability(domain.value, path) + is OptionalDomain -> domainCapabilityForProjector( + domain = domain.value, + etsType = nestedOptionalType(domain, etsType), + path = "$path.value", + options = options, + ) + + is TupleDomain -> tupleCapability(domain, etsType, path, options) + is ArrayDomain -> arrayCapability(domain, etsType, path, options) + } + } + + private fun tupleCapability( + domain: TupleDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (domain.elements.size > options.maxSymbolicCollectionLength) { + return collectionTooLarge(domain.elements.size, options, path) + } + + val elementTypes = when (etsType) { + is EtsTupleType -> etsType.types + is EtsArrayType -> List(domain.elements.size) { etsType.elementType } + else -> return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED, + message = "Tuple domain requires an EtsIR tuple or array type", + path = path, + ) + } + val elementCapabilities = domain.elements.mapIndexed { index, element -> + domainCapabilityForProjector(element, elementTypes[index], "$path.elements[$index]", options) + } + + return aggregateProjectionCapabilities(elementCapabilities) + } + + private fun arrayCapability( + domain: ArrayDomain, + etsType: EtsType, + path: String, + options: UsvmProjectionOptions, + ): ProjectionCapability { + if (domain.maxLength > options.maxSymbolicCollectionLength) { + return collectionTooLarge(domain.maxLength, options, path) + } + if ((etsType as EtsArrayType).elementType is EtsArrayType) { + return unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_ARRAY_NESTED_UNSUPPORTED, + message = "Nested EtsIR arrays are not supported by the current TypeScript heap model", + path = path, + ) + } + + val elementType = etsType.elementType + + return domainCapabilityForProjector(domain.element, elementType, "$path.element", options) + } + + private fun collectionTooLarge( + actualLength: Int, + options: UsvmProjectionOptions, + path: String, + ) = unsupported( + code = PbtDiagnosticCode.USVM_DOMAIN_COLLECTION_TOO_LARGE, + message = "Collection length $actualLength exceeds the symbolic cap " + + options.maxSymbolicCollectionLength, + path = path, + ) + + internal fun domainCompatibilityForProjector(domain: PropertyDomain, etsType: EtsType): Boolean = when (domain) { + BooleanDomain -> etsType == EtsBooleanType || etsType is EtsBooleanLiteralType + is IntegerDomain, is NumberDomain -> etsType == EtsNumberType || etsType is EtsNumberLiteralType + is StringDomain -> etsType == EtsStringType || etsType is EtsStringLiteralType + is ConstantDomain -> isConstantCompatible(domain.value, etsType) + is OptionalDomain -> isOptionalCompatible(domain, etsType) + is TupleDomain -> when (etsType) { + is EtsTupleType -> { + etsType.types.size == domain.elements.size && + domain.elements.zip(etsType.types).all { (element, elementType) -> + domainCompatibilityForProjector(element, elementType) + } + } + + is EtsArrayType -> { + etsType.dimensions == 1 && + domain.elements.all { domainCompatibilityForProjector(it, etsType.elementType) } + } + + else -> false + } + + is ArrayDomain -> { + etsType is EtsArrayType && + etsType.dimensions == 1 && + domainCompatibilityForProjector(domain.element, etsType.elementType) + } + } + + private fun isConstantCompatible(value: JsConcreteValue, etsType: EtsType): Boolean = when (value) { + is JsConcreteValue.Boolean -> etsType == EtsBooleanType || etsType is EtsBooleanLiteralType + is JsConcreteValue.Number -> etsType == EtsNumberType || etsType is EtsNumberLiteralType + is JsConcreteValue.String -> etsType == EtsStringType || etsType is EtsStringLiteralType + JsConcreteValue.Null -> etsType == EtsNullType + JsConcreteValue.Undefined -> etsType == EtsUndefinedType + is JsConcreteValue.Array -> false + } + + private fun isOptionalCompatible(domain: OptionalDomain, etsType: EtsType): Boolean { + val union = etsType as? EtsUnionType ?: return false + val nilType = nilType(domain.nil) ?: return false + + return union.types.any { it == nilType } && + union.types.any { domainCompatibilityForProjector(domain.value, it) } + } + + private fun nestedOptionalType(domain: OptionalDomain, etsType: EtsType): EtsType { + val union = etsType as EtsUnionType + + return union.types.first { domainCompatibilityForProjector(domain.value, it) } + } + + private fun nilType(nil: JsConcreteValue): EtsType? = when (nil) { + JsConcreteValue.Null -> EtsNullType + JsConcreteValue.Undefined -> EtsUndefinedType + else -> null + } + + private fun constantCapability(value: JsConcreteValue, path: String): ProjectionCapability = when (value) { + is JsConcreteValue.String -> approximateString(path) + else -> exact() + } + + private fun approximateString(path: String): ProjectionCapability { + val diagnostic = CapabilityDiagnostic( + code = PbtDiagnosticCode.USVM_DOMAIN_STRING_APPROXIMATE, + message = "Over-approximation: USVM constrains string type and length, " + + "but leaves UTF-16 contents unconstrained", + path = path, + ) + + return ProjectionCapability( + level = ProjectionLevel.APPROXIMATE, + diagnostics = listOf(diagnostic), + ) + } + + private fun unsupported(code: String, message: String, path: String): ProjectionCapability { + val diagnostic = CapabilityDiagnostic(code = code, message = message, path = path) + + return ProjectionCapability( + level = ProjectionLevel.UNSUPPORTED, + diagnostics = listOf(diagnostic), + ) + } + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) +} + +internal fun EtsMappingResult.exactTargetOrNull(): EtsEntryPointTarget? = + targets.singleOrNull()?.takeIf { status == EtsMappingStatus.EXACT } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt new file mode 100644 index 0000000000..8cbb6d46c4 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt @@ -0,0 +1,30 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.PropertyCapabilityLevel + +/** Bounds resource usage while recursively materializing symbolic property inputs. */ +data class UsvmProjectionOptions( + val maxSymbolicCollectionLength: Int = 10, +) { + init { + require(maxSymbolicCollectionLength >= 0) { + "Maximum symbolic collection length must be non-negative" + } + } +} + +/** Capability of one ordered property input at its stable manifest path. */ +data class UsvmInputProjectionCapability( + val inputName: String, + val path: String, + val capability: ProjectionCapability, +) + +/** Combined concrete and symbolic execution capability for one property. */ +data class UsvmPropertyProjectionCapability( + val inputs: List, + val precondition: ProjectionCapability, + val symbolic: ProjectionCapability, + val property: PropertyCapabilityLevel, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt new file mode 100644 index 0000000000..b8e9910946 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt @@ -0,0 +1,310 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact + +/** Overall result of projecting and evaluating one declared precondition. */ +enum class UsvmPreconditionStatus { + ACCEPTED, + REJECTED, + PROPERTY_ERROR, + TIMEOUT, + SOLVER_UNKNOWN, + UNSUPPORTED, + ENGINE_FAILURE, +} + +/** Capability and terminal states satisfying a declared mapped precondition. */ +data class UsvmPreconditionResult( + val capability: UsvmPropertyProjectionCapability, + val status: UsvmPreconditionStatus, + val acceptedStates: List, + val diagnostics: List, +) { + init { + if (status == UsvmPreconditionStatus.ACCEPTED) { + require(acceptedStates.isNotEmpty()) { "An accepted precondition requires at least one state" } + } else { + require(acceptedStates.isEmpty()) { "Only an accepted precondition can expose states" } + } + } +} + +/** Orchestrates declared-domain materialization and mapped TypeScript precondition execution. */ +class UsvmPropertyProjector( + private val scene: EtsScene, + private val machineOptions: UMachineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + ), + private val tsOptions: TsOptions = TsOptions(), + private val projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val capabilityResolver = UsvmProjectionCapabilityResolver() + private val domainProjector = UsvmDomainProjector(projectionOptions) + + fun analyzePrecondition( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + ): UsvmPreconditionResult { + requireNotNull(manifest.precondition) { "Precondition analysis requires a declared precondition" } + + val capability = capabilityResolver.resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + val capabilityDiagnostics = capability.symbolic.diagnostics + if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { + return result( + capability = capability, + status = UsvmPreconditionStatus.UNSUPPORTED, + diagnostics = capabilityDiagnostics, + ) + } + + val preconditionTarget = mapping.precondition?.exactTargetOrNull() + ?: return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "An exact precondition target was unavailable after capability validation", + path = "precondition", + ), + ) + val execution = analyzePreconditionTarget(manifest, preconditionTarget) + + return classifyPreconditionAnalysis(capability, execution) + } + + private fun analyzePreconditionTarget( + manifest: PropertyManifest, + preconditionTarget: EtsEntryPointTarget, + ): UsvmPreconditionExecution = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + ).use { machine -> + val analysis = machine.analyzeWithMetadata( + methods = listOf(preconditionTarget.method), + configureInitialState = { method, state -> + check(method == preconditionTarget.method) { + "Unexpected precondition initial state for ${method.signature}" + } + + domainProjector.configure( + state = state, + inputs = manifest.inputs, + bindings = preconditionTarget.bindings.inputs, + ) + }, + ) + val canResolve = !analysis.timedOut && analysis.states.isNotEmpty() && analysis.states.all { state -> + val methodResult = state.methodResult as? TsMethodResult.Success + methodResult != null && methodResult.value.sort == state.ctx.boolSort + } + val resolutions = if (canResolve) { + analysis.states.map(::retainTruePreconditionState) + } else { + emptyList() + } + + UsvmPreconditionExecution(analysis, resolutions) + } + + private fun classifyPreconditionAnalysis( + capability: UsvmPropertyProjectionCapability, + execution: UsvmPreconditionExecution, + ): UsvmPreconditionResult { + val analysis = execution.analysis + val failure = classifyPreconditionFailure(capability, analysis) + if (failure != null) { + return failure + } + + val capabilityDiagnostics = capability.symbolic.diagnostics + val resolutions = execution.resolutions + if (resolutions.any { it is PreconditionStateResolution.SolverUnknown }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.SOLVER_UNKNOWN, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a precondition result", + path = "precondition.result", + ), + ) + } + val acceptedStates = resolutions.mapNotNull { resolution -> + (resolution as? PreconditionStateResolution.Accepted)?.state + } + val status = if (acceptedStates.isEmpty()) { + UsvmPreconditionStatus.REJECTED + } else { + UsvmPreconditionStatus.ACCEPTED + } + + return result( + capability = capability, + status = status, + acceptedStates = acceptedStates, + diagnostics = capabilityDiagnostics, + ) + } + + private fun classifyPreconditionFailure( + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPreconditionResult? { + val capabilityDiagnostics = capability.symbolic.diagnostics + val terminalStates = analysis.states + if (terminalStates.any { state -> state.methodResult is TsMethodResult.TsException }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.PROPERTY_ERROR, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, + message = "The precondition has a reachable escaping exception", + path = "precondition", + ), + ) + } + if (terminalStates.any { state -> state.methodResult !is TsMethodResult.Success }) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Precondition analysis terminated without a method result", + path = "precondition", + ), + ) + } + val nonBooleanResult = terminalStates.any { state -> + val methodResult = state.methodResult as TsMethodResult.Success + methodResult.value.sort != state.ctx.boolSort + } + if (nonBooleanResult) { + return result( + capability = capability, + status = UsvmPreconditionStatus.PROPERTY_ERROR, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, + message = "The precondition returned a non-boolean symbolic value", + path = "precondition.result", + ), + ) + } + if (analysis.unsupportedCall) { + return result( + capability = capability, + status = UsvmPreconditionStatus.UNSUPPORTED, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, + message = "The symbolic engine encountered an unsupported precondition call", + path = "precondition", + ), + ) + } + if (analysis.engineFailed) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The symbolic engine could not execute every reachable precondition path", + path = "precondition", + ), + ) + } + if (analysis.timedOut) { + return result( + capability = capability, + status = UsvmPreconditionStatus.TIMEOUT, + diagnostics = capabilityDiagnostics, + ) + } + if (terminalStates.isEmpty()) { + return result( + capability = capability, + status = UsvmPreconditionStatus.ENGINE_FAILURE, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Precondition analysis produced no terminal states", + path = "precondition", + ), + ) + } + + return null + } + + private fun retainTruePreconditionState(state: TsState): PreconditionStateResolution { + val result = state.methodResult as TsMethodResult.Success + val returnValue = with(state.ctx) { + result.value.asExpr(boolSort) + } + val acceptedState = state.clone() + acceptedState.pathConstraints += returnValue + val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints) + + return when (solverResult) { + is USatResult -> { + acceptedState.models = listOf(solverResult.model) + PreconditionStateResolution.Accepted(acceptedState) + } + + is UUnsatResult -> PreconditionStateResolution.Rejected + is UUnknownResult -> PreconditionStateResolution.SolverUnknown + } + } + + private fun result( + capability: UsvmPropertyProjectionCapability, + status: UsvmPreconditionStatus, + diagnostics: List, + acceptedStates: List = emptyList(), + ) = UsvmPreconditionResult( + capability = capability, + status = status, + acceptedStates = acceptedStates, + diagnostics = diagnostics, + ) + + private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( + code = code, + message = message, + path = path, + ) +} + +private data class UsvmPreconditionExecution( + val analysis: TsMachineAnalysisResult, + val resolutions: List, +) + +private sealed interface PreconditionStateResolution { + data class Accepted(val state: TsState) : PreconditionStateResolution + data object Rejected : PreconditionStateResolution + data object SolverUnknown : PreconditionStateResolution +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt new file mode 100644 index 0000000000..8b3c531817 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -0,0 +1,54 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyId + +/** Terminal outcome of one USVM property-violation search. */ +enum class UsvmPropertySearchStatus { + VIOLATION_REACHED, + NO_VIOLATION_REACHED, + PRECONDITION_REJECTED, + PROPERTY_ERROR, + TIMEOUT, + SOLVER_UNKNOWN, + UNSUPPORTED, + ENGINE_FAILURE, + FAILED_INPUT_RESOLUTION, +} + +/** Supported ways in which a mapped predicate can violate its property. */ +enum class UsvmPropertyViolationTarget { + PREDICATE_FALSE, + UNEXPECTED_EXCEPTION, + ASSERTION_FAILURE, +} + +/** Backend-neutral result of searching one mapped TypeScript property with USVM. */ +data class UsvmPropertySearchResult( + val propertyId: PropertyId, + val status: UsvmPropertySearchStatus, + val target: UsvmPropertyViolationTarget?, + val inputs: List?, + val capability: UsvmPropertyProjectionCapability, + val diagnostics: List, +) { + init { + when (status) { + UsvmPropertySearchStatus.VIOLATION_REACHED -> { + requireNotNull(target) { "A reached violation requires its target" } + requireNotNull(inputs) { "A resolved violation requires candidate inputs" } + } + + UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION -> { + requireNotNull(target) { "An input-resolution failure requires its reached target" } + require(inputs == null) { "An input-resolution failure cannot contain candidate inputs" } + } + + else -> { + require(target == null) { "A result without a violation cannot contain a target" } + require(inputs == null) { "A result without a violation cannot contain candidate inputs" } + } + } + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt new file mode 100644 index 0000000000..9522aedb42 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -0,0 +1,441 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.targets.TsTarget +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsEntryPointGuardOutcome +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.state.prependBooleanEntryPointGuard +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult +import org.usvm.statistics.UMachineObserver +import org.usvm.ts.pbt.PbtDiagnosticCode +import org.usvm.ts.pbt.backend.CapabilityDiagnostic +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.PropertyId + +/** Searches mapped TypeScript predicates for concrete property violations with USVM. */ +class UsvmPropertySearcher( + private val scene: EtsScene, + machineOptions: UMachineOptions = UMachineOptions(), + private val tsOptions: TsOptions = TsOptions(), + private val projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), +) { + private val machineOptions = machineOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL) + private val capabilityResolver = UsvmProjectionCapabilityResolver() + private val domainProjector = UsvmDomainProjector(projectionOptions) + private val inputResolver = UsvmCandidateInputResolver() + + fun search( + manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + concreteCapability: ProjectionCapability, + ): UsvmPropertySearchResult { + val capability = capabilityResolver.resolve( + manifest = manifest, + mapping = mapping, + concreteCapability = concreteCapability, + options = projectionOptions, + ) + val capabilityDiagnostics = capability.symbolic.diagnostics + if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.UNSUPPORTED, + capability = capability, + diagnostics = capabilityDiagnostics, + ) + } + + val predicate = mapping.predicate.exactTargetOrNull() + ?: return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "An exact predicate target was unavailable after capability validation", + path = "predicate", + ), + ) + val precondition = mapping.precondition?.exactTargetOrNull() + val execution = executeSearch(manifest, predicate, precondition) + val terminalFailure = classifyTerminalFailure( + manifest = manifest, + capability = capability, + analysis = execution.analysis, + ) + if (terminalFailure != null) { + return terminalFailure + } + + val violationState = execution.observer.violationStates.firstOrNull() + ?: return noViolationResult( + manifest = manifest, + capability = capability, + analysis = execution.analysis, + observer = execution.observer, + ) + + return violationResult( + manifest = manifest, + capability = capability, + violationState = violationState, + projection = execution.projection, + ) + } + + private fun executeSearch( + manifest: PropertyManifest, + predicate: EtsEntryPointTarget, + precondition: EtsEntryPointTarget?, + ): UsvmSearchExecution { + lateinit var projection: UsvmDeclaredDomainProjection + val target = UsvmViolationTsTarget() + val observer = UsvmViolationObserver(target) + val analysis = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = observer, + ).use { machine -> + machine.analyzeWithMetadata( + methods = listOf(predicate.method), + targets = listOf(target), + configureInitialState = { method, state -> + check(method == predicate.method) + projection = domainProjector.configure( + state = state, + inputs = manifest.inputs, + bindings = predicate.bindings.inputs, + ) + if (precondition != null) { + state.prependBooleanEntryPointGuard( + guard = precondition.method, + arguments = projection.inputs.map(UsvmProjectedInput::value), + ) + } + }, + ) + } + + return UsvmSearchExecution( + analysis = analysis, + observer = observer, + projection = projection, + ) + } + + private fun classifyTerminalFailure( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPropertySearchResult? { + val preconditionFailure = classifyPreconditionFailure(manifest, capability, analysis) + if (preconditionFailure != null) { + return preconditionFailure + } + + val capabilityDiagnostics = capability.symbolic.diagnostics + val predicateContractError = analysis.states.any { state -> + val methodResult = state.methodResult as? TsMethodResult.Success + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + methodResult != null && + methodResult.value.sort != state.ctx.boolSort + } + if (predicateContractError) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.PROPERTY_ERROR, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_PREDICATE_RESULT_NON_BOOLEAN, + message = "The predicate returned a non-boolean symbolic value", + path = "predicate.result", + ), + ) + } + val missingPredicateResult = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + state.methodResult == TsMethodResult.NoCall + } + if (missingPredicateResult) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Predicate analysis terminated without a method result", + path = "predicate", + ), + ) + } + if (analysis.unsupportedCall) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.UNSUPPORTED, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, + message = "The symbolic engine encountered an unsupported property call", + path = "predicate", + ), + ) + } + if (analysis.engineFailed) { + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.ENGINE_FAILURE, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The symbolic engine could not execute every reachable property path", + path = "predicate", + ), + ) + } + + return null + } + + private fun classifyPreconditionFailure( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + ): UsvmPropertySearchResult? { + val capabilityDiagnostics = capability.symbolic.diagnostics + val preconditionError = analysis.states.firstOrNull { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR + } + ?: return null + val diagnostic = when (preconditionError.methodResult) { + is TsMethodResult.TsException -> diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, + message = "The precondition has a reachable escaping exception", + path = "precondition", + ) + + is TsMethodResult.Success -> diagnostic( + code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, + message = "The precondition returned a non-boolean symbolic value", + path = "precondition.result", + ) + + TsMethodResult.NoCall -> diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "The precondition guard terminated without a method result", + path = "precondition", + ) + } + val status = if (preconditionError.methodResult == TsMethodResult.NoCall) { + UsvmPropertySearchStatus.ENGINE_FAILURE + } else { + UsvmPropertySearchStatus.PROPERTY_ERROR + } + + return result( + manifest = manifest, + status = status, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic, + ) + } + + private fun noViolationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + analysis: TsMachineAnalysisResult, + observer: UsvmViolationObserver, + ): UsvmPropertySearchResult { + val capabilityDiagnostics = capability.symbolic.diagnostics + val predicateCompleted = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && + state.methodResult is TsMethodResult.Success + } + val preconditionRejected = analysis.states.any { state -> + state.entryPointGuardOutcome == TsEntryPointGuardOutcome.REJECTED + } + val status = when { + analysis.timedOut -> UsvmPropertySearchStatus.TIMEOUT + observer.solverUnknown -> UsvmPropertySearchStatus.SOLVER_UNKNOWN + predicateCompleted -> UsvmPropertySearchStatus.NO_VIOLATION_REACHED + preconditionRejected -> UsvmPropertySearchStatus.PRECONDITION_REJECTED + else -> UsvmPropertySearchStatus.ENGINE_FAILURE + } + val diagnostics = when (status) { + UsvmPropertySearchStatus.SOLVER_UNKNOWN -> capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a predicate result", + path = "predicate.result", + ) + + UsvmPropertySearchStatus.ENGINE_FAILURE -> capabilityDiagnostics + diagnostic( + code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, + message = "Property search produced no classified terminal state", + path = "predicate", + ) + + else -> capabilityDiagnostics + } + + return result( + manifest = manifest, + status = status, + capability = capability, + diagnostics = diagnostics, + ) + } + + private fun violationResult( + manifest: PropertyManifest, + capability: UsvmPropertyProjectionCapability, + violationState: TsState, + projection: UsvmDeclaredDomainProjection, + ): UsvmPropertySearchResult { + val capabilityDiagnostics = capability.symbolic.diagnostics + val violationTarget = classifyViolation(violationState) + val inputs = runCatching { + inputResolver.resolve(violationState, manifest.inputs, projection) + }.getOrElse { failure -> + val diagnostic = CapabilityDiagnostic( + code = PbtDiagnosticCode.USVM_INPUT_RESOLUTION_FAILED, + message = failure.message ?: "Failed to resolve symbolic property inputs", + path = "inputs", + ) + + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, + target = violationTarget, + capability = capability, + diagnostics = capabilityDiagnostics + diagnostic, + ) + } + + return result( + manifest = manifest, + status = UsvmPropertySearchStatus.VIOLATION_REACHED, + target = violationTarget, + inputs = inputs, + capability = capability, + diagnostics = capabilityDiagnostics, + ) + } + + private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( + code = code, + message = message, + path = path, + ) + + private fun classifyViolation(state: TsState): UsvmPropertyViolationTarget { + return when (val result = state.methodResult) { + is TsMethodResult.Success -> { + UsvmPropertyViolationTarget.PREDICATE_FALSE + } + + is TsMethodResult.TsException -> { + val message = with(state.ctx) { + val ref = state.models.single().eval(result.value) as? org.usvm.UConcreteHeapRef + ref?.takeIf(::isAllocatedConcreteHeapRef)?.let(::getStringConstantValue) + } + if (message?.contains("AssertionError") == true) { + UsvmPropertyViolationTarget.ASSERTION_FAILURE + } else { + UsvmPropertyViolationTarget.UNEXPECTED_EXCEPTION + } + } + + TsMethodResult.NoCall -> { + error("Reached a violation target without a predicate result") + } + } + } + + private fun result( + manifest: PropertyManifest, + status: UsvmPropertySearchStatus, + capability: UsvmPropertyProjectionCapability, + diagnostics: List, + target: UsvmPropertyViolationTarget? = null, + inputs: List? = null, + ) = UsvmPropertySearchResult( + propertyId = PropertyId(manifest.propertyId), + status = status, + target = target, + inputs = inputs, + capability = capability, + diagnostics = diagnostics, + ) +} + +private data class UsvmSearchExecution( + val analysis: TsMachineAnalysisResult, + val observer: UsvmViolationObserver, + val projection: UsvmDeclaredDomainProjection, +) + +private class UsvmViolationTsTarget : TsTarget(location = null) + +private class UsvmViolationObserver( + private val target: UsvmViolationTsTarget, +) : UMachineObserver { + private val mutableViolationStates = mutableListOf() + + val violationStates: List + get() = mutableViolationStates + + var solverUnknown: Boolean = false + private set + + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + if ( + !stateReachable || + state.entryPointGuardActive || + state.entryPointGuardOutcome != TsEntryPointGuardOutcome.NONE + ) { + return + } + + when (val result = state.methodResult) { + is TsMethodResult.TsException -> recordViolation(state) + is TsMethodResult.Success -> with(state.ctx) { + val returnValue = result.value.takeIf { it.sort == boolSort }?.asExpr(boolSort) ?: return@with + val candidateState = state.clone() + candidateState.pathConstraints += returnValue.not() + val solverResult = solver().check(candidateState.pathConstraints) + + when (solverResult) { + is USatResult -> { + candidateState.models = listOf(solverResult.model) + recordViolation(candidateState) + } + + is UUnsatResult -> Unit + is UUnknownResult -> solverUnknown = true + } + } + + TsMethodResult.NoCall -> Unit + } + } + + private fun recordViolation(state: TsState) { + target.propagate(state) + mutableViolationStates += state + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt new file mode 100644 index 0000000000..8c4aa193a9 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt @@ -0,0 +1,263 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.fastcheck.BackendErrorKind +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.testResourcePath +import org.usvm.ts.pbt.testResourcesRoot +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class PropertyExecutionConformanceTest { + @Test + fun `shared preconditions have the same concrete projection and search classification`() { + val cases = listOf( + ContractCase("truePrecondition", ContractOutcome.HOLDS), + ContractCase("falsePrecondition", ContractOutcome.PRECONDITION_REJECTED), + ContractCase( + exportName = "throwingPrecondition", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.precondition.threw", + path = "manifest.precondition", + ), + ), + ContractCase( + exportName = "nonBooleanPrecondition", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.result.invalid", + path = "manifest.precondition.result", + ), + ), + ) + + cases.forEach { case -> + val property = property( + predicateExport = "alwaysTrue", + preconditionExport = case.exportName, + ) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteOutcome = concreteOutcome(property, case.expectedBackendError) + val projectionOutcome = projectionOutcome( + projector.analyzePrecondition(manifest, mapping, exactCapability), + ) + val searchOutcome = searchOutcome( + searcher.search(manifest, mapping, exactCapability), + ) + + assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") + assertEquals(case.expected, projectionOutcome, "${case.exportName}: projection") + assertEquals(case.expected, searchOutcome, "${case.exportName}: search") + } + } + + @Test + fun `shared predicates have the same concrete and search classification`() { + val cases = listOf( + ContractCase("falsePredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("throwingPredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("literalFalsePredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase("literalTruePredicate", ContractOutcome.HOLDS), + ContractCase("neverPredicate", ContractOutcome.PREDICATE_VIOLATION), + ContractCase( + exportName = "nonBooleanPredicate", + expected = ContractOutcome.PROPERTY_ERROR, + expectedBackendError = BackendErrorExpectation( + code = "entrypoint.result.invalid", + path = "manifest.predicate.result", + ), + ), + ) + + cases.forEach { case -> + val property = property(predicateExport = case.exportName) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteOutcome = concreteOutcome(property, case.expectedBackendError) + val searchOutcome = searchOutcome( + searcher.search(manifest, mapping, exactCapability), + ) + + assertEquals(case.expected, concreteOutcome, "${case.exportName}: concrete") + assertEquals(case.expected, searchOutcome, "${case.exportName}: search") + } + } + + @Test + fun `symbolic candidates retain inputs from before predicate mutation`() { + val domain = ArrayDomain( + element = IntegerDomain(min = 1, max = 1), + minLength = 1, + maxLength = 1, + ) + val property = property( + predicateExport = "mutatesAndFails", + domain = domain, + ) + val manifest = property.toManifest() + val mapping = mapper.map(manifest) + + val concreteResult = backend.run(property, configuration) + val searchResult = searcher.search(manifest, mapping, exactCapability) + + val expectedInput = JsConcreteValue.Array( + elements = listOf(JsConcreteValue.number(1.0)), + ) + val symbolicInputs = assertNotNull(searchResult.inputs) + assertEquals(PropertyFailureKind.PROPERTY, concreteResult.failure?.kind) + assertEquals(listOf(expectedInput), concreteResult.counterexample) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, searchResult.status) + assertEquals(listOf(expectedInput), symbolicInputs) + assertTrue(symbolicInputs.single() in domain) + + val replay = backend.run( + property = property, + configuration = configuration.copy( + numRuns = 1, + examples = listOf(symbolicInputs), + ), + ) + + assertEquals(PropertyFailureKind.PROPERTY, replay.failure?.kind) + assertEquals(symbolicInputs, replay.counterexample) + } + + private fun concreteOutcome( + property: PropertyDefinition, + expectedBackendError: BackendErrorExpectation?, + ): ContractOutcome = try { + val result = backend.run(property, configuration) + + when (result.status) { + PropertyRunStatus.SUCCESS -> ContractOutcome.HOLDS + PropertyRunStatus.FAILURE -> when (result.failure?.kind) { + PropertyFailureKind.PROPERTY -> ContractOutcome.PREDICATE_VIOLATION + PropertyFailureKind.PRECONDITION_EXHAUSTED -> ContractOutcome.PRECONDITION_REJECTED + PropertyFailureKind.TIMEOUT, null -> error("Unexpected concrete result: $result") + } + } + } catch (failure: PbtBackendException) { + val expected = checkNotNull(expectedBackendError) { + "Unexpected concrete backend error: ${failure.kind}/${failure.code} at ${failure.path}" + } + + assertEquals(BackendErrorKind.ENTRY_POINT, failure.kind) + assertEquals(expected.code, failure.code) + assertEquals(expected.path, failure.path) + + ContractOutcome.PROPERTY_ERROR + } + + private fun projectionOutcome(result: UsvmPreconditionResult): ContractOutcome = when (result.status) { + UsvmPreconditionStatus.ACCEPTED -> ContractOutcome.HOLDS + UsvmPreconditionStatus.REJECTED -> ContractOutcome.PRECONDITION_REJECTED + UsvmPreconditionStatus.PROPERTY_ERROR -> ContractOutcome.PROPERTY_ERROR + else -> error("Unexpected projection result: $result") + } + + private fun searchOutcome(result: UsvmPropertySearchResult): ContractOutcome = when (result.status) { + UsvmPropertySearchStatus.VIOLATION_REACHED -> ContractOutcome.PREDICATE_VIOLATION + UsvmPropertySearchStatus.NO_VIOLATION_REACHED -> ContractOutcome.HOLDS + UsvmPropertySearchStatus.PRECONDITION_REJECTED -> ContractOutcome.PRECONDITION_REJECTED + UsvmPropertySearchStatus.PROPERTY_ERROR -> ContractOutcome.PROPERTY_ERROR + else -> error("Unexpected search result: $result") + } + + private fun property( + predicateExport: String, + preconditionExport: String? = null, + domain: org.usvm.ts.pbt.model.PropertyDomain = IntegerDomain(min = 0, max = 0), + ) = PropertyDefinition( + id = PropertyId("contract.$predicateExport.${preconditionExport ?: "none"}"), + inputs = listOf( + PropertyInput( + name = "value", + domain = domain, + ), + ), + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = predicateExport, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = MODULE, + exportName = exportName, + ) + }, + ) + + private data class ContractCase( + val exportName: String, + val expected: ContractOutcome, + val expectedBackendError: BackendErrorExpectation? = null, + ) + + private data class BackendErrorExpectation( + val code: String, + val path: String, + ) + + private enum class ContractOutcome { + HOLDS, + PRECONDITION_REJECTED, + PREDICATE_VIOLATION, + PROPERTY_ERROR, + } + + companion object { + private const val MODULE = "PropertyExecutionContract.ts" + + private val exactCapability = ProjectionCapability(level = ProjectionLevel.EXACT) + private val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 1, + timeoutMillis = 1_000, + ) + private val fixtureDirectory = testResourcesRoot().resolve("properties/contract") + private val backend = FastCheckBackend(sourceRoots = listOf(fixtureDirectory)) + private lateinit var mapper: PropertyEtsMapper + private lateinit var projector: UsvmPropertyProjector + private lateinit var searcher: UsvmPropertySearcher + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/properties/contract/$MODULE") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + + mapper = PropertyEtsMapper( + scene = scene, + sourceRoots = listOf(fixtureDirectory), + ) + projector = UsvmPropertyProjector(scene) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt new file mode 100644 index 0000000000..b18601d748 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt @@ -0,0 +1,175 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmCollectionDomainProjectorTest { + @Test + fun `array length and every active element satisfy their recursive domains`() { + val domain = ArrayDomain( + element = IntegerDomain(min = -1, max = 1), + minLength = 1, + maxLength = 2, + ) + + assertTrue(acceptsArray(domain, length = 1, elements = listOf(-1.0))) + assertTrue(acceptsArray(domain, length = 2, elements = listOf(-1.0, 1.0))) + assertFalse(acceptsArray(domain, length = 0, elements = emptyList())) + assertFalse(acceptsArray(domain, length = 3, elements = listOf(0.0, 0.0))) + assertFalse(acceptsArray(domain, length = 2, elements = listOf(0.0, 2.0))) + } + + @Test + fun `tuple has exact length and positional recursive domains`() { + val domain = TupleDomain(listOf(IntegerDomain(min = 2, max = 4), BooleanDomain)) + + assertTrue(acceptsTuple(domain, number = 3.0, boolean = true, length = 2)) + assertTrue(acceptsTuple(domain, number = 4.0, boolean = false, length = 2)) + assertFalse(acceptsTuple(domain, number = 1.0, boolean = true, length = 2)) + assertFalse(acceptsTuple(domain, number = 3.0, boolean = true, length = 1)) + } + + @Test + fun `oversized arrays are rejected before materialization`() { + val domain = ArrayDomain(IntegerDomain(), maxLength = 3) + val manifest = manifest(domain, exportName = "acceptsNumberArray") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + val projector = UsvmDomainProjector( + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 2), + ) + + assertFailsWith { + analyze(target.method) { state -> + projector.configure(state, manifest.inputs, target.bindings.inputs) + } + } + } + + private fun acceptsArray(domain: ArrayDomain, length: Int, elements: List): Boolean { + val manifest = manifest(domain, exportName = "acceptsNumberArray") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return runCatchingAnalyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val array = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(array, arrayType)) + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + elements.forEachIndexed { index, element -> + val lValue = mkArrayIndexLValue(fp64Sort, array, mkBv(index), arrayType) + val projectedElement = state.memory.read(lValue) + + state.pathConstraints += mkEq(projectedElement, mkFp(element, fp64Sort)) + } + } + } + } + + private fun acceptsTuple( + domain: TupleDomain, + number: Double, + boolean: Boolean, + length: Int, + ): Boolean { + val manifest = manifest(domain, exportName = "acceptsNumberBooleanTuple") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return runCatchingAnalyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val tuple = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(tuple, arrayType)) + val numberBox = state.memory.read( + mkArrayIndexLValue(addressSort, tuple, mkBv(0), arrayType), + ) as UConcreteHeapRef + val booleanBox = state.memory.read( + mkArrayIndexLValue(addressSort, tuple, mkBv(1), arrayType), + ) as UConcreteHeapRef + + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + state.pathConstraints += mkEq(numberBox.extractFp(state.memory), mkFp(number, fp64Sort)) + state.pathConstraints += mkEq(booleanBox.extractBool(state.memory), mkBool(boolean)) + } + } + } + + private fun manifest(domain: PropertyDomain, exportName: String) = PropertyManifest( + propertyId = "usvm.collection.$exportName", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + ), + ) + + private fun runCatchingAnalyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ): Boolean = runCatching { analyze(method, configure) }.isSuccess + + private fun analyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ) { + TsMachine( + scene = scene, + options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { _, state -> configure(state) }, + ) + } + } + + companion object { + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private val projector = UsvmDomainProjector() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt new file mode 100644 index 0000000000..c9a988ef7b --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt @@ -0,0 +1,110 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmInitialStateConfigurationTest { + @Test + fun `initial state configuration participates in the first solver model`() { + val source = testResourcePath("/mapping/PropertyMappingFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + val method = scene.projectClasses + .flatMap { etsClass -> etsClass.methods } + .single { candidate -> candidate.name == "isPositive" } + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL) + + val states = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { configuredMethod, state -> + assertEquals(method, configuredMethod) + + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + state.pathConstraints += mkFpEqualExpr(input, mkFp(7.0, fp64Sort)) + } + }, + ) + } + + assertTrue(states.isNotEmpty()) + states.forEach { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + val evaluated = state.models.single().eval(input) + + assertEquals(mkFp(7.0, fp64Sort), evaluated) + } + } + } + + @Test + fun `ordinary constraint pruning is not reported as an engine failure`() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + val manifest = PropertyManifest( + propertyId = "usvm.constraint-pruning", + inputs = listOf( + PropertyInput( + name = "value", + domain = ArrayDomain( + element = IntegerDomain(min = 0, max = 0), + minLength = 2, + maxLength = 2, + ), + ), + ), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = "acceptsNumberArray", + ), + ) + val mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + val predicate = requireNotNull(mapper.map(manifest).predicate.exactTargetOrNull()) + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL) + + val analysis = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(maxArraySize = 1), + ).use { machine -> + machine.analyzeWithMetadata( + methods = listOf(predicate.method), + configureInitialState = { _, state -> + UsvmDomainProjector().configure( + state = state, + inputs = manifest.inputs, + bindings = predicate.bindings.inputs, + ) + }, + ) + } + + assertEquals(emptyList(), analysis.states) + assertFalse(analysis.engineFailed) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt new file mode 100644 index 0000000000..ab0348c037 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionProjectionTest.kt @@ -0,0 +1,124 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.isTrue +import org.usvm.machine.state.TsMethodResult +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class UsvmPreconditionProjectionTest { + @Test + fun `mapped precondition retains only satisfiable true states inside the declared domain`() { + val manifest = manifest(preconditionExport = "isPositive") + val mapping = mapper.map(manifest) + + val result = projector.analyzePrecondition(manifest, mapping, exact()) + + assertEquals(ProjectionLevel.EXACT, result.capability.symbolic.level) + assertEquals(UsvmPreconditionStatus.ACCEPTED, result.status) + assertTrue(result.acceptedStates.isNotEmpty()) + result.acceptedStates.forEach { state -> + assertTrue(state.methodResult is TsMethodResult.Success) + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + val value = state.models.single().eval(input) + + assertTrue(mkFpGreaterExpr(value, mkFp(0.0, fp64Sort)).isTrue) + assertTrue(mkFpLessOrEqualExpr(value, mkFp(3.0, fp64Sort)).isTrue) + } + } + } + + @Test + fun `false-only states are rejected and unsupported exception construction is explicit`() { + val falseManifest = manifest(preconditionExport = "alwaysFalse") + val throwingManifest = manifest(preconditionExport = "acceptsNonPositiveOrThrows") + + val falseResult = projector.analyzePrecondition(falseManifest, mapper.map(falseManifest), exact()) + val throwingResult = projector.analyzePrecondition(throwingManifest, mapper.map(throwingManifest), exact()) + + assertEquals(emptyList(), falseResult.acceptedStates) + assertEquals(UsvmPreconditionStatus.REJECTED, falseResult.status) + assertEquals(emptyList(), throwingResult.acceptedStates) + assertEquals(UsvmPreconditionStatus.UNSUPPORTED, throwingResult.status) + assertTrue(throwingResult.diagnostics.any { it.code == "usvm.execution.unsupported" }) + } + + @Test + fun `async preconditions are unsupported and non-boolean preconditions are property errors`() { + val asyncManifest = manifest( + preconditionExport = "asyncIsPositive", + executionKind = ExecutionKind.ASYNC, + ) + val nonBooleanManifest = manifest(preconditionExport = "returnsNumber") + + val asyncResult = projector.analyzePrecondition(asyncManifest, mapper.map(asyncManifest), exact()) + val nonBooleanResult = projector.analyzePrecondition( + nonBooleanManifest, + mapper.map(nonBooleanManifest), + exact(), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, asyncResult.capability.precondition.level) + assertEquals(UsvmPreconditionStatus.UNSUPPORTED, asyncResult.status) + assertEquals(emptyList(), asyncResult.acceptedStates) + assertEquals(ProjectionLevel.EXACT, nonBooleanResult.capability.precondition.level) + assertEquals(UsvmPreconditionStatus.PROPERTY_ERROR, nonBooleanResult.status) + assertEquals(emptyList(), nonBooleanResult.acceptedStates) + assertTrue(nonBooleanResult.diagnostics.any { it.code == "usvm.precondition.result.non-boolean" }) + } + + private fun manifest( + preconditionExport: String, + executionKind: ExecutionKind = ExecutionKind.SYNC, + ) = PropertyManifest( + propertyId = "usvm.precondition.$preconditionExport.${executionKind.name.lowercase()}", + inputs = listOf( + PropertyInput( + name = "value", + domain = IntegerDomain(min = -2, max = 3), + ), + ), + predicate = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = "predicate", + ), + precondition = TypeScriptEntryPoint( + module = "UsvmPreconditionFixture.ts", + exportName = preconditionExport, + executionKind = executionKind, + ), + ) + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private lateinit var projector: UsvmPropertyProjector + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmPreconditionFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + projector = UsvmPropertyProjector(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt new file mode 100644 index 0000000000..5ba1249988 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt @@ -0,0 +1,208 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCapabilityLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +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.ExecutionKind +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.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import kotlin.test.assertEquals + +class UsvmProjectionCapabilityTest { + @Test + fun `reports scalar fidelity and type mismatches`() { + val cases = listOf( + Case(BooleanDomain, "acceptsBoolean", ProjectionLevel.EXACT, emptyList()), + Case(IntegerDomain(min = -2, max = 3), "acceptsNumber", ProjectionLevel.EXACT, emptyList()), + Case(NumberDomain(allowNaN = false), "acceptsNumber", ProjectionLevel.EXACT, emptyList()), + Case(StringDomain(maxLength = 4), "acceptsString", ProjectionLevel.APPROXIMATE, listOf("inputs[0].domain")), + Case( + ConstantDomain(JsConcreteValue.Boolean(value = true)), + "acceptsBoolean", + ProjectionLevel.EXACT, + emptyList(), + ), + Case(IntegerDomain(), "acceptsString", ProjectionLevel.UNSUPPORTED, listOf("inputs[0].domain")), + ) + + cases.forEach { case -> + val capability = resolve(case.domain, case.exportName) + + assertEquals(case.level, capability.symbolic.level, case.exportName) + assertEquals(case.diagnosticPaths, capability.symbolic.diagnostics.map { it.path }, case.exportName) + } + } + + @Test + fun `recursive domains inherit the least capable nested projection`() { + val optional = resolve( + domain = OptionalDomain(IntegerDomain(min = 0, max = 5)), + exportName = "acceptsOptionalNumber", + ) + val tuple = resolve( + domain = TupleDomain(listOf(IntegerDomain(), StringDomain(maxLength = 3))), + exportName = "acceptsTuple", + ) + val array = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 4), + exportName = "acceptsNumberArray", + ) + val oversizedArray = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 11), + exportName = "acceptsNumberArray", + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 10), + ) + + assertEquals(ProjectionLevel.EXACT, optional.symbolic.level) + assertEquals(ProjectionLevel.APPROXIMATE, tuple.symbolic.level) + assertEquals(listOf("inputs[0].domain.elements[1]"), tuple.symbolic.diagnostics.map { it.path }) + assertEquals(ProjectionLevel.EXACT, array.symbolic.level) + assertEquals(ProjectionLevel.UNSUPPORTED, oversizedArray.symbolic.level) + assertEquals(listOf("inputs[0].domain"), oversizedArray.symbolic.diagnostics.map { it.path }) + } + + @Test + fun `reports unsupported mapping and execution boundaries without classifying property errors`() { + val manifest = manifest(IntegerDomain(), predicateExport = "acceptsNumber") + val mapping = mapper.map(manifest) + val nonExactMapping = mapping.copy( + predicate = mapping.predicate.copy( + status = EtsMappingStatus.UNMAPPED, + targets = emptyList(), + diagnostics = listOf( + EtsMappingDiagnostic( + code = "test.mapping.unmapped", + message = "Synthetic unmapped predicate", + ), + ), + ), + ) + val asyncPreconditionManifest = manifest( + domain = IntegerDomain(), + predicateExport = "acceptsNumber", + preconditionExport = "acceptsNumber", + preconditionExecutionKind = ExecutionKind.ASYNC, + ) + val nonBooleanPreconditionManifest = manifest( + domain = IntegerDomain(), + predicateExport = "acceptsNumber", + preconditionExport = "returnsNumber", + ) + + val nonExact = resolver.resolve(manifest, nonExactMapping, exact()) + val async = resolver.resolve( + asyncPreconditionManifest, + mapper.map(asyncPreconditionManifest), + exact(), + ) + val nonBoolean = resolver.resolve( + nonBooleanPreconditionManifest, + mapper.map(nonBooleanPreconditionManifest), + exact(), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, nonExact.symbolic.level) + assertEquals( + "predicate", + nonExact.symbolic.diagnostics.single { it.code == "usvm.predicate.mapping.non-exact" }.path, + ) + assertEquals(ProjectionLevel.UNSUPPORTED, async.precondition.level) + assertEquals("precondition", async.precondition.diagnostics.single().path) + assertEquals(ProjectionLevel.EXACT, nonBoolean.precondition.level) + assertEquals(emptyList(), nonBoolean.precondition.diagnostics) + } + + @Test + fun `derives concrete only from a supported concrete projection`() { + val capability = resolve( + domain = ArrayDomain(IntegerDomain(), maxLength = 11), + exportName = "acceptsNumberArray", + concreteCapability = exact(), + options = UsvmProjectionOptions(maxSymbolicCollectionLength = 10), + ) + + assertEquals(PropertyCapabilityLevel.CONCRETE_ONLY, capability.property) + } + + private fun resolve( + domain: org.usvm.ts.pbt.model.PropertyDomain, + exportName: String, + concreteCapability: ProjectionCapability = exact(), + options: UsvmProjectionOptions = UsvmProjectionOptions(), + ): UsvmPropertyProjectionCapability { + val manifest = manifest(domain, predicateExport = exportName) + + return resolver.resolve( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = concreteCapability, + options = options, + ) + } + + private fun manifest( + domain: org.usvm.ts.pbt.model.PropertyDomain, + predicateExport: String, + preconditionExport: String? = null, + preconditionExecutionKind: ExecutionKind = ExecutionKind.SYNC, + ) = PropertyManifest( + propertyId = "usvm.capability.$predicateExport", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = predicateExport, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + executionKind = preconditionExecutionKind, + ) + }, + ) + + private fun exact() = ProjectionCapability(level = ProjectionLevel.EXACT) + + private data class Case( + val domain: org.usvm.ts.pbt.model.PropertyDomain, + val exportName: String, + val level: ProjectionLevel, + val diagnosticPaths: List, + ) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private val resolver = UsvmProjectionCapabilityResolver() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + + mapper = PropertyEtsMapper( + scene = EtsScene(listOf(file)), + sourceRoots = listOf(source.parent), + ) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt new file mode 100644 index 0000000000..bca45b6dca --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionConformanceTest.kt @@ -0,0 +1,48 @@ +package org.usvm.ts.pbt.usvm + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.fastcheck.FastCheckProjectionClient +import org.usvm.ts.pbt.fastcheck.FastCheckProjectionRequest +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsNumber +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.TupleDomain +import org.usvm.ts.pbt.model.contains +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class UsvmProjectionConformanceTest { + @Test + fun `fast-check samples satisfy the same domains used by USVM constraint tests`() { + val domains = listOf( + IntegerDomain(min = -5, max = 7), + NumberDomain( + min = JsNumber.finite(-1.5), + max = JsNumber.finite(2.5), + allowNaN = false, + ), + OptionalDomain(IntegerDomain(min = 1, max = 3)), + TupleDomain(listOf(IntegerDomain(min = 2, max = 4), BooleanDomain)), + ArrayDomain(IntegerDomain(min = -1, max = 1), minLength = 1, maxLength = 3), + ) + val response = FastCheckProjectionClient().sample( + FastCheckProjectionRequest( + seed = 351, + numSamples = 50, + domains = domains, + ), + ) + + assertEquals(50, response.samples.size) + response.samples.forEach { sample -> + assertEquals(domains.size, sample.size) + sample.zip(domains).forEach { (value, domain) -> + assertTrue(value in domain, "$value is outside $domain") + } + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt new file mode 100644 index 0000000000..676e70b781 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -0,0 +1,231 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.model.TupleDomain +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.contains +import org.usvm.ts.pbt.testResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class UsvmPropertySearcherTest { + @Test + fun `reports when no violation is reachable`() { + val manifest = manifest(predicateExport = "validProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + assertEquals(PropertyId(manifest.propertyId), result.propertyId) + assertNull(result.target) + assertNull(result.inputs) + } + + @Test + fun `finds false predicate and resolves a candidate input`() { + val manifest = manifest(predicateExport = "violatedProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertEquals(listOf(JsConcreteValue.number(2.0)), result.inputs) + } + + @Test + fun `applies mapped precondition before searching the predicate`() { + val manifest = manifest( + predicateExport = "signedOneProperty", + preconditionExport = "positive", + ) + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(listOf(JsConcreteValue.number(1.0)), result.inputs) + } + + @Test + fun `distinguishes rejected and exceptional preconditions from predicate violations`() { + val rejected = manifest( + predicateExport = "violatedProperty", + preconditionExport = "falsePrecondition", + ) + val exceptional = manifest( + predicateExport = "violatedProperty", + preconditionExport = "throwingPrecondition", + ) + + val rejectedResult = search(rejected) + val exceptionalResult = search(exceptional) + + assertEquals(UsvmPropertySearchStatus.PRECONDITION_REJECTED, rejectedResult.status) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, exceptionalResult.status) + assertNull(rejectedResult.target) + assertNull(exceptionalResult.target) + assertTrue(exceptionalResult.diagnostics.any { it.code == "usvm.precondition.threw" }) + } + + @Test + fun `supports relational predicates with multiple calls`() { + val manifest = manifest(predicateExport = "relationalProperty") + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertNotNull(result.inputs) + } + + @Test + fun `classifies unexpected exceptions and supported assertion failures`() { + val unexpected = search(manifest(predicateExport = "unexpectedException")) + val assertion = search(manifest(predicateExport = "assertionFailure")) + + assertEquals(UsvmPropertyViolationTarget.UNEXPECTED_EXCEPTION, unexpected.target) + assertEquals(UsvmPropertyViolationTarget.ASSERTION_FAILURE, assertion.target) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, unexpected.status) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, assertion.status) + } + + @Test + fun `preserves a reached target when symbolic input resolution fails`() { + val manifest = manifest( + predicateExport = "falseStringProperty", + domain = StringDomain(minLength = 0, maxLength = 3), + ) + + val result = search(manifest) + + assertEquals(UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, result.status) + assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, result.target) + assertNull(result.inputs) + assertTrue(result.diagnostics.any { it.code == "usvm.input.resolution.failed" }) + } + + @Test + fun `resolves candidates for common Kotlin domains`() { + val cases = listOf( + "falseBooleanProperty" to BooleanDomain, + "falseOptionalProperty" to OptionalDomain(IntegerDomain(min = -1, max = 1)), + "falseTupleProperty" to TupleDomain( + listOf(IntegerDomain(min = -1, max = 1), BooleanDomain), + ), + "falseNestedTupleProperty" to TupleDomain( + listOf(OptionalDomain(IntegerDomain(min = -1, max = 1)), BooleanDomain), + ), + "falseArrayProperty" to ArrayDomain( + element = IntegerDomain(min = -1, max = 1), + minLength = 1, + maxLength = 3, + ), + ) + + cases.forEach { (predicateExport, domain) -> + val result = search(manifest(predicateExport = predicateExport, domain = domain)) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, predicateExport) + assertTrue(assertNotNull(result.inputs).single() in domain, predicateExport) + } + } + + @Test + fun `reports async predicates as unsupported and non-boolean predicates as property errors`() { + val async = manifest( + predicateExport = "asyncValidProperty", + executionKind = ExecutionKind.ASYNC, + ) + val nonBoolean = manifest(predicateExport = "nonBooleanProperty") + + val asyncResult = search(async) + val nonBooleanResult = search(nonBoolean) + + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, asyncResult.status) + assertTrue(asyncResult.diagnostics.any { it.code == "usvm.predicate.async" }) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, nonBooleanResult.status) + assertTrue(nonBooleanResult.diagnostics.any { it.code == "usvm.predicate.result.non-boolean" }) + } + + @Test + fun `distinguishes timeout from exhausted search`() { + val manifest = manifest(predicateExport = "validProperty") + val zeroTimeoutSearcher = UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions(timeout = Duration.ZERO), + ) + + val result = zeroTimeoutSearcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + + assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) + } + + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + ) + + private fun manifest( + predicateExport: String, + preconditionExport: String? = null, + executionKind: ExecutionKind = ExecutionKind.SYNC, + domain: PropertyDomain = IntegerDomain(min = -3, max = 3), + ) = PropertyManifest( + propertyId = "usvm.search.$predicateExport.${executionKind.name.lowercase()}", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmPropertySearchFixture.ts", + exportName = predicateExport, + executionKind = executionKind, + ), + precondition = preconditionExport?.let { exportName -> + TypeScriptEntryPoint( + module = "UsvmPropertySearchFixture.ts", + exportName = exportName, + ) + }, + ) + + companion object { + private lateinit var mapper: PropertyEtsMapper + private lateinit var searcher: UsvmPropertySearcher + private lateinit var scene: EtsScene + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmPropertySearchFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + searcher = UsvmPropertySearcher(scene) + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt new file mode 100644 index 0000000000..2c9415833d --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt @@ -0,0 +1,245 @@ +package org.usvm.ts.pbt.usvm + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +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.JsNumber +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.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcePath +import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.mkRegisterStackLValue +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class UsvmScalarDomainProjectorTest { + @Test + fun `bounded integer accepts exactly integral non-negative-zero values inside inclusive bounds`() { + val domain = IntegerDomain(min = -2, max = 3) + + listOf(-2.0, 0.0, 3.0).forEach { value -> + assertTrue(acceptsNumber(domain, value), "Expected $value to be accepted") + } + listOf(-3.0, 4.0, 0.5, Double.NaN, Double.POSITIVE_INFINITY, -0.0).forEach { value -> + assertFalse(acceptsNumber(domain, value), "Expected $value to be rejected") + } + } + + @Test + fun `number bounds and NaN policy use shared JavaScript number semantics`() { + val bounded = NumberDomain( + min = JsNumber.finite(-1.5), + max = JsNumber.finite(2.5), + allowNaN = false, + ) + val unboundedWithNaN = NumberDomain(allowNaN = true) + + assertTrue(acceptsNumber(bounded, -1.5)) + assertTrue(acceptsNumber(bounded, 2.5)) + assertFalse(acceptsNumber(bounded, -1.6)) + assertFalse(acceptsNumber(bounded, 2.6)) + assertFalse(acceptsNumber(bounded, Double.NaN)) + assertTrue(acceptsNumber(unboundedWithNaN, Double.NaN)) + } + + @Test + fun `primitive constants admit only their declared JavaScript value`() { + val booleanDomain = ConstantDomain(JsConcreteValue.Boolean(value = true)) + val numberDomain = ConstantDomain(JsConcreteValue.number(7.25)) + + assertTrue(acceptsBoolean(booleanDomain, value = true)) + assertFalse(acceptsBoolean(booleanDomain, value = false)) + assertTrue(acceptsNumber(numberDomain, value = 7.25)) + assertFalse(acceptsNumber(numberDomain, value = 7.0)) + } + + @Test + fun `optional number admits its nested domain or exactly undefined`() { + val domain = OptionalDomain( + value = IntegerDomain(min = 1, max = 3), + nil = JsConcreteValue.Undefined, + ) + + assertTrue( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.fpTypeExpr, mkFpEqualExpr(value.extractFp(state.memory), mkFp(2.0, fp64Sort))) + } + }, + ) + assertTrue( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.refTypeExpr, mkHeapRefEq(value.extractRef(state.memory), mkUndefinedValue())) + } + }, + ) + assertFalse( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.fpTypeExpr, mkFpEqualExpr(value.extractFp(state.memory), mkFp(4.0, fp64Sort))) + } + }, + ) + assertFalse( + acceptsOptional(domain) { state, projection -> + with(state.ctx) { + val value = projection.inputs.single().value as UConcreteHeapRef + val type = value.getFakeType(state.memory) + + mkAnd(type.refTypeExpr, mkHeapRefEq(value.extractRef(state.memory), mkTsNullValue())) + } + }, + ) + } + + @Test + fun `string projection constrains inclusive UTF-16 length bounds`() { + val domain = StringDomain(minLength = 1, maxLength = 3) + + assertTrue(acceptsStringLength(domain, length = 1)) + assertTrue(acceptsStringLength(domain, length = 3)) + assertFalse(acceptsStringLength(domain, length = 0)) + assertFalse(acceptsStringLength(domain, length = 4)) + } + + private fun acceptsNumber(domain: PropertyDomain, value: Double): Boolean = acceptsScalar( + domain = domain, + exportName = "acceptsNumber", + ) { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(fp64Sort, 1)).asExpr(fp64Sort) + + mkEq(input, mkFp(value, fp64Sort)) + } + } + + private fun acceptsBoolean(domain: PropertyDomain, value: Boolean): Boolean = acceptsScalar( + domain = domain, + exportName = "acceptsBoolean", + ) { state -> + with(state.ctx) { + val input = state.memory.read(mkRegisterStackLValue(boolSort, 1)).asExpr(boolSort) + + mkEq(input, mkBool(value)) + } + } + + private fun acceptsOptional( + domain: OptionalDomain, + constraint: (TsState, UsvmDeclaredDomainProjection) -> UBoolExpr, + ): Boolean { + val manifest = manifest(domain, exportName = "acceptsOptionalNumber") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + state.pathConstraints += constraint(state, projection) + } + } + + private fun acceptsStringLength(domain: StringDomain, length: Int): Boolean { + val manifest = manifest(domain, exportName = "acceptsString") + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + val projection = projector.configure(state, manifest.inputs, target.bindings.inputs) + + with(state.ctx) { + val value = projection.inputs.single().value.asExpr(addressSort) + val arrayType = EtsArrayType(EtsStringType, dimensions = 1) + val projectedLength = state.memory.read(mkArrayLengthLValue(value, arrayType)) + + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + } + } + } + + private fun acceptsScalar( + domain: PropertyDomain, + exportName: String, + constraint: (TsState) -> UBoolExpr, + ): Boolean { + val manifest = manifest(domain, exportName) + val mapping = mapper.map(manifest) + val target = mapping.predicate.targets.single() + + return analyze(target.method) { state -> + projector.configure(state, manifest.inputs, target.bindings.inputs) + state.pathConstraints += constraint(state) + } + } + + private fun analyze( + method: org.jacodb.ets.model.EtsMethod, + configure: (TsState) -> Unit, + ): Boolean = runCatching { + TsMachine( + scene = scene, + options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze( + methods = listOf(method), + configureInitialState = { _, state -> configure(state) }, + ) + } + }.isSuccess + + private fun manifest(domain: PropertyDomain, exportName: String) = PropertyManifest( + propertyId = "usvm.scalar.$exportName", + inputs = listOf(PropertyInput(name = "value", domain = domain)), + predicate = TypeScriptEntryPoint( + module = "UsvmCapabilityFixture.ts", + exportName = exportName, + ), + ) + + companion object { + private lateinit var scene: EtsScene + private lateinit var mapper: PropertyEtsMapper + private val projector = UsvmDomainProjector() + + @JvmStatic + @BeforeAll + fun loadFixture() { + val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + scene = EtsScene(listOf(file)) + mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent)) + } + } +} diff --git a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts index 0f8e5ee7af..6a327ed5a2 100644 --- a/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts +++ b/usvm-ts-pbt/src/test/resources/properties/contract/PropertyExecutionContract.ts @@ -34,6 +34,18 @@ export function nonBooleanPredicate(_value: number): number { return 1; } +export function literalFalsePredicate(_value: number): false { + return false; +} + +export function literalTruePredicate(_value: number): true { + return true; +} + +export function neverPredicate(_value: number): never { + throw 'never predicate exploded'; +} + export function catchesExpectedException(_value: number): boolean { try { throw 'expected'; diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts new file mode 100644 index 0000000000..75c59dd333 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts @@ -0,0 +1,31 @@ +export function acceptsBoolean(value: boolean): boolean { + return value; +} + +export function acceptsNumber(value: number): boolean { + return value > 0; +} + +export function acceptsString(value: string): boolean { + return value.length > 0; +} + +export function acceptsOptionalNumber(value: number | undefined): boolean { + return value === undefined || value > 0; +} + +export function acceptsTuple(value: [number, string]): boolean { + return value.length === 2; +} + +export function acceptsNumberBooleanTuple(value: [number, boolean]): boolean { + return value !== undefined; +} + +export function acceptsNumberArray(value: number[]): boolean { + return value.length > 0; +} + +export function returnsNumber(value: number): number { + return value; +} diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts new file mode 100644 index 0000000000..5d7e1aa6d7 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPreconditionFixture.ts @@ -0,0 +1,27 @@ +export function predicate(value: number): boolean { + return value !== 0; +} + +export function isPositive(value: number): boolean { + return value > 0; +} + +export function alwaysFalse(_value: number): boolean { + return false; +} + +export function acceptsNonPositiveOrThrows(value: number): boolean { + if (value > 0) { + throw new Error("positive"); + } + + return true; +} + +export async function asyncIsPositive(value: number): Promise { + return value > 0; +} + +export function returnsNumber(value: number): number { + return value; +} diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts new file mode 100644 index 0000000000..d19ce7f06a --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmPropertySearchFixture.ts @@ -0,0 +1,71 @@ +export function validProperty(value: number): boolean { + return value === value; +} + +export function violatedProperty(value: number): boolean { + return value !== 2; +} + +export function positive(value: number): boolean { + return value > 0; +} + +export function signedOneProperty(value: number): boolean { + return value !== 1 && value !== -1; +} + +export function falsePrecondition(_value: number): boolean { + return false; +} + +export function throwingPrecondition(_value: number): boolean { + throw "precondition"; +} + +function identity(value: number): number { + return value; +} + +export function relationalProperty(value: number): boolean { + return identity(value) === identity(value + 1); +} + +export function unexpectedException(_value: number): boolean { + throw "unexpected"; +} + +export function assertionFailure(_value: number): boolean { + throw "AssertionError: expected non-zero"; +} + +export function falseStringProperty(_value: string): boolean { + return false; +} + +export function falseBooleanProperty(_value: boolean): boolean { + return false; +} + +export function falseOptionalProperty(_value: number | undefined): boolean { + return false; +} + +export function falseTupleProperty(_value: [number, boolean]): boolean { + return false; +} + +export function falseNestedTupleProperty(_value: [number | undefined, boolean]): boolean { + return false; +} + +export function falseArrayProperty(_value: number[]): boolean { + return false; +} + +export function nonBooleanProperty(value: number): number { + return value; +} + +export async function asyncValidProperty(value: number): Promise { + return value === value; +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 3d6b394f33..f37bc411a9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -11,8 +11,10 @@ import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget import org.usvm.machine.call.TsNoUnknownCallModels import org.usvm.machine.call.TsProfileUnknownCallDispatcher +import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallModelProvider +import org.usvm.machine.call.TsUnknownCallOutcome import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -38,6 +40,14 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} +/** Terminal states together with structured stop metadata for one TypeScript analysis. */ +data class TsMachineAnalysisResult( + val states: List, + val timedOut: Boolean, + val unsupportedCall: Boolean, + val engineFailed: Boolean, +) + class TsMachine( private val scene: EtsScene, override val options: UMachineOptions, @@ -56,21 +66,41 @@ class TsMachine( modelProvider = unknownCallModelProvider, observer = observer, ) + private val failureTrackingUnknownCallDispatcher = FailureTrackingUnknownCallDispatcher( + delegate = resolvedUnknownCallDispatcher, + ) private val interpreter = TsInterpreter( ctx = ctx, graph = graph, options = tsOptions, observer = observer, - unknownCallDispatcher = resolvedUnknownCallDispatcher, + unknownCallDispatcher = failureTrackingUnknownCallDispatcher, ) private val cfgStatistics = CfgStatisticsImpl(graph) fun analyze( methods: List, targets: List = emptyList(), - ): List { + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): List = analyzeWithMetadata( + methods = methods, + targets = targets, + configureInitialState = configureInitialState, + ).states + + fun analyzeWithMetadata( + methods: List, + targets: List = emptyList(), + configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, + ): TsMachineAnalysisResult { + interpreter.resetStepFailure() + failureTrackingUnknownCallDispatcher.reset() val initialStates = mutableMapOf() - methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + methods.forEach { method -> + initialStates[method] = interpreter.getInitialState(method, targets) { + configureInitialState(method, this) + } + } val methodsToTrackCoverage = when (options.coverageZone) { @@ -124,6 +154,7 @@ class TsMachine( val stepsStatistics = StepsStatistics() + var timedOut = false val stopStrategy = object : StopStrategy { val strategy = createStopStrategy( options, @@ -135,7 +166,15 @@ class TsMachine( ) override fun shouldStop(): Boolean { + if (options.timeout <= kotlin.time.Duration.ZERO) { + timedOut = true + return true + } + val result = strategy.shouldStop() + if (result && timeStatistics.runningTime >= options.timeout) { + timedOut = true + } if (result) { logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" } @@ -170,10 +209,35 @@ class TsMachine( stopStrategy = stopStrategy ) - return statesCollector.collectedStates + return TsMachineAnalysisResult( + states = statesCollector.collectedStates, + timedOut = timedOut, + unsupportedCall = failureTrackingUnknownCallDispatcher.pathStopped, + engineFailed = interpreter.stepFailed, + ) } override fun close() { components.close() } } + +private class FailureTrackingUnknownCallDispatcher( + private val delegate: TsUnknownCallDispatcher, +) : TsUnknownCallDispatcher { + var pathStopped: Boolean = false + private set + + override fun dispatch(scope: org.usvm.machine.interpreter.TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + val outcome = delegate.dispatch(scope, call) + if (outcome == TsUnknownCallOutcome.PATH_STOPPED) { + pathStopped = true + } + + return outcome + } + + fun reset() { + pathStopped = false + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt index e8f2ec65aa..524adf40c8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt @@ -61,3 +61,17 @@ class TsConcreteMethodCallStmt( return "concrete ${callee.signature.enclosingClass.name}::${callee.name}" } } + +/** Resumes the original entry point only when an auxiliary boolean guard returned true. */ +class TsEntryPointGuardResultStmt( + val entryPoint: EtsStmt, +) : EtsStmt { + override val location: EtsStmtLocation + get() = entryPoint.location + + override fun accept(visitor: EtsStmt.Visitor): R { + error("Auxiliary instruction") + } + + override fun toString(): String = "entry-point guard result" +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 0bf9f180b4..1ee6a18555 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -24,6 +24,7 @@ import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType @@ -45,6 +46,7 @@ import org.usvm.forkblacklists.UForkBlackList import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext +import org.usvm.machine.TsEntryPointGuardResultStmt import org.usvm.machine.TsGraph import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsOptions @@ -61,6 +63,7 @@ import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.expr.readGlobal import org.usvm.machine.expr.writeGlobal +import org.usvm.machine.state.TsEntryPointGuardOutcome import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt @@ -99,13 +102,19 @@ class TsInterpreter( ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() + internal var stepFailed: Boolean = false + private set + + internal fun resetStepFailure() { + stepFailed = false + } override fun step(state: TsState): StepResult { val stmt = state.lastStmt val scope = StepScope(state, forkBlackList) val result = state.methodResult - if (result is TsMethodResult.TsException) { + if (result is TsMethodResult.TsException && stmt !is TsEntryPointGuardResultStmt) { // TODO catch processing scope.doWithState { val returnSite = callStack.pop() @@ -132,6 +141,7 @@ class TsInterpreter( when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) + is TsEntryPointGuardResultStmt -> visitEntryPointGuardResult(scope, stmt) is EtsIfStmt -> visitIfStmt(scope, stmt) is EtsReturnStmt -> visitReturnStmt(scope, stmt) is EtsAssignStmt -> visitAssignStmt(scope, stmt) @@ -146,6 +156,7 @@ class TsInterpreter( } } } catch (e: Exception) { + stepFailed = true logger.error { "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { " $it" }}" } @@ -155,6 +166,45 @@ class TsInterpreter( return scope.stepResult() } + private fun visitEntryPointGuardResult( + scope: TsStepScope, + stmt: TsEntryPointGuardResultStmt, + ) = with(ctx) { + val result = scope.calcOnState { methodResult } + if (result !is TsMethodResult.Success) { + scope.doWithState { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.ERROR + callStack.pop() + } + return@with + } + val guard = result.value.takeIf { it.sort == boolSort }?.asExpr(boolSort) + if (guard == null) { + scope.doWithState { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.ERROR + callStack.pop() + } + return@with + } + + scope.fork( + condition = guard, + blockOnTrueState = { + methodResult = TsMethodResult.NoCall + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.NONE + newStmt(stmt.entryPoint) + }, + blockOnFalseState = { + entryPointGuardActive = false + entryPointGuardOutcome = TsEntryPointGuardOutcome.REJECTED + callStack.pop() + }, + ) + } + private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) = with(ctx) { val instance = stmt.instance @@ -708,7 +758,11 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + configureState: TsState.() -> Unit = {}, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -742,33 +796,40 @@ class TsInterpreter( } val parameterType = param.type - if (parameterType is EtsRefType) run { - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) - state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) + if (parameterType is EtsRefType) { + run { + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) + state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) - if (parameterType is EtsArrayType) { - state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) + if (parameterType is EtsArrayType) { + state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType) - val lengthLValue = mkArrayLengthLValue(ref, parameterType) - val length = state.memory.read(lengthLValue).asExpr(sizeSort) - state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + val lengthLValue = mkArrayLengthLValue(ref, parameterType) + val length = state.memory.read(lengthLValue).asExpr(sizeSort) + state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) - return@run - } + return@run + } - val resolvedParameterType = graph.hierarchy.classesForType(parameterType) + // Tuple inputs are materialized as fixed-size arrays by domain-aware initial-state configurators. + if (parameterType is EtsTupleType) { + return@run + } - if (resolvedParameterType.isEmpty()) { - logger.error("Cannot resolve class for parameter type: $parameterType") - return@run // TODO should be an error - } + val resolvedParameterType = graph.hierarchy.classesForType(parameterType) + + if (resolvedParameterType.isEmpty()) { + logger.error("Cannot resolve class for parameter type: $parameterType") + return@run // TODO should be an error + } - // Because of structural equality in TS we cannot determine the exact type - // Therefore, we create information about the fields the type must consist - val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) } - val auxiliaryType = EtsUnionType(types) // TODO error - state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) + // Because of structural equality in TS we cannot determine the exact type + // Therefore, we create information about the fields the type must consist + val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) } + val auxiliaryType = EtsUnionType(types) // TODO error + state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType) + } } if (parameterType == EtsNullType) { state.pathConstraints += mkHeapRefEq(ref, mkTsNullValue()) @@ -798,6 +859,8 @@ class TsInterpreter( } } + state.configureState() + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 172da63294..c133b954be 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -36,6 +36,13 @@ import org.usvm.targets.UTargetsSet import org.usvm.util.mkFieldLValue import org.usvm.util.type +/** Observable completion of an auxiliary entry-point guard. */ +enum class TsEntryPointGuardOutcome { + NONE, + REJECTED, + ERROR, +} + /** * [lValuesToAllocatedFakeObjects] contains records of l-values that were allocated with newly created fake objects. * It is important for result interpreters to be able to restore the order of fake objects allocation and @@ -74,6 +81,12 @@ class TsState( */ var dfltObjectFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), + /** True while an auxiliary entry-point guard or one of its callees is executing. */ + var entryPointGuardActive: Boolean = false, + + /** Terminal guard outcome; [TsEntryPointGuardOutcome.NONE] also covers predicate execution. */ + var entryPointGuardOutcome: TsEntryPointGuardOutcome = TsEntryPointGuardOutcome.NONE, + /** * Maps string values to their corresponding heap references that were allocated for string constants. * This tracks which string constants have been initialized in this particular state to avoid @@ -293,6 +306,8 @@ class TsState( boundThis = boundThis, dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, + entryPointGuardActive = entryPointGuardActive, + entryPointGuardOutcome = entryPointGuardOutcome, stringConstantAllocatedRefs = stringConstantAllocatedRefs, ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index 09ac543689..c884ada0ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -4,6 +4,8 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt import org.usvm.UExpr import org.usvm.USort +import org.usvm.machine.TsEntryPointGuardResultStmt +import org.usvm.util.type val TsState.lastStmt: EtsStmt get() = currentStatement @@ -27,6 +29,27 @@ fun TsState.returnValue(valueToReturn: UExpr) { } } +/** Executes [guard] over [arguments] before resuming this state's original entry point. */ +fun TsState.prependBooleanEntryPointGuard( + guard: EtsMethod, + arguments: List>, +) { + require(!entryPointGuardActive) { "An entry-point guard is already active" } + require(arguments.size == guard.parameters.size) { + "Expected ${guard.parameters.size} guard arguments, got ${arguments.size}" + } + + val originalEntryPoint = currentStatement + val receiver = memory.allocConcrete(requireNotNull(guard.enclosingClass).type) + val actualArguments = listOf(receiver) + arguments + + pushSortsForActualArguments(actualArguments) + callStack.push(guard, TsEntryPointGuardResultStmt(originalEntryPoint)) + memory.stack.push(actualArguments.toTypedArray(), guard.localsCount) + entryPointGuardActive = true + newStmt(guard.cfg.instructions.first()) +} + inline val EtsMethod.parametersWithThisCount: Int get() = parameters.size + 1 From 2d9b65a495c5a0c33854c4c59e36d0a986cf948e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 15:52:52 +0300 Subject: [PATCH 2/2] [TS PBT] Simplify USVM property execution flow --- .../usvm/ts/pbt/usvm/UsvmDomainProjector.kt | 33 ++--- .../usvm/ts/pbt/usvm/UsvmPropertyProjector.kt | 115 ++++++------------ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 101 +++++++-------- 3 files changed, 92 insertions(+), 157 deletions(-) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt index 3f70b7b6e5..4ba065068f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -39,9 +39,6 @@ import org.usvm.util.mkRegisterStackLValue /** One symbolic input written to the mapped EtsIR stack slot. */ data class UsvmProjectedInput( - val inputName: String, - val path: String, - val stackSlot: Int, val etsType: EtsType, val value: UExpr, ) @@ -65,7 +62,8 @@ class UsvmDomainProjector( "Property input count ${inputs.size} does not match EtsIR binding count ${bindings.size}" } - val preparedInputs = inputs.zip(bindings).mapIndexed { index, (input, binding) -> + val pairedInputs = inputs.zip(bindings) + pairedInputs.forEachIndexed { index, (input, binding) -> require(input.name == binding.propertyInputName) { "Property input ${input.name} does not match EtsIR binding ${binding.propertyInputName}" } @@ -77,27 +75,17 @@ class UsvmDomainProjector( path = path, options = options, ) - - PreparedInput(input, binding, path, capability) - } - preparedInputs.forEach { prepared -> - require(prepared.capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { - prepared.capability.diagnostics.joinToString { diagnostic -> diagnostic.message } + require(capability.level != org.usvm.ts.pbt.backend.ProjectionLevel.UNSUPPORTED) { + capability.diagnostics.joinToString { diagnostic -> diagnostic.message } } } - val projectedInputs = preparedInputs.map { prepared -> - val input = prepared.input - val binding = prepared.binding - val path = prepared.path - - val value = Materializer(state).materialize(input.domain, binding.parameter.type) + val materializer = Materializer(state) + val projectedInputs = pairedInputs.map { (input, binding) -> + val value = materializer.materialize(input.domain, binding.parameter.type) writeStackValue(state, binding.stackSlot, value) UsvmProjectedInput( - inputName = input.name, - path = path, - stackSlot = binding.stackSlot, etsType = binding.parameter.type, value = value, ) @@ -109,13 +97,6 @@ class UsvmDomainProjector( ) } - private data class PreparedInput( - val input: PropertyInput, - val binding: EtsInputBinding, - val path: String, - val capability: org.usvm.ts.pbt.backend.ProjectionCapability, - ) - private inner class Materializer(private val state: TsState) { fun materialize(domain: PropertyDomain, etsType: EtsType): UExpr = when (domain) { BooleanDomain -> state.makeSymbolicPrimitive(state.ctx.boolSort) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt index b8e9910946..1988e35667 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertyProjector.kt @@ -73,12 +73,10 @@ class UsvmPropertyProjector( concreteCapability = concreteCapability, options = projectionOptions, ) - val capabilityDiagnostics = capability.symbolic.diagnostics if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { return result( capability = capability, status = UsvmPreconditionStatus.UNSUPPORTED, - diagnostics = capabilityDiagnostics, ) } @@ -86,21 +84,21 @@ class UsvmPropertyProjector( ?: return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "An exact precondition target was unavailable after capability validation", path = "precondition", ), ) - val execution = analyzePreconditionTarget(manifest, preconditionTarget) - return classifyPreconditionAnalysis(capability, execution) + return analyzePreconditionTarget(manifest, preconditionTarget, capability) } private fun analyzePreconditionTarget( manifest: PropertyManifest, preconditionTarget: EtsEntryPointTarget, - ): UsvmPreconditionExecution = TsMachine( + capability: UsvmPropertyProjectionCapability, + ): UsvmPreconditionResult = TsMachine( scene = scene, options = machineOptions, tsOptions = tsOptions, @@ -119,44 +117,45 @@ class UsvmPropertyProjector( ) }, ) - val canResolve = !analysis.timedOut && analysis.states.isNotEmpty() && analysis.states.all { state -> - val methodResult = state.methodResult as? TsMethodResult.Success - methodResult != null && methodResult.value.sort == state.ctx.boolSort - } - val resolutions = if (canResolve) { - analysis.states.map(::retainTruePreconditionState) - } else { - emptyList() - } - UsvmPreconditionExecution(analysis, resolutions) + classifyPreconditionAnalysis(capability, analysis) } private fun classifyPreconditionAnalysis( capability: UsvmPropertyProjectionCapability, - execution: UsvmPreconditionExecution, + analysis: TsMachineAnalysisResult, ): UsvmPreconditionResult { - val analysis = execution.analysis val failure = classifyPreconditionFailure(capability, analysis) if (failure != null) { return failure } - val capabilityDiagnostics = capability.symbolic.diagnostics - val resolutions = execution.resolutions - if (resolutions.any { it is PreconditionStateResolution.SolverUnknown }) { - return result( - capability = capability, - status = UsvmPreconditionStatus.SOLVER_UNKNOWN, - diagnostics = capabilityDiagnostics + diagnostic( - code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, - message = "The solver could not classify a precondition result", - path = "precondition.result", - ), - ) - } - val acceptedStates = resolutions.mapNotNull { resolution -> - (resolution as? PreconditionStateResolution.Accepted)?.state + val acceptedStates = mutableListOf() + for (state in analysis.states) { + val methodResult = state.methodResult as TsMethodResult.Success + val returnValue = with(state.ctx) { + methodResult.value.asExpr(boolSort) + } + val acceptedState = state.clone() + acceptedState.pathConstraints += returnValue + + when (val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints)) { + is USatResult -> { + acceptedState.models = listOf(solverResult.model) + acceptedStates += acceptedState + } + + is UUnsatResult -> Unit + is UUnknownResult -> return result( + capability = capability, + status = UsvmPreconditionStatus.SOLVER_UNKNOWN, + additionalDiagnostic = diagnostic( + code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, + message = "The solver could not classify a precondition result", + path = "precondition.result", + ), + ) + } } val status = if (acceptedStates.isEmpty()) { UsvmPreconditionStatus.REJECTED @@ -168,7 +167,6 @@ class UsvmPropertyProjector( capability = capability, status = status, acceptedStates = acceptedStates, - diagnostics = capabilityDiagnostics, ) } @@ -176,13 +174,12 @@ class UsvmPropertyProjector( capability: UsvmPropertyProjectionCapability, analysis: TsMachineAnalysisResult, ): UsvmPreconditionResult? { - val capabilityDiagnostics = capability.symbolic.diagnostics val terminalStates = analysis.states if (terminalStates.any { state -> state.methodResult is TsMethodResult.TsException }) { return result( capability = capability, status = UsvmPreconditionStatus.PROPERTY_ERROR, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PRECONDITION_THREW, message = "The precondition has a reachable escaping exception", path = "precondition", @@ -193,7 +190,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Precondition analysis terminated without a method result", path = "precondition", @@ -208,7 +205,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.PROPERTY_ERROR, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PRECONDITION_RESULT_NON_BOOLEAN, message = "The precondition returned a non-boolean symbolic value", path = "precondition.result", @@ -219,7 +216,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.UNSUPPORTED, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, message = "The symbolic engine encountered an unsupported precondition call", path = "precondition", @@ -230,7 +227,7 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "The symbolic engine could not execute every reachable precondition path", path = "precondition", @@ -241,14 +238,13 @@ class UsvmPropertyProjector( return result( capability = capability, status = UsvmPreconditionStatus.TIMEOUT, - diagnostics = capabilityDiagnostics, ) } if (terminalStates.isEmpty()) { return result( capability = capability, status = UsvmPreconditionStatus.ENGINE_FAILURE, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Precondition analysis produced no terminal states", path = "precondition", @@ -259,36 +255,16 @@ class UsvmPropertyProjector( return null } - private fun retainTruePreconditionState(state: TsState): PreconditionStateResolution { - val result = state.methodResult as TsMethodResult.Success - val returnValue = with(state.ctx) { - result.value.asExpr(boolSort) - } - val acceptedState = state.clone() - acceptedState.pathConstraints += returnValue - val solverResult = acceptedState.ctx.solver().check(acceptedState.pathConstraints) - - return when (solverResult) { - is USatResult -> { - acceptedState.models = listOf(solverResult.model) - PreconditionStateResolution.Accepted(acceptedState) - } - - is UUnsatResult -> PreconditionStateResolution.Rejected - is UUnknownResult -> PreconditionStateResolution.SolverUnknown - } - } - private fun result( capability: UsvmPropertyProjectionCapability, status: UsvmPreconditionStatus, - diagnostics: List, acceptedStates: List = emptyList(), + additionalDiagnostic: CapabilityDiagnostic? = null, ) = UsvmPreconditionResult( capability = capability, status = status, acceptedStates = acceptedStates, - diagnostics = diagnostics, + diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), ) private fun diagnostic(code: String, message: String, path: String) = CapabilityDiagnostic( @@ -297,14 +273,3 @@ class UsvmPropertyProjector( path = path, ) } - -private data class UsvmPreconditionExecution( - val analysis: TsMachineAnalysisResult, - val resolutions: List, -) - -private sealed interface PreconditionStateResolution { - data class Accepted(val state: TsState) : PreconditionStateResolution - data object Rejected : PreconditionStateResolution - data object SolverUnknown : PreconditionStateResolution -} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 9522aedb42..9038f2d17f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -50,13 +50,11 @@ class UsvmPropertySearcher( concreteCapability = concreteCapability, options = projectionOptions, ) - val capabilityDiagnostics = capability.symbolic.diagnostics if (capability.symbolic.level == ProjectionLevel.UNSUPPORTED) { return result( manifest = manifest, status = UsvmPropertySearchStatus.UNSUPPORTED, capability = capability, - diagnostics = capabilityDiagnostics, ) } @@ -65,36 +63,19 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "An exact predicate target was unavailable after capability validation", path = "predicate", ), ) val precondition = mapping.precondition?.exactTargetOrNull() - val execution = executeSearch(manifest, predicate, precondition) - val terminalFailure = classifyTerminalFailure( - manifest = manifest, - capability = capability, - analysis = execution.analysis, - ) - if (terminalFailure != null) { - return terminalFailure - } - - val violationState = execution.observer.violationStates.firstOrNull() - ?: return noViolationResult( - manifest = manifest, - capability = capability, - analysis = execution.analysis, - observer = execution.observer, - ) - return violationResult( + return executeSearch( manifest = manifest, + predicate = predicate, + precondition = precondition, capability = capability, - violationState = violationState, - projection = execution.projection, ) } @@ -102,17 +83,19 @@ class UsvmPropertySearcher( manifest: PropertyManifest, predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, - ): UsvmSearchExecution { + capability: UsvmPropertyProjectionCapability, + ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() val observer = UsvmViolationObserver(target) - val analysis = TsMachine( + + return TsMachine( scene = scene, options = machineOptions, tsOptions = tsOptions, machineObserver = observer, ).use { machine -> - machine.analyzeWithMetadata( + val analysis = machine.analyzeWithMetadata( methods = listOf(predicate.method), targets = listOf(target), configureInitialState = { method, state -> @@ -130,13 +113,30 @@ class UsvmPropertySearcher( } }, ) - } + val terminalFailure = classifyTerminalFailure( + manifest = manifest, + capability = capability, + analysis = analysis, + ) + if (terminalFailure != null) { + return@use terminalFailure + } - return UsvmSearchExecution( - analysis = analysis, - observer = observer, - projection = projection, - ) + val violationState = observer.violationStates.firstOrNull() + ?: return@use noViolationResult( + manifest = manifest, + capability = capability, + analysis = analysis, + observer = observer, + ) + + violationResult( + manifest = manifest, + capability = capability, + violationState = violationState, + projection = projection, + ) + } } private fun classifyTerminalFailure( @@ -149,7 +149,6 @@ class UsvmPropertySearcher( return preconditionFailure } - val capabilityDiagnostics = capability.symbolic.diagnostics val predicateContractError = analysis.states.any { state -> val methodResult = state.methodResult as? TsMethodResult.Success state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && @@ -161,7 +160,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.PROPERTY_ERROR, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_PREDICATE_RESULT_NON_BOOLEAN, message = "The predicate returned a non-boolean symbolic value", path = "predicate.result", @@ -177,7 +176,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Predicate analysis terminated without a method result", path = "predicate", @@ -189,7 +188,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.UNSUPPORTED, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_EXECUTION_UNSUPPORTED, message = "The symbolic engine encountered an unsupported property call", path = "predicate", @@ -201,7 +200,7 @@ class UsvmPropertySearcher( manifest = manifest, status = UsvmPropertySearchStatus.ENGINE_FAILURE, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic( + additionalDiagnostic = diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "The symbolic engine could not execute every reachable property path", path = "predicate", @@ -217,7 +216,6 @@ class UsvmPropertySearcher( capability: UsvmPropertyProjectionCapability, analysis: TsMachineAnalysisResult, ): UsvmPropertySearchResult? { - val capabilityDiagnostics = capability.symbolic.diagnostics val preconditionError = analysis.states.firstOrNull { state -> state.entryPointGuardOutcome == TsEntryPointGuardOutcome.ERROR } @@ -251,7 +249,7 @@ class UsvmPropertySearcher( manifest = manifest, status = status, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic, + additionalDiagnostic = diagnostic, ) } @@ -261,7 +259,6 @@ class UsvmPropertySearcher( analysis: TsMachineAnalysisResult, observer: UsvmViolationObserver, ): UsvmPropertySearchResult { - val capabilityDiagnostics = capability.symbolic.diagnostics val predicateCompleted = analysis.states.any { state -> state.entryPointGuardOutcome == TsEntryPointGuardOutcome.NONE && state.methodResult is TsMethodResult.Success @@ -276,27 +273,27 @@ class UsvmPropertySearcher( preconditionRejected -> UsvmPropertySearchStatus.PRECONDITION_REJECTED else -> UsvmPropertySearchStatus.ENGINE_FAILURE } - val diagnostics = when (status) { - UsvmPropertySearchStatus.SOLVER_UNKNOWN -> capabilityDiagnostics + diagnostic( + val additionalDiagnostic = when (status) { + UsvmPropertySearchStatus.SOLVER_UNKNOWN -> diagnostic( code = PbtDiagnosticCode.USVM_SOLVER_UNKNOWN, message = "The solver could not classify a predicate result", path = "predicate.result", ) - UsvmPropertySearchStatus.ENGINE_FAILURE -> capabilityDiagnostics + diagnostic( + UsvmPropertySearchStatus.ENGINE_FAILURE -> diagnostic( code = PbtDiagnosticCode.USVM_ENGINE_FAILURE, message = "Property search produced no classified terminal state", path = "predicate", ) - else -> capabilityDiagnostics + else -> null } return result( manifest = manifest, status = status, capability = capability, - diagnostics = diagnostics, + additionalDiagnostic = additionalDiagnostic, ) } @@ -306,7 +303,6 @@ class UsvmPropertySearcher( violationState: TsState, projection: UsvmDeclaredDomainProjection, ): UsvmPropertySearchResult { - val capabilityDiagnostics = capability.symbolic.diagnostics val violationTarget = classifyViolation(violationState) val inputs = runCatching { inputResolver.resolve(violationState, manifest.inputs, projection) @@ -322,7 +318,7 @@ class UsvmPropertySearcher( status = UsvmPropertySearchStatus.FAILED_INPUT_RESOLUTION, target = violationTarget, capability = capability, - diagnostics = capabilityDiagnostics + diagnostic, + additionalDiagnostic = diagnostic, ) } @@ -332,7 +328,6 @@ class UsvmPropertySearcher( target = violationTarget, inputs = inputs, capability = capability, - diagnostics = capabilityDiagnostics, ) } @@ -370,25 +365,19 @@ class UsvmPropertySearcher( manifest: PropertyManifest, status: UsvmPropertySearchStatus, capability: UsvmPropertyProjectionCapability, - diagnostics: List, target: UsvmPropertyViolationTarget? = null, inputs: List? = null, + additionalDiagnostic: CapabilityDiagnostic? = null, ) = UsvmPropertySearchResult( propertyId = PropertyId(manifest.propertyId), status = status, target = target, inputs = inputs, capability = capability, - diagnostics = diagnostics, + diagnostics = capability.symbolic.diagnostics + listOfNotNull(additionalDiagnostic), ) } -private data class UsvmSearchExecution( - val analysis: TsMachineAnalysisResult, - val observer: UsvmViolationObserver, - val projection: UsvmDeclaredDomainProjection, -) - private class UsvmViolationTsTarget : TsTarget(location = null) private class UsvmViolationObserver(