Skip to content

Commit 8c5c0fa

Browse files
SaloedSaloed
authored
Improve various machine features (#294)
* v0 * Fix issues * Rebase * Disable bunch of python test * Fix style issues * Rebase * Add comments
1 parent 814740d commit 8c5c0fa

116 files changed

Lines changed: 2767 additions & 1827 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ jobs:
5555
uses: gradle/actions/setup-gradle@v4
5656

5757
- name: Run JVM tests
58-
run: ./gradlew :usvm-jvm:check :usvm-jvm-dataflow:check :usvm-jvm-instrumentation:check
58+
run: ./gradlew :usvm-jvm:check :usvm-jvm:usvm-jvm-api:check :usvm-jvm:usvm-jvm-test-api:check :usvm-jvm:usvm-jvm-util:check :usvm-jvm-dataflow:check :usvm-jvm-instrumentation:check
5959

6060
- name: Upload Gradle reports
6161
if: (!cancelled())

‎build.gradle.kts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@ tasks.register("validateProjectList") {
1414
project(":usvm-dataflow"),
1515
project(":usvm-sample-language"),
1616
project(":usvm-jvm"),
17+
project(":usvm-jvm:usvm-jvm-api"),
18+
project(":usvm-jvm:usvm-jvm-test-api"),
19+
project (":usvm-jvm:usvm-jvm-util"),
1720
project(":usvm-jvm-dataflow"),
1821
project(":usvm-jvm-instrumentation"),
1922
project(":usvm-python"),

‎settings.gradle.kts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@ rootProject.name = "usvm"
22

33
include("usvm-core")
44
include("usvm-jvm")
5+
include("usvm-jvm:usvm-jvm-api")
6+
include("usvm-jvm:usvm-jvm-test-api")
7+
include("usvm-jvm:usvm-jvm-util")
58
include("usvm-ts")
69
include("usvm-util")
710
include("usvm-jvm-instrumentation")

‎usvm-core/src/main/kotlin/org/usvm/CallStack.kt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ class UCallStack<Method, Statement> private constructor(
2727

2828
fun lastMethod(): Method = stack.last().method
2929

30+
fun penultimateMethod(): Method = stack[stack.lastIndex - 1].method
31+
3032
fun push(method: Method, returnSite: Statement?) {
3133
stack.add(UCallStackFrame(method, returnSite))
3234
}

‎usvm-core/src/main/kotlin/org/usvm/Machine.kt‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,16 @@ abstract class UMachine<State : UState<*, *, *, *, *, State>> : AutoCloseable {
4141
val state = pathSelector.peek()
4242
observer.onStatePeeked(state)
4343

44-
val (forkedStates, stateAlive) = interpreter.step(state)
44+
val (forkedStates, stateAlive) = try {
45+
interpreter.step(state)
46+
} catch (e: Throwable) {
47+
logger.error(e) { "Step failed" }
48+
observer.onState(state, forks = emptySequence())
49+
pathSelector.remove(state)
50+
observer.onStateTerminated(state, stateReachable = false)
51+
continue
52+
}
53+
4554
observer.onState(state, forkedStates)
4655

4756
val originalStateAlive = stateAlive && !isStateTerminated(state)
@@ -76,7 +85,8 @@ abstract class UMachine<State : UState<*, *, *, *, *, State>> : AutoCloseable {
7685
}
7786

7887
if (!pathSelector.isEmpty()) {
79-
logger.debug { stopStrategy.stopReason() }
88+
val stopReason = stopStrategy.stopReason()
89+
logger.debug { stopReason }
8090
}
8191
}
8292
}

‎usvm-core/src/main/kotlin/org/usvm/StateForker.kt‎

Lines changed: 50 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -94,34 +94,36 @@ object WithSolverStateForker : StateForker {
9494
state: T,
9595
conditions: Iterable<UBoolExpr>,
9696
): List<T?> {
97-
var curState = state
98-
val result = mutableListOf<T?>()
99-
for (condition in conditions) {
100-
val (trueModels, _, _) = splitModelsByCondition(curState.models, condition)
97+
val guardedModels = mutableListOf<Pair<List<UModelBase<Type>>, UBoolExpr>?>()
10198

102-
val nextRoot = if (trueModels.isNotEmpty()) {
103-
val root = curState.clone()
104-
curState.models = trueModels
105-
curState.pathConstraints += condition
99+
for (condition in conditions) {
100+
val (trueModels, _, _) = splitModelsByCondition(state.models, condition)
106101

107-
root
102+
if (trueModels.isNotEmpty()) {
103+
guardedModels += trueModels to condition
108104
} else {
109-
val root = forkIfSat(
110-
curState,
105+
forkOriginalStateIfSat(
106+
state,
111107
newConstraintToOriginalState = condition,
112-
newConstraintToForkedState = condition.ctx.trueExpr,
113-
stateToCheck = OriginalState
108+
guardedModels
114109
)
115-
116-
root
117110
}
118-
119-
if (nextRoot != null) {
120-
result += curState
121-
curState = nextRoot
122-
} else {
111+
}
112+
val result = mutableListOf<T?>()
113+
var curState = state
114+
val lastNotNullIndex = guardedModels.indexOfLast { x -> x != null }
115+
for (i in guardedModels.indices) {
116+
val current = guardedModels[i]
117+
if (current == null) {
123118
result += null
119+
continue
124120
}
121+
val nextState = if (i == lastNotNullIndex) curState else curState.clone()
122+
val (models, cond) = current
123+
curState.models = models
124+
curState.pathConstraints += cond
125+
result += curState
126+
curState = nextState
125127
}
126128

127129
return result
@@ -190,6 +192,34 @@ object WithSolverStateForker : StateForker {
190192
}
191193
}
192194
}
195+
196+
@Suppress("MoveVariableDeclarationIntoWhen")
197+
private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>> forkOriginalStateIfSat(
198+
state: T,
199+
newConstraintToOriginalState: UBoolExpr,
200+
guardedModels: MutableList<Pair<List<UModelBase<Type>>, UBoolExpr>?>
201+
) {
202+
val constraintsToCheck = state.pathConstraints.clone()
203+
204+
constraintsToCheck += newConstraintToOriginalState
205+
val solver = state.ctx.solver<Type>()
206+
val satResult = solver.check(constraintsToCheck)
207+
208+
when (satResult) {
209+
is UUnsatResult -> guardedModels += null
210+
211+
is USatResult -> {
212+
// Note that we cannot extract common code here due to
213+
// heavy plusAssign operator in path constraints.
214+
// Therefore, it is better to reuse already constructed [constraintToCheck].
215+
guardedModels += listOf(satResult.model) to newConstraintToOriginalState
216+
}
217+
218+
is UUnknownResult -> {
219+
guardedModels += null
220+
}
221+
}
222+
}
193223
}
194224

195225
object NoSolverStateForker : StateForker {

‎usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt‎

Lines changed: 71 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,37 @@ fun <Type> UState<Type, *, *, *, *, *>.objectTypeEquals(
4242
)
4343
}
4444

45+
fun <Type> UState<Type, *, *, *, *, *>.objectTypeSubtype(
46+
lhs: UHeapRef,
47+
rhs: UHeapRef
48+
): UBoolExpr = with(lhs.uctx) {
49+
mapTypeStream(
50+
ref = lhs,
51+
onNull = { trueExpr },
52+
operation = { lhsRef, lhsTypes ->
53+
mapTypeStream(
54+
rhs,
55+
onNull = { falseExpr },
56+
operation = { rhsRef, rhsTypes ->
57+
mkSubtypeConstraint(lhsRef, lhsTypes, rhsRef, rhsTypes)
58+
}
59+
)
60+
}
61+
)
62+
}
63+
64+
fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStreamNotNull(
65+
ref: UHeapRef,
66+
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
67+
): UExpr<R>? = mapTypeStream(
68+
ref = ref,
69+
onNull = { error("unexpected null") },
70+
operation = { expr, types ->
71+
operation(expr, types) ?: return null
72+
},
73+
ignoreNullRefs = true
74+
)
75+
4576
fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
4677
ref: UHeapRef,
4778
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
@@ -53,6 +84,12 @@ fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
5384
}
5485
)
5586

87+
/**
88+
* Utility function to assert that type of lhs ref is equal to the type of the rhs ref.
89+
*
90+
* Note: if both refs have no concrete type stream, the result expression will be extremely complex.
91+
* So, we mock the result of this operation.
92+
* */
5693
private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
5794
lhs: UHeapRef,
5895
lhsTypes: UTypeStream<Type>,
@@ -78,12 +115,44 @@ private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
78115
makeSymbolicPrimitive(boolSort)
79116
}
80117

118+
/**
119+
* Utility function to assert that type of lhs ref is subtype of type of the rhs ref.
120+
*
121+
* Note: if both refs have no concrete type stream, the result expression will be extremely complex.
122+
* So, we mock the result of this operation.
123+
* */
124+
private fun <Type> UState<Type, *, *, *, *, *>.mkSubtypeConstraint(
125+
lhs: UHeapRef,
126+
lhsTypes: UTypeStream<Type>,
127+
rhs: UHeapRef,
128+
rhsTypes: UTypeStream<Type>,
129+
): UBoolExpr = with(lhs.uctx) {
130+
val lhsType = lhsTypes.singleOrNull()
131+
val rhsType = rhsTypes.singleOrNull()
132+
133+
if (lhsType != null) {
134+
return if (lhsType == rhsType) {
135+
trueExpr
136+
} else {
137+
memory.types.evalIsSupertype(rhs, lhsType)
138+
}
139+
}
140+
141+
if (rhsType != null) {
142+
return memory.types.evalIsSubtype(lhs, rhsType)
143+
}
144+
145+
// TODO: don't mock type equals
146+
makeSymbolicPrimitive(boolSort)
147+
}
148+
81149
private inline fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
82150
ref: UHeapRef,
83151
onNull: () -> UExpr<R>,
84-
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>
152+
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>,
153+
ignoreNullRefs: Boolean = false,
85154
): UExpr<R> = ref.mapWithStaticAsConcrete(
86-
ignoreNullRefs = false,
155+
ignoreNullRefs = ignoreNullRefs,
87156
concreteMapper = { concreteRef ->
88157
val types = memory.types.getTypeStream(concreteRef)
89158
operation(concreteRef, types)

‎usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@ import org.usvm.regions.Region
2323
import org.usvm.types.UTypeStream
2424
import org.usvm.uctx
2525
import org.usvm.withSizeSort
26-
import org.usvm.collection.array.allocateArray as allocateArrayInternal
27-
import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitializedInternal
26+
import org.usvm.collection.array.initializeArrayLength as initializeArrayLengthInternal
27+
import org.usvm.collection.array.initializeArray as initializeArrayInternal
2828

2929
fun <Type> UReadOnlyMemory<Type>.typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
3030
types.getTypeStream(ref)
@@ -93,13 +93,20 @@ fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.mems
9393
memsetInternal(ref, type, sort, sizeSort, contents)
9494
}
9595

96-
fun <ArrayType, USizeSort : USort> UWritableMemory<ArrayType>.allocateArray(
97-
type: ArrayType, sizeSort: USizeSort, count: UExpr<USizeSort>,
98-
): UConcreteHeapRef = allocateArrayInternal(type, sizeSort, count)
96+
fun <ArrayType, USizeSort : USort> UWritableMemory<ArrayType>.initializeArrayLength(
97+
arrayHeapRef: UConcreteHeapRef,
98+
type: ArrayType,
99+
sizeSort: USizeSort,
100+
count: UExpr<USizeSort>,
101+
) = initializeArrayLengthInternal(arrayHeapRef, type, sizeSort, count)
99102

100-
fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.allocateArrayInitialized(
101-
type: ArrayType, sort: Sort, sizeSort: USizeSort, contents: Sequence<UExpr<Sort>>
102-
): UConcreteHeapRef = allocateArrayInitializedInternal(type, sort, sizeSort, contents)
103+
fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.initializeArray(
104+
arrayHeapRef: UConcreteHeapRef,
105+
type: ArrayType,
106+
sort: Sort,
107+
sizeSort: USizeSort,
108+
contents: Sequence<UExpr<Sort>>
109+
) = initializeArrayInternal(arrayHeapRef, type, sort, sizeSort, contents)
103110

104111
fun <SetType, ElemSort : USort, Reg : Region<Reg>> UWritableMemory<SetType>.setAddElement(
105112
ref: UHeapRef,

‎usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,31 @@ fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRef(
2323
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
2424
mockSymbolicRef { memory.types.evalTypeEquals(it, type) }
2525

26+
fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRef(
27+
type: Type
28+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
29+
mockSymbolicRef { ctx.mkOr(memory.types.evalTypeEquals(it, type), ctx.mkEq(it, ctx.nullRef)) }
30+
31+
fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefSubtype(
32+
type: Type
33+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
34+
mockSymbolicRef { ctx.mkAnd(memory.types.evalIsSubtype(it, type), ctx.mkNot(ctx.mkEq(it, ctx.nullRef))) }
35+
36+
fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefSubtype(
37+
type: Type
38+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
39+
mockSymbolicRef { memory.types.evalIsSubtype(it, type) }
40+
41+
fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefSubtype(
42+
representative: UHeapRef
43+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
44+
mockSymbolicRef { ctx.mkAnd(objectTypeSubtype(it, representative), ctx.mkNot(ctx.mkEq(it, ctx.nullRef))) }
45+
46+
fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefSubtype(
47+
representative: UHeapRef
48+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
49+
mockSymbolicRef { objectTypeSubtype(it, representative) }
50+
2651
fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefWithSameType(
2752
representative: UHeapRef
2853
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =

‎usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import org.usvm.memory.mapWithStaticAsConcrete
1515
import org.usvm.mkSizeAddExpr
1616
import org.usvm.mkSizeExpr
1717
import org.usvm.mkSizeGeExpr
18+
import org.usvm.mkSizeGtExpr
1819
import org.usvm.mkSizeSubExpr
1920
import org.usvm.sizeSort
2021
import org.usvm.utils.logAssertFailure
@@ -150,7 +151,12 @@ object ListCollectionApi {
150151
memory.writeArrayLength(listRef, updatedSize, listType, sizeSort)
151152
}
152153

153-
fun <ListType, Sort : USort, USizeSort : USort> UState<ListType, *, *, *, *, *>.symbolicListCopyRange(
154+
private fun <USizeSort : USort, Ctx: UContext<USizeSort>> Ctx.max(
155+
first: UExpr<USizeSort>,
156+
second: UExpr<USizeSort>
157+
): UExpr<USizeSort> = mkIte(mkSizeGtExpr(first, second), first, second)
158+
159+
fun <ListType, Sort : USort, USizeSort : USort, Ctx: UContext<USizeSort>> UState<ListType, *, *, Ctx, *, *>.symbolicListCopyRange(
154160
srcRef: UHeapRef,
155161
dstRef: UHeapRef,
156162
listType: ListType,
@@ -159,6 +165,7 @@ object ListCollectionApi {
159165
dstFrom: UExpr<USizeSort>,
160166
length: UExpr<USizeSort>,
161167
) {
168+
// Copying contents
162169
memory.memcpy(
163170
srcRef = srcRef,
164171
dstRef = dstRef,
@@ -168,5 +175,11 @@ object ListCollectionApi {
168175
fromDst = dstFrom,
169176
length = length
170177
)
178+
179+
// Modifying destination length
180+
val dstLength = symbolicListSize(dstRef, listType)
181+
val copyLength = ctx.mkSizeAddExpr(dstFrom, length)
182+
val resultDstLength = ctx.max(dstLength, copyLength)
183+
memory.writeArrayLength(dstRef, resultDstLength, listType, ctx.sizeSort)
171184
}
172185
}

0 commit comments

Comments
 (0)