Skip to content

Commit 90270d3

Browse files
CaelmBleiddLipen
CaelmBleidd
and
Lipen
authored
Input arrays support (#285)
--------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent 76fd962 commit 90270d3

17 files changed

Lines changed: 758 additions & 141 deletions

File tree

‎usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,6 @@ class TsContext(
5252
val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
5353
val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
5454

55-
5655
/**
5756
* In TS we treat undefined value as a null reference in other objects.
5857
* For real null represented in the language we create another reference.
@@ -77,14 +76,15 @@ class TsContext(
7776
else -> TODO("${type::class.simpleName} is not yet supported: $type")
7877
}
7978

80-
// TODO: for now, ALL descriptors for array are UNKNOWN
81-
// in order to make ALL reading/writing, including '.length' access consistent
82-
// and possible in cases when the array type is not known.
83-
// For example, when we access '.length' of some array, we do not care about its type,
84-
// but we HAVE TO use some type consistent with the type used when this array was created.
85-
// Note: Using UnknownType everywhere does not lead to any errors yet,
86-
// since we do not rely on array types in any way.
87-
fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType
79+
fun arrayDescriptorOf(type: EtsArrayType): EtsType {
80+
return when (type.elementType) {
81+
is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1)
82+
is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1)
83+
is EtsArrayType -> TODO("Unsupported yet: $type")
84+
is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1)
85+
else -> EtsArrayType(EtsUnknownType, dimensions = 1)
86+
}
87+
}
8888

8989
fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType {
9090
check(isFakeObject())

‎usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ import org.usvm.statistics.UMachineObserver
2323
import org.usvm.statistics.collectors.AllStatesCollector
2424
import org.usvm.statistics.collectors.CoveredNewStatesCollector
2525
import org.usvm.statistics.collectors.TargetsReachedStatesCollector
26+
import org.usvm.statistics.constraints.SoftConstraintsObserver
2627
import org.usvm.statistics.distances.CfgStatisticsImpl
2728
import org.usvm.statistics.distances.PlainCallGraphStatistics
2829
import org.usvm.stopstrategies.createStopStrategy
@@ -94,6 +95,10 @@ class TsMachine(
9495
val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
9596
observers.add(statesCollector)
9697

98+
if (options.useSoftConstraints) {
99+
observers.add(SoftConstraintsObserver())
100+
}
101+
97102
val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
98103

99104
val stopStrategy = createStopStrategy(

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt‎

Lines changed: 133 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
55
import mu.KotlinLogging
66
import org.jacodb.ets.model.EtsAddExpr
77
import org.jacodb.ets.model.EtsAndExpr
8+
import org.jacodb.ets.model.EtsAnyType
89
import org.jacodb.ets.model.EtsArrayAccess
910
import org.jacodb.ets.model.EtsArrayType
1011
import org.jacodb.ets.model.EtsAwaitExpr
@@ -14,6 +15,7 @@ import org.jacodb.ets.model.EtsBitNotExpr
1415
import org.jacodb.ets.model.EtsBitOrExpr
1516
import org.jacodb.ets.model.EtsBitXorExpr
1617
import org.jacodb.ets.model.EtsBooleanConstant
18+
import org.jacodb.ets.model.EtsBooleanType
1719
import org.jacodb.ets.model.EtsCastExpr
1820
import org.jacodb.ets.model.EtsConstant
1921
import org.jacodb.ets.model.EtsDeleteExpr
@@ -44,6 +46,7 @@ import org.jacodb.ets.model.EtsNotExpr
4446
import org.jacodb.ets.model.EtsNullConstant
4547
import org.jacodb.ets.model.EtsNullishCoalescingExpr
4648
import org.jacodb.ets.model.EtsNumberConstant
49+
import org.jacodb.ets.model.EtsNumberType
4750
import org.jacodb.ets.model.EtsOrExpr
4851
import org.jacodb.ets.model.EtsParameterRef
4952
import org.jacodb.ets.model.EtsPostDecExpr
@@ -77,15 +80,16 @@ import org.jacodb.ets.utils.getDeclaredLocals
7780
import org.usvm.UAddressSort
7881
import org.usvm.UBoolExpr
7982
import org.usvm.UBoolSort
83+
import org.usvm.UConcreteHeapRef
8084
import org.usvm.UExpr
8185
import org.usvm.UHeapRef
8286
import org.usvm.USort
8387
import org.usvm.api.allocateArray
8488
import org.usvm.dataflow.ts.infer.tryGetKnownType
8589
import org.usvm.dataflow.ts.util.type
86-
import org.usvm.isTrue
8790
import org.usvm.machine.TsConcreteMethodCallStmt
8891
import org.usvm.machine.TsContext
92+
import org.usvm.machine.TsSizeSort
8993
import org.usvm.machine.TsVirtualMethodCallStmt
9094
import org.usvm.machine.interpreter.TsStepScope
9195
import org.usvm.machine.interpreter.isInitialized
@@ -590,6 +594,9 @@ class TsExprResolver(
590594

591595
override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
592596
val array = resolve(value.array)?.asExpr(addressSort) ?: return null
597+
598+
checkUndefinedOrNullPropertyRead(array) ?: return null
599+
593600
val index = resolve(value.index)?.asExpr(fp64Sort) ?: return null
594601
val bvIndex = mkFpToBvExpr(
595602
roundingMode = fpRoundingModeSortDefaultValue(),
@@ -598,20 +605,73 @@ class TsExprResolver(
598605
isSigned = true,
599606
).asExpr(sizeSort)
600607

601-
val lValue = mkArrayIndexLValue(
602-
sort = addressSort,
603-
ref = array,
604-
index = bvIndex,
605-
type = value.array.type as EtsArrayType
606-
)
607-
val expr = scope.calcOnState { memory.read(lValue) }
608+
val arrayType = value.array.type as? EtsArrayType
609+
?: error("Expected EtsArrayType, but got ${value.array.type}")
610+
val sort = typeToSort(arrayType.elementType)
611+
612+
val lengthLValue = mkArrayLengthLValue(array, arrayType)
613+
val length = scope.calcOnState { memory.read(lengthLValue) }
614+
615+
checkNegativeIndexRead(bvIndex) ?: return null
616+
checkReadingInRange(bvIndex, length) ?: return null
617+
618+
val expr = if (sort is TsUnresolvedSort) {
619+
// Concrete arrays with the unresolved sort should consist of fake objects only.
620+
if (array is UConcreteHeapRef) {
621+
// Read a fake object from the array.
622+
val lValue = mkArrayIndexLValue(
623+
sort = addressSort,
624+
ref = array,
625+
index = bvIndex,
626+
type = arrayType
627+
)
628+
629+
scope.calcOnState { memory.read(lValue) }
630+
} else {
631+
// If the array is not concrete, we need to allocate a fake object
632+
val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
633+
val boolLValue = mkArrayIndexLValue(boolSort, array, bvIndex, boolArrayType)
634+
635+
val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
636+
val fpLValue = mkArrayIndexLValue(fp64Sort, array, bvIndex, numberArrayType)
637+
638+
val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
639+
val refLValue = mkArrayIndexLValue(addressSort, array, bvIndex, unknownArrayType)
640+
641+
scope.calcOnState {
642+
val boolValue = memory.read(boolLValue)
643+
val fpValue = memory.read(fpLValue)
644+
val refValue = memory.read(refLValue)
645+
646+
// Read an object from the memory at first,
647+
// we don't need to recreate it if it is already a fake object.
648+
val fakeObj = if (refValue.isFakeObject()) {
649+
refValue
650+
} else {
651+
mkFakeValue(scope, boolValue, fpValue, refValue).also {
652+
lValuesToAllocatedFakeObjects += refLValue to it
653+
}
654+
}
655+
656+
memory.write(refLValue, fakeObj.asExpr(addressSort), guard = trueExpr)
608657

609-
check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
658+
fakeObj
659+
}
660+
}
661+
} else {
662+
val lValue = mkArrayIndexLValue(
663+
sort = sort,
664+
ref = array,
665+
index = bvIndex,
666+
type = arrayType
667+
)
668+
scope.calcOnState { memory.read(lValue) }
669+
}
610670

611671
return expr
612672
}
613673

614-
private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
674+
fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
615675
val neqNull = mkAnd(
616676
mkHeapRefEq(instance, mkUndefinedValue()).not(),
617677
mkHeapRefEq(instance, mkTsNullValue()).not()
@@ -623,6 +683,24 @@ class TsExprResolver(
623683
)
624684
}
625685

686+
fun checkNegativeIndexRead(index: UExpr<TsSizeSort>) = with(ctx) {
687+
val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0))
688+
689+
scope.fork(
690+
condition,
691+
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
692+
)
693+
}
694+
695+
fun checkReadingInRange(index: UExpr<TsSizeSort>, length: UExpr<TsSizeSort>) = with(ctx) {
696+
val condition = mkBvSignedLessExpr(index, length)
697+
698+
scope.fork(
699+
condition,
700+
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
701+
)
702+
}
703+
626704
private fun allocateException(type: EtsType): (TsState) -> Unit = { state ->
627705
val address = state.memory.allocConcrete(type)
628706
state.throwExceptionWithoutStackFrameDrop(address, type)
@@ -675,9 +753,10 @@ class TsExprResolver(
675753
val fakeRef = if (ref.isFakeObject()) {
676754
ref
677755
} else {
678-
mkFakeValue(scope, bool, fp, ref)
756+
mkFakeValue(scope, bool, fp, ref).also {
757+
lValuesToAllocatedFakeObjects += refLValue to it
758+
}
679759
}
680-
681760
memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
682761

683762
fakeRef
@@ -696,32 +775,46 @@ class TsExprResolver(
696775
// TODO It is a hack for array's length
697776
if (value.field.name == "length") {
698777
if (value.instance.type is EtsArrayType) {
699-
val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
778+
val arrayType = value.instance.type as EtsArrayType
779+
val lengthLValue = mkArrayLengthLValue(instanceRef, arrayType)
700780
val length = scope.calcOnState { memory.read(lengthLValue) }
781+
scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
782+
701783
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
702784
}
703785

704786
// TODO: handle "length" property for arrays inside fake objects
705787
if (instanceRef.isFakeObject()) {
706788
val fakeType = instanceRef.getFakeType(scope)
707-
// TODO: replace '.isTrue' with fork or assert
708-
if (fakeType.refTypeExpr.isTrue) {
709-
val refLValue = getIntermediateRefLValue(instanceRef.address)
710-
val obj = scope.calcOnState { memory.read(refLValue) }
711-
// TODO: fix array type. It should be the same as the type used when "writing" the length.
712-
// However, current value.instance typically has 'unknown' type, and the best we can do here is
713-
// to pretend that this is an array-like object (with "array length", not just "length" field),
714-
// and "cast" instance to "unknown[]". The same could be done for any length writes, making
715-
// the array type (for length) consistent (unknown everywhere), but less precise.
716-
val lengthLValue = mkArrayLengthLValue(obj, EtsArrayType(EtsUnknownType, 1))
717-
val length = scope.calcOnState { memory.read(lengthLValue) }
718-
return mkBvToFpExpr(
719-
fp64Sort,
720-
fpRoundingModeSortDefaultValue(),
721-
length.asExpr(sizeSort),
722-
signed = true
723-
)
789+
790+
// If we want to get length from a fake object, we assume that it is an array.
791+
scope.doWithState { pathConstraints += fakeType.refTypeExpr }
792+
793+
val refLValue = getIntermediateRefLValue(instanceRef.address)
794+
val obj = scope.calcOnState { memory.read(refLValue) }
795+
796+
val type = value.instance.type
797+
val arrayType = type as? EtsArrayType ?: run {
798+
check(type is EtsAnyType || type is EtsUnknownType) {
799+
"Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type"
800+
}
801+
802+
// We don't know the type of the array, since it is a fake object
803+
// If we'd know the type, we would have used it instead of creating a fake object
804+
EtsArrayType(EtsUnknownType, dimensions = 1)
724805
}
806+
val lengthLValue = mkArrayLengthLValue(obj, arrayType)
807+
val length = scope.calcOnState { memory.read(lengthLValue) }
808+
809+
scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
810+
811+
return mkBvToFpExpr(
812+
fp64Sort,
813+
fpRoundingModeSortDefaultValue(),
814+
length.asExpr(sizeSort),
815+
signed = true
816+
)
817+
725818
}
726819
}
727820

@@ -779,6 +872,12 @@ class TsExprResolver(
779872
}
780873

781874
override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? = with(ctx) {
875+
val arrayType = expr.type
876+
877+
require(arrayType is EtsArrayType) {
878+
"Expected EtsArrayType in newArrayExpr, but got ${arrayType::class.simpleName}"
879+
}
880+
782881
scope.calcOnState {
783882
val size = resolve(expr.size) ?: return@calcOnState null
784883

@@ -809,7 +908,10 @@ class TsExprResolver(
809908
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
810909
)
811910

812-
val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type
911+
if (arrayType.elementType is EtsArrayType) {
912+
TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287")
913+
}
914+
813915
val address = memory.allocateArray(arrayType, sizeSort, bvSize)
814916

815917
address

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt‎

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -73,18 +73,30 @@ class TsVoidSort(ctx: TsContext) : USort(ctx) {
7373
}
7474
}
7575

76-
fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
76+
fun UExpr<*>.toConcreteBoolValue(): Boolean = when (this) {
7777
ctx.trueExpr -> true
7878
ctx.falseExpr -> false
79-
else -> error("Cannot extract boolean from $this")
79+
else -> error("Cannot extract Boolean from $this")
8080
}
8181

82-
fun extractInt(expr: UExpr<out USort>): Int =
83-
(expr as? KBitVec32Value)?.intValue ?: error("Cannot extract int from $expr")
84-
85-
fun UExpr<out USort>.extractDouble(): Double {
82+
/**
83+
* Extracts a double value from [this] expression if possible.
84+
* Otherwise, throws an error.
85+
*/
86+
fun UExpr<*>.extractDouble(): Double {
8687
if (this@extractDouble is KFp64Value) {
8788
return value
8889
}
89-
error("Cannot extract double from $this")
90+
error("Cannot extract Double from $this")
91+
}
92+
93+
/**
94+
* Extracts an integer value from [this] expression if possible.
95+
* Otherwise, throws an error.
96+
*/
97+
fun UExpr<*>.extractInt(): Int {
98+
if (this@extractInt is KBitVec32Value) {
99+
return intValue
100+
}
101+
error("Cannot extract Int from $this")
90102
}

0 commit comments

Comments
 (0)