Fix: review comments

UnitTestBot · Jun 28, 2023 · 784c221 · 784c221
1 parent 22522f3
commit 784c221
Show file tree

Hide file tree

Showing 14 changed files with 54 additions and 42 deletions.
diff --git 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<Method, Statement> {
     fun exitPoints(method: Method): Sequence<Statement>
 
     fun methodOf(node: Statement): Method
+
+    fun statementsOf(method: Method): Sequence<Statement>
 }
diff --git 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/...pstregies/CollectedStatesLimitStrategy.kt → ...trategies/CollectedStatesLimitStrategy.kt b/...pstregies/CollectedStatesLimitStrategy.kt → ...trategies/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/...stregies/StepsCountingStoppingStrategy.kt → ...rategies/StepsCountingStoppingStrategy.kt b/...stregies/StepsCountingStoppingStrategy.kt → ...rategies/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/ps/stopstregies/StoppingStrategy.kt → ...svm/ps/stopstrategies/StoppingStrategy.kt b/.../usvm/ps/stopstregies/StoppingStrategy.kt → ...svm/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/...tregies/TargetsCoveredStoppingStrategy.kt → ...ategies/TargetsCoveredStoppingStrategy.kt b/...tregies/TargetsCoveredStoppingStrategy.kt → ...ategies/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<Method, Statement>(
     graph: ApplicationGraph<Method, Statement>,
 ) : Statistics<Method, Statement>(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<Statement> {
-        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
@@ -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<USatResult<UModelBase<Field, Type>>>(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<USatResult<UModelBase<Field, Type>>>(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<USatResult<UModelBase<Field, Type>>>(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
@@ -113,7 +113,7 @@ class JcTestResolver(
         private val method: JcTypedMethod,
         private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(),
     ) {
-        private val resolvedCache = mutableMapOf<Int, Any?>()
+        private val resolvedCache = mutableMapOf<UConcreteHeapAddress, Any?>()
 
         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
@@ -48,4 +48,31 @@ class JcApplicationGraph(
             // maybe there is a better way, but I didn't find it
             enclosingClass.toType().declaredMethods.first { it.method == this }
         }
+
+    private val statementsOfMethodCache = ConcurrentHashMap<JcMethod, Collection<JcInst>>()
+
+    override fun statementsOf(method: JcMethod): Sequence<JcInst> =
+        statementsOfMethodCache
+            .getOrPut(method) { computeAllStatementsOfMethod(method) }
+            .asSequence()
+
+    private fun computeAllStatementsOfMethod(method: JcMethod): Collection<JcInst> {
+        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
@@ -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
@@ -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
@@ -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
@@ -99,6 +99,9 @@ class SampleApplicationGraph(
         }
     }
 
+    override fun statementsOf(method: Method<*>): Sequence<Stmt> =
+        method.body?.stmts.orEmpty().asSequence()
+
     override fun predecessors(node: Stmt): Sequence<Stmt> {
         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
@@ -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.