Skip to content

Commit

Permalink
use memory ownership in memcpy, union, merge
Browse files Browse the repository at this point in the history
  • Loading branch information
@oveeernight
oveeernight committed Jul 25, 2024
1 parent 41e73bd commit 0c31856
Show file tree
Hide file tree
Showing 10 changed files with 37 additions and 27 deletions.
6 changes: 4 additions & 2 deletions usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ interface UArrayRegion<ArrayType, Sort : USort, USizeSort : USort> : UMemoryRegi
fromDstIdx: UExpr<USizeSort>,
toDstIdx: UExpr<USizeSort>,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
): UArrayRegion<ArrayType, Sort, USizeSort>

fun initializeAllocatedArray(
Expand Down Expand Up @@ -134,6 +135,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
fromDstIdx: UExpr<USizeSort>,
toDstIdx: UExpr<USizeSort>,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
) = foldHeapRef2(
ref0 = srcRef,
ref1 = dstRef,
Expand All @@ -146,7 +148,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
fromSrcIdx, fromDstIdx, toDstIdx, USizeExprKeyInfo()
)
val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedArray(dstConcrete.address, newDstCollection, srcRef.uctx.defaultOwnership)
region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership)
},

blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
Expand All @@ -171,7 +173,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
USizeExprKeyInfo()
)
val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedArray(dstConcrete.address, newDstCollection, srcRef.uctx.defaultOwnership)
region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership)
},
blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
val srcCollection = region.getInputArray(type, elementSort)
Expand Down
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ internal fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<*>.mem
"memcpy is not applicable to $region"
}

val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard)
val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard, ownership)
setRegion(regionId, newRegion)
}

Expand Down
6 changes: 4 additions & 2 deletions usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ interface UMapRegion<MapType, KeySort : USort, ValueSort : USort, Reg : Region<R
mapType: MapType,
srcKeySet: USetRegion<MapType, KeySort, *>,
initialGuard: UBoolExpr,
ownership: MutabilityOwnership,
): UMapRegion<MapType, KeySort, ValueSort, Reg>
}

Expand Down Expand Up @@ -155,6 +156,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
mapType: MapType,
srcKeySet: USetRegion<MapType, KeySort, *>,
initialGuard: UBoolExpr,
ownership: MutabilityOwnership,
) = foldHeapRef2(
ref0 = srcRef,
ref1 = dstRef,
Expand All @@ -170,7 +172,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg

val adapter = UAllocatedToAllocatedSymbolicMapMergeAdapter(srcKeys)
val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedMap(dstId, newDstCollection, defaultOwnership)
region.updateAllocatedMap(dstId, newDstCollection, ownership)
},
blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
val srcId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, srcConcrete.address)
Expand All @@ -191,7 +193,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg

val adapter = UInputToAllocatedSymbolicMapMergeAdapter(srcSymbolic, srcKeys)
val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedMap(dstId, newDstCollection, defaultOwnership)
region.updateAllocatedMap(dstId, newDstCollection, ownership)
},
blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
val srcCollection = region.getInputMap()
Expand Down
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,6 @@ internal fun <MapType, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UW
"mapMerge is not applicable to set $region"
}

val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard)
val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard, ownership)
setRegion(regionId, newRegion)
}
18 changes: 10 additions & 8 deletions usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ interface URefMapRegion<MapType, ValueSort : USort>
sort: ValueSort,
keySet: URefSetRegion<MapType>,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
): URefMapRegion<MapType, ValueSort>
}

Expand Down Expand Up @@ -256,6 +257,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
sort: ValueSort,
keySet: URefSetRegion<MapType>,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
) = foldHeapRef2(
ref0 = srcRef,
ref1 = dstRef,
Expand All @@ -271,7 +273,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
read = { initialAllocatedMapState[it] ?: valueSort.sampleUValue() },
mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) },
write = { result, dstKeyId, value, g ->
result.guardedWrite(dstKeyId, value, g, defaultOwnership) { valueSort.sampleUValue() }
result.guardedWrite(dstKeyId, value, g, ownership) { valueSort.sampleUValue() }
}
)
val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap)
Expand All @@ -285,7 +287,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(

val adapter = UAllocatedToAllocatedSymbolicRefMapMergeAdapter(srcKeys)
val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard)
updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, defaultOwnership)
updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership)
},
blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
val initialAllocatedMapState = region.allocatedMapWithAllocatedKeys
Expand All @@ -295,8 +297,8 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
mkDstKeyId = { inputMapWithAllocatedKeyId(it) },
write = { result, dstKeyId, value, g ->
val newMap = result.getInputMapWithAllocatedKeys(dstKeyId)
.write(dstSymbolic, value, g, defaultOwnership)
result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, defaultOwnership)
.write(dstSymbolic, value, g, ownership)
result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership)
}
)

Expand All @@ -317,7 +319,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
read = { region.getInputMapWithAllocatedKeys(it).read(srcSymbolic) },
mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) },
write = { result, dstKeyId, value, g ->
result.guardedWrite(dstKeyId, value, g, defaultOwnership) { sort.sampleUValue() }
result.guardedWrite(dstKeyId, value, g, ownership) { sort.sampleUValue() }
}
)
val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap)
Expand All @@ -330,7 +332,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(

val adapter = UInputToAllocatedSymbolicRefMapMergeAdapter(srcSymbolic, srcKeys)
val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard)
updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, defaultOwnership)
updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership)
},
blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
val updatedRegion = region.mergeInputMapAllocatedKeys(
Expand All @@ -339,8 +341,8 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
mkDstKeyId = { inputMapWithAllocatedKeyId(it) },
write = { result, dstKeyId, value, g ->
val newMap = result.getInputMapWithAllocatedKeys(dstKeyId)
.write(dstSymbolic, value, g, defaultOwnership)
result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, defaultOwnership)
.write(dstSymbolic, value, g, ownership)
result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership)
}
)
val srcKeys = keySet.inputSetWithInputElements()
Expand Down
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,6 @@ internal fun <MapType, ValueSort : USort> UWritableMemory<*>.refMapMerge(
"refMapMerge is not applicable to set $region"
}

