diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 60feb720dc..e65ae84670 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -84,7 +84,8 @@ class TsUnknownCallModelSuccessor( * A semantic-model execution plan. * * [residualGuard] is the input domain not covered by the model. `null` means that the model completely handles every - * state accepted by [TsUnknownCallModel.apply]. + * state accepted by [TsUnknownCallModel.apply]. States excluded by every successor guard are pruned, for example + * when a model-owned assumption is inconsistent with the current path. */ class TsUnknownCallModelExecution( successors: List, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 7cb6ca3a13..f27af0a0fc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -143,7 +143,10 @@ class TsModelUnknownCallDispatcher( } scope.forkMulti(guardedStateChanges) - if (modelApplied) { + // A complete relation (including assume(false)) may have no feasible outputs. That is pruning, + // not an unsupported call and not a request to invent a fresh result. + val modelPruned = !modelApplied && !freshResidualApplied && !stoppedResidualIsSatisfiable + if (modelApplied || modelPruned) { observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(application.modelId))) } if (freshResidualApplied || stoppedResidualIsSatisfiable) { @@ -154,7 +157,7 @@ class TsModelUnknownCallDispatcher( modelApplied -> TsUnknownCallOutcome.MODEL_APPLIED freshResidualApplied -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN stoppedResidualIsSatisfiable -> TsUnknownCallOutcome.PATH_STOPPED - else -> error("Semantic model ${application.modelId} produced no satisfiable successor or residual state") + else -> TsUnknownCallOutcome.MODEL_APPLIED } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsModelAssume.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsModelAssume.kt new file mode 100644 index 0000000000..679d07a7d5 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsModelAssume.kt @@ -0,0 +1,50 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.state.TsState + +/** + * Restricts a private source-model path without admitting the condition's negative domain. + * Source artifacts declare `TsModelPrimitives.assume(condition: boolean): void` and depend on [id]. + * The argument must already be a Boolean term; evaluating short-circuit source expressions may itself branch. + */ +internal object TsModelAssume : TsBuiltInUnknownCallModel { + override val id: String = "ts.model.assume" + override val target = TsUnknownCallTarget( + methodName = "assume", + enclosingClassName = "TsModelPrimitives", + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + val helperOwner = call.callee.enclosingClass + val caller = call.callSite.location.method + val callerOwner = caller.signature.enclosingClass + val sameArtifact = helperOwner.file == callerOwner.file && helperOwner.namespace == null + val privateSourceCaller = state.ctx.isSourceModelClass(callerOwner) + val ownsActiveFrame = state.isUnknownCallModelFileActive(helperOwner) + if (!sameArtifact || !privateSourceCaller || !ownsActiveFrame) return null + + check(call.receiver == null && call.arguments.size == 1) { + "Private model assume requires one boolean argument" + } + val condition = requireNotNull(call.arguments.single().resolved) { + "Private model assume requires an evaluated boolean argument" + } + check(condition.sort == state.ctx.boolSort) { + "Private model assume requires a boolean term, got ${condition.sort}" + } + + val successor = TsUnknownCallModelSuccessor( + guard = condition.asExpr(state.ctx.boolSort), + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + return TsUnknownCallModelExecution(successors = listOf(successor)) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModelAssumeTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModelAssumeTest.kt new file mode 100644 index 0000000000..5689431a47 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModelAssumeTest.kt @@ -0,0 +1,249 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNamespaceSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.isTrue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsMachineAnalysisResult +import org.usvm.machine.TsMethodCall +import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsModelAssume +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.solver.USatResult +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsModelAssumeTest { + @TempDir + lateinit var directory: Path + + private val sourcePath = getResourcePath("/models/SourceAssumeCalls.ts") + private val scene = EtsScene(listOf(loadEtsFileAutoConvert(sourcePath, provider = EtsIrProvider.TS_FRONTEND))) + private val artifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = getResourcePath("/models/SourceAssumeModels.ts"), + entryPointClassName = "SourceAssumeModels", + entryPointMethodName = "always", + ) + private val models = TsUnknownCallModelCatalog( + listOf("always", "never", "gated", "positive").map { name -> + val entryPoint = artifact.entryPoint.enclosingClass!!.methods.single { it.name == name } + TsEtsIrUnknownCallModel( + id = "test.assume.$name", + target = TsUnknownCallTarget(methodName = name, enclosingClassName = "ExternalAssume"), + artifact = artifact.copy(entryPoint = entryPoint), + requiredModelIds = setOf(TsModelAssume.id), + ) + } + TsModelAssume, + selection = TsUnknownCallModelSelection.Only( + setOf("test.assume.always", "test.assume.never", "test.assume.gated", "test.assume.positive") + ), + ) + + @Test + fun `true continues and false prunes without fallback or unsupported outcome`() { + val accepted = analyze("always") + val rejected = analyze("never") + + assertEquals(expected = 1, actual = accepted.states.size) + assertTrue(rejected.states.isEmpty()) + for (result in listOf(accepted, rejected)) { + assertFalse(result.analysis.engineFailed) + assertFalse(result.analysis.unsupportedCall) + assertTrue(result.analysis.unsupportedPaths.isEmpty()) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.MODEL_APPLIED), + result.events.map { it.outcome }, + ) + } + } + + @Test + fun `symbolic assumption keeps only its positive domain and refreshes witness models`() { + var cachedOrder = emptyList() + val result = analyze("gated") { state -> + val argument = state.ctx.mkRegisterReading(idx = 1, sort = state.ctx.boolSort) + val cachedModels = listOf(state.ctx.mkNot(argument), argument).map { guard -> + val constraints = state.pathConstraints.clone() + constraints += guard + when (val result = state.ctx.solver().check(constraints)) { + is USatResult -> result.model + else -> error("Both boolean cache domains must be feasible") + } + } + state.models = cachedModels + cachedOrder = cachedModels.map { it.eval(argument).isTrue } + } + val method = method("gated") + + assertEquals(listOf(false, true), cachedOrder) + assertEquals(expected = 1, actual = result.states.size) + val state = result.states.single() + val test = TsTestResolver().resolve(method, state) + assertTrue(assertIs(test.before.parameters.single()).value) + assertEquals(1.0, assertIs(test.returnValue).number) + assertTrue(state.models.isNotEmpty()) + for (model in state.models) { + val argument = state.ctx.mkRegisterReading(idx = 1, sort = state.ctx.boolSort) + assertTrue(model.eval(argument).isTrue) + } + } + + @Test + fun `application declarations cannot acquire assume semantics`() { + val result = analyze("foreign") + val test = TsTestResolver().resolve(method("foreign"), result.states.single()) + + assertEquals(9.0, assertIs(test.returnValue).number) + assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), result.events.map { it.outcome }) + } + + @Test + fun `namespaced helper cannot impersonate the private helper inside an active artifact`() { + var checked = false + val observer = object : TsInterpreterObserver { + override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + if (stmt is TsMethodCall) return + val expression = stmt.callExpr ?: return + if (expression.callee.name != "assume") return + + val owner = expression.callee.enclosingClass + val forgedOwner = owner.copy(namespace = EtsNamespaceSignature(name = "Forged", file = owner.file)) + scope.calcOnState { + val call = TsUnknownCall( + callee = expression.callee.copy(enclosingClass = forgedOwner), + receiver = null, + arguments = listOf(TsUnknownCallValue(expression.args.single(), ctx.trueExpr)), + resultType = expression.type, + callSite = stmt, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ) + assertTrue(isUnknownCallModelFileActive(owner)) + assertNull(TsModelAssume.apply(this, call)) + checked = true + } + } + } + + TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + unknownCallModels = models, + observer = observer, + ).use { machine -> machine.analyze(listOf(method("always"))) } + + assertTrue(checked) + } + + @Test + fun `private artifact helper requires its active dispatcher frame`() { + val callSite = artifact.entryPoint.cfg.stmts.single { it.callExpr?.callee?.name == "assume" } + val expression = requireNotNull(callSite.callExpr) + var checked = false + + analyze("always") { state -> + val call = TsUnknownCall( + callee = expression.callee, + receiver = null, + arguments = listOf(TsUnknownCallValue(expression.args.single(), state.ctx.trueExpr)), + resultType = expression.type, + callSite = callSite, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ) + assertNull(TsModelAssume.apply(state, call)) + checked = true + } + + assertTrue(checked) + } + + @Test + fun `positive numeric witnesses replay in the original source contract`() { + val method = method("positive") + val result = analyze("positive") + val checks = result.states.map { state -> + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).number + val output = assertIs(test.returnValue).number + assertTrue(input > 0) + assertEquals(input, output) + "if (!Object.is(new SourceAssumeCalls().positive($input), $output)) throw Error('positive');" + } + assertTrue(checks.isNotEmpty()) + + assertNodeReplay( + source = sourcePath.readText() + "\nconst ExternalAssume = { positive: value => value };\n" + + checks.joinToString(separator = "\n"), + directory = directory, + name = "assume-positive", + timeoutMessage = "Assume witness replay timed out", + ) + } + + private fun analyze(name: String, configureInitialState: (TsState) -> Unit = {}): Result { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + val analysis = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + unknownCallModels = models, + observer = observer, + ).use { machine -> + machine.analyzeWithMetadata(listOf(method(name))) { _, state -> configureInitialState(state) } + } + return Result(analysis = analysis, events = events) + } + + private fun method(name: String): EtsMethod = scene.projectClasses.single { it.name == "SourceAssumeCalls" } + .methods + .single { it.name == name } + + private data class Result( + val analysis: TsMachineAnalysisResult, + val events: List, + ) { + val states: List get() = analysis.states + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 252c729ebb..17253ef33e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -14,6 +14,7 @@ import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily +import org.usvm.machine.call.intrinsic.TsModelAssume import org.usvm.machine.call.intrinsic.TsNumericIntrinsicModelFamily import org.usvm.machine.state.TsState import kotlin.test.Test @@ -213,6 +214,7 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.MATH_ROUND_ID, TsNumericIntrinsicModelFamily.MATH_SQRT_ID, TsNumericIntrinsicModelFamily.MATH_TRUNC_ID, + TsModelAssume.id, TsNumericIntrinsicModelFamily.NUMBER_IS_FINITE_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, diff --git a/usvm-ts/src/test/resources/models/SourceAssumeCalls.ts b/usvm-ts/src/test/resources/models/SourceAssumeCalls.ts new file mode 100644 index 0000000000..8320063709 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SourceAssumeCalls.ts @@ -0,0 +1,22 @@ +declare class ExternalAssume { + static always(): number; + static never(): number; + static gated(condition: boolean): number; + static positive(value: number): number; +} + +declare class TsModelPrimitives { + static assume(condition: boolean): void; +} + +export class SourceAssumeCalls { + always(): number { return ExternalAssume.always(); } + never(): number { return ExternalAssume.never(); } + gated(condition: boolean): number { return ExternalAssume.gated(condition); } + positive(value: number): number { return ExternalAssume.positive(value); } + + foreign(): number { + TsModelPrimitives.assume(false); + return 9; + } +} diff --git a/usvm-ts/src/test/resources/models/SourceAssumeModels.ts b/usvm-ts/src/test/resources/models/SourceAssumeModels.ts new file mode 100644 index 0000000000..5663597f01 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SourceAssumeModels.ts @@ -0,0 +1,25 @@ +declare class TsModelPrimitives { + static assume(condition: boolean): void; +} + +export class SourceAssumeModels { + static always(): number { + TsModelPrimitives.assume(true); + return 7; + } + + static never(): number { + TsModelPrimitives.assume(false); + return 7; + } + + static gated(condition: boolean): number { + TsModelPrimitives.assume(condition); + return condition ? 1 : 0; + } + + static positive(value: number): number { + TsModelPrimitives.assume(value > 0); + return value; + } +}