@@ -215,13 +215,17 @@ class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
215
215
createArray(addr, valueType, useConcreteType = false )
216
216
}
217
217
218
- listOf (
219
- MethodResult (
220
- SymbolicSuccess (resultObject),
221
- typeRegistry.typeConstraintToGenericTypeParameter(addr, wrapper.addr, i = TYPE_PARAMETER_INDEX )
222
- .asHardConstraint()
223
- )
224
- )
218
+ val typeIndex = wrapper.asWrapperOrNull?.getOperationTypeIndex
219
+ ? : error(" Wrapper was expected, got $wrapper " )
220
+ val typeConstraint = typeRegistry.typeConstraintToGenericTypeParameter(
221
+ addr,
222
+ wrapper.addr,
223
+ i = typeIndex
224
+ ).asHardConstraint()
225
+
226
+ val methodResult = MethodResult (SymbolicSuccess (resultObject), typeConstraint)
227
+
228
+ listOf (methodResult)
225
229
}
226
230
227
231
@Suppress(" UNUSED_PARAMETER" )
@@ -418,16 +422,17 @@ class AssociativeArrayWrapper : WrapperInterface {
418
422
val addr = UtAddrExpression (value)
419
423
val resultObject = createObject(addr, OBJECT_TYPE , useConcreteType = false )
420
424
421
- listOf (
422
- MethodResult (
423
- SymbolicSuccess (resultObject),
424
- typeRegistry.typeConstraintToGenericTypeParameter(
425
- addr,
426
- wrapper.addr,
427
- TYPE_PARAMETER_INDEX
428
- ).asHardConstraint()
429
- )
430
- )
425
+ val typeIndex = wrapper.asWrapperOrNull?.selectOperationTypeIndex
426
+ ? : error(" Wrapper was expected, got $wrapper " )
427
+ val hardConstraints = typeRegistry.typeConstraintToGenericTypeParameter(
428
+ addr,
429
+ wrapper.addr,
430
+ typeIndex
431
+ ).asHardConstraint()
432
+
433
+ val methodResult = MethodResult (SymbolicSuccess (resultObject), hardConstraints)
434
+
435
+ listOf (methodResult)
431
436
}
432
437
433
438
@Suppress(" UNUSED_PARAMETER" )
@@ -440,21 +445,31 @@ class AssociativeArrayWrapper : WrapperInterface {
440
445
with (traverser) {
441
446
val storageValue = getStorageArrayExpression(wrapper).store(parameters[0 ].addr, parameters[1 ].addr)
442
447
val sizeValue = getIntFieldValue(wrapper, sizeField)
448
+
449
+ // it is the reason why it's important to use an `oldKey` in `UtHashMap.put` method.
450
+ // We navigate in the associative array using only this old address, not a new one.
443
451
val touchedValue = getTouchedArrayExpression(wrapper).store(sizeValue, parameters[0 ].addr)
444
- listOf (
445
- MethodResult (
446
- SymbolicSuccess (voidValue),
447
- memoryUpdates = arrayUpdateWithValue(
448
- getStorageArrayField(wrapper.addr).addr ,
449
- OBJECT_TYPE .arrayType,
450
- storageValue
451
- ) + arrayUpdateWithValue(
452
- getTouchedArrayField(wrapper.addr).addr,
453
- OBJECT_TYPE .arrayType,
454
- touchedValue ,
455
- ) + objectUpdate(wrapper, sizeField, Add (sizeValue.toIntValue(), 1 .toPrimitiveValue()))
456
- )
452
+ val storageArrayAddr = getStorageArrayField(wrapper.addr).addr
453
+ val touchedArrayFieldAddr = getTouchedArrayField(wrapper.addr).addr
454
+
455
+ val storageArrayUpdate = arrayUpdateWithValue(
456
+ storageArrayAddr ,
457
+ OBJECT_TYPE .arrayType,
458
+ storageValue
459
+ )
460
+
461
+ val touchedArrayUpdate = arrayUpdateWithValue(
462
+ touchedArrayFieldAddr ,
463
+ OBJECT_TYPE .arrayType,
464
+ touchedValue,
457
465
)
466
+
467
+ val sizeUpdate = objectUpdate(wrapper, sizeField, Add (sizeValue.toIntValue(), 1 .toPrimitiveValue()))
468
+
469
+ val memoryUpdates = storageArrayUpdate + touchedArrayUpdate + sizeUpdate
470
+ val methodResult = MethodResult (SymbolicSuccess (voidValue), memoryUpdates = memoryUpdates)
471
+
472
+ listOf (methodResult)
458
473
}
459
474
460
475
override val wrappedMethods: Map <String , MethodSymbolicImplementation > = mapOf (
@@ -480,7 +495,7 @@ class AssociativeArrayWrapper : WrapperInterface {
480
495
// construct model values of an array
481
496
val touchedValues = UtArrayModel (
482
497
resolver.holder.concreteAddr(UtAddrExpression (touchedArrayAddr)),
483
- objectClassId ,
498
+ objectArrayClassId ,
484
499
sizeValue,
485
500
UtNullModel (objectClassId),
486
501
stores = (0 until sizeValue).associateWithTo(mutableMapOf ()) { i ->
@@ -504,7 +519,7 @@ class AssociativeArrayWrapper : WrapperInterface {
504
519
505
520
val storageValues = UtArrayModel (
506
521
resolver.holder.concreteAddr(UtAddrExpression (storageArrayAddr)),
507
- objectClassId ,
522
+ objectArrayClassId ,
508
523
sizeValue,
509
524
UtNullModel (objectClassId),
510
525
stores = (0 until sizeValue).associateTo(mutableMapOf ()) { i ->
@@ -518,10 +533,12 @@ class AssociativeArrayWrapper : WrapperInterface {
518
533
)
519
534
})
520
535
521
- val model = UtCompositeModel (resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, false )
536
+ val model = UtCompositeModel (resolver.holder.concreteAddr(wrapper.addr), associativeArrayId, isMock = false )
537
+
522
538
model.fields[sizeField.fieldId] = UtPrimitiveModel (sizeValue)
523
539
model.fields[touchedField.fieldId] = touchedValues
524
540
model.fields[storageField.fieldId] = storageValues
541
+
525
542
return model
526
543
}
527
544
@@ -537,7 +554,7 @@ class AssociativeArrayWrapper : WrapperInterface {
537
554
private fun Traverser.getStorageArrayExpression (
538
555
wrapper : ObjectValue
539
556
): UtExpression = selectArrayExpressionFromMemory(getStorageArrayField(wrapper.addr))
540
- }
541
557
542
- // Arrays and lists have the only type parameter with index zero
543
- private const val TYPE_PARAMETER_INDEX = 0
558
+ override val selectOperationTypeIndex: Int
559
+ get() = 1
560
+ }
0 commit comments