@@ -14,13 +14,15 @@ import org.utbot.engine.pc.UtExpression
1414import org.utbot.engine.pc.UtFalse
1515import org.utbot.engine.pc.UtInt32Sort
1616import org.utbot.engine.pc.UtIntSort
17+ import org.utbot.engine.pc.UtLongSort
1718import org.utbot.engine.pc.UtMkArrayExpression
1819import org.utbot.engine.pc.UtMkTermArrayExpression
1920import org.utbot.engine.pc.UtSeqSort
2021import org.utbot.engine.pc.UtSort
2122import org.utbot.engine.pc.UtTrue
2223import org.utbot.engine.pc.mkArrayConst
2324import org.utbot.engine.pc.mkInt
25+ import org.utbot.engine.pc.mkLong
2426import org.utbot.engine.pc.select
2527import org.utbot.engine.pc.store
2628import org.utbot.engine.pc.toSort
@@ -110,6 +112,12 @@ data class Memory( // TODO: split purely symbolic memory and information about s
110112 UtFalse ,
111113 UtArraySort (UtAddrSort , UtBoolSort )
112114 ),
115+ // const array here is because even in the situation when MUT is marked as a `PassThrough` we will
116+ // process this information in a current state, not initial one
117+ private var taintArray : UtArrayExpressionBase = UtConstArrayExpression (
118+ mkLong(value = 0L),
119+ UtArraySort (indexSort = UtAddrSort , itemSort = UtLongSort )
120+ ),
113121 private val symbolicEnumValues : PersistentList <ObjectValue > = persistentListOf()
114122) {
115123 val chunkIds: Set <ChunkId >
@@ -164,6 +172,8 @@ data class Memory( // TODO: split purely symbolic memory and information about s
164172 */
165173 fun isSpeculativelyNotNull (addr : UtAddrExpression ): UtArraySelectExpression = speculativelyNotNullAddresses.select(addr)
166174
175+ fun taintVector (addr : UtAddrExpression ): UtArraySelectExpression = taintArray.select(addr)
176+
167177 /* *
168178 * @return ImmutableCollection of the initial values for all the arrays we touched during the execution
169179 */
@@ -269,6 +279,17 @@ data class Memory( // TODO: split purely symbolic memory and information about s
269279 acc.store(addr, UtTrue )
270280 }
271281
282+ val updTaintArray = update.taintArrayUpdate
283+ .groupBy { (addr, _) ->
284+ addr
285+ }.map { (addr, listUpdates) ->
286+ addr to listUpdates.fold(mkLong(0 ).toLongValue()) { acc, (_, taintVector) ->
287+ Or (acc, taintVector.toLongValue()).toLongValue()
288+ }
289+ }.fold(taintArray) { acc, (addr, taintVector) ->
290+ acc.store(addr, taintVector.expr)
291+ }
292+
272293 // We have a list with updates for generic type info, and we want to apply
273294 // them in such way that only updates with more precise type information
274295 // should be applied.
@@ -305,6 +326,7 @@ data class Memory( // TODO: split purely symbolic memory and information about s
305326 touchedAddresses = updTouchedAddresses,
306327 instanceFieldReadOperations = instanceFieldReadOperations.addAll(update.instanceFieldReads),
307328 speculativelyNotNullAddresses = updSpeculativelyNotNullAddresses,
329+ taintArray = updTaintArray,
308330 symbolicEnumValues = symbolicEnumValues.addAll(update.symbolicEnumValues)
309331 )
310332 }
@@ -407,6 +429,7 @@ data class MemoryUpdate(
407429 val classIdToClearStatics : ClassId ? = null ,
408430 val instanceFieldReads : PersistentSet <InstanceFieldReadOperation > = persistentHashSetOf(),
409431 val speculativelyNotNullAddresses : PersistentList <UtAddrExpression > = persistentListOf(),
432+ val taintArrayUpdate : PersistentList <Pair <UtAddrExpression , UtExpression >> = persistentListOf(),
410433 val symbolicEnumValues : PersistentList <ObjectValue > = persistentListOf()
411434) {
412435 operator fun plus (other : MemoryUpdate ) =
@@ -428,6 +451,7 @@ data class MemoryUpdate(
428451 classIdToClearStatics = other.classIdToClearStatics,
429452 instanceFieldReads = instanceFieldReads.addAll(other.instanceFieldReads),
430453 speculativelyNotNullAddresses = speculativelyNotNullAddresses.addAll(other.speculativelyNotNullAddresses),
454+ taintArrayUpdate = taintArrayUpdate.addAll(other.taintArrayUpdate),
431455 symbolicEnumValues = symbolicEnumValues.addAll(other.symbolicEnumValues),
432456 )
433457
0 commit comments