Introduce utbot-light module

settings.gradle.kts

@@ -89,3 +89,5 @@ if (projectType == springEdition || projectType == ultimateEdition) {
 
 
 
+include("utbot-light")
+

utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt

@@ -145,6 +145,7 @@ class UtExpressionStructureCounter(private val input: Iterable<UtExpression>) :
     override fun visit(expr: UtAddNoOverflowExpression) = multipleExpressions(expr.left, expr.right)
 
     override fun visit(expr: UtSubNoOverflowExpression) = multipleExpressions(expr.left, expr.right)
+    override fun visit(expr: UtMulNoOverflowExpression)= multipleExpressions(expr.left, expr.right)
 
     override fun visit(expr: UtNegExpression): NestStat {
         val stat = buildState(expr.variable.expr)

utbot-api/build.gradle.kts

@@ -1,12 +0,0 @@
-import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
-
-plugins {
-    id("com.github.johnrengelman.shadow") version "7.1.2"
-}
-
-tasks {
-    withType<ShadowJar> {
-        archiveClassifier.set(" ")
-        minimize()
-    }
-}

utbot-core/build.gradle.kts

@@ -1,5 +1,3 @@
-import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
-
 val kotlinLoggingVersion: String by rootProject
 val junit4Version: String by rootProject
 
@@ -12,11 +10,4 @@ dependencies {
     implementation(group = "net.java.dev.jna", name = "jna-platform", version = "5.5.0")
 
     testImplementation(group = "junit", name = "junit", version = junit4Version)
-}
-
-tasks {
-    withType<ShadowJar> {
-        archiveClassifier.set(" ")
-        minimize()
-    }
 }

utbot-framework-api/build.gradle.kts

@@ -1,5 +1,3 @@
-import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
-
 val junit4Version: String by rootProject
 val sootVersion: String by rootProject
 val commonsLangVersion: String by rootProject
@@ -8,10 +6,6 @@ val rdVersion: String? by rootProject
 val kryoVersion: String? by rootProject
 val kryoSerializersVersion: String? by rootProject
 
-plugins {
-    id("com.github.johnrengelman.shadow") version "7.1.2"
-}
-
 dependencies {
     api(project(":utbot-core"))
     api(project(":utbot-api"))
@@ -30,11 +24,8 @@ dependencies {
     testImplementation(group = "junit", name = "junit", version = junit4Version)
 }
 
-tasks {
-    withType<ShadowJar> {
-        archiveClassifier.set(" ")
-        minimize()
-    }
+java {
+    withSourcesJar()
 }
 
 tasks {

utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt

@@ -576,6 +576,13 @@ object UtSettings : AbstractSettings(logger, defaultKeyForSettingsPath, defaultS
     var maxArraySize by getIntProperty(1024)
 
     // endregion
+
+    // region UTBot light related options
+    // Changes to improve symbolic engine for light version
+
+    var disableUnsatChecking by getBooleanProperty(false)
+
+    // endregion
 }
 
 /**
@@ -592,6 +599,11 @@ enum class PathSelectorType {
      */
     INHERITORS_SELECTOR,
 
+    /**
+     * [BFSSelector]
+     */
+    BFS_SELECTOR,
+
     /**
      * [SubpathGuidedSelector]
      */

utbot-framework-test/src/main/java/org/utbot/examples/manual/examples/Trivial.java

@@ -2,6 +2,10 @@
 
 public class Trivial {
     public int aMethod(int a) {
-        return a;
+        String s = "a";
+        if (a > 1) {
+            return s.length();
+        }
+        return s.length() + 1;
     }
 }

utbot-framework-test/src/test/java/org/utbot/examples/manual/UtBotJavaApiTest.java

@@ -18,6 +18,7 @@
 import org.utbot.examples.manual.examples.customer.C;
 import org.utbot.examples.manual.examples.customer.Demo9;
 import org.utbot.external.api.TestMethodInfo;
+import org.utbot.external.api.UnitTestBotLight;
 import org.utbot.external.api.UtBotJavaApi;
 import org.utbot.external.api.UtModelFactory;
 import org.utbot.framework.codegen.domain.ForceStaticMocking;
@@ -1306,7 +1307,16 @@ public void testFuzzingSimple() {
 
     @NotNull
     private String getClassPath(Class<?> clazz) {
-        return clazz.getProtectionDomain().getCodeSource().getLocation().getPath();
+        try {
+            return normalizePath(clazz.getProtectionDomain().getCodeSource().getLocation());
+        } catch (URISyntaxException e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    @NotNull
+    private String normalizePath(URL url) throws URISyntaxException {
+        return new File(url.toURI()).getPath();
     }
 
     @NotNull
@@ -1376,4 +1386,37 @@ public UtCompositeModel createArrayOfComplexArraysModel() {
                 classIdOfArrayOfComplexArraysClass,
                 Collections.singletonMap("array", arrayOfComplexArrayClasses));
     }
+
+    @Test
+    public void testUnitTestBotLight() {
+        String classpath = getClassPath(Trivial.class);
+        String dependencyClassPath = getDependencyClassPath();
+
+        UtCompositeModel model = modelFactory.
+                produceCompositeModel(
+                        classIdForType(Trivial.class)
+                );
+
+        EnvironmentModels environmentModels = new EnvironmentModels(
+                model,
+                Collections.singletonList(new UtPrimitiveModel(2)),
+                Collections.emptyMap()
+        );
+
+        Method methodUnderTest = PredefinedGeneratorParameters.getMethodByName(
+                Trivial.class,
+                "aMethod",
+                int.class
+        );
+
+        UnitTestBotLight.run(
+                (engine, state) -> System.err.println("Got a call:" + state.getStmt()),
+                new TestMethodInfo(
+                        methodUnderTest,
+                        environmentModels
+                ),
+                classpath,
+                dependencyClassPath
+        );
+    }
 }

utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionStateListener.kt

@@ -0,0 +1,10 @@
+package org.utbot.engine
+
+import org.utbot.engine.state.ExecutionState
+
+/**
+ * [UtBotSymbolicEngine] will fire an event every time it traverses new [ExecutionState].
+ */
+fun interface ExecutionStateListener {
+    fun visit(graph: InterProceduralUnitGraph, state: ExecutionState)
+}

utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt

@@ -4060,12 +4060,14 @@ class Traverser(
         val memory = symbolicState.memory
         val solver = symbolicState.solver
 
-        //no need to respect soft constraints in NestedMethod
-        val holder = solver.check(respectSoft = !environment.state.isInNestedMethod())
+        if (!UtSettings.disableUnsatChecking) {
+            //no need to respect soft constraints in NestedMethod
+            val holder = solver.check(respectSoft = !environment.state.isInNestedMethod())
 
-        if (holder !is UtSolverStatusSAT) {
-            logger.trace { "processResult<${environment.method.signature}> UNSAT" }
-            return
+            if (holder !is UtSolverStatusSAT) {
+                logger.trace { "processResult<${environment.method.signature}> UNSAT" }
+                return
+            }
         }
         val methodResult = MethodResult(symbolicResult)
 

utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt

@@ -48,11 +48,14 @@ import org.utbot.instrumentation.ConcreteExecutor
 import org.utbot.instrumentation.instrumentation.Instrumentation
 import org.utbot.instrumentation.instrumentation.execution.UtConcreteExecutionData
 import org.utbot.instrumentation.instrumentation.execution.UtConcreteExecutionResult
+import org.utbot.instrumentation.instrumentation.execution.UtExecutionInstrumentation
 import org.utbot.taint.*
 import org.utbot.taint.model.TaintConfiguration
 import soot.jimple.Stmt
 import soot.tagkit.ParamNamesTag
 import java.lang.reflect.Method
+import java.util.function.Consumer
+import java.util.function.Predicate
 import kotlin.math.min
 import kotlin.system.measureTimeMillis
 
@@ -80,6 +83,9 @@ private fun pathSelector(graph: InterProceduralUnitGraph, typeRegistry: TypeRegi
         PathSelectorType.INHERITORS_SELECTOR -> inheritorsSelector(graph, typeRegistry) {
             withStepsLimit(pathSelectorStepsLimit)
         }
+        PathSelectorType.BFS_SELECTOR -> bfsSelector(graph, StrategyOption.VISIT_COUNTING) {
+            withStepsLimit(pathSelectorStepsLimit)
+        }
         PathSelectorType.SUBPATH_GUIDED_SELECTOR -> subpathGuidedSelector(graph, StrategyOption.DISTANCE) {
             withStepsLimit(pathSelectorStepsLimit)
         }
@@ -141,6 +147,18 @@ class UtBotSymbolicEngine(
         mockerContext = applicationContext.mockerContext,
     )
 
+    private val stateListeners: MutableList<ExecutionStateListener> = mutableListOf();
+
+    fun addListener(listener: ExecutionStateListener): UtBotSymbolicEngine {
+        stateListeners += listener
+        return this
+    }
+
+    fun removeListener(listener: ExecutionStateListener): UtBotSymbolicEngine {
+        stateListeners -= listener
+        return this
+    }
+
     fun attachMockListener(mockListener: MockListener) = mocker.mockListenerController?.attach(mockListener)
 
     fun detachMockListener(mockListener: MockListener) = mocker.mockListenerController?.detach(mockListener)
@@ -216,6 +234,22 @@ class UtBotSymbolicEngine(
         .onStart { preTraverse() }
         .onCompletion { postTraverse() }
 
+    /**
+     * Traverse through all states and get results.
+     *
+     * This method is supposed to used when calling [traverse] is not suitable,
+     * e.g. from Java programs. It runs traversing with blocking style using callback
+     * to provide [UtResult].
+     */
+    @JvmOverloads
+    fun traverseAll(consumer: Consumer<UtResult> = Consumer { }) {
+        runBlocking {
+            traverse().collect {
+                consumer.accept(it)
+            }
+        }
+    }
+
     private fun traverseImpl(): Flow<UtResult> = flow {
 
         require(trackableResources.isEmpty())
@@ -252,7 +286,7 @@ class UtBotSymbolicEngine(
                             "queue size=${(pathSelector as? NonUniformRandomSearch)?.size ?: -1}"
                 }
 
-                if (controller.executeConcretely || statesForConcreteExecution.isNotEmpty()) {
+                if (UtSettings.useConcreteExecution && (controller.executeConcretely || statesForConcreteExecution.isNotEmpty())) {
                     val state = pathSelector.pollUntilFastSAT()
                         ?: statesForConcreteExecution.pollUntilSat(processUnknownStatesDuringConcreteExecution)
                         ?: break
@@ -316,6 +350,14 @@ class UtBotSymbolicEngine(
                         }
                     }
 
+                    // I am not sure this part works correctly when concrete execution is enabled.
+                    // todo test this part more accurate
+                    try {
+                        fireExecutionStateEvent(state)
+                    } catch (ce: CancellationException) {
+                        break
+                    }
+
                 } else {
                     val state = pathSelector.poll()
 
@@ -360,11 +402,27 @@ class UtBotSymbolicEngine(
 
                     // TODO: think about concise modifying globalGraph in Traverser and UtBotSymbolicEngine
                     globalGraph.visitNode(state)
+
+                    try {
+                        fireExecutionStateEvent(state)
+                    } catch (ce: CancellationException) {
+                        break
+                    }
                 }
             }
         }
     }
 
+    private fun fireExecutionStateEvent(state: ExecutionState) {
+        stateListeners.forEach { l ->
+            try {
+                l.visit(globalGraph, state)
+            } catch (t: Throwable) {
+                logger.error(t) { "$l failed with error" }
+            }
+        }
+    }
+
 
     /**
      * Run fuzzing flow.
@@ -516,7 +574,11 @@ class UtBotSymbolicEngine(
         val solver = state.solver
         val parameters = state.parameters.map { it.value }
         val symbolicResult = requireNotNull(state.methodResult?.symbolicResult) { "The state must have symbolicResult" }
-        val holder = requireNotNull(solver.lastStatus as? UtSolverStatusSAT) { "The state must be SAT!" }
+        val holder = if (UtSettings.disableUnsatChecking) {
+            (solver.lastStatus as? UtSolverStatusSAT) ?: return
+        } else {
+            requireNotNull(solver.lastStatus as? UtSolverStatusSAT) { "The state must be SAT!" }
+        }
 
         val predictedTestName = Predictors.testName.predict(state.path)
         Predictors.testName.provide(state.path, predictedTestName, "")

utbot-framework/src/main/kotlin/org/utbot/engine/pc/Simplificator.kt

@@ -607,6 +607,12 @@ open class Simplificator(
             applySimplification(expr.right)
         )
 
+    override fun visit(expr: UtMulNoOverflowExpression): UtExpression =
+        UtMulNoOverflowExpression(
+            applySimplification(expr.left),
+            applySimplification(expr.right)
+        )
+
     // CONFLUENCE:UtBot+Expression+Optimizations#UtBotExpressionOptimizations-negConcrete
     // Neg (Concrete a) ---> Concrete (-a)
     override fun visit(expr: UtNegExpression): UtExpression =

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt

@@ -805,6 +805,31 @@ data class UtSubNoOverflowExpression(
     override fun hashCode() = hashCode
 }
 
+data class UtMulNoOverflowExpression(
+    val left: UtExpression,
+    val right: UtExpression,
+) : UtBoolExpression() {
+    override val hashCode = Objects.hash(left, right)
+
+    override fun <TResult> accept(visitor: UtExpressionVisitor<TResult>): TResult = visitor.visit(this)
+
+    override fun toString() = "(mulNoOverflow $left $right)"
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (javaClass != other?.javaClass) return false
+
+        other as UtMulNoOverflowExpression
+
+        if (left != other.left) return false
+        if (right != other.right) return false
+
+        return true
+    }
+
+    override fun hashCode() = hashCode
+}
+
 data class UtNegExpression(val variable: PrimitiveValue) : UtExpression(alignSort(variable.type.toSort())) {
     override val hashCode = variable.hashCode
 

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpressionVisitor.kt

@@ -42,4 +42,5 @@ interface UtExpressionVisitor<TResult> {
     // Add and Sub with overflow detection
     fun visit(expr: UtAddNoOverflowExpression): TResult
     fun visit(expr: UtSubNoOverflowExpression): TResult
+    fun visit(expr: UtMulNoOverflowExpression): TResult
 }