Skip to content

Commit 8fdcacc

Browse files
sergeypospelovsergeypospelov
committed
Add: common simplificator for expressions in the engine
1 parent 57f18d7 commit 8fdcacc

File tree

12 files changed

+382
-101
lines changed

12 files changed

+382
-101
lines changed

‎utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ package org.utbot.engine
33
import org.utbot.engine.MemoryState.CURRENT
44
import org.utbot.engine.MemoryState.INITIAL
55
import org.utbot.engine.MemoryState.STATIC_INITIAL
6-
import org.utbot.engine.pc.RewritingVisitor
76
import org.utbot.engine.pc.UtAddrExpression
87
import org.utbot.engine.pc.UtAddrSort
98
import org.utbot.engine.pc.UtArrayExpressionBase
@@ -417,20 +416,20 @@ data class UtNamedStore(
417416
)
418417

419418
/**
420-
* Create [UtNamedStore] with simplified [index] and [value] expressions.
419+
* Create [UtNamedStore] with unsimplified [index] and [value] expressions.
421420
*
422-
* @see RewritingVisitor
421+
* @note simplifications occur explicitly in [Traverser]
423422
*/
424-
fun simplifiedNamedStore(
423+
fun namedStore(
425424
chunkDescriptor: MemoryChunkDescriptor,
426425
index: UtExpression,
427426
value: UtExpression
428-
) = RewritingVisitor().let { visitor -> UtNamedStore(chunkDescriptor, index.accept(visitor), value.accept(visitor)) }
427+
) = UtNamedStore(chunkDescriptor, index, value)
429428

