Move analysis module from jacodb (#189)

* Upgrade jacodb version

* Move analysis module from jacodb

buildSrc/src/main/kotlin/Versions.kt

@@ -6,7 +6,7 @@ object Versions {
     const val coroutines = "1.6.4"
 
     const val jacodbPackage = "com.github.UnitTestBot.jacodb"
-    const val jacodb = "890624770b" // jacodb neo branch
+    const val jacodb = "5102242db4" // jacodb neo branch
 
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
@@ -20,4 +20,6 @@ object Versions {
     const val samplesJetbrainsAnnotations = "16.0.2"
     const val rd = "2023.2.0"
     const val ini4j = "0.5.4"
+
+    const val sarif4k = "0.5.0"
 }

settings.gradle.kts

@@ -5,6 +5,8 @@ include("usvm-jvm")
 include("usvm-util")
 include("usvm-jvm-instrumentation")
 include("usvm-sample-language")
+include("usvm-dataflow")
+include("usvm-jvm-dataflow")
 
 pluginManagement {
     resolutionStrategy {

usvm-dataflow/build.gradle.kts

@@ -0,0 +1,30 @@
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    id("usvm.kotlin-conventions")
+}
+
+dependencies {
+    implementation("${Versions.jacodbPackage}:jacodb-api-common:${Versions.jacodb}")
+    implementation("${Versions.jacodbPackage}:jacodb-taint-configuration:${Versions.jacodb}")
+
+    implementation("io.github.detekt.sarif4k", "sarif4k", Versions.sarif4k)
+
+    api("io.github.microutils:kotlin-logging:${Versions.klogging}")
+}
+
+tasks.withType<KotlinCompile> {
+    kotlinOptions {
+        freeCompilerArgs = freeCompilerArgs + listOf(
+            "-Xcontext-receivers",
+        )
+    }
+}
+
+publishing {
+    publications {
+        create<MavenPublication>("maven") {
+            from(components["java"])
+        }
+    }
+}

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/config/Condition.kt

@@ -0,0 +1,148 @@
+/*
+ *  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.usvm.dataflow.config
+
+import org.usvm.dataflow.ifds.Maybe
+import org.usvm.dataflow.ifds.onSome
+import org.usvm.dataflow.taint.Tainted
+import org.usvm.dataflow.util.Traits
+import org.usvm.dataflow.util.removeTrailingElementAccessors
+import org.jacodb.api.common.CommonMethod
+import org.jacodb.api.common.cfg.CommonInst
+import org.jacodb.api.common.cfg.CommonValue
+import org.jacodb.taint.configuration.And
+import org.jacodb.taint.configuration.AnnotationType
+import org.jacodb.taint.configuration.ConditionVisitor
+import org.jacodb.taint.configuration.ConstantEq
+import org.jacodb.taint.configuration.ConstantGt
+import org.jacodb.taint.configuration.ConstantLt
+import org.jacodb.taint.configuration.ConstantMatches
+import org.jacodb.taint.configuration.ConstantTrue
+import org.jacodb.taint.configuration.ContainsMark
+import org.jacodb.taint.configuration.IsConstant
+import org.jacodb.taint.configuration.IsType
+import org.jacodb.taint.configuration.Not
+import org.jacodb.taint.configuration.Or
+import org.jacodb.taint.configuration.PositionResolver
+import org.jacodb.taint.configuration.SourceFunctionMatches
+import org.jacodb.taint.configuration.TypeMatches
+
+context(Traits<CommonMethod, CommonInst>)
+open class BasicConditionEvaluator(
+    internal val positionResolver: PositionResolver<Maybe<CommonValue>>,
+) : ConditionVisitor<Boolean> {
+
+    override fun visit(condition: ConstantTrue): Boolean {
+        return true
+    }
+
+    override fun visit(condition: Not): Boolean {
+        return !condition.arg.accept(this)
+    }
+
+    override fun visit(condition: And): Boolean {
+        return condition.args.all { it.accept(this) }
+    }
+
+    override fun visit(condition: Or): Boolean {
+        return condition.args.any { it.accept(this) }
+    }
+
+    override fun visit(condition: IsType): Boolean {
+        // Note: TaintConfigurationFeature.ConditionSpecializer is responsible for
+        // expanding IsType condition upon parsing the taint configuration.
+        error("Unexpected condition: $condition")
+    }
+
+    override fun visit(condition: AnnotationType): Boolean {
+        // Note: TaintConfigurationFeature.ConditionSpecializer is responsible for
+        // expanding AnnotationType condition upon parsing the taint configuration.
+        error("Unexpected condition: $condition")
+    }
+
+    override fun visit(condition: IsConstant): Boolean {
+        positionResolver.resolve(condition.position).onSome {
+            return it.isConstant()
+        }
+        return false
+    }
+
+    override fun visit(condition: ConstantEq): Boolean {
+        positionResolver.resolve(condition.position).onSome { value ->
+            return value.eqConstant(condition.value)
+        }
+        return false
+    }
+
+    override fun visit(condition: ConstantLt): Boolean {
+        positionResolver.resolve(condition.position).onSome { value ->
+            return value.ltConstant(condition.value)
+        }
+        return false
+    }
+
+    override fun visit(condition: ConstantGt): Boolean {
+        positionResolver.resolve(condition.position).onSome { value ->
+            return value.gtConstant(condition.value)
+        }
+        return false
+    }
+
+    override fun visit(condition: ConstantMatches): Boolean {
+        positionResolver.resolve(condition.position).onSome { value ->
+            return value.matches(condition.pattern)
+        }
+        return false
+    }
+
+    override fun visit(condition: SourceFunctionMatches): Boolean {
+        TODO("Not implemented yet")
+    }
+
+    override fun visit(condition: ContainsMark): Boolean {
+        error("This visitor does not support condition $condition. Use FactAwareConditionEvaluator instead")
+    }
+
+    override fun visit(condition: TypeMatches): Boolean {
+        positionResolver.resolve(condition.position).onSome { value ->
+            return value.typeMatches(condition)
+        }
+        return false
+    }
+}
+
+context(Traits<CommonMethod, CommonInst>)
+class FactAwareConditionEvaluator(
+    private val fact: Tainted,
+    positionResolver: PositionResolver<Maybe<CommonValue>>,
+) : BasicConditionEvaluator(positionResolver) {
+
+    override fun visit(condition: ContainsMark): Boolean {
+        if (fact.mark != condition.mark) return false
+        positionResolver.resolve(condition.position).onSome { value ->
+            val variable = value.toPath()
+
+            // FIXME: Adhoc for arrays
+            val variableWithoutStars = variable.removeTrailingElementAccessors()
+            val factWithoutStars = fact.variable.removeTrailingElementAccessors()
+            if (variableWithoutStars == factWithoutStars) return true
+
+            return variable == fact.variable
+        }
+        return false
+    }
+}

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/config/Position.kt

@@ -0,0 +1,104 @@
+/*
+ *  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.usvm.dataflow.config
+
+import org.usvm.dataflow.ifds.AccessPath
+import org.usvm.dataflow.ifds.ElementAccessor
+import org.usvm.dataflow.ifds.Maybe
+import org.usvm.dataflow.ifds.fmap
+import org.usvm.dataflow.ifds.toMaybe
+import org.usvm.dataflow.util.Traits
+import org.jacodb.api.common.CommonMethod
+import org.jacodb.api.common.CommonProject
+import org.jacodb.api.common.cfg.CommonAssignInst
+import org.jacodb.api.common.cfg.CommonInst
+import org.jacodb.api.common.cfg.CommonInstanceCallExpr
+import org.jacodb.api.common.cfg.CommonValue
+import org.jacodb.taint.configuration.AnyArgument
+import org.jacodb.taint.configuration.Argument
+import org.jacodb.taint.configuration.Position
+import org.jacodb.taint.configuration.PositionResolver
+import org.jacodb.taint.configuration.Result
+import org.jacodb.taint.configuration.ResultAnyElement
+import org.jacodb.taint.configuration.This
+
+context(Traits<CommonMethod, CommonInst>)
+class CallPositionToAccessPathResolver(
+    private val callStatement: CommonInst,
+) : PositionResolver<Maybe<AccessPath>> {
+    private val callExpr = callStatement.getCallExpr()
+        ?: error("Call statement should have non-null callExpr")
+
+    override fun resolve(position: Position): Maybe<AccessPath> = when (position) {
+        AnyArgument -> Maybe.none()
+        is Argument -> callExpr.args[position.index].toPathOrNull().toMaybe()
+        This -> (callExpr as? CommonInstanceCallExpr)?.instance?.toPathOrNull().toMaybe()
+        Result -> (callStatement as? CommonAssignInst)?.lhv?.toPathOrNull().toMaybe()
+        ResultAnyElement -> (callStatement as? CommonAssignInst)?.lhv?.toPathOrNull().toMaybe()
+            .fmap { it + ElementAccessor }
+    }
+}
+
+context(Traits<CommonMethod, CommonInst>)
+class CallPositionToValueResolver(
+    private val callStatement: CommonInst,
+) : PositionResolver<Maybe<CommonValue>> {
+    private val callExpr = callStatement.getCallExpr()
+        ?: error("Call statement should have non-null callExpr")
+
+    override fun resolve(position: Position): Maybe<CommonValue> = when (position) {
+        AnyArgument -> Maybe.none()
+        is Argument -> Maybe.some(callExpr.args[position.index])
+        This -> (callExpr as? CommonInstanceCallExpr)?.instance.toMaybe()
+        Result -> (callStatement as? CommonAssignInst)?.lhv.toMaybe()
+        ResultAnyElement -> Maybe.none()
+    }
+}
+
+context(Traits<CommonMethod, CommonInst>)
+class EntryPointPositionToValueResolver(
+    private val method: CommonMethod,
+    private val project: CommonProject,
+) : PositionResolver<Maybe<CommonValue>> {
+    override fun resolve(position: Position): Maybe<CommonValue> = when (position) {
+        This -> Maybe.some(method.thisInstance)
+
+        is Argument -> {
+            val p = method.parameters[position.index]
+            project.getArgument(p).toMaybe()
+        }
+
+        AnyArgument, Result, ResultAnyElement -> error("Unexpected $position")
+    }
+}
+
+context(Traits<CommonMethod, CommonInst>)
+class EntryPointPositionToAccessPathResolver(
+    private val method: CommonMethod,
+    private val project: CommonProject,
+) : PositionResolver<Maybe<AccessPath>> {
+    override fun resolve(position: Position): Maybe<AccessPath> = when (position) {
+        This -> method.thisInstance.toPathOrNull().toMaybe()
+
+        is Argument -> {
+            val p = method.parameters[position.index]
+            project.getArgument(p)?.toPathOrNull().toMaybe()
+        }
+
+        AnyArgument, Result, ResultAnyElement -> error("Unexpected $position")
+    }
+}

usvm-dataflow/src/main/kotlin/org/usvm/dataflow/config/TaintAction.kt

@@ -0,0 +1,70 @@
+/*
+ *  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.usvm.dataflow.config
+
+import org.usvm.dataflow.ifds.AccessPath
+import org.usvm.dataflow.ifds.Maybe
+import org.usvm.dataflow.ifds.fmap
+import org.usvm.dataflow.ifds.map
+import org.usvm.dataflow.taint.Tainted
+import org.jacodb.taint.configuration.AssignMark
+import org.jacodb.taint.configuration.CopyAllMarks
+import org.jacodb.taint.configuration.CopyMark
+import org.jacodb.taint.configuration.PositionResolver
+import org.jacodb.taint.configuration.RemoveAllMarks
+import org.jacodb.taint.configuration.RemoveMark
+
+class TaintActionEvaluator(
+    private val positionResolver: PositionResolver<Maybe<AccessPath>>,
+) {
+    fun evaluate(action: CopyAllMarks, fact: Tainted): Maybe<Collection<Tainted>> =
+        positionResolver.resolve(action.from).map { from ->
+            if (from != fact.variable) return@map Maybe.none()
+            positionResolver.resolve(action.to).fmap { to ->
+                setOf(fact, fact.copy(variable = to))
+            }
+        }
+
+    fun evaluate(action: CopyMark, fact: Tainted): Maybe<Collection<Tainted>> {
+        if (fact.mark != action.mark) return Maybe.none()
+        return positionResolver.resolve(action.from).map { from ->
+            if (from != fact.variable) return@map Maybe.none()
+            positionResolver.resolve(action.to).fmap { to ->
+                setOf(fact, fact.copy(variable = to))
+            }
+        }
+    }
+
+    fun evaluate(action: AssignMark): Maybe<Collection<Tainted>> =
+        positionResolver.resolve(action.position).fmap { variable ->
+            setOf(Tainted(variable, action.mark))
+        }
+
+    fun evaluate(action: RemoveAllMarks, fact: Tainted): Maybe<Collection<Tainted>> =
+        positionResolver.resolve(action.position).map { variable ->
+            if (variable != fact.variable) return@map Maybe.none()
+            Maybe.some(emptySet())
+        }
+
+    fun evaluate(action: RemoveMark, fact: Tainted): Maybe<Collection<Tainted>> {
+        if (fact.mark != action.mark) return Maybe.none()
+        return positionResolver.resolve(action.position).map { variable ->
+            if (variable != fact.variable) return@map Maybe.none()
+            Maybe.some(emptySet())
+        }
+    }
+}