Add mkNumericExpr (#255)

Author: Lipen

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

@@ -1,5 +1,6 @@
 package org.usvm.machine.expr
 
+import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
@@ -12,15 +13,17 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.machine.types.FakeType
 import org.usvm.types.single
+import org.usvm.util.boolToFp
 
-fun TsContext.mkTruthyExpr(expr: UExpr<out USort>, scope: TsStepScope): UBoolExpr = scope.calcOnState {
+fun TsContext.mkTruthyExpr(
+    expr: UExpr<out USort>,
+    scope: TsStepScope,
+): UBoolExpr = scope.calcOnState {
     if (expr.isFakeObject()) {
         val falseBranchGround = makeSymbolicPrimitive(boolSort)
 
         val conjuncts = mutableListOf<ExprWithTypeConstraint<UBoolSort>>()
-        val possibleType = scope.calcOnState {
-            memory.types.getTypeStream(expr.asExpr(addressSort))
-        }.single() as FakeType
+        val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as FakeType
 
         scope.assert(possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr))
 
@@ -82,3 +85,43 @@ fun TsContext.mkTruthyExpr(expr: UExpr<out USort>, scope: TsStepScope): UBoolExp
         }
     }
 }
+
+fun TsContext.mkNumericExpr(
+    expr: UExpr<out USort>,
+    scope: TsStepScope,
+): UExpr<KFp64Sort> = scope.calcOnState {
+
+    // 7.1.4 ToNumber ( argument )
+    //
+    // 1. If argument is a Number, return argument.
+    // 2. If argument is either a Symbol or a BigInt, throw a TypeError exception.
+    // 3. If argument is undefined, return NaN.
+    // 4. If argument is either null or false, return +0𝔽.
+    // 5. If argument is true, return 1𝔽.
+    // 6. If argument is a String, return StringToNumber(argument).
+    // 7. Assert: argument is an Object.
+    // 8. Let primValue be ToPrimitive(argument, "number").
+    // 9. Assert: primValue is not an Object.
+    // 10. Return ToNumber(primValue).
+
+    if (expr.sort == fp64Sort) {
+        return@calcOnState expr.asExpr(fp64Sort)
+    }
+
+    if (expr == mkUndefinedValue()) {
+        return@calcOnState mkFp64NaN()
+    }
+
+    if (expr == mkTsNullValue()) {
+        return@calcOnState mkFp64(0.0)
+    }
+
+    if (expr.sort == boolSort) {
+        return@calcOnState boolToFp(expr.asExpr(boolSort))
+    }
+
+    // TODO: ToPrimitive, then ToNumber again
+    // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
+
+    error("Unsupported sort: ${expr.sort}")
+}

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

@@ -424,6 +424,13 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsStaticCallExpr): UExpr<out USort>? {
+        if (expr.method.name == "Number" && expr.method.enclosingClass.name == "") {
+            check(expr.args.size == 1) { "Number constructor should have exactly one argument" }
+            return resolveAfterResolved(expr.args.single()) {
+                ctx.mkNumericExpr(it, scope)
+            }
+        }
+
         return resolveInvoke(
             method = expr.method,
             instance = null,

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt

@@ -3,18 +3,19 @@ package org.usvm.machine.operator
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
 import org.usvm.UAddressSort
-import org.usvm.UBoolSort
+import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.machine.TsContext
+import org.usvm.machine.expr.mkNumericExpr
 import org.usvm.machine.expr.mkTruthyExpr
 import org.usvm.machine.interpreter.TsStepScope
 
 sealed interface TsUnaryOperator {
 
     fun TsContext.resolveBool(
-        arg: UExpr<UBoolSort>,
+        arg: UBoolExpr,
         scope: TsStepScope,
     ): UExpr<out USort>
 
@@ -50,70 +51,61 @@ sealed interface TsUnaryOperator {
 
     data object Not : TsUnaryOperator {
         override fun TsContext.resolveBool(
-            arg: UExpr<UBoolSort>,
+            arg: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<out USort> {
+        ): UBoolExpr {
             return mkNot(arg)
         }
 
         override fun TsContext.resolveFp(
             arg: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<out USort> {
+        ): UBoolExpr {
             return mkNot(mkTruthyExpr(arg, scope))
         }
 
         override fun TsContext.resolveRef(
             arg: UExpr<UAddressSort>,
             scope: TsStepScope,
-        ): UExpr<out USort> {
+        ): UBoolExpr {
             return mkNot(mkTruthyExpr(arg, scope))
         }
 
         override fun TsContext.resolveFake(
             arg: UConcreteHeapRef,
             scope: TsStepScope,
-        ): UExpr<out USort> {
-            TODO("Not yet implemented")
+        ): UBoolExpr {
+            return mkNot(mkTruthyExpr(arg, scope))
         }
     }
 
     data object Neg : TsUnaryOperator {
         override fun TsContext.resolveBool(
-            arg: UExpr<UBoolSort>,
+            arg: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<out USort> {
-            // -true = -1.0
-            // -false = -0.0
-            @Suppress("MagicNumber")
-            return mkIte(arg, mkFp64(-1.0), mkFp64(-0.0))
+        ): UExpr<KFp64Sort> {
+            return mkFpNegationExpr(mkNumericExpr(arg, scope))
         }
 
         override fun TsContext.resolveFp(
             arg: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<out USort> {
+        ): UExpr<KFp64Sort> {
             return mkFpNegationExpr(arg)
         }
 
         override fun TsContext.resolveRef(
             arg: UExpr<UAddressSort>,
             scope: TsStepScope,
-        ): UExpr<out USort> {
-            // -undefined = NaN
-            if (arg == mkUndefinedValue()) {
-                return mkFp64NaN()
-            }
-
-            // TODO: convert to numeric value and then negate
-            TODO("Not yet implemented")
+        ): UExpr<KFp64Sort> {
+            return mkFpNegationExpr(mkNumericExpr(arg, scope))
         }
 
         override fun TsContext.resolveFake(
             arg: UConcreteHeapRef,
             scope: TsStepScope,
-        ): UExpr<out USort> {
-            TODO("Not yet implemented")
+        ): UExpr<KFp64Sort> {
+            return mkFpNegationExpr(mkNumericExpr(arg, scope))
         }
     }
 }