|
| 1 | +package org.usvm.machine.expr |
| 2 | + |
| 3 | +import io.ksmt.utils.asExpr |
| 4 | +import org.jacodb.ets.model.EtsArrayAccess |
| 5 | +import org.jacodb.ets.model.EtsArrayType |
| 6 | +import org.jacodb.ets.model.EtsBooleanType |
| 7 | +import org.jacodb.ets.model.EtsNumberType |
| 8 | +import org.jacodb.ets.model.EtsUnknownType |
| 9 | +import org.usvm.UConcreteHeapRef |
| 10 | +import org.usvm.UExpr |
| 11 | +import org.usvm.UHeapRef |
| 12 | +import org.usvm.api.typeStreamOf |
| 13 | +import org.usvm.isAllocatedConcreteHeapRef |
| 14 | +import org.usvm.machine.TsContext |
| 15 | +import org.usvm.machine.TsSizeSort |
| 16 | +import org.usvm.machine.interpreter.TsStepScope |
| 17 | +import org.usvm.machine.types.mkFakeValue |
| 18 | +import org.usvm.sizeSort |
| 19 | +import org.usvm.types.first |
| 20 | +import org.usvm.util.mkArrayIndexLValue |
| 21 | +import org.usvm.util.mkArrayLengthLValue |
| 22 | + |
| 23 | +internal fun TsExprResolver.handleArrayAccess( |
| 24 | + value: EtsArrayAccess, |
| 25 | +): UExpr<*>? = with(ctx) { |
| 26 | + // Resolve the array. |
| 27 | + val array = resolve(value.array) ?: return null |
| 28 | + check(array.sort == addressSort) { |
| 29 | + "Expected address sort for array, got: ${array.sort}" |
| 30 | + } |
| 31 | + val arrayRef = array.asExpr(addressSort) |
| 32 | + |
| 33 | + // Check for undefined or null array access. |
| 34 | + checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null |
| 35 | + |
| 36 | + // Resolve the index. |
| 37 | + val resolvedIndex = resolve(value.index) ?: return null |
| 38 | + check(resolvedIndex.sort == fp64Sort) { |
| 39 | + "Expected fp64 sort for index, got: ${resolvedIndex.sort}" |
| 40 | + } |
| 41 | + val index = resolvedIndex.asExpr(fp64Sort) |
| 42 | + |
| 43 | + // Convert the index to a bit-vector. |
| 44 | + val bvIndex = mkFpToBvExpr( |
| 45 | + roundingMode = fpRoundingModeSortDefaultValue(), |
| 46 | + value = index, |
| 47 | + bvSize = sizeSort.sizeBits.toInt(), |
| 48 | + isSigned = true, |
| 49 | + ).asExpr(sizeSort) |
| 50 | + |
| 51 | + // Determine the array type. |
| 52 | + val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) { |
| 53 | + scope.calcOnState { memory.typeStreamOf(arrayRef).first() } |
| 54 | + } else { |
| 55 | + value.array.type |
| 56 | + } |
| 57 | + check(arrayType is EtsArrayType) { |
| 58 | + "Expected EtsArrayType, got: ${value.array.type}" |
| 59 | + } |
| 60 | + |
| 61 | + // Read the array element. |
| 62 | + readArray(scope, arrayRef, bvIndex, arrayType) |
| 63 | +} |
| 64 | + |
| 65 | +fun TsContext.readArray( |
| 66 | + scope: TsStepScope, |
| 67 | + array: UHeapRef, |
| 68 | + index: UExpr<TsSizeSort>, |
| 69 | + arrayType: EtsArrayType, |
| 70 | +): UExpr<*>? { |
| 71 | + // Read the array length. |
| 72 | + val length = scope.calcOnState { |
| 73 | + val lengthLValue = mkArrayLengthLValue(array, arrayType) |
| 74 | + memory.read(lengthLValue) |
| 75 | + } |
| 76 | + |
| 77 | + // Check for out-of-bounds access. |
| 78 | + checkNegativeIndexRead(scope, index) ?: return null |
| 79 | + checkReadingInRange(scope, index, length) ?: return null |
| 80 | + |
| 81 | + // Determine the element sort. |
| 82 | + val sort = typeToSort(arrayType.elementType) |
| 83 | + |
| 84 | + // If the element type is known, we can read it directly. |
| 85 | + if (sort !is TsUnresolvedSort) { |
| 86 | + val lValue = mkArrayIndexLValue( |
| 87 | + sort = sort, |
| 88 | + ref = array, |
| 89 | + index = index, |
| 90 | + type = arrayType, |
| 91 | + ) |
| 92 | + return scope.calcOnState { memory.read(lValue) } |
| 93 | + } |
| 94 | + |
| 95 | + // Concrete arrays with the unresolved sort should consist of fake objects only. |
| 96 | + if (array is UConcreteHeapRef) { |
| 97 | + // Read a fake object from the array. |
| 98 | + val lValue = mkArrayIndexLValue( |
| 99 | + sort = addressSort, |
| 100 | + ref = array, |
| 101 | + index = index, |
| 102 | + type = arrayType, |
| 103 | + ) |
| 104 | + return scope.calcOnState { memory.read(lValue) } |
| 105 | + } |
| 106 | + |
| 107 | + // If the element type is unresolved, we need to create a fake object |
| 108 | + // that can hold boolean, number, and reference values. |
| 109 | + // We read all three types from the array and combine them into a fake object. |
| 110 | + return scope.calcOnState { |
| 111 | + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) |
| 112 | + val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType) |
| 113 | + val bool = memory.read(boolLValue) |
| 114 | + |
| 115 | + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) |
| 116 | + val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType) |
| 117 | + val fp = memory.read(fpLValue) |
| 118 | + |
| 119 | + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) |
| 120 | + val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType) |
| 121 | + val ref = memory.read(refLValue) |
| 122 | + |
| 123 | + // If the read reference is already a fake object, we can return it directly. |
| 124 | + // Otherwise, we need to create a new fake object and write it back to the memory. |
| 125 | + // TODO: Think about the type constraint to get a consistent array resolution later |
| 126 | + if (ref.isFakeObject()) { |
| 127 | + ref |
| 128 | + } else { |
| 129 | + val fakeObj = mkFakeValue(scope, bool, fp, ref) |
| 130 | + lValuesToAllocatedFakeObjects += refLValue to fakeObj |
| 131 | + memory.write(refLValue, fakeObj, guard = trueExpr) |
| 132 | + fakeObj |
| 133 | + } |
| 134 | + } |
| 135 | +} |
0 commit comments