Skip to content

Commit

Permalink
more or less final version of AbstractDomainSolver
Browse files Browse the repository at this point in the history
  • Loading branch information
@AbdullinAM
AbdullinAM committed Nov 9, 2023
1 parent c1debf6 commit ed71aaa
Show file tree
Hide file tree
Showing 3 changed files with 82 additions and 37 deletions.
5 changes: 0 additions & 5 deletions kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,11 +166,6 @@ class AsyncChecker(
val result = AsyncSMTProxySolver(ctx).use {
it.isPathPossibleAsync(state, query)
}
// val aiResult = tryAbstractDomainSolve(state, query)
// if (aiResult is Result.UnsatResult && result !is Result.UnsatResult) {
// val a = tryAbstractDomainSolve(state, query)
// log.error("AAAAAAAAAAAA")
// }
log.debug("Acquired {}", result)
return result
}
Expand Down
87 changes: 75 additions & 12 deletions ...runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomain.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,14 @@ val AbstractDomainValue.isFalse: Boolean
val AbstractDomainValue.isNull: Boolean
get() = this is NullDomainValue

val AbstractDomainValue.canBeNull: Boolean
get() = when (this) {
is NullDomainValue -> true
is NullableDomainValue -> true
is Top -> true
else -> false
}

val AbstractDomainValue.isConstant: Boolean
get() = this is IntervalDomainValue<*> && this.isConstant

Expand Down Expand Up @@ -233,21 +241,71 @@ data class IntervalDomainValue<T : Number>(val min: T, val max: T) : NumberAbstr

override fun assign(other: AbstractDomainValue): AbstractDomainValue = other

@Suppress("UNCHECKED_CAST")
private fun <T : Number> lowerBound(num: T): T = when (num) {
is Byte -> Byte.MIN_VALUE
is Short -> Short.MIN_VALUE
is Int -> Int.MIN_VALUE
is Long -> Long.MIN_VALUE
is Float -> Float.NEGATIVE_INFINITY
is Double -> Double.NEGATIVE_INFINITY
else -> unreachable { log.error("Unknown number impl $num") }
} as T

@Suppress("UNCHECKED_CAST")
private fun <T : Number> upperBound(num: T) = when (num) {
is Byte -> Byte.MAX_VALUE
is Short -> Short.MAX_VALUE
is Int -> Int.MAX_VALUE
is Long -> Long.MAX_VALUE
is Float -> Float.POSITIVE_INFINITY
is Double -> Double.POSITIVE_INFINITY
else -> unreachable { log.error("Unknown number impl $num") }
} as T

