[TS PBT] Map property coverage to EtsIR

build.gradle.kts

@@ -10,6 +10,7 @@ tasks.register("validateProjectList") {
         // Define the expected subprojects here.
         val expectedProjects = setOf(
             project(":usvm-core"),
+            project(":usvm-detekt-rules"),
             project(":usvm-util"),
             project(":usvm-dataflow"),
             project(":usvm-sample-language"),

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "9ea33879c9"
+    const val jacodb = "ddb127d9ef"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

buildSrc/src/main/kotlin/DetektConfiguration.kt

@@ -11,8 +11,13 @@ import org.gradle.kotlin.dsl.dependencies
 import org.gradle.kotlin.dsl.withType
 
 fun Project.configureDetekt() {
+    val usesStrictTsRules = path in STRICT_TS_DETEKT_PROJECT_PATHS
+
     dependencies {
         detektPlugins("io.gitlab.arturbosch.detekt:detekt-formatting:${detekt.toolVersion}")
+        if (usesStrictTsRules) {
+            detektPlugins(project(USVM_DETEKT_RULES_PROJECT_PATH))
+        }
     }
 
     val includes = listOf(
@@ -37,7 +42,6 @@ fun Project.configureDetekt() {
     val configFile = rootDir.resolve("detekt").resolve("config.yml")
     val tsConfigFile = rootDir.resolve("detekt").resolve("ts-config.yml")
     val reportFile = rootProject.layout.buildDirectory.file("reports/detekt/detekt.sarif")
-    val usesStrictTsRules = name in STRICT_TS_DETEKT_PROJECTS
     val configFiles = if (usesStrictTsRules) listOf(configFile, tsConfigFile) else listOf(configFile)
 
     detekt {
@@ -89,4 +93,5 @@ fun Project.configureDetekt() {
     }
 }
 
-private val STRICT_TS_DETEKT_PROJECTS = setOf("usvm-ts", "usvm-ts-pbt")
+private val STRICT_TS_DETEKT_PROJECT_PATHS = setOf(":usvm-ts", ":usvm-ts-pbt")
+private const val USVM_DETEKT_RULES_PROJECT_PATH = ":usvm-detekt-rules"

detekt/baselines/usvm-ts-Main.yml

@@ -44,6 +44,24 @@
     <ID>NestedBlockDepth:TsInterpreter.kt$TsInterpreter$private fun assignToInDfltDflt( scope: TsStepScope, lhv: EtsLValue, expr: UExpr&lt;*&gt;, ): Unit?</ID>
     <ID>NestedBlockDepth:TsInterpreter.kt$TsInterpreter$private fun visitVirtualMethodCall(scope: TsStepScope, stmt: TsVirtualMethodCallStmt)</ID>
     <ID>NestedBlockDepth:WriteField.kt$internal fun TsExprResolver.handleAssignToInstanceField( lhv: EtsInstanceFieldRef, expr: UExpr&lt;*&gt;, ): Unit?</ID>
+    <ID>NestedCallArguments:BuildEtsMethod.kt$EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = enclosingClass.signature, name = name, parameters = parameters.mapIndexed { index, (name, type) -&gt; EtsMethodParameter(index, name, type) }, returnType = returnType, ) )</ID>
+    <ID>NestedCallArguments:CallApproximations.kt$mkAnd( mkBvSignedGreaterOrEqualExpr(symbolicResult, mkBv(0)), mkBvSignedLessExpr(symbolicResult, length) )</ID>
+    <ID>NestedCallArguments:CallApproximations.kt$resolveEtsMethods( EtsMethodSignature( enclosingClass = EtsClassSignature.UNKNOWN, name = executorLocal.name, parameters = emptyList(), returnType = EtsUnknownType, ) )</ID>
+    <ID>NestedCallArguments:EtsFakeType.kt$EtsFakeType$mkAnd( mkImplies(boolTypeExpr, mkNot(fpTypeExpr)), mkImplies(boolTypeExpr, mkNot(refTypeExpr)), mkImplies(fpTypeExpr, mkNot(refTypeExpr)), mkOr(boolTypeExpr, fpTypeExpr, refTypeExpr), )</ID>
+    <ID>NestedCallArguments:EtsHierarchy.kt$EtsHierarchy.Companion$EtsClassType( signature = EtsClassSignature( name = "Object", file = EtsFileSignature(projectName = "ES2015", fileName = "BuiltinClass") ), )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$ExprWithTypeConstraint( constraint = possibleType.boolTypeExpr, expr = memory.read(getIntermediateBoolLValue(expr.address)) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$ExprWithTypeConstraint( constraint = possibleType.refTypeExpr, expr = mkAnd( mkHeapRefEq(value, mkTsNullValue()).not(), mkHeapRefEq(value, mkUndefinedValue()).not(), ) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkAnd( mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), mkBvSignedLessOrEqualExpr(length, mkBv(maxLength)) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkIte( condition = fakeType.refTypeExpr, trueBranch = mkOr( mkHeapRefEq(ref, mkTsNullValue()), mkHeapRefEq(ref, mkUndefinedValue()) ), falseBranch = mkFalse(), )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkIte( condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()), trueBranch = mkFp(0.0, fp64Sort), falseBranch = mkIte( mkEq(expr.asExpr(addressSort), mkUndefinedValue()), mkFp64NaN(), mkFp64NaN() ) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkIte( condition = type.fpTypeExpr, trueBranch = expr.extractFp(scope), falseBranch = mkIte( condition = type.boolTypeExpr, trueBranch = mkNumericExpr(expr.extractBool(scope), scope), falseBranch = mkNumericExpr(expr.extractRef(scope), scope) ) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkNot( mkOr( mkHeapRefEq(ref, mkTsNullValue()), mkHeapRefEq(ref, mkUndefinedValue()) ) )</ID>
+    <ID>NestedCallArguments:ExprUtil.kt$mkOr( mkHeapRefEq(ref, mkTsNullValue()), mkHeapRefEq(ref, mkUndefinedValue()) )</ID>
+    <ID>NestedCallArguments:TsExprResolver.kt$TsExprResolver$mkAnd( mkEq( mkBvToFpExpr( sort = fp64Sort, roundingMode = fpRoundingModeSortDefaultValue(), value = bvSize, signed = true, ), size.asExpr(fp64Sort) ), mkAnd( mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)), mkBvSignedLessOrEqualExpr(bvSize.asExpr(bv32Sort), mkBv(Int.MAX_VALUE)) ) )</ID>
+    <ID>NestedCallArguments:TsExprResolver.kt$TsExprResolver$mkBvAndExpr( rightBv, mkBv(ECMASCRIPT_BITWISE_SHIFT_MASK, ECMASCRIPT_BITWISE_INTEGER_SIZE.toUInt()) )</ID>
+    <ID>NestedCallArguments:TsExprResolver.kt$TsExprResolver$mkIte( condition = mkHeapRefEq(ref, mkTsNullValue()), trueBranch = mkStringConstant("object", scope), falseBranch = mkIte( condition = mkHeapRefEq(ref, mkUndefinedValue()), trueBranch = mkStringConstant("undefined", scope), falseBranch = mkIte( condition = scope.calcOnState { val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) // TODO: adhoc: "expand" ITE if (unwrappedRef is UIteExpr&lt;*&gt;) { val trueBranch = unwrappedRef.trueBranch val falseBranch = unwrappedRef.falseBranch if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { val unwrappedTrueExpr = trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) val unwrappedFalseExpr = falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) return@calcOnState mkIte( condition = unwrappedRef.condition, trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType), falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType), ) } } memory.types.evalTypeEquals(unwrappedRef, EtsStringType) }, trueBranch = mkStringConstant("string", scope), falseBranch = mkStringConstant("object", scope), ) ) )</ID>
+    <ID>NestedCallArguments:TsUnknownCall.kt$dispatch( scope, TsUnknownCall( callee = callee, receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) }, arguments = call.args.zip(resolvedArguments) { source, resolved -&gt; TsUnknownCallValue(source, resolved) }, resultType = call.type, callSite = callSite, failureReason = failureReason, ), )</ID>
+    <ID>NestedCallArguments:TsUnknownCallProfile.kt$TsProfileUnknownCallDispatcher$TsUnknownCallEvent( callSite = call.callSite, callee = call.callee, failureReason = call.failureReason, profile = profile.copy(residualOverrides = profile.residualOverrides.toMap()), outcome = outcome, decision = decision, )</ID>
     <ID>NoBlankLineInList:TsState.kt$TsState$ </ID>
     <ID>NoEmptyFirstLineInMethodBlock:TsInterpreter.kt$TsInterpreter$ </ID>
     <ID>NoMultipleSpaces:TsTypeSystem.kt$TsTypeSystem$ </ID>

detekt/ts-config.yml

@@ -11,5 +11,15 @@ complexity:
     threshold: 4
 
 style:
+  BracesOnWhenStatements:
+    active: false
   CascadingCallWrapping:
     active: true
+
+usvm:
+  active: true
+  MultilineWhenBranchBraces:
+    active: true
+  NestedCallArguments:
+    active: true
+    excludes: [ '**/test/**' ]

settings.gradle.kts

@@ -28,6 +28,7 @@ develocity {
 }
 
 include("usvm-core")
+include("usvm-detekt-rules")
 include("usvm-jvm")
 include("usvm-jvm:usvm-jvm-api")
 include("usvm-jvm:usvm-jvm-test-api")

usvm-detekt-rules/build.gradle.kts

@@ -0,0 +1,38 @@
+import org.jetbrains.kotlin.gradle.dsl.JvmTarget
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    kotlin("jvm")
+}
+
+group = "org.usvm"
+
+java {
+    sourceCompatibility = JavaVersion.VERSION_1_8
+    targetCompatibility = JavaVersion.VERSION_1_8
+}
+
+repositories {
+    mavenCentral()
+}
+
+val detektVersion = "1.23.5"
+
+dependencies {
+    compileOnly("io.gitlab.arturbosch.detekt:detekt-api:$detektVersion")
+
+    testImplementation("io.gitlab.arturbosch.detekt:detekt-test:$detektVersion")
+    testImplementation(Libs.junit_jupiter_api)
+    testRuntimeOnly(Libs.junit_jupiter_engine)
+}
+
+tasks.withType<KotlinCompile>().configureEach {
+    compilerOptions {
+        jvmTarget.set(JvmTarget.JVM_1_8)
+        allWarningsAsErrors.set(true)
+    }
+}
+
+tasks.withType<Test>().configureEach {
+    useJUnitPlatform()
+}

usvm-detekt-rules/src/main/kotlin/org/usvm/detekt/MultilineWhenBranchBraces.kt

@@ -0,0 +1,48 @@
+package org.usvm.detekt
+
+import io.gitlab.arturbosch.detekt.api.CodeSmell
+import io.gitlab.arturbosch.detekt.api.Config
+import io.gitlab.arturbosch.detekt.api.Debt
+import io.gitlab.arturbosch.detekt.api.Entity
+import io.gitlab.arturbosch.detekt.api.Issue
+import io.gitlab.arturbosch.detekt.api.Rule
+import io.gitlab.arturbosch.detekt.api.Severity
+import org.jetbrains.kotlin.psi.KtBlockExpression
+import org.jetbrains.kotlin.psi.KtWhenEntry
+
+/** Requires a block when a `when` branch body starts below its arrow. */
+internal class MultilineWhenBranchBraces(config: Config = Config.empty) : Rule(config) {
+    override val issue = Issue(
+        id = "MultilineWhenBranchBraces",
+        severity = Severity.Style,
+        description = "Requires braces when a when branch body starts on a new line",
+        debt = Debt.FIVE_MINS,
+    )
+
+    override fun visitWhenEntry(entry: KtWhenEntry) {
+        super.visitWhenEntry(entry)
+
+        val expression = entry.expression ?: return
+        if (expression is KtBlockExpression) {
+            return
+        }
+
+        val arrow = entry.arrow ?: return
+        val fileText = entry.containingFile.text
+        val textBeforeExpression = fileText.substring(
+            startIndex = arrow.textRange.endOffset,
+            endIndex = expression.textRange.startOffset,
+        )
+        if (!textBeforeExpression.contains('\n') && !textBeforeExpression.contains('\r')) {
+            return
+        }
+
+        report(
+            CodeSmell(
+                issue = issue,
+                entity = Entity.from(expression),
+                message = "A when branch body that starts on a new line must be enclosed in braces",
+            ),
+        )
+    }
+}

usvm-detekt-rules/src/main/kotlin/org/usvm/detekt/NestedCallArguments.kt

@@ -0,0 +1,86 @@
+package org.usvm.detekt
+
+import io.gitlab.arturbosch.detekt.api.CodeSmell
+import io.gitlab.arturbosch.detekt.api.Config
+import io.gitlab.arturbosch.detekt.api.Debt
+import io.gitlab.arturbosch.detekt.api.Entity
+import io.gitlab.arturbosch.detekt.api.Issue
+import io.gitlab.arturbosch.detekt.api.Rule
+import io.gitlab.arturbosch.detekt.api.Severity
+import org.jetbrains.kotlin.psi.KtCallExpression
+import org.jetbrains.kotlin.psi.KtExpression
+import org.jetbrains.kotlin.psi.KtParenthesizedExpression
+import org.jetbrains.kotlin.psi.KtQualifiedExpression
+import org.jetbrains.kotlin.psi.KtValueArgument
+
+/** Prevents deeply nested calls such as `outer(middle(inner()))`. */
+internal class NestedCallArguments(config: Config = Config.empty) : Rule(config) {
+    override val issue = Issue(
+        id = "NestedCallArguments",
+        severity = Severity.Style,
+        description = "Nested call arguments should be extracted into intermediate variables",
+        debt = Debt.FIVE_MINS,
+    )
+
+    override fun visitCallExpression(expression: KtCallExpression) {
+        super.visitCallExpression(expression)
+
+        if (expression.isArgumentRootCall()) {
+            return
+        }
+        if (!expression.textContains('\n')) {
+            return
+        }
+
+        val depth = expression.argumentCallDepth()
+        if (depth <= MAX_ARGUMENT_CALL_DEPTH) {
+            return
+        }
+
+        report(
+            CodeSmell(
+                issue = issue,
+                entity = Entity.from(expression),
+                message = "Call arguments are nested $depth levels deep; extract an inner call into a variable",
+            ),
+        )
+    }
+}
+
+private fun KtCallExpression.argumentCallDepth(): Int {
+    val nestedDepth = valueArguments
+        .asSequence()
+        .mapNotNull { argument -> argument.getArgumentExpression()?.rootCallOrNull() }
+        .maxOfOrNull { nestedCall -> nestedCall.argumentCallDepth() }
+        ?: 0
+
+    return nestedDepth + 1
+}
+
+private fun KtExpression.rootCallOrNull(): KtCallExpression? = when (this) {
+    is KtCallExpression -> this
+    is KtParenthesizedExpression -> expression?.rootCallOrNull()
+    is KtQualifiedExpression -> selectorExpression?.rootCallOrNull()
+    else -> null
+}
+
+private fun KtCallExpression.isArgumentRootCall(): Boolean {
+    var current: KtExpression = this
+    while (true) {
+        val parentExpression = current.parent as? KtExpression ?: break
+        val wrapsCurrent = when (parentExpression) {
+            is KtParenthesizedExpression -> parentExpression.expression == current
+            is KtQualifiedExpression -> parentExpression.selectorExpression == current
+            else -> false
+        }
+        if (!wrapsCurrent) {
+            break
+        }
+
+        current = parentExpression
+    }
+
+    return current.parent is KtValueArgument
+}
+
+private const val MAX_ARGUMENT_CALL_DEPTH = 2

usvm-detekt-rules/src/main/kotlin/org/usvm/detekt/UsvmRuleSetProvider.kt

@@ -0,0 +1,18 @@
+package org.usvm.detekt
+
+import io.gitlab.arturbosch.detekt.api.Config
+import io.gitlab.arturbosch.detekt.api.RuleSet
+import io.gitlab.arturbosch.detekt.api.RuleSetProvider
+
+/** Makes USVM-specific rules discoverable by Detekt. */
+class UsvmRuleSetProvider : RuleSetProvider {
+    override val ruleSetId: String = "usvm"
+
+    override fun instance(config: Config): RuleSet = RuleSet(
+        id = ruleSetId,
+        rules = listOf(
+            MultilineWhenBranchBraces(config),
+            NestedCallArguments(config),
+        ),
+    )
+}

usvm-detekt-rules/src/main/resources/META-INF/services/io.gitlab.arturbosch.detekt.api.RuleSetProvider

@@ -0,0 +1 @@
+org.usvm.detekt.UsvmRuleSetProvider

usvm-detekt-rules/src/test/kotlin/org/usvm/detekt/MultilineWhenBranchBracesTest.kt

@@ -0,0 +1,86 @@
+package org.usvm.detekt
+
+import io.gitlab.arturbosch.detekt.test.compileAndLint
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Test
+
+class MultilineWhenBranchBracesTest {
+    private val rule = MultilineWhenBranchBraces()
+
+    @Test
+    fun `allows branch body on the same line`() {
+        val code = """
+            fun choose(condition: Boolean): Int = when {
+                condition -> 1
+                else -> 0
+            }
+        """.trimIndent()
+
+        val findings = rule.compileAndLint(code)
+
+        assertEquals(0, findings.size)
+    }
+
+    @Test
+    fun `reports branch body moved to a new line without braces`() {
+        val code = """
+            fun choose(condition: Boolean): Int = when {
+                condition ->
+                    1
+                else -> 0
+            }
+        """.trimIndent()
+
+        val findings = rule.compileAndLint(code)
+
+        assertEquals(1, findings.size)
+    }
+
+    @Test
+    fun `allows branch body moved to a new line inside braces`() {
+        val code = """
+            fun choose(condition: Boolean): Int = when {
+                condition -> {
+                    1
+                }
+                else -> 0
+            }
+        """.trimIndent()
+
+        val findings = rule.compileAndLint(code)
+
+        assertEquals(0, findings.size)
+    }
+
+    @Test
+    fun `reports else body moved to a new line without braces`() {
+        val code = """
+            fun choose(condition: Boolean): Int = when {
+                condition -> 1
+                else ->
+                    0
+            }
+        """.trimIndent()
+
+        val findings = rule.compileAndLint(code)
+
+        assertEquals(1, findings.size)
+    }
+
+    @Test
+    fun `allows multiline body inside braces`() {
+        val code = """
+            fun choose(condition: Boolean): Int = when {
+                condition -> {
+                    println("selected")
+                    1
+                }
+                else -> 0
+            }
+        """.trimIndent()
+
+        val findings = rule.compileAndLint(code)
+
+        assertEquals(0, findings.size)
+    }
+}