Skip to content

Commit 0314612

Browse files
DamtevDamtev
authored
Checkers API (#72)
1 parent a453cbc commit 0314612

File tree

12 files changed

+560
-19
lines changed

12 files changed

+560
-19
lines changed

‎usvm-core/src/main/kotlin/org/usvm/State.kt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>>
156156
} else {
157157
newConstraintToOriginalState
158158
}
159-
val solver = newConstraintToForkedState.uctx.solver<Type>()
159+
val solver = state.ctx.solver<Type>()
160160
val satResult = solver.checkWithSoftConstraints(constraintsToCheck)
161161

162162
return when (satResult) {
@@ -214,7 +214,7 @@ fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>> fork(
214214
holdsInModel.isTrue
215215
}
216216

217-
val notCondition = condition.uctx.mkNot(condition)
217+
val notCondition = state.ctx.mkNot(condition)
218218
val (posState, negState) = when {
219219

220220
trueModels.isNotEmpty() && falseModels.isNotEmpty() -> {

‎usvm-core/src/main/kotlin/org/usvm/StepScope.kt‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -207,6 +207,19 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
207207
return forkMulti(filteredConditionsWithBlockOnStates)
208208
}
209209

210+
/**
211+
* [assert]s the [condition] on the scope with the cloned [originalState]. Returns this cloned state, if this [condition]
212+
* is satisfiable, and returns `null` otherwise.
213+
*/
214+
fun checkSat(condition: UBoolExpr): T? {
215+
val conditionalState = originalState.clone()
216+
val conditionalScope = StepScope(conditionalState, forkBlackList)
217+
218+
return conditionalScope.assert(condition)?.let {
219+
conditionalState
220+
}
221+
}
222+
210223
/**
211224
* Represents the current state of this [StepScope].
212225
*/

‎usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
package org.usvm.api.checkers
2+
3+
import org.jacodb.api.JcClasspath
4+
import org.jacodb.api.JcMethod
5+
import org.jacodb.api.JcType
6+
import org.jacodb.api.cfg.JcInstVisitor
7+
import org.jacodb.api.cfg.JcValue
8+
import org.usvm.UBoolExpr
9+
import org.usvm.UExpr
10+
import org.usvm.UMachineOptions
11+
import org.usvm.api.targets.JcTarget
12+
import org.usvm.machine.JcContext
13+
import org.usvm.machine.JcMachine
14+
import org.usvm.memory.UReadOnlyMemory
15+
16+
sealed interface JcCheckerResult {
17+
// Has no data for now
18+
}
19+
20+
interface JcCheckerSatResult : JcCheckerResult
21+
interface JcCheckerUnsatResult : JcCheckerResult
22+
interface JcCheckerUnknownResult : JcCheckerResult
23+
24+
interface JcCheckerApi {
25+
val ctx: JcContext
26+
val memory: UReadOnlyMemory<JcType>
27+
28+
fun resolveValue(value: JcValue): UExpr<*>
29+
fun checkSat(condition: UBoolExpr): JcCheckerResult
30+
}
31+
32+
class JcCheckerRunner(val cp: JcClasspath) {
33+
private val apiImpl = JcCheckerApiImpl()
34+
35+
val api: JcCheckerApi
36+
get() = apiImpl
37+
38+
fun <T> runChecker(
39+
entryPoint: JcMethod,
40+
checkersVisitor: JcInstVisitor<T>,
41+
targets: List<JcTarget> = emptyList(),
42+
options: UMachineOptions = UMachineOptions(),
43+
) {
44+
val checkersObserver = JcCheckerObserver(checkersVisitor, apiImpl)
45+
46+
JcMachine(cp, options, checkersObserver).use { machine ->
47+
machine.analyze(entryPoint, targets)
48+
}
49+
}
50+
}

‎usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
package org.usvm.api.checkers
2+
3+
import org.jacodb.api.JcType
4+
import org.jacodb.api.cfg.JcAssignInst
5+
import org.jacodb.api.cfg.JcCallExpr
6+
import org.jacodb.api.cfg.JcCallInst
7+
import org.jacodb.api.cfg.JcCatchInst
8+
import org.jacodb.api.cfg.JcEnterMonitorInst
9+
import org.jacodb.api.cfg.JcExitMonitorInst
10+
import org.jacodb.api.cfg.JcGotoInst
11+
import org.jacodb.api.cfg.JcIfInst
12+
import org.jacodb.api.cfg.JcInstVisitor
13+
import org.jacodb.api.cfg.JcReturnInst
14+
import org.jacodb.api.cfg.JcSwitchInst
15+
import org.jacodb.api.cfg.JcThrowInst
16+
import org.jacodb.api.cfg.JcValue
17+
import org.usvm.UBoolExpr
18+
import org.usvm.UExpr
19+
import org.usvm.machine.JcContext
20+
import org.usvm.machine.JcInterpreterObserver
21+
import org.usvm.machine.JcMethodCallBaseInst
22+
import org.usvm.machine.JcMethodEntrypointInst
23+
import org.usvm.machine.interpreter.JcSimpleValueResolver
24+
import org.usvm.machine.interpreter.JcStepScope
25+
import org.usvm.memory.UReadOnlyMemory
26+
27+
internal class JcCheckerApiImpl : JcCheckerApi {
28+
// TODO How to retrieve it properly?
29+
private var internalStepScope: JcStepScope? = null
30+
private var internalExprResolver: JcSimpleValueResolver? = null
31+
32+
private val stepScope: JcStepScope
33+
get() = ensureProcessing(internalStepScope)
34+
35+
private val exprResolver: JcSimpleValueResolver
36+
get() = ensureProcessing(internalExprResolver)
37+
38+
private fun <T> ensureProcessing(e: T?): T =
39+
e ?: error("Checker API can be used during instruction processing only")
40+
41+
override val ctx: JcContext
42+
get() = stepScope.calcOnState { ctx }
43+
44+
override val memory: UReadOnlyMemory<JcType>
45+
get() = stepScope.calcOnState { memory }
46+
47+
override fun resolveValue(value: JcValue): UExpr<*> = value.accept(exprResolver)
48+
49+
override fun checkSat(condition: UBoolExpr): JcCheckerResult =
50+
stepScope.checkSat(condition)?.let {
51+
JcCheckerSatResultImpl
52+
} ?: JcCheckerUnsatResultImpl
53+
54+
internal fun setResolverAndScope(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) {
55+
internalExprResolver = simpleValueResolver
56+
internalStepScope = stepScope
57+
}
58+
59+
internal fun resetResolverAndScope() {
60+
internalStepScope = null
61+
internalExprResolver = null
62+
}
63+
}
64+
65+
internal object JcCheckerSatResultImpl : JcCheckerSatResult
66+
internal object JcCheckerUnsatResultImpl : JcCheckerUnsatResult
67+
internal object JcCheckerUnknownSatResultImpl : JcCheckerUnknownResult
68+
69+
internal class JcCheckerObserver<T>(
70+
private val visitor: JcInstVisitor<T>,
71+
private val jcCheckerApi: JcCheckerApiImpl,
72+
) : JcInterpreterObserver {
73+
override fun onAssignStatement(
74+
simpleValueResolver: JcSimpleValueResolver,
75+
stmt: JcAssignInst,
76+
stepScope: JcStepScope,
77+
) {
78+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcAssignInst(stmt) }
79+
}
80+
81+
override fun onEntryPoint(
82+
simpleValueResolver: JcSimpleValueResolver,
83+
stmt: JcMethodEntrypointInst,
84+
stepScope: JcStepScope,
85+
) {
86+
withScopeAndResolver(simpleValueResolver, stepScope) {
87+
// Looks like we do not need this signal in the ast-based checker
88+
}
89+
}
90+
91+
override fun onMethodCallWithUnresolvedArguments(
92+
simpleValueResolver: JcSimpleValueResolver,
93+
stmt: JcCallExpr,
94+
stepScope: JcStepScope,
95+
) {
96+
withScopeAndResolver(simpleValueResolver, stepScope) {
97+
// Looks like we do not need this signal in the ast-based checker
98+
}
99+
}
100+
101+
override fun onMethodCallWithResolvedArguments(
102+
simpleValueResolver: JcSimpleValueResolver,
103+
stmt: JcMethodCallBaseInst,
104+
stepScope: JcStepScope,
105+
) {
106+
withScopeAndResolver(simpleValueResolver, stepScope) {
107+
// Looks like we do not need this signal in the ast-based checker
108+
}
109+
}
110+
111+
override fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) {
112+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcIfInst(stmt) }
113+
}
114+
115+
override fun onReturnStatement(
116+
simpleValueResolver: JcSimpleValueResolver,
117+
stmt: JcReturnInst,
118+
stepScope: JcStepScope,
119+
) {
120+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcReturnInst(stmt) }
121+
}
122+
123+
override fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {
124+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcGotoInst(stmt) }
125+
}
126+
127+
override fun onCatchStatement(
128+
simpleValueResolver: JcSimpleValueResolver,
129+
stmt: JcCatchInst,
130+
stepScope: JcStepScope
131+
) {
132+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCatchInst(stmt) }
133+
}
134+
135+
override fun onSwitchStatement(
136+
simpleValueResolver: JcSimpleValueResolver,
137+
stmt: JcSwitchInst,
138+
stepScope: JcStepScope,
139+
) {
140+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcSwitchInst(stmt) }
141+
}
142+
143+
override fun onThrowStatement(
144+
simpleValueResolver: JcSimpleValueResolver,
145+
stmt: JcThrowInst,
146+
stepScope: JcStepScope,
147+
) {
148+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcThrowInst(stmt) }
149+
}
150+
151+
override fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {
152+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCallInst(stmt) }
153+
}
154+
155+
override fun onEnterMonitorStatement(
156+
simpleValueResolver: JcSimpleValueResolver,
157+
stmt: JcEnterMonitorInst,
158+
stepScope: JcStepScope,
159+
) {
160+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcEnterMonitorInst(stmt) }
161+
}
162+
163+
override fun onExitMonitorStatement(
164+
simpleValueResolver: JcSimpleValueResolver,
165+
stmt: JcExitMonitorInst,
166+
stepScope: JcStepScope,
167+
) {
168+
withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcExitMonitorInst(stmt) }
169+
}
170+
171+
// TODO it's very dirty way to get required fields, rewrite
172+
private inline fun withScopeAndResolver(
173+
simpleValueResolver: JcSimpleValueResolver,
174+
stepScope: JcStepScope,
175+
blockOnStmt: () -> Unit
176+
) = try {
177+
jcCheckerApi.setResolverAndScope(simpleValueResolver, stepScope)
178+
179+
blockOnStmt()
180+
} finally {
181+
jcCheckerApi.resetResolverAndScope()
182+
}
183+
}

