Skip to content

Commit

Permalink
Field writing support
Browse files Browse the repository at this point in the history 
Squashed
  • Loading branch information
@CaelmBleidd @Lipen
CaelmBleidd authored and Lipen committed Feb 26, 2025
1 parent fb0614d commit 9ad2a16
Show file tree
Hide file tree
Showing 9 changed files with 358 additions and 95 deletions.
44 changes: 39 additions & 5 deletions usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package org.usvm.machine

import io.ksmt.sort.KFp64Sort
import io.ksmt.utils.asExpr
import org.jacodb.ets.base.EtsAnyType
import org.jacodb.ets.base.EtsBooleanType
import org.jacodb.ets.base.EtsNullType
import org.jacodb.ets.base.EtsNumberType
Expand All @@ -19,10 +20,13 @@ import org.usvm.UContext
import org.usvm.UExpr
import org.usvm.USort
import org.usvm.collection.field.UFieldLValue
import org.usvm.isTrue
import org.usvm.machine.expr.TsUndefinedSort
import org.usvm.machine.expr.TsUnresolvedSort
import org.usvm.machine.interpreter.TsStepScope
import org.usvm.machine.types.FakeType
import org.usvm.types.single
import org.usvm.util.mkFieldLValue
import kotlin.contracts.ExperimentalContracts
import kotlin.contracts.contract

Expand Down Expand Up @@ -51,6 +55,7 @@ class TsContext(
is EtsUndefinedType -> addressSort
is EtsUnknownType -> unresolvedSort
is EtsUnionType -> unresolvedSort
is EtsAnyType -> unresolvedSort
else -> TODO("Support all JacoDB types, encountered $type")
}

