Skip to content

Commit f37c4e6

Browse files
SaloedCaelmBleidd
Saloed
and
CaelmBleidd
authored
Stdlib approximations (#62)
Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>
1 parent a4123e6 commit f37c4e6

File tree

19 files changed

+1019
-67
lines changed

19 files changed

+1019
-67
lines changed

‎buildSrc/src/main/kotlin/Versions.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ object Versions {
44
const val ksmt = "0.5.7"
55
const val collections = "0.3.5"
66
const val coroutines = "1.6.4"
7-
const val jcdb = "1.2.0"
7+
const val jcdb = "1.3.0"
88
const val mockk = "1.13.4"
99
const val junitParams = "5.9.3"
1010
const val logback = "1.4.8"

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

Lines changed: 89 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,99 @@
11
package org.usvm.api
22

33
import org.usvm.UBoolExpr
4+
import org.usvm.UExpr
45
import org.usvm.UHeapRef
6+
import org.usvm.UNullRef
7+
import org.usvm.USort
58
import org.usvm.UState
9+
import org.usvm.constraints.UTypeEvaluator
10+
import org.usvm.memory.mapWithStaticAsConcrete
11+
import org.usvm.types.UTypeStream
12+
import org.usvm.types.singleOrNull
13+
import org.usvm.uctx
614

15+
fun <Type> UTypeEvaluator<Type>.evalTypeEquals(ref: UHeapRef, type: Type): UBoolExpr =
16+
with(ref.uctx) {
17+
mkAnd(
18+
evalIsSubtype(ref, type),
19+
evalIsSupertype(ref, type)
20+
)
21+
}
722

8-
fun UState<*, *, *, *, *, *>.assume(expr: UBoolExpr) {
9-
pathConstraints += expr
23+
fun <Type> UState<Type, *, *, *, *, *>.objectTypeEquals(
24+
lhs: UHeapRef,
25+
rhs: UHeapRef
26+
): UBoolExpr = with(lhs.uctx) {
27+
mapTypeStream(
28+
ref = lhs,
29+
onNull = {
30+
// type(null) = type(null); type(null) <: T /\ T <: type(null) ==> true /\ false
31+
mapTypeStream(rhs, onNull = { trueExpr }, { _, _ -> falseExpr })
32+
},
33+
operation = { lhsRef, lhsTypes ->
34+
mapTypeStream(
35+
rhs,
36+
onNull = { falseExpr },
37+
operation = { rhsRef, rhsTypes ->
38+
mkTypeEqualsConstraint(lhsRef, lhsTypes, rhsRef, rhsTypes)
39+
}
40+
)
41+
}
42+
)
1043
}
1144

12-
fun UState<*, *, *, *, *, *>.objectTypeEquals(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr {
13-
TODO("Objects types equality check: $lhs, $rhs")
45+
fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
46+
ref: UHeapRef,
47+
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
48+
): UExpr<R>? = mapTypeStream(
49+
ref = ref,
50+
onNull = { return null },
51+
operation = { expr, types ->
52+
operation(expr, types) ?: return null
53+
}
54+
)
55+
56+
private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
57+
lhs: UHeapRef,
58+
lhsTypes: UTypeStream<Type>,
59+
rhs: UHeapRef,
60+
rhsTypes: UTypeStream<Type>,
61+
): UBoolExpr = with(lhs.uctx) {
62+
val lhsType = lhsTypes.singleOrNull()
63+
val rhsType = rhsTypes.singleOrNull()
64+
65+
if (lhsType != null) {
66+
return if (lhsType == rhsType) {
67+
trueExpr
68+
} else {
69+
memory.types.evalTypeEquals(rhs, lhsType)
70+
}
71+
}
72+
73+
if (rhsType != null) {
74+
return memory.types.evalTypeEquals(lhs, rhsType)
75+
}
76+
77+
// TODO: don't mock type equals
78+
makeSymbolicPrimitive(boolSort)
1479
}
80+
81+
private inline fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
82+
ref: UHeapRef,
83+
onNull: () -> UExpr<R>,
84+
operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>
85+
): UExpr<R> = ref.mapWithStaticAsConcrete(
86+
ignoreNullRefs = false,
87+
concreteMapper = { concreteRef ->
88+
val types = memory.types.getTypeStream(concreteRef)
89+
operation(concreteRef, types)
90+
},
91+
symbolicMapper = { symbolicRef ->
92+
if (symbolicRef is UNullRef) {
93+
onNull()
94+
} else {
95+
val types = memory.types.getTypeStream(symbolicRef)
96+
operation(symbolicRef, types)
97+
}
98+
},
99+
)

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

Lines changed: 20 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
package org.usvm.api
22

3+
import org.usvm.StepScope
4+
import org.usvm.UBoolExpr
35
import org.usvm.UExpr
46
import org.usvm.UHeapRef
5-
import org.usvm.USizeExpr
67
import org.usvm.USort
78
import org.usvm.UState
89
import org.usvm.uctx
@@ -16,22 +17,28 @@ fun <Method, T : USort> UState<*, Method, *, *, *, *>.makeSymbolicPrimitive(
1617
return memory.mock { call(lastEnteredMethod, emptySequence(), sort) }
1718
}
1819

19-
fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicRef(type: Type): UHeapRef {
20-
val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
20+
fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRef(
21+
type: Type
22+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
23+
mockSymbolicRef { memory.types.evalTypeEquals(it, type) }
2124

22-
memory.types.addSubtype(ref, type)
23-
memory.types.addSupertype(ref, type)
25+
fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRefWithSameType(
26+
representative: UHeapRef
27+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
28+
mockSymbolicRef { objectTypeEquals(it, representative) }
2429

25-
return ref
26-
}
27-
28-
fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicArray(arrayType: Type, size: USizeExpr): UHeapRef {
29-
val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
30+
private inline fun <Type, Method, State> StepScope<State, Type, *>.mockSymbolicRef(
31+
crossinline mkTypeConstraint: State.(UHeapRef) -> UBoolExpr
32+
): UHeapRef? where State : UState<Type, Method, *, *, *, State> {
33+
val ref = calcOnState {
34+
memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
35+
}
3036

31-
memory.types.addSubtype(ref, arrayType)
32-
memory.types.addSupertype(ref, arrayType)
37+
val typeConstraint = calcOnState {
38+
mkTypeConstraint(ref)
39+
}
3340

34-
memory.writeArrayLength(ref, size, arrayType)
41+
assert(typeConstraint) ?: return null
3542

3643
return ref
3744
}

‎usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,17 @@ import org.usvm.types.UTypeSystem
1616
import org.usvm.uctx
1717

1818
interface UTypeEvaluator<Type> {
19+
20+
/**
21+
* Check that [ref] = `null` or type([ref]) <: [supertype].
22+
* Note that T <: T always holds.
23+
* */
1924
fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr
25+
26+
/**
27+
* Check that [ref] != `null` and [subtype] <: type([ref]).
28+
* Note that T <: T always holds.
29+
* */
2030
fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr
2131
fun getTypeStream(ref: UHeapRef): UTypeStream<Type>
2232
}

‎usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,11 @@ fun <Type> UTypeStream<Type>.first(): Type = take(1).first()
7575

7676
fun <Type> UTypeStream<Type>.firstOrNull(): Type? = take(1).firstOrNull()
7777

78+
// Note: we try to take at least two types to ensure that we don't have no more than one type.
79+
fun <Type> UTypeStream<Type>.single(): Type = take(2).single()
80+
81+
fun <Type> UTypeStream<Type>.singleOrNull(): Type? = take(2).singleOrNull()
82+
7883
/**
7984
* Consists of just one type [singleType].
8085
*/

‎usvm-jvm/build.gradle.kts‎

Lines changed: 39 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,32 @@ plugins {
22
id("usvm.kotlin-conventions")
33
}
44

5+
val samples by sourceSets.creating {
6+
java {
7+
srcDir("src/samples/java")
8+
}
9+
}
10+
11+
val `usvm-api` by sourceSets.creating {
12+
java {
13+
srcDir("src/usvm-api/java")
14+
}
15+
}
16+
17+
val approximations by configurations.creating
18+
val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations"
19+
val approximationsVersion = "53ceeb23ea"
20+
521
dependencies {
622
implementation(project(":usvm-core"))
723

824
implementation("org.jacodb:jacodb-core:${Versions.jcdb}")
925
implementation("org.jacodb:jacodb-analysis:${Versions.jcdb}")
1026

27+
implementation("org.jacodb:jacodb-approximations:${Versions.jcdb}")
28+
29+
implementation(`usvm-api`.output)
30+
1131
implementation("io.ksmt:ksmt-yices:${Versions.ksmt}")
1232
implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}")
1333
implementation("io.ksmt:ksmt-symfpu:${Versions.ksmt}")
@@ -16,22 +36,14 @@ dependencies {
1636
testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}")
1737
testImplementation("ch.qos.logback:logback-classic:${Versions.logback}")
1838

39+
testImplementation(samples.output)
40+
1941
// https://mvnrepository.com/artifact/org.burningwave/core
2042
// Use it to export all modules to all
2143
testImplementation("org.burningwave:core:12.62.7")
22-
}
23-
24-
sourceSets {
25-
val samples by creating {
26-
java {
27-
srcDir("src/samples/java")
28-
}
29-
}
3044

31-
test {
32-
compileClasspath += samples.output
33-
runtimeClasspath += samples.output
34-
}
45+
approximations(approximationsRepo, "approximations", approximationsVersion)
46+
testImplementation(approximationsRepo, "tests", approximationsVersion)
3547
}
3648

3749
val samplesImplementation: Configuration by configurations.getting
@@ -43,3 +55,18 @@ dependencies {
4355
samplesImplementation("com.github.stephenc.findbugs:findbugs-annotations:${Versions.samplesFindBugs}")
4456
samplesImplementation("org.jetbrains:annotations:${Versions.samplesJetbrainsAnnotations}")
4557
}
58+
59+
val `usvm-api-jar` = tasks.register<Jar>("usvm-api-jar") {
60+
archiveBaseName.set(`usvm-api`.name)
61+
from(`usvm-api`.output)
62+
}
63+
64+
tasks.withType<Test> {
65+
dependsOn(`usvm-api-jar`)
66+
67+
val usvmApiJarPath = `usvm-api-jar`.get().outputs.files.singleFile
68+
val usvmApproximationJarPath = approximations.resolvedConfiguration.files.single()
69+
70+
environment("usvm.jvm.api.jar.path", usvmApiJarPath.absolutePath)
71+
environment("usvm.jvm.approximations.jar.path", usvmApproximationJarPath.absolutePath)
72+
}

0 commit comments

Comments
 (0)