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..2faeeac528 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -207,6 +207,19 @@ class StepScope, Type, Statement, return forkMulti(filteredConditionsWithBlockOnStates) } + /** + * [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) + + return conditionalScope.assert(condition)?.let { + conditionalState + } + } + /** * Represents the current state of this [StepScope]. */ 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/JcCheckerImpl.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt new file mode 100644 index 0000000000..18129090e4 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt @@ -0,0 +1,183 @@ +package org.usvm.api.checkers + +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.machine.JcContext +import org.usvm.machine.JcInterpreterObserver +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 JcCheckerApiImpl : JcCheckerApi { + // 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() = 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): JcCheckerResult = + stepScope.checkSat(condition)?.let { + JcCheckerSatResultImpl + } ?: JcCheckerUnsatResultImpl + + internal fun setResolverAndScope(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) { + internalExprResolver = simpleValueResolver + internalStepScope = stepScope + } + + internal fun resetResolverAndScope() { + internalStepScope = null + internalExprResolver = null + } +} + +internal object JcCheckerSatResultImpl : JcCheckerSatResult +internal object JcCheckerUnsatResultImpl : JcCheckerUnsatResult +internal object JcCheckerUnknownSatResultImpl : JcCheckerUnknownResult + +internal class JcCheckerObserver( + private val visitor: JcInstVisitor, + private val jcCheckerApi: JcCheckerApiImpl, +) : 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 inline fun withScopeAndResolver( + simpleValueResolver: JcSimpleValueResolver, + stepScope: JcStepScope, + blockOnStmt: () -> Unit + ) = try { + jcCheckerApi.setResolverAndScope(simpleValueResolver, stepScope) + + blockOnStmt() + } finally { + jcCheckerApi.resetResolverAndScope() + } +} 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..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 @@ -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)?.let { taintedState -> // TODO remove corresponding target - collectedStates += originalStateCopy - target?.propagate(taintedStepScope.state) + collectedStates += taintedState + target?.propagate(taintedState) } } 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) {} 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 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..dd16b1f518 --- /dev/null +++ b/usvm-jvm/src/samples/java/org/usvm/samples/checkers/DivisionExample.java @@ -0,0 +1,80 @@ +package org.usvm.samples.checkers; + +@SuppressWarnings({"UnnecessaryLocalVariable"}) +public class DivisionExample { + int divideBy42ConstantSinglePath(int x) { + int divider = 42; + int result = x / divider; + + 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; + } + + int divideBySymbolic42SinglePath(int divider) { + int result = 100 / divider; + + return result; + } + + int divideBySymbolic42TrueNegative(int divider) { + if (divider == 42) { + return -42; + } else { + int result = 100 / divider; + + return result; + } + } + + int divideBySymbolic42Branching(int divider, boolean condition) { + final int result; + if (condition) { + result = (divider + 1) / divider; + } else { + 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 new file mode 100644 index 0000000000..ea2f2c1b12 --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/DivisionExampleTest.kt @@ -0,0 +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.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertIsNot + +class DivisionExampleTest { + private val cp: JcClasspath = JacoDBContainer(samplesKey).cp + + @Test + fun analyzeConstantSinglePath() { + val jcMethod = DivisionExample::divideBy42ConstantSinglePath.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(1, targetStatements.size) + + val value = targetStatements.single().rhv + assertIs(value) + } + + @Test + fun analyzeConstantBranching() { + val jcMethod = DivisionExample::divideBy42ConstantBranching.jcMethod + val targetStatements = runChecker(jcMethod) + + assertEquals(2, targetStatements.size) + + 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 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) + + checker.runChecker(jcMethod.method, checkersVisitor) + + 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 new file mode 100644 index 0000000000..8fc4235d84 --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/checkers/JcDiv42Checker.kt @@ -0,0 +1,107 @@ +package org.usvm.samples.checkers + +import io.ksmt.utils.asExpr +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.UBoolExpr +import org.usvm.api.checkers.JcCheckerApi +import org.usvm.api.checkers.JcCheckerSatResult + +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) { + if (!matchAst(inst)) return + + val symbolicConstraint = checkSymbolic(inst) + val satResult = api.checkSat(symbolicConstraint) + + if (satResult is JcCheckerSatResult) { + reportError(inst) + } + } + + 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")*/ + } +} + +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 + } + + 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) { + _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