Expand All @@ -70,7 +75,7 @@ class TsContext(

val ref = createFakeObjectRef()

scope.calcOnState {
scope.doWithState {
when (sort) {
boolSort -> {
val lvalue = getIntermediateBoolLValue(ref.address)
Expand All @@ -86,8 +91,8 @@ class TsContext(

addressSort -> {
val lValue = getIntermediateRefLValue(ref.address)
memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
memory.write(lValue, this@toFakeObject.asExpr(addressSort), guard = trueExpr)
memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
}

else -> TODO("Not yet supported")
Expand All @@ -97,6 +102,35 @@ class TsContext(
return ref
}

fun UExpr<out USort>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
if (!isFakeObject()) return null

val type = scope.calcOnState {
memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType
}

return scope.calcOnState {
when {
type.boolTypeExpr.isTrue -> {
val lValue = getIntermediateBoolLValue(address)
memory.read(lValue).asExpr(boolSort)
}

type.fpTypeExpr.isTrue -> {
val lValue = getIntermediateFpLValue(address)
memory.read(lValue).asExpr(fp64Sort)
}

type.refTypeExpr.isTrue -> {
val lValue = getIntermediateRefLValue(address)
memory.read(lValue).asExpr(addressSort)
}

else -> null
}
}
}

fun createFakeObjectRef(): UConcreteHeapRef {
val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
return mkConcreteHeapRef(address)
Expand All @@ -108,15 +142,15 @@ class TsContext(
private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())

fun getIntermediateBoolLValue(addr: Int): UFieldLValue<IntermediateLValueField, UBoolSort> {
return UFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
return mkFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
}

fun getIntermediateFpLValue(addr: Int): UFieldLValue<IntermediateLValueField, KFp64Sort> {
return UFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP)
return mkFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP)
}

fun getIntermediateRefLValue(addr: Int): UFieldLValue<IntermediateLValueField, UAddressSort> {
return UFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
return mkFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
}
}

Expand Down
70 changes: 46 additions & 24 deletions usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,29 +74,28 @@ import org.jacodb.ets.model.EtsField
import org.jacodb.ets.model.EtsFieldSignature
import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.model.EtsMethodSignature
import org.jacodb.ets.utils.getDeclaredLocals
import org.usvm.UAddressSort
import org.usvm.UBoolSort
import org.usvm.UExpr
import org.usvm.UHeapRef
import org.usvm.USort
import org.usvm.api.allocateArray
import org.usvm.api.makeSymbolicPrimitive
import org.usvm.collection.array.UArrayIndexLValue
import org.usvm.collection.array.length.UArrayLengthLValue
import org.usvm.collection.field.UFieldLValue
import org.usvm.machine.TsContext
import org.usvm.machine.interpreter.TsStepScope
import org.usvm.machine.operator.TsBinaryOperator
import org.usvm.machine.operator.TsUnaryOperator
import org.usvm.machine.state.TsMethodResult
import org.usvm.machine.state.TsState
import org.usvm.machine.state.localsCount
import org.usvm.machine.state.newStmt
import org.usvm.machine.types.FakeType
import org.usvm.machine.types.mkFakeValue
import org.usvm.memory.ULValue
import org.usvm.memory.URegisterStackLValue
import org.usvm.sizeSort
import org.usvm.util.fieldLookUp
import org.usvm.util.mkArrayIndexLValue
import org.usvm.util.mkArrayLengthLValue
import org.usvm.util.mkFieldLValue
import org.usvm.util.mkRegisterStackLValue
import org.usvm.util.throwExceptionWithoutStackFrameDrop

private val logger = KotlinLogging.logger {}
Expand Down Expand Up @@ -415,7 +414,7 @@ class TsExprResolver(
pushSortsForArguments(expr.instance, expr.args, localToIdx)

callStack.push(method, currentStatement)
memory.stack.push(args.toTypedArray(), method.localsCount)
memory.stack.push(args.toTypedArray(), method.getDeclaredLocals().size)

newStmt(method.cfg.stmts.first())
}
Expand Down Expand Up @@ -541,7 +540,12 @@ class TsExprResolver(
isSigned = true
)

val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type)
val lValue = mkArrayIndexLValue(
addressSort,
instance,
bvIndex.asExpr(ctx.sizeSort),
value.array.type as EtsArrayType
)
val expr = scope.calcOnState { memory.read(lValue) }

check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
Expand Down Expand Up @@ -599,7 +603,7 @@ class TsExprResolver(

// TODO It is a hack for array's length
if (value.instance.type is EtsArrayType && value.field.name == "length") {
val lValue = UArrayLengthLValue(instanceRef, value.instance.type, ctx.sizeSort)
val lValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
val expr = scope.calcOnState { memory.read(lValue) }

check(expr.sort == ctx.sizeSort)
Expand All @@ -612,6 +616,33 @@ class TsExprResolver(
val lValue = UFieldLValue(sort, instanceRef, value.field.name)
val expr = scope.calcOnState { memory.read(lValue) }

val expr = if (sort == unresolvedSort) {
val boolLValue = mkFieldLValue(boolSort, instanceRef, value.field)
val fpLValue = mkFieldLValue(fp64Sort, instanceRef, value.field)
val refLValue = mkFieldLValue(addressSort, instanceRef, value.field)

scope.calcOnState {
val bool = memory.read(boolLValue)
val fp = memory.read(fpLValue)
val ref = memory.read(refLValue)

// If a fake object is already created and assigned to the field,
// there is no need to recreate another one
val fakeRef = if (ref.isFakeObject()) {
ref
} else {
mkFakeValue(scope, bool, fp, ref)
}

memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)

fakeRef
}
} else {
val lValue = mkFieldLValue(sort, instanceRef, value.field)
scope.calcOnState { memory.read(lValue) }
}

if (assertIsSubtype(expr, value.type)) {
expr
} else {
Expand Down Expand Up @@ -706,20 +737,20 @@ class TsSimpleValueResolver(
// If we are not in the entrypoint, all correct values are already resolved and we can just return
// a registerStackLValue for the local
if (currentMethod != entrypoint) {
return URegisterStackLValue(sort, localIdx)
return mkRegisterStackLValue(sort, localIdx)
}

// arguments and this for the first stack frame
return when (sort) {
is UBoolSort -> URegisterStackLValue(sort, localIdx)
is KFp64Sort -> URegisterStackLValue(sort, localIdx)
is UAddressSort -> URegisterStackLValue(sort, localIdx)
is UBoolSort -> mkRegisterStackLValue(sort, localIdx)
is KFp64Sort -> mkRegisterStackLValue(sort, localIdx)
is UAddressSort -> mkRegisterStackLValue(sort, localIdx)
is TsUnresolvedSort -> {
check(local is EtsThis || local is EtsParameterRef) {
"Only This and ParameterRef are expected here"
}

val lValue = URegisterStackLValue(ctx.addressSort, localIdx)
val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx)

val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort)
val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort)
Expand All @@ -728,15 +759,6 @@ class TsSimpleValueResolver(
val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue)
scope.calcOnState {
with(ctx) {
val type = FakeType(
boolTypeExpr = makeSymbolicPrimitive(boolSort),
fpTypeExpr = makeSymbolicPrimitive(boolSort),
refTypeExpr = makeSymbolicPrimitive(boolSort)
)

scope.assert(type.mkExactlyOneTypeConstraint(ctx))

memory.types.allocate(fakeObject.address, type)
memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr)
}
}
Expand Down
41 changes: 32 additions & 9 deletions usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,12 @@ package org.usvm.machine.interpreter
import io.ksmt.utils.asExpr
import mu.KotlinLogging
import org.jacodb.ets.base.EtsArrayAccess
import org.jacodb.ets.base.EtsArrayType
import org.jacodb.ets.base.EtsAssignStmt
import org.jacodb.ets.base.EtsCallStmt
import org.jacodb.ets.base.EtsGotoStmt
import org.jacodb.ets.base.EtsIfStmt
import org.jacodb.ets.base.EtsInstanceFieldRef
import org.jacodb.ets.base.EtsLocal
import org.jacodb.ets.base.EtsNopStmt
import org.jacodb.ets.base.EtsNullType
Expand All @@ -19,12 +21,11 @@ import org.jacodb.ets.base.EtsThrowStmt
import org.jacodb.ets.base.EtsType
import org.jacodb.ets.base.EtsValue
import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.utils.getDeclaredLocals
import org.usvm.StepResult
import org.usvm.StepScope
import org.usvm.UInterpreter
import org.usvm.api.targets.TsTarget
import org.usvm.collection.array.UArrayIndexLValue
import org.usvm.collection.array.length.UArrayLengthLValue
import org.usvm.collections.immutable.internal.MutabilityOwnership
import org.usvm.forkblacklists.UForkBlackList
import org.usvm.machine.TsApplicationGraph
Expand All @@ -34,13 +35,15 @@ import org.usvm.machine.expr.mkTruthyExpr
import org.usvm.machine.state.TsMethodResult
import org.usvm.machine.state.TsState
import org.usvm.machine.state.lastStmt
import org.usvm.machine.state.localsCount
import org.usvm.machine.state.newStmt
import org.usvm.machine.state.parametersWithThisCount
import org.usvm.machine.state.returnValue
import org.usvm.memory.URegisterStackLValue
import org.usvm.sizeSort
import org.usvm.targets.UTargetsSet
import org.usvm.util.mkArrayIndexLValue
import org.usvm.util.mkArrayLengthLValue
import org.usvm.util.mkFieldLValue
import org.usvm.util.mkRegisterStackLValue
import org.usvm.utils.ensureSat

private val logger = KotlinLogging.logger {}
Expand Down Expand Up @@ -139,7 +142,7 @@ class TsInterpreter(
val idx = mapLocalToIdx(lastEnteredMethod, lhv)
saveSortForLocal(idx, expr.sort)

val lValue = URegisterStackLValue(expr.sort, idx)
val lValue = mkRegisterStackLValue(expr.sort, idx)
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
}

Expand All @@ -155,7 +158,7 @@ class TsInterpreter(
isSigned = true
).asExpr(sizeSort)

val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort)
val lengthLValue = mkArrayLengthLValue(instance, lhv.array.type as EtsArrayType)
val currentLength = memory.read(lengthLValue).asExpr(sizeSort)

val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength)
Expand All @@ -165,10 +168,29 @@ class TsInterpreter(

val fakeExpr = expr.toFakeObject(scope)

val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type)
val lValue = mkArrayIndexLValue(
addressSort,
instance,
bvIndex.asExpr(sizeSort),
lhv.array.type as EtsArrayType
)
memory.write(lValue, fakeExpr, guard = trueExpr)
}

is EtsInstanceFieldRef -> {
val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState

val sort = typeToSort(lhv.type)
if (sort == unresolvedSort) {
val fakeObject = expr.toFakeObject(scope)
val lValue = mkFieldLValue(addressSort, instance, lhv.field)
memory.write(lValue, fakeObject, guard = trueExpr)
} else {
val lValue = mkFieldLValue(sort, instance, lhv.field)
memory.write(lValue, expr.asExpr(sort), guard = trueExpr)
}
}

else -> TODO("Not yet implemented")
}

