From 10fcd6043eda30ca63326a2adadd19a7f3eed732 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 01:26:49 +0300 Subject: [PATCH 1/5] feat(ets): prove isolated Number.isInteger calls --- .../main/kotlin/org/jacodb/ets/dto/Convert.kt | 16 + .../main/kotlin/org/jacodb/ets/dto/Values.kt | 21 + .../main/kotlin/org/jacodb/ets/model/Expr.kt | 18 + .../ets/test/EtsBuiltinCallProofTest.kt | 165 ++++++++ jacodb-ets/ts-frontend/src/dto/values.ts | 21 + .../ts-frontend/src/lowering/builtinProof.ts | 396 ++++++++++++++++++ .../ts-frontend/src/lowering/exprLowering.ts | 20 + .../ts-frontend/src/lowering/methodBuilder.ts | 9 +- .../ts-frontend/test/builtin-proof.spec.ts | 198 +++++++++ 9 files changed, 863 insertions(+), 1 deletion(-) create mode 100644 jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt create mode 100644 jacodb-ets/ts-frontend/src/lowering/builtinProof.ts create mode 100644 jacodb-ets/ts-frontend/test/builtin-proof.spec.ts diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt index 3a7457182..f62d41220 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt @@ -34,6 +34,9 @@ import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsBuiltin +import org.jacodb.ets.model.EtsBuiltinCallProof +import org.jacodb.ets.model.EtsBuiltinEntryRequirement import org.jacodb.ets.model.EtsCallExpr import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsCastExpr @@ -429,12 +432,14 @@ class EtsMethodBuilder( callee = method.toEtsMethodSignature(), args = args.map { ensureLocal(it.toEtsEntity()) }, type = type.toEtsType(), + builtinProof = builtinProof?.toEtsBuiltinCallProof(), ) is StaticCallExprDto -> EtsStaticCallExpr( callee = method.toEtsMethodSignature(), args = args.map { ensureLocal(it.toEtsEntity()) }, type = type.toEtsType(), + builtinProof = builtinProof?.toEtsBuiltinCallProof(), ) is PtrCallExprDto -> EtsPtrCallExpr( @@ -442,6 +447,7 @@ class EtsMethodBuilder( callee = method.toEtsMethodSignature(), args = args.map { ensureLocal(it.toEtsEntity()) }, type = type.toEtsType(), + builtinProof = builtinProof?.toEtsBuiltinCallProof(), ) is ThisRefDto -> EtsThis( @@ -723,6 +729,16 @@ fun MethodSignatureDto.toEtsMethodSignature(): EtsMethodSignature { ) } +private fun BuiltinCallProofDto.toEtsBuiltinCallProof(): EtsBuiltinCallProof = EtsBuiltinCallProof( + builtin = when (builtin) { + ProvenBuiltinDto.NUMBER_IS_INTEGER -> EtsBuiltin.NUMBER_IS_INTEGER + }, + entryRequirement = when (entryRequirement) { + BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY -> EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY + }, + entryMethod = entryMethod.toEtsMethodSignature(), +) + fun LocalSignatureDto.toEtsLocalSignature(): EtsLocalSignature { return EtsLocalSignature( name = name, diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt index c7346bc37..640ebd5f5 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt @@ -240,10 +240,28 @@ data class RelationOperationDto( override val type: TypeDto = UnknownTypeDto, ) : ConditionExprDto +@Serializable +enum class ProvenBuiltinDto { + NUMBER_IS_INTEGER, +} + +@Serializable +enum class BuiltinEntryRequirementDto { + DIRECT_ISOLATED_ENTRY, +} + +@Serializable +data class BuiltinCallProofDto( + val builtin: ProvenBuiltinDto, + val entryRequirement: BuiltinEntryRequirementDto, + val entryMethod: MethodSignatureDto, +) + @Serializable sealed interface CallExprDto : ExprDto { val method: MethodSignatureDto val args: List + val builtinProof: BuiltinCallProofDto? override val type: TypeDto get() = method.returnType @@ -255,6 +273,7 @@ data class InstanceCallExprDto( val instance: ValueDto, // Local override val method: MethodSignatureDto, override val args: List, + override val builtinProof: BuiltinCallProofDto? = null, ) : CallExprDto @Serializable @@ -262,6 +281,7 @@ data class InstanceCallExprDto( data class StaticCallExprDto( override val method: MethodSignatureDto, override val args: List, + override val builtinProof: BuiltinCallProofDto? = null, ) : CallExprDto @Serializable @@ -270,6 +290,7 @@ data class PtrCallExprDto( val ptr: ValueDto, // Local or FieldRef override val method: MethodSignatureDto, override val args: List, + override val builtinProof: BuiltinCallProofDto? = null, ) : CallExprDto @Serializable diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt index c212fb293..88d79e5a7 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt @@ -725,9 +725,24 @@ data class EtsNullishCoalescingExpr( } } +enum class EtsBuiltin { + NUMBER_IS_INTEGER, +} + +enum class EtsBuiltinEntryRequirement { + DIRECT_ISOLATED_ENTRY, +} + +data class EtsBuiltinCallProof( + val builtin: EtsBuiltin, + val entryRequirement: EtsBuiltinEntryRequirement, + val entryMethod: EtsMethodSignature, +) + interface EtsCallExpr : EtsExpr, CommonCallExpr { val callee: EtsMethodSignature override val args: List + val builtinProof: EtsBuiltinCallProof? } data class EtsInstanceCallExpr( @@ -735,6 +750,7 @@ data class EtsInstanceCallExpr( override val callee: EtsMethodSignature, override val args: List, override val type: EtsType, + override val builtinProof: EtsBuiltinCallProof? = null, ) : EtsCallExpr, CommonInstanceCallExpr { override fun toString(): String { return "call ${instance}.${callee.name}(${args.joinToString()})" @@ -749,6 +765,7 @@ data class EtsStaticCallExpr( override val callee: EtsMethodSignature, override val args: List, override val type: EtsType, + override val builtinProof: EtsBuiltinCallProof? = null, ) : EtsCallExpr { override fun toString(): String { return "static_call ${callee.enclosingClass.name}.${callee.name}(${args.joinToString()})" @@ -764,6 +781,7 @@ data class EtsPtrCallExpr( override val callee: EtsMethodSignature, override val args: List, override val type: EtsType, + override val builtinProof: EtsBuiltinCallProof? = null, ) : EtsCallExpr { override fun toString(): String { return "ptr_call ${ptr}(${args.joinToString()})" diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt new file mode 100644 index 000000000..68833f53e --- /dev/null +++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt @@ -0,0 +1,165 @@ +/* + * Copyright 2022 UnitTestBot contributors (utbot.org) + *

+ * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + *

+ * http://www.apache.org/licenses/LICENSE-2.0 + *

+ * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.jacodb.ets.test + +import kotlinx.serialization.SerializationException +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.json.Json +import org.jacodb.ets.dto.BasicBlockDto +import org.jacodb.ets.dto.BodyDto +import org.jacodb.ets.dto.BooleanTypeDto +import org.jacodb.ets.dto.BuiltinCallProofDto +import org.jacodb.ets.dto.BuiltinEntryRequirementDto +import org.jacodb.ets.dto.CallStmtDto +import org.jacodb.ets.dto.CfgDto +import org.jacodb.ets.dto.ClassSignatureDto +import org.jacodb.ets.dto.FileSignatureDto +import org.jacodb.ets.dto.LocalDto +import org.jacodb.ets.dto.MethodDto +import org.jacodb.ets.dto.MethodParameterDto +import org.jacodb.ets.dto.MethodSignatureDto +import org.jacodb.ets.dto.NumberTypeDto +import org.jacodb.ets.dto.ProvenBuiltinDto +import org.jacodb.ets.dto.StaticCallExprDto +import org.jacodb.ets.dto.ValueDto +import org.jacodb.ets.dto.dtoModule +import org.jacodb.ets.dto.toEtsMethod +import org.jacodb.ets.model.EtsBuiltin +import org.jacodb.ets.model.EtsBuiltinEntryRequirement +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsStaticCallExpr +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertNull + +class EtsBuiltinCallProofTest { + private val json = Json { serializersModule = dtoModule } + + @Test + fun `preserves builtin proof from DTO to model`() { + val file = FileSignatureDto(projectName = "project", fileName = "entry.ts") + val owner = ClassSignatureDto(name = "%dflt", declaringFile = file) + val entry = MethodSignatureDto( + declaringClass = owner, + name = "%AM0\$%dflt", + parameters = listOf(MethodParameterDto(name = "value", type = NumberTypeDto)), + returnType = BooleanTypeDto, + ) + val builtin = MethodSignatureDto( + declaringClass = ClassSignatureDto( + name = "Number", + declaringFile = FileSignatureDto(projectName = "%unk", fileName = "%unk"), + ), + name = "isInteger", + parameters = emptyList(), + returnType = BooleanTypeDto, + ) + val argument = LocalDto(name = "value", type = NumberTypeDto) + val call = StaticCallExprDto( + method = builtin, + args = listOf(argument), + builtinProof = BuiltinCallProofDto( + builtin = ProvenBuiltinDto.NUMBER_IS_INTEGER, + entryRequirement = BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY, + entryMethod = entry, + ), + ) + val method = MethodDto( + signature = entry, + modifiers = 0, + decorators = emptyList(), + body = BodyDto( + locals = listOf(argument), + cfg = CfgDto( + blocks = listOf( + BasicBlockDto( + id = 0, + successors = emptyList(), + stmts = listOf(CallStmtDto(expr = call)), + ), + ), + ), + ), + ).toEtsMethod() + + val modelCall = assertIs(assertIs(method.cfg.stmts.single()).expr) + assertEquals(EtsBuiltin.NUMBER_IS_INTEGER, modelCall.builtinProof?.builtin) + assertEquals(EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY, modelCall.builtinProof?.entryRequirement) + assertEquals(method.signature, modelCall.builtinProof?.entryMethod) + } + + @Test + fun `defaults missing proof to absent`() { + val dto = json.decodeFromString( + """ + { + "_": "StaticCallExpr", + "method": { + "declaringClass": { + "name": "Number", + "declaringFile": { "projectName": "%unk", "fileName": "%unk" } + }, + "name": "isInteger", + "parameters": [], + "returnType": { "_": "NumberType" } + }, + "args": [] + } + """.trimIndent(), + ) + + assertNull(assertIs(dto).builtinProof) + } + + @Test + fun `rejects malformed builtin proof`() { + val malformed = """ + { + "_": "StaticCallExpr", + "method": { + "declaringClass": { + "name": "Number", + "declaringFile": { "projectName": "%unk", "fileName": "%unk" } + }, + "name": "isInteger", + "parameters": [], + "returnType": { "_": "NumberType" } + }, + "args": [], + "builtinProof": { + "builtin": "UNKNOWN_BUILTIN", + "entryRequirement": "DIRECT_ISOLATED_ENTRY", + "entryMethod": { + "declaringClass": { + "name": "%dflt", + "declaringFile": { "projectName": "project", "fileName": "entry.ts" } + }, + "name": "%AM0${'$'}%dflt", + "parameters": [], + "returnType": { "_": "NumberType" } + } + } + } + """.trimIndent() + + assertFailsWith { + json.decodeFromString(malformed) + } + } +} diff --git a/jacodb-ets/ts-frontend/src/dto/values.ts b/jacodb-ets/ts-frontend/src/dto/values.ts index dbf136bd3..c90409059 100644 --- a/jacodb-ets/ts-frontend/src/dto/values.ts +++ b/jacodb-ets/ts-frontend/src/dto/values.ts @@ -59,6 +59,24 @@ export type ExprDto = export type CallExprDto = InstanceCallExprDto | StaticCallExprDto | PtrCallExprDto; +/** Builtins whose identity was proven from TypeScript default-library declarations. */ +export type ProvenBuiltinDto = "NUMBER_IS_INTEGER"; + +/** Runtime context required for a frontend proof to remain valid. */ +export type BuiltinEntryRequirementDto = "DIRECT_ISOLATED_ENTRY"; + +/** + * Source-derived proof attached to one call expression. + * + * The entry signature prevents the proof from being reused for a different root; + * runtimes must also enforce the declared entry requirement in their own scene. + */ +export interface BuiltinCallProofDto { + builtin: ProvenBuiltinDto; + entryRequirement: BuiltinEntryRequirementDto; + entryMethod: MethodSignatureDto; +} + export type RefDto = | ThisRefDto | ParameterRefDto @@ -167,12 +185,14 @@ export interface InstanceCallExprDto { instance: LocalDto; // Kotlin Convert casts this to LocalDto — MUST be a Local method: MethodSignatureDto; args: ValueDto[]; + builtinProof?: BuiltinCallProofDto; } export interface StaticCallExprDto { readonly _: "StaticCallExpr"; method: MethodSignatureDto; args: ValueDto[]; + builtinProof?: BuiltinCallProofDto; } export interface PtrCallExprDto { @@ -180,6 +200,7 @@ export interface PtrCallExprDto { ptr: ValueDto; // Local or FieldRef (must be a value, not an expr) method: MethodSignatureDto; args: ValueDto[]; + builtinProof?: BuiltinCallProofDto; } export interface ThisRefDto { diff --git a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts new file mode 100644 index 000000000..18e02a743 --- /dev/null +++ b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts @@ -0,0 +1,396 @@ +/* + * Copyright 2022 UnitTestBot contributors (utbot.org) + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +import * as ts from "typescript"; +import { MethodSignatureDto } from "../dto/signatures"; +import { BuiltinCallProofDto } from "../dto/values"; +import { MethodContext, VerifiedBuiltinEntry } from "./methodBuilder"; + +/** + * Prove the one closed builtin context supported by the first model increment. + * The result remains conditional on direct isolated execution of [entryMethod]. + */ +export function verifiedBuiltinEntryFor( + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + m: MethodContext, + entryMethod: MethodSignatureDto, +): VerifiedBuiltinEntry | undefined { + if (!isExportedTopLevelScalarClosure(closure, m.checker)) return undefined; + if (!hasAdmissibleModuleInitialization(closure.getSourceFile(), m.checker)) return undefined; + if (containsThis(closure.body!)) return undefined; + if (containsNestedFunction(closure)) return undefined; + + const calls = collectNumberIsIntegerCalls(closure, m); + const admittedCalls = calls.filter((call) => hasEffectFreeScalarPrefix(closure, call, m.checker)); + if (admittedCalls.length === 0) return undefined; + + const admittedSet = new Set(admittedCalls); + const receiver = admittedCalls[0].expression.expression; + if (!ts.isIdentifier(receiver)) return undefined; + const numberSymbol = m.converter.symbolOf(receiver); + if (numberSymbol === undefined) return undefined; + const memberSymbols = new Set(); + for (const call of admittedCalls) { + const member = m.converter.symbolOf(call.expression.name); + if (member !== undefined) memberSymbols.add(member); + } + + let unsafeBuiltinUse = false; + visit(closure.body!, (node) => { + if (!ts.isIdentifier(node)) return; + const symbol = m.converter.symbolOf(node); + if (symbol === numberSymbol && !isAdmittedNumberReceiver(node, admittedSet)) { + unsafeBuiltinUse = true; + } + if (symbol !== undefined && memberSymbols.has(symbol) && !isAdmittedNumberMember(node, admittedSet)) { + unsafeBuiltinUse = true; + } + }); + if (unsafeBuiltinUse) return undefined; + + const prunableCaptures = new Set([numberSymbol]); + const errorSymbols = referencedDefaultLibraryErrorSymbols(closure.body!, m); + for (const errorSymbol of errorSymbols) { + if (!isPrunableErrorCapture(errorSymbol, closure.body!, m)) return undefined; + prunableCaptures.add(errorSymbol); + } + + for (const identifier of collectFreeCaptureIdentifiers(closure, m.checker)) { + if (m.moduleFieldForIdentifier(identifier) !== undefined) continue; + const symbol = m.converter.symbolOf(identifier); + if (symbol === undefined || !prunableCaptures.has(symbol)) { + return undefined; + } + } + + const proofs = new Map(); + for (const call of admittedCalls) { + proofs.set(call, { + builtin: "NUMBER_IS_INTEGER", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod, + }); + } + return { calls: proofs, prunableCaptures }; +} + +function isExportedTopLevelScalarClosure( + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + checker: ts.TypeChecker, +): closure is ts.ArrowFunction | ts.FunctionExpression { + if (!ts.isArrowFunction(closure) && !ts.isFunctionExpression(closure)) return false; + const declaration = closure.parent; + if (!ts.isVariableDeclaration(declaration) || declaration.initializer !== closure) return false; + if (!ts.isIdentifier(declaration.name)) return false; + const declarationList = declaration.parent; + if (!ts.isVariableDeclarationList(declarationList) || declarationList.declarations.length !== 1) return false; + if ((declarationList.flags & ts.NodeFlags.Const) === 0) return false; + const statement = declarationList.parent; + if (!ts.isVariableStatement(statement) || !ts.isSourceFile(statement.parent)) return false; + if (!statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword)) return false; + if (closure.parameters.some((parameter) => + !ts.isIdentifier(parameter.name) + || parameter.initializer !== undefined + || parameter.dotDotDotToken !== undefined + || !isPrimitiveScalarType(checker.getTypeAtLocation(parameter.name)))) { + return false; + } + const signature = checker.getSignatureFromDeclaration(closure); + return signature !== undefined && isPrimitiveScalarType(checker.getReturnTypeOfSignature(signature)); +} + +function hasAdmissibleModuleInitialization(sourceFile: ts.SourceFile, checker: ts.TypeChecker): boolean { + return sourceFile.statements.every((statement) => { + if (ts.isEmptyStatement(statement) || ts.isInterfaceDeclaration(statement) || ts.isTypeAliasDeclaration(statement)) { + return true; + } + if (ts.isFunctionDeclaration(statement)) { + return statement.body !== undefined && statement.modifiers?.every((modifier) => + modifier.kind === ts.SyntaxKind.ExportKeyword + || modifier.kind === ts.SyntaxKind.DefaultKeyword + || modifier.kind === ts.SyntaxKind.AsyncKeyword, + ) !== false; + } + if (!ts.isVariableStatement(statement)) return false; + if ((statement.declarationList.flags & ts.NodeFlags.Const) === 0) return false; + return statement.declarationList.declarations.every((declaration) => + ts.isIdentifier(declaration.name) + && declaration.initializer !== undefined + && ( + ts.isArrowFunction(declaration.initializer) + || ts.isFunctionExpression(declaration.initializer) + || isPureScalarExpression(declaration.initializer, checker, ScalarIdentifierPolicy.REJECT) + ), + ); + }); +} + +function collectNumberIsIntegerCalls( + closure: ts.ArrowFunction | ts.FunctionExpression, + m: MethodContext, +): Array { + const calls: Array = []; + const visitBody = (node: ts.Node): void => { + if (node !== closure.body && ts.isFunctionLike(node)) return; + if (isDefaultLibraryNumberIsIntegerCall(node, m)) calls.push(node); + ts.forEachChild(node, visitBody); + }; + visitBody(closure.body); + return calls; +} + +function isDefaultLibraryNumberIsIntegerCall( + node: ts.Node, + m: MethodContext, +): node is ts.CallExpression & { expression: ts.PropertyAccessExpression } { + if (!ts.isCallExpression(node) || node.questionDotToken !== undefined || node.arguments.length !== 1) return false; + const callee = node.expression; + if (!ts.isPropertyAccessExpression(callee) || callee.questionDotToken !== undefined) return false; + if (!ts.isIdentifier(callee.expression) || callee.expression.text !== "Number" || callee.name.text !== "isInteger") { + return false; + } + return isDefaultLibrarySymbol(m.converter.symbolOf(callee.expression), m) + && isDefaultLibrarySymbol(m.converter.symbolOf(callee.name), m) + && isNumberLikeType(m.checker.getTypeAtLocation(node.arguments[0])); +} + +function isDefaultLibrarySymbol(symbol: ts.Symbol | undefined, m: MethodContext): boolean { + const declarations = symbol?.declarations; + return declarations !== undefined + && declarations.length > 0 + && declarations.every((declaration) => m.ctx.isDefaultLibrarySourceFile(declaration.getSourceFile())); +} + +function hasEffectFreeScalarPrefix( + closure: ts.ArrowFunction | ts.FunctionExpression, + call: ts.CallExpression, + checker: ts.TypeChecker, +): boolean { + if (!call.arguments.every((argument) => !ts.isSpreadElement(argument) && isPureScalarExpression(argument, checker))) { + return false; + } + if (!ts.isBlock(closure.body)) return hasPurePrefixWithinExpression(closure.body, call, checker); + + let containingStatement: ts.Node = call; + while (containingStatement.parent !== closure.body) { + containingStatement = containingStatement.parent; + if (ts.isFunctionLike(containingStatement)) return false; + } + const statementIndex = closure.body.statements.findIndex((statement) => statement === containingStatement); + if (statementIndex < 0) return false; + if (!closure.body.statements.slice(0, statementIndex).every((statement) => + isPureScalarPrefixStatement(statement, checker))) return false; + + const statement = closure.body.statements[statementIndex]; + if (ts.isIfStatement(statement)) { + return containsNode(statement.expression, call) + && hasPurePrefixWithinExpression(statement.expression, call, checker); + } + if (ts.isReturnStatement(statement) && statement.expression !== undefined) { + return hasPurePrefixWithinExpression(statement.expression, call, checker); + } + return false; +} + +function isPureScalarPrefixStatement(statement: ts.Statement, checker: ts.TypeChecker): boolean { + if (ts.isEmptyStatement(statement)) return true; + if (!ts.isVariableStatement(statement)) return false; + return statement.declarationList.declarations.every((declaration) => + ts.isIdentifier(declaration.name) + && declaration.initializer !== undefined + && isPrimitiveScalarType(checker.getTypeAtLocation(declaration.name)) + && isPureScalarExpression(declaration.initializer, checker), + ); +} + +function hasPurePrefixWithinExpression(root: ts.Expression, target: ts.CallExpression, checker: ts.TypeChecker): boolean { + if (root === target) return true; + const children: ts.Node[] = []; + ts.forEachChild(root, (child) => { + children.push(child); + }); + for (let index = 0; index < children.length; index++) { + const child = children[index]; + if (!containsNode(child, target)) continue; + const earlierExpressions = children.slice(0, index).filter(ts.isExpression); + return earlierExpressions.every((expression) => isPureScalarExpression(expression, checker)) + && ts.isExpression(child) + && hasPurePrefixWithinExpression(child, target, checker); + } + return false; +} + +enum ScalarIdentifierPolicy { + ALLOW, + REJECT, +} + +function isPureScalarExpression( + node: ts.Expression, + checker: ts.TypeChecker, + identifierPolicy: ScalarIdentifierPolicy = ScalarIdentifierPolicy.ALLOW, +): boolean { + if (!isPrimitiveScalarType(checker.getTypeAtLocation(node))) return false; + if (ts.isIdentifier(node)) return identifierPolicy === ScalarIdentifierPolicy.ALLOW; + if (ts.isNumericLiteral(node) || ts.isStringLiteral(node) + || ts.isNoSubstitutionTemplateLiteral(node) || node.kind === ts.SyntaxKind.TrueKeyword + || node.kind === ts.SyntaxKind.FalseKeyword || node.kind === ts.SyntaxKind.NullKeyword) return true; + if (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || ts.isTypeAssertionExpression(node) + || ts.isNonNullExpression(node) || ts.isSatisfiesExpression(node)) { + return isPureScalarExpression(node.expression, checker, identifierPolicy); + } + if (ts.isPrefixUnaryExpression(node)) { + if (node.operator === ts.SyntaxKind.PlusPlusToken || node.operator === ts.SyntaxKind.MinusMinusToken) { + return false; + } + return isPureScalarExpression(node.operand, checker, identifierPolicy); + } + if (ts.isBinaryExpression(node)) { + const operator = node.operatorToken.kind; + if (isAssignmentOperator(operator) || operator === ts.SyntaxKind.CommaToken) return false; + return isPureScalarExpression(node.left, checker, identifierPolicy) + && isPureScalarExpression(node.right, checker, identifierPolicy); + } + if (ts.isConditionalExpression(node)) { + return isPureScalarExpression(node.condition, checker, identifierPolicy) + && isPureScalarExpression(node.whenTrue, checker, identifierPolicy) + && isPureScalarExpression(node.whenFalse, checker, identifierPolicy); + } + return false; +} + +function isAssignmentOperator(kind: ts.SyntaxKind): boolean { + return kind >= ts.SyntaxKind.FirstAssignment && kind <= ts.SyntaxKind.LastAssignment; +} + +function isPrimitiveScalarType(type: ts.Type): boolean { + if (type.isUnion()) return type.types.every(isPrimitiveScalarType); + const primitive = ts.TypeFlags.NumberLike | ts.TypeFlags.BooleanLike | ts.TypeFlags.StringLike + | ts.TypeFlags.Null | ts.TypeFlags.Undefined; + return (type.flags & primitive) !== 0 + && (type.flags & (ts.TypeFlags.Any | ts.TypeFlags.Unknown | ts.TypeFlags.Intersection)) === 0; +} + +function isNumberLikeType(type: ts.Type): boolean { + if (type.isUnion()) return type.types.every(isNumberLikeType); + return (type.flags & ts.TypeFlags.NumberLike) !== 0 + && (type.flags & (ts.TypeFlags.Any | ts.TypeFlags.Unknown | ts.TypeFlags.Intersection)) === 0; +} + +function containsNode(root: ts.Node, target: ts.Node): boolean { + if (root === target) return true; + let found = false; + ts.forEachChild(root, (child) => { + if (!found && containsNode(child, target)) found = true; + }); + return found; +} + +function visit(root: ts.Node, visitor: (node: ts.Node) => void): void { + visitor(root); + ts.forEachChild(root, (child) => visit(child, visitor)); +} + +function containsThis(root: ts.Node): boolean { + let found = false; + visit(root, (node) => { + if (node.kind === ts.SyntaxKind.ThisKeyword) found = true; + }); + return found; +} + +function containsNestedFunction(closure: ts.ArrowFunction | ts.FunctionExpression): boolean { + let found = false; + ts.forEachChild(closure.body, function visitNested(node): void { + if (ts.isFunctionLike(node)) { + found = true; + return; + } + ts.forEachChild(node, visitNested); + }); + return found; +} + +function isAdmittedNumberReceiver(identifier: ts.Identifier, calls: ReadonlySet): boolean { + const access = identifier.parent; + return ts.isPropertyAccessExpression(access) && access.expression === identifier + && ts.isCallExpression(access.parent) && access.parent.expression === access && calls.has(access.parent); +} + +function isAdmittedNumberMember(identifier: ts.Identifier, calls: ReadonlySet): boolean { + const access = identifier.parent; + return ts.isPropertyAccessExpression(access) && access.name === identifier + && ts.isCallExpression(access.parent) && access.parent.expression === access && calls.has(access.parent); +} + +function referencedDefaultLibraryErrorSymbols(body: ts.ConciseBody, m: MethodContext): Set { + const symbols = new Set(); + visit(body, (node) => { + if (!ts.isIdentifier(node) || node.text !== "Error") return; + const symbol = m.converter.symbolOf(node); + if (symbol !== undefined && isDefaultLibrarySymbol(symbol, m)) symbols.add(symbol); + }); + return symbols; +} + +function isPrunableErrorCapture(symbol: ts.Symbol, body: ts.ConciseBody, m: MethodContext): boolean { + const uses: ts.Identifier[] = []; + visit(body, (node) => { + if (ts.isIdentifier(node) && m.converter.symbolOf(node) === symbol) uses.push(node); + }); + return uses.length > 0 && uses.every((identifier) => + ts.isNewExpression(identifier.parent) && identifier.parent.expression === identifier); +} + +function collectFreeCaptureIdentifiers( + closure: ts.ArrowFunction | ts.FunctionExpression, + checker: ts.TypeChecker, +): ts.Identifier[] { + const ownDeclarations = new Set([closure]); + const collectOwn = (node: ts.Node): void => { + if (isCapturableDeclaration(node)) ownDeclarations.add(node); + ts.forEachChild(node, collectOwn); + }; + closure.parameters.forEach(collectOwn); + collectOwn(closure.body); + + const result = new Map(); + visit(closure.body, (node) => { + if (!ts.isIdentifier(node)) return; + let symbol: ts.Symbol | undefined; + try { + symbol = checker.getSymbolAtLocation(node); + if (ts.isShorthandPropertyAssignment(node.parent) && node.parent.name === node) { + symbol = checker.getShorthandAssignmentValueSymbol(node.parent) ?? symbol; + } + } catch { + return; + } + if (symbol === undefined || result.has(symbol)) return; + const declarations = symbol.declarations?.filter(isCapturableDeclaration); + if (declarations === undefined || declarations.length === 0) return; + if (declarations.some((declaration) => ownDeclarations.has(declaration))) return; + result.set(symbol, node); + }); + return [...result.values()]; +} + +function isCapturableDeclaration(node: ts.Node): node is ts.Declaration { + return ts.isVariableDeclaration(node) + || ts.isParameter(node) + || ts.isBindingElement(node) + || ts.isFunctionDeclaration(node); +} diff --git a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts index a14c3d7aa..8eb9596a5 100644 --- a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts +++ b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts @@ -66,6 +66,7 @@ import { ValueDto, } from "../dto/values"; import { syntaxKindName, unsupportedValue } from "./diagnostics"; +import { verifiedBuiltinEntryFor } from "./builtinProof"; import { MethodContext } from "./methodBuilder"; const RELATION_BY_SYNTAX: Partial> = { @@ -855,6 +856,19 @@ export class ExprLowerer { if (ts.isPropertyAccessExpression(callee)) { const methodName = callee.name.text; + const builtinProof = this.m.verifiedBuiltinEntry?.calls.get(node); + if (builtinProof !== undefined) { + const builtinClass: ClassSignatureDto = { + name: "Number", + declaringFile: UNKNOWN_FILE_SIGNATURE, + }; + return { + _: "StaticCallExpr", + method: this.methodSignatureForCall(node, methodName, builtinClass), + args: this.lowerCallArguments(node), + builtinProof, + }; + } // `this.m()` inside a static method targets a static member of the // current class, just like `C.m()`. if (callee.expression.kind === ts.SyntaxKind.ThisKeyword && this.m.isStaticMethod) { @@ -1136,8 +1150,13 @@ export class ExprLowerer { const { parameters, prologueParams } = buildParameters(this.m.ctx, node); const returnType = returnTypeOf(this.m.ctx, node); const baseSignature: MethodSignatureDto = { declaringClass, name, parameters, returnType }; + const verifiedBuiltinEntry = verifiedBuiltinEntryFor(node, this.m, baseSignature); const captures = collectCapturedIdentifiers(node, this.m.checker) .filter((identifier) => this.m.moduleFieldForIdentifier(identifier) === undefined) + .filter((identifier) => { + const symbol = this.m.converter.symbolOf(identifier); + return symbol === undefined || !verifiedBuiltinEntry?.prunableCaptures.has(symbol); + }) .map((identifier) => this.m.captureForIdentifier(identifier, this.safeTypeOf(identifier))); let signature = baseSignature; @@ -1170,6 +1189,7 @@ export class ExprLowerer { declaringClass, name, ts.isArrowFunction(node) && this.m.isStaticMethod, + verifiedBuiltinEntry, ); if (environment === undefined) { closureContext.emitPrologue(prologueParams); diff --git a/jacodb-ets/ts-frontend/src/lowering/methodBuilder.ts b/jacodb-ets/ts-frontend/src/lowering/methodBuilder.ts index 1e4b2708c..6ba33d5e0 100644 --- a/jacodb-ets/ts-frontend/src/lowering/methodBuilder.ts +++ b/jacodb-ets/ts-frontend/src/lowering/methodBuilder.ts @@ -19,7 +19,7 @@ import { DEFAULT_ARK_CLASS_NAME, FORBIDDEN_LOCAL_PREFIX, TEMP_LOCAL_PREFIX } fro import { BodyDto, ClassDto, LocalDeclDto, MethodDto, SourceSpanDto } from "../dto/model"; import { ClassSignatureDto, FieldSignatureDto, FileSignatureDto } from "../dto/signatures"; import { ClassTypeDto, LexicalEnvTypeDto, TypeDto, UNKNOWN_TYPE } from "../dto/types"; -import { ClosureFieldRefDto, LocalDto, StaticFieldRefDto, ValueDto } from "../dto/values"; +import { BuiltinCallProofDto, ClosureFieldRefDto, LocalDto, StaticFieldRefDto, ValueDto } from "../dto/values"; import { TypeConverter } from "../types/convert"; import { CfgBuilder } from "./cfg"; import { Diagnostics, syntaxKindName } from "./diagnostics"; @@ -57,6 +57,12 @@ export interface ClosureCapture { forwardedFieldName?: string; } +/** Proofs valid only while lowering one verified direct-entry method. */ +export interface VerifiedBuiltinEntry { + calls: ReadonlyMap; + prunableCaptures: ReadonlySet; +} + /** * Per-method lowering state: locals table, temp counter, CFG builder. * @@ -78,6 +84,7 @@ export class MethodContext { readonly methodName: string, /** In static methods `this` refers to the class itself (static field access). */ readonly isStaticMethod: boolean = false, + readonly verifiedBuiltinEntry?: VerifiedBuiltinEntry, ) {} get checker(): ts.TypeChecker { diff --git a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts new file mode 100644 index 000000000..5c6b0508a --- /dev/null +++ b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts @@ -0,0 +1,198 @@ +import { describe, expect, it } from "vitest"; +import { EtsFileDto, MethodDto } from "../src/dto/model"; +import { StaticCallExprDto } from "../src/dto/values"; +import { lower, lowerProject, methodByName } from "./util"; + +function staticCalls(method: MethodDto): StaticCallExprDto[] { + if (method.body === undefined) return []; + return method.body.cfg.blocks + .flatMap((block) => block.stmts) + .flatMap((stmt) => { + if (stmt._ === "AssignStmt" && stmt.right._ === "StaticCallExpr") return [stmt.right]; + if (stmt._ === "CallStmt" && stmt.expr._ === "StaticCallExpr") return [stmt.expr]; + return []; + }); +} + +function numberIsIntegerCall(method: MethodDto): StaticCallExprDto | undefined { + return staticCalls(method).find((call) => call.method.name === "isInteger"); +} + +function hasBuiltinProof(file: EtsFileDto): boolean { + const calls = file.classes + .flatMap((clazz) => clazz.methods) + .flatMap(staticCalls); + return calls.some((call) => call.builtinProof !== undefined); +} + +function expectNoProof(source: string): void { + expect(hasBuiltinProof(lower(source).file)).toBe(false); +} + +describe("verified builtin call proof", () => { + it("proves Number.isInteger for closed exported scalar arrows and prunes builtin captures", () => { + const { file } = lower(` + export const isEven = (num: number): boolean => { + if (!Number.isInteger(num)) throw new Error("integer expected"); + return num % 2 === 0; + }; + export const isOdd = (num: number): boolean => { + if (!Number.isInteger(num)) throw new Error("integer expected"); + return num % 2 !== 0; + }; + export const isLeapYear = (year: number): boolean => { + if (year <= 0 || !Number.isInteger(year)) throw new Error("integer expected"); + return year % 4 === 0 && (year % 100 !== 0 || year % 400 === 0); + }; + `); + + for (const methodName of ["%AM0$%dflt", "%AM1$%dflt", "%AM2$%dflt"]) { + const method = methodByName(file, methodName); + const call = numberIsIntegerCall(method); + + expect(method.signature.parameters).toEqual([ + expect.objectContaining({ type: { _: "NumberType" } }), + ]); + expect(method.body!.locals.some((local) => local.type._ === "LexicalEnvType")).toBe(false); + expect(call).toMatchObject({ + _: "StaticCallExpr", + method: { name: "isInteger", declaringClass: { name: "Number" } }, + builtinProof: { + builtin: "NUMBER_IS_INTEGER", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod: method.signature, + }, + }); + } + }); + + it("keeps proof bound to direct isolated execution when another function calls the entry", () => { + const { file } = lower(` + export const isEven = (num: number): boolean => Number.isInteger(num); + export function caller(num: number): boolean { + return isEven(num); + } + `); + const entry = methodByName(file, "%AM0$%dflt"); + const call = numberIsIntegerCall(entry)!; + + expect(call.builtinProof?.entryRequirement).toBe("DIRECT_ISOLATED_ENTRY"); + expect(call.builtinProof?.entryMethod).toEqual(entry.signature); + }); + + it("declines shadowed, reassigned, aliased, computed, and effectful contexts", () => { + const cases = [ + ` + export const f = ( + Number: { isInteger(value: number): boolean }, + value: number, + ): boolean => Number.isInteger(value); + `, + ` + export const f = (value: number): boolean => { + (Number as any).isInteger = () => true; + return Number.isInteger(value); + }; + `, + ` + export const f = (value: number): boolean => { + Number = {} as NumberConstructor; + return Number.isInteger(value); + }; + `, + ` + export const f = (value: number): boolean => { + const integer = Number.isInteger; + return integer(value); + }; + `, + ` + export const f = (value: number): boolean => { + Number["isInteger"] = () => true; + return Number.isInteger(value); + }; + `, + ` + function mutate(): void { (Number as any).isInteger = () => true; } + export const f = (value: number): boolean => { + mutate(); + return Number.isInteger(value); + }; + `, + ` + declare function unknown(): void; + export const f = (value: number): boolean => { + unknown(); + return Number.isInteger(value); + }; + `, + ` + export const f = (value: number): boolean => Number.isInteger(++value); + `, + ]; + + for (const source of cases) expectNoProof(source); + }); + + it("declines foreign ambient reads during module initialization", () => { + const { file } = lowerProject({ + "ambient.d.ts": "declare var trigger: number;", + "entry.ts": ` + const setup = trigger; + export const f = (input: number): boolean => Number.isInteger(input); + `, + }, "entry.ts"); + + expect(hasBuiltinProof(file)).toBe(false); + }); + + it("declines modules and entries outside the closed direct-entry subset", () => { + const cases = [ + ` + import { value } from "./dependency"; + export const f = (input: number): boolean => Number.isInteger(input); + `, + ` + function sideEffect(): void {} + sideEffect(); + export const f = (input: number): boolean => Number.isInteger(input); + `, + ` + class Holder {} + export const f = (input: number): boolean => Number.isInteger(input); + `, + `const f = (input: number): boolean => Number.isInteger(input);`, + ` + export const outer = (input: number): boolean => { + const nested = (): boolean => Number.isInteger(input); + return nested(); + }; + `, + ` + export const f = (input: number): boolean => { + if (Number.isInteger(input)) { + const makeError = (): Error => new Error("later"); + return makeError() === undefined; + } + return false; + }; + `, + ` + export const f = (input: number): boolean => { + const object = { input }; + return Number.isInteger(object.input); + }; + `, + ]; + + for (const source of cases) expectNoProof(source); + }); + + it("preserves ordinary Number.isInteger lowering when proof is unavailable", () => { + const { file } = lower(`const f = (input: number): boolean => Number.isInteger(input);`); + const method = methodByName(file, "%AM0$%dflt"); + + expect(numberIsIntegerCall(method)).toBeUndefined(); + expect(method.signature.parameters[0].type._).toBe("LexicalEnvType"); + }); +}); From 79711abca3e0d669fb395278f4a4b730b100878e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 01:59:44 +0300 Subject: [PATCH 2/5] refactor(ets): reuse emitted closure captures --- .../ts-frontend/src/lowering/builtinProof.ts | 44 +------------------ .../ts-frontend/src/lowering/exprLowering.ts | 7 +-- 2 files changed, 6 insertions(+), 45 deletions(-) diff --git a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts index 18e02a743..636f37cf5 100644 --- a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts +++ b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts @@ -27,6 +27,7 @@ export function verifiedBuiltinEntryFor( closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, m: MethodContext, entryMethod: MethodSignatureDto, + captures: readonly ts.Identifier[], ): VerifiedBuiltinEntry | undefined { if (!isExportedTopLevelScalarClosure(closure, m.checker)) return undefined; if (!hasAdmissibleModuleInitialization(closure.getSourceFile(), m.checker)) return undefined; @@ -68,8 +69,7 @@ export function verifiedBuiltinEntryFor( prunableCaptures.add(errorSymbol); } - for (const identifier of collectFreeCaptureIdentifiers(closure, m.checker)) { - if (m.moduleFieldForIdentifier(identifier) !== undefined) continue; + for (const identifier of captures) { const symbol = m.converter.symbolOf(identifier); if (symbol === undefined || !prunableCaptures.has(symbol)) { return undefined; @@ -354,43 +354,3 @@ function isPrunableErrorCapture(symbol: ts.Symbol, body: ts.ConciseBody, m: Meth return uses.length > 0 && uses.every((identifier) => ts.isNewExpression(identifier.parent) && identifier.parent.expression === identifier); } - -function collectFreeCaptureIdentifiers( - closure: ts.ArrowFunction | ts.FunctionExpression, - checker: ts.TypeChecker, -): ts.Identifier[] { - const ownDeclarations = new Set([closure]); - const collectOwn = (node: ts.Node): void => { - if (isCapturableDeclaration(node)) ownDeclarations.add(node); - ts.forEachChild(node, collectOwn); - }; - closure.parameters.forEach(collectOwn); - collectOwn(closure.body); - - const result = new Map(); - visit(closure.body, (node) => { - if (!ts.isIdentifier(node)) return; - let symbol: ts.Symbol | undefined; - try { - symbol = checker.getSymbolAtLocation(node); - if (ts.isShorthandPropertyAssignment(node.parent) && node.parent.name === node) { - symbol = checker.getShorthandAssignmentValueSymbol(node.parent) ?? symbol; - } - } catch { - return; - } - if (symbol === undefined || result.has(symbol)) return; - const declarations = symbol.declarations?.filter(isCapturableDeclaration); - if (declarations === undefined || declarations.length === 0) return; - if (declarations.some((declaration) => ownDeclarations.has(declaration))) return; - result.set(symbol, node); - }); - return [...result.values()]; -} - -function isCapturableDeclaration(node: ts.Node): node is ts.Declaration { - return ts.isVariableDeclaration(node) - || ts.isParameter(node) - || ts.isBindingElement(node) - || ts.isFunctionDeclaration(node); -} diff --git a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts index 8eb9596a5..b5e08adde 100644 --- a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts +++ b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts @@ -1150,9 +1150,10 @@ export class ExprLowerer { const { parameters, prologueParams } = buildParameters(this.m.ctx, node); const returnType = returnTypeOf(this.m.ctx, node); const baseSignature: MethodSignatureDto = { declaringClass, name, parameters, returnType }; - const verifiedBuiltinEntry = verifiedBuiltinEntryFor(node, this.m, baseSignature); - const captures = collectCapturedIdentifiers(node, this.m.checker) - .filter((identifier) => this.m.moduleFieldForIdentifier(identifier) === undefined) + const capturedIdentifiers = collectCapturedIdentifiers(node, this.m.checker) + .filter((identifier) => this.m.moduleFieldForIdentifier(identifier) === undefined); + const verifiedBuiltinEntry = verifiedBuiltinEntryFor(node, this.m, baseSignature, capturedIdentifiers); + const captures = capturedIdentifiers .filter((identifier) => { const symbol = this.m.converter.symbolOf(identifier); return symbol === undefined || !verifiedBuiltinEntry?.prunableCaptures.has(symbol); From bbde8e53d58740e4a9144e3d0e6b468475839eaf Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 15:13:02 +0300 Subject: [PATCH 3/5] feat(ets): prove bounded numeric builtin calls --- .../main/kotlin/org/jacodb/ets/dto/Convert.kt | 3 + .../main/kotlin/org/jacodb/ets/dto/Values.kt | 3 + .../main/kotlin/org/jacodb/ets/model/Expr.kt | 3 + .../ets/test/EtsBuiltinCallProofTest.kt | 61 +- jacodb-ets/ts-frontend/src/dto/values.ts | 2 +- .../ts-frontend/src/lowering/builtinProof.ts | 522 +++++++++++++----- .../ts-frontend/src/lowering/classBuilder.ts | 9 +- .../ts-frontend/src/lowering/exprLowering.ts | 2 +- jacodb-ets/ts-frontend/src/types/convert.ts | 3 + .../ts-frontend/test/builtin-proof.spec.ts | 159 +++++- jacodb-ets/ts-frontend/test/types.spec.ts | 5 + 11 files changed, 614 insertions(+), 158 deletions(-) diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt index f62d41220..395635788 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Convert.kt @@ -732,6 +732,9 @@ fun MethodSignatureDto.toEtsMethodSignature(): EtsMethodSignature { private fun BuiltinCallProofDto.toEtsBuiltinCallProof(): EtsBuiltinCallProof = EtsBuiltinCallProof( builtin = when (builtin) { ProvenBuiltinDto.NUMBER_IS_INTEGER -> EtsBuiltin.NUMBER_IS_INTEGER + ProvenBuiltinDto.MATH_ABS -> EtsBuiltin.MATH_ABS + ProvenBuiltinDto.MATH_MIN -> EtsBuiltin.MATH_MIN + ProvenBuiltinDto.MATH_MAX -> EtsBuiltin.MATH_MAX }, entryRequirement = when (entryRequirement) { BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY -> EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt index 640ebd5f5..bc3fdfed2 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt @@ -243,6 +243,9 @@ data class RelationOperationDto( @Serializable enum class ProvenBuiltinDto { NUMBER_IS_INTEGER, + MATH_ABS, + MATH_MIN, + MATH_MAX, } @Serializable diff --git a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt index 88d79e5a7..6cf800e10 100644 --- a/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt +++ b/jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt @@ -727,6 +727,9 @@ data class EtsNullishCoalescingExpr( enum class EtsBuiltin { NUMBER_IS_INTEGER, + MATH_ABS, + MATH_MIN, + MATH_MAX, } enum class EtsBuiltinEntryRequirement { diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt index 68833f53e..f3e5281cc 100644 --- a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt +++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt @@ -71,37 +71,46 @@ class EtsBuiltinCallProofTest { returnType = BooleanTypeDto, ) val argument = LocalDto(name = "value", type = NumberTypeDto) - val call = StaticCallExprDto( - method = builtin, - args = listOf(argument), - builtinProof = BuiltinCallProofDto( - builtin = ProvenBuiltinDto.NUMBER_IS_INTEGER, - entryRequirement = BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY, - entryMethod = entry, - ), + val builtins = listOf( + ProvenBuiltinDto.NUMBER_IS_INTEGER to EtsBuiltin.NUMBER_IS_INTEGER, + ProvenBuiltinDto.MATH_ABS to EtsBuiltin.MATH_ABS, + ProvenBuiltinDto.MATH_MIN to EtsBuiltin.MATH_MIN, + ProvenBuiltinDto.MATH_MAX to EtsBuiltin.MATH_MAX, ) - val method = MethodDto( - signature = entry, - modifiers = 0, - decorators = emptyList(), - body = BodyDto( - locals = listOf(argument), - cfg = CfgDto( - blocks = listOf( - BasicBlockDto( - id = 0, - successors = emptyList(), - stmts = listOf(CallStmtDto(expr = call)), + + for ((dtoBuiltin, expectedBuiltin) in builtins) { + val call = StaticCallExprDto( + method = builtin, + args = listOf(argument), + builtinProof = BuiltinCallProofDto( + builtin = dtoBuiltin, + entryRequirement = BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY, + entryMethod = entry, + ), + ) + val method = MethodDto( + signature = entry, + modifiers = 0, + decorators = emptyList(), + body = BodyDto( + locals = listOf(argument), + cfg = CfgDto( + blocks = listOf( + BasicBlockDto( + id = 0, + successors = emptyList(), + stmts = listOf(CallStmtDto(expr = call)), + ), ), ), ), - ), - ).toEtsMethod() + ).toEtsMethod() - val modelCall = assertIs(assertIs(method.cfg.stmts.single()).expr) - assertEquals(EtsBuiltin.NUMBER_IS_INTEGER, modelCall.builtinProof?.builtin) - assertEquals(EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY, modelCall.builtinProof?.entryRequirement) - assertEquals(method.signature, modelCall.builtinProof?.entryMethod) + val modelCall = assertIs(assertIs(method.cfg.stmts.single()).expr) + assertEquals(expectedBuiltin, modelCall.builtinProof?.builtin) + assertEquals(EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY, modelCall.builtinProof?.entryRequirement) + assertEquals(method.signature, modelCall.builtinProof?.entryMethod) + } } @Test diff --git a/jacodb-ets/ts-frontend/src/dto/values.ts b/jacodb-ets/ts-frontend/src/dto/values.ts index c90409059..640ca2ed2 100644 --- a/jacodb-ets/ts-frontend/src/dto/values.ts +++ b/jacodb-ets/ts-frontend/src/dto/values.ts @@ -60,7 +60,7 @@ export type ExprDto = export type CallExprDto = InstanceCallExprDto | StaticCallExprDto | PtrCallExprDto; /** Builtins whose identity was proven from TypeScript default-library declarations. */ -export type ProvenBuiltinDto = "NUMBER_IS_INTEGER"; +export type ProvenBuiltinDto = "NUMBER_IS_INTEGER" | "MATH_ABS" | "MATH_MIN" | "MATH_MAX"; /** Runtime context required for a frontend proof to remain valid. */ export type BuiltinEntryRequirementDto = "DIRECT_ISOLATED_ENTRY"; diff --git a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts index 636f37cf5..cd30becf5 100644 --- a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts +++ b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts @@ -16,100 +16,157 @@ import * as ts from "typescript"; import { MethodSignatureDto } from "../dto/signatures"; -import { BuiltinCallProofDto } from "../dto/values"; -import { MethodContext, VerifiedBuiltinEntry } from "./methodBuilder"; +import { BuiltinCallProofDto, ProvenBuiltinDto } from "../dto/values"; +import { LoweringContext, VerifiedBuiltinEntry } from "./methodBuilder"; + +interface SupportedBuiltin { + readonly receiverName: "Number" | "Math"; + readonly memberName: "isInteger" | "abs" | "min" | "max"; + readonly arity: number; + readonly builtin: ProvenBuiltinDto; +} + +interface BuiltinCandidate { + readonly call: ts.CallExpression & { expression: ts.PropertyAccessExpression }; + readonly builtin: ProvenBuiltinDto; + readonly receiverSymbol: ts.Symbol; + readonly memberSymbol: ts.Symbol; +} + +const SUPPORTED_BUILTINS: readonly SupportedBuiltin[] = [ + { receiverName: "Number", memberName: "isInteger", arity: 1, builtin: "NUMBER_IS_INTEGER" }, + { receiverName: "Math", memberName: "abs", arity: 1, builtin: "MATH_ABS" }, + { receiverName: "Math", memberName: "min", arity: 2, builtin: "MATH_MIN" }, + { receiverName: "Math", memberName: "max", arity: 2, builtin: "MATH_MAX" }, +]; /** - * Prove the one closed builtin context supported by the first model increment. + * Prove a bounded set of numeric builtins in a closed entry context. * The result remains conditional on direct isolated execution of [entryMethod]. */ export function verifiedBuiltinEntryFor( closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, - m: MethodContext, + ctx: LoweringContext, entryMethod: MethodSignatureDto, captures: readonly ts.Identifier[], ): VerifiedBuiltinEntry | undefined { - if (!isExportedTopLevelScalarClosure(closure, m.checker)) return undefined; - if (!hasAdmissibleModuleInitialization(closure.getSourceFile(), m.checker)) return undefined; + if (!isExportedTopLevelEntry(closure, ctx.checker)) return undefined; + if (!hasAdmissibleModuleInitialization(closure.getSourceFile(), ctx.checker)) return undefined; if (containsThis(closure.body!)) return undefined; if (containsNestedFunction(closure)) return undefined; - const calls = collectNumberIsIntegerCalls(closure, m); - const admittedCalls = calls.filter((call) => hasEffectFreeScalarPrefix(closure, call, m.checker)); - if (admittedCalls.length === 0) return undefined; + const candidates = collectBuiltinCandidates(closure, ctx); + const candidateCalls = new Set(candidates.map(({ call }) => call)); + const admittedCandidates = candidates.filter(({ call }) => + hasEffectFreePrefix(closure, call, ctx, candidateCalls)); + if (admittedCandidates.length === 0) return undefined; - const admittedSet = new Set(admittedCalls); - const receiver = admittedCalls[0].expression.expression; - if (!ts.isIdentifier(receiver)) return undefined; - const numberSymbol = m.converter.symbolOf(receiver); - if (numberSymbol === undefined) return undefined; - const memberSymbols = new Set(); - for (const call of admittedCalls) { - const member = m.converter.symbolOf(call.expression.name); - if (member !== undefined) memberSymbols.add(member); - } - - let unsafeBuiltinUse = false; - visit(closure.body!, (node) => { - if (!ts.isIdentifier(node)) return; - const symbol = m.converter.symbolOf(node); - if (symbol === numberSymbol && !isAdmittedNumberReceiver(node, admittedSet)) { - unsafeBuiltinUse = true; - } - if (symbol !== undefined && memberSymbols.has(symbol) && !isAdmittedNumberMember(node, admittedSet)) { - unsafeBuiltinUse = true; - } - }); - if (unsafeBuiltinUse) return undefined; + const admittedByReceiver = new Map>(); + for (const candidate of admittedCandidates) { + const calls = admittedByReceiver.get(candidate.receiverSymbol) ?? new Set(); + calls.add(candidate.call); + admittedByReceiver.set(candidate.receiverSymbol, calls); + } + + const unsafeReceivers = new Set(); + for (const [receiverSymbol, admittedCalls] of admittedByReceiver) { + visit(closure.body!, (node) => { + if (!ts.isIdentifier(node) || ctx.converter.symbolOf(node) !== receiverSymbol) return; + if (!isAdmittedBuiltinReceiver(node, admittedCalls)) unsafeReceivers.add(receiverSymbol); + }); + } + + const admittedByMember = new Map>(); + for (const candidate of admittedCandidates) { + const calls = admittedByMember.get(candidate.memberSymbol) ?? new Set(); + calls.add(candidate.call); + admittedByMember.set(candidate.memberSymbol, calls); + } + + const unsafeMembers = new Set(); + for (const [memberSymbol, admittedCalls] of admittedByMember) { + visit(closure.body!, (node) => { + if (!ts.isIdentifier(node) || ctx.converter.symbolOf(node) !== memberSymbol) return; + if (!isAdmittedBuiltinMember(node, admittedCalls)) unsafeMembers.add(memberSymbol); + }); + } - const prunableCaptures = new Set([numberSymbol]); - const errorSymbols = referencedDefaultLibraryErrorSymbols(closure.body!, m); + const provenCandidates = admittedCandidates.filter((candidate) => + !unsafeReceivers.has(candidate.receiverSymbol) && !unsafeMembers.has(candidate.memberSymbol)); + if (provenCandidates.length === 0) return undefined; + + const prunableCaptures = new Set(provenCandidates.map(({ receiverSymbol }) => receiverSymbol)); + const errorSymbols = referencedDefaultLibraryErrorSymbols(closure.body!, ctx); for (const errorSymbol of errorSymbols) { - if (!isPrunableErrorCapture(errorSymbol, closure.body!, m)) return undefined; + if (!isPrunableErrorCapture(errorSymbol, closure.body!, ctx)) return undefined; prunableCaptures.add(errorSymbol); } for (const identifier of captures) { - const symbol = m.converter.symbolOf(identifier); + const symbol = ctx.converter.symbolOf(identifier); if (symbol === undefined || !prunableCaptures.has(symbol)) { return undefined; } } - const proofs = new Map(); - for (const call of admittedCalls) { - proofs.set(call, { - builtin: "NUMBER_IS_INTEGER", + const calls = new Map(); + for (const candidate of provenCandidates) { + calls.set(candidate.call, { + builtin: candidate.builtin, entryRequirement: "DIRECT_ISOLATED_ENTRY", entryMethod, }); } - return { calls: proofs, prunableCaptures }; + + return { calls, prunableCaptures }; } -function isExportedTopLevelScalarClosure( +function isExportedTopLevelEntry( closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, checker: ts.TypeChecker, -): closure is ts.ArrowFunction | ts.FunctionExpression { - if (!ts.isArrowFunction(closure) && !ts.isFunctionExpression(closure)) return false; - const declaration = closure.parent; - if (!ts.isVariableDeclaration(declaration) || declaration.initializer !== closure) return false; - if (!ts.isIdentifier(declaration.name)) return false; - const declarationList = declaration.parent; - if (!ts.isVariableDeclarationList(declarationList) || declarationList.declarations.length !== 1) return false; - if ((declarationList.flags & ts.NodeFlags.Const) === 0) return false; - const statement = declarationList.parent; - if (!ts.isVariableStatement(statement) || !ts.isSourceFile(statement.parent)) return false; - if (!statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword)) return false; - if (closure.parameters.some((parameter) => - !ts.isIdentifier(parameter.name) - || parameter.initializer !== undefined - || parameter.dotDotDotToken !== undefined - || !isPrimitiveScalarType(checker.getTypeAtLocation(parameter.name)))) { - return false; +): boolean { + let statement: ts.FunctionDeclaration | ts.VariableStatement; + if (ts.isFunctionDeclaration(closure)) { + if (closure.body === undefined || closure.name === undefined || !ts.isSourceFile(closure.parent)) return false; + statement = closure; + } else { + const declaration = closure.parent; + if (!ts.isVariableDeclaration(declaration) || declaration.initializer !== closure) return false; + if (!ts.isIdentifier(declaration.name)) return false; + + const declarationList = declaration.parent; + if (!ts.isVariableDeclarationList(declarationList) || declarationList.declarations.length !== 1) return false; + if ((declarationList.flags & ts.NodeFlags.Const) === 0) return false; + if (!ts.isVariableStatement(declarationList.parent) || !ts.isSourceFile(declarationList.parent.parent)) return false; + statement = declarationList.parent; } + + if (!statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword)) return false; + if (!closure.parameters.every((parameter) => isAdmissibleEntryParameter(parameter, checker))) return false; + const signature = checker.getSignatureFromDeclaration(closure); - return signature !== undefined && isPrimitiveScalarType(checker.getReturnTypeOfSignature(signature)); + return signature !== undefined && isAdmissibleEntryType(checker.getReturnTypeOfSignature(signature), checker); +} + +function isAdmissibleEntryParameter(parameter: ts.ParameterDeclaration, checker: ts.TypeChecker): boolean { + if (!ts.isIdentifier(parameter.name) || parameter.dotDotDotToken !== undefined) return false; + if (!isAdmissibleEntryType(checker.getTypeAtLocation(parameter.name), checker)) return false; + if (parameter.initializer === undefined) return true; + + return isNumberLikeType(checker.getTypeAtLocation(parameter.initializer)) + && isPureScalarExpression( + parameter.initializer, + checker, + new Set(), + ScalarIdentifierPolicy.REJECT, + ); +} + +function isAdmissibleEntryType(type: ts.Type, checker: ts.TypeChecker): boolean { + if (isPrimitiveScalarType(type) || checker.isArrayType(type) || checker.isTupleType(type)) return true; + + const symbol = type.aliasSymbol ?? type.getSymbol(); + return symbol?.getName() === "ReadonlyArray"; } function hasAdmissibleModuleInitialization(sourceFile: ts.SourceFile, checker: ts.TypeChecker): boolean { @@ -118,7 +175,9 @@ function hasAdmissibleModuleInitialization(sourceFile: ts.SourceFile, checker: t return true; } if (ts.isFunctionDeclaration(statement)) { - return statement.body !== undefined && statement.modifiers?.every((modifier) => + if (statement.body === undefined) return true; + + return statement.modifiers?.every((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword || modifier.kind === ts.SyntaxKind.DefaultKeyword || modifier.kind === ts.SyntaxKind.AsyncKeyword, @@ -126,98 +185,277 @@ function hasAdmissibleModuleInitialization(sourceFile: ts.SourceFile, checker: t } if (!ts.isVariableStatement(statement)) return false; if ((statement.declarationList.flags & ts.NodeFlags.Const) === 0) return false; + return statement.declarationList.declarations.every((declaration) => ts.isIdentifier(declaration.name) && declaration.initializer !== undefined && ( ts.isArrowFunction(declaration.initializer) || ts.isFunctionExpression(declaration.initializer) - || isPureScalarExpression(declaration.initializer, checker, ScalarIdentifierPolicy.REJECT) + || isPureScalarExpression( + declaration.initializer, + checker, + new Set(), + ScalarIdentifierPolicy.REJECT, + ) ), ); }); } -function collectNumberIsIntegerCalls( - closure: ts.ArrowFunction | ts.FunctionExpression, - m: MethodContext, -): Array { - const calls: Array = []; +function collectBuiltinCandidates( + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, +): BuiltinCandidate[] { + const calls: BuiltinCandidate[] = []; const visitBody = (node: ts.Node): void => { if (node !== closure.body && ts.isFunctionLike(node)) return; - if (isDefaultLibraryNumberIsIntegerCall(node, m)) calls.push(node); + + const candidate = builtinCandidateFor(node, ctx); + if (candidate !== undefined) calls.push(candidate); ts.forEachChild(node, visitBody); }; - visitBody(closure.body); + visitBody(closure.body!); + return calls; } -function isDefaultLibraryNumberIsIntegerCall( - node: ts.Node, - m: MethodContext, -): node is ts.CallExpression & { expression: ts.PropertyAccessExpression } { - if (!ts.isCallExpression(node) || node.questionDotToken !== undefined || node.arguments.length !== 1) return false; +function builtinCandidateFor(node: ts.Node, ctx: LoweringContext): BuiltinCandidate | undefined { + if (!ts.isCallExpression(node) || node.questionDotToken !== undefined) return undefined; + const callee = node.expression; - if (!ts.isPropertyAccessExpression(callee) || callee.questionDotToken !== undefined) return false; - if (!ts.isIdentifier(callee.expression) || callee.expression.text !== "Number" || callee.name.text !== "isInteger") { - return false; - } - return isDefaultLibrarySymbol(m.converter.symbolOf(callee.expression), m) - && isDefaultLibrarySymbol(m.converter.symbolOf(callee.name), m) - && isNumberLikeType(m.checker.getTypeAtLocation(node.arguments[0])); + if (!ts.isPropertyAccessExpression(callee) || callee.questionDotToken !== undefined) return undefined; + const receiver = callee.expression; + if (!ts.isIdentifier(receiver)) return undefined; + + const definition = SUPPORTED_BUILTINS.find((candidate) => + candidate.receiverName === receiver.text + && candidate.memberName === callee.name.text + && candidate.arity === node.arguments.length); + if (definition === undefined) return undefined; + if (node.arguments.some(ts.isSpreadElement)) return undefined; + if (!node.arguments.every((argument) => isNumberLikeType(ctx.checker.getTypeAtLocation(argument)))) return undefined; + + const receiverSymbol = ctx.converter.symbolOf(receiver); + const memberSymbol = ctx.converter.symbolOf(callee.name); + if (!isDefaultLibrarySymbol(receiverSymbol, ctx) || !isDefaultLibrarySymbol(memberSymbol, ctx)) return undefined; + + return { + call: node as ts.CallExpression & { expression: ts.PropertyAccessExpression }, + builtin: definition.builtin, + receiverSymbol, + memberSymbol, + }; } -function isDefaultLibrarySymbol(symbol: ts.Symbol | undefined, m: MethodContext): boolean { +function isDefaultLibrarySymbol(symbol: ts.Symbol | undefined, ctx: LoweringContext): symbol is ts.Symbol { const declarations = symbol?.declarations; return declarations !== undefined && declarations.length > 0 - && declarations.every((declaration) => m.ctx.isDefaultLibrarySourceFile(declaration.getSourceFile())); + && declarations.every((declaration) => ctx.isDefaultLibrarySourceFile(declaration.getSourceFile())); } -function hasEffectFreeScalarPrefix( - closure: ts.ArrowFunction | ts.FunctionExpression, +function hasEffectFreePrefix( + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, call: ts.CallExpression, - checker: ts.TypeChecker, + ctx: LoweringContext, + safeCalls: ReadonlySet, ): boolean { - if (!call.arguments.every((argument) => !ts.isSpreadElement(argument) && isPureScalarExpression(argument, checker))) { + if (!call.arguments.every((argument) => + !ts.isSpreadElement(argument) && isPureScalarExpression(argument, ctx.checker, safeCalls))) { return false; } - if (!ts.isBlock(closure.body)) return hasPurePrefixWithinExpression(closure.body, call, checker); + if (!ts.isBlock(closure.body!)) { + return hasPurePrefixWithinExpression(closure.body!, call, ctx.checker, safeCalls); + } + + return hasSafePrefixInStatements(closure.body.statements, call, closure, ctx, safeCalls); +} + +function hasSafePrefixInStatements( + statements: readonly ts.Statement[], + target: ts.CallExpression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { + for (const statement of statements) { + if (containsNode(statement, target)) { + return hasSafePrefixWithinStatement(statement, target, closure, ctx, safeCalls); + } + if (!isSafeCompleteStatement(statement, closure, ctx, safeCalls)) return false; + } + + return false; +} - let containingStatement: ts.Node = call; - while (containingStatement.parent !== closure.body) { - containingStatement = containingStatement.parent; - if (ts.isFunctionLike(containingStatement)) return false; +function hasSafePrefixWithinStatement( + statement: ts.Statement, + target: ts.CallExpression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { + if (ts.isBlock(statement)) { + return hasSafePrefixInStatements(statement.statements, target, closure, ctx, safeCalls); } - const statementIndex = closure.body.statements.findIndex((statement) => statement === containingStatement); - if (statementIndex < 0) return false; - if (!closure.body.statements.slice(0, statementIndex).every((statement) => - isPureScalarPrefixStatement(statement, checker))) return false; + if (ts.isExpressionStatement(statement)) { + return isLocalScalarAssignmentShape(statement.expression, closure, ctx) + && hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + } + if (ts.isVariableStatement(statement)) { + for (const declaration of statement.declarationList.declarations) { + if (declaration.initializer !== undefined && containsNode(declaration.initializer, target)) { + return isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, false) + && hasPurePrefixWithinExpression(declaration.initializer, target, ctx.checker, safeCalls); + } + if (!isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, true)) return false; + } - const statement = closure.body.statements[statementIndex]; + return false; + } if (ts.isIfStatement(statement)) { - return containsNode(statement.expression, call) - && hasPurePrefixWithinExpression(statement.expression, call, checker); + if (containsNode(statement.expression, target)) { + return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + } + if (!isPureScalarExpression(statement.expression, ctx.checker, safeCalls)) return false; + + if (containsNode(statement.thenStatement, target)) { + return (statement.elseStatement === undefined + || isSafeCompleteStatement(statement.elseStatement, closure, ctx, safeCalls)) + && hasSafePrefixWithinStatement(statement.thenStatement, target, closure, ctx, safeCalls); + } + if (statement.elseStatement !== undefined && containsNode(statement.elseStatement, target)) { + return isSafeCompleteStatement(statement.thenStatement, closure, ctx, safeCalls) + && hasSafePrefixWithinStatement(statement.elseStatement, target, closure, ctx, safeCalls); + } + + return false; + } + if (ts.isWhileStatement(statement)) { + return containsNode(statement.statement, target) + && isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + && isSafeCompleteStatement(statement.statement, closure, ctx, safeCalls); } if (ts.isReturnStatement(statement) && statement.expression !== undefined) { - return hasPurePrefixWithinExpression(statement.expression, call, checker); + return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); } + if (ts.isThrowStatement(statement)) { + return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + } + return false; } -function isPureScalarPrefixStatement(statement: ts.Statement, checker: ts.TypeChecker): boolean { +function isSafeCompleteStatement( + statement: ts.Statement, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { if (ts.isEmptyStatement(statement)) return true; - if (!ts.isVariableStatement(statement)) return false; - return statement.declarationList.declarations.every((declaration) => - ts.isIdentifier(declaration.name) - && declaration.initializer !== undefined - && isPrimitiveScalarType(checker.getTypeAtLocation(declaration.name)) - && isPureScalarExpression(declaration.initializer, checker), - ); + if (ts.isBlock(statement)) { + return statement.statements.every((nested) => isSafeCompleteStatement(nested, closure, ctx, safeCalls)); + } + if (ts.isVariableStatement(statement)) { + return statement.declarationList.declarations.every((declaration) => + isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, true)); + } + if (ts.isExpressionStatement(statement)) { + return isSafeLocalScalarAssignment(statement.expression, closure, ctx, safeCalls); + } + if (ts.isIfStatement(statement)) { + return isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + && isSafeCompleteStatement(statement.thenStatement, closure, ctx, safeCalls) + && (statement.elseStatement === undefined + || isSafeCompleteStatement(statement.elseStatement, closure, ctx, safeCalls)); + } + if (ts.isWhileStatement(statement)) { + return isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + && isSafeCompleteStatement(statement.statement, closure, ctx, safeCalls); + } + if (ts.isReturnStatement(statement)) { + return statement.expression === undefined + || isPureScalarExpression(statement.expression, ctx.checker, safeCalls); + } + if (ts.isThrowStatement(statement)) { + return isSafeThrowExpression(statement.expression, ctx, safeCalls); + } + + return false; +} + +function isSafeScalarDeclaration( + declaration: ts.VariableDeclaration, + checker: ts.TypeChecker, + safeCalls: ReadonlySet, + checkInitializer: boolean, +): boolean { + if (!ts.isIdentifier(declaration.name)) return false; + if (!isPrimitiveScalarType(checker.getTypeAtLocation(declaration.name))) return false; + if (!checkInitializer || declaration.initializer === undefined) return true; + + return isPureScalarExpression(declaration.initializer, checker, safeCalls); +} + +function isSafeLocalScalarAssignment( + expression: ts.Expression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { + return isLocalScalarAssignmentShape(expression, closure, ctx) + && ts.isBinaryExpression(expression) + && isPureScalarExpression(expression.right, ctx.checker, safeCalls); +} + +function isLocalScalarAssignmentShape( + expression: ts.Expression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, +): boolean { + if (!ts.isBinaryExpression(expression) || expression.operatorToken.kind !== ts.SyntaxKind.EqualsToken) return false; + if (!ts.isIdentifier(expression.left)) return false; + if (!isPrimitiveScalarType(ctx.checker.getTypeAtLocation(expression.left))) return false; + + const symbol = ctx.converter.symbolOf(expression.left); + return symbol !== undefined && symbol.declarations?.some((declaration) => + declarationBelongsToEntry(declaration, closure)) === true; } -function hasPurePrefixWithinExpression(root: ts.Expression, target: ts.CallExpression, checker: ts.TypeChecker): boolean { +function declarationBelongsToEntry( + declaration: ts.Declaration, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, +): boolean { + for (let current: ts.Node | undefined = declaration; current !== undefined; current = current.parent) { + if (ts.isFunctionLike(current)) return current === closure; + } + + return false; +} + +function isSafeThrowExpression( + expression: ts.Expression, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { + if (isPureScalarExpression(expression, ctx.checker, safeCalls)) return true; + if (!ts.isNewExpression(expression) || !ts.isIdentifier(expression.expression)) return false; + if (expression.expression.text !== "Error") return false; + if (!isDefaultLibrarySymbol(ctx.converter.symbolOf(expression.expression), ctx)) return false; + + return (expression.arguments ?? []).every((argument) => + !ts.isSpreadElement(argument) && isPureScalarExpression(argument, ctx.checker, safeCalls)); +} + +function hasPurePrefixWithinExpression( + root: ts.Expression, + target: ts.CallExpression, + checker: ts.TypeChecker, + safeCalls: ReadonlySet, +): boolean { if (root === target) return true; + const children: ts.Node[] = []; ts.forEachChild(root, (child) => { children.push(child); @@ -225,11 +463,13 @@ function hasPurePrefixWithinExpression(root: ts.Expression, target: ts.CallExpre for (let index = 0; index < children.length; index++) { const child = children[index]; if (!containsNode(child, target)) continue; + const earlierExpressions = children.slice(0, index).filter(ts.isExpression); - return earlierExpressions.every((expression) => isPureScalarExpression(expression, checker)) + return earlierExpressions.every((expression) => isPureScalarExpression(expression, checker, safeCalls)) && ts.isExpression(child) - && hasPurePrefixWithinExpression(child, target, checker); + && hasPurePrefixWithinExpression(child, target, checker, safeCalls); } + return false; } @@ -241,6 +481,7 @@ enum ScalarIdentifierPolicy { function isPureScalarExpression( node: ts.Expression, checker: ts.TypeChecker, + safeCalls: ReadonlySet, identifierPolicy: ScalarIdentifierPolicy = ScalarIdentifierPolicy.ALLOW, ): boolean { if (!isPrimitiveScalarType(checker.getTypeAtLocation(node))) return false; @@ -250,25 +491,34 @@ function isPureScalarExpression( || node.kind === ts.SyntaxKind.FalseKeyword || node.kind === ts.SyntaxKind.NullKeyword) return true; if (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || ts.isTypeAssertionExpression(node) || ts.isNonNullExpression(node) || ts.isSatisfiesExpression(node)) { - return isPureScalarExpression(node.expression, checker, identifierPolicy); + return isPureScalarExpression(node.expression, checker, safeCalls, identifierPolicy); } if (ts.isPrefixUnaryExpression(node)) { if (node.operator === ts.SyntaxKind.PlusPlusToken || node.operator === ts.SyntaxKind.MinusMinusToken) { return false; } - return isPureScalarExpression(node.operand, checker, identifierPolicy); + + return isPureScalarExpression(node.operand, checker, safeCalls, identifierPolicy); } if (ts.isBinaryExpression(node)) { const operator = node.operatorToken.kind; if (isAssignmentOperator(operator) || operator === ts.SyntaxKind.CommaToken) return false; - return isPureScalarExpression(node.left, checker, identifierPolicy) - && isPureScalarExpression(node.right, checker, identifierPolicy); + + return isPureScalarExpression(node.left, checker, safeCalls, identifierPolicy) + && isPureScalarExpression(node.right, checker, safeCalls, identifierPolicy); } if (ts.isConditionalExpression(node)) { - return isPureScalarExpression(node.condition, checker, identifierPolicy) - && isPureScalarExpression(node.whenTrue, checker, identifierPolicy) - && isPureScalarExpression(node.whenFalse, checker, identifierPolicy); + return isPureScalarExpression(node.condition, checker, safeCalls, identifierPolicy) + && isPureScalarExpression(node.whenTrue, checker, safeCalls, identifierPolicy) + && isPureScalarExpression(node.whenFalse, checker, safeCalls, identifierPolicy); + } + if (ts.isCallExpression(node) && safeCalls.has(node)) { + return node.questionDotToken === undefined + && node.arguments.every((argument) => + !ts.isSpreadElement(argument) + && isPureScalarExpression(argument, checker, safeCalls, identifierPolicy)); } + return false; } @@ -278,6 +528,7 @@ function isAssignmentOperator(kind: ts.SyntaxKind): boolean { function isPrimitiveScalarType(type: ts.Type): boolean { if (type.isUnion()) return type.types.every(isPrimitiveScalarType); + const primitive = ts.TypeFlags.NumberLike | ts.TypeFlags.BooleanLike | ts.TypeFlags.StringLike | ts.TypeFlags.Null | ts.TypeFlags.Undefined; return (type.flags & primitive) !== 0 @@ -286,16 +537,19 @@ function isPrimitiveScalarType(type: ts.Type): boolean { function isNumberLikeType(type: ts.Type): boolean { if (type.isUnion()) return type.types.every(isNumberLikeType); + return (type.flags & ts.TypeFlags.NumberLike) !== 0 && (type.flags & (ts.TypeFlags.Any | ts.TypeFlags.Unknown | ts.TypeFlags.Intersection)) === 0; } function containsNode(root: ts.Node, target: ts.Node): boolean { if (root === target) return true; + let found = false; ts.forEachChild(root, (child) => { if (!found && containsNode(child, target)) found = true; }); + return found; } @@ -309,48 +563,62 @@ function containsThis(root: ts.Node): boolean { visit(root, (node) => { if (node.kind === ts.SyntaxKind.ThisKeyword) found = true; }); + return found; } -function containsNestedFunction(closure: ts.ArrowFunction | ts.FunctionExpression): boolean { +function containsNestedFunction( + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, +): boolean { let found = false; - ts.forEachChild(closure.body, function visitNested(node): void { + ts.forEachChild(closure.body!, function visitNested(node): void { if (ts.isFunctionLike(node)) { found = true; return; } + ts.forEachChild(node, visitNested); }); + return found; } -function isAdmittedNumberReceiver(identifier: ts.Identifier, calls: ReadonlySet): boolean { +function isAdmittedBuiltinReceiver( + identifier: ts.Identifier, + calls: ReadonlySet, +): boolean { const access = identifier.parent; return ts.isPropertyAccessExpression(access) && access.expression === identifier && ts.isCallExpression(access.parent) && access.parent.expression === access && calls.has(access.parent); } -function isAdmittedNumberMember(identifier: ts.Identifier, calls: ReadonlySet): boolean { +function isAdmittedBuiltinMember( + identifier: ts.Identifier, + calls: ReadonlySet, +): boolean { const access = identifier.parent; return ts.isPropertyAccessExpression(access) && access.name === identifier && ts.isCallExpression(access.parent) && access.parent.expression === access && calls.has(access.parent); } -function referencedDefaultLibraryErrorSymbols(body: ts.ConciseBody, m: MethodContext): Set { +function referencedDefaultLibraryErrorSymbols(body: ts.ConciseBody, ctx: LoweringContext): Set { const symbols = new Set(); visit(body, (node) => { if (!ts.isIdentifier(node) || node.text !== "Error") return; - const symbol = m.converter.symbolOf(node); - if (symbol !== undefined && isDefaultLibrarySymbol(symbol, m)) symbols.add(symbol); + + const symbol = ctx.converter.symbolOf(node); + if (symbol !== undefined && isDefaultLibrarySymbol(symbol, ctx)) symbols.add(symbol); }); + return symbols; } -function isPrunableErrorCapture(symbol: ts.Symbol, body: ts.ConciseBody, m: MethodContext): boolean { +function isPrunableErrorCapture(symbol: ts.Symbol, body: ts.ConciseBody, ctx: LoweringContext): boolean { const uses: ts.Identifier[] = []; visit(body, (node) => { - if (ts.isIdentifier(node) && m.converter.symbolOf(node) === symbol) uses.push(node); + if (ts.isIdentifier(node) && ctx.converter.symbolOf(node) === symbol) uses.push(node); }); + return uses.length > 0 && uses.every((identifier) => ts.isNewExpression(identifier.parent) && identifier.parent.expression === identifier); } diff --git a/jacodb-ets/ts-frontend/src/lowering/classBuilder.ts b/jacodb-ets/ts-frontend/src/lowering/classBuilder.ts index c6b625ff8..406edc4ad 100644 --- a/jacodb-ets/ts-frontend/src/lowering/classBuilder.ts +++ b/jacodb-ets/ts-frontend/src/lowering/classBuilder.ts @@ -40,6 +40,7 @@ import { ClassDto, FieldDto, MethodDto } from "../dto/model"; import { ClassSignatureDto, UNKNOWN_FILE_SIGNATURE } from "../dto/signatures"; import { ClassTypeDto, TypeDto, BOOLEAN_TYPE, NUMBER_TYPE, STRING_TYPE, UNKNOWN_TYPE, VOID_TYPE } from "../dto/types"; import { buildParameters, decoratorsOf, memberName, modifiersOf, parameterType, returnTypeOf } from "./astUtils"; +import { verifiedBuiltinEntryFor } from "./builtinProof"; import { constant } from "./exprLowering"; import { LoweringContext, MethodContext } from "./methodBuilder"; import { StmtLowerer } from "./stmtLowering"; @@ -298,8 +299,9 @@ export class ClassBuilder { const { parameters, prologueParams } = buildParameters(this.ctx, decl); const returnType = returnTypeOf(this.ctx, decl); + const signature = { declaringClass, name, parameters, returnType }; const method: MethodDto = { - signature: { declaringClass, name, parameters, returnType }, + signature, modifiers: modifiersOf(decl), decorators: decoratorsOf(decl), }; @@ -310,7 +312,10 @@ export class ClassBuilder { if (decl.body !== undefined) { const isStaticMethod = (modifiersOf(decl) & Modifier.STATIC) !== 0; - const m = new MethodContext(this.ctx, declaringClass, name, isStaticMethod); + const builtinEntry = ts.isFunctionDeclaration(decl) + ? verifiedBuiltinEntryFor(decl, this.ctx, signature, []) + : undefined; + const m = new MethodContext(this.ctx, declaringClass, name, isStaticMethod, builtinEntry); m.emitPrologue(prologueParams); const lowerer = new StmtLowerer(m); this.lowerParameterPatterns(lowerer, m, prologueParams); diff --git a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts index b5e08adde..1c2f944bc 100644 --- a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts +++ b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts @@ -1152,7 +1152,7 @@ export class ExprLowerer { const baseSignature: MethodSignatureDto = { declaringClass, name, parameters, returnType }; const capturedIdentifiers = collectCapturedIdentifiers(node, this.m.checker) .filter((identifier) => this.m.moduleFieldForIdentifier(identifier) === undefined); - const verifiedBuiltinEntry = verifiedBuiltinEntryFor(node, this.m, baseSignature, capturedIdentifiers); + const verifiedBuiltinEntry = verifiedBuiltinEntryFor(node, this.m.ctx, baseSignature, capturedIdentifiers); const captures = capturedIdentifiers .filter((identifier) => { const symbol = this.m.converter.symbolOf(identifier); diff --git a/jacodb-ets/ts-frontend/src/types/convert.ts b/jacodb-ets/ts-frontend/src/types/convert.ts index 26309234a..e4d9bec53 100644 --- a/jacodb-ets/ts-frontend/src/types/convert.ts +++ b/jacodb-ets/ts-frontend/src/types/convert.ts @@ -168,6 +168,9 @@ export class TypeConverter { if (ts.isParenthesizedTypeNode(node)) { return this.convertTypeNode(node.type, depth, substitutions); } + if (ts.isTypeOperatorNode(node) && node.operator === ts.SyntaxKind.ReadonlyKeyword) { + return this.convertTypeNode(node.type, depth, substitutions); + } if (ts.isArrayTypeNode(node)) { return foldArray(this.convertTypeNode(node.elementType, depth + 1, substitutions)); } diff --git a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts index 5c6b0508a..bc74630a6 100644 --- a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts +++ b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts @@ -14,8 +14,21 @@ function staticCalls(method: MethodDto): StaticCallExprDto[] { }); } +function builtinCall(method: MethodDto, name: string): StaticCallExprDto | undefined { + return staticCalls(method).find((call) => call.method.name === name); +} + function numberIsIntegerCall(method: MethodDto): StaticCallExprDto | undefined { - return staticCalls(method).find((call) => call.method.name === "isInteger"); + return builtinCall(method, "isInteger"); +} + +function methodWithBodyByName(file: EtsFileDto, name: string): MethodDto { + const method = file.classes + .flatMap((clazz) => clazz.methods) + .find((candidate) => candidate.signature.name === name && candidate.body !== undefined); + if (method === undefined) throw new Error("method '" + name + "' with body not found"); + + return method; } function hasBuiltinProof(file: EtsFileDto): boolean { @@ -188,6 +201,150 @@ describe("verified builtin call proof", () => { for (const source of cases) expectNoProof(source); }); + it("proves the pinned Math.abs loop with a numeric default and scalar backedge", () => { + const { file } = lower(` + export const squareRoot = (num: number, precision: number = 1e-15): number => { + if (num < 0) throw new Error("number must be non-negative number"); + if (num === 0) return 0; + + let sqrt: number = num; + let curr: number; + while (true) { + curr = 0.5 * (sqrt + num / sqrt); + if (Math.abs(curr - sqrt) < precision) { + return sqrt; + } + sqrt = curr; + } + }; + `); + const method = methodByName(file, "%AM0$%dflt"); + const call = builtinCall(method, "abs"); + + expect(method.body!.locals.some((local) => local.type._ === "LexicalEnvType")).toBe(false); + expect(call?.builtinProof).toMatchObject({ + builtin: "MATH_ABS", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod: method.signature, + }); + }); + + it("proves Number.isInteger in the pinned overloaded range declaration", () => { + const { file } = lower(` + export function range(end: number): number[]; + export function range(start: number, end: number): number[]; + export function range(start: number, end: number, step: number): number[]; + export function range(start: number, end?: number, step = 1): number[] { + if (end == null) { + end = start; + start = 0; + } + + if (!Number.isInteger(step) || step === 0) { + throw new Error("The step value must be a non-zero integer."); + } + + const length = Math.max(Math.ceil((end - start) / step), 0); + const result = new Array(length); + for (let i = 0; i < length; i++) { + result[i] = start + i * step; + } + return result; + } + `); + const method = methodWithBodyByName(file, "range"); + + expect(numberIsIntegerCall(method)?.builtinProof).toMatchObject({ + builtin: "NUMBER_IS_INTEGER", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod: method.signature, + }); + expect(builtinCall(method, "max")?.builtinProof).toBeUndefined(); + }); + + it("proves pinned Math.min and Math.max assignments in generic array entries", () => { + const minFile = lower(` + export function dropRight(arr: readonly T[], itemsCount: number): T[] { + itemsCount = Math.min(-itemsCount, 0); + if (itemsCount === 0) { + return arr.slice(); + } + return arr.slice(0, itemsCount); + } + `).file; + const maxFile = lower(` + export function drop(arr: readonly T[], itemsCount: number): T[] { + itemsCount = Math.max(itemsCount, 0); + return arr.slice(itemsCount); + } + `).file; + const minMethod = methodWithBodyByName(minFile, "dropRight"); + const maxMethod = methodWithBodyByName(maxFile, "drop"); + + expect(builtinCall(minMethod, "min")?.builtinProof).toMatchObject({ + builtin: "MATH_MIN", + entryMethod: minMethod.signature, + }); + expect(builtinCall(maxMethod, "max")?.builtinProof).toMatchObject({ + builtin: "MATH_MAX", + entryMethod: maxMethod.signature, + }); + }); + + it("declines unsafe numeric builtin prefixes and identities", () => { + const cases = [ + ` + export const f = (Math: { abs(value: number): number }, value: number): number => + Math.abs(value); + `, + ` + export const f = (value: number): number => { + (Math as any).abs = () => 0; + return Math.abs(value); + }; + `, + ` + declare function unknown(): void; + export const f = (value: number): number => { + unknown(); + return Math.abs(value); + }; + `, + ` + declare function unknown(): number; + export const f = (value: number = unknown()): number => Math.abs(value); + `, + ` + export const f = (object: { value: number }): number => Math.abs(object.value); + `, + ` + export const f = (value: number): number => Math.min(value); + `, + ` + export const f = (value: number): number => Math.abs(value, value); + `, + ` + export const f = (value: number): number => Math.max(value, value, value); + `, + ` + export const f = (value: number): boolean => Number.isInteger(value, value); + `, + ` + declare function unknown(): void; + export const f = (value: number): number => { + let current = value; + while (true) { + if (Math.abs(current) < 1) return current; + unknown(); + current = current / 2; + } + }; + `, + ]; + + for (const source of cases) expectNoProof(source); + }); + it("preserves ordinary Number.isInteger lowering when proof is unavailable", () => { const { file } = lower(`const f = (input: number): boolean => Number.isInteger(input);`); const method = methodByName(file, "%AM0$%dflt"); diff --git a/jacodb-ets/ts-frontend/test/types.spec.ts b/jacodb-ets/ts-frontend/test/types.spec.ts index 0218d548f..7fa7546e3 100644 --- a/jacodb-ets/ts-frontend/test/types.spec.ts +++ b/jacodb-ets/ts-frontend/test/types.spec.ts @@ -74,6 +74,11 @@ describe("convertTypeNode (annotations)", () => { elementType: { _: "NumberType" }, dimensions: 1, }); + expect(annotationOf("let x: readonly number[];")).toEqual({ + _: "ArrayType", + elementType: { _: "NumberType" }, + dimensions: 1, + }); }); it("converts tuples", () => { From bee49552b838a91c36f618974f13729f0b8e69f6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 15:38:55 +0300 Subject: [PATCH 4/5] fix(ets): validate numeric builtin proof context --- .../ets/test/EtsBuiltinCallProofTest.kt | 58 ++++++-- .../ts-frontend/src/lowering/builtinProof.ts | 140 +++++++++++++----- .../ts-frontend/src/lowering/exprLowering.ts | 6 +- .../ts-frontend/test/builtin-proof.spec.ts | 129 ++++++++++++++-- 4 files changed, 269 insertions(+), 64 deletions(-) diff --git a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt index f3e5281cc..b14aeefa0 100644 --- a/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt +++ b/jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt @@ -61,29 +61,56 @@ class EtsBuiltinCallProofTest { parameters = listOf(MethodParameterDto(name = "value", type = NumberTypeDto)), returnType = BooleanTypeDto, ) - val builtin = MethodSignatureDto( - declaringClass = ClassSignatureDto( - name = "Number", - declaringFile = FileSignatureDto(projectName = "%unk", fileName = "%unk"), - ), - name = "isInteger", - parameters = emptyList(), - returnType = BooleanTypeDto, + data class BuiltinCase( + val dtoBuiltin: ProvenBuiltinDto, + val expectedBuiltin: EtsBuiltin, + val ownerName: String, + val methodName: String, ) + val argument = LocalDto(name = "value", type = NumberTypeDto) val builtins = listOf( - ProvenBuiltinDto.NUMBER_IS_INTEGER to EtsBuiltin.NUMBER_IS_INTEGER, - ProvenBuiltinDto.MATH_ABS to EtsBuiltin.MATH_ABS, - ProvenBuiltinDto.MATH_MIN to EtsBuiltin.MATH_MIN, - ProvenBuiltinDto.MATH_MAX to EtsBuiltin.MATH_MAX, + BuiltinCase( + dtoBuiltin = ProvenBuiltinDto.NUMBER_IS_INTEGER, + expectedBuiltin = EtsBuiltin.NUMBER_IS_INTEGER, + ownerName = "Number", + methodName = "isInteger", + ), + BuiltinCase( + dtoBuiltin = ProvenBuiltinDto.MATH_ABS, + expectedBuiltin = EtsBuiltin.MATH_ABS, + ownerName = "Math", + methodName = "abs", + ), + BuiltinCase( + dtoBuiltin = ProvenBuiltinDto.MATH_MIN, + expectedBuiltin = EtsBuiltin.MATH_MIN, + ownerName = "Math", + methodName = "min", + ), + BuiltinCase( + dtoBuiltin = ProvenBuiltinDto.MATH_MAX, + expectedBuiltin = EtsBuiltin.MATH_MAX, + ownerName = "Math", + methodName = "max", + ), ) - for ((dtoBuiltin, expectedBuiltin) in builtins) { + for (builtinCase in builtins) { + val builtin = MethodSignatureDto( + declaringClass = ClassSignatureDto( + name = builtinCase.ownerName, + declaringFile = FileSignatureDto(projectName = "%unk", fileName = "%unk"), + ), + name = builtinCase.methodName, + parameters = emptyList(), + returnType = BooleanTypeDto, + ) val call = StaticCallExprDto( method = builtin, args = listOf(argument), builtinProof = BuiltinCallProofDto( - builtin = dtoBuiltin, + builtin = builtinCase.dtoBuiltin, entryRequirement = BuiltinEntryRequirementDto.DIRECT_ISOLATED_ENTRY, entryMethod = entry, ), @@ -107,7 +134,8 @@ class EtsBuiltinCallProofTest { ).toEtsMethod() val modelCall = assertIs(assertIs(method.cfg.stmts.single()).expr) - assertEquals(expectedBuiltin, modelCall.builtinProof?.builtin) + assertEquals(builtinCase.ownerName, modelCall.callee.enclosingClass.name) + assertEquals(builtinCase.expectedBuiltin, modelCall.builtinProof?.builtin) assertEquals(EtsBuiltinEntryRequirement.DIRECT_ISOLATED_ENTRY, modelCall.builtinProof?.entryRequirement) assertEquals(method.signature, modelCall.builtinProof?.entryMethod) } diff --git a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts index cd30becf5..2fd68517b 100644 --- a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts +++ b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts @@ -262,11 +262,12 @@ function hasEffectFreePrefix( safeCalls: ReadonlySet, ): boolean { if (!call.arguments.every((argument) => - !ts.isSpreadElement(argument) && isPureScalarExpression(argument, ctx.checker, safeCalls))) { + !ts.isSpreadElement(argument) + && isPureEntryScalarExpression(argument, closure, ctx, safeCalls))) { return false; } if (!ts.isBlock(closure.body!)) { - return hasPurePrefixWithinExpression(closure.body!, call, ctx.checker, safeCalls); + return hasPurePrefixWithinExpression(closure.body!, call, closure, ctx, safeCalls); } return hasSafePrefixInStatements(closure.body.statements, call, closure, ctx, safeCalls); @@ -301,24 +302,24 @@ function hasSafePrefixWithinStatement( } if (ts.isExpressionStatement(statement)) { return isLocalScalarAssignmentShape(statement.expression, closure, ctx) - && hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + && hasPurePrefixWithinExpression(statement.expression, target, closure, ctx, safeCalls); } if (ts.isVariableStatement(statement)) { for (const declaration of statement.declarationList.declarations) { if (declaration.initializer !== undefined && containsNode(declaration.initializer, target)) { - return isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, false) - && hasPurePrefixWithinExpression(declaration.initializer, target, ctx.checker, safeCalls); + return isSafeScalarDeclaration(declaration, closure, ctx, safeCalls, false) + && hasPurePrefixWithinExpression(declaration.initializer, target, closure, ctx, safeCalls); } - if (!isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, true)) return false; + if (!isSafeScalarDeclaration(declaration, closure, ctx, safeCalls, true)) return false; } return false; } if (ts.isIfStatement(statement)) { if (containsNode(statement.expression, target)) { - return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + return hasPurePrefixWithinExpression(statement.expression, target, closure, ctx, safeCalls); } - if (!isPureScalarExpression(statement.expression, ctx.checker, safeCalls)) return false; + if (!isPureEntryScalarExpression(statement.expression, closure, ctx, safeCalls)) return false; if (containsNode(statement.thenStatement, target)) { return (statement.elseStatement === undefined @@ -334,14 +335,14 @@ function hasSafePrefixWithinStatement( } if (ts.isWhileStatement(statement)) { return containsNode(statement.statement, target) - && isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + && isPureEntryScalarExpression(statement.expression, closure, ctx, safeCalls) && isSafeCompleteStatement(statement.statement, closure, ctx, safeCalls); } if (ts.isReturnStatement(statement) && statement.expression !== undefined) { - return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + return hasPurePrefixWithinExpression(statement.expression, target, closure, ctx, safeCalls); } if (ts.isThrowStatement(statement)) { - return hasPurePrefixWithinExpression(statement.expression, target, ctx.checker, safeCalls); + return hasPurePrefixWithinExpression(statement.expression, target, closure, ctx, safeCalls); } return false; @@ -359,27 +360,27 @@ function isSafeCompleteStatement( } if (ts.isVariableStatement(statement)) { return statement.declarationList.declarations.every((declaration) => - isSafeScalarDeclaration(declaration, ctx.checker, safeCalls, true)); + isSafeScalarDeclaration(declaration, closure, ctx, safeCalls, true)); } if (ts.isExpressionStatement(statement)) { return isSafeLocalScalarAssignment(statement.expression, closure, ctx, safeCalls); } if (ts.isIfStatement(statement)) { - return isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + return isPureEntryScalarExpression(statement.expression, closure, ctx, safeCalls) && isSafeCompleteStatement(statement.thenStatement, closure, ctx, safeCalls) && (statement.elseStatement === undefined || isSafeCompleteStatement(statement.elseStatement, closure, ctx, safeCalls)); } if (ts.isWhileStatement(statement)) { - return isPureScalarExpression(statement.expression, ctx.checker, safeCalls) + return isPureEntryScalarExpression(statement.expression, closure, ctx, safeCalls) && isSafeCompleteStatement(statement.statement, closure, ctx, safeCalls); } if (ts.isReturnStatement(statement)) { return statement.expression === undefined - || isPureScalarExpression(statement.expression, ctx.checker, safeCalls); + || isPureEntryScalarExpression(statement.expression, closure, ctx, safeCalls); } if (ts.isThrowStatement(statement)) { - return isSafeThrowExpression(statement.expression, ctx, safeCalls); + return isSafeThrowExpression(statement.expression, closure, ctx, safeCalls); } return false; @@ -387,15 +388,16 @@ function isSafeCompleteStatement( function isSafeScalarDeclaration( declaration: ts.VariableDeclaration, - checker: ts.TypeChecker, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, safeCalls: ReadonlySet, checkInitializer: boolean, ): boolean { if (!ts.isIdentifier(declaration.name)) return false; - if (!isPrimitiveScalarType(checker.getTypeAtLocation(declaration.name))) return false; + if (!isPrimitiveScalarType(ctx.checker.getTypeAtLocation(declaration.name))) return false; if (!checkInitializer || declaration.initializer === undefined) return true; - return isPureScalarExpression(declaration.initializer, checker, safeCalls); + return isPureEntryScalarExpression(declaration.initializer, closure, ctx, safeCalls); } function isSafeLocalScalarAssignment( @@ -406,7 +408,7 @@ function isSafeLocalScalarAssignment( ): boolean { return isLocalScalarAssignmentShape(expression, closure, ctx) && ts.isBinaryExpression(expression) - && isPureScalarExpression(expression.right, ctx.checker, safeCalls); + && isPureEntryScalarExpression(expression.right, closure, ctx, safeCalls); } function isLocalScalarAssignmentShape( @@ -436,22 +438,25 @@ function declarationBelongsToEntry( function isSafeThrowExpression( expression: ts.Expression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, ctx: LoweringContext, safeCalls: ReadonlySet, ): boolean { - if (isPureScalarExpression(expression, ctx.checker, safeCalls)) return true; + if (isPureEntryScalarExpression(expression, closure, ctx, safeCalls)) return true; if (!ts.isNewExpression(expression) || !ts.isIdentifier(expression.expression)) return false; if (expression.expression.text !== "Error") return false; if (!isDefaultLibrarySymbol(ctx.converter.symbolOf(expression.expression), ctx)) return false; return (expression.arguments ?? []).every((argument) => - !ts.isSpreadElement(argument) && isPureScalarExpression(argument, ctx.checker, safeCalls)); + !ts.isSpreadElement(argument) + && isPureEntryScalarExpression(argument, closure, ctx, safeCalls)); } function hasPurePrefixWithinExpression( root: ts.Expression, target: ts.CallExpression, - checker: ts.TypeChecker, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, safeCalls: ReadonlySet, ): boolean { if (root === target) return true; @@ -465,9 +470,10 @@ function hasPurePrefixWithinExpression( if (!containsNode(child, target)) continue; const earlierExpressions = children.slice(0, index).filter(ts.isExpression); - return earlierExpressions.every((expression) => isPureScalarExpression(expression, checker, safeCalls)) + return earlierExpressions.every((expression) => + isPureEntryScalarExpression(expression, closure, ctx, safeCalls)) && ts.isExpression(child) - && hasPurePrefixWithinExpression(child, target, checker, safeCalls); + && hasPurePrefixWithinExpression(child, target, closure, ctx, safeCalls); } return false; @@ -478,45 +484,111 @@ enum ScalarIdentifierPolicy { REJECT, } +function isPureEntryScalarExpression( + node: ts.Expression, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, + safeCalls: ReadonlySet, +): boolean { + return isPureScalarExpression( + node, + ctx.checker, + safeCalls, + ScalarIdentifierPolicy.ALLOW, + (identifier) => isSafeEntryScalarIdentifier(identifier, closure, ctx), + ); +} + +function isSafeEntryScalarIdentifier( + identifier: ts.Identifier, + closure: ts.ArrowFunction | ts.FunctionExpression | ts.FunctionDeclaration, + ctx: LoweringContext, +): boolean { + const symbol = ctx.converter.symbolOf(identifier); + if (symbol === undefined) return false; + if (symbol.declarations?.some((declaration) => declarationBelongsToEntry(declaration, closure)) === true) { + return true; + } + if ((identifier.text === "Infinity" || identifier.text === "NaN") + && isDefaultLibrarySymbol(symbol, ctx)) { + return true; + } + + return isSafeModuleScalarBinding(symbol, closure.getSourceFile(), ctx); +} + +function isSafeModuleScalarBinding( + symbol: ts.Symbol, + sourceFile: ts.SourceFile, + ctx: LoweringContext, +): boolean { + const declarations = symbol.declarations; + if (declarations?.length !== 1) return false; + + const declaration = declarations[0]; + if (!ts.isVariableDeclaration(declaration) || !ts.isIdentifier(declaration.name)) return false; + if (declaration.getSourceFile() !== sourceFile || declaration.initializer === undefined) return false; + if (!isPrimitiveScalarType(ctx.checker.getTypeAtLocation(declaration.name))) return false; + + const declarationList = declaration.parent; + if (!ts.isVariableDeclarationList(declarationList) + || (declarationList.flags & ts.NodeFlags.Const) === 0) { + return false; + } + const statement = declarationList.parent; + if (!ts.isVariableStatement(statement) || !ts.isSourceFile(statement.parent)) return false; + + return isPureScalarExpression( + declaration.initializer, + ctx.checker, + new Set(), + ScalarIdentifierPolicy.REJECT, + ); +} + function isPureScalarExpression( node: ts.Expression, checker: ts.TypeChecker, safeCalls: ReadonlySet, identifierPolicy: ScalarIdentifierPolicy = ScalarIdentifierPolicy.ALLOW, + identifierGuard?: (identifier: ts.Identifier) => boolean, ): boolean { if (!isPrimitiveScalarType(checker.getTypeAtLocation(node))) return false; - if (ts.isIdentifier(node)) return identifierPolicy === ScalarIdentifierPolicy.ALLOW; + if (ts.isIdentifier(node)) { + return identifierPolicy === ScalarIdentifierPolicy.ALLOW + && (identifierGuard === undefined || identifierGuard(node)); + } if (ts.isNumericLiteral(node) || ts.isStringLiteral(node) || ts.isNoSubstitutionTemplateLiteral(node) || node.kind === ts.SyntaxKind.TrueKeyword || node.kind === ts.SyntaxKind.FalseKeyword || node.kind === ts.SyntaxKind.NullKeyword) return true; if (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || ts.isTypeAssertionExpression(node) || ts.isNonNullExpression(node) || ts.isSatisfiesExpression(node)) { - return isPureScalarExpression(node.expression, checker, safeCalls, identifierPolicy); + return isPureScalarExpression(node.expression, checker, safeCalls, identifierPolicy, identifierGuard); } if (ts.isPrefixUnaryExpression(node)) { if (node.operator === ts.SyntaxKind.PlusPlusToken || node.operator === ts.SyntaxKind.MinusMinusToken) { return false; } - return isPureScalarExpression(node.operand, checker, safeCalls, identifierPolicy); + return isPureScalarExpression(node.operand, checker, safeCalls, identifierPolicy, identifierGuard); } if (ts.isBinaryExpression(node)) { const operator = node.operatorToken.kind; if (isAssignmentOperator(operator) || operator === ts.SyntaxKind.CommaToken) return false; - return isPureScalarExpression(node.left, checker, safeCalls, identifierPolicy) - && isPureScalarExpression(node.right, checker, safeCalls, identifierPolicy); + return isPureScalarExpression(node.left, checker, safeCalls, identifierPolicy, identifierGuard) + && isPureScalarExpression(node.right, checker, safeCalls, identifierPolicy, identifierGuard); } if (ts.isConditionalExpression(node)) { - return isPureScalarExpression(node.condition, checker, safeCalls, identifierPolicy) - && isPureScalarExpression(node.whenTrue, checker, safeCalls, identifierPolicy) - && isPureScalarExpression(node.whenFalse, checker, safeCalls, identifierPolicy); + return isPureScalarExpression(node.condition, checker, safeCalls, identifierPolicy, identifierGuard) + && isPureScalarExpression(node.whenTrue, checker, safeCalls, identifierPolicy, identifierGuard) + && isPureScalarExpression(node.whenFalse, checker, safeCalls, identifierPolicy, identifierGuard); } if (ts.isCallExpression(node) && safeCalls.has(node)) { return node.questionDotToken === undefined && node.arguments.every((argument) => !ts.isSpreadElement(argument) - && isPureScalarExpression(argument, checker, safeCalls, identifierPolicy)); + && isPureScalarExpression(argument, checker, safeCalls, identifierPolicy, identifierGuard)); } return false; diff --git a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts index 1c2f944bc..d17065ef5 100644 --- a/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts +++ b/jacodb-ets/ts-frontend/src/lowering/exprLowering.ts @@ -858,8 +858,12 @@ export class ExprLowerer { const methodName = callee.name.text; const builtinProof = this.m.verifiedBuiltinEntry?.calls.get(node); if (builtinProof !== undefined) { + const builtinReceiver = callee.expression; + if (!ts.isIdentifier(builtinReceiver)) { + throw new LoweringError("proven builtin without an identifier receiver"); + } const builtinClass: ClassSignatureDto = { - name: "Number", + name: builtinReceiver.text, declaringFile: UNKNOWN_FILE_SIGNATURE, }; return { diff --git a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts index bc74630a6..6acafb2c6 100644 --- a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts +++ b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts @@ -42,6 +42,15 @@ function expectNoProof(source: string): void { expect(hasBuiltinProof(lower(source).file)).toBe(false); } +function expectNoAmbientProjectProof(entrySource: string): void { + const { file } = lowerProject({ + "ambient.d.ts": "declare var trigger: number;", + "entry.ts": entrySource, + }, "entry.ts"); + + expect(hasBuiltinProof(file)).toBe(false); +} + describe("verified builtin call proof", () => { it("proves Number.isInteger for closed exported scalar arrows and prunes builtin captures", () => { const { file } = lower(` @@ -222,10 +231,13 @@ describe("verified builtin call proof", () => { const call = builtinCall(method, "abs"); expect(method.body!.locals.some((local) => local.type._ === "LexicalEnvType")).toBe(false); - expect(call?.builtinProof).toMatchObject({ - builtin: "MATH_ABS", - entryRequirement: "DIRECT_ISOLATED_ENTRY", - entryMethod: method.signature, + expect(call).toMatchObject({ + method: { declaringClass: { name: "Math" } }, + builtinProof: { + builtin: "MATH_ABS", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod: method.signature, + }, }); }); @@ -254,10 +266,13 @@ describe("verified builtin call proof", () => { `); const method = methodWithBodyByName(file, "range"); - expect(numberIsIntegerCall(method)?.builtinProof).toMatchObject({ - builtin: "NUMBER_IS_INTEGER", - entryRequirement: "DIRECT_ISOLATED_ENTRY", - entryMethod: method.signature, + expect(numberIsIntegerCall(method)).toMatchObject({ + method: { declaringClass: { name: "Number" } }, + builtinProof: { + builtin: "NUMBER_IS_INTEGER", + entryRequirement: "DIRECT_ISOLATED_ENTRY", + entryMethod: method.signature, + }, }); expect(builtinCall(method, "max")?.builtinProof).toBeUndefined(); }); @@ -281,16 +296,102 @@ describe("verified builtin call proof", () => { const minMethod = methodWithBodyByName(minFile, "dropRight"); const maxMethod = methodWithBodyByName(maxFile, "drop"); - expect(builtinCall(minMethod, "min")?.builtinProof).toMatchObject({ - builtin: "MATH_MIN", - entryMethod: minMethod.signature, + expect(builtinCall(minMethod, "min")).toMatchObject({ + method: { declaringClass: { name: "Math" } }, + builtinProof: { + builtin: "MATH_MIN", + entryMethod: minMethod.signature, + }, }); - expect(builtinCall(maxMethod, "max")?.builtinProof).toMatchObject({ - builtin: "MATH_MAX", - entryMethod: maxMethod.signature, + expect(builtinCall(maxMethod, "max")).toMatchObject({ + method: { declaringClass: { name: "Math" } }, + builtinProof: { + builtin: "MATH_MAX", + entryMethod: maxMethod.signature, + }, }); }); + it("admits only entry locals and verified module scalars in evaluated prefixes", () => { + const { file } = lower(` + const offset = 1; + export function named(value: number): number { + const adjusted = value + offset; + return Math.abs(adjusted); + } + export const arrow = (value: number): number => { + const adjusted = value + offset; + return Math.abs(adjusted); + }; + `); + const named = methodWithBodyByName(file, "named"); + const arrow = methodByName(file, "%AM0$%dflt"); + + for (const method of [named, arrow]) { + expect(builtinCall(method, "abs")).toMatchObject({ + method: { declaringClass: { name: "Math" } }, + builtinProof: { + builtin: "MATH_ABS", + entryMethod: method.signature, + }, + }); + } + }); + + it("declines ambient scalar reads for declarations and arrows at every evaluated site", () => { + const entryPairs = [ + [ + ` + export function f(value: number): number { + const ignored = trigger; + return Math.abs(value); + } + `, + ` + export const f = (value: number): number => { + const ignored = trigger; + return Math.abs(value); + }; + `, + ], + [ + ` + export function f(value: number): number { + return Math.abs(value + trigger); + } + `, + ` + export const f = (value: number): number => Math.abs(value + trigger); + `, + ], + [ + ` + export function f(value: number): number { + let current = value; + while (true) { + if (Math.abs(current) < 1) return current; + current = trigger; + } + } + `, + ` + export const f = (value: number): number => { + let current = value; + while (true) { + if (Math.abs(current) < 1) return current; + current = trigger; + } + }; + `, + ], + ]; + + for (const [declaration, arrow] of entryPairs) { + expectNoAmbientProjectProof(declaration); + expectNoAmbientProjectProof(arrow); + } + }); + it("declines unsafe numeric builtin prefixes and identities", () => { const cases = [ ` From 35f248b25ff60563bd8fa6877e05c93cbc3dd442 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 15:51:51 +0300 Subject: [PATCH 5/5] fix(ets): preserve proofs across intrinsic undefined guards --- .../ts-frontend/src/lowering/builtinProof.ts | 14 +++++++ .../ts-frontend/test/builtin-proof.spec.ts | 39 +++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts index 2fd68517b..6b5e7c995 100644 --- a/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts +++ b/jacodb-ets/ts-frontend/src/lowering/builtinProof.ts @@ -509,6 +509,7 @@ function isSafeEntryScalarIdentifier( if (symbol.declarations?.some((declaration) => declarationBelongsToEntry(declaration, closure)) === true) { return true; } + if (isIntrinsicUndefined(identifier, symbol, ctx.checker)) return true; if ((identifier.text === "Infinity" || identifier.text === "NaN") && isDefaultLibrarySymbol(symbol, ctx)) { return true; @@ -517,6 +518,19 @@ function isSafeEntryScalarIdentifier( return isSafeModuleScalarBinding(symbol, closure.getSourceFile(), ctx); } +function isIntrinsicUndefined( + identifier: ts.Identifier, + symbol: ts.Symbol, + checker: ts.TypeChecker, +): boolean { + return identifier.text === "undefined" + && symbol.getName() === "undefined" + && (symbol.flags & ts.SymbolFlags.Transient) !== 0 + && (symbol.declarations?.length ?? 0) === 0 + && symbol.valueDeclaration === undefined + && checker.getTypeAtLocation(identifier).flags === ts.TypeFlags.Undefined; +} + function isSafeModuleScalarBinding( symbol: ts.Symbol, sourceFile: ts.SourceFile, diff --git a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts index 6acafb2c6..16ff87684 100644 --- a/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts +++ b/jacodb-ets/ts-frontend/test/builtin-proof.spec.ts @@ -338,6 +338,45 @@ describe("verified builtin call proof", () => { } }); + it("proves optional-parameter guards against intrinsic undefined for declarations and arrows", () => { + const { file } = lower(` + export function named(value?: number): number { + if (value === undefined) value = -1; + return Math.abs(value); + } + export const arrow = (value?: number): number => { + if (value === undefined) value = -1; + return Math.abs(value); + }; + `); + const named = methodWithBodyByName(file, "named"); + const arrow = methodByName(file, "%AM0$%dflt"); + + for (const method of [named, arrow]) { + expect(builtinCall(method, "abs")).toMatchObject({ + method: { declaringClass: { name: "Math" } }, + builtinProof: { + builtin: "MATH_ABS", + entryMethod: method.signature, + }, + }); + } + }); + + it("declines a project-global shadow named undefined", () => { + const { file } = lowerProject({ + "globals.ts": "declare var undefined: undefined;", + "entry.ts": ` + export function f(value?: number): number { + if (value === undefined) value = -1; + return Math.abs(value); + } + `, + }, "entry.ts"); + + expect(hasBuiltinProof(file)).toBe(false); + }); + it("declines ambient scalar reads for declarations and arrows at every evaluated site", () => { const entryPairs = [ [