Skip to content

Commit 236d98d

Browse files
LipenLipen
committed
Refactor and add new operators
1 parent 3a6940f commit 236d98d

Some content is hidden

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

83 files changed

+3587
-1286
lines changed

‎usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,13 @@ sealed interface TsTestValue {
3333
data object TsException : TsTestValue
3434

3535
data class TsBoolean(val value: Boolean) : TsTestValue
36-
data class TsString(val value: String) : TsTestValue
36+
37+
data class TsString(val value: String) : TsTestValue {
38+
override fun toString(): String {
39+
return "${this::class.simpleName}(value=\"$value\")"
40+
}
41+
}
42+
3743
data class TsBigInt(val value: String) : TsTestValue
3844

3945
sealed interface TsNumber : TsTestValue {

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -149,3 +149,36 @@ fun TsContext.mkNumericExpr(
149149
)
150150
)
151151
}
152+
153+
fun TsContext.mkNullishExpr(
154+
expr: UExpr<out USort>,
155+
scope: TsStepScope,
156+
): UBoolExpr {
157+
// Handle fake objects specially
158+
if (expr.isFakeObject()) {
159+
val fakeType = expr.getFakeType(scope)
160+
val ref = expr.extractRef(scope)
161+
// Only check for nullish if the fake object represents a reference type.
162+
// If it represents a primitive type (bool/number), it's never nullish.
163+
return mkIte(
164+
condition = fakeType.refTypeExpr,
165+
trueBranch = mkOr(
166+
mkHeapRefEq(ref, mkTsNullValue()),
167+
mkHeapRefEq(ref, mkUndefinedValue())
168+
),
169+
falseBranch = mkFalse(),
170+
)
171+
}
172+
173+
// Regular reference is nullish if it is either null or undefined
174+
if (expr.sort == addressSort) {
175+
val ref = expr.asExpr(addressSort)
176+
return mkOr(
177+
mkHeapRefEq(ref, mkTsNullValue()),
178+
mkHeapRefEq(ref, mkUndefinedValue())
179+
)
180+
}
181+
182+
// Non-reference types (numbers, booleans, strings) are never nullish
183+
return mkFalse()
184+
}

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

Lines changed: 190 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,7 @@ import org.usvm.machine.state.lastStmt
124124
import org.usvm.machine.state.localsCount
125125
import org.usvm.machine.state.newStmt
126126
import org.usvm.machine.types.EtsAuxiliaryType
127+
import org.usvm.machine.types.iteWriteIntoFakeObject
127128
import org.usvm.machine.types.mkFakeValue
128129
import org.usvm.sizeSort
129130
import org.usvm.util.EtsHierarchy
@@ -251,9 +252,10 @@ class TsExprResolver(
251252
return resolveUnaryOperator(TsUnaryOperator.Neg, expr)
252253
}
253254

