From ff7b80fdd5411ceda560c04d6e5cb2af347cd086 Mon Sep 17 00:00:00 2001 From: Max Nigmatulin Date: Wed, 4 Oct 2023 15:50:43 +0300 Subject: [PATCH] Rebase --- .../kotlin/org/usvm/jvm/interpreter/JcBlockInterpreter.kt | 6 ++++-- usvm-ml-path-selection/src/main/kotlin/org/usvm/ps/Utils.kt | 2 +- 2 files changed, 5 insertions(+), 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 index 29da6006d8..afa804c623 100644 --- 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 = UForkBlackList.createDefault(), ) : UInterpreter() { companion object { @@ -67,7 +69,7 @@ class JcBlockInterpreter( } } - val solver = ctx.solver() + val solver = ctx.solver() 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 index d130748e59..cc451bdad2 100644 --- 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 UPathConstraints.size(): Int { +fun UPathConstraints.size(): Int { return numericConstraints.constraints().count() + this.equalityConstraints.distinctReferences.count() + this.equalityConstraints.equalReferences.count() +