Support of UTypeStreams and casts in JcInterpreter (#34)

Co-authored-by: Yury Kamenev <[email protected]>

buildSrc/src/main/kotlin/Versions.kt

@@ -2,7 +2,7 @@ object Versions {
     const val ksmt = "0.5.3"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.0.0"
+    const val jcdb = "1.1.3"
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
 

usvm-core/src/main/kotlin/org/usvm/Context.kt

@@ -17,6 +17,7 @@ import org.usvm.memory.UInputArrayRegion
 import org.usvm.memory.UInputFieldRegion
 import org.usvm.memory.splitUHeapRef
 import org.usvm.solver.USolverBase
+import org.usvm.types.UTypeSystem
 
 @Suppress("LeakingThis")
 open class UContext(
@@ -91,8 +92,8 @@ open class UContext(
             lhs is UConcreteHeapRef && rhs is UConcreteHeapRef -> mkBool(lhs == rhs)
             // unfolding
             else -> {
-                val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs)
-                val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs)
+                val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
+                val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
 
                 val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
 

usvm-core/src/main/kotlin/org/usvm/Expressions.kt

@@ -138,6 +138,28 @@ class UNullRef internal constructor(
     }
 }
 
+// We split all addresses into three parts:
+//     * input values: [Int.MIN_VALUE..0),
+//     * null value: [0]
+//     * allocated values: (0..[Int.MAX_VALUE]
+
+/**
+ * A constant corresponding to `null`.
+ */
+const val NULL_ADDRESS = 0
+
+/**
+ * A constant corresponding to the first input address in any decoded model.
+ * Input addresses takes this semi-interval: [[Int.MIN_VALUE]..0)
+ */
+const val INITIAL_INPUT_ADDRESS = NULL_ADDRESS - 1
+/**
+ * A constant corresponding to the first allocated address in any symbolic memory.
+ * Input addresses takes this semi-interval: (0..[Int.MAX_VALUE])
+ */
+const val INITIAL_CONCRETE_ADDRESS = NULL_ADDRESS + 1
+
+
 //endregion
 
 //region LValues
@@ -342,6 +364,10 @@ class UIndexedMethodReturnValue<Method, Sort : USort> internal constructor(
 
 //region Subtyping Expressions
 
+/**
+ * Means **either** [ref] is [UNullRef] **or** [ref] !is [UNullRef] and [ref] <: [type]. Thus, the actual type
+ * inheritance is checked only on non-null refs.
+ */
 class UIsExpr<Type> internal constructor(
     ctx: UContext,
     val ref: UHeapRef,
@@ -358,7 +384,7 @@ class UIsExpr<Type> internal constructor(
 
 
     override fun print(printer: ExpressionPrinter) {
-        TODO("Not yet implemented")
+        printer.append("($ref instance of $type)")
     }
 
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { ref }, { type })
@@ -372,4 +398,4 @@ class UIsExpr<Type> internal constructor(
 val UBoolExpr.isFalse get() = this == ctx.falseExpr
 val UBoolExpr.isTrue get() = this == ctx.trueExpr
 
-//endregion
+//endregion

usvm-core/src/main/kotlin/org/usvm/State.kt

@@ -20,8 +20,6 @@ abstract class UState<Type, Field, Method, Statement>(
     open var models: List<UModelBase<Field, Type>>,
     open var path: PersistentList<Statement>
 ) {
-    open val ctx: UContext = ctx
-
     /**
      * Deterministic state id.
      * TODO: Can be replaced with overridden hashCode
@@ -74,7 +72,7 @@ private fun <T : UState<Type, Field, *, *>, Type, Field> forkIfSat(
         return null
     }
 
-    val solver = state.ctx.solver<Field, Type, Any?>()
+    val solver = satisfiedCondition.uctx.solver<Field, Type, Any?>()
     val satResult = solver.check(pathConstraints, useSoftConstraints = true)
 
     return when (satResult) {
@@ -133,7 +131,7 @@ fun <T : UState<Type, Field, *, *>, Type, Field> fork(
         holdsInModel.isTrue
     }
 
-    val notCondition = state.ctx.mkNot(condition)
+    val notCondition = condition.uctx.mkNot(condition)
     val (posState, negState) = when {
 
         trueModels.isNotEmpty() && falseModels.isNotEmpty() -> {

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -50,7 +50,7 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
      * Forks on a [condition], performing [blockOnTrueState] on a state satisfying [condition] and
      * [blockOnFalseState] on a state satisfying [condition].not().
      *
-     * If the [condition], sets underlying state to `null`.
+     * If the [condition] is unsatisfiable, sets underlying state to `null`.
      *
      * @return `null` if the [condition] is unsatisfiable.
      */

usvm-core/src/main/kotlin/org/usvm/UComponents.kt

@@ -1,6 +1,7 @@
 package org.usvm
 
 import org.usvm.solver.USolverBase
+import org.usvm.types.UTypeSystem
 
 /**
  * Provides core USVM components tuned for specific language.

usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt

@@ -36,11 +36,11 @@ class UEqualityConstraints private constructor(
         equalReferences.subscribe(::rename)
     }
 
-    var isContradiction = false
+    var isContradicting = false
         private set
 
     private fun contradiction() {
-        isContradiction = true
+        isContradicting = true
         equalReferences.clear()
         mutableDistinctReferences.clear()
         mutableReferenceDisequalities.clear()
@@ -89,8 +89,8 @@ class UEqualityConstraints private constructor(
     /**
      * Adds an assertion that [ref1] is always equal to [ref2].
      */
-    fun addReferenceEquality(ref1: UHeapRef, ref2: UHeapRef) {
-        if (isContradiction) {
+    fun makeEqual(ref1: UHeapRef, ref2: UHeapRef) {
+        if (isContradicting) {
             return
         }
 
@@ -125,7 +125,7 @@ class UEqualityConstraints private constructor(
             mutableReferenceDisequalities.remove(from)
             fromDiseqs.forEach {
                 mutableReferenceDisequalities[it]?.remove(from)
-                addReferenceDisequality(to, it)
+                makeNonEqual(to, it)
             }
         }
 
@@ -142,7 +142,7 @@ class UEqualityConstraints private constructor(
             }
         } else if (containsNullableDisequality(from, to)) {
             // If x === y, nullable disequality can hold only if both references are null
-            addReferenceEquality(to, nullRepr)
+            makeEqual(to, nullRepr)
         } else {
             val removedFrom = mutableNullableDisequalities.remove(from)
             removedFrom?.forEach {
@@ -210,8 +210,8 @@ class UEqualityConstraints private constructor(
     /**
      * Adds an assertion that [ref1] is never equal to [ref2].
      */
-    fun addReferenceDisequality(ref1: UHeapRef, ref2: UHeapRef) {
-        if (isContradiction) {
+    fun makeNonEqual(ref1: UHeapRef, ref2: UHeapRef) {
+        if (isContradicting) {
             return
         }
 
@@ -233,7 +233,7 @@ class UEqualityConstraints private constructor(
      * Adds an assertion that [ref1] is never equal to [ref2] or both are null.
      */
     fun makeNonEqualOrBothNull(ref1: UHeapRef, ref2: UHeapRef) {
-        if (isContradiction) {
+        if (isContradicting) {
             return
         }
 
@@ -242,7 +242,7 @@ class UEqualityConstraints private constructor(
 
         if (repr1 == repr2) {
             // In this case, (repr1 != repr2) || (repr1 == null && repr2 == null) is equivalent to (repr1 == null).
-            addReferenceEquality(repr1, ctx.nullRef)
+            makeEqual(repr1, ctx.nullRef)
             return
         }
 
@@ -284,9 +284,9 @@ class UEqualityConstraints private constructor(
      * Note that current subscribers get unsubscribed!
      */
     fun clone(): UEqualityConstraints {
-        if (isContradiction) {
+        if (isContradicting) {
             val result = UEqualityConstraints(ctx, DisjointSets(), mutableSetOf(), mutableMapOf(), mutableMapOf())
-            result.isContradiction = true
+            result.isContradicting = true
             return result
         }
 

usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt

@@ -41,8 +41,8 @@ open class UPathConstraints<Type> private constructor(
     constructor(ctx: UContext) : this(ctx, persistentSetOf())
 
     open val isFalse: Boolean
-        get() = equalityConstraints.isContradiction ||
-            typeConstraints.isContradiction ||
+        get() = equalityConstraints.isContradicting ||
+            typeConstraints.isContradicting ||
             logicalConstraints.singleOrNull() is UFalse
 
     @Suppress("UNCHECKED_CAST")
@@ -54,9 +54,9 @@ open class UPathConstraints<Type> private constructor(
                 constraint == trueExpr || constraint in logicalConstraints -> {}
 
                 constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) ->
-                    equalityConstraints.addReferenceEquality(constraint.lhs as UHeapRef, constraint.rhs as UHeapRef)
+                    equalityConstraints.makeEqual(constraint.lhs as UHeapRef, constraint.rhs as UHeapRef)
 
-                constraint is UIsExpr<*> -> typeConstraints.cast(constraint.ref, constraint.type as Type)
+                constraint is UIsExpr<*> -> typeConstraints.addSupertype(constraint.ref, constraint.type as Type)
 
                 constraint is UAndExpr -> constraint.args.forEach(::plusAssign)
 
@@ -67,12 +67,17 @@ open class UPathConstraints<Type> private constructor(
                             isSymbolicHeapRef(notConstraint.lhs) &&
                             isSymbolicHeapRef(notConstraint.rhs) -> {
                             require(notConstraint.rhs.sort == addressSort)
-                            equalityConstraints.addReferenceDisequality(
+                            equalityConstraints.makeNonEqual(
                                 notConstraint.lhs as UHeapRef,
                                 notConstraint.rhs as UHeapRef
                             )
                         }
 
+                        notConstraint is UIsExpr<*> -> typeConstraints.excludeSupertype(
+                            notConstraint.ref,
+                            notConstraint.type as Type
+                        )
+
                         notConstraint in logicalConstraints -> contradiction(ctx)
 
                         notConstraint is UOrExpr -> notConstraint.args.forEach { plusAssign(ctx.mkNot(it)) }