‎usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt‎

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -96,10 +96,10 @@ class TaintAnalysis(
9696
state.targets.filter { it in targets }
9797
}.orEmpty().toList().uncheckedCast()
9898

99-
override fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {
99+
override fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {
100100
// Sinks are already processed at this moment since we resolved it on a call statement
101101

102-
stmt.callExpr?.let { processTaintConfiguration(it, stepScope, exprResolver) }
102+
stmt.callExpr?.let { processTaintConfiguration(it, stepScope, simpleValueResolver) }
103103

104104
// TODO add fields processing
105105
}
@@ -241,15 +241,10 @@ class TaintAnalysis(
241241

242242
val resolvedCondition = stepScope.ctx.mkAnd(resolvedConfigCondition, resolvedSinkCondition)
243243

244-
val (originalStateCopy, taintedStepScope) = stepScope.calcOnState {
245-
val originalStateCopy = clone()
246-
originalStateCopy to JcStepScope(originalStateCopy, UForkBlackList.createDefault())
247-
}
248-
249-
taintedStepScope.assert(resolvedCondition)?.let {
244+
stepScope.checkSat(resolvedCondition)?.let { taintedState ->
250245
// TODO remove corresponding target
251-
collectedStates += originalStateCopy
252-
target?.propagate(taintedStepScope.state)
246+
collectedStates += taintedState
247+
target?.propagate(taintedState)
253248
}
254249
}
255250

‎usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ package org.usvm.machine
33
import org.jacodb.api.cfg.JcAssignInst
44
import org.jacodb.api.cfg.JcCallExpr
55
import org.jacodb.api.cfg.JcCallInst
6+
import org.jacodb.api.cfg.JcCatchInst
67
import org.jacodb.api.cfg.JcEnterMonitorInst
78
import org.jacodb.api.cfg.JcExitMonitorInst
89
import org.jacodb.api.cfg.JcGotoInst
@@ -15,14 +16,14 @@ import org.usvm.machine.interpreter.JcStepScope
1516
import org.usvm.statistics.UInterpreterObserver
1617

1718
interface JcInterpreterObserver : UInterpreterObserver {
18-
fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {}
19+
fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {}
1920
fun onEntryPoint(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodEntrypointInst, stepScope: JcStepScope)
2021
fun onMethodCallWithUnresolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallExpr, stepScope: JcStepScope) {}
2122
fun onMethodCallWithResolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodCallBaseInst, stepScope: JcStepScope) {}
2223
fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) {}
2324
fun onReturnStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcReturnInst, stepScope: JcStepScope) {}
2425
fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {}
25-
fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) {}
26+
fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCatchInst, stepScope: JcStepScope) {}
2627
fun onSwitchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcSwitchInst, stepScope: JcStepScope) {}
2728
fun onThrowStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcThrowInst, stepScope: JcStepScope) {}
2829
fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {}

‎usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ class JcInterpreter(
278278
is JcMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
279279
is JcMethodResult.JcException -> error("Exceptions must be processed earlier")
280280
}
281-
}
281+
} ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
282282

283283
val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return
284284
val expr = exprResolver.resolveJcExpr(stmt.rhv, stmt.lhv.type) ?: return

0 commit comments

Comments
 (0)