From a6cdaff1251ec187244d280c9aa2c2131c7a8b89 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 28 Jun 2023 10:22:22 +0300 Subject: [PATCH] Fix: review comments --- .../main/kotlin/org/usvm/ApplicationGraph.kt | 2 ++ usvm-core/src/main/kotlin/org/usvm/Machine.kt | 2 +- .../CollectedStatesLimitStrategy.kt | 2 +- .../StepsCountingStoppingStrategy.kt | 2 +- .../StoppingStrategy.kt | 2 +- .../TargetsCoveredStoppingStrategy.kt | 24 ++-------------- .../org/usvm/model/ModelDecodingTest.kt | 20 ++++++------- .../org/usvm/api/util/JcTestResolver.kt | 2 +- .../org/usvm/machine/JcApplicationGraph.kt | 28 ++++++++++++++++++- .../main/kotlin/org/usvm/machine/JcMachine.kt | 2 +- .../usvm/operators/JcBinaryOperatorTest.kt | 2 +- .../org/usvm/operators/JcUnaryOperatorTest.kt | 4 +-- .../usvm/machine/SampleApplicationGraph.kt | 3 ++ .../kotlin/org/usvm/machine/SampleMachine.kt | 2 +- 14 files changed, 54 insertions(+), 43 deletions(-) rename usvm-core/src/main/kotlin/org/usvm/ps/{stopstregies => stopstrategies}/CollectedStatesLimitStrategy.kt (90%) rename usvm-core/src/main/kotlin/org/usvm/ps/{stopstregies => stopstrategies}/StepsCountingStoppingStrategy.kt (96%) rename usvm-core/src/main/kotlin/org/usvm/ps/{stopstregies => stopstrategies}/StoppingStrategy.kt (89%) rename usvm-core/src/main/kotlin/org/usvm/ps/{stopstregies => stopstrategies}/TargetsCoveredStoppingStrategy.kt (53%) diff --git a/usvm-core/src/main/kotlin/org/usvm/ApplicationGraph.kt b/usvm-core/src/main/kotlin/org/usvm/ApplicationGraph.kt index 9c0a46af08..bea3d5eecd 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ApplicationGraph.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ApplicationGraph.kt @@ -11,4 +11,6 @@ interface ApplicationGraph { fun exitPoints(method: Method): Sequence fun methodOf(node: Statement): Method + + fun statementsOf(method: Method): Sequence } diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt index edc0b652f4..c1cd84a0bc 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt @@ -1,6 +1,6 @@ package org.usvm -import org.usvm.ps.stopstregies.StoppingStrategy +import org.usvm.ps.stopstrategies.StoppingStrategy /** diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/CollectedStatesLimitStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/CollectedStatesLimitStrategy.kt similarity index 90% rename from usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/CollectedStatesLimitStrategy.kt rename to usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/CollectedStatesLimitStrategy.kt index 78309723f6..3be79c20d0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/CollectedStatesLimitStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/CollectedStatesLimitStrategy.kt @@ -1,4 +1,4 @@ -package org.usvm.ps.stopstregies +package org.usvm.ps.stopstrategies class CollectedStatesLimitStrategy( val statesLimit: Int = STATES_LIMIT diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StepsCountingStoppingStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StepsCountingStoppingStrategy.kt similarity index 96% rename from usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StepsCountingStoppingStrategy.kt rename to usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StepsCountingStoppingStrategy.kt index b2b52872e2..53988d9eb9 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StepsCountingStoppingStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StepsCountingStoppingStrategy.kt @@ -1,4 +1,4 @@ -package org.usvm.ps.stopstregies +package org.usvm.ps.stopstrategies import org.usvm.ApplicationGraph import org.usvm.ps.statistics.Statistics diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StoppingStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StoppingStrategy.kt similarity index 89% rename from usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StoppingStrategy.kt rename to usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StoppingStrategy.kt index 942f5bcf74..2ced27cc76 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/StoppingStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/StoppingStrategy.kt @@ -1,4 +1,4 @@ -package org.usvm.ps.stopstregies +package org.usvm.ps.stopstrategies fun interface StoppingStrategy { fun shouldStop(): Boolean diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/TargetsCoveredStoppingStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/TargetsCoveredStoppingStrategy.kt similarity index 53% rename from usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/TargetsCoveredStoppingStrategy.kt rename to usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/TargetsCoveredStoppingStrategy.kt index c96e46213b..1809a2639b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/stopstregies/TargetsCoveredStoppingStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/stopstrategies/TargetsCoveredStoppingStrategy.kt @@ -1,4 +1,4 @@ -package org.usvm.ps.stopstregies +package org.usvm.ps.stopstrategies import org.usvm.ApplicationGraph import org.usvm.ps.statistics.Statistics @@ -8,31 +8,11 @@ class TargetsCoveredStoppingStrategy( graph: ApplicationGraph, ) : Statistics(graph), StoppingStrategy { private val uncoveredStatements = methods - .flatMap { findAllStatementsOfMethod(it) } + .flatMap { graph.statementsOf(it) } .toMutableSet() val uncoveredStatementsCount get() = uncoveredStatements.size - private fun findAllStatementsOfMethod(method: Method): Collection { - val entryStatements = graph.entryPoint(method) - val statements = entryStatements.toMutableSet() - - val queue = ArrayDeque(entryStatements.toList()) - - while (queue.isNotEmpty()) { - val statement = queue.removeLast() - val successors = graph.successors(statement) - for (successor in successors) { - if (successor !in statements) { - statements += successor - queue += successor - } - } - } - - return statements - } - override fun shouldStop(): Boolean = uncoveredStatements.isEmpty() override fun onStatementVisit(statement: Statement) { diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt index c3a06e6947..16484e7e29 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt @@ -156,15 +156,15 @@ class ModelDecodingTest { val idx = stack.readRegister(3, bv32Sort) heap.writeArrayIndex(concreteRef, concreteIdx, array, addressSort, symbolicRef1, trueExpr) - val readedRef = heap.readArrayIndex(concreteRef, idx, array, addressSort) + val readRef = heap.readArrayIndex(concreteRef, idx, array, addressSort) - val readedRef1 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) + val readRef1 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) - heap.writeArrayIndex(readedRef, idx, array, addressSort, symbolicRef0, trueExpr) + heap.writeArrayIndex(readRef, idx, array, addressSort, symbolicRef0, trueExpr) - val readedRef2 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) + val readRef2 = heap.readArrayIndex(symbolicRef2, idx, array, addressSort) - pc += (symbolicRef2 neq nullRef) and (readedRef1 neq readedRef2) + pc += (symbolicRef2 neq nullRef) and (readRef1 neq readRef2) val status = solver.checkWithSoftConstraints(pc) val model = assertIs>>(status).model @@ -186,18 +186,18 @@ class ModelDecodingTest { heap.writeArrayIndex(symbolicRef1, concreteIdx, array, addressSort, symbolicRef2, trueExpr) heap.writeArrayIndex(symbolicRef2, concreteIdx, array, addressSort, symbolicRef0, trueExpr) - val readedRef = heap.readArrayIndex(symbolicRef0, concreteIdx, array, addressSort) + val readRef = heap.readArrayIndex(symbolicRef0, concreteIdx, array, addressSort) pc += symbolicRef0 neq nullRef pc += symbolicRef1 neq nullRef pc += symbolicRef2 neq nullRef - pc += readedRef neq symbolicRef1 + pc += readRef neq symbolicRef1 pc += symbolicRef0 eq symbolicRef1 val status = solver.checkWithSoftConstraints(pc) val model = assertIs>>(status).model assertSame(falseExpr, model.eval(symbolicRef2 eq symbolicRef0)) - assertSame(model.eval(readedRef), model.eval(symbolicRef2)) + assertSame(model.eval(readRef), model.eval(symbolicRef2)) } @Test @@ -208,9 +208,9 @@ class ModelDecodingTest { val concreteIdx = mkBv(3) - val readedExpr = heap.readArrayIndex(symbolicRef0, concreteIdx, array, bv32Sort) + val readExpr = heap.readArrayIndex(symbolicRef0, concreteIdx, array, bv32Sort) pc += symbolicRef0 neq nullRef - pc += readedExpr eq mkBv(42) + pc += readExpr eq mkBv(42) val status = solver.checkWithSoftConstraints(pc) val model = assertIs>>(status).model diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt index ab18701074..3fcb9ce1cc 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt @@ -113,7 +113,7 @@ class JcTestResolver( private val method: JcTypedMethod, private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(), ) { - private val resolvedCache = mutableMapOf() + private val resolvedCache = mutableMapOf() fun resolveState(): JcParametersState { // TODO: now we need to explicitly evaluate indices of registers, because we don't have specific ULValues diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt index b17a999acf..305e834553 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt @@ -45,7 +45,33 @@ class JcApplicationGraph( val JcMethod.typed get() = typedMethodsCache.getOrPut(this) { - // maybe there is a better way, but I didn't find it enclosingClass.toType().declaredMethods.first { it.method == this } } + + private val statementsOfMethodCache = ConcurrentHashMap>() + + override fun statementsOf(method: JcMethod): Sequence = + statementsOfMethodCache + .getOrPut(method) { computeAllStatementsOfMethod(method) } + .asSequence() + + private fun computeAllStatementsOfMethod(method: JcMethod): Collection { + val entryStatements = entryPoint(method) + val statements = entryStatements.toMutableSet() + + val queue = ArrayDeque(entryStatements.toList()) + + while (queue.isNotEmpty()) { + val statement = queue.removeLast() + val successors = successors(statement) + for (successor in successors) { + if (successor !in statements) { + statements += successor + queue += successor + } + } + } + + return statements + } } 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 743e4b93e1..0b3332b150 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -9,7 +9,7 @@ import org.usvm.machine.state.JcState import org.usvm.ps.BfsPathSelector import org.usvm.ps.DfsPathSelector import org.usvm.ps.combinators.ParallelSelector -import org.usvm.ps.stopstregies.TargetsCoveredStoppingStrategy +import org.usvm.ps.stopstrategies.TargetsCoveredStoppingStrategy class JcMachine( cp: JcClasspath, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/operators/JcBinaryOperatorTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/operators/JcBinaryOperatorTest.kt index 5c9a99969a..18420b72c4 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/operators/JcBinaryOperatorTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/operators/JcBinaryOperatorTest.kt @@ -60,7 +60,7 @@ class JcBinaryOperatorTest { onBytes = Byte::times, onChars = { a, b -> a.code * b.code }, onShorts = Short::times, - operatorText = "+", + operatorText = "*", onInts = Int::times, onLongs = Long::times, onFloats = Float::times, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/operators/JcUnaryOperatorTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/operators/JcUnaryOperatorTest.kt index 2c2efeb8b2..4f36b11546 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/operators/JcUnaryOperatorTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/operators/JcUnaryOperatorTest.kt @@ -40,8 +40,8 @@ class JcUnaryOperatorTest { @Test fun `Test cast byte to short`() = testOperator( - JcUnaryOperator.CastToChar, - "(char)", + JcUnaryOperator.CastToShort, + "(short)", { it.toInt().toShort() }, ::extractShort, ctx::mkBv, diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleApplicationGraph.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleApplicationGraph.kt index 8c7bffddda..71e0c1c1ae 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleApplicationGraph.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleApplicationGraph.kt @@ -99,6 +99,9 @@ class SampleApplicationGraph( } } + override fun statementsOf(method: Method<*>): Sequence = + method.body?.stmts.orEmpty().asSequence() + override fun predecessors(node: Stmt): Sequence { val info = lazyGetStmtInfo(node) return info.predecessors.asSequence() 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 903556e286..09c13c8654 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 @@ -9,7 +9,7 @@ import org.usvm.language.Method import org.usvm.language.Program import org.usvm.language.SampleType import org.usvm.ps.DfsPathSelector -import org.usvm.ps.stopstregies.CollectedStatesLimitStrategy +import org.usvm.ps.stopstrategies.CollectedStatesLimitStrategy /** * Entry point for a sample language analyzer.