Disable local memory simplifications

Author: sergeypospelov

utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/SetsTest.kt

@@ -34,6 +34,17 @@ internal class SetsTest : UtValueTestCaseChecker(
         )
     }
 
+    @Test
+    fun testSetContains2() {
+        check(
+            Sets::setContains2,
+            eq(3),
+            { s, _, _ -> s == null },
+            { s, a, r -> r!! && s != null && !s.contains(1 + a) },
+            { s, a, r -> !r!! && s != null && s.contains(1 + a) }
+        )
+    }
+
     @Test
     fun testSetContainsInteger() {
         check(

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

@@ -16,6 +16,7 @@ import org.utbot.engine.symbolic.*
 import org.utbot.engine.types.TypeResolver
 import org.utbot.framework.plugin.api.FieldId
 import org.utbot.framework.plugin.api.UtInstrumentation
+import soot.RefType
 import java.util.Objects
 import soot.Scene
 import soot.SootMethod

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

@@ -84,7 +84,6 @@ import org.utbot.engine.symbolic.asHardConstraint
 import org.utbot.engine.symbolic.asSoftConstraint
 import org.utbot.engine.symbolic.asAssumption
 import org.utbot.engine.symbolic.asUpdate
-import org.utbot.engine.symbolic.simplificators.LocalMemoryUpdateSimplificator
 import org.utbot.engine.symbolic.simplificators.MemoryUpdateSimplificator
 import org.utbot.engine.symbolic.simplificators.simplifySymbolicStateUpdate
 import org.utbot.engine.symbolic.simplificators.simplifySymbolicValue
@@ -316,7 +315,6 @@ class Traverser(
 
     private val simplificator = Simplificator()
     private val memoryUpdateSimplificator = with(simplificator) { MemoryUpdateSimplificator() }
-    private val localMemoryUpdateSimplificator = with(simplificator) { LocalMemoryUpdateSimplificator() }
 
     private fun TraversalContext.traverseStmt(current: Stmt) {
         if (doPreparatoryWorkIfRequired(current)) return
@@ -998,9 +996,10 @@ class Traverser(
                     createdValue
                 }
 
+
                 environment.state.parameters += Parameter(localVariable, identityRef.type, value)
 
-                val nextState = updateQueued(
+                val nextState = updateQueuedWithoutSimplification(
                     globalGraph.succ(current),
                     SymbolicStateUpdate(localMemoryUpdates = localMemoryUpdate(localVariable to value))
                 )
@@ -1449,6 +1448,8 @@ class Traverser(
                 is ArrayValue -> arrayInstanceOf(value, expr.checkType)
             }
             else -> TODO("$expr")
+        }.also {
+            with(simplificator) { simplifySymbolicValue(it) }
         }
 
     private fun initStringLiteral(stringWrapper: ObjectValue, value: String) {
@@ -3595,9 +3596,7 @@ class Traverser(
 
     private fun createExceptionStateQueued(exception: SymbolicFailure, update: SymbolicStateUpdate): ExecutionState {
         val simplifiedUpdates = with (memoryUpdateSimplificator) {
-            with(localMemoryUpdateSimplificator) {
-                simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update)
-            }
+            simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update)
         }
         val simplifiedResult = with(simplificator) {
             simplifySymbolicValue(exception.symbolic)
@@ -3609,10 +3608,8 @@ class Traverser(
     }
 
     private fun updateQueued(update: SymbolicStateUpdate): ExecutionState {
-        val symbolicStateUpdate = with(localMemoryUpdateSimplificator) {
-            with(memoryUpdateSimplificator) {
-                simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update)
-            }
+        val symbolicStateUpdate = with(memoryUpdateSimplificator) {
+            simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update)
         }
 
         return environment.state.update(
@@ -3625,34 +3622,45 @@ class Traverser(
         update: SymbolicStateUpdate = SymbolicStateUpdate(),
         doesntThrow: Boolean = false
     ): ExecutionState {
-        val symbolicStateUpdate = with(localMemoryUpdateSimplificator) {
+        val simplifiedUpdates =
             with(memoryUpdateSimplificator) {
                 simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update)
             }
-        }
 
         return environment.state.update(
             edge,
-            symbolicStateUpdate,
+            simplifiedUpdates,
             doesntThrow
         )
     }
 
+    private fun updateQueuedWithoutSimplification(
+        edge: Edge,
+        update: SymbolicStateUpdate = SymbolicStateUpdate(),
+        doesntThrow: Boolean = false
+    ): ExecutionState {
+        val updates = queuedSymbolicStateUpdates + update
+
+        return environment.state.update(
+            edge,
+            updates,
+            doesntThrow
+        )
+    }
+
+
     private fun pushQueued(
         graph: ExceptionalUnitGraph,
         parametersWithThis: List<SymbolicValue>,
         constraints: Set<UtBoolExpression>
     ): ExecutionState {
-        val updates = queuedSymbolicStateUpdates + constraints.asHardConstraint()
-        val simplifiedInputArguments = with (simplificator) {
-            ArrayDeque(parametersWithThis.map {
-                simplifySymbolicValue(it)
-            })
+        val simplifiedUpdates = with(memoryUpdateSimplificator) {
+            simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + constraints.asHardConstraint())
         }
         return environment.state.push(
             graph.head,
-            inputArguments = simplifiedInputArguments,
-            updates,
+            inputArguments = ArrayDeque(parametersWithThis),
+            simplifiedUpdates,
             graph.body.method
         )
     }

utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionState.kt

@@ -22,7 +22,6 @@ import org.utbot.framework.plugin.api.Step
 import soot.SootMethod
 import soot.jimple.Stmt
 import java.util.Objects
-import org.utbot.engine.symbolic.Assumption
 
 const val RETURN_DECISION_NUM = -1
 const val CALL_DECISION_NUM = -2

utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/simplificators/LocalMemoryUpdateSimplificator.kt

@@ -60,10 +60,9 @@ fun simplifySymbolicValue(value: SymbolicValue): SymbolicValue =
     }
 
 
-context(MemoryUpdateSimplificator, LocalMemoryUpdateSimplificator)
+context(MemoryUpdateSimplificator)
 fun simplifySymbolicStateUpdate(update: SymbolicStateUpdate) =
     with(update) {
         val memoryUpdates = simplify(memoryUpdates)
-        val localMemoryUpdates = simplify(localMemoryUpdates)
-        copy(memoryUpdates = memoryUpdates, localMemoryUpdates = localMemoryUpdates)
+        copy(memoryUpdates = memoryUpdates)
     }

utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/simplificators/Util.kt

@@ -30,6 +30,13 @@ public Set<Integer> setContainsInteger(Set<Integer> set, Integer a, Integer b) {
         }
     }
 
+    public boolean setContains2(Set<Integer> st, int a) {
+        if (st.contains(1 + a)) {
+            return false;
+        }
+        return true;
+    }
+
     @SuppressWarnings("RedundantIfStatement")
     public boolean setContains(Set<String> set, String str, String str2) {
         if (set.contains("aaa" + str)) {