Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -344,6 +344,8 @@ private fun TsExprResolver.handleArrayPop(
"Array.pop() should have no arguments, but got ${expr.args.size}"
}

checkNotFake(array)

scope.calcOnState {
// Read the length of the array
val lengthLValue = mkArrayLengthLValue(array, arrayType)
Expand Down
6 changes: 6 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,12 @@ import org.usvm.machine.types.ExprWithTypeConstraint
import org.usvm.types.single
import org.usvm.util.boolToFp

fun TsContext.checkNotFake(expr: UExpr<*>) {
require(!expr.isFakeObject()) {
"Fake object handling should be done outside of this function"
}
}

fun TsContext.mkTruthyExpr(
expr: UExpr<out USort>,
scope: TsStepScope,
Expand Down
2 changes: 2 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,8 @@ fun TsContext.readArray(
index: UExpr<TsSizeSort>,
arrayType: EtsArrayType,
): UExpr<*>? {
checkNotFake(array)

// Read the array length.
val length = scope.calcOnState {
val lengthLValue = mkArrayLengthLValue(array, arrayType)
Expand Down
4 changes: 1 addition & 3 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,7 @@ fun TsContext.readField(
field: EtsFieldSignature,
hierarchy: EtsHierarchy,
): UExpr<*> {
require(!instance.isFakeObject()) {
"Fake object handling should be done outside of this function"
}
checkNotFake(instance)

val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
is TsResolutionResult.Empty -> {
Expand Down
2 changes: 2 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ fun TsContext.readArrayLength(
array: UHeapRef,
arrayType: EtsArrayType,
): UExpr<KFp64Sort> {
checkNotFake(array)

// Read the length of the array.
val length = scope.calcOnState {
val lengthLValue = mkArrayLengthLValue(array, arrayType)
Expand Down
2 changes: 2 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,8 @@ fun TsContext.assignToArrayIndex(
expr: UExpr<*>,
arrayType: EtsArrayType,
): Unit? {
checkNotFake(array)

// Read the array length.
val length = scope.calcOnState {
val lengthLValue = mkArrayLengthLValue(array, arrayType)
Expand Down