Expand Down Expand Up @@ -239,7 +261,8 @@ class TsInterpreter(

val solver = ctx.solver<EtsType>()

val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics
// TODO check for statics
val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count())
val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)

state.pathConstraints += with(ctx) {
Expand All @@ -259,7 +282,7 @@ class TsInterpreter(
state.models = listOf(model)

state.callStack.push(method, returnSite = null)
state.memory.stack.push(method.parametersWithThisCount, method.localsCount)
state.memory.stack.push(method.parametersWithThisCount, method.getDeclaredLocals().size)
state.newStmt(method.cfg.instructions.first())

state.memory.types.allocate(ctx.mkTsNullValue().address, EtsNullType)
Expand Down
19 changes: 11 additions & 8 deletions usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,21 +56,24 @@ sealed interface TsBinaryOperator {
rhs: UExpr<out USort>,
scope: TsStepScope,
): UExpr<out USort> {
if (lhs.isFakeObject() || rhs.isFakeObject()) {
return resolveFakeObject(lhs, rhs, scope)
val lhsValue = lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs
val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs

if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) {
return resolveFakeObject(lhsValue, rhsValue, scope)
}

val lhsSort = lhs.sort
if (lhsSort == rhs.sort) {
val lhsSort = lhsValue.sort
if (lhsSort == rhsValue.sort) {
return when (lhsSort) {
boolSort -> onBool(lhs.asExpr(boolSort), rhs.asExpr(boolSort), scope)
fp64Sort -> onFp(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort), scope)
addressSort -> onRef(lhs.asExpr(addressSort), rhs.asExpr(addressSort), scope)
boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope)
fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope)
addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope)
else -> TODO("Unsupported sort $lhsSort")
}
}

return internalResolve(lhs, rhs, scope)
return internalResolve(lhsValue, rhsValue, scope)
}

data object Eq : TsBinaryOperator {
Expand Down
Loading

0 comments on commit 9ad2a16

Please sign in to comment.