override fun apply(opcode: BinaryOpcode, other: AbstractDomainValue): AbstractDomainValue = when (other) {
is Top -> Top

is IntervalDomainValue<*> -> when (opcode) {
BinaryOpcode.ADD -> IntervalDomainValue(other.min + other.min, max + other.max)
BinaryOpcode.SUB -> IntervalDomainValue(min - other.max, max + other.min)
BinaryOpcode.MUL -> IntervalDomainValue(
minOf(min * other.min, max * other.min, min * other.max, max * other.max),
maxOf(min * other.min, max * other.min, min * other.max, max * other.max)
)

BinaryOpcode.DIV -> IntervalDomainValue(
minOf(min / other.min, max / other.min, min / other.max, max / other.max),
maxOf(min / other.min, max / other.min, min / other.max, max / other.max)
)
BinaryOpcode.ADD -> {
val lb = min + other.min
val ub = max + other.max
when {
lb < min || lb < other.min -> IntervalDomainValue(lowerBound(min), upperBound(max))
ub < max || ub < other.max -> IntervalDomainValue(lowerBound(min), upperBound(max))
else -> IntervalDomainValue(lb, ub)
}
}

BinaryOpcode.SUB -> {
val lb = min - other.max
val ub = max - other.min
when {
lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
else -> IntervalDomainValue(lb, ub)
}
}

BinaryOpcode.MUL -> {
val lb = minOf(min * other.min, max * other.min, min * other.max, max * other.max)
val ub = maxOf(min * other.min, max * other.min, min * other.max, max * other.max)
when {
lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
else -> IntervalDomainValue(lb, ub)
}
}

BinaryOpcode.DIV -> {
val lb = minOf(min / other.min, max / other.min, min / other.max, max / other.max)
val ub = maxOf(min / other.min, max / other.min, min / other.max, max / other.max)
when {
lb > min -> IntervalDomainValue(lowerBound(min), upperBound(max))
ub < max -> IntervalDomainValue(lowerBound(min), upperBound(max))
else -> IntervalDomainValue(lb, ub)
}
}

BinaryOpcode.REM -> when {
this.isConstant && other.isConstant -> IntervalDomainValue(min % other.min)
Expand Down Expand Up @@ -607,7 +665,11 @@ sealed interface TermDomainValue : AbstractDomainValue {
else -> unreachable { log.error("$this == $other is unexpected satisfiability check") }
}

override fun satisfiesType(type: Type): AbstractDomainValue = this.type.satisfiesType(type)
override fun satisfiesType(type: Type): AbstractDomainValue = when {
nullity.isNull -> DomainStorage.falseDomain
nullity.canBeNull -> Top
else -> this.type.satisfiesType(type)
}
}

data class PtrDomainValue(
Expand Down Expand Up @@ -664,6 +726,7 @@ data class ArrayDomainValue(
nullity.join(other.nullity),
type.join(other.type)
)

is ArrayDomainValue -> ArrayDomainValue(
nullity.join(other.nullity),
type.join(other.type),
Expand Down
27 changes: 7 additions & 20 deletions .../src/main/kotlin/org/vorpal/research/kex/state/transformer/domain/AbstractDomainSolver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ import org.vorpal.research.kex.state.term.CmpTerm
import org.vorpal.research.kex.state.term.InstanceOfTerm
import org.vorpal.research.kex.state.term.NegTerm
import org.vorpal.research.kex.state.term.Term
import org.vorpal.research.kex.state.term.ValueTerm
import org.vorpal.research.kex.state.term.term
import org.vorpal.research.kex.state.transformer.ConstantPropagator
import org.vorpal.research.kex.state.transformer.IncrementalTransformer
Expand Down Expand Up @@ -228,7 +227,6 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
rhv.isTrue -> propagateInstanceOfCondition(condition, true)
rhv.isFalse -> propagateInstanceOfCondition(condition, false)
}
is ValueTerm -> propagateCondition(condition)
}
}
}
Expand All @@ -243,6 +241,9 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
val lhv = domainValue(predicate.lhv)
val rhv = domainValue(predicate.rhv)
satisfiabilityDomainValue = satisfiabilityDomainValue.meet(lhv.satisfiesInequality(rhv))
if (satisfiabilityDomainValue.isSat) {
propagateCmpCondition(term { predicate.lhv neq predicate.rhv } as CmpTerm)
}
}
}
return predicate
Expand All @@ -262,20 +263,14 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
}
} as CmpTerm

private fun propagateCondition(term: Term) {
System.err.println(term)
}

private fun propagateCmpCondition(term: CmpTerm) {
val lhv = storageValue(term.lhv)
val rhv = storageValue(term.rhv)
when {
term.lhv.type is KexPointer && rhv.value.isNull -> when (term.opcode) {
CmpOpcode.EQ -> lhv.value.assign(NullDomainValue)
CmpOpcode.NEQ -> lhv.value.assign(NonNullableDomainValue)
else -> {
log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
}
else -> {}
}

term.lhv.type is KexInteger && rhv.value.isConstant -> when (term.opcode) {
Expand All @@ -296,9 +291,7 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
)
)

else -> {
log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
}
else -> {}
}

CmpOpcode.GT, CmpOpcode.GE -> when (val lhvValue = lhv.value) {
Expand All @@ -316,14 +309,10 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
)
)

else -> {
log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
}
else -> {}
}

else -> {
log.error("Could not propagate cmp condition $term for ${lhv.value} and ${rhv.value}")
}
else -> {}
}
}
}
Expand All @@ -332,8 +321,6 @@ class AbstractDomainSolver(val ctx: ExecutionContext) : Transformer<AbstractDoma
val operand = storageValue(term.operand)
if (positive) {
operand.value.assign(TypeDomainValue(term.checkedType.getKfgType(ctx.types)))
} else {
log.error("Could not propagate cmp condition $term for ${operand.value}")
}
}

Expand Down

0 comments on commit ed71aaa

Please sign in to comment.