From 0376cf5faf20c7f8bceeb4f9f837ea14017ba1eb Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 19 Sep 2023 22:29:14 +0300 Subject: [PATCH] Remove redundant code --- .../src/main/kotlin/org/usvm/UComponents.kt | 2 +- .../src/main/kotlin/org/usvm/api/MemoryApi.kt | 2 - .../usvm/collection/set/ref/URefSetUtil.kt | 13 -- .../src/main/kotlin/org/usvm/solver/Solver.kt | 18 +-- .../usvm/statistics/UInterpreterObserver.kt | 2 +- .../org/usvm/targets/UTargetController.kt | 1 - .../api/targets/JcInputTaintMarkReading.kt | 41 ------ .../org/usvm/api/targets/TaintAnalysis.kt | 80 ++++------ .../api/targets/TaintConfigurationItem.kt | 18 ++- .../org/usvm/api/targets/TaintMarkRegion.kt | 137 ------------------ .../kotlin/org/usvm/machine/JcComponents.kt | 16 +- .../kotlin/org/usvm/machine/JcComposer.kt | 17 --- .../main/kotlin/org/usvm/machine/JcContext.kt | 17 --- .../org/usvm/machine/JcExprTranslator.kt | 28 ---- .../org/usvm/machine/JcInterpreterObserver.kt | 9 +- .../main/kotlin/org/usvm/machine/JcMachine.kt | 1 - .../main/kotlin/org/usvm/machine/JcModel.kt | 21 --- .../main/kotlin/org/usvm/machine/JcSolver.kt | 38 ----- .../usvm/machine/JcTaintMarkRegionDecoder.kt | 61 -------- .../org/usvm/machine/JcTaintsModelRegion.kt | 40 ----- .../kotlin/org/usvm/machine/JcTransformer.kt | 12 -- .../usvm/machine/interpreter/JcInterpreter.kt | 17 +-- .../kotlin/org/usvm/machine/state/JcState.kt | 2 +- .../usvm/samples/codegen/JavaAssertTest.kt | 1 - .../org/usvm/samples/taint/TaintTest.kt | 36 ++--- .../samples/wrappers/BooleanWrapperTest.kt | 1 - .../kotlin/org/usvm/machine/SampleMachine.kt | 2 +- 27 files changed, 71 insertions(+), 562 deletions(-) delete mode 100644 usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetUtil.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/targets/JcInputTaintMarkReading.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintMarkRegion.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcComposer.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprTranslator.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcModel.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolver.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintMarkRegionDecoder.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintsModelRegion.kt delete mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt diff --git a/usvm-core/src/main/kotlin/org/usvm/UComponents.kt b/usvm-core/src/main/kotlin/org/usvm/UComponents.kt index be37cdded4..80e34e9d2d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/UComponents.kt +++ b/usvm-core/src/main/kotlin/org/usvm/UComponents.kt @@ -8,7 +8,7 @@ import org.usvm.types.UTypeSystem /** * Provides core USVM components tuned for specific language. - * Instatiated once per [UContext]. + * Instantiated once per [UContext]. */ interface UComponents { fun mkSolver(ctx: UContext): USolverBase diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt index a838dd3b31..bd79790898 100644 --- a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt @@ -44,8 +44,6 @@ fun UWritableMemory<*>.writeArrayIndex( ref: UHeapRef, index: USizeExpr, type: ArrayType, sort: Sort, value: UExpr, guard: UBoolExpr ) = write(UArrayIndexLValue(sort, ref, index, type), value, guard) -// TODO move it here - fun UWritableMemory<*>.writeArrayLength( ref: UHeapRef, size: USizeExpr, arrayType: ArrayType ) = write(UArrayLengthLValue(ref, arrayType), size, ref.uctx.trueExpr) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetUtil.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetUtil.kt deleted file mode 100644 index ee1dd44f99..0000000000 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetUtil.kt +++ /dev/null @@ -1,13 +0,0 @@ -package org.usvm.collection.set.ref - -import org.usvm.UBoolExpr -import org.usvm.uctx - -// TODO replace with memory -fun URefSetRegion.addInSet(key: URefSetEntryLValue, guard: UBoolExpr) { - write(key, guard.uctx.trueExpr, guard) -} - -fun URefSetRegion.removeFromSet(key: URefSetEntryLValue, guard: UBoolExpr) { - write(key, guard.uctx.falseExpr, guard) -} diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt index b5bd61087c..8d74096108 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt @@ -7,17 +7,12 @@ import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UHeapRef -import org.usvm.UMockEvaluator import org.usvm.constraints.UEqualityConstraints import org.usvm.constraints.UPathConstraints import org.usvm.isFalse import org.usvm.isTrue -import org.usvm.memory.UMemoryRegionId -import org.usvm.memory.UReadOnlyMemoryRegion -import org.usvm.memory.UReadOnlyRegistersStack import org.usvm.model.UModelBase import org.usvm.model.UModelDecoder -import org.usvm.model.UTypeModel sealed interface USolverResult @@ -41,17 +36,6 @@ open class USolverBase( protected val decoder: UModelDecoder>, protected val softConstraintsProvider: USoftConstraintsProvider, ) : USolver, UModelBase>(), AutoCloseable { - // TODO remove it - protected open val modelBuilder: ( - ctx: UContext, - UReadOnlyRegistersStack, - UTypeModel, - UMockEvaluator, - Map, UReadOnlyMemoryRegion<*, *>>, - UConcreteHeapRef, - ) -> UModelBase = { ctx, stack, types, mocker, regions, nullRef -> - UModelBase(ctx, stack, types, mocker, regions, nullRef) - } protected fun translateLogicalConstraints(constraints: Iterable) { for (constraint in constraints) { @@ -179,7 +163,7 @@ open class USolverBase( // fourth, check it satisfies typeConstraints when (val typeResult = typeSolver.check(typeSolverQuery)) { is USatResult -> return USatResult( - modelBuilder( + UModelBase( ctx, uModel.stack, typeResult.model, diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/UInterpreterObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/UInterpreterObserver.kt index 2003cc0c9f..0a8e99401b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/UInterpreterObserver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/UInterpreterObserver.kt @@ -1,5 +1,5 @@ package org.usvm.statistics interface UInterpreterObserver { - + // Empty } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt b/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt index e5de4ca164..def51e4eb1 100644 --- a/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt +++ b/usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt @@ -1,6 +1,5 @@ package org.usvm.targets -// TODO add self generic for the controller interface UTargetController { val targets: MutableCollection> } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/JcInputTaintMarkReading.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/JcInputTaintMarkReading.kt deleted file mode 100644 index 4b6ac524a1..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/JcInputTaintMarkReading.kt +++ /dev/null @@ -1,41 +0,0 @@ -package org.usvm.api.targets - -import io.ksmt.cache.hash -import io.ksmt.cache.structurallyEqual -import io.ksmt.expr.KExpr -import io.ksmt.expr.printer.ExpressionPrinter -import io.ksmt.expr.transformer.KTransformerBase -import io.ksmt.sort.KBoolSort -import org.usvm.UBoolSort -import org.usvm.UCollectionReading -import org.usvm.UHeapRef -import org.usvm.UNullRef -import org.usvm.machine.JcContext -import org.usvm.machine.JcTransformer - -class JcInputTaintMarkReading( - ctx: JcContext, - collection: JcTaintMarksCollection, - val address: UHeapRef, -) : UCollectionReading, UHeapRef, UBoolSort>(ctx, collection) { - init { - require(address !is UNullRef) - } - - override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is JcTransformer) { "Expected a JcTransformer, but got: $transformer" } - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return transformer.transform(this) - } - - override fun internEquals(other: Any): Boolean = structurallyEqual(other, { collection }, { address }) - - override fun internHashCode(): Int = hash(collection, address) - - override fun print(printer: ExpressionPrinter) { - printer.append(collection.toString()) - printer.append("[") - printer.append(address) - printer.append("]") - } -} \ No newline at end of file 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 0920d3ee72..bd1c1aab2f 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 @@ -24,9 +24,8 @@ import org.usvm.machine.state.JcState import org.usvm.statistics.UMachineObserver import org.usvm.targets.UTargetController -// TODO do we need a context here? class TaintAnalysis( - private val configuration: TaintConfiguration,// TODO how to pass initial targets???? + private val configuration: TaintConfiguration, override val targets: MutableCollection = mutableListOf(), ) : UTargetController, JcInterpreterObserver, UMachineObserver { private val taintTargets: MutableMap> = mutableMapOf() @@ -37,9 +36,6 @@ class TaintAnalysis( } } - // TODO recursively add children here??????????????????????????????????????? - // TODO add recursively children at the beginning???????????????????????????????????????????????????????????????? - // TODO save mapping between initial targets and the states that reach them // Replace with the corresponding observer-collector? val collectedStates: MutableList = mutableListOf() @@ -98,7 +94,7 @@ class TaintAnalysis( }.orEmpty().toList().uncheckedCast() override fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) { - // Sinks are already processed at this moment since we resolved it on call statement + // Sinks are already processed at this moment since we resolved it on a call statement stmt.callExpr?.let { processTaintConfiguration(it, stepScope, exprResolver) } @@ -114,7 +110,9 @@ class TaintAnalysis( val methodResult = stepScope.calcOnState { methodResult } val method = callExpr.method.method - require(methodResult is JcMethodResult.Success) { "TODO message" } + require(methodResult is JcMethodResult.Success) { + "Other result statuses must be processed in `onMethodCallWithUnresolvedArguments`" + } val callPositionResolver = createCallPositionResolver(ctx, callExpr, simpleValueResolver, methodResult) @@ -138,8 +136,8 @@ class TaintAnalysis( sourceConfigurations?.forEach { val target = sourceTargets[it] - val (condition, action) = it.conditionWithAction - val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope) ?: ctx.trueExpr + val resolvedCondition = + conditionResolver.visit(it.condition, simpleValueResolver, stepScope) ?: ctx.trueExpr val targetCondition = target?.condition ?: ConstantTrue val resolvedTargetCondition = @@ -147,25 +145,23 @@ class TaintAnalysis( val combinedCondition = ctx.mkAnd(resolvedTargetCondition, resolvedCondition) - action.accept(actionResolver, stepScope, combinedCondition) + it.action.accept(actionResolver, stepScope, combinedCondition) target?.propagate(stepScope.state) } val cleanerConfigurations = configuration.cleaners[method] cleanerConfigurations?.forEach { - val (condition, action) = it.conditionWithAction - val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope) + val resolvedCondition = conditionResolver.visit(it.condition, simpleValueResolver, stepScope) - action.accept(actionResolver, stepScope, resolvedCondition) + it.action.accept(actionResolver, stepScope, resolvedCondition) } val passThroughConfigurations = configuration.passThrough[method] passThroughConfigurations?.forEach { - val (condition, action) = it.conditionWithAction - val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope) + val resolvedCondition = conditionResolver.visit(it.condition, simpleValueResolver, stepScope) - action.accept(actionResolver, stepScope, resolvedCondition) + it.action.accept(actionResolver, stepScope, resolvedCondition) } } @@ -190,19 +186,15 @@ class TaintAnalysis( // TODO entry point configuration } - // TODO documentation, but looks like sinks should be processed here since - // otherwise some extra conditions might be added during the parameters resolving (e.g., non-null - // constraint in virtual invokes override fun onMethodCallWithUnresolvedArguments( simpleValueResolver: JcSimpleValueResolver, stmt: JcCallExpr, stepScope: JcStepScope, ) { - // TODO add comment about absence of configuration val method = stmt.method.method val methodResult = stepScope.calcOnState { methodResult } - require(methodResult is JcMethodResult.NoCall) { "TODO" } + require(methodResult is JcMethodResult.NoCall) { "This signal must be sent before the method call" } val ctx = stepScope.ctx @@ -213,10 +205,11 @@ class TaintAnalysis( val currentStatement = stepScope.calcOnState { currentStatement } val targets = findTaintTargets(currentStatement, stepScope.state) - val sinks = targets.filterIsInstance() - sinks.forEach { - processSink(it.configRule, it.condition, conditionResolver, simpleValueResolver, stepScope, it) - } + targets + .filterIsInstance() + .forEach { + processSink(it.configRule, it.condition, conditionResolver, simpleValueResolver, stepScope, it) + } } else { val methodSinks = configuration.methodSinks[method] ?: return methodSinks.forEach { @@ -252,7 +245,6 @@ class TaintAnalysis( taintedStepScope.assert(resolvedCondition)?.let { // TODO remove corresponding target - // TODO probably, we should terminate this state? Yes, we should collectedStates += originalStateCopy target?.propagate(taintedStepScope.state) } @@ -263,23 +255,13 @@ class TaintAnalysis( stmt: JcMethodCallBaseInst, stepScope: JcStepScope, ) { - // TODO message, it is a redundant signal + // It is a redundant signal } override fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) { processTaintConfiguration(stmt.callExpr, stepScope, simpleValueResolver) } - override fun onStateProcessed( - simpleValueResolver: () -> JcSimpleValueResolver, - stmt: JcInst, - stepScope: JcStepScope, - ) { - // TODO for now, we might process each target several times if we have a transition with the same instruction - // and different path constraints - - } - override fun onState(parent: JcState, forks: Sequence) { propagateIntermediateTarget(parent) @@ -287,8 +269,9 @@ class TaintAnalysis( } private fun propagateIntermediateTarget(state: JcState) { - // TODO add comment why is it safe - val targets = findTaintTargets(state.pathLocation.parent!!.statement, state) + val parent = state.pathLocation.parent ?: error("This is impossible by construction") + val targets = findTaintTargets(parent.statement, state) + targets.forEach { when (it) { is TaintIntermediateTarget -> it.propagate(state) @@ -297,31 +280,26 @@ class TaintAnalysis( } } - sealed class TaintTarget( - location: JcInst, - ) : JcTarget(location) + private fun resolveCallInstance( + callExpr: JcCallExpr, + ) = if (callExpr is JcInstanceCallExpr) callExpr.instance else null + + sealed class TaintTarget(location: JcInst) : JcTarget(location) class TaintMethodSourceTarget( location: JcInst, val condition: Condition, val configurationRule: TaintMethodSource, ) : TaintTarget(location) - // TODO add field source targets - - class TaintIntermediateTarget(location: JcInst) : TaintTarget(location) { + // TODO add field sources and sinks targets - } + class TaintIntermediateTarget(location: JcInst) : TaintTarget(location) - // TODO is it important? Or we track every possible mark? class TaintMethodSinkTarget( location: JcInst, val condition: Condition, val configRule: TaintMethodSink, ) : TaintTarget(location) - - private fun resolveCallInstance( - callExpr: JcCallExpr, - ) = if (callExpr is JcInstanceCallExpr) callExpr.instance else null } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintConfigurationItem.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintConfigurationItem.kt index 5a32950c56..536e46e255 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintConfigurationItem.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintConfigurationItem.kt @@ -3,6 +3,7 @@ package org.usvm.api.targets import org.jacodb.api.JcField import org.jacodb.api.JcMethod +// TODO separate cleaning actions from the ones who can taint data data class TaintConfiguration( val entryPoints: Map>, val methodSources: Map>, @@ -17,19 +18,20 @@ sealed interface TaintConfigurationItem class TaintEntryPointSource( val method: JcMethod, - val conditionWithAction: Pair, + val condition: Condition, + val action: Action, ) : TaintConfigurationItem -// TODO probably conditions should be stored in some other way -// source is it either a method call or a field reading class TaintMethodSource( val method: JcMethod, - val conditionWithAction: Pair, // TODO replace with a specific class + val condition: Condition, + val action: Action, ) : TaintConfigurationItem class TaintFieldSource( val field: JcField, - val conditionWithAction: Pair, + val condition: Condition, + val action: Action, ) : TaintConfigurationItem class TaintMethodSink( @@ -44,11 +46,13 @@ class TaintFieldSink( class TaintPassThrough( val methodInfo: JcMethod, - val conditionWithAction: Pair, + val condition: Condition, + val action: Action, ) : TaintConfigurationItem class TaintCleaner( val methodInfo: JcMethod, - val conditionWithAction: Pair, + val condition: Condition, + val action: Action, ) : TaintConfigurationItem diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintMarkRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintMarkRegion.kt deleted file mode 100644 index 41a44d4a8f..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintMarkRegion.kt +++ /dev/null @@ -1,137 +0,0 @@ -package org.usvm.api.targets - -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentMapOf -import org.usvm.UBoolExpr -import org.usvm.UBoolSort -import org.usvm.UComposer -import org.usvm.UConcreteHeapAddress -import org.usvm.UExpr -import org.usvm.UHeapRef -import org.usvm.machine.jctx -import org.usvm.memory.UFlatUpdates -import org.usvm.memory.ULValue -import org.usvm.memory.UMemoryRegion -import org.usvm.memory.UMemoryRegionId -import org.usvm.memory.URegisterStackId.sort -import org.usvm.memory.USymbolicCollection -import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionKeyInfo -import org.usvm.memory.UWritableMemory -import org.usvm.memory.foldHeapRef -import org.usvm.memory.guardedWrite -import org.usvm.memory.key.UHeapRefKeyInfo -import org.usvm.memory.map -import java.util.Objects.hash - -typealias JcTaintMarksCollection = USymbolicCollection, UHeapRef, UBoolSort> - -data class JcTaintMarkLValue( - override val sort: UBoolSort, - val ref: UHeapRef, - val mark: Mark, -) : ULValue, UBoolSort> { - override val memoryRegionId: UMemoryRegionId, UBoolSort> - get() = TODO("Not yet implemented") - - override val key: JcTaintMarkLValue - get() = this - -} - -data class JcTaintMarksRegionId( - override val sort: UBoolSort, - val mark: Mark -) : UMemoryRegionId, UBoolSort> { - override fun emptyRegion(): UMemoryRegion, UBoolSort> = JcTaintMarksMemoryRegion() -} - -internal class JcTaintMarksMemoryRegion( - private val allocatedObjects: PersistentMap> = persistentMapOf(), - private var inputObjects: JcTaintMarksCollection? = null, -) : UMemoryRegion, UBoolSort> { - override fun read(key: JcTaintMarkLValue): UExpr = - key.ref.map( - { concreteRef -> allocatedObjects[concreteRef.address] ?: concreteRef.ctx.falseExpr }, - { symbolicRef -> getInputMarks(key).read(symbolicRef) } - ) - - private fun getInputMarks(lValue: JcTaintMarkLValue): JcTaintMarksCollection { - if (inputObjects == null) { - inputObjects = JcInputTaintMarkId(lValue.sort, lValue.mark).emptyRegion() - } - - return inputObjects!! - } - - override fun write( - key: JcTaintMarkLValue, - value: UExpr, - guard: UBoolExpr, - ): UMemoryRegion, UBoolSort> = - foldHeapRef( - key.ref, - initial = this, - initialGuard = guard, - blockOnConcrete = { region, (concreteRef, innerGuard) -> - val newRegion = region.allocatedObjects.guardedWrite(concreteRef.address, value, innerGuard) { - sort.ctx.falseExpr - } - JcTaintMarksMemoryRegion(newRegion, inputObjects) - }, - blockOnSymbolic = { region, (symbolicRef, innerGuard) -> - val oldRegion = region.getInputMarks(key) - val newRegion = oldRegion.write(symbolicRef, value, innerGuard) - JcTaintMarksMemoryRegion(allocatedObjects, newRegion) - } - ) - -} - -class JcInputTaintMarkId( - override val sort: UBoolSort, - internal val mark: Mark, -) : USymbolicCollectionId> { - override fun keyInfo(): USymbolicCollectionKeyInfo = UHeapRefKeyInfo - - override fun emptyRegion(): JcTaintMarksCollection = - USymbolicCollection(collectionId = this, UFlatUpdates(keyInfo())) - - private fun mkLValue(key: UHeapRef) = JcTaintMarkLValue(sort, key, mark) - - override fun write( - memory: UWritableMemory, - key: UHeapRef, - value: UExpr, - guard: UBoolExpr, - ) = memory.write(mkLValue(key), value, guard) - - - override fun instantiate( - collection: JcTaintMarksCollection, - key: UHeapRef, - composer: UComposer<*>?, - ): UExpr { - if (composer == null) { - return key.jctx.mkInputTaintMarkReading(collection, key) - } - - val memory = composer.memory.toWritableMemory() - collection.applyTo(memory, key, composer) - return memory.read(mkLValue(key)) - } - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as JcInputTaintMarkId<*> - - if (sort != other.sort) return false - return mark == other.mark - } - - override fun hashCode(): Int = hash(sort, mark) - - override fun toString(): String = "taintMark<$mark>()" -} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt index 3ac312f659..cd5bbddfe6 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt @@ -3,13 +3,12 @@ package org.usvm.machine import io.ksmt.solver.yices.KYicesSolver import io.ksmt.solver.z3.KZ3Solver import io.ksmt.symfpu.solver.KSymFpuSolver -import io.ksmt.utils.uncheckedCast import org.jacodb.api.JcType import org.usvm.SolverType import org.usvm.UComponents import org.usvm.UContext -import org.usvm.model.ULazyModelDecoder import org.usvm.solver.USoftConstraintsProvider +import org.usvm.solver.USolverBase import org.usvm.solver.UTypeSolver class JcComponents( @@ -18,7 +17,7 @@ class JcComponents( ) : UComponents { private val closeableResources = mutableListOf() - override fun mkSolver(ctx: UContext): JcSolver { + override fun mkSolver(ctx: UContext): USolverBase { val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) val softConstraintsProvider = USoftConstraintsProvider(ctx) @@ -30,7 +29,7 @@ class JcComponents( val typeSolver = UTypeSolver(typeSystem) closeableResources += smtSolver - return JcSolver(ctx.uncheckedCast(), smtSolver, typeSolver, translator, decoder, softConstraintsProvider) + return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, softConstraintsProvider) } fun close() { @@ -40,13 +39,4 @@ class JcComponents( override fun mkTypeSystem(ctx: UContext): JcTypeSystem { return typeSystem } - - override fun buildTranslatorAndLazyDecoder( - ctx: UContext - ): Pair> { - val translator = JcExprTranslator(ctx.uncheckedCast()) - val decoder = ULazyModelDecoder(translator) - - return translator to decoder - } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComposer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComposer.kt deleted file mode 100644 index cd19198f81..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComposer.kt +++ /dev/null @@ -1,17 +0,0 @@ -package org.usvm.machine - -import org.jacodb.api.JcType -import org.usvm.UBoolSort -import org.usvm.UComposer -import org.usvm.UExpr -import org.usvm.api.targets.JcInputTaintMarkReading -import org.usvm.api.targets.JcTaintMark -import org.usvm.memory.UReadOnlyMemory - -class JcComposer( - ctx: JcContext, - memory: UReadOnlyMemory, -) : UComposer(ctx, memory), JcTransformer { - override fun transform(expr: JcInputTaintMarkReading): UExpr = - transformCollectionReading(expr, expr.address) -} \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt index 56e7ee5b38..b3e3c3eda9 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt @@ -1,6 +1,5 @@ package org.usvm.machine -import io.ksmt.utils.cast import org.jacodb.api.JcArrayType import org.jacodb.api.JcClasspath import org.jacodb.api.JcField @@ -22,13 +21,7 @@ import org.jacodb.api.ext.toType import org.jacodb.api.ext.void import org.jacodb.impl.bytecode.JcFieldImpl import org.jacodb.impl.types.FieldInfo -import org.usvm.UBoolSort import org.usvm.UContext -import org.usvm.UHeapRef -import org.usvm.api.targets.JcInputTaintMarkId -import org.usvm.api.targets.JcInputTaintMarkReading -import org.usvm.api.targets.JcTaintMark -import org.usvm.memory.USymbolicCollection import org.usvm.util.extractJcRefType class JcContext( @@ -136,14 +129,4 @@ class JcContext( val arrayStoreExceptionType by lazy { extractJcRefType(ArrayStoreException::class) } - - private val inputTaintMarkReadingCache = mkAstInterner>() - - fun mkInputTaintMarkReading( - region: USymbolicCollection, UHeapRef, UBoolSort>, - address: UHeapRef, - ): JcInputTaintMarkReading = inputTaintMarkReadingCache.createIfContextActive { - JcInputTaintMarkReading(this, region, address) - }.cast() - } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprTranslator.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprTranslator.kt deleted file mode 100644 index 9f83ca20fd..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprTranslator.kt +++ /dev/null @@ -1,28 +0,0 @@ -package org.usvm.machine - -import org.jacodb.api.JcType -import org.usvm.UBoolSort -import org.usvm.UExpr -import org.usvm.api.targets.JcInputTaintMarkId -import org.usvm.api.targets.JcInputTaintMarkReading -import org.usvm.api.targets.JcTaintMark -import org.usvm.api.targets.JcTaintMarksRegionId -import org.usvm.solver.UExprTranslator - -class JcExprTranslator(ctx: JcContext) : UExprTranslator(ctx), JcTransformer { - override fun transform(expr: JcInputTaintMarkReading): UExpr = - transformExprAfterTransformed(expr, expr.address) { address -> - val translator = taintMarksRegionDecoder(expr.collection.collectionId) - .inputTaintMarkRegionTranslator(expr.collection.collectionId) - translator.translateReading(expr.collection, address) - } - - private fun > taintMarksRegionDecoder( - markId: MarkId, - ): JcTaintMarkRegionDecoder { - val marksRegionId = JcTaintMarksRegionId(ctx.boolSort, markId.mark) - return getOrPutRegionDecoder(marksRegionId) { - JcTaintMarkRegionDecoder(marksRegionId, exprTranslator = this) - } - } -} \ No newline at end of file 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 4129ac13d7..7d014e169a 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt @@ -7,7 +7,6 @@ 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.JcReturnInst import org.jacodb.api.cfg.JcSwitchInst import org.jacodb.api.cfg.JcThrowInst @@ -17,22 +16,16 @@ import org.usvm.statistics.UInterpreterObserver interface JcInterpreterObserver : UInterpreterObserver { fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {} - // TODO add call statement 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 onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {} fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, 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) {} fun onEnterMonitorStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcEnterMonitorInst, stepScope: JcStepScope) {} fun onExitMonitorStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcExitMonitorInst, stepScope: JcStepScope) {} - fun onStateProcessed(simpleValueResolver: () -> JcSimpleValueResolver, stmt: JcInst, stepScope: JcStepScope) {} } - -// TODO create a composite observer -// TODO probably not due to multiplication of the complexities of the analysis -// TODO No, we should have it \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index 6db36fadee..ee14726902 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -40,7 +40,6 @@ class JcMachine( private val components = JcComponents(typeSystem, options.solverType) private val ctx = JcContext(cp, components) - // TODO change the way of observers creation private val interpreter = JcInterpreter(ctx, applicationGraph, interpreterObserver) private val cfgStatistics = CfgStatisticsImpl(applicationGraph) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcModel.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcModel.kt deleted file mode 100644 index b7f1d07c1b..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcModel.kt +++ /dev/null @@ -1,21 +0,0 @@ -package org.usvm.machine - -import org.jacodb.api.JcType -import org.usvm.UConcreteHeapRef -import org.usvm.UMockEvaluator -import org.usvm.memory.UMemoryRegionId -import org.usvm.memory.UReadOnlyMemoryRegion -import org.usvm.memory.UReadOnlyRegistersStack -import org.usvm.model.UModelBase -import org.usvm.model.UTypeModel - -class JcModel( - ctx: JcContext, - override val stack: UReadOnlyRegistersStack, - override val types: UTypeModel, - override val mocker: UMockEvaluator, - regions: Map, UReadOnlyMemoryRegion<*, *>>, - nullRef: UConcreteHeapRef, -) : UModelBase(ctx, stack, types, mocker, regions, nullRef) { - override val composer = JcComposer(ctx, memory = this) -} \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolver.kt deleted file mode 100644 index b9ba2f890b..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolver.kt +++ /dev/null @@ -1,38 +0,0 @@ -package org.usvm.machine - -import io.ksmt.solver.KSolver -import io.ksmt.utils.cast -import org.jacodb.api.JcType -import org.usvm.UConcreteHeapRef -import org.usvm.UContext -import org.usvm.UMockEvaluator -import org.usvm.memory.UMemoryRegionId -import org.usvm.memory.UReadOnlyMemoryRegion -import org.usvm.memory.UReadOnlyRegistersStack -import org.usvm.model.UModelBase -import org.usvm.model.UModelDecoder -import org.usvm.model.UTypeModel -import org.usvm.solver.UExprTranslator -import org.usvm.solver.USoftConstraintsProvider -import org.usvm.solver.USolverBase -import org.usvm.solver.UTypeSolver - -class JcSolver( - ctx: JcContext, - smtSolver: KSolver<*>, - typeSolver: UTypeSolver, - translator: UExprTranslator, - decoder: UModelDecoder>, - softConstraintsProvider: USoftConstraintsProvider, -) : USolverBase(ctx, smtSolver, typeSolver, translator, decoder, softConstraintsProvider) { - override val modelBuilder: ( - ctx: UContext, - UReadOnlyRegistersStack, - UTypeModel, - UMockEvaluator, - Map, UReadOnlyMemoryRegion<*, *>>, - UConcreteHeapRef, - ) -> UModelBase = { ctx, stack, types, mocker, regions, nullRef -> - JcModel(ctx.cast(), stack, types, mocker, regions, nullRef) - } -} \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintMarkRegionDecoder.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintMarkRegionDecoder.kt deleted file mode 100644 index 79efe21803..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintMarkRegionDecoder.kt +++ /dev/null @@ -1,61 +0,0 @@ -package org.usvm.machine - -import io.ksmt.expr.KExpr -import io.ksmt.solver.KModel -import org.usvm.UBoolSort -import org.usvm.UConcreteHeapRef -import org.usvm.UHeapRef -import org.usvm.api.targets.JcInputTaintMarkId -import org.usvm.api.targets.JcTaintMark -import org.usvm.api.targets.JcTaintMarkLValue -import org.usvm.api.targets.JcTaintMarksRegionId -import org.usvm.memory.UReadOnlyMemoryRegion -import org.usvm.memory.USymbolicCollection -import org.usvm.solver.UCollectionDecoder -import org.usvm.solver.URegionDecoder -import org.usvm.solver.URegionTranslator - -class JcTaintMarkRegionDecoder( - private val regionId: JcTaintMarksRegionId, - private val exprTranslator: JcExprTranslator, -) : URegionDecoder, UBoolSort> { - private var inputRegionTranslator: JcInputTaintMarkRegionTranslator? = null - - fun inputTaintMarkRegionTranslator( - collectionId: JcInputTaintMarkId, - ): URegionTranslator, UHeapRef, UBoolSort> { - - println(collectionId) // TODO - - if (inputRegionTranslator == null) { - inputRegionTranslator = JcInputTaintMarkRegionTranslator() - } - - return inputRegionTranslator!! - } - - override fun decodeLazyRegion( - model: KModel, - mapping: Map, - ): UReadOnlyMemoryRegion, UBoolSort>? = inputRegionTranslator?.let { - JcTaintMarksLazyModelRegion(regionId, model, mapping, it) - } -} - -private class JcInputTaintMarkRegionTranslator : - URegionTranslator, UHeapRef, UBoolSort>, UCollectionDecoder { - override fun translateReading( - region: USymbolicCollection, UHeapRef, UBoolSort>, - key: UHeapRef, - ): KExpr { - TODO("Not yet implemented") - } - - override fun decodeCollection( - model: KModel, - mapping: Map, - ): UReadOnlyMemoryRegion { - TODO("Not yet implemented") - } - -} \ No newline at end of file diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintsModelRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintsModelRegion.kt deleted file mode 100644 index b693e936ab..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTaintsModelRegion.kt +++ /dev/null @@ -1,40 +0,0 @@ -package org.usvm.machine - -import io.ksmt.solver.KModel -import org.usvm.UBoolSort -import org.usvm.UExpr -import org.usvm.UHeapRef -import org.usvm.api.targets.JcTaintMark -import org.usvm.api.targets.JcTaintMarkLValue -import org.usvm.api.targets.JcTaintMarksRegionId -import org.usvm.memory.UReadOnlyMemoryRegion -import org.usvm.model.AddressesMapping -import org.usvm.model.modelEnsureConcreteInputRef -import org.usvm.solver.UCollectionDecoder - -abstract class JcTaintMarksModelRegion( - private val regionId: JcTaintMarksRegionId, -) : UReadOnlyMemoryRegion, UBoolSort> { - abstract val inputMarks: UReadOnlyMemoryRegion - - override fun read(key: JcTaintMarkLValue): UExpr { - val ref = modelEnsureConcreteInputRef(key.ref) - return inputMarks.read(ref) - } -} - -class JcTaintMarksLazyModelRegion( - regionId: JcTaintMarksRegionId, - private val model: KModel, - private val addressesMapping: AddressesMapping, - private val inputMarksDecoder: UCollectionDecoder, -) : JcTaintMarksModelRegion(regionId) { - override val inputMarks: UReadOnlyMemoryRegion by lazy { - inputMarksDecoder.decodeCollection(model, addressesMapping) - } -} - -class JcTaintMarksEagerModelRegion( - regionId: JcTaintMarksRegionId, - override val inputMarks: UReadOnlyMemoryRegion, -) : JcTaintMarksModelRegion(regionId) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt deleted file mode 100644 index c57c61db76..0000000000 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt +++ /dev/null @@ -1,12 +0,0 @@ -package org.usvm.machine - -import org.jacodb.api.JcType -import org.usvm.UBoolSort -import org.usvm.UExpr -import org.usvm.UTransformer -import org.usvm.api.targets.JcInputTaintMarkReading -import org.usvm.api.targets.JcTaintMark - -interface JcTransformer : UTransformer { - fun transform(expr: JcInputTaintMarkReading): UExpr -} \ No newline at end of file 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 a753a060f2..2940b544ed 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 @@ -145,8 +145,6 @@ class JcInterpreter( else -> error("Unknown stmt: $ stmt") } - observer?.onStateProcessed(lazySimpleValueResolverWithScope(scope), stmt, scope) - return scope.stepResult() } @@ -202,7 +200,7 @@ class JcInterpreter( private val typeSelector = JcFixedInheritorsNumberTypeSelector() private fun visitMethodCall(scope: JcStepScope, stmt: JcMethodCallBaseInst) { - val resolver = lazySimpleValueResolverWithScope(scope)() + val resolver = simpleValueResolverWithScope(scope) when (stmt) { is JcMethodEntrypointInst -> { @@ -247,11 +245,10 @@ class JcInterpreter( stmt.callExpr?.let { val methodResult = scope.calcOnState { methodResult } - // TODo comment when (methodResult) { is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(exprResolver.simpleValueResolver, it, scope) is JcMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) - is JcMethodResult.JcException -> error("TODO") + is JcMethodResult.JcException -> error("Exceptions must be processed earlier") } } @@ -303,7 +300,7 @@ class JcInterpreter( } private fun visitGotoStmt(scope: JcStepScope, stmt: JcGotoInst) { - observer?.onGotoStatement(lazySimpleValueResolverWithScope(scope), stmt, scope) + observer?.onGotoStatement(simpleValueResolverWithScope(scope), stmt, scope) val nextStmt = stmt.location.method.instList[stmt.target.index] scope.doWithState { newStmt(nextStmt) } @@ -358,11 +355,10 @@ class JcInterpreter( val callExpr = stmt.callExpr val methodResult = scope.calcOnState { methodResult } - // TODO comment when (methodResult) { is JcMethodResult.NoCall -> observer?.onMethodCallWithUnresolvedArguments(exprResolver.simpleValueResolver, callExpr, scope) is JcMethodResult.Success -> observer?.onCallStatement(exprResolver.simpleValueResolver, stmt, scope) - is JcMethodResult.JcException -> error("TODO") + is JcMethodResult.JcException -> error("Exceptions must be processed earlier") } exprResolver.resolveJcExpr(callExpr) ?: return @@ -408,10 +404,9 @@ class JcInterpreter( ::stringConstantAllocator, ) - // TODO remove lazyness from it - private fun lazySimpleValueResolverWithScope( + private fun simpleValueResolverWithScope( scope: JcStepScope, - ): () -> JcSimpleValueResolver = { exprResolverWithScope(scope).simpleValueResolver } + ): JcSimpleValueResolver = exprResolverWithScope(scope).simpleValueResolver private val localVarToIdx = mutableMapOf>() // (method, localName) -> idx diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt index ac136ff36e..f63095bb7f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt @@ -21,7 +21,7 @@ class JcState( models: List> = listOf(), override var pathLocation: PathsTrieNode = ctx.mkInitialLocation(), var methodResult: JcMethodResult = JcMethodResult.NoCall, - targets: List> = emptyList() + targets: List> = emptyList(), ) : UState, JcState>( ctx, callStack, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt index b439473632..e1c1d0684f 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.codegen -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/taint/TaintTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/taint/TaintTest.kt index 8407bd5330..c28f57a81d 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/taint/TaintTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/taint/TaintTest.kt @@ -141,9 +141,7 @@ class TaintTest : JavaMethodTestRunner() { } } - // TODO separate cleaning actions - // TODO for demonstration purposes only, must be either moved to another place or removed completely - fun sampleConfiguration(cp: JcClasspath): TaintConfiguration { + private fun sampleConfiguration(cp: JcClasspath): TaintConfiguration { fun findMethod(className: String, methodName: String) = cp .findClassOrNull(className)!! .declaredMethods @@ -152,13 +150,13 @@ class TaintTest : JavaMethodTestRunner() { val sampleClassName = "org.usvm.samples.taint.Taint" val taintEntryPointSourceMethod = findMethod(sampleClassName, "taintedEntrySource") - val taintEntryPointSourceCondition = ConstantTrue // TODO could be replaced with a check for emptiness + val taintEntryPointSourceCondition = ConstantTrue val sampleEntryPointsSources = mapOf( taintEntryPointSourceMethod to listOf( TaintEntryPointSource( taintEntryPointSourceMethod, - taintEntryPointSourceCondition to AssignMark(Argument(0u), SqlInjection) + taintEntryPointSourceCondition, AssignMark(Argument(0u), SqlInjection) ) ) ) @@ -169,11 +167,11 @@ class TaintTest : JavaMethodTestRunner() { sampleSourceMethod to listOf( TaintMethodSource( sampleSourceMethod, - sampleCondition to AssignMark(Result, SqlInjection) + sampleCondition, AssignMark(Result, SqlInjection) ), TaintMethodSource( sampleSourceMethod, - sampleCondition to AssignMark(Result, SensitiveData) // TODO replace with a bulk operation + sampleCondition, AssignMark(Result, SensitiveData) ), ) ) @@ -188,12 +186,12 @@ class TaintTest : JavaMethodTestRunner() { samplePassThoughMethod to listOf( TaintPassThrough( samplePassThoughMethod, - samplePassThroughCondition to CopyAllMarks(Argument(0u), Result) - ), // TODO replace with a bulk operation + samplePassThroughCondition, CopyAllMarks(Argument(0u), Result) + ), TaintPassThrough( samplePassThoughMethod, - samplePassThroughCondition to CopyAllMarks(Argument(1u), Result) - ), // TODO replace with a bulk operation + samplePassThroughCondition, CopyAllMarks(Argument(1u), Result) + ), ) ) @@ -203,7 +201,7 @@ class TaintTest : JavaMethodTestRunner() { sampleCleanerMethod to listOf( TaintCleaner( sampleCleanerMethod, - cleanerCondition to RemoveAllMarks(Result) + cleanerCondition, RemoveAllMarks(Result) ) ) ) @@ -242,9 +240,7 @@ class TaintTest : JavaMethodTestRunner() { ) } - - // TODO REMOVE IT, FOR DEMONSTRATION PURPOSES ONLY - fun constructSampleTaintAnalysis(cp: JcClasspath): TaintAnalysis { + private fun constructSampleTaintAnalysis(cp: JcClasspath): TaintAnalysis { fun findMethod(className: String, methodName: String) = cp .findClassOrNull(className)!! .declaredMethods @@ -272,7 +268,7 @@ class TaintTest : JavaMethodTestRunner() { findMethod(sampleClassName, "simpleTaint") .instList .last { "stringProducer" in it.toString() }, - stringProducerRule.conditionWithAction.first, + stringProducerRule.condition, stringProducerRule ) @@ -290,7 +286,7 @@ class TaintTest : JavaMethodTestRunner() { findMethod(sampleClassName, "simpleFalsePositive") .instList .first { "stringProducer" in it.toString() }, - stringProducerRule.conditionWithAction.first, + stringProducerRule.condition, stringProducerRule ) @@ -322,7 +318,7 @@ class TaintTest : JavaMethodTestRunner() { findMethod(sampleClassName, "simpleTruePositive") .instList .first { "stringProducer" in it.toString() }, - stringProducerRule.conditionWithAction.first, + stringProducerRule.condition, stringProducerRule ) @@ -355,7 +351,7 @@ class TaintTest : JavaMethodTestRunner() { findMethod(sampleClassName, "taintWithReturningValue") .instList .first { "stringProducer" in it.toString() }, - stringProducerRule.conditionWithAction.first, + stringProducerRule.condition, stringProducerRule ) @@ -377,7 +373,7 @@ class TaintTest : JavaMethodTestRunner() { findMethod(sampleClassName, "goThroughCleaner") .instList .first { "stringProducer" in it.toString() }, - stringProducerRule.conditionWithAction.first, + stringProducerRule.condition, stringProducerRule ) diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt index 16abae13ed..c0efa82e9a 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.wrappers -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt index 9dcf7423fe..3428f7548f 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt @@ -98,7 +98,7 @@ class SampleMachine( private fun getInitialState( method: Method<*>, - targets: List> // TODO pass analyzers and controllers instead of the targets?????????????????????????????????????????????????? + targets: List> ): SampleState = SampleState(ctx, targets = targets).apply { addEntryMethodCall(applicationGraph, method)