diff --git a/buildSrc/src/main/kotlin/DetektConfiguration.kt b/buildSrc/src/main/kotlin/DetektConfiguration.kt index b1fa87b9b9..926b917ef3 100644 --- a/buildSrc/src/main/kotlin/DetektConfiguration.kt +++ b/buildSrc/src/main/kotlin/DetektConfiguration.kt @@ -3,6 +3,7 @@ import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.detektPlugi import io.gitlab.arturbosch.detekt.Detekt import io.gitlab.arturbosch.detekt.DetektCreateBaselineTask import io.gitlab.arturbosch.detekt.report.ReportMergeTask +import org.gradle.api.JavaVersion import org.gradle.api.Project import org.gradle.api.tasks.TaskProvider import org.gradle.kotlin.dsl.assign @@ -34,17 +35,21 @@ fun Project.configureDetekt() { .resolve("${project}-${taskPostfix}.yml") } val configFile = rootDir.resolve("detekt").resolve("config.yml") + val tsConfigFile = rootDir.resolve("detekt").resolve("ts-config.yml") val reportFile = rootProject.layout.buildDirectory.file("reports/detekt/detekt.sarif") + val usesStrictTsRules = name in STRICT_TS_DETEKT_PROJECTS + val configFiles = if (usesStrictTsRules) listOf(configFile, tsConfigFile) else listOf(configFile) detekt { buildUponDefaultConfig = true - ignoreFailures = true + ignoreFailures = !usesStrictTsRules parallel = true - config.setFrom(configFile) + config.setFrom(configFiles) } tasks.withType { + jvmTarget = JavaVersion.VERSION_1_8.toString() setIncludes(includes) setExcludes(excludes) @@ -61,6 +66,7 @@ fun Project.configureDetekt() { } tasks.withType { + jvmTarget = JavaVersion.VERSION_1_8.toString() baseline = resolveBaselineFile(project.name, this@withType.name) } @@ -82,3 +88,5 @@ fun Project.configureDetekt() { setDependsOn(dependsOn.filterNot { it is TaskProvider<*> && it.name == "detekt" }) } } + +private val STRICT_TS_DETEKT_PROJECTS = setOf("usvm-ts", "usvm-ts-pbt") diff --git a/detekt/baselines/usvm-ts-Main.yml b/detekt/baselines/usvm-ts-Main.yml new file mode 100644 index 0000000000..24a7b7ba16 --- /dev/null +++ b/detekt/baselines/usvm-ts-Main.yml @@ -0,0 +1,157 @@ + + + + + ArgumentListWrapping:TsImports.kt$("File not found for relative path: '$importPath' from ${currentFile.signature.fileName}") + BracesOnWhenStatements:CallApproximations.kt$when + BracesOnWhenStatements:ReadField.kt$when + BracesOnWhenStatements:ReadLength.kt$when + BracesOnWhenStatements:TsBinaryOperator.kt$TsBinaryOperator.Add$when + BracesOnWhenStatements:TsBinaryOperator.kt$TsBinaryOperator.StrictEq$when + BracesOnWhenStatements:TsContext.kt$TsContext$when + BracesOnWhenStatements:TsInterpreter.kt$TsInterpreter$when + CascadingCallWrapping:TsExprResolver.kt$TsExprResolver$type + CascadingCallWrapping:TsState.kt$TsState$stmt.location.method.cfg.blocks.indexOfFirst { it.statements.contains(stmt) } .takeIf { it >= 0 } ?: error("Statement $stmt is not found in the method CFG") + CascadingCallWrapping:UnreachableCodeDetector.kt$UnreachableCodeDetector$toMap() + ChainWrapping:TsTypeSystem.kt$TsTypeSystem$&& + CommentSpacing:CallApproximations.kt$//! Note: `reversedArray` is a temporary object not used outside this function, + Filename:TsApproximations.kt$org.usvm.machine.expr.TsApproximations.kt + ImportOrdering:TsContext.kt$import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UBv32Sort import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.allocateStaticRef import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue import org.usvm.isTrue import org.usvm.machine.Constants.Companion.MAGIC_OFFSET import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.TsVoidSort import org.usvm.machine.expr.TsVoidValue import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory import org.usvm.types.single import org.usvm.util.mkFieldLValue import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract + Indentation:TsTypeSystem.kt$TsTypeSystem$ + LargeClass:TsExprResolver.kt$TsExprResolver : Visitor + LongMethod:TsBinaryOperator.kt$TsBinaryOperator$fun <R : USort> TsContext.commonResolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, resultSort: R, reduce: (List<ExprWithTypeConstraint<R>>) -> UExpr<R>, ): UExpr<R>? + LongMethod:TsInterpreter.kt$TsInterpreter$private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) + LongMethod:TsTypeSystem.kt$TsTypeSystem$override fun isSupertype(supertype: EtsType, type: EtsType): Boolean + MagicNumber:CallApproximations.kt$3 + MagicNumber:EtsHierarchy.kt$EtsHierarchy$100 + MagicNumber:TsExprResolver.kt$TsExprResolver$3 + MagicNumber:TsInterpreter.kt$TsInterpreter$10 + MagicNumber:TsInterpreter.kt$TsInterpreter$5 + MatchingDeclarationName:TsApproximations.kt$TsExprApproximationResult + MatchingDeclarationName:TsPromise.kt$PromiseState + MaxChainedCallsOnSameLine:TsState.kt$TsState$stmt.location.method.cfg.blocks.indexOfFirst { it.statements.contains(stmt) } + MaxLineLength:TsExprResolver.kt$TsSimpleValueResolver$logger.error { "Cannot find symbol '$local' in '${resolutionResult.file.name}': ${resolutionResult.reason}" } + MaxLineLength:TsImports.kt$ImportResolutionResult.NotFound("File not found for relative path: '$importPath' from ${currentFile.signature.fileName}") + MaximumLineLength:TsExprResolver.kt$TsSimpleValueResolver$ + MaximumLineLength:TsImports.kt$ + MultiLineIfElse:TsInterpreter.kt$TsInterpreter$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) 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 } 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) } + NestedBlockDepth:Call.kt$internal fun TsExprResolver.handleInstanceCall( expr: EtsInstanceCallExpr, ): UExpr<*>? + NestedBlockDepth:ReadArray.kt$internal fun TsExprResolver.handleArrayAccess( value: EtsArrayAccess, ): UExpr<*>? + NestedBlockDepth:ReadField.kt$internal fun TsExprResolver.handleInstanceFieldRef( value: EtsInstanceFieldRef, ): UExpr<*>? + NestedBlockDepth:TsExprResolver.kt$TsExprResolver$override fun visit(expr: EtsAwaitExpr): UExpr<out USort>? + NestedBlockDepth:TsExprResolver.kt$TsExprResolver$override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? + NestedBlockDepth:TsExprResolver.kt$TsSimpleValueResolver$private fun resolveLocal(local: EtsValue): UExpr<*>? + NestedBlockDepth:TsInterpreter.kt$TsInterpreter$private fun assignToInDfltDflt( scope: TsStepScope, lhv: EtsLValue, expr: UExpr<*>, ): Unit? + NestedBlockDepth:TsInterpreter.kt$TsInterpreter$private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt) + NestedBlockDepth:WriteField.kt$internal fun TsExprResolver.handleAssignToInstanceField( lhv: EtsInstanceFieldRef, expr: UExpr<*>, ): Unit? + NoBlankLineInList:TsState.kt$TsState$ + NoEmptyFirstLineInMethodBlock:TsInterpreter.kt$TsInterpreter$ + NoMultipleSpaces:TsTypeSystem.kt$TsTypeSystem$ + NoNameShadowing:EtsFieldResolver.kt$field + NoNameShadowing:EtsFieldResolver.kt${ it.name != CONSTRUCTOR_NAME } + NoNameShadowing:EtsFieldResolver.kt${ it.name } + NoNameShadowing:EtsHierarchy.kt$EtsHierarchy$result + NoNameShadowing:TsBinaryOperator.kt$TsBinaryOperator.Eq$lhs + NoNameShadowing:TsBinaryOperator.kt$TsBinaryOperator.Eq$rhs + NoNameShadowing:TsInterpreter.kt$TsInterpreter$ref + NoNameShadowing:TsInterpreter.kt$TsInterpreter${ it.methods.any { it.name == stmt.callee.name } } + NoNameShadowing:TsInterpreter.kt$TsInterpreter${ it.name == stmt.callee.name } + NoNameShadowing:WriteField.kt$field + NoSemicolons:TsPromise.kt$PromiseState.REJECTED$; + TooGenericExceptionCaught:TsImports.kt$e: Exception + TooGenericExceptionCaught:TsInterpreter.kt$TsInterpreter$e: Exception + TrailingCommaOnDeclarationSite:TsPromise.kt$PromiseState + UnderscoresInNumericLiterals:TsContext.kt$Constants.Companion$1000000 + UndocumentedPublicClass:EtsFakeType.kt$EtsFakeType : EtsType + UndocumentedPublicClass:EtsFakeType.kt$ExprWithTypeConstraint<Sort : USort> + UndocumentedPublicClass:EtsFieldResolver.kt$TsResolutionResult$Empty : TsResolutionResult + UndocumentedPublicClass:EtsFieldResolver.kt$TsResolutionResult<out T> + UndocumentedPublicClass:EtsHierarchy.kt$EtsHierarchy + UndocumentedPublicClass:ReachabilityObserver.kt$ReachabilityObserver : UMachineObserver + UndocumentedPublicClass:TsApproximations.kt$TsExprApproximationResult + UndocumentedPublicClass:TsApproximations.kt$TsExprApproximationResult$NoApproximation : TsExprApproximationResult + UndocumentedPublicClass:TsApproximations.kt$TsExprApproximationResult$ResolveFailure : TsExprApproximationResult + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Add : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$And : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Div : TsArithmeticOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Eq : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Gt : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Lt : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Mul : TsArithmeticOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Neq : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Or : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Rem : TsArithmeticOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$StrictEq : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$StrictNeq : TsBinaryOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$Sub : TsArithmeticOperator + UndocumentedPublicClass:TsBinaryOperator.kt$TsBinaryOperator$TsArithmeticOperator : TsBinaryOperator + UndocumentedPublicClass:TsComponents.kt$TsComponents : UComponents + UndocumentedPublicClass:TsContext.kt$Constants + UndocumentedPublicClass:TsContext.kt$IntermediateLValueField + UndocumentedPublicClass:TsContext.kt$TsContext : UContext + UndocumentedPublicClass:TsExprResolver.kt$TsExprResolver : Visitor + UndocumentedPublicClass:TsExprResolver.kt$TsSimpleValueResolver : Visitor + UndocumentedPublicClass:TsExpressions.kt$TsUndefinedSort : USort + UndocumentedPublicClass:TsExpressions.kt$TsUndefinedValue : UExpr + UndocumentedPublicClass:TsExpressions.kt$TsVoidSort : USort + UndocumentedPublicClass:TsExpressions.kt$TsVoidValue : UExpr + UndocumentedPublicClass:TsFunction.kt$TsFunction + UndocumentedPublicClass:TsGraph.kt$TsGraph : ApplicationGraph + UndocumentedPublicClass:TsImports.kt$ImportResolutionResult + UndocumentedPublicClass:TsImports.kt$SymbolResolutionResult + UndocumentedPublicClass:TsInterpreter.kt$TsInterpreter : UInterpreter + UndocumentedPublicClass:TsInterpreterObserver.kt$TsInterpreterObserver : UInterpreterObserver + UndocumentedPublicClass:TsMachine.kt$TsMachine : UMachine + UndocumentedPublicClass:TsMethodCall.kt$TsConcreteMethodCallStmt : TsMethodCall + UndocumentedPublicClass:TsMethodCall.kt$TsMethodCall : EtsStmt + UndocumentedPublicClass:TsMethodCall.kt$TsVirtualMethodCallStmt : TsMethodCall + UndocumentedPublicClass:TsMethodResult.kt$TsMethodResult$Success : TsMethodResult + UndocumentedPublicClass:TsOptions.kt$TsOptions + UndocumentedPublicClass:TsPromise.kt$PromiseState + UndocumentedPublicClass:TsStateVisualizer.kt$TsStateVisualizer : TsInterpreterObserverUMachineObserver + UndocumentedPublicClass:TsTarget.kt$TsReachabilityTarget : TsTarget + UndocumentedPublicClass:TsTarget.kt$TsTarget : UTarget + UndocumentedPublicClass:TsTest.kt$GlobalFieldValue + UndocumentedPublicClass:TsTest.kt$NoCoverage : TsMethodCoverage + UndocumentedPublicClass:TsTest.kt$TsMethodCoverage + UndocumentedPublicClass:TsTest.kt$TsParametersState + UndocumentedPublicClass:TsTest.kt$TsTest + UndocumentedPublicClass:TsTest.kt$TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsAny : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsException : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsNull : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsNumber : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsUndefined : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue$TsUnknown : TsTestValue + UndocumentedPublicClass:TsTest.kt$TsTestValue.TsException$UnknownException : TsException + UndocumentedPublicClass:TsTransformer.kt$TsComposer : UComposerTsTransformer + UndocumentedPublicClass:TsTransformer.kt$TsExprTranslator : UExprTranslatorTsTransformer + UndocumentedPublicClass:TsTransformer.kt$TsTransformer : UTransformer + UndocumentedPublicClass:TsTypeSystem.kt$TsTypeSystem : UTypeSystem + UndocumentedPublicClass:TsUnaryOperator.kt$TsUnaryOperator + UndocumentedPublicClass:TsUnaryOperator.kt$TsUnaryOperator$Neg : TsUnaryOperator + UndocumentedPublicClass:TsUnaryOperator.kt$TsUnaryOperator$Not : TsUnaryOperator + UndocumentedPublicClass:UnreachableCodeDetector.kt$UncoveredIfSuccessors + UndocumentedPublicClass:UnreachableCodeDetector.kt$UnreachableCodeDetector : TsInterpreterObserverUMachineObserver + UnreachableCode:FakeExprUtil.kt$memory.read(lValue) to typeCondition + UnsafeCallOnNullableType:CallStatic.kt$it.enclosingClass!! + UnsafeCallOnNullableType:CallStatic.kt$resolved.property.enclosingClass!! + UnsafeCallOnNullableType:TsExprResolver.kt$TsSimpleValueResolver$currentMethod.enclosingClass!! + UnsafeCallOnNullableType:TsExprResolver.kt$TsSimpleValueResolver$currentMethod.enclosingClass!!.declaringFile!! + UnsafeCallOnNullableType:TsInterpreter.kt$TsInterpreter$lastEnteredMethod.enclosingClass!! + UnsafeCallOnNullableType:TsInterpreter.kt$TsInterpreter$lastEnteredMethod.enclosingClass!!.declaringFile!! + UnsafeCallOnNullableType:TsInterpreter.kt$TsInterpreter$method.enclosingClass!! + UnsafeCallOnNullableType:WriteLocal.kt$currentMethod.enclosingClass!! + UnsafeCallOnNullableType:WriteLocal.kt$currentMethod.enclosingClass!!.declaringFile!! + UnusedParameter:CallApproximations.kt$arrayType: EtsArrayType + UnusedParameter:CallApproximations.kt$elementSort: USort + UnusedParameter:TsStatic.kt$clazz: EtsClassSignature + UnusedPrivateProperty:CallApproximations.kt$val searchElement = resolve(expr.args.single()) ?: return null + UnusedPrivateProperty:TsExprResolver.kt$TsExprResolver$val property = resolve(expr.left) ?: return null + UseOrEmpty:EtsHierarchy.kt$EtsHierarchy$suitableClasses[signature]?.let { setOf(it) } ?: emptySet() + UseOrEmpty:TsTypeSystem.kt$fields.reduceOrNull { acc, set -> acc.intersect(set) } ?: emptySet() + UseOrEmpty:TsTypeSystem.kt$methods.reduceOrNull { acc, set -> acc.intersect(set) } ?: emptySet() + UtilityClassWithPublicConstructor:TsContext.kt$Constants + + diff --git a/detekt/baselines/usvm-ts-Test.yml b/detekt/baselines/usvm-ts-Test.yml new file mode 100644 index 0000000000..6553b38732 --- /dev/null +++ b/detekt/baselines/usvm-ts-Test.yml @@ -0,0 +1,118 @@ + + + + + ArgumentListWrapping:TsMethodTestRunner.kt$TsMethodTestRunner$( typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class) ) + BlockCommentInitialStarAlignment:TsMethodTestRunner.kt$TsMethodTestRunner$/* Both KClass and TsObject instances come here because only KClass<TsObject> is available to match different objects. However, this method is also used in parent TestRunner class and passes here TsObject instances. So this check on current level is required. */ + BracesOnWhenStatements:TsMethodTestRunner.kt$TsMethodTestRunner$when + BracesOnWhenStatements:TsTestResolver.kt$TsTestStateResolver$when + CascadingCallWrapping:CallFallbackBaselineTest.kt$CallFallbackBaselineTest$single { it.name == methodName } + CascadingCallWrapping:CallFallbackBaselineTest.kt$CallFallbackBaselineTest$stmts + CascadingCallWrapping:InheritanceReachabilityTest.kt$InheritanceReachabilityTest$filter { it.name == "process" } + CascadingCallWrapping:TsMethodTestRunner.kt$TsMethodTestRunner$filter { it.name == methodName } + CascadingCallWrapping:TsMethodTestRunner.kt$TsMethodTestRunner$single { it.name == className } + ChainWrapping:Add.kt$Add$&& + ChainWrapping:Add.kt$Add$|| + ChainWrapping:ArrayMethods.kt$ArrayMethods$&& + CommentSpacing:LoadEts.kt$//----------------------------------------------------------------------------- + Filename:DemoCalc.kt$org.usvm.project.DemoCalc.kt + Filename:DemoPhotos.kt$org.usvm.project.DemoPhotos.kt + Filename:ImportExportResolution.kt$org.usvm.machine.ImportExportResolution.kt + Filename:ImportResolver.kt$org.usvm.project.ImportResolver.kt + Filename:UnreachableCodeDetector.kt$org.usvm.checkers.UnreachableCodeDetector.kt + ForbiddenMethodCall:DemoCalc.kt$RunOnDemoCalcProject$println("${es.first()}") + ForbiddenMethodCall:DemoCalc.kt$RunOnDemoCalcProject$println("Total classes: ${classes.size}") + ForbiddenMethodCall:DemoCalc.kt$RunOnDemoCalcProject$println("Total exceptions: ${exc.size}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " Available exports: ${ exportNames.joinToString(", ") }${ if (availableExports.size > 5) " ..." else "" }" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " ✅ '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + " (type: ${importInfo.type})" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " ❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + " (type: ${importInfo.type})" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " 🎯 '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + " exports: ${getExportDescription(exportInfo)} (import type: ${importInfo.type})" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " 📁❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + " (import type: ${importInfo.type})" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println( " 🔍❌ '${importInfo.name}' from '${importInfo.from}' -> ${result.reason}" + " (import type: ${importInfo.type})" ) + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println(" $status '$input' -> '$result' (expected: '$expected')") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println(" ✓ '$importPath' resolved to '${result.file.signature.fileName}'") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println(" ✗ '$importPath' failed: ${result.reason}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Complete symbol resolution success rate: $symbolSuccessRate%") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Failed to resolve files: $failedImports") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("File not found: $fileNotFoundSymbols") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("File resolution success rate: $successRate%") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Loading SDK from path: $sdkPath") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Loading SDK from resource: $it") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Loading project from path: $projectPath") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Loading project from resources: $path") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Merging project and SDK files...") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Project files by extension: ${projectFilesByExtension.mapValues { it.value.size }}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Project files: ${scene.projectFiles.size}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Project loaded: ${projectScene.projectName} with ${projectScene.projectFiles.size} files") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("SDK files by extension: ${sdkFilesByExtension.mapValues { it.value.size }}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("SDK files: ${scene.sdkFiles.size}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("SDK loaded: ${sdkScene.projectName} with ${sdkScene.projectFiles.size} files") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Scene loaded with ${scene.projectFiles.size} project files and ${scene.sdkFiles.size} SDK files") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Successfully resolved files: $successfulImports") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Successfully resolved symbols: $successfulSymbols") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Symbol not found in file: $symbolNotFoundSymbols") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Total files: ${scene.projectAndSdkClasses.size}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Total imports found: $totalImports") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Total imports in project files: ${scene.projectFiles.sumOf { it.importInfos.size }}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Total symbols to resolve: $totalSymbols") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("Using test file: ${testFile.signature.fileName}") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n$category:") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Complete Symbol Resolution Summary ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- File Import Resolution Summary ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Setting up scene for import resolution tests ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Summary ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Testing common import patterns ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Testing complete symbol resolver ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n--- Testing file-level import resolver ---") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\nPath Normalization Tests:") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n[${index + 1}/${allFiles.size}] File: $fileName (${imports.size} imports)") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n[${index + 1}/${allFiles.size}] File: $fileName (no imports)") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n[${index + 1}/${allFiles.size}] File: '$fileName' (${imports.size} imports)") + ForbiddenMethodCall:ImportResolver.kt$ImportResolverTest$println("\n[${index + 1}/${allFiles.size}] File: '$fileName' (no imports)") + FunctionOnlyReturningConstant:Truthy.kt$fun isTruthy(x: TsTestValue.TsClass): Boolean + ImportOrdering:StaticOverloads.kt$import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test import org.usvm.api.TsTestValue import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.state.TsState import org.usvm.statistics.UMachineObserver import org.usvm.test.util.checkers.eq as exactly import org.usvm.util.TsMethodTestRunner import org.usvm.util.eq import kotlin.test.assertEquals + LongMethod:Division.kt$Division$@Test fun `test number div number`() + MatchingDeclarationName:ImportExportResolution.kt$ImportExportResolutionTest + MatchingDeclarationName:UnreachableCodeDetector.kt$UnreachableCodeDetectorTest + MaxLineLength:Division.kt$Division$(a.number == Double.NEGATIVE_INFINITY) && b.number.isFinite() && (b.number < 0) && (r.number == Double.POSITIVE_INFINITY) + MaxLineLength:Division.kt$Division$(a.number == Double.NEGATIVE_INFINITY) && b.number.isFinite() && (b.number > 0) && (r.number == Double.NEGATIVE_INFINITY) + MaxLineLength:Division.kt$Division$(a.number == Double.POSITIVE_INFINITY) && b.number.isFinite() && (b.number < 0) && (r.number == Double.NEGATIVE_INFINITY) + MaxLineLength:Division.kt$Division$(a.number == Double.POSITIVE_INFINITY) && b.number.isFinite() && (b.number > 0) && (r.number == Double.POSITIVE_INFINITY) + MaxLineLength:Division.kt$Division$a.number.isFinite() && (a.number < 0) && b.number.isFinite() && (b.number < 0) && (r.number == a.number / b.number) + MaxLineLength:Division.kt$Division$a.number.isFinite() && (a.number < 0) && b.number.isFinite() && (b.number < 0) && (r.number >= 0) && (r.number == a.number / b.number) + MaxLineLength:Division.kt$Division$a.number.isFinite() && (a.number < 0) && b.number.isFinite() && (b.number > 0) && (r.number <= 0) && (r.number == a.number / b.number) + MaxLineLength:Division.kt$Division$a.number.isFinite() && (a.number > 0) && b.number.isFinite() && (b.number > 0) && (r.number == a.number / b.number) + MaxLineLength:ImportResolver.kt$ImportResolverTest$" ✅ '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + MaxLineLength:ImportResolver.kt$ImportResolverTest$" 🎯 '${importInfo.name}' from '${importInfo.from}' -> '${result.file.signature.fileName}'" + MaxLineLength:ImportResolver.kt$ImportResolverTest$"All path normalization tests should pass (expected: ${normalizationTests.size}, actual: $correctNormalizations)" + MaxLineLength:InheritanceReachabilityTest.kt$InheritanceReachabilityTest$// const obj = new ConcreteA(value) -> const specificResult = obj.specificMethodA() -> if (specificResult === 1) -> return 1 + MaxLineLength:InstanceMethods.kt$InstanceMethods$discoverProperties + MaxLineLength:RecursionReachabilityTest.kt$RecursionReachabilityTest$// if (input > 0 && input < 5) -> const evenResult = this.isEven(input) -> if (evenResult && input === 4) -> return 1 + MaxLineLength:StaticMethods.kt$StaticMethods$discoverProperties + MaxLineLength:TsMethodTestRunner.kt$TsMethodTestRunner$protected inline + MaxLineLength:TypeGuardsReachabilityTest.kt$TypeGuardsReachabilityTest$// if (typeof value === "object" && value !== null) -> if (value instanceof Date) -> if (value.getFullYear() > 2020) -> return 1 + MaximumLineLength:Division.kt$Division$ + MaximumLineLength:ImportResolver.kt$ImportResolverTest$ + MaximumLineLength:InstanceMethods.kt$InstanceMethods$ + MaximumLineLength:StaticMethods.kt$StaticMethods$ + MaximumLineLength:TsMethodTestRunner.kt$TsMethodTestRunner$ + MultiLineIfElse:TypeStream.kt$TypeStream$true + NestedBlockDepth:TsTestResolver.kt$TsTestStateResolver$private fun resolvePrimitive( expr: UExpr<out USort>, type: EtsPrimitiveType, ): TsTestValue + NoBlankLineInList:ImportExportResolution.kt$ImportExportResolutionTest$ + NoEmptyFirstLineInMethodBlock:And.kt$And$ + NoEmptyFirstLineInMethodBlock:NullishCoalescing.kt$NullishCoalescing$ + NoEmptyFirstLineInMethodBlock:Truthy.kt$Truthy$ + NoNameShadowing:NullishCoalescing.kt$NullishCoalescing$a + NoTrailingSpaces:LoopsReachabilityTest.kt$LoopsReachabilityTest$ + NoUnusedImports:ArrayReachabilityTest.kt$org.usvm.reachability.ArrayReachabilityTest.kt + NoUnusedImports:DemoPhotos.kt$org.usvm.project.DemoPhotos.kt + UnderscoresInNumericLiterals:Bitwise.kt$Bitwise$2147483647 + UnderscoresInNumericLiterals:ReachabilityChecker.kt$ReachabilityChecker$15000000 + UnderscoresInNumericLiterals:TsMethodTestRunner.kt$TsMethodTestRunner$1000000000 + UnusedParameter:Truthy.kt$x: TsTestValue.TsClass + UseCheckNotNull:UnreachableCodeDetector.kt$UnreachableCodeDetectorTest$check(uncoveredStatements != null) { "Uncovered statements are incorrect, results are $uncoveredStatements" } + VarCouldBeVal:HigherOrderFunctionsReachabilityTest.kt$HigherOrderFunctionsReachabilityTest$var target: TsTarget = initialTarget + Wrapping:Add.kt$Add$( + Wrapping:ImportResolver.kt$ImportResolverTest$( + + diff --git a/detekt/ts-config.yml b/detekt/ts-config.yml new file mode 100644 index 0000000000..003c5075c3 --- /dev/null +++ b/detekt/ts-config.yml @@ -0,0 +1,15 @@ +comments: + UndocumentedPublicClass: + active: true + searchInNestedClass: false + excludes: + - '**/test/**' + +complexity: + ComplexCondition: + active: true + threshold: 4 + +style: + CascadingCallWrapping: + active: true diff --git a/usvm-ts-pbt/README.md b/usvm-ts-pbt/README.md index 2194743127..174b207336 100644 --- a/usvm-ts-pbt/README.md +++ b/usvm-ts-pbt/README.md @@ -1,27 +1,129 @@ # USVM TypeScript property-based testing -`usvm-ts-pbt` is the integration baseline for the fast-check and symbolic-execution pipeline tracked by -[issue #346](https://github.com/UnitTestBot/usvm/issues/346). Property execution is introduced by later issues. +`usvm-ts-pbt` is the Kotlin-owned integration layer for concrete property-based testing backends and USVM. +Kotlin defines each property once; fast-check is the first replaceable concrete backend. -## Design +## Architecture -- TypeScript is parsed by the repository's default JacoDB native `ts-frontend`; ArkAnalyzer is not required. -- The module follows the repository-wide JacoDB dependency without a separate version pin. -- The smoke test loads a TypeScript method into EtsIR and verifies its CFG and `EtsSourceSpan` origins. +```text +Kotlin PropertyDefinition + | + +--> versioned PropertyManifest + | + +--> PBT projection ----------> private fast-check Node adapter + | + +--> symbolic projection -----> USVM (#351) +``` -## Run +Kotlin owns property identity, ordered inputs, domain semantics, TypeScript entry-point references, validation, +capability aggregation, and later orchestration. Common Kotlin code never contains `fc.Arbitrary` or another +backend-native generator type. -Requires JDK 11, Node.js 18.18 or newer, and the repository's Gradle wrapper. +Predicate and precondition bodies remain exported TypeScript functions. Kotlin refers to each function by a +normalized project-relative module path, export name, and synchronous or asynchronous execution kind. Issue #347 +validates and serializes those references but does not load or execute the functions. -```shell -env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ - ./gradlew --no-daemon :usvm-ts-pbt:clean :usvm-ts-pbt:check +## Kotlin property model + +```kotlin +val property = PropertyDefinition( + id = PropertyId("array.reverse-twice"), + inputs = listOf( + PropertyInput( + name = "values", + domain = ArrayDomain(IntegerDomain(-100, 100), minLength = 0, maxLength = 20), + ), + ), + predicate = TypeScriptEntryPoint( + module = "properties/arrays.ts", + exportName = "reverseTwicePreservesValues", + ), +) + +val manifest = property.toManifest() ``` -To substitute a local JacoDB checkout: +Input order is significant because TypeScript parameters are positional. Names are unique and are retained in +diagnostics and artifacts. + +| Domain | Semantics and defaults | +| ---------------- | -------------------------------------------------------------------------------------------------- | +| `BooleanDomain` | JavaScript booleans | +| `IntegerDomain` | Inclusive signed 32-bit range; defaults to `Int.MIN_VALUE..Int.MAX_VALUE` | +| `NumberDomain` | ECMAScript binary64; defaults to both infinities and `allowNaN = true`; bounded domains reject NaN | +| `StringDomain` | Arbitrary UTF-16 code units; length is JavaScript `String.length`; defaults to `0..10` | +| `ConstantDomain` | One tagged JavaScript primitive | +| `OptionalDomain` | Nested domain plus exactly `undefined` or `null` as the nil value | +| `TupleDomain` | Non-empty ordered recursive domains | +| `ArrayDomain` | Recursive element domain; defaults to length `0..10` | + +`PropertyDomain` describes a set of allowed inputs. `JsConcreteValue` describes one concrete JavaScript value used as a +constant or returned sample; it is unrelated to JacoDB IR values. Its tagged encoding preserves `undefined`, +`null`, NaN, both infinities, and the raw IEEE-754 bits of finite numbers, including negative zero. Protocol +samples also use recursive tagged arrays so tuple and array values cross JSON without losing nested special +values. `ConstantDomain` still rejects composite values. + +## Manifest and capability are separate + +`PropertyManifest` is schema-versioned engine-neutral data. It contains property semantics and TypeScript +entry-point references, but no backend name, fast-check configuration, seed, replay path, shrink data, coverage, +or USVM expression. + +`ProjectionCapability` is a backend-and-version-specific report with `EXACT`, `APPROXIMATE`, or `UNSUPPORTED` +level and stable diagnostics. Recursive composition selects the least capable child. A concrete projection that +is supported while the selected USVM projection is unsupported is classified by the pipeline as `CONCRETE_ONLY`; +that classification is not stored in the manifest. + +## Private fast-check adapter + +`fast-check-adapter` is a private TypeScript module pinned to fast-check 4.9.0. Gradle compiles it with `tsc` into +an ignored `dist` directory before Kotlin integration tests run. The adapter recursively reconstructs real +`fc.Arbitrary` objects from common domain descriptors. Kotlin invokes the compiled one-shot `sample` operation +over one JSON request on stdin and one JSON response on stdout. The adapter does not discover properties, load +predicates, run campaigns, select USVM, or orchestrate the pipeline. + +Both manifest and protocol versions start at `1`. Kotlin validates outgoing request sizes and verifies process +exit status, JSON shape, protocol version, request identity, sample shape, and typed backend diagnostics. + +## Extension rules + +- A new PBT backend consumes the common manifest and implements projection/capability reporting. Existing + `PropertyDefinition` instances and USVM code must not change for already-supported domains. +- A new common domain needs explicit Kotlin semantics and validation, serialization, a capability decision from + every backend, and conformance tests. +- A backend-specific extension must be namespaced and must be reported as unsupported by backends that do not + implement it. +- Backend-native arbitrary objects, arbitrary TypeScript closures, silent approximation, and backend defaults in + the common model are rejected extension mechanisms. + +## Verification + +Requires JDK 11, Node.js 18.18 or newer, npm, and the repository Gradle wrapper. The full Gradle check installs and +compiles the pinned private adapter, runs its compiled Node tests, runs Kotlin/Node protocol tests, and retains the +native `ts-frontend` baseline from #346. ```shell +npm ci --prefix usvm-ts-pbt/fast-check-adapter --ignore-scripts +npm run build --prefix usvm-ts-pbt/fast-check-adapter +npm test --prefix usvm-ts-pbt/fast-check-adapter + env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ - ./gradlew --no-daemon -PuseLocalJacodb=/absolute/path/to/jacodb \ - :usvm-ts-pbt:clean :usvm-ts-pbt:check + ./gradlew --no-daemon :usvm-ts-pbt:test + +env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend \ + ./gradlew --no-daemon :usvm-ts-pbt:clean :usvm-ts-pbt:check ``` + +To substitute a local JacoDB checkout, add +`-PuseLocalJacodb=/absolute/path/to/jacodb` to the Gradle command. + +## Issue boundaries + +- #348 loads TypeScript entry points and executes Kotlin definitions through `fc.check`. +- #349 records backend-neutral per-property coverage. +- #350 maps entry points and coverage locations to EtsIR. +- #351 projects common domains and preconditions into USVM. +- #352 searches for property violations with USVM. +- #353 replays USVM witnesses and delegates shrinking to a capable PBT backend. +- #354 assembles the Kotlin-orchestrated end-to-end pipeline. +- #355–#357 build runtime hints, benchmarks, and evaluation on backend-identified artifacts. diff --git a/usvm-ts-pbt/build.gradle.kts b/usvm-ts-pbt/build.gradle.kts index 4393ff574c..56503aa6b4 100644 --- a/usvm-ts-pbt/build.gradle.kts +++ b/usvm-ts-pbt/build.gradle.kts @@ -1,10 +1,58 @@ plugins { id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin } dependencies { implementation(project(":usvm-ts")) implementation(Libs.jacodb_ets) + implementation(Libs.kotlinx_serialization_json) testImplementation(Libs.logback) } + +val fastCheckAdapterDir = layout.projectDirectory.dir("fast-check-adapter") +val npmExecutable = if (System.getProperty("os.name").lowercase().contains("windows")) "npm.cmd" else "npm" + +val installFastCheckAdapter = tasks.register("installFastCheckAdapter") { + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "ci", "--ignore-scripts") + inputs.files( + fastCheckAdapterDir.file("package.json"), + fastCheckAdapterDir.file("package-lock.json"), + ) + outputs.dir(fastCheckAdapterDir.dir("node_modules")) +} + +val buildFastCheckAdapter = tasks.register("buildFastCheckAdapter") { + dependsOn(installFastCheckAdapter) + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "run", "build") + inputs.files( + fastCheckAdapterDir.file("package.json"), + fastCheckAdapterDir.file("package-lock.json"), + fastCheckAdapterDir.file("tsconfig.json"), + ) + inputs.dir(fastCheckAdapterDir.dir("src")) + inputs.dir(fastCheckAdapterDir.dir("test")) + outputs.dir(fastCheckAdapterDir.dir("dist")) +} + +val testFastCheckAdapter = tasks.register("testFastCheckAdapter") { + dependsOn(buildFastCheckAdapter) + workingDir(fastCheckAdapterDir) + commandLine(npmExecutable, "run", "test:compiled") + inputs.dir(fastCheckAdapterDir.dir("dist")) +} + +tasks.test { + dependsOn(buildFastCheckAdapter) +} + +tasks.check { + dependsOn(testFastCheckAdapter) +} + +tasks.clean { + delete(fastCheckAdapterDir.dir("dist")) +} diff --git a/usvm-ts-pbt/fast-check-adapter/.gitignore b/usvm-ts-pbt/fast-check-adapter/.gitignore new file mode 100644 index 0000000000..b947077876 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/.gitignore @@ -0,0 +1,2 @@ +node_modules/ +dist/ diff --git a/usvm-ts-pbt/fast-check-adapter/package-lock.json b/usvm-ts-pbt/fast-check-adapter/package-lock.json new file mode 100644 index 0000000000..c1e53b916d --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/package-lock.json @@ -0,0 +1,91 @@ +{ + "name": "@usvm/fast-check-adapter", + "version": "0.1.0", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "@usvm/fast-check-adapter", + "version": "0.1.0", + "dependencies": { + "fast-check": "4.9.0" + }, + "devDependencies": { + "@types/node": "18.19.130", + "typescript": "5.9.2" + }, + "engines": { + "node": ">=18.18.0" + } + }, + "node_modules/@types/node": { + "version": "18.19.130", + "resolved": "https://registry.npmjs.org/@types/node/-/node-18.19.130.tgz", + "integrity": "sha512-GRaXQx6jGfL8sKfaIDD6OupbIHBr9jv7Jnaml9tB7l4v068PAOXqfcujMMo5PhbIs6ggR1XODELqahT2R8v0fg==", + "dev": true, + "license": "MIT", + "dependencies": { + "undici-types": "~5.26.4" + } + }, + "node_modules/fast-check": { + "version": "4.9.0", + "resolved": "https://registry.npmjs.org/fast-check/-/fast-check-4.9.0.tgz", + "integrity": "sha512-7ms6T7SybUev/PQITciI0yLM2pOSFy5zpG8Ty7tQofcVaQUvrMXp6CBwqF6fThLCLOrfBtuHAtwq6Yu4XPCllg==", + "funding": [ + { + "type": "individual", + "url": "https://github.com/sponsors/dubzzz" + }, + { + "type": "opencollective", + "url": "https://opencollective.com/fast-check" + } + ], + "license": "MIT", + "dependencies": { + "pure-rand": "^8.0.0" + }, + "engines": { + "node": ">=12.17.0" + } + }, + "node_modules/pure-rand": { + "version": "8.4.2", + "resolved": "https://registry.npmjs.org/pure-rand/-/pure-rand-8.4.2.tgz", + "integrity": "sha512-vvuOGgcuPJAirlHvuQw1TrOiw7ptaIXXmIbNuiNOY6lNGJJH49PQ1Kj4nd783nPdQhQdicgOjVI2yI/9BD6/Ng==", + "funding": [ + { + "type": "individual", + "url": "https://github.com/sponsors/dubzzz" + }, + { + "type": "opencollective", + "url": "https://opencollective.com/fast-check" + } + ], + "license": "MIT" + }, + "node_modules/typescript": { + "version": "5.9.2", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.2.tgz", + "integrity": "sha512-CWBzXQrc/qOkhidw1OzBTQuYRbfyxDXJMVJ1XNwUHGROVmuaeiEm3OslpZ1RV96d7SKKjZKrSJu3+t/xlw3R9A==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/undici-types": { + "version": "5.26.5", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-5.26.5.tgz", + "integrity": "sha512-JlCMO+ehdEIKqlFxk6IfVoAUVmgz7cU7zD/h9XZ0qzeosSHmUJVOzSQvvYSYWXkFXC+IfLKSIffhv0sVZup6pA==", + "dev": true, + "license": "MIT" + } + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/package.json b/usvm-ts-pbt/fast-check-adapter/package.json new file mode 100644 index 0000000000..96a9d74f78 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/package.json @@ -0,0 +1,24 @@ +{ + "name": "@usvm/fast-check-adapter", + "version": "0.1.0", + "private": true, + "type": "module", + "scripts": { + "clean": "node --input-type=module --eval \"import { rmSync } from 'node:fs'; rmSync('dist', { recursive: true, force: true })\"", + "prebuild": "npm run clean", + "build": "tsc --project tsconfig.json", + "pretest": "npm run build", + "test": "npm run test:compiled", + "test:compiled": "node --test dist/test/js-value.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js" + }, + "dependencies": { + "fast-check": "4.9.0" + }, + "devDependencies": { + "@types/node": "18.19.130", + "typescript": "5.9.2" + }, + "engines": { + "node": ">=18.18.0" + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/src/js-value.ts b/usvm-ts-pbt/fast-check-adapter/src/js-value.ts new file mode 100644 index 0000000000..781ad8ae6b --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/js-value.ts @@ -0,0 +1,152 @@ +export type JsConcreteValue = + | undefined + | null + | boolean + | string + | number + | JsConcreteValue[]; + +export type TaggedJsNumber = + | { value: 'finite'; bits: string } + | { value: 'nan' } + | { value: 'positive-infinity' } + | { value: 'negative-infinity' }; + +export type TaggedJsValue = + | { kind: 'undefined' } + | { kind: 'null' } + | { kind: 'boolean'; value: boolean } + | { kind: 'string'; value: string } + | ({ kind: 'number' } & TaggedJsNumber) + | { kind: 'array'; elements: TaggedJsValue[] }; + +export class ProtocolError extends Error { + constructor( + readonly code: string, + readonly diagnosticMessage: string, + readonly path: string, + ) { + super(`${code}: ${diagnosticMessage}`); + this.name = 'ProtocolError'; + } +} + +export function decodeJsValue(value: unknown, path = 'value'): JsConcreteValue { + requireObject(value, 'js-value.invalid', 'Tagged JavaScript value must be an object', path); + switch (value.kind) { + case 'undefined': + return undefined; + case 'null': + return null; + case 'boolean': + if (typeof value.value !== 'boolean') { + throw protocolError('js-value.boolean.invalid', 'Boolean value must contain a boolean', path); + } + return value.value; + case 'string': + if (typeof value.value !== 'string') { + throw protocolError('js-value.string.invalid', 'String value must contain a string', path); + } + return value.value; + case 'number': + return decodeJsNumber(value, path); + case 'array': + if (!Array.isArray(value.elements)) { + throw protocolError('js-value.array.invalid', 'Array value must contain elements', path); + } + return value.elements.map((element: unknown, index: number) => + decodeJsValue(element, `${path}.elements[${index}]`)); + default: + throw protocolError( + 'js-value.kind.unknown', + `Unknown JavaScript value kind: ${String(value.kind)}`, + path, + ); + } +} + +export function encodeJsValue(value: unknown): TaggedJsValue { + if (value === undefined) return { kind: 'undefined' }; + if (value === null) return { kind: 'null' }; + if (typeof value === 'boolean') return { kind: 'boolean', value }; + if (typeof value === 'string') return { kind: 'string', value }; + if (typeof value === 'number') return { kind: 'number', ...encodeJsNumber(value) }; + if (Array.isArray(value)) return { kind: 'array', elements: value.map(encodeJsValue) }; + throw protocolError( + 'js-value.type.unsupported', + `Unsupported JavaScript value type: ${typeof value}`, + 'value', + ); +} + +export function decodeJsNumber(taggedNumber: unknown, path = 'number'): number { + requireObject(taggedNumber, 'js-number.invalid', 'Tagged JavaScript number must be an object', path); + switch (taggedNumber.value) { + case 'finite': + if (typeof taggedNumber.bits !== 'string' || !/^[0-9a-f]{16}$/.test(taggedNumber.bits)) { + throw protocolError( + 'js-number.encoding.invalid', + 'Finite JavaScript numbers require sixteen lowercase hexadecimal digits', + path, + ); + } + return bitsToDouble(taggedNumber.bits); + case 'nan': + requireNoBits(taggedNumber, path); + return Number.NaN; + case 'positive-infinity': + requireNoBits(taggedNumber, path); + return Number.POSITIVE_INFINITY; + case 'negative-infinity': + requireNoBits(taggedNumber, path); + return Number.NEGATIVE_INFINITY; + default: + throw protocolError( + 'js-number.kind.unknown', + `Unknown JavaScript number kind: ${String(taggedNumber.value)}`, + path, + ); + } +} + +export function encodeJsNumber(value: number): TaggedJsNumber { + if (Number.isNaN(value)) return { value: 'nan' }; + if (value === Number.POSITIVE_INFINITY) return { value: 'positive-infinity' }; + if (value === Number.NEGATIVE_INFINITY) return { value: 'negative-infinity' }; + return { value: 'finite', bits: doubleToBits(value) }; +} + +export function protocolError(code: string, message: string, path: string): ProtocolError { + return new ProtocolError(code, message, path); +} + +function bitsToDouble(bits: string): number { + const buffer = new ArrayBuffer(8); + const view = new DataView(buffer); + view.setBigUint64(0, BigInt(`0x${bits}`), false); + return view.getFloat64(0, false); +} + +function doubleToBits(value: number): string { + const buffer = new ArrayBuffer(8); + const view = new DataView(buffer); + view.setFloat64(0, value, false); + return view.getBigUint64(0, false).toString(16).padStart(16, '0'); +} + +function requireNoBits(taggedNumber: Record, path: string): void { + if (taggedNumber.bits !== undefined) { + throw protocolError('js-number.encoding.invalid', 'Non-finite JavaScript numbers must not contain bits', path); + } +} + +function requireObject( + value: unknown, + code: string, + message: string, + path: string, +): asserts value is Record { + if (value === null || typeof value !== 'object' || Array.isArray(value)) { + throw protocolError(code, message, path); + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts new file mode 100644 index 0000000000..954ab21f1c --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/project-domain.ts @@ -0,0 +1,173 @@ +import fc from 'fast-check'; +import { + decodeJsNumber, + decodeJsValue, + ProtocolError, + protocolError, +} from './js-value.js'; + +export const FAST_CHECK_BACKEND_ID = 'fast-check'; +export const FAST_CHECK_BACKEND_VERSION = '4.9.0'; + +export interface ProjectionDiagnostic { + code: string; + message: string; + path: string; +} + +export interface ProjectionCapability { + backendId: string; + backendVersion: string; + level: 'exact' | 'unsupported'; + diagnostics: ProjectionDiagnostic[]; +} + +type DomainRecord = Record; + +export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary { + requireDomainObject(domain, path); + switch (domain.kind) { + case 'boolean': + return fc.boolean(); + case 'integer': + validateIntegerDomain(domain, path); + return fc.integer({ min: domain.min, max: domain.max }); + case 'number': + return projectNumber(domain, path); + case 'string': + validateLengths(domain, path); + return fc.array(fc.integer({ min: 0, max: 0xffff }), { + minLength: domain.minLength, + maxLength: domain.maxLength, + }).map((units) => units.map((unit) => String.fromCharCode(unit)).join('')); + case 'constant': + return fc.constant(decodeJsValue(domain.value, `${path}.value`)); + case 'optional': { + const nil = decodeJsValue(domain.nil, `${path}.nil`); + if (nil !== undefined && nil !== null) { + throw protocolError('domain.optional.nil', 'Optional nil must be null or undefined', `${path}.nil`); + } + return fc.option(projectDomain(domain.value, `${path}.value`), { nil }); + } + case 'tuple': + if (!Array.isArray(domain.elements) || domain.elements.length === 0) { + throw protocolError('domain.tuple.empty', 'Tuple domain must contain elements', path); + } + return fc.tuple(...domain.elements.map( + (element: unknown, index: number) => projectDomain(element, `${path}.elements[${index}]`), + )); + case 'array': + validateLengths(domain, path); + return fc.array(projectDomain(domain.element, `${path}.element`), { + minLength: domain.minLength, + maxLength: domain.maxLength, + }); + default: + throw protocolError( + 'domain.kind.unknown', + `Unknown property domain kind: ${String(domain.kind)}`, + path, + ); + } +} + +export function projectionCapability(domain: unknown, path = 'domain'): ProjectionCapability { + try { + projectDomain(domain, path); + return { + backendId: FAST_CHECK_BACKEND_ID, + backendVersion: FAST_CHECK_BACKEND_VERSION, + level: 'exact', + diagnostics: [], + }; + } catch (error: unknown) { + if (!(error instanceof ProtocolError)) throw error; + return { + backendId: FAST_CHECK_BACKEND_ID, + backendVersion: FAST_CHECK_BACKEND_VERSION, + level: 'unsupported', + diagnostics: [{ + code: error.code, + message: error.diagnosticMessage, + path: error.path, + }], + }; + } +} + +function projectNumber(domain: DomainRecord, path: string): fc.Arbitrary { + if (typeof domain.allowNaN !== 'boolean') { + throw protocolError('domain.number.allow-nan.invalid', 'allowNaN must be a boolean', `${path}.allowNaN`); + } + const min = decodeJsNumber(domain.min, `${path}.min`); + const max = decodeJsNumber(domain.max, `${path}.max`); + if (Number.isNaN(min) || Number.isNaN(max)) { + throw protocolError('domain.number.bound.nan', 'Number bounds must not be NaN', path); + } + if (min > max) { + throw protocolError('domain.number.bounds', 'Number minimum exceeds maximum', path); + } + const bounded = min !== Number.NEGATIVE_INFINITY || max !== Number.POSITIVE_INFINITY; + if (bounded && domain.allowNaN) { + throw protocolError('domain.number.nan-bounded', 'Bounded number domains must exclude NaN', `${path}.allowNaN`); + } + + const finiteMin = min === Number.NEGATIVE_INFINITY ? -Number.MAX_VALUE : min; + const finiteMax = max === Number.POSITIVE_INFINITY ? Number.MAX_VALUE : max; + const arbitraries: fc.Arbitrary[] = []; + if (finiteMin <= finiteMax) { + arbitraries.push(fc.double({ + min: finiteMin, + max: finiteMax, + noNaN: true, + noDefaultInfinity: true, + })); + } + if (domain.allowNaN) arbitraries.push(fc.constant(Number.NaN)); + if (min === Number.NEGATIVE_INFINITY) arbitraries.push(fc.constant(Number.NEGATIVE_INFINITY)); + if (max === Number.POSITIVE_INFINITY) arbitraries.push(fc.constant(Number.POSITIVE_INFINITY)); + if (min <= 0 && max >= 0) arbitraries.push(fc.constant(-0)); + + const [first, ...rest] = arbitraries; + if (first === undefined) { + throw protocolError('domain.number.empty', 'Number domain does not contain any values', path); + } + return rest.length === 0 ? first : fc.oneof(first, ...rest); +} + +function validateIntegerDomain( + domain: DomainRecord, + path: string, +): asserts domain is DomainRecord & { min: number; max: number } { + const valid = typeof domain.min === 'number' + && typeof domain.max === 'number' + && Number.isInteger(domain.min) + && Number.isInteger(domain.max) + && domain.min >= -0x80000000 + && domain.max <= 0x7fffffff + && domain.min <= domain.max; + if (!valid) { + throw protocolError('domain.integer.bounds', 'Integer bounds must be an inclusive signed 32-bit range', path); + } +} + +function validateLengths( + domain: DomainRecord, + path: string, +): asserts domain is DomainRecord & { minLength: number; maxLength: number } { + const valid = typeof domain.minLength === 'number' + && typeof domain.maxLength === 'number' + && Number.isInteger(domain.minLength) + && Number.isInteger(domain.maxLength) + && domain.minLength >= 0 + && domain.minLength <= domain.maxLength; + if (!valid) { + throw protocolError('domain.length.invalid', 'Domain length bounds are invalid', path); + } +} + +function requireDomainObject(domain: unknown, path: string): asserts domain is DomainRecord { + if (domain === null || typeof domain !== 'object' || Array.isArray(domain)) { + throw protocolError('domain.invalid', 'Property domain must be an object', path); + } +} diff --git a/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts b/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts new file mode 100644 index 0000000000..06e8af735b --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/src/projection-cli.ts @@ -0,0 +1,143 @@ +import fc from 'fast-check'; +import { + encodeJsValue, + ProtocolError, + protocolError, +} from './js-value.js'; +import type { TaggedJsValue } from './js-value.js'; +import { projectDomain } from './project-domain.js'; + +const PROTOCOL_VERSION = 1; + +interface FastCheckProjectionRequest { + protocolVersion: 1; + requestId: string; + operation: 'sample'; + seed: number; + numSamples: number; + domains: unknown[]; +} + +interface FastCheckProjectionSuccess { + protocolVersion: 1; + requestId: string; + status: 'ok'; + samples: TaggedJsValue[][]; +} + +interface FastCheckProjectionFailure { + protocolVersion: 1; + requestId?: string; + status: 'error'; + diagnostics: Array<{ + code: string; + message: string; + path: string; + }>; +} + +type FastCheckProjectionWireResponse = FastCheckProjectionSuccess | FastCheckProjectionFailure; + +let parsedRequest: unknown = undefined; +let response: FastCheckProjectionWireResponse; +try { + const input = await readStdin(); + try { + parsedRequest = JSON.parse(input) as unknown; + } catch { + throw protocolError('protocol.json.invalid', 'Standard input is not valid JSON', 'request'); + } + const request = validateRequest(parsedRequest); + const arbitrary = fc.tuple( + ...request.domains.map((domain, index) => projectDomain(domain, `domains[${index}]`)), + ); + const tuples = fc.sample(arbitrary, { + seed: request.seed, + numRuns: request.numSamples, + }); + response = { + protocolVersion: PROTOCOL_VERSION, + requestId: request.requestId, + status: 'ok', + samples: tuples.map((tuple) => tuple.map(encodeJsValue)), + }; +} catch (error: unknown) { + response = protocolErrorResponse(error, parsedRequest); +} + +process.stdout.write(`${JSON.stringify(response)}\n`); + +async function readStdin(): Promise { + process.stdin.setEncoding('utf8'); + let input = ''; + for await (const chunk of process.stdin) input += chunk; + return input; +} + +function validateRequest(request: unknown): FastCheckProjectionRequest { + if (!isRecord(request)) { + throw protocolError('protocol.request.invalid', 'Request must be a JSON object', 'request'); + } + if (request.protocolVersion !== PROTOCOL_VERSION) { + throw protocolError( + 'protocol.version.unsupported', + `Unsupported protocol version: ${String(request.protocolVersion)}`, + 'protocolVersion', + ); + } + if (request.operation !== 'sample') { + throw protocolError( + 'protocol.operation.unsupported', + `Unsupported protocol operation: ${String(request.operation)}`, + 'operation', + ); + } + const valid = typeof request.requestId === 'string' + && request.requestId.length > 0 + && typeof request.seed === 'number' + && Number.isInteger(request.seed) + && request.seed >= -0x80000000 + && request.seed <= 0x7fffffff + && typeof request.numSamples === 'number' + && Number.isInteger(request.numSamples) + && request.numSamples >= 1 + && request.numSamples <= 10_000 + && Array.isArray(request.domains) + && request.domains.length > 0; + if (!valid) { + throw protocolError( + 'protocol.request.invalid', + 'Request requires a non-empty ID and domains, an Int seed, and numSamples in 1..10000', + 'request', + ); + } + return { + protocolVersion: PROTOCOL_VERSION, + requestId: request.requestId as string, + operation: 'sample', + seed: request.seed as number, + numSamples: request.numSamples as number, + domains: request.domains as unknown[], + }; +} + +function protocolErrorResponse(error: unknown, request: unknown): FastCheckProjectionFailure { + const protocolFailure = error instanceof ProtocolError ? error : undefined; + const result: FastCheckProjectionFailure = { + protocolVersion: PROTOCOL_VERSION, + status: 'error', + diagnostics: [{ + code: protocolFailure?.code ?? 'protocol.request.invalid', + message: protocolFailure?.diagnosticMessage ?? (error instanceof Error ? error.message : String(error)), + path: protocolFailure?.path ?? 'request', + }], + }; + if (isRecord(request) && typeof request.requestId === 'string') { + result.requestId = request.requestId; + } + return result; +} + +function isRecord(value: unknown): value is Record { + return value !== null && typeof value === 'object' && !Array.isArray(value); +} diff --git a/usvm-ts-pbt/fast-check-adapter/test/js-value.test.ts b/usvm-ts-pbt/fast-check-adapter/test/js-value.test.ts new file mode 100644 index 0000000000..15154526fd --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/js-value.test.ts @@ -0,0 +1,66 @@ +import assert from 'node:assert/strict'; +import test from 'node:test'; +import { + decodeJsValue, + encodeJsValue, +} from '../src/js-value.js'; +import type { JsConcreteValue } from '../src/js-value.js'; + +interface RoundTripCase { + tagged: unknown; + matches: (value: JsConcreteValue) => boolean; +} + +test('tagged JavaScript primitives round trip without losing semantics', () => { + const cases: RoundTripCase[] = [ + { tagged: { kind: 'undefined' }, matches: (value) => value === undefined }, + { tagged: { kind: 'null' }, matches: (value) => value === null }, + { tagged: { kind: 'boolean', value: true }, matches: (value) => value === true }, + { tagged: { kind: 'string', value: 'text' }, matches: (value) => value === 'text' }, + { + tagged: { kind: 'number', value: 'finite', bits: '0000000000000000' }, + matches: (value) => Object.is(value, 0), + }, + { + tagged: { kind: 'number', value: 'finite', bits: '8000000000000000' }, + matches: (value) => Object.is(value, -0), + }, + { tagged: { kind: 'number', value: 'nan' }, matches: Number.isNaN }, + { + tagged: { kind: 'number', value: 'positive-infinity' }, + matches: (value) => value === Number.POSITIVE_INFINITY, + }, + { + tagged: { kind: 'number', value: 'negative-infinity' }, + matches: (value) => value === Number.NEGATIVE_INFINITY, + }, + { + tagged: { + kind: 'array', + elements: [{ kind: 'undefined' }, { kind: 'number', value: 'finite', bits: '8000000000000000' }], + }, + matches: (value) => Array.isArray(value) + && value[0] === undefined + && Object.is(value[1], -0), + }, + ]; + + for (const { tagged, matches } of cases) { + const decoded = decodeJsValue(tagged); + assert.ok(matches(decoded), `decoded value does not match ${JSON.stringify(tagged)}`); + assert.deepEqual(encodeJsValue(decoded), tagged); + } +}); + +test('tagged finite numbers require exactly sixteen lowercase hexadecimal digits', () => { + for (const bits of [undefined, '0', '000000000000000G', '800000000000000A']) { + assert.throws( + () => decodeJsValue({ kind: 'number', value: 'finite', bits }), + /js-number\.encoding\.invalid/, + ); + } +}); + +test('unknown tagged value kinds are rejected explicitly', () => { + assert.throws(() => decodeJsValue({ kind: 'symbol' }), /js-value\.kind\.unknown/); +}); diff --git a/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts new file mode 100644 index 0000000000..3ae1be60b8 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/project-domain.test.ts @@ -0,0 +1,167 @@ +import assert from 'node:assert/strict'; +import test from 'node:test'; +import fc from 'fast-check'; +import { + projectDomain, + projectionCapability, +} from '../src/project-domain.js'; + +test('bounded integers use a real fast-check arbitrary', () => { + const samples = sample({ kind: 'integer', min: -3, max: 7 }); + assert.ok(samples.every( + (value) => typeof value === 'number' && Number.isInteger(value) && value >= -3 && value <= 7, + )); +}); + +test('strings are arbitrary UTF-16 code-unit sequences with declared lengths', () => { + const samples = sample({ kind: 'string', minLength: 2, maxLength: 4 }); + assert.ok(samples.every( + (value) => typeof value === 'string' && value.length >= 2 && value.length <= 4, + )); +}); + +test('unbounded numbers include ECMAScript special values', () => { + const samples = sample( + { + kind: 'number', + min: { value: 'negative-infinity' }, + max: { value: 'positive-infinity' }, + allowNaN: true, + }, + 500, + ); + + assert.ok(samples.some((value) => typeof value === 'number' && Number.isNaN(value))); + assert.ok(samples.includes(Number.NEGATIVE_INFINITY)); + assert.ok(samples.includes(Number.POSITIVE_INFINITY)); + assert.ok(samples.some((value) => typeof value === 'number' && Object.is(value, -0))); +}); + +test('bounded numbers exclude NaN and values outside their inclusive bounds', () => { + const samples = sample({ + kind: 'number', + min: taggedNumber(-1.5), + max: taggedNumber(2.5), + allowNaN: false, + }); + assert.ok(samples.every( + (value) => typeof value === 'number' && !Number.isNaN(value) && value >= -1.5 && value <= 2.5, + )); +}); + +test('singleton infinity ranges project without an empty finite arbitrary', () => { + const bounds: Array = [ + [{ value: 'negative-infinity' }, Number.NEGATIVE_INFINITY], + [{ value: 'positive-infinity' }, Number.POSITIVE_INFINITY], + ]; + for (const [bound, expected] of bounds) { + const samples = sample({ + kind: 'number', + min: bound, + max: bound, + allowNaN: false, + }); + assert.ok(samples.every((value) => value === expected)); + } +}); + +interface ProjectionCase { + name: string; + domain: unknown; + matches: (value: unknown) => boolean; +} + +const projectionCases: ProjectionCase[] = [ + { + name: 'boolean', + domain: { kind: 'boolean' }, + matches: (value) => typeof value === 'boolean', + }, + { + name: 'constant -0', + domain: { kind: 'constant', value: { kind: 'number', value: 'finite', bits: '8000000000000000' } }, + matches: (value) => Object.is(value, -0), + }, + { + name: 'optional undefined', + domain: { kind: 'optional', value: { kind: 'integer', min: -2, max: 2 }, nil: { kind: 'undefined' } }, + matches: (value) => value === undefined + || (typeof value === 'number' && Number.isInteger(value) && value >= -2 && value <= 2), + }, + { + name: 'optional null', + domain: { kind: 'optional', value: { kind: 'boolean' }, nil: { kind: 'null' } }, + matches: (value) => value === null || typeof value === 'boolean', + }, + { + name: 'tuple', + domain: { kind: 'tuple', elements: [{ kind: 'boolean' }, { kind: 'integer', min: 0, max: 3 }] }, + matches: (value) => Array.isArray(value) + && value.length === 2 + && typeof value[0] === 'boolean', + }, + { + name: 'nested array', + domain: { + kind: 'array', + element: { kind: 'array', element: { kind: 'integer', min: 0, max: 3 }, minLength: 1, maxLength: 2 }, + minLength: 1, + maxLength: 4, + }, + matches: (value) => Array.isArray(value) + && value.length >= 1 + && value.length <= 4 + && value.every((inner: unknown) => Array.isArray(inner) && inner.length >= 1 && inner.length <= 2), + }, +]; + +for (const { name, domain, matches } of projectionCases) { + test(`${name} projects to values satisfying the common domain`, () => { + assert.ok(sample(domain).every(matches)); + }); +} + +test('fast-check capability is exact for supported recursive domains', () => { + assert.deepEqual( + projectionCapability({ + kind: 'array', + element: { kind: 'tuple', elements: [{ kind: 'boolean' }, { kind: 'string', minLength: 0, maxLength: 3 }] }, + minLength: 0, + maxLength: 2, + }), + { + backendId: 'fast-check', + backendVersion: '4.9.0', + level: 'exact', + diagnostics: [], + }, + ); +}); + +test('unknown domain kinds are rejected and reported as unsupported', () => { + assert.throws(() => projectDomain({ kind: 'object' }), /domain\.kind\.unknown/); + assert.deepEqual( + projectionCapability({ kind: 'object' }, 'inputs[0].domain'), + { + backendId: 'fast-check', + backendVersion: '4.9.0', + level: 'unsupported', + diagnostics: [{ + code: 'domain.kind.unknown', + message: 'Unknown property domain kind: object', + path: 'inputs[0].domain', + }], + }, + ); +}); + +function sample(domain: unknown, numRuns = 100): unknown[] { + return fc.sample(projectDomain(domain), { seed: 42, numRuns }); +} + +function taggedNumber(value: number): { value: 'finite'; bits: string } { + const buffer = new ArrayBuffer(8); + const view = new DataView(buffer); + view.setFloat64(0, value, false); + return { value: 'finite', bits: view.getBigUint64(0, false).toString(16).padStart(16, '0') }; +} diff --git a/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts b/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts new file mode 100644 index 0000000000..6f46a87566 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/test/projection-cli.test.ts @@ -0,0 +1,182 @@ +import assert from 'node:assert/strict'; +import { spawn } from 'node:child_process'; +import type { Readable } from 'node:stream'; +import { fileURLToPath } from 'node:url'; +import test from 'node:test'; +import type { TaggedJsValue } from '../src/js-value.js'; + +const cliPath = fileURLToPath(new URL('../src/projection-cli.js', import.meta.url)); + +interface SuccessResponse { + protocolVersion: number; + requestId: string; + status: 'ok'; + samples: TaggedJsValue[][]; +} + +interface ErrorResponse { + protocolVersion: number; + requestId?: string; + status: 'error'; + diagnostics: Array<{ + code: string; + message: string; + path: string; + }>; +} + +type WireResponse = SuccessResponse | ErrorResponse; + +interface InvocationResult { + exitCode: number | null; + stdout: string; + stderr: string; + response: WireResponse | undefined; +} + +test('sample response echoes request identity and returns deterministic tagged values', async () => { + const request = { + protocolVersion: 1, + requestId: 'sample-1', + operation: 'sample', + seed: 42, + numSamples: 4, + domains: [{ kind: 'integer', min: -1, max: 1 }], + }; + + const first = await invokeCli(JSON.stringify(request)); + const second = await invokeCli(JSON.stringify(request)); + const firstResponse = requireResponse(first); + const secondResponse = requireResponse(second); + + assert.equal(first.exitCode, 0); + assert.equal(first.stderr, ''); + assert.equal(first.stdout.trim().split('\n').length, 1); + assert.deepEqual(firstResponse, secondResponse); + assert.equal(firstResponse.protocolVersion, 1); + assert.equal(firstResponse.requestId, 'sample-1'); + assert.equal(firstResponse.status, 'ok'); + if (firstResponse.status !== 'ok') assert.fail('Expected a successful response'); + assert.equal(firstResponse.samples.length, 4); + assert.ok(firstResponse.samples.every( + (tuple) => tuple.length === 1 && tuple[0]?.kind === 'number', + )); +}); + +interface ProtocolErrorCase { + name: string; + input: unknown; + code: string; + requestId: string; + path: string; +} + +const protocolErrorCases: ProtocolErrorCase[] = [ + { + name: 'unsupported protocol version', + input: { + protocolVersion: 2, + requestId: 'wrong-version', + operation: 'sample', + seed: 1, + numSamples: 1, + domains: [{ kind: 'boolean' }], + }, + code: 'protocol.version.unsupported', + requestId: 'wrong-version', + path: 'protocolVersion', + }, + { + name: 'unsupported operation', + input: { + protocolVersion: 1, + requestId: 'wrong-operation', + operation: 'check', + seed: 1, + numSamples: 1, + domains: [{ kind: 'boolean' }], + }, + code: 'protocol.operation.unsupported', + requestId: 'wrong-operation', + path: 'operation', + }, + { + name: 'invalid request', + input: { + protocolVersion: 1, + requestId: '', + operation: 'sample', + seed: 1.5, + numSamples: 0, + domains: [], + }, + code: 'protocol.request.invalid', + requestId: '', + path: 'request', + }, +]; + +for (const { name, input, code, requestId, path } of protocolErrorCases) { + test(`${name} returns a typed protocol error`, async () => { + const result = await invokeCli(JSON.stringify(input)); + const response = requireResponse(result); + assert.equal(result.exitCode, 0); + assert.equal(response.status, 'error'); + if (response.status !== 'error') assert.fail('Expected an error response'); + assert.deepEqual(response, { + protocolVersion: 1, + requestId, + status: 'error', + diagnostics: [{ + code, + message: response.diagnostics[0]?.message, + path, + }], + }); + }); +} + +test('malformed JSON produces one clean protocol error document', async () => { + const result = await invokeCli('{not-json'); + const response = requireResponse(result); + + assert.equal(result.exitCode, 0); + assert.equal(result.stderr, ''); + assert.equal(result.stdout.trim().split('\n').length, 1); + assert.equal(response.protocolVersion, 1); + assert.equal(response.status, 'error'); + if (response.status !== 'error') assert.fail('Expected an error response'); + assert.equal(response.diagnostics[0]?.code, 'protocol.json.invalid'); + assert.ok(!('requestId' in response)); +}); + +async function invokeCli(input: string): Promise { + const child = spawn(process.execPath, [cliPath], { stdio: ['pipe', 'pipe', 'pipe'] }); + child.stdin.end(input); + const [exitCode, stdout, stderr] = await Promise.all([ + new Promise((resolve, reject) => { + child.once('error', reject); + child.once('close', (code) => resolve(code)); + }), + collect(child.stdout), + collect(child.stderr), + ]); + let response: WireResponse | undefined; + try { + response = JSON.parse(stdout) as WireResponse; + } catch { + response = undefined; + } + return { exitCode, stdout, stderr, response }; +} + +async function collect(stream: Readable): Promise { + const chunks: Buffer[] = []; + for await (const chunk of stream) chunks.push(Buffer.from(chunk)); + return Buffer.concat(chunks).toString('utf8'); +} + +function requireResponse(result: InvocationResult): WireResponse { + assert.ok(result.response, `CLI did not return JSON: ${result.stdout}`); + return result.response; +} diff --git a/usvm-ts-pbt/fast-check-adapter/tsconfig.json b/usvm-ts-pbt/fast-check-adapter/tsconfig.json new file mode 100644 index 0000000000..706906f1c2 --- /dev/null +++ b/usvm-ts-pbt/fast-check-adapter/tsconfig.json @@ -0,0 +1,20 @@ +{ + "compilerOptions": { + "target": "ES2022", + "module": "NodeNext", + "moduleResolution": "NodeNext", + "rootDir": ".", + "outDir": "dist", + "strict": true, + "noUncheckedIndexedAccess": true, + "exactOptionalPropertyTypes": true, + "noImplicitOverride": true, + "noFallthroughCasesInSwitch": true, + "forceConsistentCasingInFileNames": true, + "verbatimModuleSyntax": true, + "noEmitOnError": true, + "skipLibCheck": true, + "types": ["node"] + }, + "include": ["src/**/*.ts", "test/**/*.ts"] +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt new file mode 100644 index 0000000000..2537881a7c --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt @@ -0,0 +1,98 @@ +package org.usvm.ts.pbt.backend + +/** Describes how faithfully a backend can project a Kotlin property domain. */ +enum class ProjectionLevel { + /** Every value produced by the backend has the declared Kotlin domain semantics. */ + EXACT, + + /** The backend can run the domain, but its values differ from the declared semantics. */ + APPROXIMATE, + + /** The backend cannot project the domain. */ + UNSUPPORTED, +} + +/** Describes which execution modes remain available for a complete property. */ +enum class PropertyCapabilityLevel { + /** Both concrete and symbolic projections preserve the declared property semantics. */ + EXACT, + + /** Both projections are available, but at least one is approximate. */ + APPROXIMATE, + + /** Concrete PBT execution is available, but symbolic execution is not. */ + CONCRETE_ONLY, + + /** Concrete PBT execution is unavailable, so the property cannot be executed. */ + UNSUPPORTED, +} + +/** + * Explains why a projection is not exact. + * + * @property code stable machine-readable diagnostic code + * @property message human-readable description of the limitation + * @property path location of the affected value in the property model + */ +data class CapabilityDiagnostic( + val code: String, + val message: String, + val path: String, +) + +/** + * Reports whether one backend version can represent a property domain. + * + * @property backendId stable backend identifier + * @property backendVersion backend version used to evaluate support + * @property level semantic fidelity of the projection + * @property diagnostics limitations that explain a non-exact [level] + */ +data class ProjectionCapability( + val backendId: String, + val backendVersion: String, + val level: ProjectionLevel, + val diagnostics: List = emptyList(), +) { + init { + require(backendId.isNotBlank()) { "Backend ID must not be blank" } + require(backendVersion.isNotBlank()) { "Backend version must not be blank" } + require(level == ProjectionLevel.EXACT || diagnostics.isNotEmpty()) { + "A non-exact projection requires at least one diagnostic" + } + } +} + +/** Combines domain-level [capabilities] into one deterministic backend capability report. */ +fun aggregateProjectionCapabilities( + backendId: String, + backendVersion: String, + capabilities: List, +): ProjectionCapability { + require(capabilities.all { it.backendId == backendId && it.backendVersion == backendVersion }) { + "All projection capabilities must belong to $backendId $backendVersion" + } + val level = capabilities.maxOfOrNull { it.level } ?: ProjectionLevel.EXACT + val diagnostics = capabilities + .flatMap(ProjectionCapability::diagnostics) + .sortedWith(compareBy(CapabilityDiagnostic::path, CapabilityDiagnostic::code)) + return ProjectionCapability( + backendId = backendId, + backendVersion = backendVersion, + level = level, + diagnostics = diagnostics, + ) +} + +/** Derives the execution modes available when concrete and symbolic projections are considered together. */ +fun classifyPropertyCapability( + concrete: ProjectionCapability, + symbolic: ProjectionCapability, +): PropertyCapabilityLevel = when { + concrete.level == ProjectionLevel.UNSUPPORTED -> PropertyCapabilityLevel.UNSUPPORTED + symbolic.level == ProjectionLevel.UNSUPPORTED -> PropertyCapabilityLevel.CONCRETE_ONLY + concrete.level == ProjectionLevel.APPROXIMATE || symbolic.level == ProjectionLevel.APPROXIMATE -> + PropertyCapabilityLevel.APPROXIMATE + + else -> PropertyCapabilityLevel.EXACT +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt new file mode 100644 index 0000000000..1ce5ce3ac9 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClient.kt @@ -0,0 +1,145 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import java.io.IOException +import java.nio.file.Path +import java.util.concurrent.Executors + +/** + * Synchronous Kotlin client for the private fast-check Node adapter. + * + * Each request starts a fresh adapter process, writes one JSON request, and validates the single JSON response + * before exposing sampled values to Kotlin callers. + */ +class FastCheckProjectionClient( + private val nodeExecutable: String = "node", + private val adapterEntryPoint: Path, +) { + /** Projects the requested domains to fast-check and returns the generated samples. */ + fun sample(request: FastCheckProjectionRequest): FastCheckProjectionResponse { + validateRequest(request) + val response = decodeResponse(invokeAdapter(request)) + validateResponseIdentity(request, response) + throwBackendError(response) + validateSuccessfulResponse(request, response) + return FastCheckProjectionResponse( + protocolVersion = response.protocolVersion, + requestId = requireNotNull(response.requestId), + samples = response.samples, + ) + } + + private fun validateResponseIdentity( + request: FastCheckProjectionRequest, + response: FastCheckProjectionWireResponse, + ) { + if (response.protocolVersion != FAST_CHECK_PROTOCOL_VERSION || response.requestId != request.requestId) { + throw FastCheckProjectionException( + code = "backend.response.mismatch", + message = "fast-check response identity does not match the request", + ) + } + } + + private fun throwBackendError(response: FastCheckProjectionWireResponse) { + if (response.status == "error") { + val diagnostic = response.diagnostics.firstOrNull() + ?: invalidResponse("fast-check error response does not contain a diagnostic") + throw FastCheckProjectionException( + code = diagnostic.code, + message = diagnostic.message, + path = diagnostic.path, + ) + } + } + + private fun validateSuccessfulResponse( + request: FastCheckProjectionRequest, + response: FastCheckProjectionWireResponse, + ) { + if (response.status != "ok" || response.samples.size != request.numSamples || + response.samples.any { it.size != request.domains.size } + ) { + throw FastCheckProjectionException( + code = "backend.response.invalid", + message = "fast-check adapter returned an invalid successful response", + ) + } + } + + private fun invokeAdapter(request: FastCheckProjectionRequest): String { + val process = startAdapter() + val errorReaderExecutor = Executors.newSingleThreadExecutor() + val stderr = errorReaderExecutor.submit { + process.errorStream.bufferedReader(Charsets.UTF_8).use { reader -> reader.readText() } + } + try { + process.outputStream.bufferedWriter(Charsets.UTF_8).use { writer -> + writer.write(PropertyManifestJson.json.encodeToString(request)) + } + val stdout = process.inputStream.bufferedReader(Charsets.UTF_8).use { reader -> reader.readText() } + val exitCode = process.waitFor() + val stderrText = stderr.get() + if (exitCode != 0) { + throw FastCheckProjectionException( + code = "backend.process.failed", + message = "fast-check adapter exited with code $exitCode: ${stderrText.trim()}", + ) + } + if (stdout.isBlank()) { + throw FastCheckProjectionException( + code = "backend.response.empty", + message = "fast-check adapter returned an empty response", + ) + } + return stdout + } finally { + errorReaderExecutor.shutdownNow() + } + } + + private fun startAdapter(): Process = try { + ProcessBuilder(nodeExecutable, adapterEntryPoint.toString()).start() + } catch (error: IOException) { + throw FastCheckProjectionException( + code = "backend.process.start.failed", + message = "Failed to start fast-check adapter: ${error.message}", + cause = error, + ) + } + + private fun decodeResponse(stdout: String): FastCheckProjectionWireResponse = try { + PropertyManifestJson.json.decodeFromString(stdout) + } catch (error: IllegalArgumentException) { + throw FastCheckProjectionException( + code = "backend.response.invalid", + message = "fast-check adapter returned invalid JSON: ${error.message}", + cause = error, + ) + } + + private fun invalidResponse(message: String): Nothing = throw FastCheckProjectionException( + code = "backend.response.invalid", + message = message, + ) + + private fun validateRequest(request: FastCheckProjectionRequest) { + val valid = request.requestId.isNotEmpty() && + request.operation == "sample" && + request.numSamples in 1..MAX_SAMPLES && + request.domains.isNotEmpty() + if (!valid) { + throw FastCheckProjectionException( + code = "protocol.request.invalid", + message = "Request requires a non-empty ID and domains, operation sample, and numSamples in 1..10000", + path = "request", + ) + } + } + + private companion object { + const val MAX_SAMPLES = 10_000 + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt new file mode 100644 index 0000000000..33900a4620 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionProtocol.kt @@ -0,0 +1,49 @@ +package org.usvm.ts.pbt.fastcheck + +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDomain + +const val FAST_CHECK_PROTOCOL_VERSION = 1 + +/** One versioned request sent from Kotlin to the private fast-check adapter process. */ +@Serializable +data class FastCheckProjectionRequest( + val protocolVersion: Int = FAST_CHECK_PROTOCOL_VERSION, + val requestId: String, + val operation: String = "sample", + val seed: Int, + val numSamples: Int, + val domains: List, +) + +/** Validated samples returned by fast-check in positional input order. */ +data class FastCheckProjectionResponse( + val protocolVersion: Int, + val requestId: String, + val samples: List>, +) + +@Serializable +internal data class FastCheckProjectionWireResponse( + val protocolVersion: Int, + val requestId: String? = null, + val status: String, + val samples: List> = emptyList(), + val diagnostics: List = emptyList(), +) + +@Serializable +internal data class FastCheckProtocolDiagnostic( + val code: String, + val message: String, + val path: String? = null, +) + +/** Typed failure reported by the fast-check process or its Kotlin protocol boundary. */ +class FastCheckProjectionException( + val code: String, + message: String, + val path: String? = null, + cause: Throwable? = null, +) : RuntimeException(message, cause) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt new file mode 100644 index 0000000000..26fe1886d4 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt @@ -0,0 +1,57 @@ +package org.usvm.ts.pbt.manifest + +import kotlinx.serialization.Serializable +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.Json +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.validation.requireValid +import org.usvm.ts.pbt.validation.validatePropertyDefinition +import org.usvm.ts.pbt.validation.validatePropertyManifest + +const val PROPERTY_MANIFEST_SCHEMA_VERSION = 1 + +/** + * Versioned transport representation of a validated [PropertyDefinition]. + * + * The manifest is the boundary shared with replaceable concrete PBT adapters and later symbolic projections. + */ +@Serializable +data class PropertyManifest( + val schemaVersion: Int = PROPERTY_MANIFEST_SCHEMA_VERSION, + val propertyId: String, + val inputs: List, + val predicate: TypeScriptEntryPoint, + val precondition: TypeScriptEntryPoint? = null, +) + +fun PropertyDefinition.toManifest(): PropertyManifest { + requireValid(validatePropertyDefinition(this)) + return PropertyManifest( + propertyId = id.value, + inputs = inputs, + predicate = predicate, + precondition = precondition, + ) +} + +/** Strict JSON codec for versioned property manifests. */ +object PropertyManifestJson { + val json = Json { + classDiscriminator = "kind" + encodeDefaults = true + explicitNulls = false + ignoreUnknownKeys = false + useAlternativeNames = false + } + + fun encode(manifest: PropertyManifest): String { + requireValid(validatePropertyManifest(manifest)) + return json.encodeToString(manifest) + } + + fun decode(value: String): PropertyManifest = json.decodeFromString(value) + .also { requireValid(validatePropertyManifest(it)) } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt new file mode 100644 index 0000000000..dd53ce0943 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt @@ -0,0 +1,220 @@ +package org.usvm.ts.pbt.model + +import kotlinx.serialization.KSerializer +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable +import kotlinx.serialization.SerializationException +import kotlinx.serialization.descriptors.SerialDescriptor +import kotlinx.serialization.descriptors.buildClassSerialDescriptor +import kotlinx.serialization.encoding.Decoder +import kotlinx.serialization.encoding.Encoder +import kotlinx.serialization.json.JsonArray +import kotlinx.serialization.json.JsonDecoder +import kotlinx.serialization.json.JsonEncoder +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.booleanOrNull +import kotlinx.serialization.json.buildJsonObject +import kotlinx.serialization.json.jsonArray +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import kotlinx.serialization.json.put + +/** Tags the finite and non-finite cases of an ECMAScript binary64 value. */ +@Serializable +enum class JsNumberKind { + /** Finite value represented by its raw IEEE-754 bits. */ + @SerialName("finite") + FINITE, + + /** JavaScript NaN value. */ + @SerialName("nan") + NAN, + + /** Positive infinity. */ + @SerialName("positive-infinity") + POSITIVE_INFINITY, + + /** Negative infinity. */ + @SerialName("negative-infinity") + NEGATIVE_INFINITY, +} + +/** Lossless tagged representation of a JavaScript number, including NaN, infinities, and negative zero. */ +@Serializable +data class JsNumber( + val value: JsNumberKind, + val bits: String? = null, +) { + fun toDouble(): Double = when (value) { + JsNumberKind.FINITE -> Double.fromBits( + requireNotNull(bits) { "A finite JavaScript number requires IEEE-754 bits" } + .toULong(JS_NUMBER_HEX_RADIX) + .toLong(), + ) + + JsNumberKind.NAN -> Double.NaN + JsNumberKind.POSITIVE_INFINITY -> Double.POSITIVE_INFINITY + JsNumberKind.NEGATIVE_INFINITY -> Double.NEGATIVE_INFINITY + } + + companion object { + fun finite(value: Double): JsNumber { + require(value.isFinite()) { "Use a tagged representation for non-finite JavaScript numbers" } + return JsNumber( + value = JsNumberKind.FINITE, + bits = value + .toRawBits() + .toULong() + .toString(JS_NUMBER_HEX_RADIX) + .padStart(JS_NUMBER_HEX_DIGITS, '0'), + ) + } + + fun fromDouble(value: Double): JsNumber = when { + value.isNaN() -> nan() + value == Double.POSITIVE_INFINITY -> positiveInfinity() + value == Double.NEGATIVE_INFINITY -> negativeInfinity() + else -> finite(value) + } + + fun nan(): JsNumber = JsNumber(JsNumberKind.NAN) + + fun positiveInfinity(): JsNumber = JsNumber(JsNumberKind.POSITIVE_INFINITY) + + fun negativeInfinity(): JsNumber = JsNumber(JsNumberKind.NEGATIVE_INFINITY) + } +} + +/** Lossless transport value for JavaScript primitives and recursively nested arrays. */ +@Serializable(with = JsConcreteValueSerializer::class) +sealed interface JsConcreteValue { + /** JavaScript `undefined`. */ + data object Undefined : JsConcreteValue + + /** JavaScript `null`. */ + data object Null : JsConcreteValue + + /** Concrete JavaScript boolean value. */ + data class Boolean(val value: kotlin.Boolean) : JsConcreteValue + + /** Concrete JavaScript UTF-16 string value. */ + data class String(val value: kotlin.String) : JsConcreteValue + + /** Concrete JavaScript binary64 number with lossless special-value encoding. */ + data class Number(val number: JsNumber) : JsConcreteValue { + fun toDouble(): Double = number.toDouble() + } + + /** Ordered recursively tagged elements of one concrete JavaScript array. */ + data class Array(val elements: List) : JsConcreteValue +} + +/** JSON serializer for the tagged [JsConcreteValue] wire representation. */ +object JsConcreteValueSerializer : KSerializer { + override val descriptor: SerialDescriptor = buildClassSerialDescriptor("JsConcreteValue") + + override fun serialize(encoder: Encoder, value: JsConcreteValue) { + val jsonEncoder = encoder as? JsonEncoder + ?: throw SerializationException("JsConcreteValue supports JSON serialization only") + jsonEncoder.encodeJsonElement( + buildJsonObject { + when (value) { + JsConcreteValue.Undefined -> { + put("kind", "undefined") + } + + JsConcreteValue.Null -> { + put("kind", "null") + } + + is JsConcreteValue.Boolean -> { + put("kind", "boolean") + put("value", value.value) + } + + is JsConcreteValue.String -> { + put("kind", "string") + put("value", value.value) + } + + is JsConcreteValue.Number -> { + put("kind", "number") + put("value", value.number.value.serialName) + value.number.bits?.let { put("bits", it) } + } + + is JsConcreteValue.Array -> { + val elements = value.elements.map { element -> + jsonEncoder.json.encodeToJsonElement(JsConcreteValueSerializer, element) + } + val jsonElements = JsonArray(elements) + + put("kind", "array") + put("elements", jsonElements) + } + } + }, + ) + } + + override fun deserialize(decoder: Decoder): JsConcreteValue { + val jsonDecoder = decoder as? JsonDecoder + ?: throw SerializationException("JsConcreteValue supports JSON deserialization only") + val value = jsonDecoder.decodeJsonElement().jsonObject + return when (val kind = value.requiredString("kind")) { + "undefined" -> JsConcreteValue.Undefined + "null" -> JsConcreteValue.Null + "boolean" -> deserializeBoolean(value) + "string" -> JsConcreteValue.String(value.requiredString("value")) + "number" -> deserializeNumber(value) + "array" -> deserializeArray(jsonDecoder, value) + else -> throw SerializationException("Unknown JavaScript value kind: $kind") + } + } +} + +private fun deserializeBoolean(value: JsonObject): JsConcreteValue.Boolean { + val booleanValue = value["value"]?.jsonPrimitive?.booleanOrNull + ?: throw SerializationException("Boolean JsConcreteValue requires a boolean value") + return JsConcreteValue.Boolean(booleanValue) +} + +private fun deserializeNumber(value: JsonObject): JsConcreteValue.Number { + val numberKindName = value.requiredString("value") + val numberKind = when (numberKindName) { + "finite" -> JsNumberKind.FINITE + "nan" -> JsNumberKind.NAN + "positive-infinity" -> JsNumberKind.POSITIVE_INFINITY + "negative-infinity" -> JsNumberKind.NEGATIVE_INFINITY + else -> throw SerializationException("Unknown JavaScript number kind: $numberKindName") + } + val bits = value["bits"]?.jsonPrimitive?.content + val number = JsNumber(value = numberKind, bits = bits) + + return JsConcreteValue.Number(number) +} + +private fun deserializeArray(jsonDecoder: JsonDecoder, value: JsonObject): JsConcreteValue.Array { + val jsonElements = value["elements"]?.jsonArray + ?: throw SerializationException("Array JsConcreteValue requires elements") + val elements = jsonElements.map { element -> + jsonDecoder.json.decodeFromJsonElement(JsConcreteValueSerializer, element) + } + + return JsConcreteValue.Array(elements) +} + +private val JsNumberKind.serialName: String + get() = when (this) { + JsNumberKind.FINITE -> "finite" + JsNumberKind.NAN -> "nan" + JsNumberKind.POSITIVE_INFINITY -> "positive-infinity" + JsNumberKind.NEGATIVE_INFINITY -> "negative-infinity" + } + +private fun JsonObject.requiredString(name: String): String = + get(name)?.jsonPrimitive?.content + ?: throw SerializationException("JsConcreteValue requires a $name field") + +private const val JS_NUMBER_HEX_DIGITS = 16 +private const val JS_NUMBER_HEX_RADIX = 16 diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt new file mode 100644 index 0000000000..b9234fba98 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt @@ -0,0 +1,78 @@ +package org.usvm.ts.pbt.model + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable + +/** Stable canonical identifier used to correlate one property across artifacts and backends. */ +@JvmInline +@Serializable +value class PropertyId private constructor(val value: String) { + override fun toString(): String = value + + companion object { + operator fun invoke(value: String): PropertyId { + require(isCanonicalPropertyId(value)) { "Invalid property ID: $value" } + return PropertyId(value) + } + + internal fun unchecked(value: String): PropertyId = PropertyId(value) + } +} + +/** + * Backend-independent Kotlin definition of one property. + * + * @property id stable identity of the property + * @property inputs ordered domains matching positional TypeScript parameters + * @property predicate TypeScript function that must hold for generated inputs + * @property precondition optional TypeScript function that filters inputs before evaluation + */ +@Serializable +data class PropertyDefinition( + val id: PropertyId, + val inputs: List, + val predicate: TypeScriptEntryPoint, + val precondition: TypeScriptEntryPoint? = null, +) + +/** + * Names one positional property input and declares its backend-independent domain. + * + * @property name JavaScript identifier used in diagnostics and artifacts + * @property domain values that concrete and symbolic backends may produce + */ +@Serializable +data class PropertyInput( + val name: String, + val domain: PropertyDomain, +) + +/** + * References an exported TypeScript function without loading or executing it. + * + * @property module normalized project-relative POSIX module path + * @property exportName JavaScript identifier exported by [module] + * @property executionKind whether invoking the function returns directly or asynchronously + */ +@Serializable +data class TypeScriptEntryPoint( + val module: String, + val exportName: String, + val executionKind: ExecutionKind = ExecutionKind.SYNC, +) + +/** Describes how a referenced TypeScript function completes. */ +@Serializable +enum class ExecutionKind { + /** The function returns its result directly. */ + @SerialName("sync") + SYNC, + + /** The function returns an awaitable result. */ + @SerialName("async") + ASYNC, +} + +internal fun isCanonicalPropertyId(value: String): Boolean = PROPERTY_ID_REGEX.matches(value) + +private val PROPERTY_ID_REGEX = Regex("[A-Za-z0-9][A-Za-z0-9._/-]*") diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt new file mode 100644 index 0000000000..f7a9270775 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt @@ -0,0 +1,72 @@ +package org.usvm.ts.pbt.model + +import kotlinx.serialization.SerialName +import kotlinx.serialization.Serializable + +const val DEFAULT_MAX_STRING_LENGTH = 10 +const val DEFAULT_MAX_ARRAY_LENGTH = 10 + +/** Backend-independent set of JavaScript values that a property input may receive. */ +@Serializable +sealed interface PropertyDomain + +/** Domain containing both JavaScript boolean values. */ +@Serializable +@SerialName("boolean") +data object BooleanDomain : PropertyDomain + +/** Inclusive domain of signed 32-bit integers. */ +@Serializable +@SerialName("integer") +data class IntegerDomain( + val min: Int = Int.MIN_VALUE, + val max: Int = Int.MAX_VALUE, +) : PropertyDomain + +/** + * Inclusive ECMAScript binary64 domain. + * + * Tagged infinities are valid bounds; [allowNaN] controls whether NaN belongs to an otherwise unbounded domain. + */ +@Serializable +@SerialName("number") +data class NumberDomain( + val min: JsNumber = JsNumber.negativeInfinity(), + val max: JsNumber = JsNumber.positiveInfinity(), + val allowNaN: Boolean = true, +) : PropertyDomain + +/** Domain of arbitrary UTF-16 code-unit sequences within the inclusive length bounds. */ +@Serializable +@SerialName("string") +data class StringDomain( + val minLength: Int = 0, + val maxLength: Int = DEFAULT_MAX_STRING_LENGTH, +) : PropertyDomain + +/** Singleton domain containing one tagged JavaScript primitive. */ +@Serializable +@SerialName("constant") +data class ConstantDomain(val value: JsConcreteValue) : PropertyDomain + +/** Domain containing [value] plus exactly one nullish [nil] value. */ +@Serializable +@SerialName("optional") +data class OptionalDomain( + val value: PropertyDomain, + val nil: JsConcreteValue = JsConcreteValue.Undefined, +) : PropertyDomain + +/** Fixed-length ordered product of non-empty recursive domains. */ +@Serializable +@SerialName("tuple") +data class TupleDomain(val elements: List) : PropertyDomain + +/** Recursive array domain with inclusive JavaScript length bounds. */ +@Serializable +@SerialName("array") +data class ArrayDomain( + val element: PropertyDomain, + val minLength: Int = 0, + val maxLength: Int = DEFAULT_MAX_ARRAY_LENGTH, +) : PropertyDomain diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt new file mode 100644 index 0000000000..00078b0053 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt @@ -0,0 +1,327 @@ +package org.usvm.ts.pbt.validation + +import org.usvm.ts.pbt.manifest.PROPERTY_MANIFEST_SCHEMA_VERSION +import org.usvm.ts.pbt.manifest.PropertyManifest +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.JsNumber +import org.usvm.ts.pbt.model.JsNumberKind +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDefinition +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.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.isCanonicalPropertyId + +/** + * One deterministic validation failure. + * + * @property code stable machine-readable diagnostic code + * @property message human-readable description of the invalid value + * @property path location of the invalid value in the property model + */ +data class ValidationDiagnostic( + val code: String, + val message: String, + val path: String, +) + +/** Ordered validation diagnostics and their derived validity state. */ +data class PropertyValidationResult(val diagnostics: List) { + val isValid: Boolean + get() = diagnostics.isEmpty() +} + +/** Thrown when an operation requires a valid property but receives [result] with diagnostics. */ +class InvalidPropertyDefinitionException( + val result: PropertyValidationResult, +) : IllegalArgumentException(result.diagnostics.joinToString(separator = "; ") { "${it.path}: ${it.message}" }) + +fun validatePropertyDefinition(definition: PropertyDefinition): PropertyValidationResult = validateProperty( + propertyId = definition.id.value, + inputs = definition.inputs, + predicate = definition.predicate, + precondition = definition.precondition, +) + +fun validatePropertyManifest(manifest: PropertyManifest): PropertyValidationResult { + val diagnostics = mutableListOf() + if (manifest.schemaVersion != PROPERTY_MANIFEST_SCHEMA_VERSION) { + diagnostics += diagnostic( + code = "manifest.schema.unsupported", + message = "Unsupported property manifest schema version: ${manifest.schemaVersion}", + path = "schemaVersion", + ) + } + diagnostics += validateProperty( + propertyId = manifest.propertyId, + inputs = manifest.inputs, + predicate = manifest.predicate, + precondition = manifest.precondition, + ).diagnostics + return diagnostics.toResult() +} + +fun requireValid(result: PropertyValidationResult) { + if (!result.isValid) { + throw InvalidPropertyDefinitionException(result) + } +} + +private fun validateProperty( + propertyId: String, + inputs: List, + predicate: TypeScriptEntryPoint, + precondition: TypeScriptEntryPoint?, +): PropertyValidationResult { + val diagnostics = mutableListOf() + if (!isCanonicalPropertyId(propertyId)) { + diagnostics += diagnostic("property.id.invalid", "Invalid property ID", "propertyId") + } + if (inputs.isEmpty()) { + diagnostics += diagnostic("property.inputs.empty", "A property requires at least one input", "inputs") + } + + val firstInputByName = mutableMapOf() + inputs.forEachIndexed { index, input -> + val path = "inputs[$index]" + if (!isJavaScriptIdentifier(input.name)) { + diagnostics += diagnostic("input.name.invalid", "Invalid input name", "$path.name") + } + if (firstInputByName.putIfAbsent(input.name, index) != null) { + diagnostics += diagnostic("input.name.duplicate", "Duplicate input name: ${input.name}", path) + } + validateDomain(input.domain, "$path.domain", diagnostics) + } + + validateEntryPoint(predicate, "predicate", diagnostics) + precondition?.let { validateEntryPoint(it, "precondition", diagnostics) } + return diagnostics.toResult() +} + +private fun validateDomain( + domain: PropertyDomain, + path: String, + diagnostics: MutableList, +) { + when (domain) { + BooleanDomain -> { + Unit + } + + is IntegerDomain -> { + if (domain.min > domain.max) { + diagnostics += diagnostic("domain.integer.bounds", "Integer minimum exceeds maximum", path) + } + } + + is NumberDomain -> { + validateNumberDomain(domain, path, diagnostics) + } + + is StringDomain -> { + validateLengths( + minLength = domain.minLength, + maxLength = domain.maxLength, + code = "domain.string.length", + description = "String", + path = path, + diagnostics = diagnostics, + ) + } + + is ConstantDomain -> { + if (domain.value is JsConcreteValue.Array) { + diagnostics += diagnostic( + "domain.constant.unsupported", + "Constant domains support JavaScript primitives only", + path, + ) + } + validateJsConcreteValue(domain.value, "$path.value", diagnostics) + } + is OptionalDomain -> { + if (domain.nil != JsConcreteValue.Undefined && domain.nil != JsConcreteValue.Null) { + diagnostics += diagnostic( + "domain.optional.nil", + "Optional nil must be null or undefined", + "$path.nil", + ) + } + validateJsConcreteValue(domain.nil, "$path.nil", diagnostics) + validateDomain(domain.value, "$path.value", diagnostics) + } + + is TupleDomain -> { + if (domain.elements.isEmpty()) { + diagnostics += diagnostic("domain.tuple.empty", "Tuple domain must not be empty", path) + } + domain.elements.forEachIndexed { index, element -> + validateDomain(element, "$path.elements[$index]", diagnostics) + } + } + + is ArrayDomain -> { + validateLengths( + minLength = domain.minLength, + maxLength = domain.maxLength, + code = "domain.array.length", + description = "Array", + path = path, + diagnostics = diagnostics, + ) + validateDomain(domain.element, "$path.element", diagnostics) + } + } +} + +private fun validateNumberDomain( + domain: NumberDomain, + path: String, + diagnostics: MutableList, +) { + val minimumEncodingIsValid = validateJsNumber(domain.min, "$path.min", diagnostics) + val maximumEncodingIsValid = validateJsNumber(domain.max, "$path.max", diagnostics) + + if (domain.min.value == JsNumberKind.NAN) { + diagnostics += diagnostic("domain.number.bound.nan", "Number minimum must not be NaN", "$path.min") + } + if (domain.max.value == JsNumberKind.NAN) { + diagnostics += diagnostic("domain.number.bound.nan", "Number maximum must not be NaN", "$path.max") + } + + val encodingsAreValid = minimumEncodingIsValid && maximumEncodingIsValid + val boundsAreNotNaN = domain.min.value != JsNumberKind.NAN && domain.max.value != JsNumberKind.NAN + val boundsCanBeCompared = encodingsAreValid && boundsAreNotNaN + val minimumExceedsMaximum = boundsCanBeCompared && domain.min.toDouble() > domain.max.toDouble() + if (minimumExceedsMaximum) { + diagnostics += diagnostic("domain.number.bounds", "Number minimum exceeds maximum", path) + } + + val bounded = domain.min != JsNumber.negativeInfinity() || domain.max != JsNumber.positiveInfinity() + if (bounded && domain.allowNaN) { + diagnostics += diagnostic( + "domain.number.nan-bounded", + "Bounded number domains must exclude NaN", + "$path.allowNaN", + ) + } +} + +private fun validateJsConcreteValue( + value: JsConcreteValue, + path: String, + diagnostics: MutableList, +) { + if (value is JsConcreteValue.Number) { + validateJsNumber(value.number, path, diagnostics) + } + if (value is JsConcreteValue.Array) { + value.elements.forEachIndexed { index, element -> + validateJsConcreteValue(element, "$path.elements[$index]", diagnostics) + } + } +} + +private fun validateJsNumber( + number: JsNumber, + path: String, + diagnostics: MutableList, +): Boolean { + val valid = when (number.value) { + JsNumberKind.FINITE -> number.bits?.matches(FINITE_NUMBER_BITS_REGEX) == true + else -> number.bits == null + } + if (!valid) { + diagnostics += diagnostic( + "js-number.encoding.invalid", + "Invalid tagged JavaScript number encoding", + path, + ) + } + return valid +} + +private fun validateLengths( + minLength: Int, + maxLength: Int, + code: String, + description: String, + path: String, + diagnostics: MutableList, +) { + if (minLength < 0 || maxLength < 0 || minLength > maxLength) { + diagnostics += diagnostic(code, "$description length bounds are invalid", path) + } +} + +private fun validateEntryPoint( + entryPoint: TypeScriptEntryPoint, + path: String, + diagnostics: MutableList, +) { + if (!isProjectRelativePosixPath(entryPoint.module)) { + diagnostics += diagnostic("entrypoint.module.invalid", "Invalid TypeScript module path", "$path.module") + } + if (!isJavaScriptIdentifier(entryPoint.exportName)) { + diagnostics += diagnostic("entrypoint.export.invalid", "Invalid TypeScript export name", "$path.exportName") + } +} + +private fun isProjectRelativePosixPath(path: String): Boolean = + path.isNotBlank() && + !path.startsWith('/') && + '\\' !in path && + path.split('/').none { it.isEmpty() || it == "." || it == ".." } + +private fun isJavaScriptIdentifier(value: String): Boolean { + if (value.isEmpty()) return false + + var index = 0 + var first = true + + while (index < value.length) { + val codePoint = value.codePointAt(index) + val valid = if (first) { + isJavaScriptIdentifierStart(codePoint) + } else { + isJavaScriptIdentifierPart(codePoint) + } + if (!valid) return false + + first = false + index += Character.charCount(codePoint) + } + + return true +} + +private fun isJavaScriptIdentifierStart(codePoint: Int): Boolean = + codePoint == '$'.code || + codePoint == '_'.code || + Character.isUnicodeIdentifierStart(codePoint) + +private fun isJavaScriptIdentifierPart(codePoint: Int): Boolean = + isJavaScriptIdentifierStart(codePoint) || + codePoint == ZERO_WIDTH_NON_JOINER_CODE_POINT || + codePoint == ZERO_WIDTH_JOINER_CODE_POINT || + Character.isUnicodeIdentifierPart(codePoint) + +private fun MutableList.toResult(): PropertyValidationResult { + val orderedDiagnostics = sortedWith(compareBy(ValidationDiagnostic::path, ValidationDiagnostic::code)) + return PropertyValidationResult(orderedDiagnostics) +} + +private fun diagnostic(code: String, message: String, path: String) = ValidationDiagnostic(code, message, path) + +private val FINITE_NUMBER_BITS_REGEX = Regex("[0-9a-f]{16}") + +// ECMAScript permits these otherwise invisible Unicode characters after the first identifier character. +private const val ZERO_WIDTH_NON_JOINER_CODE_POINT = 0x200C +private const val ZERO_WIDTH_JOINER_CODE_POINT = 0x200D diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt new file mode 100644 index 0000000000..ea1739bf9c --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/backend/ProjectionCapabilityTest.kt @@ -0,0 +1,119 @@ +package org.usvm.ts.pbt.backend + +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class ProjectionCapabilityTest { + @Test + fun `least capable nested projection wins and diagnostics are deterministic`() { + val capability = aggregateProjectionCapabilities( + backendId = FAST_CHECK_ID, + backendVersion = FAST_CHECK_VERSION, + capabilities = listOf( + exact(), + approximate("inputs[1].domain", "domain.string.approximate"), + approximate("inputs[0].domain", "domain.number.approximate"), + ), + ) + + assertEquals(FAST_CHECK_ID, capability.backendId) + assertEquals(FAST_CHECK_VERSION, capability.backendVersion) + assertEquals(ProjectionLevel.APPROXIMATE, capability.level) + assertEquals( + listOf("domain.number.approximate", "domain.string.approximate"), + capability.diagnostics.map { it.code }, + ) + } + + @Test + fun `unsupported nested projection wins over approximate projection`() { + val capability = aggregateProjectionCapabilities( + backendId = FAST_CHECK_ID, + backendVersion = FAST_CHECK_VERSION, + capabilities = listOf( + approximate("inputs[0].domain", "domain.number.approximate"), + unsupported("inputs[1].domain", "domain.object.unsupported"), + ), + ) + + assertEquals(ProjectionLevel.UNSUPPORTED, capability.level) + } + + @Test + fun `non exact capability requires a diagnostic reason`() { + assertFailsWith { + ProjectionCapability( + backendId = FAST_CHECK_ID, + backendVersion = FAST_CHECK_VERSION, + level = ProjectionLevel.APPROXIMATE, + ) + } + } + + @Test + fun `supported concrete and unsupported symbolic is concrete only`() { + assertEquals( + PropertyCapabilityLevel.CONCRETE_ONLY, + classifyPropertyCapability( + concrete = exact(), + symbolic = unsupported("predicate", "entrypoint.async", backendId = "usvm"), + ), + ) + } + + @Test + fun `property classification accounts for both projections`() { + assertEquals( + PropertyCapabilityLevel.EXACT, + classifyPropertyCapability(exact(), exact(backendId = "usvm")), + ) + assertEquals( + PropertyCapabilityLevel.APPROXIMATE, + classifyPropertyCapability( + exact(), + approximate("inputs[0].domain", "domain.approximate", backendId = "usvm"), + ), + ) + assertEquals( + PropertyCapabilityLevel.UNSUPPORTED, + classifyPropertyCapability( + unsupported("inputs[0].domain", "domain.unsupported"), + exact(backendId = "usvm"), + ), + ) + } + + private fun exact(backendId: String = FAST_CHECK_ID) = ProjectionCapability( + backendId = backendId, + backendVersion = FAST_CHECK_VERSION, + level = ProjectionLevel.EXACT, + ) + + private fun approximate( + path: String, + code: String, + backendId: String = FAST_CHECK_ID, + ) = ProjectionCapability( + backendId = backendId, + backendVersion = FAST_CHECK_VERSION, + level = ProjectionLevel.APPROXIMATE, + diagnostics = listOf(CapabilityDiagnostic(code, "Approximate projection", path)), + ) + + private fun unsupported( + path: String, + code: String, + backendId: String = FAST_CHECK_ID, + ) = ProjectionCapability( + backendId = backendId, + backendVersion = FAST_CHECK_VERSION, + level = ProjectionLevel.UNSUPPORTED, + diagnostics = listOf(CapabilityDiagnostic(code, "Unsupported projection", path)), + ) + + private companion object { + const val FAST_CHECK_ID = "fast-check" + const val FAST_CHECK_VERSION = "4.9.0" + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt new file mode 100644 index 0000000000..e4493515a2 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt @@ -0,0 +1,90 @@ +package org.usvm.ts.pbt.examples + +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.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.IntegerDomain +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.validation.validatePropertyDefinition +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.absolute +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class ExamplePropertiesTest { + @Test + fun `four Kotlin property shapes validate serialize and project through fast-check`() { + assertNotNull(javaClass.getResource("/properties/examples/PropertyExamples.ts")) + val client = FastCheckProjectionClient(adapterEntryPoint = adapterEntryPoint()) + + examples.forEachIndexed { index, definition -> + assertTrue(validatePropertyDefinition(definition).isValid, definition.id.value) + val manifest = definition.toManifest() + assertEquals(manifest, PropertyManifestJson.decode(PropertyManifestJson.encode(manifest))) + + val response = client.sample( + FastCheckProjectionRequest( + requestId = "example-$index", + seed = 42, + numSamples = 5, + domains = definition.inputs.map(PropertyInput::domain), + ), + ) + assertEquals(5, response.samples.size) + assertTrue(response.samples.all { it.size == definition.inputs.size }) + } + } + + private companion object { + const val MODULE = "properties/examples/PropertyExamples.ts" + + val examples = listOf( + PropertyDefinition( + id = PropertyId("example.relational"), + inputs = listOf( + PropertyInput("left", IntegerDomain()), + PropertyInput("right", IntegerDomain()), + ), + predicate = TypeScriptEntryPoint(MODULE, "isCommutative"), + ), + PropertyDefinition( + id = PropertyId("example.bounded"), + inputs = listOf(PropertyInput("value", IntegerDomain(-100, 100))), + predicate = TypeScriptEntryPoint(MODULE, "boundedValueStaysBounded"), + ), + PropertyDefinition( + id = PropertyId("example.precondition"), + inputs = listOf( + PropertyInput("dividend", IntegerDomain(-100, 100)), + PropertyInput("divisor", IntegerDomain(-10, 10)), + ), + predicate = TypeScriptEntryPoint(MODULE, "divisionRoundTrip"), + precondition = TypeScriptEntryPoint(MODULE, "nonZeroDivisor"), + ), + PropertyDefinition( + id = PropertyId("example.array"), + inputs = listOf( + PropertyInput("values", ArrayDomain(IntegerDomain(-5, 5), minLength = 0, maxLength = 5)), + ), + predicate = TypeScriptEntryPoint(MODULE, "reverseTwicePreservesValues"), + ), + ) + + fun adapterEntryPoint(): Path { + val candidates = listOf( + Path.of("fast-check-adapter/dist/src/projection-cli.js"), + Path.of("usvm-ts-pbt/fast-check-adapter/dist/src/projection-cli.js"), + ).map { it.absolute() } + return candidates.singleOrNull(Files::isRegularFile) + ?: error("Cannot locate fast-check adapter; checked $candidates") + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt new file mode 100644 index 0000000000..e401303162 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProjectionClientTest.kt @@ -0,0 +1,197 @@ +package org.usvm.ts.pbt.fastcheck + +import org.junit.jupiter.api.Test +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.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDomain +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.absolute +import kotlin.io.path.createTempFile +import kotlin.io.path.deleteIfExists +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class FastCheckProjectionClientTest { + private val client = FastCheckProjectionClient(adapterEntryPoint = adapterEntryPoint()) + + @Test + fun `Kotlin domains produce deterministic tagged fast-check samples`() { + val request = FastCheckProjectionRequest( + requestId = "integration-1", + seed = 42, + numSamples = 20, + domains = listOf(IntegerDomain(-10, 10), ArrayDomain(BooleanDomain, 0, 3)), + ) + + val first = client.sample(request) + val second = client.sample(request) + + assertEquals(first, second) + assertEquals(FAST_CHECK_PROTOCOL_VERSION, first.protocolVersion) + assertEquals("integration-1", first.requestId) + assertEquals(20, first.samples.size) + first.samples.forEach { sample -> assertConforms(sample, request.domains) } + } + + @Test + fun `protocol version mismatch is a typed backend error`() { + val error = assertFailsWith { + client.sample(validRequest.copy(protocolVersion = 999)) + } + + assertEquals("protocol.version.unsupported", error.code) + assertEquals("protocolVersion", error.path) + } + + @Test + fun `invalid request is rejected before starting Node`() { + val missingAdapterClient = FastCheckProjectionClient( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = Path.of("missing-adapter.mjs"), + ) + + val error = assertFailsWith { + missingAdapterClient.sample(validRequest.copy(numSamples = 0)) + } + + assertEquals("protocol.request.invalid", error.code) + } + + @Test + fun `process startup and exit failures are typed transport errors`() { + val startup = assertFailsWith { + FastCheckProjectionClient( + nodeExecutable = "definitely-not-a-node-executable", + adapterEntryPoint = adapterEntryPoint(), + ).sample(validRequest) + } + assertEquals("backend.process.start.failed", startup.code) + + val exit = assertFailsWith { + FastCheckProjectionClient( + adapterEntryPoint = Path.of("missing-adapter.mjs"), + ).sample(validRequest) + } + assertEquals("backend.process.failed", exit.code) + } + + @Test + fun `invalid protocol output is a typed transport error`() { + withTemporaryAdapter("process.stdout.write('not-json\\n')") { temporaryClient -> + val malformed = assertFailsWith { + temporaryClient.sample(validRequest) + } + assertEquals("backend.response.invalid", malformed.code) + } + + withTemporaryAdapter("") { temporaryClient -> + val empty = assertFailsWith { + temporaryClient.sample(validRequest) + } + assertEquals("backend.response.empty", empty.code) + } + } + + @Test + fun `response identity mismatch is rejected`() { + withTemporaryAdapter( + """ + process.stdout.write(JSON.stringify({ + protocolVersion: 1, + requestId: 'different-request', + status: 'ok', + samples: [] + })) + """.trimIndent(), + ) { temporaryClient -> + val error = assertFailsWith { + temporaryClient.sample(validRequest) + } + assertEquals("backend.response.mismatch", error.code) + } + } + + @Test + fun `large adapter stderr does not block a successful response`() { + withTemporaryAdapter( + """ + const timeout = setTimeout(() => process.exit(2), 1000) + process.stderr.write('x'.repeat(1024 * 1024), () => { + clearTimeout(timeout) + process.stdout.write(JSON.stringify({ + protocolVersion: 1, + requestId: 'valid-request', + status: 'ok', + samples: [[{ kind: 'boolean', value: true }]] + })) + }) + """.trimIndent(), + ) { temporaryClient -> + val response = temporaryClient.sample(validRequest) + + assertEquals( + listOf(listOf(JsConcreteValue.Boolean(true))), + response.samples, + ) + } + } + + private fun assertConforms(values: List, domains: List) { + assertEquals(domains.size, values.size) + values.zip(domains).forEach { (value, domain) -> + when (domain) { + is IntegerDomain -> { + val number = (value as JsConcreteValue.Number).toDouble() + assertTrue(number % 1.0 == 0.0 && number >= domain.min && number <= domain.max) + } + + is ArrayDomain -> { + (value as JsConcreteValue.Array).elements.forEach { element -> + assertConforms(listOf(element), listOf(domain.element)) + } + } + + BooleanDomain -> { + assertTrue(value is JsConcreteValue.Boolean) + } + + else -> { + error("Unexpected test domain: $domain") + } + } + } + } + + private fun withTemporaryAdapter(source: String, block: (FastCheckProjectionClient) -> Unit) { + val script = createTempFile(prefix = "fast-check-adapter-", suffix = ".mjs") + try { + script.writeText(source) + block(FastCheckProjectionClient(adapterEntryPoint = script)) + } finally { + script.deleteIfExists() + } + } + + private companion object { + val validRequest = FastCheckProjectionRequest( + requestId = "valid-request", + seed = 42, + numSamples = 1, + domains = listOf(BooleanDomain), + ) + + fun adapterEntryPoint(): Path { + val candidates = listOf( + Path.of("fast-check-adapter/dist/src/projection-cli.js"), + Path.of("usvm-ts-pbt/fast-check-adapter/dist/src/projection-cli.js"), + ).map { it.absolute() } + return candidates.singleOrNull(Files::isRegularFile) + ?: error("Cannot locate fast-check adapter; checked $candidates") + } + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt new file mode 100644 index 0000000000..20bf0bbbed --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/manifest/PropertyManifestTest.kt @@ -0,0 +1,50 @@ +package org.usvm.ts.pbt.manifest + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.model.IntegerDomain +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 kotlin.test.assertEquals +import kotlin.test.assertFalse + +class PropertyManifestTest { + @Test + fun `manifest round trip contains only engine neutral property data`() { + val definition = PropertyDefinition( + id = PropertyId("math.commutative"), + inputs = listOf( + PropertyInput("left", IntegerDomain(-10, 10)), + PropertyInput("right", IntegerDomain(-10, 10)), + ), + predicate = TypeScriptEntryPoint("properties/math.ts", "isCommutative"), + ) + + val manifest = definition.toManifest() + val encoded = PropertyManifestJson.encode(manifest) + + assertEquals(manifest, PropertyManifestJson.decode(encoded)) + assertFalse("fast-check" in encoded) + assertFalse("backend" in encoded) + assertFalse("seed" in encoded) + } + + @Test + fun `manifest serializes resolved integer bounds and schema version`() { + val definition = PropertyDefinition( + id = PropertyId("integer.defaults"), + inputs = listOf(PropertyInput("value", IntegerDomain())), + predicate = TypeScriptEntryPoint("properties/integer.ts", "holds"), + ) + + val encoded = PropertyManifestJson.encode(definition.toManifest()) + + assertEquals( + """{"schemaVersion":1,"propertyId":"integer.defaults","inputs":[""" + + """{"name":"value","domain":{"kind":"integer","min":-2147483648,"max":2147483647}}],""" + + """"predicate":{"module":"properties/integer.ts","exportName":"holds","executionKind":"sync"}}""", + encoded, + ) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt new file mode 100644 index 0000000000..9186a91931 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt @@ -0,0 +1,47 @@ +package org.usvm.ts.pbt.model + +import kotlinx.serialization.encodeToString +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import kotlin.test.assertEquals + +class JsConcreteValueTest { + @Test + fun `special JavaScript numbers keep their semantics through JSON`() { + val values = listOf( + JsConcreteValue.Number(JsNumber.fromDouble(-0.0)), + JsConcreteValue.Number(JsNumber.fromDouble(Double.NaN)), + JsConcreteValue.Number(JsNumber.fromDouble(Double.POSITIVE_INFINITY)), + JsConcreteValue.Number(JsNumber.fromDouble(Double.NEGATIVE_INFINITY)), + ) + + values.forEach { value -> + val encoded = PropertyManifestJson.json.encodeToString(value) + val decoded = PropertyManifestJson.json.decodeFromString(encoded) + assertEquals(value, decoded) + } + + val negativeZero = values.first() as JsConcreteValue.Number + assertEquals((-0.0).toRawBits(), negativeZero.toDouble().toRawBits()) + } + + @Test + fun `finite JavaScript numbers use sixteen lowercase hexadecimal digits`() { + assertEquals("3ff8000000000000", JsNumber.finite(1.5).bits) + assertEquals("8000000000000000", JsNumber.finite(-0.0).bits) + } + + @Test + fun `recursive arrays keep tagged values through JSON`() { + val value = JsConcreteValue.Array( + listOf( + JsConcreteValue.Undefined, + JsConcreteValue.Array(listOf(JsConcreteValue.Number(JsNumber.finite(-0.0)))), + ), + ) + + val encoded = PropertyManifestJson.json.encodeToString(value) + + assertEquals(value, PropertyManifestJson.json.decodeFromString(encoded)) + } +} diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt new file mode 100644 index 0000000000..b991ef5e72 --- /dev/null +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt @@ -0,0 +1,121 @@ +package org.usvm.ts.pbt.validation + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.manifest.PROPERTY_MANIFEST_SCHEMA_VERSION +import org.usvm.ts.pbt.manifest.PropertyManifest +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.JsNumberKind +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDefinition +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.TypeScriptEntryPoint +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class PropertyValidationTest { + @Test + fun `validation reports independent structural errors in deterministic order`() { + val definition = PropertyDefinition( + id = PropertyId.unchecked(" bad id "), + inputs = listOf( + PropertyInput("value", IntegerDomain(10, -10)), + PropertyInput("value", StringDomain(-1, 0)), + ), + predicate = TypeScriptEntryPoint("../escape.ts", "not-valid-name"), + ) + + val result = validatePropertyDefinition(definition) + + assertFalse(result.isValid) + assertEquals( + listOf( + "domain.integer.bounds", + "input.name.duplicate", + "domain.string.length", + "entrypoint.export.invalid", + "entrypoint.module.invalid", + "property.id.invalid", + ), + result.diagnostics.map { it.code }, + ) + } + + @Test + fun `property ID rejects invalid canonical text at construction`() { + assertFailsWith { PropertyId(" bad id ") } + } + + @Test + fun `optional domain accepts only null or undefined as nil`() { + val definition = validDefinition( + OptionalDomain(IntegerDomain(), JsConcreteValue.String("none")), + ) + + assertEquals( + listOf("domain.optional.nil"), + validatePropertyDefinition(definition).diagnostics.map { it.code }, + ) + } + + @Test + fun `constant domain rejects composite JavaScript values`() { + val definition = validDefinition(ConstantDomain(JsConcreteValue.Array(listOf(JsConcreteValue.Null)))) + + assertEquals( + listOf("domain.constant.unsupported"), + validatePropertyDefinition(definition).diagnostics.map { it.code }, + ) + } + + @Test + fun `invalid number encodings are diagnosed without comparing the bounds`() { + val invalidMinimum = JsNumber(JsNumberKind.FINITE, bits = "invalid") + val definition = validDefinition( + NumberDomain( + min = invalidMinimum, + max = JsNumber.finite(1.0), + allowNaN = false, + ), + ) + + assertEquals( + listOf("js-number.encoding.invalid"), + validatePropertyDefinition(definition).diagnostics.map { it.code }, + ) + } + + @Test + fun `manifest validation rejects unknown schema version`() { + val manifest = PropertyManifest( + schemaVersion = PROPERTY_MANIFEST_SCHEMA_VERSION + 1, + propertyId = "valid.id", + inputs = listOf(PropertyInput("value", IntegerDomain())), + predicate = TypeScriptEntryPoint("properties/value.ts", "holds"), + ) + + assertEquals( + listOf("manifest.schema.unsupported"), + validatePropertyManifest(manifest).diagnostics.map { it.code }, + ) + } + + @Test + fun `valid definition has no diagnostics`() { + assertTrue(validatePropertyDefinition(validDefinition(IntegerDomain(-5, 5))).isValid) + } + + private fun validDefinition(domain: PropertyDomain) = PropertyDefinition( + id = PropertyId("valid.id"), + inputs = listOf(PropertyInput("value", domain)), + predicate = TypeScriptEntryPoint("properties/value.ts", "holds"), + ) +} diff --git a/usvm-ts-pbt/src/test/resources/properties/examples/PropertyExamples.ts b/usvm-ts-pbt/src/test/resources/properties/examples/PropertyExamples.ts new file mode 100644 index 0000000000..06c91b5b9d --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/properties/examples/PropertyExamples.ts @@ -0,0 +1,19 @@ +export function isCommutative(left: number, right: number): boolean { + return left + right === right + left; +} + +export function boundedValueStaysBounded(value: number): boolean { + return value >= -100 && value <= 100; +} + +export function nonZeroDivisor(_dividend: number, divisor: number): boolean { + return divisor !== 0; +} + +export function divisionRoundTrip(dividend: number, divisor: number): boolean { + return (dividend / divisor) * divisor === dividend; +} + +export function reverseTwicePreservesValues(values: number[]): boolean { + return [...values].reverse().reverse().every((value, index) => value === values[index]); +}