UConcreteHeapRef implements KInterpretedValue (#36)

UnitTestBot · Jul 5, 2023 · cf9420c · cf9420c
1 parent 6a4e8c7
commit cf9420c
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 6 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -23,7 +23,7 @@ open class UContext(
     components: UComponents<*, *, *>,
     operationMode: OperationMode = OperationMode.CONCURRENT,
     astManagementMode: AstManagementMode = AstManagementMode.GC,
-    simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY
+    simplificationMode: SimplificationMode = SimplificationMode.SIMPLIFY,
 ) : KContext(operationMode, astManagementMode, simplificationMode) {
 
     private val solver by lazy { components.mkSolver(this) }
@@ -169,18 +169,21 @@ open class UContext(
     fun <Method, Sort : USort> mkIndexedMethodReturnValue(
         method: Method,
         callIndex: Int,
-        sort: Sort
+        sort: Sort,
     ): UIndexedMethodReturnValue<Method, Sort> = indexedMethodReturnValueCache.createIfContextActive {
         UIndexedMethodReturnValue(this, method.cast(), callIndex, sort)
     }.cast()
 
     private val isExprCache = mkAstInterner<UIsExpr<Any>>()
     fun <Type> mkIsExpr(
-        ref: UHeapRef, type: Type
+        ref: UHeapRef, type: Type,
     ): UIsExpr<Type> = isExprCache.createIfContextActive {
         UIsExpr(this, ref, type.cast())
     }.cast()
 
+    fun mkConcreteHeapRefDecl(address: UConcreteHeapAddress): UConcreteHeapRefDecl =
+        UConcreteHeapRefDecl(this, address)
+
     override fun boolSortDefaultValue(): KExpr<KBoolSort> = falseExpr
 
     override fun <S : KBvSort> bvSortDefaultValue(sort: S): KExpr<S> = mkBv(0, sort)

diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
@@ -2,10 +2,28 @@ package org.usvm
 
 import io.ksmt.cache.hash
 import io.ksmt.cache.structurallyEqual
-import io.ksmt.expr.*
+import io.ksmt.decl.KConstDecl
+import io.ksmt.expr.KAndExpr
+import io.ksmt.expr.KApp
+import io.ksmt.expr.KBitVec32Value
+import io.ksmt.expr.KBitVec64Value
+import io.ksmt.expr.KEqExpr
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KFalse
+import io.ksmt.expr.KIntNumExpr
+import io.ksmt.expr.KInterpretedValue
+import io.ksmt.expr.KIteExpr
+import io.ksmt.expr.KNotExpr
+import io.ksmt.expr.KOrExpr
+import io.ksmt.expr.KTrue
 import io.ksmt.expr.printer.ExpressionPrinter
 import io.ksmt.expr.transformer.KTransformerBase
-import io.ksmt.sort.*
+import io.ksmt.sort.KBoolSort
+import io.ksmt.sort.KBv32Sort
+import io.ksmt.sort.KBvSort
+import io.ksmt.sort.KFpSort
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KUninterpretedSort
 import org.usvm.memory.UAllocatedArrayId
 import org.usvm.memory.UAllocatedArrayRegion
 import org.usvm.memory.UInputArrayId
@@ -37,6 +55,7 @@ typealias UOrExpr = KOrExpr
 typealias UIteExpr<Sort> = KIteExpr<Sort>
 typealias UEqExpr<Sort> = KEqExpr<Sort>
 typealias UNotExpr = KNotExpr
+typealias UIntepretedValue<Sort> = KInterpretedValue<Sort>
 typealias UConcreteInt = KIntNumExpr
 typealias UConcreteInt32 = KBitVec32Value
 typealias UConcreteInt64 = KBitVec64Value
@@ -69,7 +88,20 @@ typealias UConcreteHeapAddress = Int
 fun isSymbolicHeapRef(expr: UExpr<*>) =
     expr.sort == expr.uctx.addressSort && expr !is UConcreteHeapRef
 
-class UConcreteHeapRef internal constructor(ctx: UContext, val address: UConcreteHeapAddress) : UHeapRef(ctx) {
+class UConcreteHeapRefDecl internal constructor(
+    ctx: UContext,
+    val address: UConcreteHeapAddress,
+) : KConstDecl<UAddressSort>(ctx, "0x$address", ctx.addressSort) {
+    override fun apply(args: List<KExpr<*>>): KApp<UAddressSort, *> = uctx.mkConcreteHeapRef(address)
+}
+
+class UConcreteHeapRef internal constructor(
+    ctx: UContext,
+    val address: UConcreteHeapAddress,
+) : UIntepretedValue<UAddressSort>(ctx) {
+
+    override val decl: UConcreteHeapRefDecl get() = uctx.mkConcreteHeapRefDecl(address)
+
     override val sort: UAddressSort = ctx.addressSort
 
     override fun accept(transformer: KTransformerBase): KExpr<UAddressSort> {