[ETS] Prove bounded numeric builtin calls

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,19 +432,22 @@ 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(
             ptr = ensureLocal(ptr.toEtsEntity() as EtsValue), // safe cast
             callee = method.toEtsMethodSignature(),
             args = args.map { ensureLocal(it.toEtsEntity()) },
             type = type.toEtsType(),
+            builtinProof = builtinProof?.toEtsBuiltinCallProof(),
         )
 
         is ThisRefDto -> EtsThis(
@@ -723,6 +729,19 @@ 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
+    },
+    entryMethod = entryMethod.toEtsMethodSignature(),
+)
+
 fun LocalSignatureDto.toEtsLocalSignature(): EtsLocalSignature {
     return EtsLocalSignature(
         name = name,

jacodb-ets/src/main/kotlin/org/jacodb/ets/dto/Values.kt

@@ -240,10 +240,31 @@ data class RelationOperationDto(
     override val type: TypeDto = UnknownTypeDto,
 ) : ConditionExprDto
 
+@Serializable
+enum class ProvenBuiltinDto {
+    NUMBER_IS_INTEGER,
+    MATH_ABS,
+    MATH_MIN,
+    MATH_MAX,
+}
+
+@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<ValueDto>
+    val builtinProof: BuiltinCallProofDto?
 
     override val type: TypeDto
         get() = method.returnType
@@ -255,13 +276,15 @@ data class InstanceCallExprDto(
     val instance: ValueDto, // Local
     override val method: MethodSignatureDto,
     override val args: List<ValueDto>,
+    override val builtinProof: BuiltinCallProofDto? = null,
 ) : CallExprDto
 
 @Serializable
 @SerialName("StaticCallExpr")
 data class StaticCallExprDto(
     override val method: MethodSignatureDto,
     override val args: List<ValueDto>,
+    override val builtinProof: BuiltinCallProofDto? = null,
 ) : CallExprDto
 
 @Serializable
@@ -270,6 +293,7 @@ data class PtrCallExprDto(
     val ptr: ValueDto, // Local or FieldRef
     override val method: MethodSignatureDto,
     override val args: List<ValueDto>,
+    override val builtinProof: BuiltinCallProofDto? = null,
 ) : CallExprDto
 
 @Serializable

jacodb-ets/src/main/kotlin/org/jacodb/ets/model/Expr.kt

@@ -725,16 +725,35 @@ data class EtsNullishCoalescingExpr(
     }
 }
 
+enum class EtsBuiltin {
+    NUMBER_IS_INTEGER,
+    MATH_ABS,
+    MATH_MIN,
+    MATH_MAX,
+}
+
+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<EtsLocal>
+    val builtinProof: EtsBuiltinCallProof?
 }
 
 data class EtsInstanceCallExpr(
     override val instance: EtsLocal,
     override val callee: EtsMethodSignature,
     override val args: List<EtsLocal>,
     override val type: EtsType,
+    override val builtinProof: EtsBuiltinCallProof? = null,
 ) : EtsCallExpr, CommonInstanceCallExpr {
     override fun toString(): String {
         return "call ${instance}.${callee.name}(${args.joinToString()})"
@@ -749,6 +768,7 @@ data class EtsStaticCallExpr(
     override val callee: EtsMethodSignature,
     override val args: List<EtsLocal>,
     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 +784,7 @@ data class EtsPtrCallExpr(
     override val callee: EtsMethodSignature,
     override val args: List<EtsLocal>,
     override val type: EtsType,
+    override val builtinProof: EtsBuiltinCallProof? = null,
 ) : EtsCallExpr {
     override fun toString(): String {
         return "ptr_call ${ptr}(${args.joinToString()})"

jacodb-ets/src/test/kotlin/org/jacodb/ets/test/EtsBuiltinCallProofTest.kt

@@ -0,0 +1,202 @@
+/*
+ *  Copyright 2022 UnitTestBot contributors (utbot.org)
+ * <p>
+ *  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
+ * <p>
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ * <p>
+ *  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,
+        )
+        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(
+            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 (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 = builtinCase.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()
+
+            val modelCall = assertIs<EtsStaticCallExpr>(assertIs<EtsCallStmt>(method.cfg.stmts.single()).expr)
+            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)
+        }
+    }
+
+    @Test
+    fun `defaults missing proof to absent`() {
+        val dto = json.decodeFromString<ValueDto>(
+            """
+                {
+                  "_": "StaticCallExpr",
+                  "method": {
+                    "declaringClass": {
+                      "name": "Number",
+                      "declaringFile": { "projectName": "%unk", "fileName": "%unk" }
+                    },
+                    "name": "isInteger",
+                    "parameters": [],
+                    "returnType": { "_": "NumberType" }
+                  },
+                  "args": []
+                }
+            """.trimIndent(),
+        )
+
+        assertNull(assertIs<StaticCallExprDto>(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<SerializationException> {
+            json.decodeFromString<ValueDto>(malformed)
+        }
+    }
+}