Skip to content

Commit 163e637

Browse files
CaelmBleiddCaelmBleidd
committed
Input arrays support
1 parent f7bb9d7 commit 163e637

File tree

15 files changed

+731
-129
lines changed

15 files changed

+731
-129
lines changed

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

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -77,14 +77,15 @@ class TsContext(
7777
else -> TODO("${type::class.simpleName} is not yet supported: $type")
7878
}
7979

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
80+
fun arrayDescriptorOf(type: EtsArrayType): EtsType {
81+
return when (type.elementType) {
82+
is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1)
83+
is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1)
84+
is EtsArrayType -> TODO("Unsupported yet: $type")
85+
is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1)
86+
else -> EtsArrayType(EtsUnknownType, dimensions = 1)
87+
}
88+
}
8889

8990
fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType {
9091
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: 128 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,74 @@ 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)
608634

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

611672
return expr
612673
}
613674

614-
private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
675+
fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
615676
val neqNull = mkAnd(
616677
mkHeapRefEq(instance, mkUndefinedValue()).not(),
617678
mkHeapRefEq(instance, mkTsNullValue()).not()
@@ -623,6 +684,24 @@ class TsExprResolver(
623684
)
624685
}
625686

687+
fun checkNegativeIndexRead(index: UExpr<TsSizeSort>) = with(ctx) {
688+
val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0))
689+
690+
scope.fork(
691+
condition,
692+
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
693+
)
694+
}
695+
696+
fun checkReadingInRange(index: UExpr<TsSizeSort>, length: UExpr<TsSizeSort>) = with(ctx) {
697+
val condition = mkBvSignedLessExpr(index, length)
698+
699+
scope.fork(
700+
condition,
701+
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
702+
)
703+
}
704+
626705
private fun allocateException(type: EtsType): (TsState) -> Unit = { state ->
627706
val address = state.memory.allocConcrete(type)
628707
state.throwExceptionWithoutStackFrameDrop(address, type)
@@ -675,9 +754,8 @@ class TsExprResolver(
675754
val fakeRef = if (ref.isFakeObject()) {
676755
ref
677756
} else {
678-
mkFakeValue(scope, bool, fp, ref)
757+
mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it }
679758
}
680-
681759
memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
682760

683761
fakeRef
@@ -696,32 +774,46 @@ class TsExprResolver(
696774
// TODO It is a hack for array's length
697775
if (value.field.name == "length") {
698776
if (value.instance.type is EtsArrayType) {
699-
val lengthLValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
777+
val arrayType = value.instance.type as EtsArrayType
778+
val lengthLValue = mkArrayLengthLValue(instanceRef, arrayType)
700779
val length = scope.calcOnState { memory.read(lengthLValue) }
780+
scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
781+
701782
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
702783
}
703784

704785
// TODO: handle "length" property for arrays inside fake objects
705786
if (instanceRef.isFakeObject()) {
706787
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-
)
788+
789+
// If we want to get length from a fake object, we assume that it is an array.
790+
scope.assert(fakeType.refTypeExpr)
791+
792+
val refLValue = getIntermediateRefLValue(instanceRef.address)
793+
val obj = scope.calcOnState { memory.read(refLValue) }
794+
795+
val type = value.instance.type
796+
val arrayType = type as? EtsArrayType ?: run {
797+
check(type is EtsAnyType || type is EtsUnknownType) {
798+
"Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type"
799+
}
800+
801+
// We don't know the type of the array, since it is a fake object
802+
// If we'd know the type, we would have used it instead of creating a fake object
803+
EtsArrayType(EtsUnknownType, dimensions = 1)
724804
}
805+
val lengthLValue = mkArrayLengthLValue(obj, arrayType)
806+
val length = scope.calcOnState { memory.read(lengthLValue) }
807+
808+
scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
809+
810+
return mkBvToFpExpr(
811+
fp64Sort,
812+
fpRoundingModeSortDefaultValue(),
813+
length.asExpr(sizeSort),
814+
signed = true
815+
)
816+
725817
}
726818
}
727819

@@ -809,7 +901,12 @@ class TsExprResolver(
809901
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
810902
)
811903

812-
val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type
904+
val arrayType = expr.type as EtsArrayType
905+
906+
if (arrayType.elementType is EtsArrayType) {
907+
TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287")
908+
}
909+
813910
val address = memory.allocateArray(arrayType, sizeSort, bvSize)
814911

815912
address

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -79,12 +79,20 @@ fun UExpr<out USort>.toConcreteBoolValue(): Boolean = when (this) {
7979
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-
8582
fun UExpr<out USort>.extractDouble(): Double {
8683
if (this@extractDouble is KFp64Value) {
8784
return value
8885
}
8986
error("Cannot extract double from $this")
9087
}
88+
89+
/**
90+
* Extracts an integer value from [this] expression if possible.
91+
* Otherwise, throws an error.
92+
*/
93+
fun UExpr<out USort>.extractInt(): Int {
94+
if (this@extractInt is KBitVec32Value) {
95+
return intValue
96+
}
97+
error("Cannot extract int from $this")
98+
}

0 commit comments

Comments
 (0)