From a805f5f4f2c35d9daa6a07a4789d5f78d291b87d Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Fri, 29 Sep 2023 16:51:49 +0300 Subject: [PATCH 1/9] Implemented `checkSat` --- usvm-core/src/main/kotlin/org/usvm/State.kt | 4 ++-- usvm-core/src/main/kotlin/org/usvm/StepScope.kt | 12 ++++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index 4c4912055b..0e4885fd38 100644 --- a/usvm-core/src/main/kotlin/org/usvm/State.kt +++ b/usvm-core/src/main/kotlin/org/usvm/State.kt @@ -156,7 +156,7 @@ private fun , Type, Context : UContext<*>> } else { newConstraintToOriginalState } - val solver = newConstraintToForkedState.uctx.solver() + val solver = state.ctx.solver() val satResult = solver.checkWithSoftConstraints(constraintsToCheck) return when (satResult) { @@ -214,7 +214,7 @@ fun , Type, Context : UContext<*>> fork( holdsInModel.isTrue } - val notCondition = condition.uctx.mkNot(condition) + val notCondition = state.ctx.mkNot(condition) val (posState, negState) = when { trueModels.isNotEmpty() && falseModels.isNotEmpty() -> { diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index 8504c2c240..b2fbcefaf4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -207,6 +207,18 @@ class StepScope, Type, Statement, return forkMulti(filteredConditionsWithBlockOnStates) } + // TODO docs + fun checkSat(condition: UBoolExpr, blockOnSatState: T.() -> Unit = { }): Unit? { + // TODO should we check step flags here? + + val conditionalState = originalState.clone() + val conditionalScope = StepScope(conditionalState, forkBlackList) + + return conditionalScope.assert(condition)?.let { + blockOnSatState(conditionalState) + } + } + /** * Represents the current state of this [StepScope]. */ From e00202552a9dbbc395632a95cb2ec5e86744712e Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 15:56:26 +0300 Subject: [PATCH 2/9] Used `checkSat` in `TaintAnalysis` --- .../kotlin/org/usvm/api/targets/TaintAnalysis.kt | 15 +++++---------- .../org/usvm/machine/JcInterpreterObserver.kt | 5 +++-- 2 files changed, 8 insertions(+), 12 deletions(-) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt index 129b0aaea8..82bcde803d 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt @@ -96,10 +96,10 @@ class TaintAnalysis( state.targets.filter { it in targets } }.orEmpty().toList().uncheckedCast() - override fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) { + override fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) { // Sinks are already processed at this moment since we resolved it on a call statement - stmt.callExpr?.let { processTaintConfiguration(it, stepScope, exprResolver) } + stmt.callExpr?.let { processTaintConfiguration(it, stepScope, simpleValueResolver) } // TODO add fields processing } @@ -241,15 +241,10 @@ class TaintAnalysis( val resolvedCondition = stepScope.ctx.mkAnd(resolvedConfigCondition, resolvedSinkCondition) - val (originalStateCopy, taintedStepScope) = stepScope.calcOnState { - val originalStateCopy = clone() - originalStateCopy to JcStepScope(originalStateCopy, UForkBlackList.createDefault()) - } - - taintedStepScope.assert(resolvedCondition)?.let { + stepScope.checkSat(resolvedCondition) { // TODO remove corresponding target - collectedStates += originalStateCopy - target?.propagate(taintedStepScope.state) + collectedStates += this + target?.propagate(this) } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt index 7d014e169a..992f713cfc 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt @@ -3,6 +3,7 @@ package org.usvm.machine import org.jacodb.api.cfg.JcAssignInst import org.jacodb.api.cfg.JcCallExpr import org.jacodb.api.cfg.JcCallInst +import org.jacodb.api.cfg.JcCatchInst import org.jacodb.api.cfg.JcEnterMonitorInst import org.jacodb.api.cfg.JcExitMonitorInst import org.jacodb.api.cfg.JcGotoInst @@ -15,14 +16,14 @@ import org.usvm.machine.interpreter.JcStepScope import org.usvm.statistics.UInterpreterObserver interface JcInterpreterObserver : UInterpreterObserver { - fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {} + fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {} fun onEntryPoint(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodEntrypointInst, stepScope: JcStepScope) fun onMethodCallWithUnresolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallExpr, stepScope: JcStepScope) {} fun onMethodCallWithResolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodCallBaseInst, stepScope: JcStepScope) {} fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) {} fun onReturnStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcReturnInst, stepScope: JcStepScope) {} fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {} - fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) {} + fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCatchInst, stepScope: JcStepScope) {} fun onSwitchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcSwitchInst, stepScope: JcStepScope) {} fun onThrowStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcThrowInst, stepScope: JcStepScope) {} fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {} From b51bac81dbf00e894dcaaf49703080799af7f840 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 15:56:51 +0300 Subject: [PATCH 3/9] Made a definition of checkers API --- .../org/usvm/api/checkers/UCheckersApi.kt | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt new file mode 100644 index 0000000000..c9f3e34a57 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt @@ -0,0 +1,40 @@ +package org.usvm.api.checkers + +import org.jacodb.api.JcClasspath +import org.jacodb.api.JcMethod +import org.jacodb.api.JcType +import org.jacodb.api.cfg.JcInstVisitor +import org.jacodb.api.cfg.JcValue +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UMachineOptions +import org.usvm.api.targets.JcTarget +import org.usvm.machine.JcContext +import org.usvm.memory.UReadOnlyMemory + +sealed interface UCheckResult { + // Has no data for now +} + +interface USatCheckResult : UCheckResult +interface UUnsatCheckResult : UCheckResult +interface UUnknownCheckResult : UCheckResult + +interface UCheckersApi { + val ctx: JcContext + val memory: UReadOnlyMemory + + fun resolveValue(value: JcValue): UExpr<*>? + fun checkSat(condition: UBoolExpr): UCheckResult + fun analyze( + method: JcMethod, + cp: JcClasspath, + checkersVisitor: JcInstVisitor, + targets: List = emptyList(), + options: UMachineOptions = UMachineOptions(), + ) + + companion object { + fun getApi(): UCheckersApi = UCheckersApiImpl() + } +} From dba779e60a063d1d05b32bbcf0b31acfd9e151b5 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 15:59:08 +0300 Subject: [PATCH 4/9] Filthy and hideous implementation of the checkers API --- .../org/usvm/api/checkers/UCheckersApiImpl.kt | 188 ++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt new file mode 100644 index 0000000000..0254333250 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt @@ -0,0 +1,188 @@ +package org.usvm.api.checkers + +import org.jacodb.api.JcClasspath +import org.jacodb.api.JcMethod +import org.jacodb.api.JcType +import org.jacodb.api.cfg.JcAssignInst +import org.jacodb.api.cfg.JcCallExpr +import org.jacodb.api.cfg.JcCallInst +import org.jacodb.api.cfg.JcCatchInst +import org.jacodb.api.cfg.JcEnterMonitorInst +import org.jacodb.api.cfg.JcExitMonitorInst +import org.jacodb.api.cfg.JcGotoInst +import org.jacodb.api.cfg.JcIfInst +import org.jacodb.api.cfg.JcInstVisitor +import org.jacodb.api.cfg.JcReturnInst +import org.jacodb.api.cfg.JcSwitchInst +import org.jacodb.api.cfg.JcThrowInst +import org.jacodb.api.cfg.JcValue +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UMachineOptions +import org.usvm.api.targets.JcTarget +import org.usvm.machine.JcContext +import org.usvm.machine.JcInterpreterObserver +import org.usvm.machine.JcMachine +import org.usvm.machine.JcMethodCallBaseInst +import org.usvm.machine.JcMethodEntrypointInst +import org.usvm.machine.interpreter.JcSimpleValueResolver +import org.usvm.machine.interpreter.JcStepScope +import org.usvm.memory.UReadOnlyMemory + +internal class UCheckersApiImpl : UCheckersApi { + // TODO How to retrieve it properly? + internal lateinit var context: JcContext + internal lateinit var exprResolver: JcSimpleValueResolver // TODO How to retrieve it properly? + internal lateinit var stepScope: JcStepScope // TODO How to retrieve it properly? + + override val ctx: JcContext + get() = context + + override val memory: UReadOnlyMemory + get() = stepScope.calcOnState { memory } + + override fun resolveValue(value: JcValue): UExpr<*> = value.accept(exprResolver) + + override fun checkSat(condition: UBoolExpr): UCheckResult { + stepScope.checkSat(condition) { + // Do nothing + } ?: return UUnsatCheckResultImpl + + return USatCheckResultImpl + } + + override fun analyze( + method: JcMethod, + cp: JcClasspath, + checkersVisitor: JcInstVisitor, + targets: List, + options: UMachineOptions, + ) { + val checkersObserver = VisitorWrapper(checkersVisitor, this) + val machine = JcMachine(cp, options, checkersObserver) + + machine.analyze(method, targets) + } +} + +internal object USatCheckResultImpl : USatCheckResult +internal object UUnsatCheckResultImpl : UUnsatCheckResult +internal object UUnknownSatCheckResultImpl : UUnknownCheckResult + +internal class VisitorWrapper( + private val visitor: JcInstVisitor, + private val usvmCheckersApi: UCheckersApiImpl, +) : JcInterpreterObserver { + override fun onAssignStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcAssignInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcAssignInst(stmt) } + } + + override fun onEntryPoint( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcMethodEntrypointInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { + // Looks like we do not need this signal in the ast-based checker + } + } + + override fun onMethodCallWithUnresolvedArguments( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcCallExpr, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { + // Looks like we do not need this signal in the ast-based checker + } + } + + override fun onMethodCallWithResolvedArguments( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcMethodCallBaseInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { + // Looks like we do not need this signal in the ast-based checker + } + } + + override fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcIfInst(stmt) } + } + + override fun onReturnStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcReturnInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcReturnInst(stmt) } + } + + override fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcGotoInst(stmt) } + } + + override fun onCatchStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcCatchInst, + stepScope: JcStepScope + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCatchInst(stmt) } + } + + override fun onSwitchStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcSwitchInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcSwitchInst(stmt) } + } + + override fun onThrowStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcThrowInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcThrowInst(stmt) } + } + + override fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCallInst(stmt) } + } + + override fun onEnterMonitorStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcEnterMonitorInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcEnterMonitorInst(stmt) } + } + + override fun onExitMonitorStatement( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcExitMonitorInst, + stepScope: JcStepScope, + ) { + withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcExitMonitorInst(stmt) } + } + + // TODO it's very dirty way to get required fields, rewrite + private fun withScopeAndResolver( + simpleValueResolver: JcSimpleValueResolver, + stepScope: JcStepScope, + blockOnStmt: () -> Unit + ) { + val ctx = stepScope.calcOnState { ctx } + + usvmCheckersApi.context = ctx + usvmCheckersApi.exprResolver = simpleValueResolver + usvmCheckersApi.stepScope = stepScope + + blockOnStmt() + } +} From b2089790d1ff601bf08bc08ada305f139fbc197c Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 16:00:48 +0300 Subject: [PATCH 5/9] Enabled sending signal on assignment statements with no call expressions --- .../main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt index b7f1184ab9..a556a4699f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt @@ -278,7 +278,7 @@ class JcInterpreter( is JcMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) is JcMethodResult.JcException -> error("Exceptions must be processed earlier") } - } + } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return val expr = exprResolver.resolveJcExpr(stmt.rhv, stmt.lhv.type) ?: return From 3290b738bed69b8d558fcfd210b2991422c5c394 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 16:01:47 +0300 Subject: [PATCH 6/9] Example of implementing checkers visitor and using checkers API (MUST NOT BE MERGED!) --- .../api/checkers/CheckersVisitorExample.kt | 90 +++++++++++++++++++ .../samples/checkers/DivisionExample.java | 35 ++++++++ .../samples/checkers/DivisionExampleTest.kt | 63 +++++++++++++ 3 files changed, 188 insertions(+) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java create mode 100644 usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt new file mode 100644 index 0000000000..8f776608c9 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt @@ -0,0 +1,90 @@ +package org.usvm.api.checkers + +import io.ksmt.utils.cast +import org.jacodb.api.JcClasspath +import org.jacodb.api.cfg.JcAssignInst +import org.jacodb.api.cfg.JcBinaryExpr +import org.jacodb.api.cfg.JcCallInst +import org.jacodb.api.cfg.JcCatchInst +import org.jacodb.api.cfg.JcDivExpr +import org.jacodb.api.cfg.JcEnterMonitorInst +import org.jacodb.api.cfg.JcExitMonitorInst +import org.jacodb.api.cfg.JcGotoInst +import org.jacodb.api.cfg.JcIfInst +import org.jacodb.api.cfg.JcInst +import org.jacodb.api.cfg.JcInstVisitor +import org.jacodb.api.cfg.JcRemExpr +import org.jacodb.api.cfg.JcReturnInst +import org.jacodb.api.cfg.JcSwitchInst +import org.jacodb.api.cfg.JcThrowInst +import org.jacodb.api.ext.int +import org.usvm.UBvSort + +// NOTE: THIS FILE MUST NOT BE MERGED! + +class CheckersVisitorExample( + private val usvmCheckersApi: UCheckersApi, + private val cp: JcClasspath, +) : JcInstVisitor { + override fun visitJcAssignInst(inst: JcAssignInst) { + val ctx = usvmCheckersApi.ctx + + val expr = inst.rhv + if (expr is JcBinaryExpr && (expr is JcDivExpr || expr is JcRemExpr) && expr.rhv.type == cp.int) { + val divider = usvmCheckersApi.resolveValue(expr.rhv) ?: return + val sort = divider.sort + if (sort !is UBvSort) { + return + } + + with(ctx) { + val eqZero = mkEq(divider.cast(), mkBv(42, sort)) + val satResult = usvmCheckersApi.checkSat(eqZero) + + if (satResult is USatCheckResult) { + println("Division by 42 found") + } + } + } + } + + override fun visitExternalJcInst(inst: JcInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcCallInst(inst: JcCallInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcCatchInst(inst: JcCatchInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcEnterMonitorInst(inst: JcEnterMonitorInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcExitMonitorInst(inst: JcExitMonitorInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcGotoInst(inst: JcGotoInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcIfInst(inst: JcIfInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcReturnInst(inst: JcReturnInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcSwitchInst(inst: JcSwitchInst) { + /*TODO("Not yet implemented")*/ + } + + override fun visitJcThrowInst(inst: JcThrowInst) { + /*TODO("Not yet implemented")*/ + } +} diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java new file mode 100644 index 0000000000..daa9f99c68 --- /dev/null +++ b/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java @@ -0,0 +1,35 @@ +package org.usvm.samples.checkers; + +// NOTE: THIS FILE MUST NOT BE MERGED! + +@SuppressWarnings("StatementWithEmptyBody") +public class DivisionExample { + void divideBy42Constant(int x) { + int divider = 42; + int result = x / divider; + System.out.println(result); + } + + void divideBySymbolic42(int divider) { + int result = 100 / divider; + System.out.println(result); + } + + void divideBySymbolic42TN(int divider) { + if (divider == 42) { + // Do nothing + } else { + int result = 100 / divider; + System.out.println(result); + } + } + + void divideBySymbolic42TP(int divider) { + if (divider != 42) { + // Do nothing + } else { + int result = 100 / divider; + System.out.println(result); + } + } +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt new file mode 100644 index 0000000000..e25e8f42ea --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt @@ -0,0 +1,63 @@ +package org.usvm.samples.checkers + +import org.jacodb.api.JcClasspath +import org.jacodb.api.ext.findClass +import org.jacodb.api.ext.toType +import org.junit.jupiter.api.Test +import org.usvm.api.checkers.CheckersVisitorExample +import org.usvm.api.checkers.UCheckersApi +import org.usvm.samples.JacoDBContainer +import kotlin.reflect.KFunction +import kotlin.reflect.jvm.javaConstructor +import kotlin.reflect.jvm.javaMethod + +// NOTE: THIS FILE MUST NOT BE MERGED! + +class DivisionExampleTest { + private fun makeClasspath(): JcClasspath = JacoDBContainer("tests`").cp + + @Test + fun analyzeConstant() { + val cp = makeClasspath() + val api = UCheckersApi.getApi() + val checkersVisitor = CheckersVisitorExample(api, cp) + + val method = DivisionExample::divideBy42Constant + val declaringClassName = requireNotNull(method.declaringClass?.name) + val jcClass = cp.findClass(declaringClassName).toType() + val jcMethod = jcClass.declaredMethods.first { it.name == method.name } + + api.analyze(jcMethod.method, cp, checkersVisitor) + } + + @Test + fun analyzeTN() { + val cp = makeClasspath() + val api = UCheckersApi.getApi() + val checkersVisitor = CheckersVisitorExample(api, cp) + + val method = DivisionExample::divideBySymbolic42TN + val declaringClassName = requireNotNull(method.declaringClass?.name) + val jcClass = cp.findClass(declaringClassName).toType() + val jcMethod = jcClass.declaredMethods.first { it.name == method.name } + + api.analyze(jcMethod.method, cp, checkersVisitor) + } + + @Test + fun analyzeSymbolic() { + val cp = makeClasspath() + val api = UCheckersApi.getApi() + val checkersVisitor = CheckersVisitorExample(api, cp) + + val method = DivisionExample::divideBySymbolic42 + val declaringClassName = requireNotNull(method.declaringClass?.name) + val jcClass = cp.findClass(declaringClassName).toType() + val jcMethod = jcClass.declaredMethods.first { it.name == method.name } + + api.analyze(jcMethod.method, cp, checkersVisitor) + } + + private val KFunction<*>.declaringClass: Class<*>? + get() = (javaMethod ?: javaConstructor)?.declaringClass +} From 174d2243d58f0d2ab837771629b77a0444f96611 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Tue, 3 Oct 2023 20:25:44 +0300 Subject: [PATCH 7/9] Clarified --- .../src/main/kotlin/org/usvm/StepScope.kt | 6 +- .../kotlin/org/usvm/api/checkers/JcChecker.kt | 50 +++++++++++++ .../{UCheckersApiImpl.kt => JcCheckerImpl.kt} | 71 +++++++++---------- .../org/usvm/api/checkers/UCheckersApi.kt | 40 ----------- .../org/usvm/api/targets/TaintAnalysis.kt | 6 +- .../samples/checkers/DivisionExampleTest.kt | 24 +++---- .../usvm/samples/checkers/JcDiv42Checker.kt} | 64 ++++++++++------- 7 files changed, 140 insertions(+), 121 deletions(-) create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt rename usvm-jvm/src/main/kotlin/org/usvm/api/checkers/{UCheckersApiImpl.kt => JcCheckerImpl.kt} (76%) delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt rename usvm-jvm/src/{main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt => test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt} (60%) diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index b2fbcefaf4..8baf918f2d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -208,14 +208,12 @@ class StepScope, Type, Statement, } // TODO docs - fun checkSat(condition: UBoolExpr, blockOnSatState: T.() -> Unit = { }): Unit? { - // TODO should we check step flags here? - + fun checkSat(condition: UBoolExpr): T? { val conditionalState = originalState.clone() val conditionalScope = StepScope(conditionalState, forkBlackList) return conditionalScope.assert(condition)?.let { - blockOnSatState(conditionalState) + conditionalState } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt new file mode 100644 index 0000000000..29226cfac7 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt @@ -0,0 +1,50 @@ +package org.usvm.api.checkers + +import org.jacodb.api.JcClasspath +import org.jacodb.api.JcMethod +import org.jacodb.api.JcType +import org.jacodb.api.cfg.JcInstVisitor +import org.jacodb.api.cfg.JcValue +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UMachineOptions +import org.usvm.api.targets.JcTarget +import org.usvm.machine.JcContext +import org.usvm.machine.JcMachine +import org.usvm.memory.UReadOnlyMemory + +sealed interface JcCheckerResult { + // Has no data for now +} + +interface JcCheckerSatResult : JcCheckerResult +interface JcCheckerUnsatResult : JcCheckerResult +interface JcCheckerUnknownResult : JcCheckerResult + +interface JcCheckerApi { + val ctx: JcContext + val memory: UReadOnlyMemory + + fun resolveValue(value: JcValue): UExpr<*> + fun checkSat(condition: UBoolExpr): JcCheckerResult +} + +class JcCheckerRunner(val cp: JcClasspath) { + private val apiImpl = JcCheckerApiImpl() + + val api: JcCheckerApi + get() = apiImpl + + fun runChecker( + entryPoint: JcMethod, + checkersVisitor: JcInstVisitor, + targets: List = emptyList(), + options: UMachineOptions = UMachineOptions(), + ) { + val checkersObserver = JcCheckerObserver(checkersVisitor, apiImpl) + + JcMachine(cp, options, checkersObserver).use { machine -> + machine.analyze(entryPoint, targets) + } + } +} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt similarity index 76% rename from usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt rename to usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt index 0254333250..18129090e4 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApiImpl.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt @@ -1,7 +1,5 @@ package org.usvm.api.checkers -import org.jacodb.api.JcClasspath -import org.jacodb.api.JcMethod import org.jacodb.api.JcType import org.jacodb.api.cfg.JcAssignInst import org.jacodb.api.cfg.JcCallExpr @@ -18,60 +16,59 @@ import org.jacodb.api.cfg.JcThrowInst import org.jacodb.api.cfg.JcValue import org.usvm.UBoolExpr import org.usvm.UExpr -import org.usvm.UMachineOptions -import org.usvm.api.targets.JcTarget import org.usvm.machine.JcContext import org.usvm.machine.JcInterpreterObserver -import org.usvm.machine.JcMachine import org.usvm.machine.JcMethodCallBaseInst import org.usvm.machine.JcMethodEntrypointInst import org.usvm.machine.interpreter.JcSimpleValueResolver import org.usvm.machine.interpreter.JcStepScope import org.usvm.memory.UReadOnlyMemory -internal class UCheckersApiImpl : UCheckersApi { +internal class JcCheckerApiImpl : JcCheckerApi { // TODO How to retrieve it properly? - internal lateinit var context: JcContext - internal lateinit var exprResolver: JcSimpleValueResolver // TODO How to retrieve it properly? - internal lateinit var stepScope: JcStepScope // TODO How to retrieve it properly? + private var internalStepScope: JcStepScope? = null + private var internalExprResolver: JcSimpleValueResolver? = null + + private val stepScope: JcStepScope + get() = ensureProcessing(internalStepScope) + + private val exprResolver: JcSimpleValueResolver + get() = ensureProcessing(internalExprResolver) + + private fun ensureProcessing(e: T?): T = + e ?: error("Checker API can be used during instruction processing only") override val ctx: JcContext - get() = context + get() = stepScope.calcOnState { ctx } override val memory: UReadOnlyMemory get() = stepScope.calcOnState { memory } override fun resolveValue(value: JcValue): UExpr<*> = value.accept(exprResolver) - override fun checkSat(condition: UBoolExpr): UCheckResult { - stepScope.checkSat(condition) { - // Do nothing - } ?: return UUnsatCheckResultImpl + override fun checkSat(condition: UBoolExpr): JcCheckerResult = + stepScope.checkSat(condition)?.let { + JcCheckerSatResultImpl + } ?: JcCheckerUnsatResultImpl - return USatCheckResultImpl + internal fun setResolverAndScope(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) { + internalExprResolver = simpleValueResolver + internalStepScope = stepScope } - override fun analyze( - method: JcMethod, - cp: JcClasspath, - checkersVisitor: JcInstVisitor, - targets: List, - options: UMachineOptions, - ) { - val checkersObserver = VisitorWrapper(checkersVisitor, this) - val machine = JcMachine(cp, options, checkersObserver) - - machine.analyze(method, targets) + internal fun resetResolverAndScope() { + internalStepScope = null + internalExprResolver = null } } -internal object USatCheckResultImpl : USatCheckResult -internal object UUnsatCheckResultImpl : UUnsatCheckResult -internal object UUnknownSatCheckResultImpl : UUnknownCheckResult +internal object JcCheckerSatResultImpl : JcCheckerSatResult +internal object JcCheckerUnsatResultImpl : JcCheckerUnsatResult +internal object JcCheckerUnknownSatResultImpl : JcCheckerUnknownResult -internal class VisitorWrapper( +internal class JcCheckerObserver( private val visitor: JcInstVisitor, - private val usvmCheckersApi: UCheckersApiImpl, + private val jcCheckerApi: JcCheckerApiImpl, ) : JcInterpreterObserver { override fun onAssignStatement( simpleValueResolver: JcSimpleValueResolver, @@ -172,17 +169,15 @@ internal class VisitorWrapper( } // TODO it's very dirty way to get required fields, rewrite - private fun withScopeAndResolver( + private inline fun withScopeAndResolver( simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope, blockOnStmt: () -> Unit - ) { - val ctx = stepScope.calcOnState { ctx } - - usvmCheckersApi.context = ctx - usvmCheckersApi.exprResolver = simpleValueResolver - usvmCheckersApi.stepScope = stepScope + ) = try { + jcCheckerApi.setResolverAndScope(simpleValueResolver, stepScope) blockOnStmt() + } finally { + jcCheckerApi.resetResolverAndScope() } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt deleted file mode 100644 index c9f3e34a57..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/UCheckersApi.kt +++ /dev/null @@ -1,40 +0,0 @@ -package org.usvm.api.checkers - -import org.jacodb.api.JcClasspath -import org.jacodb.api.JcMethod -import org.jacodb.api.JcType -import org.jacodb.api.cfg.JcInstVisitor -import org.jacodb.api.cfg.JcValue -import org.usvm.UBoolExpr -import org.usvm.UExpr -import org.usvm.UMachineOptions -import org.usvm.api.targets.JcTarget -import org.usvm.machine.JcContext -import org.usvm.memory.UReadOnlyMemory - -sealed interface UCheckResult { - // Has no data for now -} - -interface USatCheckResult : UCheckResult -interface UUnsatCheckResult : UCheckResult -interface UUnknownCheckResult : UCheckResult - -interface UCheckersApi { - val ctx: JcContext - val memory: UReadOnlyMemory - - fun resolveValue(value: JcValue): UExpr<*>? - fun checkSat(condition: UBoolExpr): UCheckResult - fun analyze( - method: JcMethod, - cp: JcClasspath, - checkersVisitor: JcInstVisitor, - targets: List = emptyList(), - options: UMachineOptions = UMachineOptions(), - ) - - companion object { - fun getApi(): UCheckersApi = UCheckersApiImpl() - } -} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt index 82bcde803d..10bf4c0cf3 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt @@ -241,10 +241,10 @@ class TaintAnalysis( val resolvedCondition = stepScope.ctx.mkAnd(resolvedConfigCondition, resolvedSinkCondition) - stepScope.checkSat(resolvedCondition) { + stepScope.checkSat(resolvedCondition)?.let { taintedState -> // TODO remove corresponding target - collectedStates += this - target?.propagate(this) + collectedStates += taintedState + target?.propagate(taintedState) } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt index e25e8f42ea..6fb81ec3b7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt @@ -4,9 +4,9 @@ import org.jacodb.api.JcClasspath import org.jacodb.api.ext.findClass import org.jacodb.api.ext.toType import org.junit.jupiter.api.Test -import org.usvm.api.checkers.CheckersVisitorExample -import org.usvm.api.checkers.UCheckersApi +import org.usvm.api.checkers.JcCheckerRunner import org.usvm.samples.JacoDBContainer +import org.usvm.samples.samplesKey import kotlin.reflect.KFunction import kotlin.reflect.jvm.javaConstructor import kotlin.reflect.jvm.javaMethod @@ -14,48 +14,48 @@ import kotlin.reflect.jvm.javaMethod // NOTE: THIS FILE MUST NOT BE MERGED! class DivisionExampleTest { - private fun makeClasspath(): JcClasspath = JacoDBContainer("tests`").cp + private fun makeClasspath(): JcClasspath = JacoDBContainer(samplesKey).cp @Test fun analyzeConstant() { val cp = makeClasspath() - val api = UCheckersApi.getApi() - val checkersVisitor = CheckersVisitorExample(api, cp) + val runner = JcCheckerRunner(cp) + val checker = JcDiv42Checker(runner.api, cp) val method = DivisionExample::divideBy42Constant val declaringClassName = requireNotNull(method.declaringClass?.name) val jcClass = cp.findClass(declaringClassName).toType() val jcMethod = jcClass.declaredMethods.first { it.name == method.name } - api.analyze(jcMethod.method, cp, checkersVisitor) + runner.runChecker(jcMethod.method, checker) } @Test fun analyzeTN() { val cp = makeClasspath() - val api = UCheckersApi.getApi() - val checkersVisitor = CheckersVisitorExample(api, cp) + val checker = JcCheckerRunner(cp) + val checkersVisitor = JcDiv42Checker(checker.api, cp) val method = DivisionExample::divideBySymbolic42TN val declaringClassName = requireNotNull(method.declaringClass?.name) val jcClass = cp.findClass(declaringClassName).toType() val jcMethod = jcClass.declaredMethods.first { it.name == method.name } - api.analyze(jcMethod.method, cp, checkersVisitor) + checker.runChecker(jcMethod.method, checkersVisitor) } @Test fun analyzeSymbolic() { val cp = makeClasspath() - val api = UCheckersApi.getApi() - val checkersVisitor = CheckersVisitorExample(api, cp) + val checker = JcCheckerRunner(cp) + val checkersVisitor = JcDiv42Checker(checker.api, cp) val method = DivisionExample::divideBySymbolic42 val declaringClassName = requireNotNull(method.declaringClass?.name) val jcClass = cp.findClass(declaringClassName).toType() val jcMethod = jcClass.declaredMethods.first { it.name == method.name } - api.analyze(jcMethod.method, cp, checkersVisitor) + checker.runChecker(jcMethod.method, checkersVisitor) } private val KFunction<*>.declaringClass: Class<*>? diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt similarity index 60% rename from usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt rename to usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt index 8f776608c9..e52ed35f2c 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/CheckersVisitorExample.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt @@ -1,6 +1,6 @@ -package org.usvm.api.checkers +package org.usvm.samples.checkers -import io.ksmt.utils.cast +import io.ksmt.utils.asExpr import org.jacodb.api.JcClasspath import org.jacodb.api.cfg.JcAssignInst import org.jacodb.api.cfg.JcBinaryExpr @@ -18,33 +18,29 @@ import org.jacodb.api.cfg.JcReturnInst import org.jacodb.api.cfg.JcSwitchInst import org.jacodb.api.cfg.JcThrowInst import org.jacodb.api.ext.int -import org.usvm.UBvSort +import org.usvm.UBoolExpr +import org.usvm.api.checkers.JcCheckerApi +import org.usvm.api.checkers.JcCheckerSatResult // NOTE: THIS FILE MUST NOT BE MERGED! -class CheckersVisitorExample( - private val usvmCheckersApi: UCheckersApi, - private val cp: JcClasspath, -) : JcInstVisitor { +interface JcAssignInstChecker : JcInstVisitor { + val api: JcCheckerApi + + fun matchAst(inst: JcAssignInst): Boolean + + fun checkSymbolic(inst: JcAssignInst): UBoolExpr + + fun reportError(inst: JcAssignInst) + override fun visitJcAssignInst(inst: JcAssignInst) { - val ctx = usvmCheckersApi.ctx + if (!matchAst(inst)) return - val expr = inst.rhv - if (expr is JcBinaryExpr && (expr is JcDivExpr || expr is JcRemExpr) && expr.rhv.type == cp.int) { - val divider = usvmCheckersApi.resolveValue(expr.rhv) ?: return - val sort = divider.sort - if (sort !is UBvSort) { - return - } - - with(ctx) { - val eqZero = mkEq(divider.cast(), mkBv(42, sort)) - val satResult = usvmCheckersApi.checkSat(eqZero) - - if (satResult is USatCheckResult) { - println("Division by 42 found") - } - } + val symbolicConstraint = checkSymbolic(inst) + val satResult = api.checkSat(symbolicConstraint) + + if (satResult is JcCheckerSatResult) { + reportError(inst) } } @@ -88,3 +84,23 @@ class CheckersVisitorExample( /*TODO("Not yet implemented")*/ } } + +class JcDiv42Checker( + override val api: JcCheckerApi, + private val cp: JcClasspath, +) : JcAssignInstChecker { + override fun matchAst(inst: JcAssignInst): Boolean { + val expr = inst.rhv + return expr is JcBinaryExpr && (expr is JcDivExpr || expr is JcRemExpr) && expr.rhv.type == cp.int + } + + override fun checkSymbolic(inst: JcAssignInst): UBoolExpr = with(api.ctx) { + val expr = inst.rhv as JcBinaryExpr + val divider = api.resolveValue(expr.rhv).asExpr(integerSort) + mkEq(divider, mkBv(42, divider.sort)) + } + + override fun reportError(inst: JcAssignInst) { + println("Division by 42 found") + } +} From 006b0b81dcc094000d9a5f9d5058637abfa9254b Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Wed, 4 Oct 2023 13:34:50 +0300 Subject: [PATCH 8/9] Extended tests --- .../samples/checkers/DivisionExample.java | 75 +++++++++--- .../org/usvm/samples/JavaMethodTestRunner.kt | 5 +- .../samples/checkers/DivisionExampleTest.kt | 114 +++++++++++++----- .../usvm/samples/checkers/JcDiv42Checker.kt | 7 +- .../src/test/kotlin/org/usvm/util/Util.kt | 4 + 5 files changed, 150 insertions(+), 55 deletions(-) diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java index daa9f99c68..dd16b1f518 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java @@ -1,35 +1,80 @@ package org.usvm.samples.checkers; -// NOTE: THIS FILE MUST NOT BE MERGED! - -@SuppressWarnings("StatementWithEmptyBody") +@SuppressWarnings({"UnnecessaryLocalVariable"}) public class DivisionExample { - void divideBy42Constant(int x) { + int divideBy42ConstantSinglePath(int x) { int divider = 42; int result = x / divider; - System.out.println(result); + + return result; + } + + int divideBy42ConstantBranching(int x, boolean condition) { + int divider = 42; + + final int result; + if (condition) { + result = x / divider; + } else { + result = (x + 1) / divider; + } + + return result; + } + + @SuppressWarnings("ConstantValue") + int divideBy42ConstantWithUnreachableBranch(int x, boolean condition) { + int divider = 42; + + final int result; + if (condition && !condition) { + // Unreachable branch + result = x / divider; + } else { + result = (x + 1) / divider; + } + + return result; } - void divideBySymbolic42(int divider) { + int divideBySymbolic42SinglePath(int divider) { int result = 100 / divider; - System.out.println(result); + + return result; } - void divideBySymbolic42TN(int divider) { + int divideBySymbolic42TrueNegative(int divider) { if (divider == 42) { - // Do nothing + return -42; } else { int result = 100 / divider; - System.out.println(result); + + return result; } } - void divideBySymbolic42TP(int divider) { - if (divider != 42) { - // Do nothing + int divideBySymbolic42Branching(int divider, boolean condition) { + final int result; + if (condition) { + result = (divider + 1) / divider; } else { - int result = 100 / divider; - System.out.println(result); + result = 100 / divider; } + + return result; + } + + int divideBySymbolic42FalsePositive(int divider) { + int nonNegativeValue = Math.abs(divider); + + final int result; + if (nonNegativeValue < 0) { + // Unreachable branch + result = 100 / divider; + } else { + result = 0; + } + + return result; } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt index 84f26412c2..13ff829665 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt @@ -16,6 +16,7 @@ import org.usvm.machine.JcMachine import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults +import org.usvm.util.declaringClass import kotlin.reflect.KClass import kotlin.reflect.KFunction import kotlin.reflect.KFunction1 @@ -24,7 +25,6 @@ import kotlin.reflect.KFunction3 import kotlin.reflect.KFunction4 import kotlin.reflect.full.instanceParameter import kotlin.reflect.jvm.javaConstructor -import kotlin.reflect.jvm.javaMethod @TestInstance(TestInstance.Lifecycle.PER_CLASS) @@ -775,6 +775,3 @@ open class JavaMethodTestRunner : TestRunner, KClass<*>?, J } } } - -private val KFunction<*>.declaringClass: Class<*>? - get() = (javaMethod ?: javaConstructor)?.declaringClass diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt index 6fb81ec3b7..ea2f2c1b12 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt @@ -1,63 +1,111 @@ package org.usvm.samples.checkers import org.jacodb.api.JcClasspath +import org.jacodb.api.JcParameter +import org.jacodb.api.JcTypedMethod +import org.jacodb.api.cfg.JcAssignInst +import org.jacodb.api.cfg.JcDivExpr import org.jacodb.api.ext.findClass import org.jacodb.api.ext.toType import org.junit.jupiter.api.Test import org.usvm.api.checkers.JcCheckerRunner import org.usvm.samples.JacoDBContainer import org.usvm.samples.samplesKey +import org.usvm.util.declaringClass import kotlin.reflect.KFunction -import kotlin.reflect.jvm.javaConstructor -import kotlin.reflect.jvm.javaMethod - -// NOTE: THIS FILE MUST NOT BE MERGED! +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertIsNot class DivisionExampleTest { - private fun makeClasspath(): JcClasspath = JacoDBContainer(samplesKey).cp + private val cp: JcClasspath = JacoDBContainer(samplesKey).cp @Test - fun analyzeConstant() { - val cp = makeClasspath() - val runner = JcCheckerRunner(cp) - val checker = JcDiv42Checker(runner.api, cp) + fun analyzeConstantSinglePath() { + val jcMethod = DivisionExample::divideBy42ConstantSinglePath.jcMethod + val targetStatements = runChecker(jcMethod) - val method = DivisionExample::divideBy42Constant - val declaringClassName = requireNotNull(method.declaringClass?.name) - val jcClass = cp.findClass(declaringClassName).toType() - val jcMethod = jcClass.declaredMethods.first { it.name == method.name } + assertEquals(1, targetStatements.size) - runner.runChecker(jcMethod.method, checker) + val value = targetStatements.single().rhv + assertIs(value) } @Test - fun analyzeTN() { - val cp = makeClasspath() - val checker = JcCheckerRunner(cp) - val checkersVisitor = JcDiv42Checker(checker.api, cp) + fun analyzeConstantBranching() { + val jcMethod = DivisionExample::divideBy42ConstantBranching.jcMethod + val targetStatements = runChecker(jcMethod) - val method = DivisionExample::divideBySymbolic42TN - val declaringClassName = requireNotNull(method.declaringClass?.name) - val jcClass = cp.findClass(declaringClassName).toType() - val jcMethod = jcClass.declaredMethods.first { it.name == method.name } + assertEquals(2, targetStatements.size) - checker.runChecker(jcMethod.method, checkersVisitor) + targetStatements.forEach { assertIs(it.rhv) } + } + + @Test + fun analyzeConstantUnreachableBranch() { + val jcMethod = DivisionExample::divideBy42ConstantWithUnreachableBranch.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(1, targetStatements.size) + + val value = targetStatements.single().rhv + assertIs(value) + + val leftPartOfDivision = value.lhv + assertIsNot(leftPartOfDivision) + } + + @Test + fun analyzeSymbolicSinglePath() { + val jcMethod = DivisionExample::divideBySymbolic42SinglePath.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(1, targetStatements.size) + + val value = targetStatements.single().rhv + assertIs(value) + } + + @Test + fun analyzeSymbolicTrueNegative() { + val jcMethod = DivisionExample::divideBySymbolic42TrueNegative.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(0, targetStatements.size) + } + + @Test + fun analyzeSymbolicBranching() { + val jcMethod = DivisionExample::divideBySymbolic42Branching.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(2, targetStatements.size) + + targetStatements.forEach { assertIs(it.rhv) } } @Test - fun analyzeSymbolic() { - val cp = makeClasspath() + fun analyzeSymbolicFalsePositive() { + val jcMethod = DivisionExample::divideBySymbolic42FalsePositive.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(0, targetStatements.size) + } + + private val KFunction<*>.jcMethod: JcTypedMethod + get() { + val declaringClassName = requireNotNull(declaringClass?.name) + val jcClass = cp.findClass(declaringClassName).toType() + + return jcClass.declaredMethods.first { it.name == name } + } + + private fun runChecker(jcMethod: JcTypedMethod): Set { val checker = JcCheckerRunner(cp) val checkersVisitor = JcDiv42Checker(checker.api, cp) - val method = DivisionExample::divideBySymbolic42 - val declaringClassName = requireNotNull(method.declaringClass?.name) - val jcClass = cp.findClass(declaringClassName).toType() - val jcMethod = jcClass.declaredMethods.first { it.name == method.name } - checker.runChecker(jcMethod.method, checkersVisitor) - } - private val KFunction<*>.declaringClass: Class<*>? - get() = (javaMethod ?: javaConstructor)?.declaringClass + return checkersVisitor.targetStatements + } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt index e52ed35f2c..8fc4235d84 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt @@ -22,8 +22,6 @@ import org.usvm.UBoolExpr import org.usvm.api.checkers.JcCheckerApi import org.usvm.api.checkers.JcCheckerSatResult -// NOTE: THIS FILE MUST NOT BE MERGED! - interface JcAssignInstChecker : JcInstVisitor { val api: JcCheckerApi @@ -89,6 +87,9 @@ class JcDiv42Checker( override val api: JcCheckerApi, private val cp: JcClasspath, ) : JcAssignInstChecker { + private val _targetStatements: MutableSet = mutableSetOf() + val targetStatements: Set = _targetStatements + override fun matchAst(inst: JcAssignInst): Boolean { val expr = inst.rhv return expr is JcBinaryExpr && (expr is JcDivExpr || expr is JcRemExpr) && expr.rhv.type == cp.int @@ -101,6 +102,6 @@ class JcDiv42Checker( } override fun reportError(inst: JcAssignInst) { - println("Division by 42 found") + _targetStatements += inst } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/util/Util.kt b/usvm-jvm/src/test/kotlin/org/usvm/util/Util.kt index c48250ad9c..2f79eea4d0 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/util/Util.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/util/Util.kt @@ -6,6 +6,7 @@ import org.jacodb.api.ext.findClass import org.jacodb.api.ext.toType import java.io.File import kotlin.reflect.KFunction +import kotlin.reflect.jvm.javaConstructor import kotlin.reflect.jvm.javaMethod val allClasspath: List @@ -27,3 +28,6 @@ fun JcClasspath.getJcMethodByName(func: KFunction<*>): JcMethod { } inline fun Result<*>.isException(): Boolean = exceptionOrNull() is T + +internal val KFunction<*>.declaringClass: Class<*>? + get() = (javaMethod ?: javaConstructor)?.declaringClass From 55078625fe09595cc195323dcb017f91675fec45 Mon Sep 17 00:00:00 2001 From: Yury Kamenev Date: Wed, 4 Oct 2023 13:39:17 +0300 Subject: [PATCH 9/9] Added docs for `checkSat` --- usvm-core/src/main/kotlin/org/usvm/StepScope.kt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index 8baf918f2d..2faeeac528 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -207,7 +207,10 @@ class StepScope, Type, Statement, return forkMulti(filteredConditionsWithBlockOnStates) } - // TODO docs + /** + * [assert]s the [condition] on the scope with the cloned [originalState]. Returns this cloned state, if this [condition] + * is satisfiable, and returns `null` otherwise. + */ fun checkSat(condition: UBoolExpr): T? { val conditionalState = originalState.clone() val conditionalScope = StepScope(conditionalState, forkBlackList)