Rebase

UnitTestBot · Oct 4, 2023 · ff7b80f · ff7b80f
1 parent 514b55d
commit ff7b80f
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/usvm-ml-path-selection/src/main/kotlin/org/usvm/jvm/interpreter/JcBlockInterpreter.kt b/usvm-ml-path-selection/src/main/kotlin/org/usvm/jvm/interpreter/JcBlockInterpreter.kt
@@ -12,6 +12,7 @@ import org.usvm.api.allocateStaticRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.targets.JcTarget
 import org.usvm.api.typeStreamOf
+import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.jvm.JcApplicationBlockGraph
 import org.usvm.machine.*
 import org.usvm.machine.interpreter.JcExprResolver
@@ -31,6 +32,7 @@ import org.usvm.util.write
 class JcBlockInterpreter(
     private val ctx: JcContext,
     private val applicationGraph: JcApplicationBlockGraph,
+    var forkBlackList: UForkBlackList<JcState, JcInst> = UForkBlackList.createDefault(),
 ) : UInterpreter<JcState>() {
 
     companion object {
@@ -67,7 +69,7 @@ class JcBlockInterpreter(
             }
         }
 
-        val solver = ctx.solver<JcType, JcContext>()
+        val solver = ctx.solver<JcType>()
 
         val model = (solver.checkWithSoftConstraints(state.pathConstraints) as USatResult).model
         state.models = listOf(model)
@@ -82,7 +84,7 @@ class JcBlockInterpreter(
 
         logger.debug("Step: {}", stmt)
 
-        val scope = StepScope(state)
+        val scope = StepScope(state, forkBlackList)
 
         // handle exception firstly
         val result = state.methodResult

diff --git a/usvm-ml-path-selection/src/main/kotlin/org/usvm/ps/Utils.kt b/usvm-ml-path-selection/src/main/kotlin/org/usvm/ps/Utils.kt
@@ -49,7 +49,7 @@ class IDGenerator {
     }
 }
 
-fun <Type> UPathConstraints<Type, *>.size(): Int {
+fun <Type> UPathConstraints<Type>.size(): Int {
     return numericConstraints.constraints().count() +
             this.equalityConstraints.distinctReferences.count() +
             this.equalityConstraints.equalReferences.count() +