val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard)
val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard, ownership)
setRegion(regionId, newRegion)
}
6 changes: 4 additions & 2 deletions usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,7 @@ interface USetRegion<SetType, ElementSort : USort, Reg : Region<Reg>> :
srcRef: UHeapRef,
dstRef: UHeapRef,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
): USetRegion<SetType, ElementSort, Reg>
}

Expand Down Expand Up @@ -154,6 +155,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
srcRef: UHeapRef,
dstRef: UHeapRef,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
) = foldHeapRef2(
ref0 = srcRef,
ref1 = dstRef,
Expand All @@ -168,7 +170,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>

val adapter = UAllocatedToAllocatedSymbolicSetUnionAdapter(srcCollection)
val updated = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedSet(dstId, updated, defaultOwnership)
region.updateAllocatedSet(dstId, updated, ownership)
},
blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
val srcId = UAllocatedSetId(srcConcrete.address, elementSort, setType, elementInfo)
Expand All @@ -188,7 +190,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>

val adapter = UInputToAllocatedSymbolicSetUnionAdapter(srcSymbolic, srcCollection)
val updated = dstCollection.copyRange(srcCollection, adapter, guard)
region.updateAllocatedSet(dstId, updated, defaultOwnership)
region.updateAllocatedSet(dstId, updated, ownership)
},
blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
val srcCollection = region.inputSetElements()
Expand Down
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ internal fun <SetType, KeySort : USort, Reg : Region<Reg>> UWritableMemory<*>.se
"setUnion is not applicable to $region"
}

val newRegion = region.union(srcRef, dstRef, guard)
val newRegion = region.union(srcRef, dstRef, guard, ownership)
setRegion(regionId, newRegion)
}

Expand Down
18 changes: 10 additions & 8 deletions usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ interface URefSetRegion<SetType> :
srcRef: UHeapRef,
dstRef: UHeapRef,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
): URefSetRegion<SetType>
}

Expand Down Expand Up @@ -245,6 +246,7 @@ internal class URefSetMemoryRegion<SetType>(
srcRef: UHeapRef,
dstRef: UHeapRef,
operationGuard: UBoolExpr,
ownership: MutabilityOwnership,
) = foldHeapRef2(
ref0 = srcRef,
ref1 = dstRef,
Expand All @@ -259,7 +261,7 @@ internal class URefSetMemoryRegion<SetType>(
read = { initialAllocatedSetState[it] ?: sort.uctx.falseExpr },
mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) },
write = { result, dstKeyId, value, g ->
result.guardedWrite(dstKeyId, value, g, defaultOwnership) { sort.uctx.falseExpr }
result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr }
}
)
val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet)
Expand All @@ -272,7 +274,7 @@ internal class URefSetMemoryRegion<SetType>(

val adapter = UAllocatedToAllocatedSymbolicRefSetUnionAdapter(srcCollection)
val updated = dstCollection.copyRange(srcCollection, adapter, guard)
updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, defaultOwnership)
updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership)
},
blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
val initialAllocatedSetState = region.allocatedSetWithAllocatedElements
Expand All @@ -282,8 +284,8 @@ internal class URefSetMemoryRegion<SetType>(
mkDstKeyId = { inputSetWithAllocatedElementsId(it) },
write = { result, dstKeyId, value, g ->
val newMap = result.getInputSetWithAllocatedElements(dstKeyId)
.write(dstSymbolic, value, g, defaultOwnership)
result.updateInputSetWithAllocatedElements(dstKeyId, newMap, defaultOwnership)
.write(dstSymbolic, value, g, ownership)
result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership)
}
)

Expand All @@ -303,7 +305,7 @@ internal class URefSetMemoryRegion<SetType>(
read = { region.getInputSetWithAllocatedElements(it).read(srcSymbolic) },
mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) },
write = { result, dstKeyId, value, g ->
result.guardedWrite(dstKeyId, value, g, defaultOwnership) { sort.uctx.falseExpr }
result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr }
}
)
val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet)
Expand All @@ -315,7 +317,7 @@ internal class URefSetMemoryRegion<SetType>(

val adapter = UInputToAllocatedSymbolicRefSetUnionAdapter(srcSymbolic, srcCollection)
val updated = dstCollection.copyRange(srcCollection, adapter, guard)
updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, defaultOwnership)
updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership)
},
blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
val updatedRegion = region.unionInputSetAllocatedElements(
Expand All @@ -324,8 +326,8 @@ internal class URefSetMemoryRegion<SetType>(
mkDstKeyId = { inputSetWithAllocatedElementsId(it) },
write = { result, dstKeyId, value, g ->
val newMap = result.getInputSetWithAllocatedElements(dstKeyId)
.write(dstSymbolic, value, g, defaultOwnership)
result.updateInputSetWithAllocatedElements(dstKeyId, newMap, defaultOwnership)
.write(dstSymbolic, value, g, ownership)
result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership)
}
)
val srcCollection = updatedRegion.inputSetWithInputElements()
Expand Down
2 changes: 1 addition & 1 deletion usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ internal fun <SetType> UWritableMemory<*>.refSetUnion(
"setUnion is not applicable to $region"
}

val newRegion = region.union(srcRef, dstRef, guard)
val newRegion = region.union(srcRef, dstRef, guard, ownership)
setRegion(regionId, newRegion)
}

Expand Down

0 comments on commit 0c31856

Please sign in to comment.