430429
/**
431430
* Updates persistent map where value = null in update means deletion of original key-value
432431
*/
433-
private fun <K, V> PersistentMap<K, V>.update(update: Map<K, V?>): PersistentMap<K, V> {
432+
fun <K, V> PersistentMap<K, V>.update(update: Map<K, V?>): PersistentMap<K, V> {
434433
if (update.isEmpty()) return this
435434
val deletions = mutableListOf<K>()
436435
val updates = mutableMapOf<K, V>()

‎utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1272,7 +1272,7 @@ private fun Traverser.arrayToMethodResult(
12721272
}
12731273

12741274
val memoryUpdate = MemoryUpdate(
1275-
stores = persistentListOf(simplifiedNamedStore(descriptor, newAddr, updatedArray)),
1275+
stores = persistentListOf(namedStore(descriptor, newAddr, updatedArray)),
12761276
touchedChunkDescriptors = persistentSetOf(descriptor),
12771277
)
12781278

‎utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ import com.github.curiousoddman.rgxgen.RgxGen
44
import org.utbot.engine.overrides.strings.UtString
55
import org.utbot.engine.overrides.strings.UtStringBuffer
66
import org.utbot.engine.overrides.strings.UtStringBuilder
7-
import org.utbot.engine.pc.RewritingVisitor
87
import org.utbot.engine.pc.UtAddrExpression
98
import org.utbot.engine.pc.UtBoolExpression
109
import org.utbot.engine.pc.UtFalse
@@ -122,17 +121,17 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) {
122121
parameters: List<SymbolicValue>
123122
): List<InvokeResult>? {
124123
val arg = parameters[0] as ObjectValue
125-
val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(RewritingVisitor())
124+
val matchingLengthExpr = getIntFieldValue(arg, STRING_LENGTH).accept(this.simplificator)
126125

127126
if (!matchingLengthExpr.isConcrete) return null
128127

129128
val matchingValueExpr =
130-
selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(RewritingVisitor())
129+
selectArrayExpressionFromMemory(getValueArray(arg.addr)).accept(this.simplificator)
131130
val matchingLength = matchingLengthExpr.toConcrete() as Int
132131
val matchingValue = CharArray(matchingLength)
133132

134133
for (i in 0 until matchingLength) {
135-
val charExpr = matchingValueExpr.select(mkInt(i)).accept(RewritingVisitor())
134+
val charExpr = matchingValueExpr.select(mkInt(i)).accept(this.simplificator)
136135

137136
if (!charExpr.isConcrete) return null
138137

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

Lines changed: 106 additions & 61 deletions
Large diffs are not rendered by default.

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ class UnsatQuery(hard: PersistentSet<UtBoolExpression>) : BaseQuery(
8282
/**
8383
* Query of UtExpressions with applying simplifications if [useExpressionSimplification] is true.
8484
*
85-
* @see RewritingVisitor
85+
* @see Simplificator
8686
*
8787
* @param eqs - map that matches symbolic expressions with concrete values.
8888
* @param lts - map of upper bounds of integral symbolic expressions.
@@ -99,10 +99,10 @@ data class Query(
9999
private val gts: PersistentMap<UtExpression, Long> = persistentHashMapOf()
100100
) : BaseQuery(hard, soft, assumptions, status, lastAdded) {
101101

102-
val rewriter: RewritingVisitor
103-
get() = RewritingVisitor(eqs, lts, gts)
102+
val rewriter: Simplificator
103+
get() = Simplificator(eqs, lts, gts)
104104

105-
private fun UtBoolExpression.simplify(visitor: RewritingVisitor): UtBoolExpression =
105+
private fun UtBoolExpression.simplify(visitor: Simplificator): UtBoolExpression =
106106
this.accept(visitor) as UtBoolExpression
107107

108108
private fun simplifyGeneric(expr: UtBoolExpression): UtBoolExpression =
@@ -132,7 +132,7 @@ data class Query(
132132
eqs: Map<UtExpression, UtExpression> = this@Query.eqs,
133133
lts: Map<UtExpression, Long> = this@Query.lts,
134134
gts: Map<UtExpression, Long> = this@Query.gts
135-
) = AxiomInstantiationRewritingVisitor(eqs, lts, gts).let { visitor ->
135+
) = AxiomInstantiationSimplificator(eqs, lts, gts).let { visitor ->
136136
this.map { it.simplify(visitor) }
137137
.map { simplifyGeneric(it) }
138138
.flatMap { splitAnd(it) } + visitor.instantiatedArrayAxioms

‎utbot-framework/src/main/kotlin/org/utbot/engine/pc/RewritingVisitor.kt renamed to ‎utbot-framework/src/main/kotlin/org/utbot/engine/pc/Simplificator.kt

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
package org.utbot.engine.pc
22

3-
import org.utbot.common.unreachableBranch
43
import org.utbot.engine.Add
54
import org.utbot.engine.And
65
import org.utbot.engine.Cmp
@@ -44,18 +43,16 @@ import soot.Type
4443
* UtExpressionVisitor that performs simple rewritings on expressions with concrete values.
4544
*
4645
*/
47-
open class RewritingVisitor(
46+
open class Simplificator(
4847
private val eqs: Map<UtExpression, UtExpression> = emptyMap(),
4948
private val lts: Map<UtExpression, Long> = emptyMap(),
5049
private val gts: Map<UtExpression, Long> = emptyMap()
5150
) : UtExpressionVisitor<UtExpression> {
52-
val axiomInstantiationVisitor: RewritingVisitor
53-
get() = AxiomInstantiationRewritingVisitor(eqs, lts, gts)
51+
val axiomInstantiationVisitor: Simplificator
52+
get() = AxiomInstantiationSimplificator(eqs, lts, gts)
5453
protected val selectIndexStack = mutableListOf<PrimitiveValue>()
5554
private val simplificationCache = IdentityHashMap<UtExpression, UtExpression>()
5655

57-
private fun allConcrete(vararg exprs: UtExpression) = exprs.all { it.isConcrete }
58-
5956
protected inline fun <reified R> withNewSelect(index: UtExpression, block: () -> R): R {
6057
selectIndexStack += index.toIntValue()
6158
return block().also {
@@ -103,12 +100,8 @@ open class RewritingVisitor(
103100
eqs[expr] ?: block().let { if (substituteResult) eqs[it] ?: it else it }
104101
}
105102
}
106-
return if (expr.sort is UtArraySort && selectIndexStack.isNotEmpty()) {
103+
return simplificationCache.getOrPut(expr) {
107104
checkSortsEquality(value, expr)
108-
} else {
109-
simplificationCache.getOrPut(expr) {
110-
checkSortsEquality(value, expr)
111-
}
112105
}
113106
}
114107

@@ -1041,15 +1034,15 @@ private fun instantiateArrayAsNewConst(arrayExpression: UtExtendedArrayExpressio
10411034
}
10421035

10431036
/**
1044-
* Visitor that applies the same simplifications as [RewritingVisitor] and instantiate axioms for extended array theory.
1037+
* Visitor that applies the same simplifications as [Simplificator] and instantiate axioms for extended array theory.
10451038
*
10461039
* @see UtExtendedArrayExpression
10471040
*/
1048-
class AxiomInstantiationRewritingVisitor(
1041+
class AxiomInstantiationSimplificator(
10491042
eqs: Map<UtExpression, UtExpression> = emptyMap(),
10501043
lts: Map<UtExpression, Long> = emptyMap(),
10511044
gts: Map<UtExpression, Long> = emptyMap()
1052-
) : RewritingVisitor(eqs, lts, gts) {
1045+
) : Simplificator(eqs, lts, gts) {
10531046
private val instantiatedAxiomExpressions = mutableListOf<UtBoolExpression>()
10541047

10551048
/**

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -151,8 +151,8 @@ data class UtSolver constructor(
151151
//protection against solver reusage
152152
private var canBeCloned: Boolean = true
153153

154-
val rewriter: RewritingVisitor
155-
get() = constraints.let { if (it is Query) it.rewriter else RewritingVisitor() }
154+
val simplificator: Simplificator
155+
get() = constraints.let { if (it is Query) it.rewriter else Simplificator() }
156156

157157
/**
158158
* Returns the current status of the constraints.

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

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,17 +40,13 @@ data class UtSolverStatusUNSAT(override val statusKind: UtSolverStatusKind) : Ut
4040
}
4141

4242
class UtSolverStatusSAT(
43-
private val translator: Z3TranslatorVisitor,
43+
translator: Z3TranslatorVisitor,
4444
z3Solver: Solver
4545
) : UtSolverStatus(SAT) {
4646
private val model = z3Solver.model
4747

4848
private val evaluator: Z3EvaluatorVisitor = translator.evaluator(model)
4949

50-
//TODO put special markers inside expressionTranslationCache for detecting circular dependencies
51-
fun translate(expression: UtExpression): Expr =
52-
translator.translate(expression)
53-
5450
fun eval(expression: UtExpression): Expr = evaluator.eval(expression)
5551

5652
fun concreteAddr(expression: UtAddrExpression): Address = eval(expression).intValue()

‎utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/MemoryUpdateSimplificator.kt

Lines changed: 163 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
package org.utbot.engine.simplificators
2+
3+
import kotlinx.collections.immutable.PersistentList
4+
import kotlinx.collections.immutable.PersistentMap
5+
import kotlinx.collections.immutable.PersistentSet
6+
import kotlinx.collections.immutable.mutate
7+
import kotlinx.collections.immutable.toPersistentMap
8+
import kotlinx.collections.immutable.toPersistentSet
9+
import org.utbot.engine.Concrete
10+
import org.utbot.engine.InstanceFieldReadOperation
11+
import org.utbot.engine.MemoryChunkDescriptor
12+
import org.utbot.engine.MemoryUpdate
13+
import org.utbot.engine.MockInfoEnriched
14+
import org.utbot.engine.ObjectValue
15+
import org.utbot.engine.StaticFieldMemoryUpdateInfo
16+
import org.utbot.engine.UtMockInfo
17+
import org.utbot.engine.UtNamedStore
18+
import org.utbot.engine.pc.Simplificator
19+
import org.utbot.engine.pc.UtAddrExpression
20+
import org.utbot.framework.plugin.api.ClassId
21+
import org.utbot.framework.plugin.api.FieldId
22+
import soot.ArrayType
23+
24+
typealias StoresType = PersistentList<UtNamedStore>
25+
typealias TouchedChunkDescriptorsType = PersistentSet<MemoryChunkDescriptor>
26+
typealias ConcreteType = PersistentMap<UtAddrExpression, Concrete>
27+
typealias MockInfosType = PersistentList<MockInfoEnriched>
28+
typealias StaticInstanceStorageType = PersistentMap<ClassId, ObjectValue>
29+
typealias InitializedStaticFieldsType = PersistentSet<FieldId>
30+
typealias StaticFieldsUpdatesType = PersistentList<StaticFieldMemoryUpdateInfo>
31+
typealias MeaningfulStaticFieldsType = PersistentSet<FieldId>
32+
typealias AddrToArrayTypeType = PersistentMap<UtAddrExpression, ArrayType>
33+
typealias AddrToMockInfoType = PersistentMap<UtAddrExpression, UtMockInfo>
34+
typealias VisitedValuesType = PersistentList<UtAddrExpression>
35+
typealias TouchedAddressesType = PersistentList<UtAddrExpression>
36+
typealias ClassIdToClearStaticsType = ClassId?
37+
typealias InstanceFieldReadsType = PersistentSet<InstanceFieldReadOperation>
38+
typealias SpeculativelyNotNullAddressesType = PersistentList<UtAddrExpression>
39+
typealias SymbolicEnumValuesType = PersistentList<ObjectValue>
40+
41+
context(Simplificator)
42+
class MemoryUpdateSimplificator : CachingSimplificatorAdapter<MemoryUpdate>() {
43+
override fun simplifyImpl(expression: MemoryUpdate): MemoryUpdate {
44+
val stores = simplifyStores(expression.stores)
45+
val touchedChunkDescriptors = simplifyTocuhedChunkDescriptors(expression.touchedChunkDescriptors)
46+
val concrete = simplifyConcrete(expression.concrete)
47+
val mockInfos = simplifyMockInfos(expression.mockInfos)
48+
val staticInstanceStorage = simplifyStaticInstanceStorage(expression.staticInstanceStorage)
49+
val initializedStaticFields = simplifyInitializedStaticFields(expression.initializedStaticFields)
50+
val staticFieldsUpdates = simplifyStaticFieldsUpdates(expression.staticFieldsUpdates)
51+
val meaningfulStaticFields = simplifyMeaningfulStaticFields(expression.meaningfulStaticFields)
52+
val addrToArrayType = simplifyAddrToArrayType(expression.addrToArrayType)
53+
val addrToMockInfo = simplifyAddToMockInfo(expression.addrToMockInfo)
54+
val visitedValues = simplifyVisitedValues(expression.visitedValues)
55+
val touchedAddresses = simplifyTouchedAddresses(expression.touchedAddresses)
56+
val classIdToClearStatics = simplifyClassIdToClearStatics(expression.classIdToClearStatics)
57+
val instanceFieldReads = simplifyInstanceFieldReads(expression.instanceFieldReads)
58+
val speculativelyNotNullAddresses =
59+
simplifySpeculativelyNotNullAddresses(expression.speculativelyNotNullAddresses)
60+
val symbolicEnumValues = simplifyEnumValues(expression.symbolicEnumValues)
61+
return MemoryUpdate(
62+
stores,
63+
touchedChunkDescriptors,
64+
concrete,
65+
mockInfos,
66+
staticInstanceStorage,
67+
initializedStaticFields,
68+
staticFieldsUpdates,
69+
meaningfulStaticFields,
70+
addrToArrayType,
71+
addrToMockInfo,
72+
visitedValues,
73+
touchedAddresses,
74+
classIdToClearStatics,
75+
instanceFieldReads,
76+
speculativelyNotNullAddresses,
77+
symbolicEnumValues
78+
)
79+
}
80+
81+
private fun simplifyStores(stores: StoresType): StoresType =
82+
stores
83+
.mutate { prevStores ->
84+
prevStores.replaceAll { store ->
85+
store.copy(
86+
index = store.index.accept(this@Simplificator),
87+
value = store.value.accept(this@Simplificator)
88+
)
89+
}
90+
}
91+
92+
private fun simplifyTocuhedChunkDescriptors(touchedChunkDescriptors: TouchedChunkDescriptorsType): TouchedChunkDescriptorsType =
93+
touchedChunkDescriptors
94+
95+
private fun simplifyConcrete(concrete: ConcreteType): ConcreteType =
96+
concrete
97+
.mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression }
98+
.toPersistentMap()
99+
100+
private fun simplifyMockInfos(mockInfos: MockInfosType): MockInfosType =
101+
mockInfos.mutate { prevMockInfos ->
102+
prevMockInfos.replaceAll {
103+
simplifyMockInfoEnriched(it)
104+
}
105+
}
106+
107+
108+
private fun simplifyStaticInstanceStorage(staticInstanceStorage: StaticInstanceStorageType): StaticInstanceStorageType =
109+
staticInstanceStorage.mutate { prevStorage ->
110+
prevStorage.replaceAll { _, v -> simplifySymbolicValue(v) as ObjectValue }
111+
}
112+
113+
private fun simplifyInitializedStaticFields(initializedStaticFields: InitializedStaticFieldsType): InitializedStaticFieldsType =
114+
initializedStaticFields
115+
116+
private fun simplifyStaticFieldsUpdates(staticFieldsUpdates: StaticFieldsUpdatesType): StaticFieldsUpdatesType =
117+
staticFieldsUpdates.mutate { prevUpdates ->
118+
prevUpdates.replaceAll { staticFieldMemoryUpdateInfo(it) }
119+
}
120+
121+
private fun simplifyMeaningfulStaticFields(meaningfulStaticFields: MeaningfulStaticFieldsType): MeaningfulStaticFieldsType =
122+
meaningfulStaticFields
123+
124+
125+
private fun simplifyAddrToArrayType(addrToArrayType: AddrToArrayTypeType): AddrToArrayTypeType =
126+
addrToArrayType
127+
.mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression }
128+
.toPersistentMap()
129+
130+
131+
private fun simplifyAddToMockInfo(addrToMockInfo: AddrToMockInfoType): AddrToMockInfoType =
132+
addrToMockInfo
133+
.mapKeys { (k, _) -> k.accept(this@Simplificator) as UtAddrExpression }
134+
.toPersistentMap()
135+
136+
private fun simplifyVisitedValues(visitedValues: VisitedValuesType): VisitedValuesType =
137+
visitedValues.mutate { prevValues ->
138+
prevValues.replaceAll { it.accept(this@Simplificator) as UtAddrExpression }
139+
}
140+
141+
private fun simplifyTouchedAddresses(touchedAddresses: TouchedAddressesType): TouchedAddressesType =
142+
touchedAddresses.mutate { prevAddresses ->
143+
prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression }
144+
}
145+
146+
private fun simplifyClassIdToClearStatics(classIdToClearStatics: ClassIdToClearStaticsType): ClassIdToClearStaticsType =
147+
classIdToClearStatics
148+
149+
private fun simplifyInstanceFieldReads(instanceFieldReads: InstanceFieldReadsType): InstanceFieldReadsType =
150+
instanceFieldReads
151+
.map { it.copy(addr = it.addr.accept(this@Simplificator) as UtAddrExpression) }
152+
.toPersistentSet()
153+
154+
private fun simplifySpeculativelyNotNullAddresses(speculativelyNotNullAddresses: SpeculativelyNotNullAddressesType): SpeculativelyNotNullAddressesType =
155+
speculativelyNotNullAddresses.mutate { prevAddresses ->
156+
prevAddresses.replaceAll { it.accept(this@Simplificator) as UtAddrExpression }
157+
}
158+
159+
private fun simplifyEnumValues(symbolicEnumValues: SymbolicEnumValuesType): SymbolicEnumValuesType =
160+
symbolicEnumValues.mutate { values ->
161+
values.replaceAll { simplifySymbolicValue(it) as ObjectValue }
162+
}
163+
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/simplificators/SimplificatorAdapter.kt

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package org.utbot.engine.simplificators
2+
3+
import java.util.IdentityHashMap
4+
5+
6+
interface SimplificatorAdapter<T> {
7+
fun simplify(expression: T): T
8+
}
9+
10+
abstract class CachingSimplificatorAdapter<T> : SimplificatorAdapter<T> {
11+
private val cache: IdentityHashMap<T, T> = IdentityHashMap()
12+
13+
final override fun simplify(expression: T): T =
14+
cache.getOrPut(expression) { simplifyImpl(expression) }
15+
16+
protected abstract fun simplifyImpl(expression: T): T
17+
}
18+

0 commit comments

Comments
 (0)