Skip to content

Commit 4c0d9fb

Browse files
authored
[TS] Support await (#303)
1 parent d67fb63 commit 4c0d9fb

13 files changed

Lines changed: 559 additions & 101 deletions

File tree

buildSrc/src/main/kotlin/Dependencies.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ object Versions {
66
const val clikt = "5.0.0"
77
const val detekt = "1.23.7"
88
const val ini4j = "0.5.4"
9-
const val jacodb = "5889d3c784"
9+
const val jacodb = "da338ffc83"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,8 @@ class ExprTypeAnnotator(
7272
private val valueAnnotator: ValueTypeAnnotator,
7373
) : EtsExpr.Visitor<EtsExpr> {
7474

75+
private fun annotate(local: EtsLocal) = valueAnnotator.visit(local)
76+
7577
private fun annotate(value: EtsValue) = value.accept(valueAnnotator)
7678

7779
private fun annotate(expr: EtsExpr) = expr.accept(this)
@@ -267,8 +269,8 @@ class ExprTypeAnnotator(
267269
)
268270

269271
override fun visit(expr: EtsInstanceCallExpr): EtsExpr {
270-
val baseInferred = annotate(expr.instance) as EtsLocal // safe cast
271-
val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast
272+
val baseInferred = annotate(expr.instance)
273+
val argsInferred = expr.args.map { annotate(it) }
272274
val methodInferred = when (val baseType = baseInferred.type) {
273275
is EtsClassType -> {
274276
val etsClass = scene.projectAndSdkClasses.find { it.signature == baseType.signature }
@@ -284,13 +286,13 @@ class ExprTypeAnnotator(
284286
}
285287

286288
override fun visit(expr: EtsStaticCallExpr): EtsExpr {
287-
val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast
289+
val argsInferred = expr.args.map { annotate(it) }
288290
return expr.copy(args = argsInferred)
289291
}
290292

291293
override fun visit(expr: EtsPtrCallExpr): EtsExpr {
292-
val ptrInferred = annotate(expr.ptr) as EtsLocal // safe cast
293-
val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast
294+
val ptrInferred = annotate(expr.ptr)
295+
val argsInferred = expr.args.map { annotate(it) }
294296
return expr.copy(ptr = ptrInferred, args = argsInferred)
295297
}
296298
}

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ import org.usvm.machine.expr.TsUndefinedSort
3636
import org.usvm.machine.expr.TsUnresolvedSort
3737
import org.usvm.machine.expr.TsVoidSort
3838
import org.usvm.machine.expr.TsVoidValue
39-
import org.usvm.machine.expr.tctx
4039
import org.usvm.machine.interpreter.TsStepScope
4140
import org.usvm.machine.types.EtsFakeType
4241
import org.usvm.memory.UReadOnlyMemory
@@ -173,13 +172,12 @@ class TsContext(
173172
return this
174173
}
175174

176-
fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef = with(tctx) {
177-
if (this@unwrapRefWithPathConstraint.isFakeObject()) {
175+
fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef {
176+
if (isFakeObject()) {
178177
scope.assert(getFakeType(scope).refTypeExpr)
179-
extractRef(scope)
180-
} else {
181-
asExpr(addressSort)
178+
return extractRef(scope)
182179
}
180+
return this
183181
}
184182

185183
fun createFakeObjectRef(): UConcreteHeapRef {
@@ -274,7 +272,6 @@ class Constants {
274272
}
275273
}
276274

277-
278275
enum class IntermediateLValueField {
279276
BOOL, FP, REF
280277
}

0 commit comments

Comments
 (0)