254-
override fun visit(expr: EtsUnaryPlusExpr): UExpr<out USort>? {
255-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
256-
error("Not supported $expr")
255+
override fun visit(expr: EtsUnaryPlusExpr): UExpr<out USort>? = with(ctx) {
256+
// Unary plus converts its operand to a number
257+
val arg = resolve(expr.arg) ?: return null
258+
return mkNumericExpr(arg, scope)
257259
}
258260

259261
override fun visit(expr: EtsPostIncExpr): UExpr<out USort>? {
@@ -276,9 +278,26 @@ class TsExprResolver(
276278
error("Not supported $expr")
277279
}
278280

279-
override fun visit(expr: EtsBitNotExpr): UExpr<out USort>? {
280-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
281-
error("Not supported $expr")
281+
override fun visit(expr: EtsBitNotExpr): UExpr<out USort>? = with(ctx) {
282+
// Bitwise NOT: converts operand to 32-bit signed integer and inverts all bits
283+
val arg = resolve(expr.arg) ?: return null
284+
val numericArg = mkNumericExpr(arg, scope)
285+
286+
// Convert to 32-bit integer, perform bitwise NOT, then convert back to number
287+
val bvArg = mkFpToBvExpr(
288+
roundingMode = fpRoundingModeSortDefaultValue(),
289+
value = numericArg.asExpr(fp64Sort),
290+
bvSize = 32,
291+
isSigned = true
292+
)
293+
val notResult = mkBvNotExpr(bvArg)
294+
295+
return mkBvToFpExpr(
296+
fp64Sort,
297+
fpRoundingModeSortDefaultValue(),
298+
notResult,
299+
signed = true
300+
)
282301
}
283302

284303
override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) {
@@ -373,14 +392,43 @@ class TsExprResolver(
373392
error("Not supported $expr")
374393
}
375394

376-
override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? {
377-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
378-
error("Not supported $expr")
395+
override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? = with(ctx) {
396+
// The delete operator removes a property from an object and returns true/false
397+
// For property access like "delete obj.prop", we need to handle EtsInstanceFieldRef
398+
when (val operand = expr.arg) {
399+
is EtsInstanceFieldRef -> {
400+
val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null
401+
402+
// Check for null/undefined access
403+
checkUndefinedOrNullPropertyRead(instance) ?: return null
404+
405+
// For now, we simulate deletion by setting the property to undefined
406+
// This is a simplification of the real semantics but sufficient for basic cases
407+
// TODO: This is incorrect for cases that the existing field is not of sort Address.
408+
// In such case, the "overwriting" the field value with undefined does nothing
409+
// to the actual number/boolean/string value inside the field,
410+
// [if only we read the field using that "other" sort].
411+
val fieldLValue = mkFieldLValue(addressSort, instance, operand.field)
412+
scope.doWithState {
413+
memory.write(fieldLValue, mkUndefinedValue(), guard = trueExpr)
414+
}
415+
416+
// The delete operator returns true in most cases for property deletion
417+
mkTrue()
418+
}
419+
420+
else -> {
421+
// For other operands (like variables), delete typically returns true without effect
422+
resolve(operand) ?: return null // Evaluate for potential side effects
423+
mkTrue()
424+
}
425+
}
379426
}
380427

381-
override fun visit(expr: EtsVoidExpr): UExpr<out USort>? {
382-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
383-
error("Not supported $expr")
428+
override fun visit(expr: EtsVoidExpr): UExpr<out USort>? = with(ctx) {
429+
// The void operator evaluates its operand for side effects and returns undefined.
430+
resolve(expr.arg) ?: return null
431+
return mkUndefinedValue()
384432
}
385433

386434
override fun visit(expr: EtsAwaitExpr): UExpr<out USort>? = with(ctx) {
@@ -390,6 +438,10 @@ class TsExprResolver(
390438
if (arg.sort != addressSort) {
391439
return arg
392440
}
441+
// ...including null/undefined
442+
if (arg == mkTsNullValue() || arg == mkUndefinedValue()) {
443+
return arg
444+
}
393445

394446
val promise = arg.asExpr(addressSort)
395447
check(isAllocatedConcreteHeapRef(promise)) {
@@ -529,39 +581,123 @@ class TsExprResolver(
529581
error("Not supported $expr")
530582
}
531583

532-
override fun visit(expr: EtsBitAndExpr): UExpr<out USort>? {
533-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
534-
error("Not supported $expr")
584+
override fun visit(expr: EtsBitAndExpr): UExpr<out USort>? = with(ctx) {
585+
val left = resolve(expr.left) ?: return null
586+
val right = resolve(expr.right) ?: return null
587+
588+
val leftNum = mkNumericExpr(left, scope)
589+
val rightNum = mkNumericExpr(right, scope)
590+
591+
// Convert to 32-bit integers, perform bitwise AND, then convert back
592+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
593+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
594+
val result = mkBvAndExpr(leftBv, rightBv)
595+
596+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true)
535597
}
536598

537-
override fun visit(expr: EtsBitOrExpr): UExpr<out USort>? {
538-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
539-
error("Not supported $expr")
599+
override fun visit(expr: EtsBitOrExpr): UExpr<out USort>? = with(ctx) {
600+
val left = resolve(expr.left) ?: return null
601+
val right = resolve(expr.right) ?: return null
602+
603+
val leftNum = mkNumericExpr(left, scope)
604+
val rightNum = mkNumericExpr(right, scope)
605+
606+
// Convert to 32-bit integers, perform bitwise OR, then convert back
607+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
608+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
609+
val result = mkBvOrExpr(leftBv, rightBv)
610+
611+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true)
540612
}
541613

542-
override fun visit(expr: EtsBitXorExpr): UExpr<out USort>? {
543-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
544-
error("Not supported $expr")
614+
override fun visit(expr: EtsBitXorExpr): UExpr<out USort>? = with(ctx) {
615+
val left = resolve(expr.left) ?: return null
616+
val right = resolve(expr.right) ?: return null
617+
618+
val leftNum = mkNumericExpr(left, scope)
619+
val rightNum = mkNumericExpr(right, scope)
620+
621+
// Convert to 32-bit integers, perform bitwise XOR, then convert back
622+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
623+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
624+
val result = mkBvXorExpr(leftBv, rightBv)
625+
626+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true)
545627
}
546628

547-
override fun visit(expr: EtsLeftShiftExpr): UExpr<out USort>? {
548-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
549-
error("Not supported $expr")
629+
override fun visit(expr: EtsLeftShiftExpr): UExpr<out USort>? = with(ctx) {
630+
val left = resolve(expr.left) ?: return null
631+
val right = resolve(expr.right) ?: return null
632+
633+
val leftNum = mkNumericExpr(left, scope)
634+
val rightNum = mkNumericExpr(right, scope)
635+
636+
// Convert to 32-bit integers and perform left shift
637+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
638+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
639+
640+
// Mask the shift amount to 5 bits (0-31) as per JavaScript spec
641+
val shiftAmount = mkBvAndExpr(rightBv, mkBv(0x1F, 32u))
642+
val result = mkBvShiftLeftExpr(leftBv, shiftAmount)
643+
644+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true)
550645
}
551646

552-
override fun visit(expr: EtsRightShiftExpr): UExpr<out USort>? {
553-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
554-
error("Not supported $expr")
647+
override fun visit(expr: EtsRightShiftExpr): UExpr<out USort>? = with(ctx) {
648+
val left = resolve(expr.left) ?: return null
649+
val right = resolve(expr.right) ?: return null
650+
651+
val leftNum = mkNumericExpr(left, scope)
652+
val rightNum = mkNumericExpr(right, scope)
653+
654+
// Convert to 32-bit integers and perform signed right shift
655+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
656+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
657+
658+
// Mask the shift amount to 5 bits (0-31)
659+
val shiftAmount = mkBvAndExpr(rightBv, mkBv(0x1F, 32u))
660+
val result = mkBvArithShiftRightExpr(leftBv, shiftAmount)
661+
662+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true)
555663
}
556664

557-
override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr<out USort>? {
558-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
559-
error("Not supported $expr")
665+
override fun visit(expr: EtsUnsignedRightShiftExpr): UExpr<out USort>? = with(ctx) {
666+
val left = resolve(expr.left) ?: return null
667+
val right = resolve(expr.right) ?: return null
668+
669+
val leftNum = mkNumericExpr(left, scope)
670+
val rightNum = mkNumericExpr(right, scope)
671+
672+
// Convert to 32-bit integers and perform unsigned right shift
673+
val leftBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), leftNum.asExpr(fp64Sort), 32, true)
674+
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true)
675+
676+
// Mask the shift amount to 5 bits (0-31)
677+
val shiftAmount = mkBvAndExpr(rightBv, mkBv(0x1F, 32u))
678+
val result = mkBvLogicalShiftRightExpr(leftBv, shiftAmount)
679+
680+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = false)
560681
}
561682

562-
override fun visit(expr: EtsNullishCoalescingExpr): UExpr<out USort>? {
563-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
564-
error("Not supported $expr")
683+
override fun visit(expr: EtsNullishCoalescingExpr): UExpr<out USort>? = with(ctx) {
684+
val left = resolve(expr.left) ?: return null
685+
val right = resolve(expr.right) ?: return null
686+
687+
val leftIsNullish = mkNullishExpr(left, scope)
688+
689+
// If both operands have the same sort, use mkIte directly
690+
if (left.sort == right.sort) {
691+
val commonSort = left.sort
692+
return mkIte(
693+
condition = leftIsNullish,
694+
trueBranch = right.asExpr(commonSort),
695+
falseBranch = left.asExpr(commonSort)
696+
)
697+
}
698+
699+
// If sorts differ, create a fake object that can hold either value
700+
return iteWriteIntoFakeObject(scope, leftIsNullish, right, left)
565701
}
566702

567703
// endregion
@@ -606,9 +742,25 @@ class TsExprResolver(
606742
return ctx.mkOr(eq.asExpr(ctx.boolSort), gt.asExpr(ctx.boolSort))
607743
}
608744

609-
override fun visit(expr: EtsInExpr): UExpr<out USort>? {
610-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
611-
error("Not supported $expr")
745+
override fun visit(expr: EtsInExpr): UExpr<out USort>? = with(ctx) {
746+
val property = resolve(expr.left) ?: return null
747+
val obj = resolve(expr.right)?.asExpr(addressSort) ?: return null
748+
749+
// Check for null/undefined access
750+
checkUndefinedOrNullPropertyRead(obj) ?: return null
751+
752+
// For now, we simplify this by checking if the property name is a string
753+
// and assume the property exists if we can resolve it
754+
if (property.sort == addressSort) {
755+
val propertyRef = property.asExpr(addressSort)
756+
757+
// Check if it's a string constant - for now just return true
758+
// as implementing proper property existence checking requires more complex logic
759+
mkTrue()
760+
} else {
761+
// For non-reference property names (like number indices), assume they might exist
762+
mkTrue()
763+
}
612764
}
613765

614766
override fun visit(expr: EtsInstanceOfExpr): UExpr<out USort>? = with(ctx) {
@@ -823,6 +975,8 @@ class TsExprResolver(
823975
resolved.asExpr(addressSort)
824976
}
825977

978+
checkUndefinedOrNullPropertyRead(instance) ?: return null
979+
826980
val resolvedArgs = expr.args.map { resolve(it) ?: return null }
827981

828982
val virtualCall = TsVirtualMethodCallStmt(

0 commit comments

Comments
 (0)