From 9af32d139fd4c4f1298f81aa61c9095bf5d94fac Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 11:37:04 +0800 Subject: [PATCH 1/6] Refactor: move ExecutionState.kt to package --- .../utbot/features/FeatureExtractorImpl.kt | 2 +- .../FeatureProcessorWithStatesRepetition.kt | 2 +- .../org/utbot/analytics/FeatureExtractor.kt | 2 +- .../kotlin/org/utbot/engine/DataClasses.kt | 1 + .../kotlin/org/utbot/engine/Extensions.kt | 1 + .../utbot/engine/InterProceduralUnitGraph.kt | 3 + .../main/kotlin/org/utbot/engine/Memory.kt | 22 --- .../org/utbot/engine/TraversalContext.kt | 2 + .../main/kotlin/org/utbot/engine/Traverser.kt | 9 + .../org/utbot/engine/UtBotSymbolicEngine.kt | 3 + .../org/utbot/engine/selectors/BFSSelector.kt | 2 +- .../engine/selectors/BasePathSelector.kt | 2 +- .../org/utbot/engine/selectors/DFSSelector.kt | 2 +- .../engine/selectors/InterleavedSelector.kt | 2 +- .../org/utbot/engine/selectors/MLSelector.kt | 2 +- .../utbot/engine/selectors/PathSelector.kt | 2 +- .../org/utbot/engine/selectors/PathsTree.kt | 2 +- .../engine/selectors/RandomPathSelector.kt | 2 +- .../utbot/engine/selectors/RandomSelector.kt | 2 +- .../engine/selectors/nurs/CPInstSelector.kt | 2 +- .../selectors/nurs/CoveredNewSelector.kt | 2 +- .../engine/selectors/nurs/DepthSelector.kt | 2 +- .../selectors/nurs/ForkDepthSelector.kt | 2 +- .../engine/selectors/nurs/GreedySearch.kt | 2 +- .../selectors/nurs/InheritorsSelector.kt | 2 +- .../nurs/MinimalDistanceToUncovered.kt | 2 +- .../engine/selectors/nurs/NeuroSatSelector.kt | 2 +- .../selectors/nurs/NonUniformRandomSearch.kt | 2 +- .../utbot/engine/selectors/nurs/RPSelector.kt | 2 +- .../selectors/nurs/SubpathGuidedSelector.kt | 2 +- .../selectors/nurs/VisitCountingSelector.kt | 2 +- .../selectors/strategies/ChoosingStrategy.kt | 2 +- .../strategies/DistanceStatistics.kt | 4 +- .../strategies/EdgeVisitCountingStatistics.kt | 4 +- .../GeneratedTestCountingStatistics.kt | 2 +- .../engine/selectors/strategies/GraphViz.kt | 7 +- .../strategies/StatementsStatistics.kt | 2 +- .../strategies/StepsLimitStoppingStrategy.kt | 4 +- .../selectors/strategies/SubpathStatistics.kt | 6 +- .../strategies/TraverseGraphStatistics.kt | 4 +- .../engine/state/ExecutionStackElement.kt | 58 ++++++ .../engine/{ => state}/ExecutionState.kt | 179 ++---------------- .../engine/state/ExecutionStateUpdates.kt | 152 +++++++++++++++ .../utbot/engine/symbolic/SymbolicState.kt | 3 +- 44 files changed, 283 insertions(+), 233 deletions(-) create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt rename utbot-framework/src/main/kotlin/org/utbot/engine/{ => state}/ExecutionState.kt (58%) create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStateUpdates.kt diff --git a/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureExtractorImpl.kt b/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureExtractorImpl.kt index 6786c9847a..ddf1322659 100644 --- a/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureExtractorImpl.kt +++ b/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureExtractorImpl.kt @@ -1,7 +1,7 @@ package org.utbot.features import org.utbot.analytics.FeatureExtractor -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.selectors.strategies.StatementsStatistics import org.utbot.engine.selectors.strategies.SubpathStatistics diff --git a/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureProcessorWithStatesRepetition.kt b/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureProcessorWithStatesRepetition.kt index 49f9427678..62e7e398d3 100644 --- a/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureProcessorWithStatesRepetition.kt +++ b/utbot-analytics/src/main/kotlin/org/utbot/features/FeatureProcessorWithStatesRepetition.kt @@ -2,7 +2,7 @@ package org.utbot.features import org.utbot.analytics.EngineAnalyticsContext import org.utbot.analytics.FeatureProcessor -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.framework.UtSettings import soot.jimple.Stmt diff --git a/utbot-framework/src/main/kotlin/org/utbot/analytics/FeatureExtractor.kt b/utbot-framework/src/main/kotlin/org/utbot/analytics/FeatureExtractor.kt index c86cad1b54..e63ccdcc92 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/analytics/FeatureExtractor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/analytics/FeatureExtractor.kt @@ -1,6 +1,6 @@ package org.utbot.analytics -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState /** * Class that encapsulates work with FeatureExtractor during symbolic execution. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index 8c964717ce..e2178613df 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -11,6 +11,7 @@ import org.utbot.engine.pc.UtIsExpression import org.utbot.engine.pc.UtTrue import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkOr +import org.utbot.engine.state.ExecutionState import org.utbot.engine.symbolic.* import org.utbot.engine.types.TypeResolver import org.utbot.framework.plugin.api.FieldId diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt index b958d1650f..298046fa99 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt @@ -29,6 +29,7 @@ import org.utbot.engine.pc.mkInt import org.utbot.engine.pc.mkLong import org.utbot.engine.pc.mkShort import org.utbot.engine.pc.toSort +import org.utbot.engine.state.ExecutionState import org.utbot.framework.UtSettings.checkNpeInNestedMethods import org.utbot.framework.UtSettings.checkNpeInNestedNotPrivateMethods import org.utbot.framework.plugin.api.FieldId diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/InterProceduralUnitGraph.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/InterProceduralUnitGraph.kt index ff533b1085..c732463d37 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/InterProceduralUnitGraph.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/InterProceduralUnitGraph.kt @@ -1,6 +1,9 @@ package org.utbot.engine import org.utbot.engine.selectors.strategies.TraverseGraphStatistics +import org.utbot.engine.state.CALL_DECISION_NUM +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import soot.SootClass import soot.SootMethod import soot.jimple.Stmt diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt index ef92b7a419..8ad3f24469 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt @@ -49,28 +49,6 @@ import soot.Scene import soot.Type -/** - * Represents a memory associated with a certain method call. For now consists only of local variables mapping. - * TODO: think on other fields later - * - * @param [locals] represents a mapping from [LocalVariable]s of a specific method call to [SymbolicValue]s. - */ -data class LocalVariableMemory( - private val locals: PersistentMap = persistentHashMapOf() -) { - fun memoryForNestedMethod(): LocalVariableMemory = this.copy(locals = persistentHashMapOf()) - - fun update(update: LocalMemoryUpdate): LocalVariableMemory = this.copy(locals = locals.update(update.locals)) - - /** - * Returns local variable value. - */ - fun local(variable: LocalVariable): SymbolicValue? = locals[variable] - - val localValues: Set - get() = locals.values.toSet() -} - /** * Local memory implementation based on arrays. * diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/TraversalContext.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/TraversalContext.kt index 22a9c19304..99fa3836e5 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/TraversalContext.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/TraversalContext.kt @@ -1,5 +1,7 @@ package org.utbot.engine +import org.utbot.engine.state.ExecutionState + /** * Represents a mutable _Context_ during the [ExecutionState] traversing. This _Context_ consists of all mutable and * immutable properties and fields which are created and updated during analysis of a **single** Jimple instruction. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 3c5bda0c03..92e62ae907 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -66,6 +66,15 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState +import org.utbot.engine.state.LocalVariableMemory +import org.utbot.engine.state.StateLabel +import org.utbot.engine.state.createExceptionState +import org.utbot.engine.state.pop +import org.utbot.engine.state.push +import org.utbot.engine.state.update +import org.utbot.engine.state.withLabel import org.utbot.engine.symbolic.emptyAssumption import org.utbot.engine.symbolic.emptyHardConstraint import org.utbot.engine.symbolic.emptySoftConstraint diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt index 590c6f69bb..b4ea2a84a2 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt @@ -101,6 +101,9 @@ import kotlinx.coroutines.flow.onStart import kotlinx.coroutines.isActive import kotlinx.coroutines.job import kotlinx.coroutines.yield +import org.utbot.engine.state.ExecutionStackElement +import org.utbot.engine.state.ExecutionState +import org.utbot.engine.state.StateLabel import org.utbot.engine.types.TypeRegistry import org.utbot.engine.types.TypeResolver import org.utbot.framework.plugin.api.UtExecutionSuccess diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BFSSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BFSSelector.kt index 6feb62b352..f28d2449c0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BFSSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BFSSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt index 0e400f527a..2f7c680f5d 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.isPreconditionCheckMethod import org.utbot.engine.pathLogger import org.utbot.engine.pc.UtSolver diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/DFSSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/DFSSelector.kt index 9e1eba3c1b..92ad407d12 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/DFSSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/DFSSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/InterleavedSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/InterleavedSelector.kt index b46f933d66..401d9094a7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/InterleavedSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/InterleavedSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState /** * Retrieves states from different pathSelectors in rotation. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/MLSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/MLSelector.kt index 1e4b17de0a..78f12dceb1 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/MLSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/MLSelector.kt @@ -2,7 +2,7 @@ package org.utbot.engine.selectors import org.utbot.analytics.EngineAnalyticsContext import org.utbot.analytics.Predictors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.selectors.nurs.GreedySearch import org.utbot.engine.selectors.strategies.ChoosingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelector.kt index 9e98743b20..9406d03b78 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.pc.UtSolverStatusKind /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathsTree.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathsTree.kt index f908eb4fdb..7618877531 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathsTree.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/PathsTree.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import java.util.NoSuchElementException import kotlin.random.Random diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomPathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomPathSelector.kt index 844dcce9c8..64f48f544b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomPathSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomPathSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy import kotlin.random.Random diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomSelector.kt index 76245cb4a7..c27156f1ad 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/RandomSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy import kotlin.random.Random diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CPInstSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CPInstSelector.kt index 261dfc2fc2..e39e7456f0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CPInstSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CPInstSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StatementsStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CoveredNewSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CoveredNewSelector.kt index 01a98b4e82..5e3e4b5ffc 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CoveredNewSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/CoveredNewSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.DistanceStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/DepthSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/DepthSelector.kt index 5962db8768..5885df02c7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/DepthSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/DepthSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/ForkDepthSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/ForkDepthSelector.kt index 7c5e27aaf7..78ed6a93c0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/ForkDepthSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/ForkDepthSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/GreedySearch.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/GreedySearch.kt index b00d67e871..1fe1985489 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/GreedySearch.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/GreedySearch.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.BasePathSelector import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt index 611f9e0cb6..317a436736 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/InheritorsSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.types.TypeRegistry import org.utbot.engine.selectors.strategies.DistanceStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/MinimalDistanceToUncovered.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/MinimalDistanceToUncovered.kt index 3f56367ead..a3ab7f8f58 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/MinimalDistanceToUncovered.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/MinimalDistanceToUncovered.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.DistanceStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NeuroSatSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NeuroSatSelector.kt index 3736227a06..596c91492d 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NeuroSatSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NeuroSatSelector.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.nurs import org.utbot.analytics.Predictors -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NonUniformRandomSearch.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NonUniformRandomSearch.kt index 4e2d741240..6c10f233a0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NonUniformRandomSearch.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/NonUniformRandomSearch.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.BasePathSelector import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/RPSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/RPSelector.kt index d7e06e2d37..b201104802 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/RPSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/RPSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy import kotlin.math.pow diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/SubpathGuidedSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/SubpathGuidedSelector.kt index a17e94a6a2..f6a43fa0a5 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/SubpathGuidedSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/SubpathGuidedSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.ChoosingStrategy import org.utbot.engine.selectors.strategies.StoppingStrategy import org.utbot.engine.selectors.strategies.SubpathStatistics diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/VisitCountingSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/VisitCountingSelector.kt index 6e69e29dbb..e455d2d124 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/VisitCountingSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/nurs/VisitCountingSelector.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.nurs -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.selectors.strategies.EdgeVisitCountingStatistics import org.utbot.engine.selectors.strategies.StoppingStrategy diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ChoosingStrategy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ChoosingStrategy.kt index f52de7e622..0d08a7f0dd 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ChoosingStrategy.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/ChoosingStrategy.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt index 9c3e7163d8..9c1cfc16c1 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.isReturn import org.utbot.engine.pathLogger diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt index b38e1b2b94..8813973475 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.pathLogger import org.utbot.framework.UtSettings.enableLoggingForDroppedStates diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GeneratedTestCountingStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GeneratedTestCountingStatistics.kt index 315673e042..88163e49a1 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GeneratedTestCountingStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GeneratedTestCountingStatistics.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph class GeneratedTestCountingStatistics( diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GraphViz.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GraphViz.kt index fb603aad14..1cf9c38ec7 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GraphViz.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/GraphViz.kt @@ -2,9 +2,9 @@ package org.utbot.engine.selectors.strategies import mu.KotlinLogging import org.utbot.common.FileUtil.createNewFileWithParentDirectories -import org.utbot.engine.CALL_DECISION_NUM -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.CALL_DECISION_NUM +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.isLibraryNonOverriddenClass import org.utbot.engine.isReturn @@ -17,7 +17,6 @@ import soot.toolkits.graph.ExceptionalUnitGraph import java.awt.Toolkit import java.awt.datatransfer.StringSelection import java.io.FileWriter -import java.nio.file.Files import java.nio.file.Paths import org.utbot.common.FileUtil diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StatementsStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StatementsStatistics.kt index 375462191c..88d140b6ab 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StatementsStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StatementsStatistics.kt @@ -1,6 +1,6 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import soot.SootMethod import soot.jimple.Stmt diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt index f17d2b6750..a520afa1d5 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.pathLogger diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/SubpathStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/SubpathStatistics.kt index 0110cf03c9..2ecefd06e3 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/SubpathStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/SubpathStatistics.kt @@ -1,8 +1,8 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.CALL_DECISION_NUM -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.CALL_DECISION_NUM +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.framework.UtSettings import kotlin.math.pow diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/TraverseGraphStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/TraverseGraphStatistics.kt index 7ec9abedc0..2b4feac95e 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/TraverseGraphStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/TraverseGraphStatistics.kt @@ -1,7 +1,7 @@ package org.utbot.engine.selectors.strategies -import org.utbot.engine.Edge -import org.utbot.engine.ExecutionState +import org.utbot.engine.state.Edge +import org.utbot.engine.state.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import soot.jimple.Stmt import soot.toolkits.graph.ExceptionalUnitGraph diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt new file mode 100644 index 0000000000..da70be840d --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt @@ -0,0 +1,58 @@ +package org.utbot.engine.state + +import kotlinx.collections.immutable.PersistentMap +import kotlinx.collections.immutable.persistentHashMapOf +import org.utbot.engine.LocalMemoryUpdate +import org.utbot.engine.LocalVariable +import org.utbot.engine.Parameter +import org.utbot.engine.SymbolicValue +//import org.utbot.engine.symbolic.simplificators.LocalMemoryUpdateSimplificator +import org.utbot.engine.update +import soot.SootMethod +import soot.jimple.Stmt + +/** + * The stack element of the [ExecutionState]. + * Contains properties, that are suitable for specified method in call stack. + * + * @param doesntThrow if true, then engine should drop states with throwing exceptions. + * @param localVariableMemory the local memory associated with the current stack element. + */ +data class ExecutionStackElement( + val caller: Stmt?, + val localVariableMemory: LocalVariableMemory = LocalVariableMemory(), + val parameters: MutableList = mutableListOf(), + val inputArguments: ArrayDeque = ArrayDeque(), + val doesntThrow: Boolean = false, + val method: SootMethod, +) { + fun update(memoryUpdate: LocalMemoryUpdate, doesntThrow: Boolean = this.doesntThrow) = + this.copy(localVariableMemory = localVariableMemory.update(memoryUpdate), doesntThrow = doesntThrow) +} + +/** + * Represents a memory associated with a certain method call. For now consists only of local variables mapping. + * TODO: think on other fields later + * + * @param [locals] represents a mapping from [LocalVariable]s of a specific method call to [SymbolicValue]s. + */ +data class LocalVariableMemory( + private val locals: PersistentMap = persistentHashMapOf() +) { + fun memoryForNestedMethod(): LocalVariableMemory = this.copy(locals = persistentHashMapOf()) + + fun update(update: LocalMemoryUpdate): LocalVariableMemory = this.copy(locals = locals.update(update.locals)) + + /** + * Returns local variable value. + */ + fun local(variable: LocalVariable): SymbolicValue? = locals[variable] + + val localValues: Set + get() = locals.values.toSet() +} +// +//context(LocalMemoryUpdateSimplificator) +//fun updateSimplified(localVariableMemory: LocalVariableMemory, update: LocalMemoryUpdate): LocalVariableMemory { +// return localVariableMemory.update(simplify(update)) +//} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionState.kt similarity index 58% rename from utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt rename to utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionState.kt index 4adba75615..6bb6f88f80 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionState.kt @@ -1,4 +1,4 @@ -package org.utbot.engine +package org.utbot.engine.state import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.PersistentMap @@ -6,18 +6,22 @@ import kotlinx.collections.immutable.PersistentSet import kotlinx.collections.immutable.persistentHashMapOf import kotlinx.collections.immutable.persistentHashSetOf import kotlinx.collections.immutable.persistentListOf -import kotlinx.collections.immutable.plus import org.utbot.common.md5 +import org.utbot.engine.Memory +import org.utbot.engine.MethodResult +import org.utbot.engine.SymbolicFailure import org.utbot.engine.pc.UtSolver import org.utbot.engine.pc.UtSolverStatusUNDEFINED +import org.utbot.engine.state.StateLabel.CONCRETE +import org.utbot.engine.state.StateLabel.INTERMEDIATE +import org.utbot.engine.state.StateLabel.TERMINAL +import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.SymbolicState -import org.utbot.engine.symbolic.SymbolicStateUpdate import org.utbot.framework.UtSettings 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 @@ -59,25 +63,6 @@ enum class StateLabel { CONCRETE } -/** - * The stack element of the [ExecutionState]. - * Contains properties, that are suitable for specified method in call stack. - * - * @param doesntThrow if true, then engine should drop states with throwing exceptions. - * @param localVariableMemory the local memory associated with the current stack element. - */ -data class ExecutionStackElement( - val caller: Stmt?, - val localVariableMemory: LocalVariableMemory = LocalVariableMemory(), - val parameters: MutableList = mutableListOf(), - val inputArguments: ArrayDeque = ArrayDeque(), - val doesntThrow: Boolean = false, - val method: SootMethod, -) { - fun update(memoryUpdate: LocalMemoryUpdate, doesntThrow: Boolean = this.doesntThrow) = - this.copy(localVariableMemory = localVariableMemory.update(memoryUpdate), doesntThrow = doesntThrow) -} - /** * Class that store all information about execution state that needed only for analytics module */ @@ -148,14 +133,14 @@ data class ExecutionState( val lastMethod: SootMethod? = null, val methodResult: MethodResult? = null, val exception: SymbolicFailure? = null, - val label: StateLabel = StateLabel.INTERMEDIATE, - private var stateAnalyticsProperties: StateAnalyticsProperties = StateAnalyticsProperties() + val label: StateLabel = INTERMEDIATE, + var stateAnalyticsProperties: StateAnalyticsProperties = StateAnalyticsProperties() ) : AutoCloseable { val solver: UtSolver by symbolicState::solver val memory: Memory by symbolicState::memory - private var outgoingEdges = 0 + var outgoingEdges = 0 fun isInNestedMethod() = executionStack.size > 1 @@ -181,144 +166,6 @@ data class ExecutionState( val isInsideStaticInitializer get() = executionStack.any { it.method.isStaticInitializer } - fun createExceptionState( - exception: SymbolicFailure, - update: SymbolicStateUpdate - ): ExecutionState { - val last = executionStack.last() - // go to negative indexing below CALL_DECISION_NUM for exceptions - val edge = Edge(stmt, stmt, CALL_DECISION_NUM - (++outgoingEdges)) - return ExecutionState( - stmt = stmt, - symbolicState = symbolicState + update, - executionStack = executionStack.set(executionStack.lastIndex, last.update(update.localMemoryUpdates)), - path = path, - visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath, - decisionPath = decisionPath + edge.decisionNum, - edges = edges + edge, - stmts = stmts, - pathLength = pathLength + 1, - lastEdge = edge, - lastMethod = executionStack.last().method, - exception = exception, - label = label, - stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) - ) - } - - fun pop(methodResult: MethodResult): ExecutionState { - val caller = executionStack.last().caller!! - val edge = Edge(stmt, caller, RETURN_DECISION_NUM) - - val stmtHashcode = stmt.hashCode() - val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashcode] ?: 0) + 1 - - return ExecutionState( - stmt = caller, - symbolicState = symbolicState, - executionStack = executionStack.removeAt(executionStack.lastIndex), - path = path + stmt, - visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( - stmtHashcode, - stmtCountInPath - ), - decisionPath = decisionPath + edge.decisionNum, - edges = edges + edge, - stmts = stmts.putIfAbsent(stmt, pathLength), - pathLength = pathLength + 1, - lastEdge = edge, - lastMethod = executionStack.last().method, - methodResult = methodResult, - label = label, - stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) - ) - } - - fun push( - stmt: Stmt, - inputArguments: ArrayDeque, - update: SymbolicStateUpdate, - method: SootMethod - ): ExecutionState { - val edge = Edge(this.stmt, stmt, CALL_DECISION_NUM) - val stackElement = ExecutionStackElement( - this.stmt, - localVariableMemory = localVariableMemory.memoryForNestedMethod().update(update.localMemoryUpdates), - inputArguments = inputArguments, - method = method, - doesntThrow = executionStack.last().doesntThrow - ) - outgoingEdges++ - - val stmtHashCode = this.stmt.hashCode() - val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashCode] ?: 0) + 1 - - return ExecutionState( - stmt = stmt, - symbolicState = symbolicState.stateForNestedMethod() + update, - executionStack = executionStack + stackElement, - path = path + this.stmt, - visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( - stmtHashCode, - stmtCountInPath - ), - decisionPath = decisionPath + edge.decisionNum, - edges = edges + edge, - stmts = stmts.putIfAbsent(this.stmt, pathLength), - pathLength = pathLength + 1, - lastEdge = edge, - lastMethod = stackElement.method, - label = label, - stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) - ) - } - - fun update( - stateUpdate: SymbolicStateUpdate - ): ExecutionState { - val last = executionStack.last() - val stackElement = last.update(stateUpdate.localMemoryUpdates) - return copy( - symbolicState = symbolicState + stateUpdate, - executionStack = executionStack.set(executionStack.lastIndex, stackElement) - ) - } - - fun update( - edge: Edge, - symbolicStateUpdate: SymbolicStateUpdate, - doesntThrow: Boolean, - ): ExecutionState { - val last = executionStack.last() - val stackElement = last.update( - symbolicStateUpdate.localMemoryUpdates, - last.doesntThrow || doesntThrow - ) - outgoingEdges++ - - val stmtHashCode = stmt.hashCode() - val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashCode] ?: 0) + 1 - - return ExecutionState( - stmt = edge.dst, - symbolicState = symbolicState + symbolicStateUpdate, - executionStack = executionStack.set(executionStack.lastIndex, stackElement), - path = path + stmt, - visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( - stmtHashCode, - stmtCountInPath - ), - decisionPath = decisionPath + edge.decisionNum, - edges = edges + edge, - stmts = stmts.putIfAbsent(stmt, pathLength), - pathLength = pathLength + 1, - lastEdge = edge, - lastMethod = stackElement.method, - label = label, - stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) - ) - } - /** * Tell to solver that states with status [UtSolverStatusUNDEFINED] can be created from current state. * @@ -328,8 +175,6 @@ data class ExecutionState( solver.expectUndefined = true } - fun withLabel(newLabel: StateLabel) = copy(label = newLabel) - override fun close() { solver.close() } @@ -417,7 +262,7 @@ data class ExecutionState( private val hashCode by lazy { Objects.hash( - stmt, symbolicState, executionStack, path, visitedStatementsHashesToCountInPath, decisionPath, + stmt, executionStack, path, visitedStatementsHashesToCountInPath, decisionPath, edges, stmts, pathLength, lastEdge, lastMethod, methodResult, exception ) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStateUpdates.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStateUpdates.kt new file mode 100644 index 0000000000..c7052a3016 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStateUpdates.kt @@ -0,0 +1,152 @@ +package org.utbot.engine.state + +import kotlinx.collections.immutable.plus +import org.utbot.engine.MethodResult +import org.utbot.engine.SymbolicFailure +import org.utbot.engine.SymbolicValue +import org.utbot.engine.putIfAbsent +import org.utbot.engine.symbolic.SymbolicStateUpdate +import soot.SootMethod +import soot.jimple.Stmt + +fun ExecutionState.createExceptionState( + exception: SymbolicFailure, + update: SymbolicStateUpdate +): ExecutionState { + val last = executionStack.last() + // go to negative indexing below CALL_DECISION_NUM for exceptions + val edge = Edge(stmt, stmt, CALL_DECISION_NUM - (++outgoingEdges)) + val localMemory = last.update(update.localMemoryUpdates) + return ExecutionState( + stmt = stmt, + symbolicState = symbolicState + update, + executionStack = executionStack.set(executionStack.lastIndex, localMemory), + path = path, + visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath, + decisionPath = decisionPath + edge.decisionNum, + edges = edges + edge, + stmts = stmts, + pathLength = pathLength + 1, + lastEdge = edge, + lastMethod = executionStack.last().method, + exception = exception, + label = label, + stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) + ) +} + +fun ExecutionState.update( + edge: Edge, + symbolicStateUpdate: SymbolicStateUpdate, + doesntThrow: Boolean, +): ExecutionState { + val last = executionStack.last() + val stackElement = last.update( + symbolicStateUpdate.localMemoryUpdates, + last.doesntThrow || doesntThrow + ) + outgoingEdges++ + + val stmtHashCode = stmt.hashCode() + val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashCode] ?: 0) + 1 + + return ExecutionState( + stmt = edge.dst, + symbolicState = symbolicState + symbolicStateUpdate, + executionStack = executionStack.set(executionStack.lastIndex, stackElement), + path = path + stmt, + visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( + stmtHashCode, + stmtCountInPath + ), + decisionPath = decisionPath + edge.decisionNum, + edges = edges + edge, + stmts = stmts.putIfAbsent(stmt, pathLength), + pathLength = pathLength + 1, + lastEdge = edge, + lastMethod = stackElement.method, + label = label, + stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) + ) +} + +fun ExecutionState.withLabel(newLabel: StateLabel) = copy(label = newLabel) + + +fun ExecutionState.update( + stateUpdate: SymbolicStateUpdate +): ExecutionState { + val last = executionStack.last() + val stackElement = last.update(stateUpdate.localMemoryUpdates) + return copy( + symbolicState = symbolicState + stateUpdate, + executionStack = executionStack.set(executionStack.lastIndex, stackElement) + ) +} + +fun ExecutionState.push( + stmt: Stmt, + inputArguments: ArrayDeque, + update: SymbolicStateUpdate, + method: SootMethod +): ExecutionState { + val edge = Edge(this.stmt, stmt, CALL_DECISION_NUM) + val stackElement = ExecutionStackElement( + this.stmt, + localVariableMemory.memoryForNestedMethod().update(update.localMemoryUpdates), + inputArguments = inputArguments, + method = method, + doesntThrow = executionStack.last().doesntThrow + ) + outgoingEdges++ + + val stmtHashCode = this.stmt.hashCode() + val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashCode] ?: 0) + 1 + + return ExecutionState( + stmt = stmt, + symbolicState = symbolicState.stateForNestedMethod() + update, + executionStack = executionStack + stackElement, + path = path + this.stmt, + visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( + stmtHashCode, + stmtCountInPath + ), + decisionPath = decisionPath + edge.decisionNum, + edges = edges + edge, + stmts = stmts.putIfAbsent(this.stmt, pathLength), + pathLength = pathLength + 1, + lastEdge = edge, + lastMethod = stackElement.method, + label = label, + stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) + ) +} + +fun ExecutionState.pop(methodResult: MethodResult): ExecutionState { + val caller = executionStack.last().caller!! + val edge = Edge(stmt, caller, RETURN_DECISION_NUM) + + val stmtHashcode = stmt.hashCode() + val stmtCountInPath = (visitedStatementsHashesToCountInPath[stmtHashcode] ?: 0) + 1 + + return ExecutionState( + stmt = caller, + symbolicState = symbolicState, + executionStack = executionStack.removeAt(executionStack.lastIndex), + path = path + stmt, + visitedStatementsHashesToCountInPath = visitedStatementsHashesToCountInPath.put( + stmtHashcode, + stmtCountInPath + ), + decisionPath = decisionPath + edge.decisionNum, + edges = edges + edge, + stmts = stmts.putIfAbsent(stmt, pathLength), + pathLength = pathLength + 1, + lastEdge = edge, + lastMethod = executionStack.last().method, + methodResult = methodResult, + label = label, + stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this) + ) +} \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt index cbe2d5c7ef..facd1b8f39 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt @@ -35,5 +35,4 @@ data class SymbolicState( fun stateForNestedMethod() = copy( memory = memory.memoryForNestedMethod() ) - -} \ No newline at end of file +} From 653a8c86e4f60333ca77efaaf74e22ce4c67de98 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 11:44:26 +0800 Subject: [PATCH 2/6] Refactor: inline property --- .../src/main/kotlin/org/utbot/engine/DataClasses.kt | 2 -- .../src/main/kotlin/org/utbot/engine/Traverser.kt | 7 ++----- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index e2178613df..367386ee54 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -161,8 +161,6 @@ data class MethodResult( val symbolicResult: SymbolicResult, val symbolicStateUpdate: SymbolicStateUpdate = SymbolicStateUpdate() ) : InvokeResult() { - val memoryUpdates by symbolicStateUpdate::memoryUpdates - constructor( symbolicResult: SymbolicResult, hardConstraints: HardConstraint = emptyHardConstraint(), diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 92e62ae907..1ba6abe60b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -212,8 +212,6 @@ import java.lang.reflect.GenericArrayType import java.lang.reflect.TypeVariable import java.lang.reflect.WildcardType import java.util.concurrent.atomic.AtomicInteger -import kotlin.reflect.full.instanceParameter -import kotlin.reflect.jvm.javaType private val CAUGHT_EXCEPTION = LocalVariable("@caughtexception") @@ -682,7 +680,7 @@ class Traverser( } private fun isStaticInstanceInMethodResult(id: ClassId, methodResult: MethodResult?) = - methodResult != null && id in methodResult.memoryUpdates.staticInstanceStorage + methodResult != null && id in methodResult.symbolicStateUpdate.memoryUpdates.staticInstanceStorage private fun TraversalContext.skipVerticesForThrowableCreation(current: JAssignStmt) { val rightType = current.rightOp.type as RefType @@ -1030,7 +1028,6 @@ class Traverser( */ private fun updateGenericTypeInfo(identityRef: IdentityRef, value: ReferenceValue) { val callable = methodUnderTest.executable - val kCallable = ::updateGenericTypeInfo val type = if (identityRef is ThisRef) { // TODO: for ThisRef both methods don't return parameterized type if (methodUnderTest.isConstructor) { @@ -2359,7 +2356,7 @@ class Traverser( MethodResult( mockValue, hardConstraints = additionalConstraint.asHardConstraint(), - memoryUpdates = if (isInternalMock) MemoryUpdate() else mockMethodResult.memoryUpdates + memoryUpdates = if (isInternalMock) MemoryUpdate() else mockMethodResult.symbolicStateUpdate.memoryUpdates ) ) } From 57f18d75d18d9fd32f6dfeaf1babee901407bf9d Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 11:48:40 +0800 Subject: [PATCH 3/6] Refactor: remove `runBlocking` from tests --- .../TestSpecificTestCaseGenerator.kt | 45 +++++++++---------- 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt index 3ab7e3d33f..764c648e27 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/tests/infrastructure/TestSpecificTestCaseGenerator.kt @@ -1,9 +1,8 @@ package org.utbot.tests.infrastructure import kotlinx.coroutines.launch +import kotlinx.coroutines.runBlocking import mu.KotlinLogging -import org.utbot.common.runBlockingWithCancellationPredicate -import org.utbot.common.runIgnoringCancellationException import org.utbot.engine.EngineController import org.utbot.engine.Mocker import org.utbot.engine.UtBotSymbolicEngine @@ -61,32 +60,30 @@ class TestSpecificTestCaseGenerator( val forceMockListener = ForceMockListener.create(this, conflictTriggers, cancelJob = false) val forceStaticMockListener = ForceStaticMockListener.create(this, conflictTriggers, cancelJob = false) - runIgnoringCancellationException { - runBlockingWithCancellationPredicate(isCanceled) { - val controller = EngineController() - controller.job = launch { - super - .generateAsync(controller, method, mockStrategy, mockAlwaysDefaults, defaultTimeEstimator) - .collect { - when (it) { - is UtExecution -> { - if (it is UtSymbolicExecution && - (conflictTriggers.triggered(Conflict.ForceMockHappened) || - conflictTriggers.triggered(Conflict.ForceStaticMockHappened)) - ) { - it.containsMocking = true + runBlocking { + val controller = EngineController() + controller.job = launch { + super + .generateAsync(controller, method, mockStrategy, mockAlwaysDefaults, defaultTimeEstimator) + .collect { + when (it) { + is UtExecution -> { + if (it is UtSymbolicExecution && + (conflictTriggers.triggered(Conflict.ForceMockHappened) || + conflictTriggers.triggered(Conflict.ForceStaticMockHappened)) + ) { + it.containsMocking = true - conflictTriggers.reset( - Conflict.ForceMockHappened, - Conflict.ForceStaticMockHappened - ) - } - executions += it + conflictTriggers.reset( + Conflict.ForceMockHappened, + Conflict.ForceStaticMockHappened + ) } - is UtError -> errors.merge(it.description, 1, Int::plus) + executions += it } + is UtError -> errors.merge(it.description, 1, Int::plus) } - } + } } } From 8fdcacc077f872d00045caf1b56e44e7ceb79872 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 11:54:51 +0800 Subject: [PATCH 4/6] Add: common simplificator for expressions in the engine --- .../main/kotlin/org/utbot/engine/Memory.kt | 11 +- .../main/kotlin/org/utbot/engine/Resolver.kt | 2 +- .../main/kotlin/org/utbot/engine/Strings.kt | 7 +- .../main/kotlin/org/utbot/engine/Traverser.kt | 167 +++++++++++------- .../main/kotlin/org/utbot/engine/pc/Query.kt | 10 +- .../{RewritingVisitor.kt => Simplificator.kt} | 21 +-- .../kotlin/org/utbot/engine/pc/UtSolver.kt | 4 +- .../org/utbot/engine/pc/UtSolverStatus.kt | 6 +- .../MemoryUpdateSimplificator.kt | 163 +++++++++++++++++ .../simplificators/SimplificatorAdapter.kt | 18 ++ .../org/utbot/engine/simplificators/Util.kt | 68 +++++++ .../org/utbot/engine/types/TypeRegistry.kt | 6 +- 12 files changed, 382 insertions(+), 101 deletions(-) rename utbot-framework/src/main/kotlin/org/utbot/engine/pc/{RewritingVisitor.kt => Simplificator.kt} (98%) create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/SimplificatorAdapter.kt create mode 100644 utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/Util.kt diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt index 8ad3f24469..361b9c2373 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt @@ -3,7 +3,6 @@ package org.utbot.engine import org.utbot.engine.MemoryState.CURRENT import org.utbot.engine.MemoryState.INITIAL import org.utbot.engine.MemoryState.STATIC_INITIAL -import org.utbot.engine.pc.RewritingVisitor import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtAddrSort import org.utbot.engine.pc.UtArrayExpressionBase @@ -417,20 +416,20 @@ data class UtNamedStore( ) /** - * Create [UtNamedStore] with simplified [index] and [value] expressions. + * Create [UtNamedStore] with unsimplified [index] and [value] expressions. * - * @see RewritingVisitor + * @note simplifications occur explicitly in [Traverser] */ -fun simplifiedNamedStore( +fun namedStore( chunkDescriptor: MemoryChunkDescriptor, index: UtExpression, value: UtExpression -) = RewritingVisitor().let { visitor -> UtNamedStore(chunkDescriptor, index.accept(visitor), value.accept(visitor)) } +) = UtNamedStore(chunkDescriptor, index, value) /** * Updates persistent map where value = null in update means deletion of original key-value */ -private fun PersistentMap.update(update: Map): PersistentMap { +fun PersistentMap.update(update: Map): PersistentMap { if (update.isEmpty()) return this val deletions = mutableListOf() val updates = mutableMapOf() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt index c0551d7c11..d06c9c78be 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt @@ -1272,7 +1272,7 @@ private fun Traverser.arrayToMethodResult( } val memoryUpdate = MemoryUpdate( - stores = persistentListOf(simplifiedNamedStore(descriptor, newAddr, updatedArray)), + stores = persistentListOf(namedStore(descriptor, newAddr, updatedArray)), touchedChunkDescriptors = persistentSetOf(descriptor), ) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt index 06f953230a..0dbb5f348d 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt @@ -4,7 +4,6 @@ import com.github.curiousoddman.rgxgen.RgxGen import org.utbot.engine.overrides.strings.UtString import org.utbot.engine.overrides.strings.UtStringBuffer import org.utbot.engine.overrides.strings.UtStringBuilder -import org.utbot.engine.pc.RewritingVisitor import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtBoolExpression import org.utbot.engine.pc.UtFalse @@ -122,17 +121,17 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) { parameters: List ): List? { val arg = parameters[0] as ObjectValue - val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(RewritingVisitor()) + val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(this.simplificator) if (!matchingLengthExpr.isConcrete) return null val matchingValueExpr = - selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(RewritingVisitor()) + selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(this.simplificator) val matchingLength = matchingLengthExpr.toConcrete() as Int val matchingValue = CharArray(matchingLength) for (i in 0 until matchingLength) { - val charExpr = matchingValueExpr.select(mkInt(i)).accept(RewritingVisitor()) + val charExpr = matchingValueExpr.select(mkInt(i)).accept(this.simplificator) if (!charExpr.isConcrete) return null diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 1ba6abe60b..45640f1070 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -16,6 +16,7 @@ import org.utbot.engine.overrides.UtArrayMock import org.utbot.engine.overrides.UtLogicMock import org.utbot.engine.overrides.UtOverrideMock import org.utbot.engine.pc.NotBoolExpression +import org.utbot.engine.pc.Simplificator import org.utbot.engine.pc.UtAddNoOverflowExpression import org.utbot.engine.pc.UtAddrExpression import org.utbot.engine.pc.UtAndBoolExpression @@ -75,6 +76,7 @@ import org.utbot.engine.state.pop import org.utbot.engine.state.push import org.utbot.engine.state.update import org.utbot.engine.state.withLabel +import org.utbot.engine.symbolic.HardConstraint import org.utbot.engine.symbolic.emptyAssumption import org.utbot.engine.symbolic.emptyHardConstraint import org.utbot.engine.symbolic.emptySoftConstraint @@ -83,6 +85,9 @@ 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.simplificators.MemoryUpdateSimplificator +import org.utbot.engine.simplificators.simplifySymbolicStateUpdate +import org.utbot.engine.simplificators.simplifySymbolicValue import org.utbot.engine.types.ENUM_ORDINAL import org.utbot.engine.types.EQUALS_SIGNATURE import org.utbot.engine.types.HASHCODE_SIGNATURE @@ -309,6 +314,9 @@ class Traverser( return context.nextStates } + internal val simplificator = Simplificator() + private val memoryUpdateSimplificator = with(simplificator) { MemoryUpdateSimplificator() } + private fun TraversalContext.traverseStmt(current: Stmt) { if (doPreparatoryWorkIfRequired(current)) return @@ -322,10 +330,10 @@ class Traverser( is JReturnVoidStmt -> processResult(SymbolicSuccess(voidValue)) is JRetStmt -> error("This one should be already removed by Soot: $current") is JThrowStmt -> traverseThrowStmt(current) - is JBreakpointStmt -> offerState(environment.state.updateQueued(globalGraph.succ(current))) - is JGotoStmt -> offerState(environment.state.updateQueued(globalGraph.succ(current))) - is JNopStmt -> offerState(environment.state.updateQueued(globalGraph.succ(current))) - is MonitorStmt -> offerState(environment.state.updateQueued(globalGraph.succ(current))) + is JBreakpointStmt -> offerState(updateQueued(globalGraph.succ(current))) + is JGotoStmt -> offerState(updateQueued(globalGraph.succ(current))) + is JNopStmt -> offerState(updateQueued(globalGraph.succ(current))) + is MonitorStmt -> offerState(updateQueued(globalGraph.succ(current))) is DefinitionStmt -> TODO("$current") else -> error("Unsupported: ${current::class}") } @@ -445,7 +453,7 @@ class Traverser( // This branch could be useful if we have a static field, i.e. x = 5 / 0 is SymbolicFailure -> traverseException(stmt, result.symbolicResult) is SymbolicSuccess -> offerState( - environment.state.updateQueued( + updateQueued( environment.state.lastEdge!!, result.symbolicStateUpdate ) @@ -532,7 +540,7 @@ class Traverser( // $r0 = ; val edge = environment.state.lastEdge ?: globalGraph.succ(stmt) - val newState = environment.state.updateQueued(edge, updates) + val newState = updateQueued(edge, updates) offerState(newState) return true @@ -692,12 +700,12 @@ class Traverser( // mark the rest of the path leading to the '' statement as covered do { - environment.state = environment.state.updateQueued(globalGraph.succ(environment.state.stmt)) + environment.state = updateQueued(globalGraph.succ(environment.state.stmt)) globalGraph.visitEdge(environment.state.lastEdge!!) globalGraph.visitNode(environment.state) } while (!environment.state.stmt.isConstructorCall(currentExceptionJimpleLocal)) - offerState(environment.state.updateQueued(globalGraph.succ(environment.state.stmt))) + offerState(updateQueued(globalGraph.succ(environment.state.stmt))) } private fun TraversalContext.traverseAssignStmt(current: JAssignStmt) { @@ -730,9 +738,9 @@ class Traverser( is SymbolicFailure -> { //exception thrown if (environment.state.executionStack.last().doesntThrow) return@forEach - val nextState = environment.state.createExceptionState( + val nextState = createExceptionStateQueued( methodResult.symbolicResult, - queuedSymbolicStateUpdates + methodResult.symbolicStateUpdate + methodResult.symbolicStateUpdate ) globalGraph.registerImplicitEdge(nextState.lastEdge!!) offerState(nextState) @@ -744,7 +752,7 @@ class Traverser( methodResult.symbolicResult.value ) offerState( - environment.state.updateQueued( + updateQueued( globalGraph.succ(current), update + methodResult.symbolicStateUpdate ) @@ -991,7 +999,7 @@ class Traverser( environment.state.parameters += Parameter(localVariable, identityRef.type, value) - val nextState = environment.state.updateQueued( + val nextState = updateQueued( globalGraph.succ(current), SymbolicStateUpdate(localMemoryUpdates = localMemoryUpdate(localVariable to value)) ) @@ -1000,7 +1008,7 @@ class Traverser( is JCaughtExceptionRef -> { val value = localVariableMemory.local(CAUGHT_EXCEPTION) ?: error("Exception wasn't caught, stmt: $current, line: ${current.lines}") - val nextState = environment.state.updateQueued( + val nextState = updateQueued( globalGraph.succ(current), SymbolicStateUpdate(localMemoryUpdates = localMemoryUpdate(localVariable to value, CAUGHT_EXCEPTION to null)) ) @@ -1132,7 +1140,7 @@ class Traverser( if (!isAssumeExpr) { positiveCaseEdge?.let { edge -> environment.state.expectUndefined() - val positiveCaseState = environment.state.updateQueued( + val positiveCaseState = updateQueued( edge, SymbolicStateUpdate( hardConstraints = positiveCasePathConstraint.asHardConstraint(), @@ -1147,7 +1155,7 @@ class Traverser( val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else emptyHardConstraint() val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else emptyAssumption() - val negativeCaseState = environment.state.updateQueued( + val negativeCaseState = updateQueued( negativeCaseEdge, SymbolicStateUpdate( hardConstraints = hardConstraints, @@ -1177,11 +1185,11 @@ class Traverser( offerState( when (result.symbolicResult) { - is SymbolicFailure -> environment.state.createExceptionState( + is SymbolicFailure -> createExceptionStateQueued( result.symbolicResult, - queuedSymbolicStateUpdates + result.symbolicStateUpdate + result.symbolicStateUpdate ) - is SymbolicSuccess -> environment.state.updateQueued( + is SymbolicSuccess -> updateQueued( globalGraph.succ(current), result.symbolicStateUpdate ) @@ -1219,7 +1227,7 @@ class Traverser( successors.forEach { (target, expr) -> offerState( - environment.state.updateQueued( + updateQueued( target, SymbolicStateUpdate(hardConstraints = expr.asHardConstraint()), ) @@ -1468,7 +1476,7 @@ class Traverser( } queuedSymbolicStateUpdates += arrayUpdateWithValue(arrayValue.addr, CharType.v().arrayType, newArray) - environment.state = environment.state.update(queuedSymbolicStateUpdates) + environment.state = updateQueued(SymbolicStateUpdate()) queuedSymbolicStateUpdates = queuedSymbolicStateUpdates.copy(memoryUpdates = MemoryUpdate()) } @@ -1753,14 +1761,6 @@ class Traverser( } } - private fun SymbolicValue.simplify(): SymbolicValue = - when (this) { - is PrimitiveValue -> copy(expr = expr.accept(solver.rewriter)) - is ObjectValue -> copy(addr = addr.accept(solver.rewriter) as UtAddrExpression) - is ArrayValue -> copy(addr = addr.accept(solver.rewriter) as UtAddrExpression) - } - - // Type is needed for null values: we should know, which null do we require. // If valueType is NullType, return typelessNullObject. It can happen in a situation, // where we cannot find the type, for example in condition (null == null) @@ -1770,7 +1770,7 @@ class Traverser( ): SymbolicValue = when (value) { is JimpleLocal -> localVariableMemory.local(value.variable) ?: error("${value.name} not found in the locals") is Constant -> if (value is NullConstant) typeResolver.nullObject(valueType) else resolveConstant(value) - is Expr -> resolve(value, valueType).simplify() + is Expr -> resolve(value, valueType) is JInstanceFieldRef -> { val instance = (resolve(value.base) as ObjectValue) recordInstanceFieldRead(instance.addr, value.field) @@ -1836,6 +1836,8 @@ class Traverser( } is StaticFieldRef -> readStaticField(value) else -> error("${value::class} is not supported") + }.also { + with(simplificator) { simplifySymbolicValue(it) } } private fun readStaticField(fieldRef: StaticFieldRef): SymbolicValue { @@ -2153,7 +2155,7 @@ class Traverser( .select(array.addr) .store(index.expr, value) - return MemoryUpdate(persistentListOf(simplifiedNamedStore(descriptor, array.addr, updatedNestedArray))) + return MemoryUpdate(persistentListOf(namedStore(descriptor, array.addr, updatedNestedArray))) } fun objectUpdate( @@ -2163,7 +2165,7 @@ class Traverser( ): MemoryUpdate { val chunkId = hierarchy.chunkIdForField(instance.type, field) val descriptor = MemoryChunkDescriptor(chunkId, instance.type, field.type) - return MemoryUpdate(persistentListOf(simplifiedNamedStore(descriptor, instance.addr, value))) + return MemoryUpdate(persistentListOf(namedStore(descriptor, instance.addr, value))) } fun arrayUpdateWithValue( @@ -2176,7 +2178,7 @@ class Traverser( val chunkId = typeRegistry.arrayChunkId(type) val descriptor = MemoryChunkDescriptor(chunkId, type, type.elementType) - return MemoryUpdate(persistentListOf(simplifiedNamedStore(descriptor, addr, newValue))) + return MemoryUpdate(persistentListOf(namedStore(descriptor, addr, newValue))) } fun selectArrayExpressionFromMemory( @@ -2237,7 +2239,7 @@ class Traverser( val edge = findCatchBlock(current, classId) ?: return false offerState( - environment.state.updateQueued( + updateQueued( edge, SymbolicStateUpdate( hardConstraints = conditions.asHardConstraint(), @@ -2410,7 +2412,7 @@ class Traverser( instance: ObjectValue, methodSubSignature: String ): List { - val visitor = solver.rewriter.axiomInstantiationVisitor + val visitor = solver.simplificator.axiomInstantiationVisitor val simplifiedAddr = instance.addr.accept(visitor) // UtIsExpression for object with address the same as instance.addr val instanceOfConstraint = solver.assertions.singleOrNull { @@ -2684,7 +2686,7 @@ class Traverser( assumptions = assumptions.asAssumption() ) - val stateToContinue = environment.state.updateQueued( + val stateToContinue = updateQueued( globalGraph.succ(environment.state.stmt), symbolicStateUpdate ) @@ -2731,7 +2733,7 @@ class Traverser( ) } utOverrideMockDoesntThrowMethodName -> { - val stateToContinue = environment.state.updateQueued( + val stateToContinue = updateQueued( globalGraph.succ(environment.state.stmt), doesntThrow = true ) @@ -2743,7 +2745,7 @@ class Traverser( when (val param = parameters.single() as ReferenceValue) { is ObjectValue -> { val addr = param.addr.toIntValue() - val stateToContinue = environment.state.updateQueued( + val stateToContinue = updateQueued( globalGraph.succ(environment.state.stmt), SymbolicStateUpdate( hardConstraints = Le(addr, nullObjectAddr.toIntValue()).asHardConstraint() @@ -2762,7 +2764,7 @@ class Traverser( val update = MemoryUpdate( persistentListOf( - simplifiedNamedStore( + namedStore( descriptor, addr, UtArrayApplyForAll(memory.findArray(descriptor).select(addr)) { array, i -> @@ -2771,7 +2773,7 @@ class Traverser( ) ) ) - val stateToContinue = environment.state.updateQueued( + val stateToContinue = updateQueued( edge = globalGraph.succ(environment.state.stmt), SymbolicStateUpdate( hardConstraints = Le(addr.toIntValue(), nullObjectAddr.toIntValue()).asHardConstraint(), @@ -3023,25 +3025,10 @@ class Traverser( globalGraph.join(environment.state.stmt, graph, !isLibraryMethod) val parametersWithThis = listOfNotNull(caller) + callParameters offerState( - environment.state.push( - graph.head, - inputArguments = ArrayDeque(parametersWithThis), - queuedSymbolicStateUpdates + constraints.asHardConstraint(), - graph.body.method - ) + pushQueued(graph, parametersWithThis, constraints.asHardConstraint()) ) } - private fun ExecutionState.updateQueued( - edge: Edge, - update: SymbolicStateUpdate = SymbolicStateUpdate(), - doesntThrow: Boolean = false - ) = this.update( - edge, - queuedSymbolicStateUpdates + update, - doesntThrow - ) - private fun TraversalContext.resolveIfCondition(cond: BinopExpr): ResolvedCondition { // We add cond.op.type for null values only. If we have condition like "null == r1" // we'll have ObjectInstance(r1::type) and ObjectInstance(r1::type) for now @@ -3370,7 +3357,7 @@ class Traverser( // Expected in the parameters baseType is an RefType because it is either an RefType itself or an array of RefType values if (baseTypeAfterCast is RefType) { // Find parameterized type for the object if it is a parameter of the method under test and it has generic type - val newAddr = addr.accept(solver.rewriter) as UtAddrExpression + val newAddr = addr.accept(solver.simplificator) as UtAddrExpression val parameterizedType = when (newAddr.internal) { is UtArraySelectExpression -> parameterAddrToGenericType[findTheMostNestedAddr(newAddr.internal)] is UtBvConst -> parameterAddrToGenericType[newAddr] @@ -3420,11 +3407,9 @@ class Traverser( val symException = implicitThrown(exception, findNewAddr(), environment.state.isInNestedMethod()) if (!traverseCatchBlock(environment.state.stmt, symException, conditions)) { environment.state.expectUndefined() - val nextState = environment.state.createExceptionState( + val nextState = createExceptionStateQueued( symException, - queuedSymbolicStateUpdates - + conditions.asHardConstraint() - + softConditions.asSoftConstraint() + SymbolicStateUpdate(conditions.asHardConstraint(), softConditions.asSoftConstraint()) ) globalGraph.registerImplicitEdge(nextState.lastEdge!!) offerState(nextState) @@ -3564,7 +3549,7 @@ class Traverser( MemoryUpdate() // all memory updates are already added in [environment.state] } val methodResultWithUpdates = methodResult.copy(symbolicStateUpdate = queuedSymbolicStateUpdates + updates) - val stateToOffer = environment.state.pop(methodResultWithUpdates) + val stateToOffer = pop(methodResultWithUpdates) offerState(stateToOffer) logger.trace { "processResult<${environment.method.signature}> return from nested method" } @@ -3604,4 +3589,64 @@ class Traverser( queuedSymbolicStateUpdates = prevSymbolicStateUpdate } } + + private fun createExceptionStateQueued(exception: SymbolicFailure, update: SymbolicStateUpdate): ExecutionState { + val simplifiedUpdates = with (memoryUpdateSimplificator) { + simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update) + } + val simplifiedResult = with(simplificator) { + simplifySymbolicValue(exception.symbolic) + } + return environment.state.createExceptionState( + exception.copy(symbolic = simplifiedResult), + update = simplifiedUpdates + ) + } + + private fun updateQueued(update: SymbolicStateUpdate): ExecutionState { + val symbolicStateUpdate = with(memoryUpdateSimplificator) { + simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update) + } + + return environment.state.update( + symbolicStateUpdate, + ) + } + + private fun updateQueued( + edge: Edge, + update: SymbolicStateUpdate = SymbolicStateUpdate(), + doesntThrow: Boolean = false + ): ExecutionState { + val simplifiedUpdates = + with(memoryUpdateSimplificator) { + simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + update) + } + + return environment.state.update( + edge, + simplifiedUpdates, + doesntThrow + ) + } + + private fun pushQueued( + graph: ExceptionalUnitGraph, + parametersWithThis: List, + hardConstraint: HardConstraint + ): ExecutionState { + val simplifiedUpdates = with(memoryUpdateSimplificator) { + simplifySymbolicStateUpdate(queuedSymbolicStateUpdates + hardConstraint) + } + return environment.state.push( + graph.head, + inputArguments = ArrayDeque(parametersWithThis), + simplifiedUpdates, + graph.body.method + ) + } + + private fun pop(methodResultWithUpdates: MethodResult): ExecutionState { + return environment.state.pop(methodResultWithUpdates) + } } \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 50f529876a..419a0f8f67 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -82,7 +82,7 @@ class UnsatQuery(hard: PersistentSet) : BaseQuery( /** * Query of UtExpressions with applying simplifications if [useExpressionSimplification] is true. * - * @see RewritingVisitor + * @see Simplificator * * @param eqs - map that matches symbolic expressions with concrete values. * @param lts - map of upper bounds of integral symbolic expressions. @@ -99,10 +99,10 @@ data class Query( private val gts: PersistentMap = persistentHashMapOf() ) : BaseQuery(hard, soft, assumptions, status, lastAdded) { - val rewriter: RewritingVisitor - get() = RewritingVisitor(eqs, lts, gts) + val rewriter: Simplificator + get() = Simplificator(eqs, lts, gts) - private fun UtBoolExpression.simplify(visitor: RewritingVisitor): UtBoolExpression = + private fun UtBoolExpression.simplify(visitor: Simplificator): UtBoolExpression = this.accept(visitor) as UtBoolExpression private fun simplifyGeneric(expr: UtBoolExpression): UtBoolExpression = @@ -132,7 +132,7 @@ data class Query( eqs: Map = this@Query.eqs, lts: Map = this@Query.lts, gts: Map = this@Query.gts - ) = AxiomInstantiationRewritingVisitor(eqs, lts, gts).let { visitor -> + ) = AxiomInstantiationSimplificator(eqs, lts, gts).let { visitor -> this.map { it.simplify(visitor) } .map { simplifyGeneric(it) } .flatMap { splitAnd(it) } + visitor.instantiatedArrayAxioms diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Simplificator.kt similarity index 98% rename from utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt rename to utbot-framework/src/main/kotlin/org/utbot/engine/pc/Simplificator.kt index a94f15e6fd..0ce10c7021 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Simplificator.kt @@ -1,6 +1,5 @@ package org.utbot.engine.pc -import org.utbot.common.unreachableBranch import org.utbot.engine.Add import org.utbot.engine.And import org.utbot.engine.Cmp @@ -44,18 +43,16 @@ import soot.Type * UtExpressionVisitor that performs simple rewritings on expressions with concrete values. * */ -open class RewritingVisitor( +open class Simplificator( private val eqs: Map = emptyMap(), private val lts: Map = emptyMap(), private val gts: Map = emptyMap() ) : UtExpressionVisitor { - val axiomInstantiationVisitor: RewritingVisitor - get() = AxiomInstantiationRewritingVisitor(eqs, lts, gts) + val axiomInstantiationVisitor: Simplificator + get() = AxiomInstantiationSimplificator(eqs, lts, gts) protected val selectIndexStack = mutableListOf() private val simplificationCache = IdentityHashMap() - private fun allConcrete(vararg exprs: UtExpression) = exprs.all { it.isConcrete } - protected inline fun withNewSelect(index: UtExpression, block: () -> R): R { selectIndexStack += index.toIntValue() return block().also { @@ -103,12 +100,8 @@ open class RewritingVisitor( eqs[expr] ?: block().let { if (substituteResult) eqs[it] ?: it else it } } } - return if (expr.sort is UtArraySort && selectIndexStack.isNotEmpty()) { + return simplificationCache.getOrPut(expr) { checkSortsEquality(value, expr) - } else { - simplificationCache.getOrPut(expr) { - checkSortsEquality(value, expr) - } } } @@ -1041,15 +1034,15 @@ private fun instantiateArrayAsNewConst(arrayExpression: UtExtendedArrayExpressio } /** - * Visitor that applies the same simplifications as [RewritingVisitor] and instantiate axioms for extended array theory. + * Visitor that applies the same simplifications as [Simplificator] and instantiate axioms for extended array theory. * * @see UtExtendedArrayExpression */ -class AxiomInstantiationRewritingVisitor( +class AxiomInstantiationSimplificator( eqs: Map = emptyMap(), lts: Map = emptyMap(), gts: Map = emptyMap() -) : RewritingVisitor(eqs, lts, gts) { +) : Simplificator(eqs, lts, gts) { private val instantiatedAxiomExpressions = mutableListOf() /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index c6a7ca7c1f..a694c1661c 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -151,8 +151,8 @@ data class UtSolver constructor( //protection against solver reusage private var canBeCloned: Boolean = true - val rewriter: RewritingVisitor - get() = constraints.let { if (it is Query) it.rewriter else RewritingVisitor() } + val simplificator: Simplificator + get() = constraints.let { if (it is Query) it.rewriter else Simplificator() } /** * Returns the current status of the constraints. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt index 0df5e2b37c..1250023952 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt @@ -40,17 +40,13 @@ data class UtSolverStatusUNSAT(override val statusKind: UtSolverStatusKind) : Ut } class UtSolverStatusSAT( - private val translator: Z3TranslatorVisitor, + translator: Z3TranslatorVisitor, z3Solver: Solver ) : UtSolverStatus(SAT) { private val model = z3Solver.model private val evaluator: Z3EvaluatorVisitor = translator.evaluator(model) - //TODO put special markers inside expressionTranslationCache for detecting circular dependencies - fun translate(expression: UtExpression): Expr = - translator.translate(expression) - fun eval(expression: UtExpression): Expr = evaluator.eval(expression) fun concreteAddr(expression: UtAddrExpression): Address = eval(expression).intValue() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt new file mode 100644 index 0000000000..65294076c6 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt @@ -0,0 +1,163 @@ +package org.utbot.engine.simplificators + +import kotlinx.collections.immutable.PersistentList +import kotlinx.collections.immutable.PersistentMap +import kotlinx.collections.immutable.PersistentSet +import kotlinx.collections.immutable.mutate +import kotlinx.collections.immutable.toPersistentMap +import kotlinx.collections.immutable.toPersistentSet +import org.utbot.engine.Concrete +import org.utbot.engine.InstanceFieldReadOperation +import org.utbot.engine.MemoryChunkDescriptor +import org.utbot.engine.MemoryUpdate +import org.utbot.engine.MockInfoEnriched +import org.utbot.engine.ObjectValue +import org.utbot.engine.StaticFieldMemoryUpdateInfo +import org.utbot.engine.UtMockInfo +import org.utbot.engine.UtNamedStore +import org.utbot.engine.pc.Simplificator +import org.utbot.engine.pc.UtAddrExpression +import org.utbot.framework.plugin.api.ClassId +import org.utbot.framework.plugin.api.FieldId +import soot.ArrayType + +typealias StoresType = PersistentList +typealias TouchedChunkDescriptorsType = PersistentSet +typealias ConcreteType = PersistentMap +typealias MockInfosType = PersistentList +typealias StaticInstanceStorageType = PersistentMap +typealias InitializedStaticFieldsType = PersistentSet +typealias StaticFieldsUpdatesType = PersistentList +typealias MeaningfulStaticFieldsType = PersistentSet +typealias AddrToArrayTypeType = PersistentMap +typealias AddrToMockInfoType = PersistentMap +typealias VisitedValuesType = PersistentList +typealias TouchedAddressesType = PersistentList +typealias ClassIdToClearStaticsType = ClassId? +typealias InstanceFieldReadsType = PersistentSet +typealias SpeculativelyNotNullAddressesType = PersistentList +typealias SymbolicEnumValuesType = PersistentList + +context(Simplificator) +class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { + override fun simplifyImpl(expression: MemoryUpdate): MemoryUpdate { + val stores = simplifyStores(expression.stores) + val touchedChunkDescriptors = simplifyTocuhedChunkDescriptors(expression.touchedChunkDescriptors) + val concrete = simplifyConcrete(expression.concrete) + val mockInfos = simplifyMockInfos(expression.mockInfos) + val staticInstanceStorage = simplifyStaticInstanceStorage(expression.staticInstanceStorage) + val initializedStaticFields = simplifyInitializedStaticFields(expression.initializedStaticFields) + val staticFieldsUpdates = simplifyStaticFieldsUpdates(expression.staticFieldsUpdates) + val meaningfulStaticFields = simplifyMeaningfulStaticFields(expression.meaningfulStaticFields) + val addrToArrayType = simplifyAddrToArrayType(expression.addrToArrayType) + val addrToMockInfo = simplifyAddToMockInfo(expression.addrToMockInfo) + val visitedValues = simplifyVisitedValues(expression.visitedValues) + val touchedAddresses = simplifyTouchedAddresses(expression.touchedAddresses) + val classIdToClearStatics = simplifyClassIdToClearStatics(expression.classIdToClearStatics) + val instanceFieldReads = simplifyInstanceFieldReads(expression.instanceFieldReads) + val speculativelyNotNullAddresses = + simplifySpeculativelyNotNullAddresses(expression.speculativelyNotNullAddresses) + val symbolicEnumValues = simplifyEnumValues(expression.symbolicEnumValues) + return MemoryUpdate( + stores, + touchedChunkDescriptors, + concrete, + mockInfos, + staticInstanceStorage, + initializedStaticFields, + staticFieldsUpdates, + meaningfulStaticFields, + addrToArrayType, + addrToMockInfo, + visitedValues, + touchedAddresses, + classIdToClearStatics, + instanceFieldReads, + speculativelyNotNullAddresses, + symbolicEnumValues + ) + } + + private fun simplifyStores(stores: StoresType): StoresType = + stores + .mutate { prevStores -> + prevStores.replaceAll { store -> + store.copy( + index = store.index.accept(this@Simplificator), + value = store.value.accept(this@Simplificator) + ) + } + } + + private fun simplifyTocuhedChunkDescriptors(touchedChunkDescriptors: TouchedChunkDescriptorsType): TouchedChunkDescriptorsType = + touchedChunkDescriptors + + private fun simplifyConcrete(concrete: ConcreteType): ConcreteType = + concrete + .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .toPersistentMap() + + private fun simplifyMockInfos(mockInfos: MockInfosType): MockInfosType = + mockInfos.mutate { prevMockInfos -> + prevMockInfos.replaceAll { + simplifyMockInfoEnriched(it) + } + } + + + private fun simplifyStaticInstanceStorage(staticInstanceStorage: StaticInstanceStorageType): StaticInstanceStorageType = + staticInstanceStorage.mutate { prevStorage -> + prevStorage.replaceAll { _, v -> simplifySymbolicValue(v) as ObjectValue } + } + + private fun simplifyInitializedStaticFields(initializedStaticFields: InitializedStaticFieldsType): InitializedStaticFieldsType = + initializedStaticFields + + private fun simplifyStaticFieldsUpdates(staticFieldsUpdates: StaticFieldsUpdatesType): StaticFieldsUpdatesType = + staticFieldsUpdates.mutate { prevUpdates -> + prevUpdates.replaceAll { staticFieldMemoryUpdateInfo(it) } + } + + private fun simplifyMeaningfulStaticFields(meaningfulStaticFields: MeaningfulStaticFieldsType): MeaningfulStaticFieldsType = + meaningfulStaticFields + + + private fun simplifyAddrToArrayType(addrToArrayType: AddrToArrayTypeType): AddrToArrayTypeType = + addrToArrayType + .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .toPersistentMap() + + + private fun simplifyAddToMockInfo(addrToMockInfo: AddrToMockInfoType): AddrToMockInfoType = + addrToMockInfo + .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .toPersistentMap() + + private fun simplifyVisitedValues(visitedValues: VisitedValuesType): VisitedValuesType = + visitedValues.mutate { prevValues -> + prevValues.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + } + + private fun simplifyTouchedAddresses(touchedAddresses: TouchedAddressesType): TouchedAddressesType = + touchedAddresses.mutate { prevAddresses -> + prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + } + + private fun simplifyClassIdToClearStatics(classIdToClearStatics: ClassIdToClearStaticsType): ClassIdToClearStaticsType = + classIdToClearStatics + + private fun simplifyInstanceFieldReads(instanceFieldReads: InstanceFieldReadsType): InstanceFieldReadsType = + instanceFieldReads + .map { it.copy(addr = it.addr.accept(this@Simplificator) as UtAddrExpression) } + .toPersistentSet() + + private fun simplifySpeculativelyNotNullAddresses(speculativelyNotNullAddresses: SpeculativelyNotNullAddressesType): SpeculativelyNotNullAddressesType = + speculativelyNotNullAddresses.mutate { prevAddresses -> + prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + } + + private fun simplifyEnumValues(symbolicEnumValues: SymbolicEnumValuesType): SymbolicEnumValuesType = + symbolicEnumValues.mutate { values -> + values.replaceAll { simplifySymbolicValue(it) as ObjectValue } + } +} diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/SimplificatorAdapter.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/SimplificatorAdapter.kt new file mode 100644 index 0000000000..5faf5b5b32 --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/SimplificatorAdapter.kt @@ -0,0 +1,18 @@ +package org.utbot.engine.simplificators + +import java.util.IdentityHashMap + + +interface SimplificatorAdapter { + fun simplify(expression: T): T +} + +abstract class CachingSimplificatorAdapter : SimplificatorAdapter { + private val cache: IdentityHashMap = IdentityHashMap() + + final override fun simplify(expression: T): T = + cache.getOrPut(expression) { simplifyImpl(expression) } + + protected abstract fun simplifyImpl(expression: T): T +} + diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/Util.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/Util.kt new file mode 100644 index 0000000000..8403bc3c8b --- /dev/null +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/Util.kt @@ -0,0 +1,68 @@ +package org.utbot.engine.simplificators + +import org.utbot.engine.ArrayValue +import org.utbot.engine.MockInfoEnriched +import org.utbot.engine.ObjectValue +import org.utbot.engine.PrimitiveValue +import org.utbot.engine.StaticFieldMemoryUpdateInfo +import org.utbot.engine.SymbolicValue +import org.utbot.engine.UtFieldMockInfo +import org.utbot.engine.UtMockInfo +import org.utbot.engine.UtNewInstanceMockInfo +import org.utbot.engine.UtObjectMockInfo +import org.utbot.engine.UtStaticMethodMockInfo +import org.utbot.engine.UtStaticObjectMockInfo +import org.utbot.engine.pc.Simplificator +import org.utbot.engine.pc.UtAddrExpression +import org.utbot.engine.symbolic.SymbolicStateUpdate + +context(Simplificator) +fun staticFieldMemoryUpdateInfo(staticFieldMemoryUpdateInfo: StaticFieldMemoryUpdateInfo) = + with(staticFieldMemoryUpdateInfo) { + copy(value = simplifySymbolicValue(value)) + } + +context(Simplificator) +fun simplifyMockInfoEnriched(mockInfoEnriched: MockInfoEnriched): MockInfoEnriched { + val mockInfo: UtMockInfo = simplifyUtMockInfo(mockInfoEnriched.mockInfo) + val executables = mockInfoEnriched.executables.mapValues { (_, mockExecutableInstances) -> + mockExecutableInstances.map { mockExecutableInstance -> + with(mockExecutableInstance) { + val symbolicValue = simplifySymbolicValue(value) + copy(value = symbolicValue) + } + } + } + + return MockInfoEnriched(mockInfo, executables) +} + +context(Simplificator) +fun simplifyUtMockInfo(mockInfo: UtMockInfo): UtMockInfo = + with(mockInfo) { + when (this) { + is UtFieldMockInfo -> copy(ownerAddr = ownerAddr?.accept(this@Simplificator) as UtAddrExpression?) + is UtNewInstanceMockInfo -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + is UtObjectMockInfo -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + is UtStaticMethodMockInfo -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + is UtStaticObjectMockInfo -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + } + } + +context(Simplificator) +fun simplifySymbolicValue(value: SymbolicValue): SymbolicValue = + with(value) { + when (this) { + is PrimitiveValue -> copy(expr = expr.accept(this@Simplificator)) + is ArrayValue -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + is ObjectValue -> copy(addr = addr.accept(this@Simplificator) as UtAddrExpression) + } + } + + +context(MemoryUpdateSimplificator) +fun simplifySymbolicStateUpdate(update: SymbolicStateUpdate) = + with(update) { + val memoryUpdates = simplify(memoryUpdates) + copy(memoryUpdates = memoryUpdates) + } \ No newline at end of file diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt index 568cb45f77..4a8c422fcf 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/types/TypeRegistry.kt @@ -45,7 +45,7 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store -import org.utbot.engine.simplifiedNamedStore +import org.utbot.engine.namedStore import org.utbot.engine.symbolic.asHardConstraint import org.utbot.engine.toIntValue import org.utbot.engine.toPrimitiveValue @@ -337,8 +337,8 @@ class TypeRegistry { val symNumDimensions = mkInt(numDimensions) val stores = persistentListOf( - simplifiedNamedStore(CLASS_REF_TYPE_DESCRIPTOR, addr, typeId), - simplifiedNamedStore(CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR, addr, symNumDimensions) + namedStore(CLASS_REF_TYPE_DESCRIPTOR, addr, typeId), + namedStore(CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR, addr, symNumDimensions) ) val touchedDescriptors = persistentSetOf(CLASS_REF_TYPE_DESCRIPTOR, CLASS_REF_NUM_DIMENSIONS_DESCRIPTOR) From 482a79924fa87463a05c4e4674715178df6dda12 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 14:46:50 +0800 Subject: [PATCH 5/6] Remove: useless context constructor --- .../main/kotlin/org/utbot/engine/Traverser.kt | 2 +- .../MemoryUpdateSimplificator.kt | 33 ++++++++++--------- 2 files changed, 19 insertions(+), 16 deletions(-) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 45640f1070..d51af92ab4 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -315,7 +315,7 @@ class Traverser( } internal val simplificator = Simplificator() - private val memoryUpdateSimplificator = with(simplificator) { MemoryUpdateSimplificator() } + private val memoryUpdateSimplificator = MemoryUpdateSimplificator(simplificator) private fun TraversalContext.traverseStmt(current: Stmt) { if (doPreparatoryWorkIfRequired(current)) return diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt index 65294076c6..dd45f7687d 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt @@ -38,8 +38,9 @@ typealias InstanceFieldReadsType = PersistentSet typealias SpeculativelyNotNullAddressesType = PersistentList typealias SymbolicEnumValuesType = PersistentList -context(Simplificator) -class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { +class MemoryUpdateSimplificator( + private val simplificator: Simplificator +) : CachingSimplificatorAdapter() { override fun simplifyImpl(expression: MemoryUpdate): MemoryUpdate { val stores = simplifyStores(expression.stores) val touchedChunkDescriptors = simplifyTocuhedChunkDescriptors(expression.touchedChunkDescriptors) @@ -83,8 +84,8 @@ class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { .mutate { prevStores -> prevStores.replaceAll { store -> store.copy( - index = store.index.accept(this@Simplificator), - value = store.value.accept(this@Simplificator) + index = store.index.accept(simplificator), + value = store.value.accept(simplificator) ) } } @@ -94,20 +95,22 @@ class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { private fun simplifyConcrete(concrete: ConcreteType): ConcreteType = concrete - .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .mapKeys { (k, _) -> k.accept(simplificator) as UtAddrExpression } .toPersistentMap() private fun simplifyMockInfos(mockInfos: MockInfosType): MockInfosType = mockInfos.mutate { prevMockInfos -> prevMockInfos.replaceAll { - simplifyMockInfoEnriched(it) + with(simplificator) { + simplifyMockInfoEnriched(it) + } } } private fun simplifyStaticInstanceStorage(staticInstanceStorage: StaticInstanceStorageType): StaticInstanceStorageType = staticInstanceStorage.mutate { prevStorage -> - prevStorage.replaceAll { _, v -> simplifySymbolicValue(v) as ObjectValue } + prevStorage.replaceAll { _, v -> with(simplificator) { simplifySymbolicValue(v) as ObjectValue } } } private fun simplifyInitializedStaticFields(initializedStaticFields: InitializedStaticFieldsType): InitializedStaticFieldsType = @@ -115,7 +118,7 @@ class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { private fun simplifyStaticFieldsUpdates(staticFieldsUpdates: StaticFieldsUpdatesType): StaticFieldsUpdatesType = staticFieldsUpdates.mutate { prevUpdates -> - prevUpdates.replaceAll { staticFieldMemoryUpdateInfo(it) } + prevUpdates.replaceAll { with(simplificator) { staticFieldMemoryUpdateInfo(it) } } } private fun simplifyMeaningfulStaticFields(meaningfulStaticFields: MeaningfulStaticFieldsType): MeaningfulStaticFieldsType = @@ -124,23 +127,23 @@ class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { private fun simplifyAddrToArrayType(addrToArrayType: AddrToArrayTypeType): AddrToArrayTypeType = addrToArrayType - .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .mapKeys { (k, _) -> k.accept(simplificator) as UtAddrExpression } .toPersistentMap() private fun simplifyAddToMockInfo(addrToMockInfo: AddrToMockInfoType): AddrToMockInfoType = addrToMockInfo - .mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression } + .mapKeys { (k, _) -> k.accept(simplificator) as UtAddrExpression } .toPersistentMap() private fun simplifyVisitedValues(visitedValues: VisitedValuesType): VisitedValuesType = visitedValues.mutate { prevValues -> - prevValues.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + prevValues.replaceAll { it.accept(simplificator) as UtAddrExpression } } private fun simplifyTouchedAddresses(touchedAddresses: TouchedAddressesType): TouchedAddressesType = touchedAddresses.mutate { prevAddresses -> - prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + prevAddresses.replaceAll { it.accept(simplificator) as UtAddrExpression } } private fun simplifyClassIdToClearStatics(classIdToClearStatics: ClassIdToClearStaticsType): ClassIdToClearStaticsType = @@ -148,16 +151,16 @@ class MemoryUpdateSimplificator : CachingSimplificatorAdapter() { private fun simplifyInstanceFieldReads(instanceFieldReads: InstanceFieldReadsType): InstanceFieldReadsType = instanceFieldReads - .map { it.copy(addr = it.addr.accept(this@Simplificator) as UtAddrExpression) } + .map { it.copy(addr = it.addr.accept(simplificator) as UtAddrExpression) } .toPersistentSet() private fun simplifySpeculativelyNotNullAddresses(speculativelyNotNullAddresses: SpeculativelyNotNullAddressesType): SpeculativelyNotNullAddressesType = speculativelyNotNullAddresses.mutate { prevAddresses -> - prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression } + prevAddresses.replaceAll { it.accept(simplificator) as UtAddrExpression } } private fun simplifyEnumValues(symbolicEnumValues: SymbolicEnumValuesType): SymbolicEnumValuesType = symbolicEnumValues.mutate { values -> - values.replaceAll { simplifySymbolicValue(it) as ObjectValue } + values.replaceAll { with(simplificator) { simplifySymbolicValue(it) as ObjectValue } } } } From 3c85ca46bd34ce3943842633735e0c5f1d3eb4d4 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Wed, 2 Nov 2022 17:09:27 +0800 Subject: [PATCH 6/6] Fix: review comments --- .../main/kotlin/org/utbot/engine/pc/Query.kt | 2 +- .../kotlin/org/utbot/engine/pc/UtSolver.kt | 2 +- .../MemoryUpdateSimplificator.kt | 38 +++++++++---------- .../engine/state/ExecutionStackElement.kt | 10 +---- 4 files changed, 23 insertions(+), 29 deletions(-) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 419a0f8f67..0b7b579360 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -99,7 +99,7 @@ data class Query( private val gts: PersistentMap = persistentHashMapOf() ) : BaseQuery(hard, soft, assumptions, status, lastAdded) { - val rewriter: Simplificator + val simplificator: Simplificator get() = Simplificator(eqs, lts, gts) private fun UtBoolExpression.simplify(visitor: Simplificator): UtBoolExpression = diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index a694c1661c..1297636146 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -152,7 +152,7 @@ data class UtSolver constructor( private var canBeCloned: Boolean = true val simplificator: Simplificator - get() = constraints.let { if (it is Query) it.rewriter else Simplificator() } + get() = constraints.let { if (it is Query) it.simplificator else Simplificator() } /** * Returns the current status of the constraints. diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt index dd45f7687d..eb1520ccaa 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt @@ -41,24 +41,24 @@ typealias SymbolicEnumValuesType = PersistentList class MemoryUpdateSimplificator( private val simplificator: Simplificator ) : CachingSimplificatorAdapter() { - override fun simplifyImpl(expression: MemoryUpdate): MemoryUpdate { - val stores = simplifyStores(expression.stores) - val touchedChunkDescriptors = simplifyTocuhedChunkDescriptors(expression.touchedChunkDescriptors) - val concrete = simplifyConcrete(expression.concrete) - val mockInfos = simplifyMockInfos(expression.mockInfos) - val staticInstanceStorage = simplifyStaticInstanceStorage(expression.staticInstanceStorage) - val initializedStaticFields = simplifyInitializedStaticFields(expression.initializedStaticFields) - val staticFieldsUpdates = simplifyStaticFieldsUpdates(expression.staticFieldsUpdates) - val meaningfulStaticFields = simplifyMeaningfulStaticFields(expression.meaningfulStaticFields) - val addrToArrayType = simplifyAddrToArrayType(expression.addrToArrayType) - val addrToMockInfo = simplifyAddToMockInfo(expression.addrToMockInfo) - val visitedValues = simplifyVisitedValues(expression.visitedValues) - val touchedAddresses = simplifyTouchedAddresses(expression.touchedAddresses) - val classIdToClearStatics = simplifyClassIdToClearStatics(expression.classIdToClearStatics) - val instanceFieldReads = simplifyInstanceFieldReads(expression.instanceFieldReads) + override fun simplifyImpl(expression: MemoryUpdate): MemoryUpdate = with(expression) { + val stores = simplifyStores(stores) + val touchedChunkDescriptors = simplifyTouchedChunkDescriptors(touchedChunkDescriptors) + val concrete = simplifyConcrete(concrete) + val mockInfos = simplifyMockInfos(mockInfos) + val staticInstanceStorage = simplifyStaticInstanceStorage(staticInstanceStorage) + val initializedStaticFields = simplifyInitializedStaticFields(initializedStaticFields) + val staticFieldsUpdates = simplifyStaticFieldsUpdates(staticFieldsUpdates) + val meaningfulStaticFields = simplifyMeaningfulStaticFields(meaningfulStaticFields) + val addrToArrayType = simplifyAddrToArrayType(addrToArrayType) + val addrToMockInfo = simplifyAddrToMockInfo(addrToMockInfo) + val visitedValues = simplifyVisitedValues(visitedValues) + val touchedAddresses = simplifyTouchedAddresses(touchedAddresses) + val classIdToClearStatics = simplifyClassIdToClearStatics(classIdToClearStatics) + val instanceFieldReads = simplifyInstanceFieldReads(instanceFieldReads) val speculativelyNotNullAddresses = - simplifySpeculativelyNotNullAddresses(expression.speculativelyNotNullAddresses) - val symbolicEnumValues = simplifyEnumValues(expression.symbolicEnumValues) + simplifySpeculativelyNotNullAddresses(speculativelyNotNullAddresses) + val symbolicEnumValues = simplifyEnumValues(symbolicEnumValues) return MemoryUpdate( stores, touchedChunkDescriptors, @@ -90,7 +90,7 @@ class MemoryUpdateSimplificator( } } - private fun simplifyTocuhedChunkDescriptors(touchedChunkDescriptors: TouchedChunkDescriptorsType): TouchedChunkDescriptorsType = + private fun simplifyTouchedChunkDescriptors(touchedChunkDescriptors: TouchedChunkDescriptorsType): TouchedChunkDescriptorsType = touchedChunkDescriptors private fun simplifyConcrete(concrete: ConcreteType): ConcreteType = @@ -131,7 +131,7 @@ class MemoryUpdateSimplificator( .toPersistentMap() - private fun simplifyAddToMockInfo(addrToMockInfo: AddrToMockInfoType): AddrToMockInfoType = + private fun simplifyAddrToMockInfo(addrToMockInfo: AddrToMockInfoType): AddrToMockInfoType = addrToMockInfo .mapKeys { (k, _) -> k.accept(simplificator) as UtAddrExpression } .toPersistentMap() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt index da70be840d..378da0f7f0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/state/ExecutionStackElement.kt @@ -6,7 +6,6 @@ import org.utbot.engine.LocalMemoryUpdate import org.utbot.engine.LocalVariable import org.utbot.engine.Parameter import org.utbot.engine.SymbolicValue -//import org.utbot.engine.symbolic.simplificators.LocalMemoryUpdateSimplificator import org.utbot.engine.update import soot.SootMethod import soot.jimple.Stmt @@ -32,7 +31,7 @@ data class ExecutionStackElement( /** * Represents a memory associated with a certain method call. For now consists only of local variables mapping. - * TODO: think on other fields later + * TODO: think on other fields later: [#339](https://github.com/UnitTestBot/UTBotJava/issues/339) [#340](https://github.com/UnitTestBot/UTBotJava/issues/340) * * @param [locals] represents a mapping from [LocalVariable]s of a specific method call to [SymbolicValue]s. */ @@ -50,9 +49,4 @@ data class LocalVariableMemory( val localValues: Set get() = locals.values.toSet() -} -// -//context(LocalMemoryUpdateSimplificator) -//fun updateSimplified(localVariableMemory: LocalVariableMemory, update: LocalMemoryUpdate): LocalVariableMemory { -// return localVariableMemory.update(simplify(update)) -//} \ No newline at end of file +} \ No newline at end of file