Skip to content

Commit

Permalink
Symbolic sets and map merge (#55)
Browse files Browse the repository at this point in the history 
---------

Co-authored-by: Sergey Pospelov <[email protected]>
  • Loading branch information
@Saloed @sergeypospelov
Saloed and sergeypospelov authored Sep 5, 2023
1 parent 6ed724e commit 2021212
Show file tree
Hide file tree
Showing 62 changed files with 3,734 additions and 1,165 deletions.
24 changes: 23 additions & 1 deletion usvm-core/src/main/kotlin/org/usvm/Composition.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@ import org.usvm.collection.map.primitive.UInputMapReading
import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading
import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
import org.usvm.collection.set.primitive.UAllocatedSetReading
import org.usvm.collection.set.primitive.UInputSetReading
import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
import org.usvm.memory.UReadOnlyMemory
import org.usvm.memory.USymbolicCollectionId
import org.usvm.regions.Region
Expand Down Expand Up @@ -100,10 +105,27 @@ open class UComposer<Type>(
override fun transform(expr: UInputMapLengthReading<Type>): USizeExpr =
transformCollectionReading(expr, expr.address)

override fun <ElemSort : USort, Reg : Region<Reg>> transform(
expr: UAllocatedSetReading<Type, ElemSort, Reg>
): UBoolExpr = transformCollectionReading(expr, expr.element)

override fun <ElemSort : USort, Reg : Region<Reg>> transform(
expr: UInputSetReading<Type, ElemSort, Reg>
): UBoolExpr = transformCollectionReading(expr, expr.address to expr.element)

override fun transform(expr: UAllocatedRefSetWithInputElementsReading<Type>): UBoolExpr =
transformCollectionReading(expr, expr.elementRef)

override fun transform(expr: UInputRefSetWithAllocatedElementsReading<Type>): UBoolExpr =
transformCollectionReading(expr, expr.setRef)

override fun transform(expr: UInputRefSetWithInputElementsReading<Type>): UBoolExpr =
transformCollectionReading(expr, expr.setRef to expr.elementRef)

override fun transform(expr: UConcreteHeapRef): UExpr<UAddressSort> = expr

override fun transform(expr: UNullRef): UExpr<UAddressSort> = memory.nullRef()
}

@Suppress("NOTHING_TO_INLINE")
inline fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr
inline fun <T : USort> UComposer<*>?.compose(expr: UExpr<T>) = this?.apply(expr) ?: expr
66 changes: 66 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/Context.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,16 @@ import org.usvm.collection.map.ref.UInputRefMap
import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeys
import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
import org.usvm.collection.set.primitive.UAllocatedSet
import org.usvm.collection.set.primitive.UAllocatedSetReading
import org.usvm.collection.set.primitive.UInputSet
import org.usvm.collection.set.primitive.UInputSetReading
import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElements
import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElements
import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithInputElements
import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
import org.usvm.memory.splitUHeapRef
import org.usvm.solver.USolverBase
import org.usvm.types.UTypeSystem
Expand Down Expand Up @@ -248,6 +258,62 @@ open class UContext(
UInputMapLengthReading<MapType>(this, region, address)
}.cast()


private val allocatedSymbolicSetReadingCache = mkAstInterner<UAllocatedSetReading<*, *, *>>()

fun <SetType, ElementSort : USort, Reg : Region<Reg>> mkAllocatedSetReading(
region: UAllocatedSet<SetType, ElementSort, Reg>,
element: UExpr<ElementSort>
): UAllocatedSetReading<SetType, ElementSort, Reg> =
allocatedSymbolicSetReadingCache.createIfContextActive {
UAllocatedSetReading(this, region, element)
}.cast()

private val inputSymbolicSetReadingCache = mkAstInterner<UInputSetReading<*, *, *>>()

fun <SetType, ElementSort : USort, Reg : Region<Reg>> mkInputSetReading(
region: UInputSet<SetType, ElementSort, Reg>,
address: UHeapRef,
element: UExpr<ElementSort>
): UInputSetReading<SetType, ElementSort, Reg> =
inputSymbolicSetReadingCache.createIfContextActive {
UInputSetReading(this, region, address, element)
}.cast()

private val allocatedSymbolicRefSetWithInputElementsReadingCache =
mkAstInterner<UAllocatedRefSetWithInputElementsReading<*>>()

fun <SetType> mkAllocatedRefSetWithInputElementsReading(
region: UAllocatedRefSetWithInputElements<SetType>,
elementRef: UHeapRef
): UAllocatedRefSetWithInputElementsReading<SetType> =
allocatedSymbolicRefSetWithInputElementsReadingCache.createIfContextActive {
UAllocatedRefSetWithInputElementsReading(this, region, elementRef)
}.cast()

private val inputSymbolicRefSetWithAllocatedElementsReadingCache =
mkAstInterner<UInputRefSetWithAllocatedElementsReading<*>>()

fun <SetType> mkInputRefSetWithAllocatedElementsReading(
region: UInputRefSetWithAllocatedElements<SetType>,
setRef: UHeapRef
): UInputRefSetWithAllocatedElementsReading<SetType> =
inputSymbolicRefSetWithAllocatedElementsReadingCache.createIfContextActive {
UInputRefSetWithAllocatedElementsReading(this, region, setRef)
}.cast()

private val inputSymbolicRefSetWithInputElementsReadingCache =
mkAstInterner<UInputRefSetWithInputElementsReading<*>>()

fun <SetType> mkInputRefSetWithInputElementsReading(
region: UInputRefSetWithInputElements<SetType>,
setRef: UHeapRef,
elementRef: UHeapRef
): UInputRefSetWithInputElementsReading<SetType> =
inputSymbolicRefSetWithInputElementsReadingCache.createIfContextActive {
UInputRefSetWithInputElementsReading(this, region, setRef, elementRef)
}.cast()

private val indexedMethodReturnValueCache = mkAstInterner<UIndexedMethodReturnValue<Any, out USort>>()

fun <Method, Sort : USort> mkIndexedMethodReturnValue(
Expand Down
18 changes: 18 additions & 0 deletions usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,11 @@ import org.usvm.collection.map.primitive.UInputMapReading
import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading
import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading
import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading
import org.usvm.collection.set.primitive.UAllocatedSetReading
import org.usvm.collection.set.primitive.UInputSetReading
import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
import org.usvm.regions.Region

interface UTransformer<Type> : KTransformer {
Expand Down Expand Up @@ -45,6 +50,16 @@ interface UTransformer<Type> : KTransformer {

fun transform(expr: UInputMapLengthReading<Type>): USizeExpr

fun <ElemSort : USort, Reg : Region<Reg>> transform(expr: UAllocatedSetReading<Type, ElemSort, Reg>): UBoolExpr

fun <ElemSort : USort, Reg : Region<Reg>> transform(expr: UInputSetReading<Type, ElemSort, Reg>): UBoolExpr

fun transform(expr: UAllocatedRefSetWithInputElementsReading<Type>): UBoolExpr

fun transform(expr: UInputRefSetWithAllocatedElementsReading<Type>): UBoolExpr

fun transform(expr: UInputRefSetWithInputElementsReading<Type>): UBoolExpr

fun <Sort : USort> transform(expr: UMockSymbol<Sort>): UExpr<Sort>

fun <Method, Sort : USort> transform(expr: UIndexedMethodReturnValue<Method, Sort>): UExpr<Sort>
Expand All @@ -64,3 +79,6 @@ abstract class UExprTransformer<Type>(

@Suppress("UNCHECKED_CAST")
fun <Type> UTransformer<*>.asTypedTransformer() = this as UTransformer<Type>

@Suppress("NOTHING_TO_INLINE")
inline fun <T : USort> UTransformer<*>?.apply(expr: UExpr<T>) = this?.apply(expr) ?: expr
70 changes: 43 additions & 27 deletions usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package org.usvm.api.collection

import org.usvm.StepScope
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.USizeExpr
Expand All @@ -11,72 +12,87 @@ import org.usvm.api.readArrayLength
import org.usvm.api.writeArrayIndex
import org.usvm.api.writeArrayLength
import org.usvm.memory.map
import org.usvm.uctx

object ListCollectionApi {
fun <ListType> UState<ListType, *, *, *, *>.mkSymbolicList(
listType: ListType
listType: ListType,
): UHeapRef = with(memory.ctx) {
val ref = memory.alloc(listType)
memory.writeArrayLength(ref, mkSizeExpr(0), listType)
return ref
ref
}

/**
* List size may be incorrect for input lists.
* Use [ensureListSizeCorrect] to guarantee that list size is correct.
* */
fun <ListType> UState<ListType, *, *, *, *>.symbolicListSize(
listRef: UHeapRef,
listType: ListType
): USizeExpr = with(memory.ctx) {
listType: ListType,
): USizeExpr = memory.readArrayLength(listRef, listType)

fun <ListType, State : UState<ListType, *, *, *, State>> StepScope<State, ListType, *>.ensureListSizeCorrect(
listRef: UHeapRef,
listType: ListType,
): Unit? {
listRef.map(
concreteMapper = { concreteListRef ->
memory.readArrayLength(concreteListRef, listType)
concreteMapper = {
// Concrete list size is always correct
it
},
symbolicMapper = { symbolicListRef ->
memory.readArrayLength(symbolicListRef, listType).also {
pathConstraints += mkBvSignedGreaterOrEqualExpr(it, mkSizeExpr(0))
val length = calcOnState { memory.readArrayLength(symbolicListRef, listType) }
with(length.uctx) {
val boundConstraint = mkBvSignedGreaterOrEqualExpr(length, mkSizeExpr(0))
// List size must be correct regardless of guard
assert(boundConstraint) ?: return null
}
symbolicListRef
}
)
return Unit
}

fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListGet(
listRef: UHeapRef,
index: USizeExpr,
listType: ListType,
sort: Sort
): UExpr<Sort> = with(memory.ctx) {
memory.readArrayIndex(listRef, index, listType, sort)
}
sort: Sort,
): UExpr<Sort> = memory.readArrayIndex(listRef, index, listType, sort)

fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListAdd(
listRef: UHeapRef,
listType: ListType,
sort: Sort,
value: UExpr<Sort>
): Unit = with(memory.ctx) {
value: UExpr<Sort>,
) {
val size = symbolicListSize(listRef, listType)

memory.writeArrayIndex(listRef, size, listType, sort, value, guard = trueExpr)

val updatedSize = mkBvAddExpr(size, mkSizeExpr(1))
memory.writeArrayLength(listRef, updatedSize, listType)
with(memory.ctx) {
memory.writeArrayIndex(listRef, size, listType, sort, value, guard = trueExpr)
val updatedSize = mkBvAddExpr(size, mkSizeExpr(1))
memory.writeArrayLength(listRef, updatedSize, listType)
}
}

fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListSet(
listRef: UHeapRef,
listType: ListType,
sort: Sort,
index: USizeExpr,
value: UExpr<Sort>
) = with(memory.ctx) {
memory.writeArrayIndex(listRef, index, listType, sort, value, guard = trueExpr)
value: UExpr<Sort>,
) {
memory.writeArrayIndex(listRef, index, listType, sort, value, guard = memory.ctx.trueExpr)
}

fun <ListType, Sort : USort> UState<ListType, *, *, *, *>.symbolicListInsert(
listRef: UHeapRef,
listType: ListType,
sort: Sort,
index: USizeExpr,
value: UExpr<Sort>
): Unit = with(memory.ctx) {
value: UExpr<Sort>,
) = with(memory.ctx) {
val currentSize = symbolicListSize(listRef, listType)

val srcIndex = index
Expand Down Expand Up @@ -104,8 +120,8 @@ object ListCollectionApi {
listRef: UHeapRef,
listType: ListType,
sort: Sort,
index: USizeExpr
): Unit = with(memory.ctx) {
index: USizeExpr,
) = with(memory.ctx) {
val currentSize = symbolicListSize(listRef, listType)

val firstIndexAfterRemove = mkBvAddExpr(index, mkSizeExpr(1))
Expand Down Expand Up @@ -133,8 +149,8 @@ object ListCollectionApi {
sort: Sort,
srcFrom: USizeExpr,
dstFrom: USizeExpr,
length: USizeExpr
): Unit = with(memory.ctx) {
length: USizeExpr,
) {
memory.memcpy(
srcRef = srcRef,
dstRef = dstRef,
Expand Down
Loading

0 comments on commit 2021212

Please sign in to comment.