diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index 2dccd3f1c6..4342c1fae1 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -44,10 +44,15 @@ open class UComposer( expr: UIndexedMethodReturnValue, ): UExpr = mockEvaluator.eval(expr) - override fun transform(expr: UIsExpr): UBoolExpr = with(expr) { - val composedAddress = compose(ref) - typeEvaluator.evalIs(composedAddress, type) - } + override fun transform(expr: UIsSubtypeExpr): UBoolExpr = + transformExprAfterTransformed(expr, expr.ref) { ref -> + typeEvaluator.evalIsSubtype(ref, expr.supertype) + } + + override fun transform(expr: UIsSupertypeExpr): UBoolExpr = + transformExprAfterTransformed(expr, expr.ref) { ref -> + typeEvaluator.evalIsSupertype(ref, expr.subtype) + } fun , Key, Sort : USort> transformHeapReading( expr: UHeapReading, diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index 2b920cb82a..34207fae05 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -175,11 +175,18 @@ open class UContext( UIndexedMethodReturnValue(this, method.cast(), callIndex, sort) }.cast() - private val isExprCache = mkAstInterner>() - fun mkIsExpr( + private val isSubtypeExprCache = mkAstInterner>() + fun mkIsSubtypeExpr( ref: UHeapRef, type: Type, - ): UIsExpr = isExprCache.createIfContextActive { - UIsExpr(this, ref, type.cast()) + ): UIsSubtypeExpr = isSubtypeExprCache.createIfContextActive { + UIsSubtypeExpr(this, ref, type.cast()) + }.cast() + + private val isSupertypeExprCache = mkAstInterner>() + fun mkIsSupertypeExpr( + ref: UHeapRef, type: Type, + ): UIsSupertypeExpr = isSupertypeExprCache.createIfContextActive { + UIsSupertypeExpr(this, ref, type.cast()) }.cast() fun mkConcreteHeapRefDecl(address: UConcreteHeapAddress): UConcreteHeapRefDecl = diff --git a/usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt b/usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt index 8265749307..affa0e32f9 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ExprTransformer.kt @@ -1,24 +1,31 @@ package org.usvm import io.ksmt.expr.transformer.KNonRecursiveTransformer +import io.ksmt.expr.transformer.KTransformer -abstract class UExprTransformer(ctx: UContext): KNonRecursiveTransformer(ctx) { - abstract fun transform(expr: USymbol): UExpr +interface UTransformer : KTransformer { + fun transform(expr: USymbol): UExpr - abstract fun transform(expr: URegisterReading): UExpr + fun transform(expr: URegisterReading): UExpr - abstract fun transform(expr: UHeapReading<*, *, *>): UExpr - abstract fun transform(expr: UInputFieldReading): UExpr - abstract fun transform(expr: UAllocatedArrayReading): UExpr - abstract fun transform(expr: UInputArrayReading): UExpr - abstract fun transform(expr: UInputArrayLengthReading): USizeExpr + fun transform(expr: UHeapReading<*, *, *>): UExpr + fun transform(expr: UInputFieldReading): UExpr + fun transform(expr: UAllocatedArrayReading): UExpr + fun transform(expr: UInputArrayReading): UExpr + fun transform(expr: UInputArrayLengthReading): USizeExpr - abstract fun transform(expr: UMockSymbol): UExpr - abstract fun transform(expr: UIndexedMethodReturnValue): UExpr + fun transform(expr: UMockSymbol): UExpr + fun transform(expr: UIndexedMethodReturnValue): UExpr - abstract fun transform(expr: UIsExpr): UBoolExpr + fun transform(expr: UIsSubtypeExpr): UBoolExpr - abstract fun transform(expr: UConcreteHeapRef): UExpr + fun transform(expr: UIsSupertypeExpr): UBoolExpr - abstract fun transform(expr: UNullRef): UExpr -} \ No newline at end of file + fun transform(expr: UConcreteHeapRef): UExpr + + fun transform(expr: UNullRef): UExpr +} + +abstract class UExprTransformer( + ctx: UContext +) : KNonRecursiveTransformer(ctx), UTransformer diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index 2a340632ab..a6a195c5ee 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -72,7 +72,7 @@ abstract class USymbol(ctx: UContext) : UExpr(ctx) //region Object References /** - * An expr is of a [UHeapRef] type iff it's a [UConcreteHeapRef], [USymbolicHeapRef] or [UIteExpr] with [UAddressSort]. + * An expr is a [UHeapRef] iff it's a [UConcreteHeapRef], [USymbolicHeapRef] or [UIteExpr] with [UAddressSort]. * [UIteExpr]s have [UConcreteHeapRef]s and [USymbolicHeapRef]s as leafs. */ typealias UHeapRef = UExpr @@ -105,7 +105,7 @@ class UConcreteHeapRef internal constructor( override val sort: UAddressSort = ctx.addressSort override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } return transformer.transform(this) } @@ -125,7 +125,7 @@ class UNullRef internal constructor( get() = uctx.addressSort override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } return transformer.transform(this) } @@ -153,6 +153,7 @@ const val NULL_ADDRESS = 0 * 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]) @@ -191,7 +192,7 @@ class URegisterReading internal constructor( override val sort: Sort, ) : USymbol(ctx) { override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } return transformer.transform(this) } @@ -222,9 +223,9 @@ class UInputFieldReading internal constructor( @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return (transformer as UExprTransformer).transform(this) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer).transform(this) } override fun internEquals(other: Any): Boolean = structurallyEqual(other, { region }, { address }) @@ -246,9 +247,9 @@ class UAllocatedArrayReading internal constructor( ) : UHeapReading, USizeExpr, Sort>(ctx, region) { @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return (transformer as UExprTransformer<*, ArrayType>).transform(this) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer<*, ArrayType>).transform(this) } override fun internEquals(other: Any): Boolean = @@ -280,9 +281,9 @@ class UInputArrayReading internal constructor( @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return (transformer as UExprTransformer<*, ArrayType>).transform(this) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer<*, ArrayType>).transform(this) } override fun internEquals(other: Any): Boolean = @@ -316,9 +317,9 @@ class UInputArrayLengthReading internal constructor( @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): USizeExpr { - require(transformer is UExprTransformer<*, *>) - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return (transformer as UExprTransformer<*, ArrayType>).transform(this) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer<*, ArrayType>).transform(this) } override fun internEquals(other: Any): Boolean = structurallyEqual(other, { region }, { address }) @@ -347,7 +348,7 @@ class UIndexedMethodReturnValue internal constructor( override val sort: Sort, ) : UMockSymbol(ctx, sort) { override fun accept(transformer: KTransformerBase): KExpr { - require(transformer is UExprTransformer<*, *>) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } return transformer.transform(this) } @@ -364,33 +365,63 @@ class UIndexedMethodReturnValue 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 internal constructor( +abstract class UIsExpr internal constructor( ctx: UContext, val ref: UHeapRef, - val type: Type, ) : USymbol(ctx) { - override val sort = ctx.boolSort + final override val sort = ctx.boolSort +} +/** + * Means **either** [ref] is [UNullRef] **or** [ref] !is [UNullRef] and [ref] <: [supertype]. Thus, the actual type + * inheritance is checked only on non-null refs. + */ +class UIsSubtypeExpr internal constructor( + ctx: UContext, + ref: UHeapRef, + val supertype: Type, +) : UIsExpr(ctx, ref) { @Suppress("UNCHECKED_CAST") override fun accept(transformer: KTransformerBase): UBoolExpr { - require(transformer is UExprTransformer<*, *>) - // An unchecked cast here it to be able to choose the right overload from UExprTransformer - return (transformer as UExprTransformer<*, Type>).transform(this) + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer<*, Type>).transform(this) + } + + override fun print(printer: ExpressionPrinter) { + printer.append("($ref is $supertype)") } + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { ref }, { supertype }) + + override fun internHashCode(): Int = hash(ref, supertype) +} + +/** + * Means [ref] !is [UNullRef] and [subtype] <: [ref]. Thus, the actual type + * inheritance is checked only on non-null refs. + */ +class UIsSupertypeExpr internal constructor( + ctx: UContext, + ref: UHeapRef, + val subtype: Type, +) : UIsExpr(ctx, ref) { + @Suppress("UNCHECKED_CAST") + override fun accept(transformer: KTransformerBase): UBoolExpr { + require(transformer is UTransformer<*, *>) { "Expected a UTransformer, but got: $transformer" } + // An unchecked cast here it to be able to choose the right overload from UTransformer + return (transformer as UTransformer<*, Type>).transform(this) + } override fun print(printer: ExpressionPrinter) { - printer.append("($ref instance of $type)") + printer.append("($subtype is subtype of type($ref))") } - override fun internEquals(other: Any): Boolean = structurallyEqual(other, { ref }, { type }) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { ref }, { subtype }) - override fun internHashCode(): Int = hash(ref, type) + override fun internHashCode(): Int = hash(ref, subtype) } + //endregion //region Utils diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index e65ff50ad1..ce577ab78a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/State.kt +++ b/usvm-core/src/main/kotlin/org/usvm/State.kt @@ -81,7 +81,7 @@ private fun , Type, Field> forkIfSat( newConstraintToOriginalState } val solver = newConstraintToForkedState.uctx.solver() - val satResult = solver.check(constraintsToCheck, useSoftConstraints = true) + val satResult = solver.checkWithSoftConstraints(constraintsToCheck) return when (satResult) { is UUnsatResult -> null diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt index 04e8280fda..00526d8a0f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt @@ -1,36 +1,37 @@ package org.usvm.constraints import org.usvm.UContext -import org.usvm.UHeapRef +import org.usvm.USymbolicHeapRef import org.usvm.util.DisjointSets /** - * Represents equality constraints between heap references. There are three kinds of constraints: + * Represents equality constraints between symbolic heap references. There are three kinds of constraints: * - Equalities represented as collection of equivalence classes in union-find data structure [equalReferences]. * - Disequalities: [referenceDisequalities].get(x).contains(y) means that x !== y. * - Nullable disequalities: [nullableDisequalities].get(x).contains(y) means that x !== y || (x == null && y == null). * - * Maintains graph of disequality constraints. Tries to detect (or at least approximate) maximal set of distinct heap references - * by fast-check of clique in disequality graph (not exponential!) (see [distinctReferences]). + * Maintains graph of disequality constraints. Tries to detect (or at least approximate) maximal set of distinct + * symbolic heap references by fast-check of clique in disequality graph (not exponential!) (see [distinctReferences]). * All the rest disequalities (i.e., outside of the maximal clique) are stored into [referenceDisequalities]. * * Important invariant: [distinctReferences], [referenceDisequalities] and [nullableDisequalities] include - * *only* representatives of reference equivalence classes, i.e. only references x such that [equalReferences].find(x) == x. + * *only* representatives of reference equivalence classes, i.e. only references x, + * such that [equalReferences].find(x) == x. */ class UEqualityConstraints private constructor( private val ctx: UContext, - val equalReferences: DisjointSets, - private val mutableDistinctReferences: MutableSet, - private val mutableReferenceDisequalities: MutableMap>, - private val mutableNullableDisequalities: MutableMap>, + val equalReferences: DisjointSets, + private val mutableDistinctReferences: MutableSet, + private val mutableReferenceDisequalities: MutableMap>, + private val mutableNullableDisequalities: MutableMap>, ) { constructor(ctx: UContext) : this(ctx, DisjointSets(), mutableSetOf(ctx.nullRef), mutableMapOf(), mutableMapOf()) - val distinctReferences: Set = mutableDistinctReferences + val distinctReferences: Set = mutableDistinctReferences - val referenceDisequalities: Map> = mutableReferenceDisequalities + val referenceDisequalities: Map> = mutableReferenceDisequalities - val nullableDisequalities: Map> = mutableNullableDisequalities + val nullableDisequalities: Map> = mutableNullableDisequalities init { equalReferences.subscribe(::rename) @@ -46,24 +47,24 @@ class UEqualityConstraints private constructor( mutableReferenceDisequalities.clear() } - private fun containsReferenceDisequality(ref1: UHeapRef, ref2: UHeapRef) = + private fun containsReferenceDisequality(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) = referenceDisequalities[ref1]?.contains(ref2) ?: false - private fun containsNullableDisequality(ref1: UHeapRef, ref2: UHeapRef) = + private fun containsNullableDisequality(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) = nullableDisequalities[ref1]?.contains(ref2) ?: false /** * Returns if [ref1] is identical to [ref2] in *all* models. */ - internal fun areEqual(ref1: UHeapRef, ref2: UHeapRef) = + internal fun areEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) = equalReferences.connected(ref1, ref2) /** * Returns if [ref] is null in all models. */ - internal fun isNull(ref: UHeapRef) = areEqual(ctx.nullRef, ref) + internal fun isNull(ref: USymbolicHeapRef) = areEqual(ctx.nullRef, ref) - private fun areDistinctRepresentatives(repr1: UHeapRef, repr2: UHeapRef): Boolean { + private fun areDistinctRepresentatives(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef): Boolean { if (repr1 == repr2) { return false } @@ -75,7 +76,7 @@ class UEqualityConstraints private constructor( /** * Returns if [ref1] is distinct from [ref2] in *all* models. */ - internal fun areDistinct(ref1: UHeapRef, ref2: UHeapRef): Boolean { + internal fun areDistinct(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef): Boolean { val repr1 = equalReferences.find(ref1) val repr2 = equalReferences.find(ref2) return areDistinctRepresentatives(repr1, repr2) @@ -84,12 +85,12 @@ class UEqualityConstraints private constructor( /** * Returns if [ref] is not null in all models. */ - internal fun isNotNull(ref: UHeapRef) = areDistinct(ctx.nullRef, ref) + internal fun isNotNull(ref: USymbolicHeapRef) = areDistinct(ctx.nullRef, ref) /** * Adds an assertion that [ref1] is always equal to [ref2]. */ - internal fun makeEqual(ref1: UHeapRef, ref2: UHeapRef) { + internal fun makeEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) { if (isContradicting) { return } @@ -104,7 +105,7 @@ class UEqualityConstraints private constructor( * Here we react to merging of equivalence classes of [from] and [to] into one represented by [to], by eliminating * [from] and merging its disequality constraints into [to]. */ - private fun rename(to: UHeapRef, from: UHeapRef) { + private fun rename(to: USymbolicHeapRef, from: USymbolicHeapRef) { if (distinctReferences.contains(from)) { if (distinctReferences.contains(to)) { contradiction() @@ -152,7 +153,7 @@ class UEqualityConstraints private constructor( } } - private fun addDisequalityUnguarded(repr1: UHeapRef, repr2: UHeapRef) { + private fun addDisequalityUnguarded(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef) { when (distinctReferences.size) { 0 -> { require(referenceDisequalities.isEmpty()) @@ -210,7 +211,7 @@ class UEqualityConstraints private constructor( /** * Adds an assertion that [ref1] is never equal to [ref2]. */ - internal fun makeNonEqual(ref1: UHeapRef, ref2: UHeapRef) { + internal fun makeNonEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) { if (isContradicting) { return } @@ -232,7 +233,7 @@ class UEqualityConstraints private constructor( /** * Adds an assertion that [ref1] is never equal to [ref2] or both are null. */ - internal fun makeNonEqualOrBothNull(ref1: UHeapRef, ref2: UHeapRef) { + internal fun makeNonEqualOrBothNull(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) { if (isContradicting) { return } @@ -262,7 +263,7 @@ class UEqualityConstraints private constructor( (mutableNullableDisequalities.getOrPut(repr2) { mutableSetOf() }).add(repr1) } - private fun removeNullableDisequality(repr1: UHeapRef, repr2: UHeapRef) { + private fun removeNullableDisequality(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef) { if (containsNullableDisequality(repr1, repr2)) { mutableNullableDisequalities[repr1]?.remove(repr2) mutableNullableDisequalities[repr2]?.remove(repr1) @@ -275,7 +276,7 @@ class UEqualityConstraints private constructor( * [equalityCallback] (x, y) is called. * Note that the order of arguments matters: the first argument is a representative of the new equivalence class. */ - fun subscribe(equalityCallback: (UHeapRef, UHeapRef) -> Unit) { + fun subscribe(equalityCallback: (USymbolicHeapRef, USymbolicHeapRef) -> Unit) { equalReferences.subscribe(equalityCallback) } @@ -292,8 +293,8 @@ class UEqualityConstraints private constructor( val newEqualReferences = equalReferences.clone() val newDistinctReferences = distinctReferences.toMutableSet() - val newReferenceDisequalities = mutableMapOf>() - val newNullableDisequalities = mutableMapOf>() + val newReferenceDisequalities = mutableMapOf>() + val newNullableDisequalities = mutableMapOf>() referenceDisequalities.mapValuesTo(newReferenceDisequalities) { it.value.toMutableSet() } nullableDisequalities.mapValuesTo(newNullableDisequalities) { it.value.toMutableSet() } diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt index 159056ce2f..c9133229fa 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -7,12 +7,12 @@ import org.usvm.UBoolExpr import org.usvm.UContext import org.usvm.UEqExpr import org.usvm.UFalse -import org.usvm.UHeapRef -import org.usvm.UIsExpr +import org.usvm.UIsSubtypeExpr +import org.usvm.UIsSupertypeExpr import org.usvm.UNotExpr import org.usvm.UOrExpr +import org.usvm.USymbolicHeapRef import org.usvm.isSymbolicHeapRef -import org.usvm.memory.map import org.usvm.uctx /** @@ -55,20 +55,14 @@ open class UPathConstraints private constructor( constraint == trueExpr || constraint in logicalConstraints -> {} constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) -> - equalityConstraints.makeEqual(constraint.lhs as UHeapRef, constraint.rhs as UHeapRef) - - constraint is UIsExpr<*> -> { - val expr = constraint.ref.map( - concreteMapper = { typeConstraints.evalIs(it, constraint.type as Type) }, - symbolicMapper = { if (it == nullRef) trueExpr else ctx.mkIsExpr(it, constraint.type) }, - ignoreNullRefs = false - ) - - if (expr is UIsExpr<*>) { - typeConstraints.addSupertype(expr.ref, expr.type as Type) - } else { - logicalConstraints = logicalConstraints.add(expr) - } + equalityConstraints.makeEqual(constraint.lhs as USymbolicHeapRef, constraint.rhs as USymbolicHeapRef) + + constraint is UIsSubtypeExpr<*> -> { + typeConstraints.addSupertype(constraint.ref, constraint.supertype as Type) + } + + constraint is UIsSupertypeExpr<*> -> { + typeConstraints.addSubtype(constraint.ref, constraint.subtype as Type) } constraint is UAndExpr -> constraint.args.forEach(::plusAssign) @@ -81,14 +75,19 @@ open class UPathConstraints private constructor( isSymbolicHeapRef(notConstraint.rhs) -> { require(notConstraint.rhs.sort == addressSort) equalityConstraints.makeNonEqual( - notConstraint.lhs as UHeapRef, - notConstraint.rhs as UHeapRef + notConstraint.lhs as USymbolicHeapRef, + notConstraint.rhs as USymbolicHeapRef ) } - notConstraint is UIsExpr<*> -> typeConstraints.excludeSupertype( + notConstraint is UIsSubtypeExpr<*> -> typeConstraints.excludeSupertype( + notConstraint.ref, + notConstraint.supertype as Type + ) + + notConstraint is UIsSupertypeExpr<*> -> typeConstraints.excludeSubtype( notConstraint.ref, - notConstraint.type as Type + notConstraint.subtype as Type ) notConstraint in logicalConstraints -> contradiction(ctx) diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt index 5c82ea737a..99d243ee7e 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt @@ -1,6 +1,5 @@ package org.usvm.constraints -import org.usvm.NULL_ADDRESS import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UConcreteHeapRef @@ -8,11 +7,6 @@ import org.usvm.UHeapRef import org.usvm.UNullRef import org.usvm.USymbolicHeapRef import org.usvm.memory.map -import org.usvm.model.UModel -import org.usvm.model.UTypeModel -import org.usvm.solver.USatResult -import org.usvm.solver.USolverResult -import org.usvm.solver.UUnsatResult import org.usvm.types.USingleTypeStream import org.usvm.types.UTypeRegion import org.usvm.types.UTypeStream @@ -20,7 +14,8 @@ import org.usvm.types.UTypeSystem import org.usvm.uctx interface UTypeEvaluator { - fun evalIs(ref: UHeapRef, type: Type): UBoolExpr + fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr + fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr } /** @@ -40,12 +35,16 @@ class UTypeConstraints( private val typeSystem: UTypeSystem, private val equalityConstraints: UEqualityConstraints, private val concreteRefToType: MutableMap = mutableMapOf(), - private val symbolicRefToTypeRegion: MutableMap> = mutableMapOf(), + symbolicRefToTypeRegion: MutableMap> = mutableMapOf(), ) : UTypeEvaluator { init { - equalityConstraints.subscribe(::intersectConstraints) + equalityConstraints.subscribe(::intersectRegions) } + val symbolicRefToTypeRegion get(): Map> = _symbolicRefToTypeRegion + + private val _symbolicRefToTypeRegion = symbolicRefToTypeRegion + /** * Returns true if the current type and equality constraints are unsatisfiable (syntactically). */ @@ -70,51 +69,46 @@ class UTypeConstraints( concreteRefToType[ref] = type } - private operator fun get(symbolicRef: UHeapRef) = - symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] ?: topTypeRegion + /** + * @param useRepresentative use the representive from the [equalityConstraints] for the [symbolicRef]. The false + * value used, when we intersect regions on their refs union. + * @see intersectRegions + */ + private fun getTypeRegion(symbolicRef: USymbolicHeapRef, useRepresentative: Boolean = true): UTypeRegion { + val representative = if (useRepresentative) { + equalityConstraints.equalReferences.find(symbolicRef) + } else { + symbolicRef + } + return _symbolicRefToTypeRegion[representative] ?: topTypeRegion + } - private operator fun set(symbolicRef: UHeapRef, value: UTypeRegion) { - symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] = value + private fun setTypeRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion) { + _symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] = value } /** * Constraints **either** the [ref] is null **or** the [ref] isn't null and the type of the [ref] to - * be a subtype of the [type]. If it is impossible within current type and equality constraints, + * be a subtype of the [supertype]. If it is impossible within current type and equality constraints, * then type constraints become contradicting (@see [isContradicting]). * * NB: this function **must not** be used to cast types in interpreters. - * To do so you should add corresponding constraint using [evalIs] function. + * To do so you should add corresponding constraint using [evalIsSubtype] function. */ - internal fun addSupertype(ref: UHeapRef, type: Type) { + internal fun addSupertype(ref: UHeapRef, supertype: Type) { when (ref) { is UNullRef -> return is UConcreteHeapRef -> { val concreteType = concreteRefToType.getValue(ref.address) - if (!typeSystem.isSupertype(type, concreteType)) { + if (!typeSystem.isSupertype(supertype, concreteType)) { contradiction() } } is USymbolicHeapRef -> { - val constraints = this[ref] - val newConstraints = constraints.addSupertype(type) - if (newConstraints.isContradicting) { - // the only left option here is to be equal to null - equalityConstraints.makeEqual(ref, ref.uctx.nullRef) - } else { - // Inferring new symbolic disequalities here - for ((key, value) in symbolicRefToTypeRegion.entries) { - // TODO: cache intersections? - if (key != ref && value.intersect(newConstraints).isEmpty) { - // If we have two inputs of incomparable reference types, then they are either non equal, - // or both nulls - equalityConstraints.makeNonEqualOrBothNull(ref, key) - } - } - this[ref] = newConstraints - } + updateRegionCanBeEqualNull(ref) { it.addSupertype(supertype) } } else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref") @@ -122,44 +116,83 @@ class UTypeConstraints( } /** - * Constraints **both** the type of the [ref] to be a not subtype of the [type] and the [ref] not equals null. + * Constraints **both** the type of the [ref] to be a not subtype of the [supertype] and the [ref] not equals null. * If it is impossible within current type and equality constraints, * then type constraints become contradicting (@see [isContradicting]). * * NB: this function **must not** be used to exclude types in interpreters. - * To do so you should add corresponding constraint using [evalIs] function. + * To do so you should add corresponding constraint using [evalIsSubtype] function. */ - internal fun excludeSupertype(ref: UHeapRef, type: Type) { + internal fun excludeSupertype(ref: UHeapRef, supertype: Type) { when (ref) { is UNullRef -> contradiction() // the [ref] can't be equal to null is UConcreteHeapRef -> { val concreteType = concreteRefToType.getValue(ref.address) - if (typeSystem.isSupertype(type, concreteType)) { + if (typeSystem.isSupertype(supertype, concreteType)) { contradiction() } } is USymbolicHeapRef -> { - val constraints = this[ref] - val newConstraints = constraints.excludeSupertype(type) - equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef) - if (newConstraints.isContradicting || equalityConstraints.isContradicting) { - // the [ref] can't be equal to null + updateRegionCannotBeEqualNull(ref) { it.excludeSupertype(supertype) } + } + + else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref") + } + } + + /** + * Constraints the [ref] isn't null and the type of the [ref] to + * be a supertype of the [subtype]. If it is impossible within current type and equality constraints, + * then type constraints become contradicting (@see [isContradicting]). + * + * NB: this function **must not** be used to cast types in interpreters. + * To do so you should add corresponding constraint using [evalIsSupertype] function. + */ + internal fun addSubtype(ref: UHeapRef, subtype: Type) { + when (ref) { + is UNullRef -> contradiction() + + is UConcreteHeapRef -> { + val concreteType = concreteRefToType.getValue(ref.address) + if (!typeSystem.isSupertype(concreteType, subtype)) { + contradiction() + } + } + + is USymbolicHeapRef -> { + updateRegionCannotBeEqualNull(ref) { it.addSubtype(subtype) } + } + + else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref") + } + } + + /** + * Constraints **either** the [ref] is null or the [ref] isn't null and the type of + * the [ref] to be a not supertype of the [subtype]. + * If it is impossible within current type and equality constraints, + * then type constraints become contradicting (@see [isContradicting]). + * + * NB: this function **must not** be used to exclude types in interpreters. + * To do so you should add corresponding constraint using [evalIsSupertype] function. + */ + internal fun excludeSubtype(ref: UHeapRef, subtype: Type) { + when (ref) { + is UNullRef -> return + + is UConcreteHeapRef -> { + val concreteType = concreteRefToType.getValue(ref.address) + if (typeSystem.isSupertype(concreteType, subtype)) { contradiction() - } else { - // Inferring new symbolic disequalities here - for ((key, value) in symbolicRefToTypeRegion.entries) { - // TODO: cache intersections? - if (key != ref && value.intersect(newConstraints).isEmpty) { - // If we have two inputs of incomparable reference types, then they are non equal - equalityConstraints.makeNonEqual(ref, key) - } - } - this[ref] = newConstraints } } + is USymbolicHeapRef -> { + updateRegionCanBeEqualNull(ref) { it.excludeSubtype(subtype) } + } + else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref") } } @@ -167,7 +200,7 @@ class UTypeConstraints( /** * @return a type stream corresponding to the [ref]. */ - internal fun readTypeStream(ref: UHeapRef): UTypeStream = + internal fun getTypeStream(ref: UHeapRef): UTypeStream = when (ref) { is UConcreteHeapRef -> { val concreteType = concreteRefToType[ref.address] @@ -180,21 +213,73 @@ class UTypeConstraints( } is UNullRef -> error("Null ref should be handled explicitly earlier") - else -> this[ref].typeStream + + is USymbolicHeapRef -> { + getTypeRegion(ref).typeStream + } + + else -> error("Unexpected ref: $ref") } - private fun intersectConstraints(ref1: UHeapRef, ref2: UHeapRef) { - this[ref1] = this[ref1].intersect(this[ref2]) + private fun intersectRegions(to: USymbolicHeapRef, from: USymbolicHeapRef) { + val region = getTypeRegion(from, useRepresentative = false).intersect(getTypeRegion(to)) + updateRegionCanBeEqualNull(to, region::intersect) + } + + private fun updateRegionCannotBeEqualNull( + ref: USymbolicHeapRef, + regionMapper: (UTypeRegion) -> UTypeRegion, + ) { + val region = getTypeRegion(ref) + val newRegion = regionMapper(region) + if (newRegion == region) { + return + } + equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef) + if (newRegion.isEmpty || equalityConstraints.isContradicting) { + contradiction() + return + } + for ((key, value) in _symbolicRefToTypeRegion.entries) { + // TODO: cache intersections? + if (key != ref && value.intersect(newRegion).isEmpty) { + // If we have two inputs of incomparable reference types, then they are non equal + equalityConstraints.makeNonEqual(ref, key) + } + } + setTypeRegion(ref, newRegion) + } + + private fun updateRegionCanBeEqualNull( + ref: USymbolicHeapRef, + regionMapper: (UTypeRegion) -> UTypeRegion, + ) { + val region = getTypeRegion(ref) + val newRegion = regionMapper(region) + if (newRegion == region) { + return + } + if (newRegion.isEmpty) { + equalityConstraints.makeEqual(ref, ref.uctx.nullRef) + } + for ((key, value) in _symbolicRefToTypeRegion.entries) { + // TODO: cache intersections? + if (key != ref && value.intersect(newRegion).isEmpty) { + // If we have two inputs of incomparable reference types, then they are non equal or both null + equalityConstraints.makeNonEqualOrBothNull(ref, key) + } + } + setTypeRegion(ref, newRegion) } /** - * Evaluates the [ref] <: [type] in the current [UTypeConstraints]. Always returns true on null references. + * Evaluates the [ref] <: [supertype] in the current [UTypeConstraints]. Always returns true on null references. */ - override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr = + override fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr = ref.map( concreteMapper = { concreteRef -> val concreteType = concreteRefToType.getValue(concreteRef.address) - if (typeSystem.isSupertype(type, concreteType)) { + if (typeSystem.isSupertype(supertype, concreteType)) { concreteRef.ctx.trueExpr } else { concreteRef.ctx.falseExpr @@ -202,20 +287,45 @@ class UTypeConstraints( }, symbolicMapper = mapper@{ symbolicRef -> if (symbolicRef == symbolicRef.uctx.nullRef) { - // accordingly to the [UIsExpr] specification, [nullRef] always satisfies the [type] + // accordingly to the [UIsSubtypeExpr] specification, [nullRef] always satisfies the [type] return@mapper symbolicRef.ctx.trueExpr } - val typeRegion = this[symbolicRef] + val typeRegion = getTypeRegion(symbolicRef) - if (typeRegion.addSupertype(type).isContradicting) { + if (typeRegion.addSupertype(supertype).isEmpty) { symbolicRef.ctx.falseExpr } else { - symbolicRef.uctx.mkIsExpr(symbolicRef, type) + symbolicRef.uctx.mkIsSubtypeExpr(symbolicRef, supertype) } }, ignoreNullRefs = false ) + override fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr = + ref.map( + concreteMapper = { concreteRef -> + val concreteType = concreteRefToType.getValue(concreteRef.address) + if (typeSystem.isSupertype(concreteType, subtype)) { + concreteRef.ctx.trueExpr + } else { + concreteRef.ctx.falseExpr + } + }, + symbolicMapper = mapper@{ symbolicRef -> + if (symbolicRef == symbolicRef.uctx.nullRef) { + // accordingly to the [UIsSupertypeExpr] specification, on [nullRef] return false + return@mapper symbolicRef.ctx.falseExpr + } + val typeRegion = getTypeRegion(symbolicRef) + + if (typeRegion.addSubtype(subtype).isEmpty) { + symbolicRef.ctx.falseExpr + } else { + symbolicRef.uctx.mkIsSupertypeExpr(symbolicRef, subtype) + } + }, + ignoreNullRefs = false + ) /** * Creates a mutable copy of these constraints connected to new instance of [equalityConstraints]. @@ -225,124 +335,6 @@ class UTypeConstraints( typeSystem, equalityConstraints, concreteRefToType.toMutableMap(), - symbolicRefToTypeRegion.toMutableMap() + _symbolicRefToTypeRegion.toMutableMap() ) - - /** - * Checks if the [model] satisfies this [UTypeConstraints]. - * - * Checking works as follows: - * 1. Groups symbolic references into clusters by their concrete interpretation in the [model] and filters out nulls - * 2. For each cluster processes symbolic references one by one and intersects their type regions - * 3. If the current region became empty, then we found a conflicting group, so add reference disequality - * 4. If no conflicting references were found, builds a type model - * - * Example: - * ``` - * a <: T1 | T2 - * b <: T2 | T3 - * c <: T3 | T1 - * d <: T1 | T2 - * e <: T2 - * cluster: (a, b, c, d, e) - * ``` - * Suppose we have the single cluster, so we process it as follows: - * - * 1. Peek `a`. The current region is empty, so it becomes `T1 | T2`. Potential conflicting refs = `{a}`. - * 2. Peek `b`. The current region becomes `T2`. Potential conflicting refs = `{a, b}`. - * 3. Peek `c`. The intersection of the current region with `T3 | T1` is empty, so we add the following constraint: - * `a != c || b != c || a == null || b == null || c == null`. The region becomes `T3 | T1`. - * Potential conflicting refs = `{c}. - * 4. Peek `d`. The current region becomes `T1`. Potential conflicting refs = `{c, d}`. - * 5. Peek `e`. The intersection of the current region with `T2` is empty, so we add the following constraint: - * `c != e || d != e || c == null || d == null || e == null`. - * - * @return The result of verification: - * * [UTypeModel] if the [model] satisfies this [UTypeConstraints] - * * [UUnsatResult] if no model satisfying this [UTypeConstraints] exists - * * [UTypeUnsatResult] with reference disequalities constraints if the [model] - * doesn't satisfy this [UTypeConstraints], but other model may satisfy - */ - internal fun verify(model: UModel): USolverResult> { - // firstly, group symbolic references by their interpretations in the [model] - val concreteRefToTypeRegions = symbolicRefToTypeRegion - .entries - .groupBy { (key, _) -> (model.eval(key) as UConcreteHeapRef).address } - .filter { it.key != NULL_ADDRESS } // we don't want to evaluate types of nulls - - val bannedRefEqualities = mutableListOf() - - // then for each group check conflicting types - val concreteToRegionWithCluster = concreteRefToTypeRegions.mapValues { (_, cluster) -> - var currentRegion: UTypeRegion? = null - val potentialConflictingRefs = mutableListOf() - - for ((heapRef, region) in cluster) { - if (currentRegion == null) { // process the first element - currentRegion = region - potentialConflictingRefs.add(heapRef) - } else { - var nextRegion = currentRegion.intersect(region) // add [heapRef] to the current region - if (nextRegion.isEmpty) { - // conflict detected, so it's impossible for [potentialConflictingRefs] - // to have the common type with [heapRef], therefore they can't be equal or - // some of them equals null - val disjunct = mutableListOf() - with(heapRef.uctx) { - // can't be equal to heapRef - potentialConflictingRefs.mapTo(disjunct) { it.neq(heapRef) } - // some of them is null - potentialConflictingRefs.mapTo(disjunct) { it.eq(nullRef) } - disjunct += heapRef.eq(nullRef) - } - bannedRefEqualities += heapRef.ctx.mkOr(disjunct) - - // start a new group - nextRegion = region - potentialConflictingRefs.clear() - potentialConflictingRefs.add(heapRef) - } else if (nextRegion == region) { - // the current [heapRef] gives the same region as the potentialConflictingRefs, so it's better - // to keep only the [heapRef] to minimize the disequalities amount in the result disjunction - potentialConflictingRefs.clear() - potentialConflictingRefs.add(heapRef) - } else if (nextRegion != currentRegion) { - // no conflict detected, but the current region became smaller - potentialConflictingRefs.add(heapRef) - } - - currentRegion = nextRegion - } - } - checkNotNull(currentRegion) - - currentRegion to cluster - } - - // if there were some conflicts, return constraints on reference equalities - if (bannedRefEqualities.isNotEmpty()) { - return UTypeUnsatResult(bannedRefEqualities) - } - - // otherwise, return the type assignment - val allConcreteRefToType = concreteToRegionWithCluster.mapValues { (_, regionToCluster) -> - val (region, cluster) = regionToCluster - val typeStream = region.typeStream - if (typeStream.isEmpty) { - // the only way to reach here is when some of the clusters consists of a single reference - // because if the cluster is bigger, then we called region.isEmpty previously at least once - check(cluster.size == 1) - return UUnsatResult() - } - - typeStream - } - - val typeModel = UTypeModel(typeSystem, allConcreteRefToType) - return USatResult(typeModel) - } } - -class UTypeUnsatResult( - val referenceDisequalitiesDisjuncts: List, -) : UUnsatResult>() diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt index 61278fe7ca..150408ce78 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt @@ -162,5 +162,5 @@ open class UMemoryBase( UMemoryBase(ctx, typeConstraints, stack.clone(), heap.toMutableHeap(), mocker) override fun typeStreamOf(ref: UHeapRef): UTypeStream = - types.readTypeStream(ref) + types.getTypeStream(ref) } diff --git a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt index 8af8d64149..673d1b88f8 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt @@ -24,7 +24,6 @@ fun buildTranslatorAndLazyDecoder( ctx: UContext, ): Pair, ULazyModelDecoder> { val translator = UExprTranslator(ctx) - val decoder = ULazyModelDecoder(translator) return translator to decoder diff --git a/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt index 6cc7ce92d1..ec5d8dbbec 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt @@ -117,7 +117,7 @@ class ULazyHeapModel( // All the expressions in the model are interpreted, therefore, they must // have concrete addresses. Moreover, the model knows only about input values // which have addresses less or equal than INITIAL_INPUT_ADDRESS - require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) + require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } val resolvedRegion = resolvedInputFields[field] val regionId = UInputFieldId(field, sort, contextHeap = null) @@ -142,7 +142,7 @@ class ULazyHeapModel( // All the expressions in the model are interpreted, therefore, they must // have concrete addresses. Moreover, the model knows only about input values // which have addresses less or equal than INITIAL_INPUT_ADDRESS - require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) + require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } val key = ref to index @@ -164,7 +164,7 @@ class ULazyHeapModel( // All the expressions in the model are interpreted, therefore, they must // have concrete addresses. Moreover, the model knows only about input values // which have addresses less or equal than INITIAL_INPUT_ADDRESS - require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) + require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } val resolvedRegion = resolvedInputLengths[arrayType] val regionId = UInputArrayLengthId(arrayType, ref.uctx.sizeSort, contextHeap = null) diff --git a/usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt b/usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt index 2369ff30e1..66dc0d3a27 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt @@ -19,7 +19,7 @@ class UTypeModel( fun typeStream(ref: UConcreteHeapRef): UTypeStream = typeStreamByAddr[ref.address] ?: typeSystem.topTypeStream() - override fun evalIs(ref: UHeapRef, type: Type): UBoolExpr = + override fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr = when { ref is UConcreteHeapRef && ref.address == NULL_ADDRESS -> ref.ctx.trueExpr @@ -27,10 +27,33 @@ class UTypeModel( // All the expressions in the model are interpreted, therefore, they must // have concrete addresses. Moreover, the model knows only about input values // which have addresses less or equal than INITIAL_INPUT_ADDRESS - require(ref.address <= INITIAL_INPUT_ADDRESS) + require(ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } val evaluatedTypeStream = typeStream(ref) - val typeStream = evaluatedTypeStream.filterBySupertype(type) + val typeStream = evaluatedTypeStream.filterBySupertype(supertype) + if (!typeStream.isEmpty) { + typeStreamByAddr[ref.address] = typeStream + ref.ctx.trueExpr + } else { + ref.ctx.falseExpr + } + } + + else -> error("Expecting concrete ref, but got $ref") + } + + override fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr = + when { + ref is UConcreteHeapRef && ref.address == NULL_ADDRESS -> ref.ctx.falseExpr + + ref is UConcreteHeapRef -> { + // All the expressions in the model are interpreted, therefore, they must + // have concrete addresses. Moreover, the model knows only about input values + // which have addresses less or equal than INITIAL_INPUT_ADDRESS + require(ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } + + val evaluatedTypeStream = typeStream(ref) + val typeStream = evaluatedTypeStream.filterBySubtype(subtype) if (!typeStream.isEmpty) { typeStreamByAddr[ref.address] = typeStream ref.ctx.trueExpr diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt index 7804c81d24..89e28a0ab4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt @@ -1,5 +1,6 @@ package org.usvm.solver +import io.ksmt.decl.KDecl import io.ksmt.expr.KExpr import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArraySort @@ -7,6 +8,7 @@ import io.ksmt.sort.KBoolSort import io.ksmt.utils.mkConst import org.usvm.UAddressSort import org.usvm.UAllocatedArrayReading +import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr @@ -18,6 +20,8 @@ import org.usvm.UInputArrayLengthReading import org.usvm.UInputArrayReading import org.usvm.UInputFieldReading import org.usvm.UIsExpr +import org.usvm.UIsSubtypeExpr +import org.usvm.UIsSupertypeExpr import org.usvm.UMockSymbol import org.usvm.UNullRef import org.usvm.URegisterReading @@ -25,6 +29,7 @@ import org.usvm.USizeExpr import org.usvm.USizeSort import org.usvm.USort import org.usvm.USymbol +import org.usvm.USymbolicHeapRef import org.usvm.memory.UAllocatedArrayId import org.usvm.memory.UInputArrayId import org.usvm.memory.UInputArrayLengthId @@ -71,8 +76,26 @@ open class UExprTranslator( override fun transform(expr: UConcreteHeapRef): KExpr = error("Unexpected UConcreteHeapRef $expr in UExprTranslator, that has to be impossible by construction!") - override fun transform(expr: UIsExpr): KExpr = - error("Unexpected UIsExpr $expr in UExprTranslator, that has to be impossible by construction!") + private val _declToIsExpr = mutableMapOf, UIsExpr>() + val declToIsExpr: Map, UIsExpr> get() = _declToIsExpr + + override fun transform(expr: UIsSubtypeExpr): KExpr { + require(expr.ref is USymbolicHeapRef) { "Unexpected ref: ${expr.ref}" } + + val const = expr.sort.mkConst("isSubtype#${_declToIsExpr.size}") + // we need to track declarations to pass them to the type solver in the DPLL(T) procedure + _declToIsExpr[const.decl] = expr + return const + } + + override fun transform(expr: UIsSupertypeExpr): KExpr { + require(expr.ref is USymbolicHeapRef) { "Unexpected ref: ${expr.ref}" } + + val const = expr.sort.mkConst("isSupertype#${_declToIsExpr.size}") + // we need to track declarations to pass them to the type solver in the DPLL(T) procedure + _declToIsExpr[const.decl] = expr + return const + } override fun transform(expr: UInputArrayLengthReading): KExpr = transformExprAfterTransformed(expr, expr.address) { address -> diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt index 15f9ac9dd9..bcd88614fc 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt @@ -2,13 +2,15 @@ package org.usvm.solver import io.ksmt.solver.KSolver import io.ksmt.solver.KSolverStatus +import io.ksmt.utils.asExpr import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UHeapRef import org.usvm.constraints.UEqualityConstraints import org.usvm.constraints.UPathConstraints -import org.usvm.constraints.UTypeUnsatResult import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.memory.UMemoryBase import org.usvm.model.UModelBase import org.usvm.model.UModelDecoder @@ -23,17 +25,18 @@ open class UUnsatResult : USolverResult open class UUnknownResult : USolverResult -abstract class USolver : AutoCloseable { - abstract fun check(pc: PathCondition, useSoftConstraints: Boolean): USolverResult +abstract class USolver { + abstract fun check(query: Query): USolverResult } open class USolverBase( protected val ctx: UContext, protected val smtSolver: KSolver<*>, + protected val typeSolver: UTypeSolver, protected val translator: UExprTranslator, protected val decoder: UModelDecoder, UModelBase>, protected val softConstraintsProvider: USoftConstraintsProvider, -) : USolver, UModelBase>() { +) : USolver, UModelBase>(), AutoCloseable { protected fun translateLogicalConstraints(constraints: Iterable) { for (constraint in constraints) { @@ -95,11 +98,15 @@ open class USolverBase( translateLogicalConstraints(pc.logicalConstraints) } - internal fun checkWithSoftConstraints( + override fun check(query: UPathConstraints): USolverResult> = + internalCheck(query, useSoftConstraints = false) + + fun checkWithSoftConstraints( pc: UPathConstraints, - ) = check(pc, useSoftConstraints = true) + ) = internalCheck(pc, useSoftConstraints = true) + - override fun check( + private fun internalCheck( pc: UPathConstraints, useSoftConstraints: Boolean, ): USolverResult> { @@ -115,8 +122,8 @@ open class USolverBase( pc.logicalConstraints.flatMapTo(softConstraints) { softConstraintsProvider .provide(it) - .map { sc -> translator.translate(sc) } - .filterNot { sc -> sc.isFalse } + .map(translator::translate) + .filterNot(UBoolExpr::isFalse) } } @@ -136,8 +143,24 @@ open class USolverBase( // second, decode it unto uModel val uModel = decoder.decode(kModel) - // third, check it satisfies typeConstraints - when (val typeResult = pc.typeConstraints.verify(uModel)) { + // find interpretations of type constraints + + val isExprToInterpretation = kModel.declarations.mapNotNull { decl -> + translator.declToIsExpr[decl]?.let { isSubtypeExpr -> + val expr = decl.apply(emptyList()) + isSubtypeExpr to kModel.eval(expr, isComplete = true).asExpr(ctx.boolSort).isTrue + } + } + + // third, build a type solver query + val typeSolverQuery = TypeSolverQuery( + symbolicToConcrete = { uModel.eval(it) as UConcreteHeapRef }, + symbolicRefToTypeRegion = pc.typeConstraints.symbolicRefToTypeRegion, + isExprToInterpretation = isExprToInterpretation, + ) + + // fourth, check it satisfies typeConstraints + when (val typeResult = typeSolver.check(typeSolverQuery)) { is USatResult -> return USatResult( UModelBase( ctx, @@ -149,7 +172,7 @@ open class USolverBase( ) // in case of failure, assert reference disequality expressions - is UTypeUnsatResult -> typeResult.referenceDisequalitiesDisjuncts + is UTypeUnsatResult -> typeResult.conflictLemmas .map(translator::translate) .forEach(smtSolver::assert) diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/TypeSolver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/TypeSolver.kt new file mode 100644 index 0000000000..f0ca2fc824 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/solver/TypeSolver.kt @@ -0,0 +1,222 @@ +package org.usvm.solver + +import org.usvm.NULL_ADDRESS +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UIsExpr +import org.usvm.UIsSubtypeExpr +import org.usvm.UIsSupertypeExpr +import org.usvm.USymbolicHeapRef +import org.usvm.model.UTypeModel +import org.usvm.types.UTypeRegion +import org.usvm.types.UTypeSystem +import org.usvm.uctx + +data class TypeSolverQuery( + val symbolicToConcrete: (USymbolicHeapRef) -> UConcreteHeapRef, + val symbolicRefToTypeRegion: Map>, + val isExprToInterpretation: List, Boolean>>, +) + +class UTypeUnsatResult( + val conflictLemmas: List, +) : UUnsatResult>() + +class UTypeSolver( + private val typeSystem: UTypeSystem, +) : USolver, UTypeModel>() { + private val topTypeRegion by lazy { UTypeRegion(typeSystem, typeSystem.topTypeStream()) } + + /** + * Checks the [query]. + * + * Checking works as follows: + * 1. Groups propositional variables by symbolic heap references and builds nullability conflict lemmas. + * 2. Groups symbolic references into clusters by their concrete interpretations and filters out nulls. + * 3. For each cluster processes symbolic references one by one, intersects their type regions according to + * [UIsSubtypeExpr]s and [UIsSupertypeExpr]s. + * 4. If the current region became empty, then we have found a conflicting group, so build a new reference + * disequality lemma with negation of [UIsSubtypeExpr]s and [UIsSupertypeExpr]s. + * 5. If no conflicting references were found, builds a type model. + * + * Example: + * ``` + * a <: T1 | T2 + * b <: T2 | T3 + * c <: T3 | T1 + * d <: T1 | T2 + * e <: T2 + * cluster: (a, b, c, d, e) + * ``` + * Suppose we have the single cluster, so we process it as follows: + * + * 1. Peek `a`. The current region is empty, so it becomes `T1 | T2`. Potential conflicting refs = `{a}`. + * 2. Peek `b`. The current region becomes `T2`. Potential conflicting refs = `{a, b}`. + * 3. Peek `c`. The intersection of the current region with `T3 | T1` is empty, so we add the following constraint: + * `a != c || b != c || a == null || b == null || c == null`. The region becomes `T3 | T1`. + * Potential conflicting refs = `{c}. + * 4. Peek `d`. The current region becomes `T1`. Potential conflicting refs = `{c, d}`. + * 5. Peek `e`. The intersection of the current region with `T2` is empty, so we add the following constraint: + * `c != e || d != e || c == null || d == null || e == null`. + * + * @return The result of verification: + * * [UTypeModel] if the [query] is satisfiable. + * * [UUnsatResult] if the [query] is unsatisfiable in all models. + * * [UTypeUnsatResult] with lemmas explaining conflicts if the [query] is unsatisfiable in the current model, + * but may be satisfiable in other models. + */ + override fun check( + query: TypeSolverQuery, + ): USolverResult> { + val conflictLemmas = mutableListOf() + + val symbolicRefToIsExprs = extractIsExpressionsAndFindNullConflicts( + query.symbolicToConcrete, + query.isExprToInterpretation, + onHolds = { ref, isExpr -> + if (isExpr is UIsSupertypeExpr) { + conflictLemmas += with(ref.uctx) { mkOr(ref neq nullRef, !isExpr) } + } + }, + onNotHolds = { ref, isExpr -> + if (isExpr is UIsSubtypeExpr) { + conflictLemmas += with(ref.uctx) { mkOr(ref neq nullRef, isExpr) } + } + } + ) + + val symbolicRefToRegion = + symbolicRefToIsExprs.mapValues { topTypeRegion } + + query.symbolicRefToTypeRegion + + + val concreteRefToCluster = symbolicRefToRegion.entries + .groupBy { (ref, _) -> query.symbolicToConcrete(ref).address } + .filterNot { (address, _) -> address == NULL_ADDRESS } + + + // then for each group check conflicting types + val concreteToRegionWithCluster = concreteRefToCluster.mapValues { (_, cluster) -> + checkCluster(cluster, symbolicRefToIsExprs, conflictLemmas) + } + + // if there were some conflicts, return constraints on reference equalities + if (conflictLemmas.isNotEmpty()) { + return UTypeUnsatResult(conflictLemmas) + } + + // otherwise, return the type assignment + val allConcreteRefToType = concreteToRegionWithCluster.mapValues { (_, regionToCluster) -> + val (region, cluster) = regionToCluster + val typeStream = region.typeStream + if (typeStream.isEmpty) { + // the only way to reach here is when some of the clusters consists of a single reference + // because if the cluster is bigger, then we called region.isEmpty previously at least once + check(cluster.size == 1) + return UUnsatResult() + } + + typeStream + } + + val typeModel = UTypeModel(typeSystem, allConcreteRefToType) + return USatResult(typeModel) + } + + private fun checkCluster( + cluster: List>>, + symbolicRefToIsExpr: Map, Boolean>>>, + conflictLemmas: MutableList, + ): Pair, List>>> { + var currentRegion = topTypeRegion + val potentialConflictingRefs = mutableListOf() + val potentialConflictingIsExprs = mutableListOf() + + for ((heapRef, region) in cluster) { + var nextRegion = currentRegion.intersect(region) // add [heapRef] to the current region + + val isExprs = symbolicRefToIsExpr.getOrElse(heapRef, ::emptyList) + + val evaluatedIsExprs = isExprs.map { (isExpr, holds) -> + if (holds) { + nextRegion = when (isExpr) { + is UIsSupertypeExpr -> nextRegion.addSubtype(isExpr.subtype) + is UIsSubtypeExpr -> nextRegion.addSupertype(isExpr.supertype) + else -> error("Unexpected isExpr: $isExpr") + } + isExpr + } else { + nextRegion = when (isExpr) { + is UIsSupertypeExpr -> nextRegion.excludeSubtype(isExpr.subtype) + is UIsSubtypeExpr -> nextRegion.excludeSupertype(isExpr.supertype) + else -> error("Unexpected isExpr: $isExpr") + } + isExpr.ctx.mkNot(isExpr) + } + } + + if (nextRegion.isEmpty) { + // conflict detected, so it's impossible for [potentialConflictingRefs] + // to have the common type with [heapRef], therefore they can't be equal, or + // some of them equals null, or some of the [potentialConflictingIsExprs] is false + val disjunct = mutableListOf() + with(heapRef.uctx) { + // can't be equal to heapRef + potentialConflictingRefs.mapTo(disjunct) { it.neq(heapRef) } + // some of them is null + potentialConflictingRefs.mapTo(disjunct) { it.eq(nullRef) } + disjunct += heapRef.eq(nullRef) + // the accumulated conflicting propositional variables + potentialConflictingIsExprs.mapTo(disjunct) { it.not() } + // the new propositional variables + evaluatedIsExprs.mapTo(disjunct) { it.not() } + } + conflictLemmas += heapRef.ctx.mkOr(disjunct) + + // start a new group + nextRegion = region + potentialConflictingIsExprs.clear() + potentialConflictingRefs.clear() + potentialConflictingRefs.add(heapRef) + } else if (nextRegion == region) { + // the current [heapRef] gives the same region as the potentialConflictingRefs, so it's better + // to keep only the [heapRef] to minimize the disequalities amount in the result disjunction + potentialConflictingIsExprs.clear() + potentialConflictingRefs.clear() + potentialConflictingRefs.add(heapRef) + } else if (nextRegion != currentRegion) { + // no conflict detected, but the current region became smaller + potentialConflictingRefs.add(heapRef) + potentialConflictingIsExprs += evaluatedIsExprs + } + + currentRegion = nextRegion + } + + return currentRegion to cluster + } + + private inline fun extractIsExpressionsAndFindNullConflicts( + symbolicToConcrete: (USymbolicHeapRef) -> UConcreteHeapRef, + isExpressions: List, Boolean>>, + onHolds: (USymbolicHeapRef, UIsExpr) -> Unit = { _, _ -> }, + onNotHolds: (USymbolicHeapRef, UIsExpr) -> Unit = { _, _ -> }, + ): Map, Boolean>>> { + val symbolicRefToIsSubtypeExprs = isExpressions.groupBy { (expr, _) -> expr.ref as USymbolicHeapRef } + for ((ref, isSupertypeExprs) in symbolicRefToIsSubtypeExprs) { + val concreteRef = symbolicToConcrete(ref).address + if (concreteRef != NULL_ADDRESS) { + continue + } + for ((isExpr, holds) in isSupertypeExprs) { + if (holds) { + onHolds(ref, isExpr) + } else { + onNotHolds(ref, isExpr) + } + } + } + return symbolicRefToIsSubtypeExprs + } + +} diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt b/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt index be6e6edd40..10d3131939 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt @@ -28,31 +28,33 @@ import org.usvm.UBvSort import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr -import org.usvm.UExprTransformer import org.usvm.UHeapReading import org.usvm.UIndexedMethodReturnValue import org.usvm.UInputArrayLengthReading import org.usvm.UInputArrayReading import org.usvm.UInputFieldReading -import org.usvm.UIsExpr +import org.usvm.UIsSubtypeExpr +import org.usvm.UIsSupertypeExpr import org.usvm.UMockSymbol import org.usvm.UNullRef import org.usvm.URegisterReading import org.usvm.USizeExpr import org.usvm.USort import org.usvm.USymbol +import org.usvm.UTransformer import org.usvm.uctx -class USoftConstraintsProvider(ctx: UContext) : UExprTransformer(ctx) { +class USoftConstraintsProvider(override val ctx: UContext) : UTransformer { // We have a list here since sometimes we want to add several soft constraints // to make it possible to drop only a part of them, not the whole soft constraint - private val caches = hashMapOf, Set>().withDefault { emptySet() } + private val caches = hashMapOf, Set>() private val sortPreferredValuesProvider = SortPreferredValuesProvider() - fun provide(initialExpr: UExpr<*>): Set { - apply(initialExpr) - return caches.getValue(initialExpr) - } + fun provide(initialExpr: UExpr<*>): Set = + caches.getOrElse(initialExpr) { + apply(initialExpr) + caches.getOrPut(initialExpr, ::emptySet) + } // region The most common methods @@ -61,13 +63,11 @@ class USoftConstraintsProvider(ctx: UContext) : UExprTransformer transformApp(expr: KApp): KExpr = - transformExprAfterTransformed(expr, expr.args) { args -> - computeSideEffect(expr) { - val nestedConstraints = args.flatMapTo(mutableSetOf()) { caches.getValue(it) } - val selfConstraint = expr.sort.accept(sortPreferredValuesProvider)(expr) + computeSideEffect(expr) { + val nestedConstraints = expr.args.flatMapTo(mutableSetOf(), ::provide) + val selfConstraint = expr.sort.accept(sortPreferredValuesProvider)(expr) - caches[expr] = nestedConstraints + selfConstraint - } + caches[expr] = nestedConstraints + selfConstraint } private fun transformAppIfPossible(expr: UExpr): UExpr = @@ -100,34 +100,31 @@ class USoftConstraintsProvider(ctx: UContext) : UExprTransformer = expr - override fun transform(expr: UIsExpr): UBoolExpr = - error("Illegal operation since UIsExpr should not be translated into a SMT solver") + override fun transform(expr: UIsSubtypeExpr): UBoolExpr = expr + + override fun transform(expr: UIsSupertypeExpr): UBoolExpr = expr override fun transform( expr: UInputArrayLengthReading, - ): USizeExpr = transformExprAfterTransformed(expr, expr.address) { - computeSideEffect(expr) { - with(expr.ctx) { - val addressIsNull = caches.getValue(expr.address) - val arraySize = mkBvSignedLessOrEqualExpr(expr, PREFERRED_MAX_ARRAY_SIZE.toBv()) + ): USizeExpr = computeSideEffect(expr) { + with(expr.ctx) { + val addressIsNull = provide(expr.address) + val arraySize = mkBvSignedLessOrEqualExpr(expr, PREFERRED_MAX_ARRAY_SIZE.toBv()) - caches[expr] = addressIsNull + arraySize - } + caches[expr] = addressIsNull + arraySize } } override fun transform( expr: UInputArrayReading, - ): UExpr = transformExprAfterTransformed(expr, expr.index, expr.address) { _, _ -> - computeSideEffect(expr) { - val constraints = mutableSetOf() + ): UExpr = computeSideEffect(expr) { + val constraints = mutableSetOf() - constraints += caches.getValue(expr.index) - constraints += caches.getValue(expr.address) - constraints += expr.sort.accept(sortPreferredValuesProvider)(expr) + constraints += provide(expr.index) + constraints += provide(expr.address) + constraints += expr.sort.accept(sortPreferredValuesProvider)(expr) - caches[expr] = constraints - } + caches[expr] = constraints } override fun transform(expr: UAllocatedArrayReading): UExpr = @@ -139,23 +136,19 @@ class USoftConstraintsProvider(ctx: UContext) : UExprTransformer readingWithSingleArgumentTransform( expr: UHeapReading<*, *, Sort>, arg: UExpr<*>, - ): UExpr = transformExprAfterTransformed(expr, arg) { _ -> - computeSideEffect(expr) { - val argConstraint = caches.getValue(arg) - val selfConstraint = expr.sort.accept(sortPreferredValuesProvider)(expr) + ): UExpr = computeSideEffect(expr) { + val argConstraint = provide(arg) + val selfConstraint = expr.sort.accept(sortPreferredValuesProvider)(expr) - caches[expr] = argConstraint + selfConstraint - } + caches[expr] = argConstraint + selfConstraint } // region KExpressions override fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = with(expr.ctx) { - transformExprAfterTransformed(expr, expr.arg0, expr.arg1) { lhs, rhs -> - computeSideEffect(expr) { - val selfConstraint = mkEq(lhs, rhs) - caches[expr] = mutableSetOf(selfConstraint) + caches.getValue(lhs) + caches.getValue(rhs) - } + computeSideEffect(expr) { + val selfConstraint = mkEq(expr.arg0, expr.arg1) + caches[expr] = mutableSetOf(selfConstraint) + provide(expr.arg0) + provide(expr.arg1) } } @@ -267,10 +260,8 @@ private class SortPreferredValuesProvider : KSortVisitor<(KExpr<*>) -> KExpr mkAnd( - mkAnd( - mkArithLe(mkRealNum(INT_MIN_VALUE), expr.asExpr(sort)), - mkArithGe(mkRealNum(INT_MAX_VALUE), expr.asExpr(sort)) - ) + mkArithLe(mkRealNum(INT_MIN_VALUE), expr.asExpr(sort)), + mkArithGe(mkRealNum(INT_MAX_VALUE), expr.asExpr(sort)) ) } } @@ -297,4 +288,4 @@ private class SortPreferredValuesProvider : KSortVisitor<(KExpr<*>) -> KExpr private constructor( private val typeSystem: UTypeSystem, private val cachingSequence: CachingSequence, + private val cacheFromQueries: List, private val supportType: Type, private val filtering: (Type) -> Boolean, ) : UTypeStream { - override fun filterBySupertype(type: Type): UTypeStream { - return when { - typeSystem.isSupertype(supportType, type) -> { // we update the [supportType] - USupportTypeStream( - typeSystem, - rootSequence(typeSystem, type).filter(filtering), + override fun filterBySupertype(type: Type): UTypeStream = + when { + // we update the [supportType] + typeSystem.isSupertype(supportType, type) -> USupportTypeStream( + typeSystem, + rootSequence(typeSystem, type).filter(filtering), + cacheFromQueries.addIfDoesntExceedSizeAndFilter( type, + maxSize = MAX_SIZE, filtering - ) - } + ) { typeSystem.isSupertype(type, it) }, + type, + filtering + ) - else -> { // just add one more filter - USupportTypeStream( - typeSystem, - cachingSequence.filter { typeSystem.isSupertype(type, it) }, - supportType, - filtering = { filtering(it) && typeSystem.isSupertype(type, it) } - ) - } + // just add one more filter + else -> withNewFiltering(type) { typeSystem.isSupertype(type, it) } } - } - override fun filterBySubtype(type: Type): UTypeStream { - return when { - typeSystem.isSupertype(type, supportType) -> { - if (type == supportType && filtering(type) && typeSystem.isInstantiable(type)) { // exact type + override fun filterBySubtype(type: Type): UTypeStream = + when { + // exact type + typeSystem.isSupertype(type, supportType) -> + if (type == supportType && filtering(type) && typeSystem.isInstantiable(type)) { USingleTypeStream(typeSystem, type) } else { emptyTypeStream() } - } - else -> { - USupportTypeStream( - typeSystem, - cachingSequence.filter { typeSystem.isSupertype(it, type) }, - supportType, - filtering = { filtering(it) && typeSystem.isSupertype(it, type) } - ) - } + else -> withNewFiltering(type) { typeSystem.isSupertype(it, type) } } - } - override fun filterByNotSupertype(type: Type): UTypeStream { - return when { - typeSystem.isSupertype(type, supportType) -> { - emptyTypeStream() - } + override fun filterByNotSupertype(type: Type): UTypeStream = + when { + typeSystem.isSupertype(type, supportType) -> emptyTypeStream() + else -> withNewFiltering(type) { !typeSystem.isSupertype(type, it) } + } - else -> { - USupportTypeStream( - typeSystem, - cachingSequence.filter { !typeSystem.isSupertype(type, it) }, - supportType, - filtering = { filtering(it) && !typeSystem.isSupertype(type, it) }, - ) - } + override fun filterByNotSubtype(type: Type): UTypeStream = + when { + typeSystem.isSupertype(type, supportType) && type != supportType -> this + else -> withNewFiltering(type) { !typeSystem.isSupertype(it, type) } } - } - override fun filterByNotSubtype(type: Type): UTypeStream { - return when { - typeSystem.isSupertype(type, supportType) && type != supportType -> { - this - } + private fun withNewFiltering(type: Type, newFiltering: (Type) -> Boolean) = + USupportTypeStream( + typeSystem, + cachingSequence.filter(newFiltering), + cacheFromQueries.addIfDoesntExceedSizeAndFilter( + type, + maxSize = MAX_SIZE, + filtering + ) { newFiltering(it) && typeSystem.isSupertype(supportType, it) }, + supportType, + filtering = { filtering(it) && newFiltering(it) } + ) - else -> { - USupportTypeStream( - typeSystem, - cachingSequence.filter { !typeSystem.isSupertype(it, type) }, - supportType, - filtering = { filtering(it) && !typeSystem.isSupertype(it, type) } - ) + override fun take(n: Int): Set { + val set = cacheFromQueries.toMutableSet() + for (it in cachingSequence) { + if (set.size == n) { + break } + set += it } + return set } - override fun take(n: Int): List = - cachingSequence.take(n).toList() - override val isEmpty: Boolean get() = take(1).isEmpty() companion object { fun from(typeSystem: UTypeSystem, type: Type): USupportTypeStream { val root = rootSequence(typeSystem, type).filter(typeSystem::isInstantiable) - return USupportTypeStream(typeSystem, root, type, typeSystem::isInstantiable) + val fromQueries = if (typeSystem.isInstantiable(type)) listOf(type) else listOf() + return USupportTypeStream(typeSystem, root, fromQueries, type, typeSystem::isInstantiable) } private fun rootSequence( @@ -112,5 +107,32 @@ class USupportTypeStream private constructor( val dfsIterator = DfsIterator(type) { typeNode -> typeSystem.findSubtypes(typeNode).iterator() } return CachingSequence(dfsIterator) } + + /** + * In practice, usually the type doesn't have more than 8 concrete inheritors, and [MAX_SIZE] is less than + * the default capacity of [java.util.ArrayList]. + */ + private const val MAX_SIZE = 8 + + /** + * @param type the type to be added + * @param maxSize the maximum size of the result list + * @param filtering the filtering function for checking the [type] + * @param newFiltering the filtering function for checking the types in [this] list and the [type] + */ + private inline fun List.addIfDoesntExceedSizeAndFilter( + type: Type, + maxSize: Int, + filtering: (Type) -> Boolean, + newFiltering: (Type) -> Boolean, + ): List = + filter(newFiltering) + .run { + if (size < maxSize && filtering(type) && newFiltering(type) && type !in this) { + this + type + } else { + this + } + } } } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt index 6f91dac877..f33b87b299 100644 --- a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt @@ -8,7 +8,7 @@ import org.usvm.util.RegionComparisonResult /** * Class representing possible types which certain objects can have. */ -open class UTypeRegion( +class UTypeRegion( val typeSystem: UTypeSystem, val typeStream: UTypeStream, val supertypes: PersistentSet = persistentSetOf(), @@ -16,14 +16,13 @@ open class UTypeRegion( val subtypes: PersistentSet = persistentSetOf(), val notSubtypes: PersistentSet = persistentSetOf(), ) : Region> { - val isContradicting get() = typeStream.isEmpty - /** * Returns region that represents empty set of types. Called when type * constraints contradict, for example if X <: Y and X ( * - X <: t && X <: u && u { - if (isContradicting || supertypes.any { typeSystem.isSupertype(supertype, it) }) { + fun addSupertype(supertype: Type): UTypeRegion { + if (isEmpty || supertypes.any { typeSystem.isSupertype(supertype, it) }) { return this } @@ -83,8 +82,8 @@ open class UTypeRegion( * (here X is type from this region and t is [notSupertype]): * X <: u && u <: t && X { - if (isContradicting || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) { + fun excludeSupertype(notSupertype: Type): UTypeRegion { + if (isEmpty || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) { return this } @@ -108,8 +107,8 @@ open class UTypeRegion( * - t <: X && u <: t && u { - if (isContradicting || subtypes.any { typeSystem.isSupertype(it, subtype) }) { + fun addSubtype(subtype: Type): UTypeRegion { + if (isEmpty || subtypes.any { typeSystem.isSupertype(it, subtype) }) { return this } @@ -134,8 +133,8 @@ open class UTypeRegion( * - u <: X && t <: u && t { - if (isContradicting || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) { + fun excludeSubtype(notSubtype: Type): UTypeRegion { + if (isEmpty || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) { return this } @@ -153,9 +152,10 @@ open class UTypeRegion( return UTypeRegion(typeSystem, newTypeStream, notSubtypes = newNotSubtypes) } - override val isEmpty: Boolean = isContradicting - override fun intersect(other: UTypeRegion): UTypeRegion { + if (this == other) { + return this + } // TODO: optimize things up by not re-allocating type regions after each operation val otherSize = other.size val thisSize = this.size @@ -164,6 +164,9 @@ open class UTypeRegion( } else { this to other } + if (smallRegion.isEmpty) { + return smallRegion + } val result1 = smallRegion.supertypes.fold(largeRegion) { acc, t -> acc.addSupertype(t) } val result2 = smallRegion.notSupertypes.fold(result1) { acc, t -> acc.excludeSupertype(t) } @@ -172,6 +175,9 @@ open class UTypeRegion( } override fun subtract(other: UTypeRegion): UTypeRegion { + if (isEmpty || other.isEmpty) { + return this + } if (other.notSupertypes.isNotEmpty() || other.notSubtypes.isEmpty() || other.supertypes.size + other.subtypes.size != 1) { TODO("For now, we are able to subtract only positive singleton type constraints") } diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt index e124cbe601..cfac8b5d60 100644 --- a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt +++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt @@ -71,7 +71,9 @@ object UEmptyTypeStream : UTypeStream { @Suppress("UNCHECKED_CAST") fun emptyTypeStream(): UTypeStream = UEmptyTypeStream as UTypeStream -fun UTypeStream.takeFirst(): Type = take(1).single() +fun UTypeStream.first(): Type = take(1).first() + +fun UTypeStream.firstOrNull(): Type? = take(1).firstOrNull() /** * Consists of just one type [singleType]. diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt index 23ec94b830..90773dd9d6 100644 --- a/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt +++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt @@ -7,29 +7,29 @@ package org.usvm.types interface UTypeSystem { /** - * @return true if t <: u. + * @return true if [type] <: [supertype]. */ - fun isSupertype(u: Type, t: Type): Boolean + fun isSupertype(supertype: Type, type: Type): Boolean /** - * @return true if [t] can be supertype for some type together with some incomparable type u. + * @return true if [type] can be supertype for some type together with some incomparable type u. */ - fun isMultipleInheritanceAllowedFor(t: Type): Boolean + fun isMultipleInheritanceAllowedFor(type: Type): Boolean /** - * @return true if there is no type u distinct from [t] and subtyping [t]. + * @return true if there is no type u distinct from [type] and subtyping [type]. */ - fun isFinal(t: Type): Boolean + fun isFinal(type: Type): Boolean /** - * @return true if [t] is instantiable, meaning it can be created via constructor. + * @return true if [type] is instantiable, meaning it can be created via constructor. */ - fun isInstantiable(t: Type): Boolean + fun isInstantiable(type: Type): Boolean /** - * @return a sequence of **direct** inheritors of the [t]. + * @return a sequence of **direct** inheritors of the [type]. */ - fun findSubtypes(t: Type): Sequence + fun findSubtypes(type: Type): Sequence /** diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 1a822d2aed..48365a6885 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -201,10 +201,10 @@ internal class CompositionTest { val heapEvaluator = mockk>>() // TODO replace with jacoDB type val composer = UComposer(ctx, stackEvaluator, heapEvaluator, typeEvaluator, mockEvaluator) // TODO remove - val isExpression = ctx.mkIsExpr(heapRef, type) + val isExpression = ctx.mkIsSubtypeExpr(heapRef, type) every { heapRef.accept(any()) } returns addressFromMemory as KExpr - every { typeEvaluator.evalIs(addressFromMemory, type) } returns typeResult + every { typeEvaluator.evalIsSubtype(addressFromMemory, type) } returns typeResult val composedExpression = composer.compose(isExpression) diff --git a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt index 8e7b1a950d..296129155d 100644 --- a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt @@ -200,14 +200,14 @@ class UContextInterningTest { val fstSort = bv16Sort // TODO replace with jacodb type val sndSort = bv32Sort - val equal = List(10) { mkIsExpr(fstRef, fstSort) } + val equal = List(10) { mkIsSubtypeExpr(fstRef, fstSort) } - val createdWithoutContext = UIsExpr(this, fstRef, fstSort) + val createdWithoutContext = UIsSubtypeExpr(this, fstRef, fstSort) val distinct = listOf( - mkIsExpr(fstRef, fstSort), - mkIsExpr(fstRef, sndSort), - mkIsExpr(sndRef, sndSort), + mkIsSubtypeExpr(fstRef, fstSort), + mkIsSubtypeExpr(fstRef, sndSort), + mkIsSubtypeExpr(sndRef, sndSort), createdWithoutContext ) diff --git a/usvm-core/src/test/kotlin/org/usvm/constraints/EqualityConstraintsTests.kt b/usvm-core/src/test/kotlin/org/usvm/constraints/EqualityConstraintsTests.kt index 17ab394501..313095f7f5 100644 --- a/usvm-core/src/test/kotlin/org/usvm/constraints/EqualityConstraintsTests.kt +++ b/usvm-core/src/test/kotlin/org/usvm/constraints/EqualityConstraintsTests.kt @@ -7,7 +7,6 @@ import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import org.usvm.UComponents import org.usvm.UContext -import org.usvm.UHeapRef import kotlin.test.assertSame import kotlin.test.assertTrue @@ -25,13 +24,13 @@ class EqualityConstraintsTests { @Test fun testDiseq() { - val ref1: UHeapRef = ctx.mkRegisterReading(1, ctx.addressSort) - val ref2: UHeapRef = ctx.mkRegisterReading(2, ctx.addressSort) - val ref3: UHeapRef = ctx.mkRegisterReading(3, ctx.addressSort) - val ref4: UHeapRef = ctx.mkRegisterReading(4, ctx.addressSort) - val ref5: UHeapRef = ctx.mkRegisterReading(5, ctx.addressSort) - val ref6: UHeapRef = ctx.mkRegisterReading(6, ctx.addressSort) - val ref7: UHeapRef = ctx.mkRegisterReading(7, ctx.addressSort) + val ref1 = ctx.mkRegisterReading(1, ctx.addressSort) + val ref2 = ctx.mkRegisterReading(2, ctx.addressSort) + val ref3 = ctx.mkRegisterReading(3, ctx.addressSort) + val ref4 = ctx.mkRegisterReading(4, ctx.addressSort) + val ref5 = ctx.mkRegisterReading(5, ctx.addressSort) + val ref6 = ctx.mkRegisterReading(6, ctx.addressSort) + val ref7 = ctx.mkRegisterReading(7, ctx.addressSort) constraints.makeNonEqual(ref1, ctx.nullRef) constraints.makeNonEqual(ref2, ctx.nullRef) @@ -80,10 +79,10 @@ class EqualityConstraintsTests { @Test fun testNullableDiseq() { - val ref1: UHeapRef = ctx.mkRegisterReading(1, ctx.addressSort) - val ref2: UHeapRef = ctx.mkRegisterReading(2, ctx.addressSort) - val ref3: UHeapRef = ctx.mkRegisterReading(3, ctx.addressSort) - val ref4: UHeapRef = ctx.mkRegisterReading(4, ctx.addressSort) + val ref1 = ctx.mkRegisterReading(1, ctx.addressSort) + val ref2 = ctx.mkRegisterReading(2, ctx.addressSort) + val ref3 = ctx.mkRegisterReading(3, ctx.addressSort) + val ref4 = ctx.mkRegisterReading(4, ctx.addressSort) constraints.makeNonEqualOrBothNull(ref1, ref2) constraints.makeNonEqualOrBothNull(ref1, ref3) diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt index 3e8ec59ae2..858b193b8d 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt @@ -9,7 +9,6 @@ import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import org.usvm.Field import org.usvm.Method -import org.usvm.Type import org.usvm.UArrayIndexLValue import org.usvm.UComponents import org.usvm.UConcreteHeapRef @@ -22,11 +21,13 @@ import org.usvm.memory.URegistersStack import org.usvm.solver.USatResult import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase +import org.usvm.solver.UTypeSolver import org.usvm.solver.UUnsatResult -import org.usvm.types.USingleTypeStream import org.usvm.types.single.SingleTypeSystem import kotlin.test.assertIs +private typealias Type = SingleTypeSystem.SingleType + class ModelDecodingTest { private lateinit var ctx: UContext private lateinit var solver: USolverBase @@ -42,9 +43,10 @@ class ModelDecodingTest { every { components.mkTypeSystem(any()) } returns SingleTypeSystem ctx = UContext(components) - val softConstraintProvider = USoftConstraintsProvider(ctx) + val softConstraintsProvider = USoftConstraintsProvider(ctx) val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) - solver = USolverBase(ctx, KZ3Solver(ctx), translator, decoder, softConstraintProvider) + val typeSolver = UTypeSolver(SingleTypeSystem) + solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider) stack = URegistersStack() stack.push(10) diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt index c44acee6ba..5b8bdd192c 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt @@ -14,11 +14,12 @@ import org.usvm.constraints.UPathConstraints import org.usvm.memory.emptyInputArrayLengthRegion import org.usvm.model.ULazyModelDecoder import org.usvm.model.buildTranslatorAndLazyDecoder -import org.usvm.types.UTypeSystem import org.usvm.types.single.SingleTypeSystem import kotlin.test.assertSame -open class SoftConstraintsTest { +private typealias Type = SingleTypeSystem.SingleType + +open class SoftConstraintsTest { private lateinit var ctx: UContext private lateinit var softConstraintsProvider: USoftConstraintsProvider private lateinit var translator: UExprTranslator @@ -37,7 +38,8 @@ open class SoftConstraintsTest { translator = translatorWithDecoder.first decoder = translatorWithDecoder.second - solver = USolverBase(ctx, KZ3Solver(ctx), translator, decoder, softConstraintsProvider) + val typeSolver = UTypeSolver(SingleTypeSystem) + solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider) } @Test @@ -78,7 +80,8 @@ open class SoftConstraintsTest { pc += sndExpr pc += sameAsFirstExpr - val solver = USolverBase(ctx, KZ3Solver(ctx), translator, decoder, softConstraintsProvider) + val typeSolver = UTypeSolver(mockk()) + val solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider) val result = solver.checkWithSoftConstraints(pc) as USatResult val model = result.model diff --git a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt index f98ded75f3..c5722dcf13 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt @@ -3,7 +3,6 @@ package org.usvm.types import io.ksmt.solver.z3.KZ3Solver import io.mockk.every import io.mockk.mockk -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.Field import org.usvm.INITIAL_INPUT_ADDRESS @@ -13,17 +12,24 @@ import org.usvm.UComponents import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.constraints.UPathConstraints -import org.usvm.constraints.UTypeUnsatResult +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.memory.UMemoryBase import org.usvm.memory.URegionHeap import org.usvm.memory.emptyInputArrayRegion +import org.usvm.memory.heapRefEq import org.usvm.model.UModelBase import org.usvm.model.buildTranslatorAndLazyDecoder +import org.usvm.solver.TypeSolverQuery import org.usvm.solver.USatResult import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase +import org.usvm.solver.UTypeSolver +import org.usvm.solver.UTypeUnsatResult import org.usvm.solver.UUnsatResult import org.usvm.types.system.TestType +import org.usvm.types.system.a +import org.usvm.types.system.b import org.usvm.types.system.base1 import org.usvm.types.system.base2 import org.usvm.types.system.c @@ -38,6 +44,7 @@ import org.usvm.types.system.interfaceAC import org.usvm.types.system.interfaceBC1 import org.usvm.types.system.interfaceBC2 import org.usvm.types.system.testTypeSystem +import org.usvm.types.system.top import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertNotEquals @@ -48,13 +55,14 @@ class TypeSolverTest { private val components = mockk>() private val ctx = UContext(components) private val solver: USolverBase + private val typeSolver: UTypeSolver init { val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) val softConstraintsProvider = USoftConstraintsProvider(ctx) - val smtSolver = KZ3Solver(ctx) - solver = USolverBase(ctx, smtSolver, translator, decoder, softConstraintsProvider) + typeSolver = UTypeSolver(typeSystem) + solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider) every { components.mkSolver(ctx) } returns solver every { components.mkTypeSystem(ctx) } returns typeSystem @@ -72,10 +80,10 @@ class TypeSolverTest { @Test fun `Test symbolic ref -- open type inheritance`() = with(ctx) { - val ref = ctx.mkRegisterReading(0, addressSort) - pc += mkIsExpr(ref, base1) + val ref = mkRegisterReading(0, addressSort) + pc += mkIsSubtypeExpr(ref, base1) pc += mkHeapRefEq(ref, nullRef).not() - val model = (solver.check(pc, useSoftConstraints = false) as USatResult>).model + val model = (solver.check(pc) as USatResult>).model val concreteRef = assertIs(model.eval(ref)) val types = model.typeStreamOf(concreteRef) types.take100AndAssertEqualsToSetOf(base1, derived1A, derived1B) @@ -83,10 +91,10 @@ class TypeSolverTest { @Test fun `Test symbolic ref -- interface type inheritance`() = with(ctx) { - val ref = ctx.mkRegisterReading(0, addressSort) - pc += mkIsExpr(ref, interface1) + val ref = mkRegisterReading(0, addressSort) + pc += mkIsSubtypeExpr(ref, interface1) pc += mkHeapRefEq(ref, nullRef).not() - val model = (solver.check(pc, useSoftConstraints = false) as USatResult>).model + val model = (solver.check(pc) as USatResult>).model val concreteRef = assertIs(model.eval(ref)) val types = model.typeStreamOf(concreteRef) types.take100AndAssertEqualsToSetOf(derived1A, derivedMulti, derivedMultiInterfaces) @@ -95,65 +103,88 @@ class TypeSolverTest { @Test fun `Test concrete ref -- empty intersection simplification`() = with(ctx) { val ref = memory.alloc(base1) - pc += mkIsExpr(ref, base2) + pc += mkIsSubtypeExpr(ref, base2) assertTrue(pc.isFalse) } @Test fun `Test symbolic ref -- empty intersection simplification`() = with(ctx) { - val ref = ctx.mkRegisterReading(0, addressSort) - pc += mkIsExpr(ref, base1) - pc += mkIsExpr(ref, base2) + val ref = mkRegisterReading(0, addressSort) + pc += mkIsSubtypeExpr(ref, base1) + pc += mkIsSubtypeExpr(ref, base2) pc += mkHeapRefEq(ref, nullRef).not() assertTrue(pc.isFalse) } @Test fun `Test symbolic ref cast -- empty intersection simplification`(): Unit = with(ctx) { - val ref = ctx.mkRegisterReading(0, addressSort) - pc += mkIsExpr(ref, base1) - pc += mkIsExpr(ref, base2) + val ref = mkRegisterReading(0, addressSort) + pc += mkIsSubtypeExpr(ref, base1) + pc += mkIsSubtypeExpr(ref, base2) - val resultWithoutNullConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithoutNullConstraint = solver.check(pc) assertIs>>(resultWithoutNullConstraint) pc += mkHeapRefEq(ref, nullRef).not() - val resultWithNullConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithNullConstraint = solver.check(pc) assertIs>>(resultWithNullConstraint) } @Test fun `Test symbolic ref -- different types`(): Unit = with(ctx) { - val ref0 = ctx.mkRegisterReading(0, addressSort) - val ref1 = ctx.mkRegisterReading(1, addressSort) + val ref0 = mkRegisterReading(0, addressSort) + val ref1 = mkRegisterReading(1, addressSort) - pc += mkIsExpr(ref0, base1) - pc += mkIsExpr(ref1, base2) + pc += mkIsSubtypeExpr(ref0, base1) + pc += mkIsSubtypeExpr(ref1, base2) pc += mkHeapRefEq(ref0, nullRef).not() pc += mkHeapRefEq(ref1, nullRef).not() - val resultWithoutEqConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithoutEqConstraint = solver.check(pc) val model = assertIs>>(resultWithoutEqConstraint).model assertNotEquals(model.eval(ref0), model.eval(ref1)) pc += mkHeapRefEq(ref0, ref1) - val resultWithEqConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithEqConstraint = solver.check(pc) assertIs>>(resultWithEqConstraint) } + @Test + fun `Test symbolic ref -- different types 3 refs`(): Unit = with(ctx) { + val ref0 = mkRegisterReading(0, addressSort) + val ref1 = mkRegisterReading(1, addressSort) + val ref2 = mkRegisterReading(2, addressSort) + + pc += mkIsSubtypeExpr(ref0, interfaceAB) + pc += mkIsSubtypeExpr(ref1, interfaceBC1) + pc += mkIsSubtypeExpr(ref2, interfaceAC) + pc += mkHeapRefEq(ref0, nullRef).not() + pc += mkHeapRefEq(ref1, nullRef).not() + pc += mkHeapRefEq(ref2, nullRef).not() + + val resultWithoutEqConstraint = solver.check(pc) + val model = assertIs>>(resultWithoutEqConstraint).model + assertNotEquals(model.eval(ref0), model.eval(ref1)) + + pc += mkHeapRefEq(ref0, ref1) + pc += mkHeapRefEq(ref1, ref2) + + assertTrue(pc.isFalse) + } + @Test fun `Test symbolic ref -- different interface types but same base type`(): Unit = with(ctx) { - val ref0 = ctx.mkRegisterReading(0, addressSort) - val ref1 = ctx.mkRegisterReading(1, addressSort) + val ref0 = mkRegisterReading(0, addressSort) + val ref1 = mkRegisterReading(1, addressSort) - pc += mkIsExpr(ref0, base1) - pc += mkIsExpr(ref0, interface1) - pc += mkIsExpr(ref1, base1) - pc += mkIsExpr(ref1, interface2) + pc += mkIsSubtypeExpr(ref0, base1) + pc += mkIsSubtypeExpr(ref0, interface1) + pc += mkIsSubtypeExpr(ref1, base1) + pc += mkIsSubtypeExpr(ref1, interface2) - val resultWithoutEqConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithoutEqConstraint = solver.check(pc) val modelWithoutEqConstraint = assertIs>>(resultWithoutEqConstraint).model @@ -165,7 +196,7 @@ class TypeSolverTest { pc += mkHeapRefEq(ref0, ref1) - val resultWithEqConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithEqConstraint = solver.check(pc) val modelWithEqConstraint = assertIs>>(resultWithEqConstraint).model assertEquals(mkConcreteHeapRef(NULL_ADDRESS), modelWithEqConstraint.eval(ref0)) @@ -173,31 +204,31 @@ class TypeSolverTest { pc += mkHeapRefEq(nullRef, ref0).not() - val resultWithEqAndNotNullConstraint = solver.check(pc, useSoftConstraints = false) + val resultWithEqAndNotNullConstraint = solver.check(pc) assertIs>>(resultWithEqAndNotNullConstraint) } @Test fun `Test symbolic ref -- expressions to assert correctness`(): Unit = with(ctx) { - val a = ctx.mkRegisterReading(0, addressSort) - val b1 = ctx.mkRegisterReading(1, addressSort) - val b2 = ctx.mkRegisterReading(2, addressSort) - val c = ctx.mkRegisterReading(3, addressSort) + val a = mkRegisterReading(0, addressSort) + val b1 = mkRegisterReading(1, addressSort) + val b2 = mkRegisterReading(2, addressSort) + val c = mkRegisterReading(3, addressSort) pc += mkHeapRefEq(a, nullRef).not() and - mkHeapRefEq(b1, nullRef).not() and - mkHeapRefEq(b2, nullRef).not() and - mkHeapRefEq(c, nullRef).not() + mkHeapRefEq(b1, nullRef).not() and + mkHeapRefEq(b2, nullRef).not() and + mkHeapRefEq(c, nullRef).not() - pc += mkIsExpr(a, interfaceAB) - pc += mkIsExpr(b1, interfaceBC1) - pc += mkIsExpr(b2, interfaceBC2) - pc += mkIsExpr(c, interfaceAC) + pc += mkIsSubtypeExpr(a, interfaceAB) + pc += mkIsSubtypeExpr(b1, interfaceBC1) + pc += mkIsSubtypeExpr(b2, interfaceBC2) + pc += mkIsSubtypeExpr(c, interfaceAC) pc += mkHeapRefEq(b1, b2) with(pc.clone()) { - val result = solver.check(this, useSoftConstraints = false) + val result = solver.check(this) assertIs>>(result) val concreteA = result.model.eval(a) @@ -216,32 +247,39 @@ class TypeSolverTest { every { eval(b2) } returns mkConcreteHeapRef(INITIAL_INPUT_ADDRESS) every { eval(c) } returns mkConcreteHeapRef(INITIAL_INPUT_ADDRESS) } - val result = typeConstraints.verify(model) + + val query = TypeSolverQuery( + symbolicToConcrete = { model.eval(it) as UConcreteHeapRef }, + symbolicRefToTypeRegion = typeConstraints.symbolicRefToTypeRegion, + isExprToInterpretation = emptyList(), + ) + + val result = typeSolver.check(query) assertIs>(result) } with(pc.clone()) { this += mkHeapRefEq(a, c) and mkHeapRefEq(b1, c) - val result = solver.check(this, useSoftConstraints = false) + val result = solver.check(this) assertIs>>(result) } } @Test fun `Test symbolic ref -- expressions to assert correctness about null -- three equals`(): Unit = with(ctx) { - val a = ctx.mkRegisterReading(0, addressSort) - val b = ctx.mkRegisterReading(1, addressSort) - val c = ctx.mkRegisterReading(2, addressSort) + val a = mkRegisterReading(0, addressSort) + val b = mkRegisterReading(1, addressSort) + val c = mkRegisterReading(2, addressSort) - pc += mkIsExpr(a, interfaceAB) - pc += mkIsExpr(b, interfaceBC1) - pc += mkIsExpr(c, interfaceAC) + pc += mkIsSubtypeExpr(a, interfaceAB) + pc += mkIsSubtypeExpr(b, interfaceBC1) + pc += mkIsSubtypeExpr(c, interfaceAC) // it's overcomplicated a == c && b == c, so it's not leak to the UEqualityConstraints pc += (mkHeapRefEq(a, c) or mkHeapRefEq(b, c)) and (!mkHeapRefEq(a, c) or !mkHeapRefEq(b, c)).not() - val resultBeforeNotNullConstraints = solver.check(pc, useSoftConstraints = false) + val resultBeforeNotNullConstraints = solver.check(pc) val model = assertIs>>(resultBeforeNotNullConstraints).model assertIs>>(resultBeforeNotNullConstraints) @@ -254,26 +292,26 @@ class TypeSolverTest { pc += mkOrNoSimplify(mkHeapRefEq(a, nullRef).not(), falseExpr) - val resultWithNotNullConstraints = solver.check(pc, useSoftConstraints = false) + val resultWithNotNullConstraints = solver.check(pc) assertIs>>(resultWithNotNullConstraints) } @Test fun `Test symbolic ref -- expressions to assert correctness about null -- two equals`(): Unit = with(ctx) { - val a = ctx.mkRegisterReading(0, addressSort) - val b = ctx.mkRegisterReading(1, addressSort) - val c = ctx.mkRegisterReading(2, addressSort) + val a = mkRegisterReading(0, addressSort) + val b = mkRegisterReading(1, addressSort) + val c = mkRegisterReading(2, addressSort) - pc += mkIsExpr(a, interfaceAB) - pc += mkIsExpr(b, interfaceBC1) - pc += mkIsExpr(c, interfaceAC) + pc += mkIsSubtypeExpr(a, interfaceAB) + pc += mkIsSubtypeExpr(b, interfaceBC1) + pc += mkIsSubtypeExpr(c, interfaceAC) // it's overcomplicated a == b, so it's not leak to the UEqualityConstraints pc += mkOrNoSimplify(mkHeapRefEq(a, b), falseExpr) pc += mkOrNoSimplify(mkHeapRefEq(a, nullRef).not(), falseExpr) - val result = solver.check(pc, useSoftConstraints = false) + val result = solver.check(pc) val model = assertIs>>(result).model val concreteA = assertIs(model.eval(a)).address @@ -284,14 +322,12 @@ class TypeSolverTest { } @Test - fun `ite must not occur as refs in type constraints`() = with(ctx) { + fun `Symbolic ref -- ite must not occur as refs in type constraints`() = with(ctx) { val arr1 = mkRegisterReading(0, addressSort) val arr2 = mkRegisterReading(1, addressSort) - val val1 = mkConcreteHeapRef(1) - val val2 = mkConcreteHeapRef(2) - - val pc = UPathConstraints(ctx) + val val1 = memory.alloc(base2) + val val2 = memory.alloc(base2) pc += mkHeapRefEq(arr1, nullRef).not() pc += mkHeapRefEq(arr2, nullRef).not() @@ -312,67 +348,168 @@ class TypeSolverTest { val firstReading = inputRegion.read(arr1 to idx1) val secondReading = inputRegion.read(arr2 to idx2) - pc += mkIsExpr(arr1, base1) - pc += mkIsExpr(arr2, base1) - - pc.typeConstraints.allocate(val1.address, base2) - pc.typeConstraints.allocate(val2.address, base2) + pc += mkIsSubtypeExpr(arr1, base1) + pc += mkIsSubtypeExpr(arr2, base1) pc += mkHeapRefEq(firstReading, nullRef).not() pc += mkHeapRefEq(secondReading, nullRef).not() - pc += mkIsExpr(firstReading, base2) - pc += mkIsExpr(secondReading, base2) + pc += pc.typeConstraints.evalIsSubtype(firstReading, base2) + pc += pc.typeConstraints.evalIsSubtype(secondReading, base2) val fstFieldValue = heap.readField(firstReading, field, bv32Sort) val sndFieldValue = heap.readField(secondReading, field, bv32Sort) pc += fstFieldValue eq sndFieldValue - val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) - - val solver = USolverBase( - this, - KZ3Solver(this), - translator, - decoder, - softConstraintsProvider = USoftConstraintsProvider(this) - ) - - val status = solver.check(pc, useSoftConstraints = true) + val status = solver.check(pc) assertTrue { status is USatResult<*> } } @Test - @Disabled("Support propositional type variables") fun `Test symbolic ref -- not instance of constraint`(): Unit = with(ctx) { - val a = ctx.mkRegisterReading(0, addressSort) - pc += mkHeapRefEq(a, nullRef) or mkIsExpr(a, interfaceAB).not() - val result = solver.check(pc, useSoftConstraints = false) - assertIs>>(result) + val ref = mkRegisterReading(0, addressSort) + + pc += mkHeapRefEq(ref, nullRef) or mkIsSubtypeExpr(ref, interfaceAB).not() + assertIs>>(solver.check(pc)) + + pc += heapRefEq(ref, nullRef).not() and (mkIsSubtypeExpr(ref, a) or mkIsSubtypeExpr(ref, b)) + assertIs>(solver.check(pc)) } @Test - @Disabled("Support propositional type variables") fun `Test symbolic ref -- isExpr or bool variable`(): Unit = with(ctx) { - val a = ctx.mkRegisterReading(0, addressSort) - val unboundedBoolean = ctx.mkRegisterReading(1, boolSort) - pc += mkIsExpr(a, interfaceAB) xor unboundedBoolean - val result1 = solver.check(pc, useSoftConstraints = false) + val ref = mkRegisterReading(0, addressSort) + val unboundedBoolean = mkRegisterReading(1, boolSort) + pc += mkIsSubtypeExpr(ref, a) or mkIsSubtypeExpr(ref, b) or mkIsSubtypeExpr(ref, c) + pc += mkIsSubtypeExpr(ref, interfaceAB) xor unboundedBoolean + val result1 = solver.check(pc) assertIs>>(result1) pc += unboundedBoolean - val result2 = solver.check(pc, useSoftConstraints = false) + val result2 = solver.check(pc) val model = assertIs>>(result2).model - val concreteA = model.eval(a) as UConcreteHeapRef + val concreteA = model.eval(ref) as UConcreteHeapRef val types = model.typeStreamOf(concreteA) types.take100AndAssertEqualsToSetOf(c) } + @Test + fun `Test symbolic ref -- ite constraint`(): Unit = with(ctx) { + val ref1 = mkRegisterReading(0, addressSort) + val ref2 = mkRegisterReading(1, addressSort) + + val unboundedBoolean1 = mkRegisterReading(2, boolSort) + val unboundedBoolean2 = mkRegisterReading(3, boolSort) + + pc += mkHeapRefEq(ref1, nullRef).not() + pc += mkHeapRefEq(ref2, nullRef).not() + + val iteIsExpr1 = pc.typeConstraints.evalIsSubtype(mkIte(unboundedBoolean1, ref1, ref2), base1) + val iteIsExpr2 = pc.typeConstraints.evalIsSubtype(mkIte(unboundedBoolean2, ref1, ref2), base2) + + pc += iteIsExpr1 + pc += iteIsExpr2 + pc += ref1 neq ref2 + + val result = solver.check(pc) + val model = assertIs>>(result).model + + val concreteA = model.eval(ref1) + val concreteB = model.eval(ref2) + + assertNotEquals(model.typeStreamOf(concreteA).first(), model.typeStreamOf(concreteB).first()) + assertNotEquals(model.eval(unboundedBoolean1), model.eval(unboundedBoolean2)) + + pc += unboundedBoolean1 eq unboundedBoolean2 + + assertIs>(solver.check(pc)) + } + + @Test + fun `Test symbolic ref -- and supertype constraint`(): Unit = with(ctx) { + val ref = mkRegisterReading(0, addressSort) + + pc += mkIsSupertypeExpr(ref, derived1B) + pc += mkIsSupertypeExpr(ref, derived1A) + val model = assertIs>>(solver.check(pc)).model + + val concreteRef = model.eval(ref) as UConcreteHeapRef + + val typeStream = model.typeStreamOf(concreteRef) + + typeStream.take100AndAssertEqualsToSetOf(top, base1) + + pc += mkIsSupertypeExpr(ref, base1).not() + + assertIs>(solver.check(pc)) + } + + @Test + fun `Test symbolic ref -- or supertype constraint`(): Unit = with(ctx) { + val ref = mkRegisterReading(0, addressSort) + val cond = mkRegisterReading(1, boolSort) + + + pc += mkIte(cond, mkIsSupertypeExpr(ref, derived1B), mkIsSupertypeExpr(ref, derived1A)) + with(pc) { + val model = assertIs>>(solver.check(this)).model + + val concreteRef = model.eval(ref) as UConcreteHeapRef + val typeStream = model.typeStreamOf(concreteRef) + + if (model.eval(cond).isTrue) { + typeStream.take100AndAssertEqualsToSetOf(derived1B, base1, top) + } else { + typeStream.take100AndAssertEqualsToSetOf(derived1A, base1, top) + } + } + + pc += mkIsSupertypeExpr(ref, derived1B).not() + + with(pc) { + val model = assertIs>>(solver.check(this)).model + + val concreteRef = model.eval(ref) as UConcreteHeapRef + val typeStream = model.typeStreamOf(concreteRef) + + assertTrue(model.eval(cond).isFalse) + typeStream.take100AndAssertEqualsToSetOf(derived1A) + } + } + + @Test + fun `Test symbolic ref -- supertype and subtype constraint`(): Unit = with(ctx) { + val ref = mkRegisterReading(0, addressSort) + val cond = mkRegisterReading(1, boolSort) + + pc += mkIte(cond, mkIsSupertypeExpr(ref, derived1A), mkIsSupertypeExpr(ref, derived1B)) + pc += mkIte(cond, mkIsSubtypeExpr(ref, interface2), mkIsSubtypeExpr(ref, interface1)) + + assertIs>(solver.check(pc)) + } + + @Test + fun `Test symbolic ref -- exclude supertype and subtype`(): Unit = with(ctx) { + val ref = mkConcreteHeapRef(1) + pc.typeConstraints.allocate(ref.address, base1) + + with(pc.clone()) { + this += mkIsSubtypeExpr(ref, top).not() + assertTrue(isFalse) + } + + with(pc.clone()) { + this += mkIsSupertypeExpr(ref, derived1A).not() + assertTrue(isFalse) + } + + } + private fun UTypeStream.take100AndAssertEqualsToSetOf(vararg elements: T) { val set = elements.toSet() val result = take(100) - assertEquals(set.size, result.size) + assertEquals(set.size, result.size, result.toString()) assertEquals(set, result.toSet()) } -} \ No newline at end of file +} diff --git a/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt b/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt index ef981515cf..7a7142cbfb 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt @@ -7,15 +7,15 @@ import org.usvm.types.UTypeSystem object SingleTypeSystem : UTypeSystem { object SingleType - override fun isSupertype(u: SingleType, t: SingleType): Boolean = true + override fun isSupertype(supertype: SingleType, type: SingleType): Boolean = true - override fun isMultipleInheritanceAllowedFor(t: SingleType): Boolean = false + override fun isMultipleInheritanceAllowedFor(type: SingleType): Boolean = false - override fun isFinal(t: SingleType): Boolean = true + override fun isFinal(type: SingleType): Boolean = true - override fun isInstantiable(t: SingleType): Boolean = true + override fun isInstantiable(type: SingleType): Boolean = true - override fun findSubtypes(t: SingleType): Sequence = emptySequence() + override fun findSubtypes(type: SingleType): Sequence = emptySequence() override fun topTypeStream(): UTypeStream = USingleTypeStream(this, SingleType) } diff --git a/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt b/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt index 1253e55323..b7294ffae7 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt @@ -43,29 +43,29 @@ class TestTypeSystem : UTypeSystem { require(inheritorTypeSupertypes.count { !it.isMultipleInheritanceAllowed } <= 1) } - override fun isSupertype(u: TestType, t: TestType): Boolean { - if (u == t || u == topType) { + override fun isSupertype(supertype: TestType, type: TestType): Boolean { + if (supertype == type || supertype == topType) { return true } return typeToDirectSupertypes - .getOrElse(t) { return false } - .any { isSupertype(u, it) } + .getOrElse(type) { return false } + .any { isSupertype(supertype, it) } } - override fun isMultipleInheritanceAllowedFor(t: TestType): Boolean { - return t.isMultipleInheritanceAllowed + override fun isMultipleInheritanceAllowedFor(type: TestType): Boolean { + return type.isMultipleInheritanceAllowed } - override fun isFinal(t: TestType): Boolean { - return t.isFinal + override fun isFinal(type: TestType): Boolean { + return type.isFinal } - override fun isInstantiable(t: TestType): Boolean { - return t.isInstantiable + override fun isInstantiable(type: TestType): Boolean { + return type.isInstantiable } - override fun findSubtypes(t: TestType): Sequence { - return typeToDirectSubtypes.getOrDefault(t, hashSetOf()).asSequence() + override fun findSubtypes(type: TestType): Sequence { + return typeToDirectSubtypes.getOrDefault(type, hashSetOf()).asSequence() } override fun topTypeStream(): UTypeStream { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt index 63513aa8f5..3f313e2f9e 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt @@ -48,7 +48,7 @@ import org.usvm.machine.state.JcState import org.usvm.machine.state.localIdx import org.usvm.memory.UReadOnlySymbolicMemory import org.usvm.model.UModelBase -import org.usvm.types.takeFirst +import org.usvm.types.firstOrNull /** * A class, responsible for resolving a single [JcTest] for a specific method from a symbolic state. @@ -172,16 +172,27 @@ class JcTestResolver( if (ref.address == NULL_ADDRESS) { return null } + // to find a type, we need to understand the source of the object + val typeStream = if (ref.address <= INITIAL_INPUT_ADDRESS) { + // input object + model.typeStreamOf(ref) + } else { + // allocated object + memory.typeStreamOf(ref) + }.filterBySupertype(type) + + // We filter allocated object type stream, because it could be stored in the input array, + // which resolved to a wrong type, since we do not build connections between element types + // and array types right now. + // In such cases, we need to resolve this element to null. + + val evaluatedType = typeStream.firstOrNull() ?: return null + + // We check for the type stream emptiness firsly and only then for the resolved cache, + // because even if the object is already resolved, it could be incompatible with the [type], if it + // is an element of an array of the wrong type. + return resolvedCache.getOrElse(ref.address) { - // to find a type, we need to understand the source of the object - val evaluatedType = if (ref.address <= INITIAL_INPUT_ADDRESS) { - // input object - val typeStream = model.typeStreamOf(ref).filterBySupertype(type) - typeStream.takeFirst() as JcRefType - } else { - // allocated object - memory.typeStreamOf(ref).takeFirst() - } when (evaluatedType) { is JcArrayType -> resolveArray(ref, heapRef, evaluatedType) is JcClassType -> resolveObject(ref, heapRef, evaluatedType) @@ -216,13 +227,16 @@ class JcTestResolver( // TODO: works incorrectly for inner array val clazz = resolveType(type.elementType as JcRefType) val instance = Reflection.allocateArray(clazz, length) + resolvedCache[ref.address] = instance for (i in 0 until length) { instance[i] = resolveElement(i) } instance } } - resolvedCache[ref.address] = instance + if (type.elementType is JcPrimitiveType) { + resolvedCache[ref.address] = instance + } return instance } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt index cbf78d994b..919506da8f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt @@ -11,6 +11,7 @@ import org.usvm.UContext import org.usvm.model.buildTranslatorAndLazyDecoder import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase +import org.usvm.solver.UTypeSolver class JcComponents( private val typeSystem: JcTypeSystem, @@ -26,8 +27,9 @@ class JcComponents( SolverType.YICES -> KYicesSolver(ctx) SolverType.Z3 -> KZ3Solver(ctx) } + val typeSolver = UTypeSolver(typeSystem) closeableResources += smtSolver - return USolverBase(ctx, smtSolver, translator, decoder, softConstraintsProvider) + return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, softConstraintsProvider) } fun close() { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt index 90aca00597..11c3ca63da 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt @@ -295,7 +295,7 @@ class JcExprResolver( val ref = resolveJcExpr(expr.operand)?.asExpr(addressSort) ?: return null scope.calcOnState { val notEqualsNull = mkHeapRefEq(ref, memory.heap.nullRef()).not() - val isExpr = memory.types.evalIs(ref, expr.targetType) + val isExpr = memory.types.evalIsSubtype(ref, expr.targetType) mkAnd(notEqualsNull, isExpr) } } @@ -510,7 +510,7 @@ class JcExprResolver( ref = classRef ) - private fun resolveArrayAccess(array: JcValue, index: JcValue): ULValue? = with(ctx) { + private fun resolveArrayAccess(array: JcValue, index: JcValue): UArrayIndexLValue? = with(ctx) { val arrayRef = resolveJcExpr(array)?.asExpr(addressSort) ?: return null checkNullPointer(arrayRef) ?: return null @@ -530,7 +530,7 @@ class JcExprResolver( return UArrayIndexLValue(cellSort, arrayRef, idx, arrayDescriptor) } - private fun resolveLocal(local: JcLocal): ULValue { + private fun resolveLocal(local: JcLocal): URegisterLValue { val method = requireNotNull(scope.calcOnState { lastEnteredMethod }) val localIdx = localToIdx(method, local) val sort = ctx.typeToSort(local.type) @@ -658,7 +658,7 @@ class JcExprResolver( type: JcRefType, ): UExpr? { return if (!typeBefore.isAssignable(type)) { - val isExpr = scope.calcOnState { memory.types.evalIs(expr.asExpr(ctx.addressSort), type) } + val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr.asExpr(ctx.addressSort), type) } ?: return null scope.fork( isExpr, diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt index 1ff9d28f85..691205451e 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt @@ -66,7 +66,7 @@ class JcInterpreter( val thisLValue = URegisterLValue(addressSort, 0) val ref = state.memory.read(thisLValue).asExpr(addressSort) state.pathConstraints += mkEq(ref, nullRef).not() - state.pathConstraints += mkIsExpr(ref, typedMethod.enclosingType) + state.pathConstraints += mkIsSubtypeExpr(ref, typedMethod.enclosingType) } } @@ -76,14 +76,14 @@ class JcInterpreter( if (type is JcRefType) { val argumentLValue = URegisterLValue(typeToSort(type), method.localIdx(idx)) val ref = state.memory.read(argumentLValue).asExpr(addressSort) - state.pathConstraints += mkIsExpr(ref, type) + state.pathConstraints += mkIsSubtypeExpr(ref, type) } } } val solver = ctx.solver() - val model = (solver.check(state.pathConstraints, useSoftConstraints = true) as USatResult).model + val model = (solver.checkWithSoftConstraints(state.pathConstraints) as USatResult).model state.models = listOf(model) return state @@ -143,7 +143,7 @@ class JcInterpreter( val throwableTypes = catchInst.throwableTypes val typeConstraint = scope.calcOnState { - val currentTypeConstraints = throwableTypes.map { memory.types.evalIs(exception.address, it) } + val currentTypeConstraints = throwableTypes.map { memory.types.evalIsSubtype(exception.address, it) } val result = ctx.mkAnd(typeConstraintsNegations + ctx.mkOr(currentTypeConstraints)) typeConstraintsNegations += currentTypeConstraints.map { ctx.mkNot(it) } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt index f8c2ae7a78..944793576f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt @@ -19,28 +19,41 @@ class JcTypeSystem( ) : UTypeSystem { private val hierarchy = HierarchyExtensionImpl(cp) - override fun isSupertype(u: JcType, t: JcType): Boolean = - t.isAssignable(u) + override fun isSupertype(supertype: JcType, type: JcType): Boolean = + type.isAssignable(supertype) - override fun isMultipleInheritanceAllowedFor(t: JcType): Boolean = - (t as? JcClassType)?.jcClass?.isInterface ?: false + override fun isMultipleInheritanceAllowedFor(type: JcType): Boolean = + (type as? JcClassType)?.jcClass?.isInterface ?: false - override fun isFinal(t: JcType): Boolean = - (t as? JcClassType)?.isFinal ?: false + override fun isFinal(type: JcType): Boolean = + (type as? JcClassType)?.isFinal ?: false - override fun isInstantiable(t: JcType): Boolean = - t !is JcRefType || (!t.jcClass.isInterface && !t.jcClass.isAbstract) + override fun isInstantiable(type: JcType): Boolean = + type !is JcRefType || (!type.jcClass.isInterface && !type.jcClass.isAbstract) // TODO: deal with generics // TODO: handle object type, serializable and cloneable - override fun findSubtypes(t: JcType): Sequence = when (t) { + override fun findSubtypes(type: JcType): Sequence = when (type) { is JcPrimitiveType -> emptySequence() // TODO: should not be called here - is JcArrayType -> findSubtypes(t.elementType).map { cp.arrayTypeOf(it) } + is JcArrayType -> findSubtypes(type.elementType).map { cp.arrayTypeOf(it) } is JcRefType -> hierarchy - .findSubClasses(t.jcClass, allHierarchy = false) // TODO: prioritize classes somehow and filter bad classes + .findSubClasses( + type.jcClass, + allHierarchy = false + ) // TODO: prioritize classes somehow and filter bad classes .map { it.toType() } - - else -> error("Unknown type $t") + .run { + if (type == cp.objectType) { + // since we use DFS iterator, the array of objects should come last + // here we return only the direct successors, so (2,3,...)-dimensional arrays isn't returned here + // such arrays are subtypes of `Object[]` + flatMap { listOf(it, cp.arrayTypeOf(it)) } + sequenceOf(cp.arrayTypeOf(type)) + } else { + this + } + } + + else -> error("Unknown type $type") } private val topTypeStream by lazy { USupportTypeStream.from(this, cp.objectType) } diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/casts/InstanceOfExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/casts/InstanceOfExample.java index 12b9b9629b..2a76bd4cf2 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/casts/InstanceOfExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/casts/InstanceOfExample.java @@ -112,8 +112,9 @@ public int instanceOfAsPartOfInternalExpressionsCastClass(Object[] objectExample } public int instanceOfAsPartOfInternalExpressionsXor(Object[] objectExample) { - assume(objectExample != null); - assume(objectExample.length == 2); + if (objectExample == null || objectExample.length != 2) { + return 0; + } boolean isElem0SecondSucc = objectExample[0] instanceof CastClassSecondSucc[]; boolean isElem1FirstSucc = objectExample[1] instanceof CastClassFirstSucc[]; @@ -135,8 +136,9 @@ public int instanceOfAsPartOfInternalExpressionsXor(Object[] objectExample) { } public int instanceOfAsPartOfInternalExpressionsXorInverse(Object[] objectExample) { - assume(objectExample != null); - assume(objectExample.length == 2); + if (objectExample == null || objectExample.length != 2) { + return 0; + } boolean isElem0SecondSucc = objectExample[0] instanceof CastClassSecondSucc[]; boolean isElem1FirstSucc = objectExample[1] instanceof CastClassFirstSucc[]; diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/objects/HiddenFieldExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/objects/HiddenFieldExample.java index e7b38c26fd..c7b1544d18 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/objects/HiddenFieldExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/objects/HiddenFieldExample.java @@ -1,10 +1,10 @@ package org.usvm.samples.objects; -import static org.usvm.api.mock.UMockKt.assume; - public class HiddenFieldExample { public int checkHiddenField(HiddenFieldSuperClass o) { - assume(!(o instanceof HiddenFieldSuccClass)); + if (o instanceof HiddenFieldSuccClass) { + return 0; + } if (o.a == 1 && o.b == 2) { return 1; diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/types/PathDependentGenericsExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/types/PathDependentGenericsExample.java index e38cc908e4..77d9813b39 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/types/PathDependentGenericsExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/types/PathDependentGenericsExample.java @@ -42,11 +42,11 @@ private void functionWithSeveralGenerics(List firstValu } private void functionWithOneGeneric(ClassWithOneGeneric value) { - System.out.println(); + } private void functionWithTwoGenerics(ClassWithTwoGenerics value) { - System.out.println(); + } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt index 0ca41f85b3..cb128c866a 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/CastClassTest.kt @@ -9,7 +9,7 @@ import org.usvm.test.util.checkers.eq internal class CastClassTest : JavaMethodTestRunner() { @Test - @Disabled("Support instanceof") + @Disabled("Support assumptions") fun testThisTypeChoice() { checkDiscoveredProperties( CastClass::castToInheritor, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt index c95de1f41a..9301ca68e2 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt @@ -7,8 +7,6 @@ import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ge import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults - -@Disabled("Support instanceof") internal class InstanceOfExampleTest : JavaMethodTestRunner() { @Test fun testSimpleInstanceOf() { @@ -53,6 +51,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test + @Disabled("Support virtual calls") fun testVirtualCallWithoutOneInheritor() { checkDiscoveredProperties( InstanceOfExample::virtualCallWithoutOneInheritor, @@ -65,6 +64,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test + @Disabled("Support virtual calls") fun testVirtualCallWithoutOneInheritorInverse() { checkDiscoveredProperties( InstanceOfExample::virtualCallWithoutOneInheritorInverse, @@ -165,7 +165,8 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { fun testInstanceOfAsPartOfInternalExpressionsXor() { checkDiscoveredProperties( InstanceOfExample::instanceOfAsPartOfInternalExpressionsXor, - eq(4), + eq(5), + { _, o, r -> (o == null || o.size != 2) && r == 0 }, { _, o, r -> val o0isSecond = o[0].isInstanceOfArray() val o1isFirst = o[1].isInstanceOfArray() @@ -193,7 +194,8 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { fun testInstanceOfAsPartOfInternalExpressionsXorInverse() { checkDiscoveredProperties( InstanceOfExample::instanceOfAsPartOfInternalExpressionsXorInverse, - eq(4), + eq(5), + { _, o, r -> (o == null || o.size != 2) && r == 0 }, { _, o, r -> val o0isSecond = o[0].isInstanceOfArray() val o1isFirst = o[1].isInstanceOfArray() @@ -234,7 +236,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test - @Disabled("Unexpected lvalue org.usvm.machine.JcStaticFieldRef@74414a78") + @Disabled("An operation is not implemented: Support collections") fun testInstanceOfAsInternalExpressionsMap() { checkDiscoveredProperties( InstanceOfExample::instanceOfAsInternalExpressionsMap, @@ -247,9 +249,8 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { fun testSymbolicInstanceOf() { checkDiscoveredProperties( InstanceOfExample::symbolicInstanceOf, - eq(6), - { _, _, i, r -> i < 1 && r == null }, - { _, _, i, r -> i > 3 && r == null }, + eq(5), + { _, _, i, r -> (i < 1 || i > 3) && r == null }, { _, o, _, _ -> o == null }, { _, o, i, _ -> o != null && i > o.lastIndex }, { _, o, i, r -> o != null && o[i] is CastClassFirstSucc && r is CastClassFirstSucc }, @@ -258,14 +259,12 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() { } @Test + @Disabled("Support virtual calls") fun testComplicatedInstanceOf() { checkDiscoveredProperties( InstanceOfExample::complicatedInstanceOf, - eq(8), - { _, _, index, _, result -> index < 0 && result == null }, - { _, _, index, _, result -> index > 2 && result == null }, - { _, objects, index, _, result -> index in 0..2 && objects == null && result == null }, - { _, objects, index, _, result -> index in 0..2 && objects != null && objects.size < index + 2 && result == null }, + ge(5), + { _, objects, index, _, result -> (index !in 0..2 || objects == null || objects.size >= index + 2) && result == null }, { _, objects, index, objectExample, result -> require(objects != null && result != null && objectExample is CastClassFirstSucc) diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/HiddenFieldExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/HiddenFieldExampleTest.kt index 2bbdc122c0..5c2e969a81 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/HiddenFieldExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/HiddenFieldExampleTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.objects -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -8,12 +7,12 @@ import org.usvm.test.util.checkers.eq internal class HiddenFieldExampleTest : JavaMethodTestRunner() { @Test - @Disabled("Support instanceof") fun testCheckHiddenField() { checkDiscoveredProperties( HiddenFieldExample::checkHiddenField, - eq(4), + eq(5), { _, o, _ -> o == null }, + { _, o, r -> o is HiddenFieldSuccClass && r == 0 }, { _, o, r -> o != null && o.a != 1 && r == 2 }, { _, o, r -> o != null && o.a == 1 && o.b != 2 && r == 2 }, { _, o, r -> o != null && o.a == 1 && o.b == 2 && r == 1 }, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt index 812663d6e7..defc847db7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/StandardStructuresTest.kt @@ -9,7 +9,7 @@ import java.util.TreeMap internal class StandardStructuresTest : JavaMethodTestRunner() { @Test - @Disabled("Support instanceof") + @Disabled("Support creation of collections") fun testGetList() { checkDiscoveredProperties( StandardStructures::getList, @@ -24,7 +24,7 @@ internal class StandardStructuresTest : JavaMethodTestRunner() { } @Test - @Disabled("Support instanceof") + @Disabled("Support creation of collections") fun testGetMap() { checkDiscoveredProperties( StandardStructures::getMap, @@ -36,7 +36,7 @@ internal class StandardStructuresTest : JavaMethodTestRunner() { } @Test - @Disabled("Support instanceof") + @Disabled("Support creation of collections") fun testGetDeque() { checkDiscoveredProperties( StandardStructures::getDeque, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/types/PathDependentGenericsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/types/PathDependentGenericsExampleTest.kt index ea69b05a5a..03e663c59d 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/types/PathDependentGenericsExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/types/PathDependentGenericsExampleTest.kt @@ -8,7 +8,6 @@ import org.usvm.test.util.checkers.eq internal class PathDependentGenericsExampleTest : JavaMethodTestRunner() { @Test - @Disabled("Support instanceof") fun testPathDependentGenerics() { checkDiscoveredProperties( PathDependentGenericsExample::pathDependentGenerics, diff --git a/usvm-jvm/src/test/resources/logback.xml b/usvm-jvm/src/test/resources/logback.xml index cf11c9cba0..21170a981d 100644 --- a/usvm-jvm/src/test/resources/logback.xml +++ b/usvm-jvm/src/test/resources/logback.xml @@ -6,7 +6,7 @@ - + \ No newline at end of file diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleLanguageComponents.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleLanguageComponents.kt index 8820179b35..49366bf5ee 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleLanguageComponents.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleLanguageComponents.kt @@ -5,13 +5,14 @@ import io.ksmt.solver.z3.KZ3Solver import org.usvm.SolverType import org.usvm.UComponents import org.usvm.UContext -import org.usvm.types.UTypeSystem import org.usvm.language.Field import org.usvm.language.Method import org.usvm.language.SampleType import org.usvm.model.buildTranslatorAndLazyDecoder import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase +import org.usvm.solver.UTypeSolver +import org.usvm.types.UTypeSystem class SampleLanguageComponents( private val typeSystem: SampleTypeSystem, @@ -27,7 +28,8 @@ class SampleLanguageComponents( SolverType.Z3 -> KZ3Solver(ctx) } - return USolverBase(ctx, solver, translator, decoder, softConstraintsProvider) + val typeSolver = UTypeSolver(typeSystem) + return USolverBase(ctx, solver, typeSolver, translator, decoder, softConstraintsProvider) } override fun mkTypeSystem(ctx: UContext): UTypeSystem = typeSystem diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt index 2d0329512e..3fd0e42acf 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt @@ -6,15 +6,15 @@ import org.usvm.types.UTypeSystem import org.usvm.types.emptyTypeStream class SampleTypeSystem : UTypeSystem { - override fun isSupertype(u: SampleType, t: SampleType): Boolean = - u == t + override fun isSupertype(supertype: SampleType, type: SampleType): Boolean = + supertype == type - override fun isFinal(t: SampleType): Boolean = true + override fun isFinal(type: SampleType): Boolean = true - override fun isMultipleInheritanceAllowedFor(t: SampleType): Boolean = false - override fun isInstantiable(t: SampleType): Boolean = true + override fun isMultipleInheritanceAllowedFor(type: SampleType): Boolean = false + override fun isInstantiable(type: SampleType): Boolean = true - override fun findSubtypes(t: SampleType): Sequence = emptySequence() + override fun findSubtypes(type: SampleType): Sequence = emptySequence() override fun topTypeStream(): UTypeStream = emptyTypeStream