Skip to content

Commit

Permalink
Add ApplicationGraph and bump jacodb (#236)
Browse files Browse the repository at this point in the history
  • Loading branch information
Lipen authored Dec 26, 2024
1 parent 59dfe48 commit a43da92
Show file tree
Hide file tree
Showing 25 changed files with 75 additions and 24 deletions.
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/Dependencies.kt
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import org.gradle.plugin.use.PluginDependenciesSpec
object Versions {
const val detekt = "1.18.1"
const val ini4j = "0.5.4"
const val jacodb = "6539d5020c"
const val jacodb = "ad5e1f170e"
const val juliet = "1.3.2"
const val junit = "5.9.3"
const val kotlin = "2.1.0"
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
package org.usvm.dataflow.graph

import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.cfg.CommonInst

/**
* Provides both CFG and call graph (i.e., the supergraph in terms of RHS95 paper).
*/
interface ApplicationGraph<Method, Statement>
where Method : CommonMethod,
Statement : CommonInst {

fun predecessors(node: Statement): Sequence<Statement>
fun successors(node: Statement): Sequence<Statement>

fun callees(node: Statement): Sequence<Method>
fun callers(method: Method): Sequence<Statement>

fun entryPoints(method: Method): Sequence<Statement>
fun exitPoints(method: Method): Sequence<Statement>

fun methodOf(node: Statement): Method
}
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@
package org.usvm.dataflow.graph

import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst

private class BackwardApplicationGraphImpl<Method, Statement>(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ import kotlinx.coroutines.channels.getOrElse
import kotlinx.coroutines.coroutineScope
import kotlinx.coroutines.isActive
import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.util.Traits
import java.util.concurrent.ConcurrentHashMap

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,12 @@ package org.usvm.dataflow.taint

import mu.KLogging
import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.jacodb.taint.configuration.TaintConfigurationItem
import org.jacodb.taint.configuration.TaintMethodSink
import org.usvm.dataflow.config.CallPositionToValueResolver
import org.usvm.dataflow.config.FactAwareConditionEvaluator
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.ifds.Analyzer
import org.usvm.dataflow.ifds.Edge
import org.usvm.dataflow.ifds.Reason
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ import org.usvm.dataflow.ifds.Reason
import org.usvm.dataflow.ifds.UnitResolver
import org.usvm.dataflow.ifds.UnitType
import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.usvm.dataflow.graph.ApplicationGraph

class TaintBidiRunner<Method, Statement>(
val manager: TaintManager<Method, Statement>,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@
package org.usvm.dataflow.taint

import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonAssignInst
import org.jacodb.api.common.cfg.CommonExpr
import org.jacodb.api.common.cfg.CommonInst
Expand All @@ -42,6 +41,7 @@ import org.usvm.dataflow.config.EntryPointPositionToAccessPathResolver
import org.usvm.dataflow.config.EntryPointPositionToValueResolver
import org.usvm.dataflow.config.FactAwareConditionEvaluator
import org.usvm.dataflow.config.TaintActionEvaluator
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.ifds.ElementAccessor
import org.usvm.dataflow.ifds.FlowFunction
import org.usvm.dataflow.ifds.FlowFunctions
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,9 @@ import kotlinx.coroutines.launch
import kotlinx.coroutines.runBlocking
import kotlinx.coroutines.withTimeoutOrNull
import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.jacodb.taint.configuration.TaintConfigurationItem
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.graph.reversed
import org.usvm.dataflow.ifds.ControlEvent
import org.usvm.dataflow.ifds.IfdsResult
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ import kotlinx.coroutines.DelicateCoroutinesApi
import kotlinx.coroutines.GlobalScope
import kotlinx.coroutines.future.future
import org.jacodb.api.jvm.JcClasspath
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.impl.features.usagesExt
import java.util.concurrent.CompletableFuture

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
/*
* 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.jvm.graph

import org.jacodb.api.jvm.JcClasspath
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.cfg.JcInst
import org.usvm.dataflow.graph.ApplicationGraph

/**
* Interface for [JcApplicationGraph] built with jacodb.
*/
interface JcApplicationGraph : ApplicationGraph<JcMethod, JcInst> {
val cp: JcClasspath
}
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ package org.usvm.dataflow.jvm.graph

import org.jacodb.api.jvm.JcClasspath
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.api.jvm.ext.cfg.callExpr
import org.jacodb.impl.features.SyncUsagesExtension
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ package org.usvm.dataflow.jvm.graph
import kotlinx.coroutines.runBlocking
import org.jacodb.api.jvm.JcClassType
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.api.jvm.cfg.JcVirtualCallExpr
import org.jacodb.api.jvm.ext.cfg.callExpr
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@
package org.usvm.dataflow.jvm.npe

import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.taint.configuration.TaintConfigurationItem
import org.jacodb.taint.configuration.TaintMark
Expand All @@ -26,6 +25,7 @@ import org.usvm.dataflow.config.CallPositionToValueResolver
import org.usvm.dataflow.config.FactAwareConditionEvaluator
import org.usvm.dataflow.ifds.Analyzer
import org.usvm.dataflow.ifds.Reason
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.util.JcTraits
import org.usvm.dataflow.taint.EdgeForOtherRunner
import org.usvm.dataflow.taint.NewSummaryEdge
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ import org.jacodb.api.common.cfg.CommonValue
import org.jacodb.api.jvm.JcArrayType
import org.jacodb.api.jvm.JcClasspath
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcArgument
import org.jacodb.api.jvm.cfg.JcAssignInst
import org.jacodb.api.jvm.cfg.JcCallExpr
Expand Down Expand Up @@ -65,6 +64,7 @@ import org.usvm.dataflow.ifds.isOnHeap
import org.usvm.dataflow.ifds.isStatic
import org.usvm.dataflow.ifds.minus
import org.usvm.dataflow.ifds.onSome
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.util.JcTraits
import org.usvm.dataflow.taint.TaintDomainFact
import org.usvm.dataflow.taint.TaintZeroFact
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,14 @@
package org.usvm.dataflow.jvm.npe

import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.taint.configuration.TaintConfigurationFeature
import org.jacodb.taint.configuration.TaintConfigurationItem
import org.usvm.dataflow.ifds.UniRunner
import org.usvm.dataflow.ifds.UnitResolver
import org.usvm.dataflow.ifds.UnitType
import org.usvm.dataflow.ifds.UnknownUnit
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.ifds.JcUnitResolver
import org.usvm.dataflow.jvm.util.JcTraits
import org.usvm.dataflow.taint.TaintManager
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
package org.usvm.dataflow.jvm.taint

import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.taint.configuration.TaintConfigurationFeature
import org.jacodb.taint.configuration.TaintConfigurationItem
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.ifds.JcUnitResolver
import org.usvm.dataflow.jvm.util.JcTraits
import org.usvm.dataflow.taint.TaintManager
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@
package org.usvm.dataflow.jvm.unused

import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.ifds.Analyzer
import org.usvm.dataflow.ifds.Edge
import org.usvm.dataflow.ifds.Vertex
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,11 @@
package org.usvm.dataflow.jvm.unused

import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonAssignInst
import org.jacodb.api.common.cfg.CommonInst
import org.jacodb.api.jvm.cfg.JcSpecialCallExpr
import org.jacodb.api.jvm.cfg.JcStaticCallExpr
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.ifds.FlowFunction
import org.usvm.dataflow.ifds.FlowFunctions
import org.usvm.dataflow.ifds.isOnHeap
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ import kotlinx.coroutines.launch
import kotlinx.coroutines.runBlocking
import kotlinx.coroutines.withTimeoutOrNull
import org.jacodb.api.common.CommonMethod
import org.jacodb.api.common.analysis.ApplicationGraph
import org.jacodb.api.common.cfg.CommonInst
import org.usvm.dataflow.graph.ApplicationGraph
import org.usvm.dataflow.ifds.ControlEvent
import org.usvm.dataflow.ifds.Edge
import org.usvm.dataflow.ifds.Manager
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,12 @@
import kotlin.time.DurationUnit;
import org.jacodb.api.jvm.JcClassOrInterface;
import org.jacodb.api.jvm.JcMethod;
import org.jacodb.api.jvm.analysis.JcApplicationGraph;
import org.jacodb.api.jvm.cfg.JcInst;
import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.api.TestInstance;
import org.usvm.dataflow.jvm.graph.ApplicationGraphFactory;
import org.usvm.dataflow.jvm.graph.JcApplicationGraph;
import org.usvm.dataflow.jvm.ifds.JcUnitResolver;
import org.usvm.dataflow.jvm.ifds.UnitResolverKt;
import org.usvm.dataflow.jvm.taint.TaintManagerKt;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ import kotlinx.coroutines.runBlocking
import org.jacodb.api.jvm.JcClasspath
import org.jacodb.api.jvm.JcDatabase
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcInst
import org.jacodb.api.jvm.ext.findClass
import org.jacodb.api.jvm.ext.methods
Expand All @@ -36,6 +35,7 @@ import org.junit.jupiter.api.AfterAll
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.params.provider.Arguments
import org.usvm.dataflow.ifds.Vulnerability
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.graph.newApplicationGraphForAnalysis
import java.io.File
import java.util.stream.Stream
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ import io.mockk.every
import io.mockk.mockk
import org.jacodb.api.jvm.JcClassType
import org.jacodb.api.jvm.JcMethod
import org.jacodb.api.jvm.analysis.JcApplicationGraph
import org.jacodb.api.jvm.cfg.JcArgument
import org.jacodb.api.jvm.cfg.JcAssignInst
import org.jacodb.api.jvm.cfg.JcCallExpr
Expand All @@ -39,6 +38,7 @@ import org.junit.jupiter.api.Assertions
import org.junit.jupiter.api.Test
import org.junit.jupiter.api.TestInstance
import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
import org.usvm.dataflow.jvm.graph.JcApplicationGraph
import org.usvm.dataflow.jvm.util.JcTraits
import org.usvm.dataflow.jvm.util.callee
import org.usvm.dataflow.jvm.util.toPath
Expand Down
4 changes: 1 addition & 3 deletions usvm-ts/src/main/kotlin/org/usvm/TSApplicationGraph.kt
Original file line number Diff line number Diff line change
@@ -1,14 +1,12 @@
package org.usvm

import org.jacodb.ets.base.EtsStmt
import org.jacodb.ets.graph.EtsApplicationGraphImpl
import org.jacodb.ets.model.EtsFile
import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.model.EtsScene
import org.usvm.statistics.ApplicationGraph

class TSApplicationGraph(project: EtsFile) : ApplicationGraph<EtsMethod, EtsStmt> {
private val applicationGraph = EtsApplicationGraphImpl(EtsScene(listOf(project)))
private val applicationGraph: ApplicationGraph<EtsMethod, EtsStmt> = TODO()

override fun predecessors(node: EtsStmt): Sequence<EtsStmt> =
applicationGraph.predecessors(node)
Expand Down
5 changes: 5 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/TSExprResolver.kt
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ import org.jacodb.ets.base.EtsPostDecExpr
import org.jacodb.ets.base.EtsPostIncExpr
import org.jacodb.ets.base.EtsPreDecExpr
import org.jacodb.ets.base.EtsPreIncExpr
import org.jacodb.ets.base.EtsPtrCallExpr
import org.jacodb.ets.base.EtsRemExpr
import org.jacodb.ets.base.EtsRightShiftExpr
import org.jacodb.ets.base.EtsStaticCallExpr
Expand Down Expand Up @@ -300,6 +301,10 @@ class TSExprResolver(
TODO("Not yet implemented")
}

override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
TODO("Not yet implemented")
}

override fun visit(expr: EtsStrictEqExpr): UExpr<out USort> {
TODO("Not yet implemented")
}
Expand Down
2 changes: 1 addition & 1 deletion usvm-ts/src/main/kotlin/org/usvm/TSInterpreter.kt
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ class TSInterpreter(
state.models = listOf(model)

state.callStack.push(method, returnSite = null)
state.memory.stack.push(method.parameters.size, method.localsCount)
state.memory.stack.push(method.parameters.size, method.locals.size)
state.pathNode += method.cfg.instructions.first()

return state
Expand Down

0 comments on commit a43da92

Please sign in to comment.