boolToFpSort bug fix

UnitTestBot · Sep 30, 2024 · cbd2070 · cbd2070
1 parent 6abe719
commit cbd2070
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 10 deletions.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt
@@ -8,6 +8,7 @@ sealed class TSBinaryOperator(
     val onFp: TSContext.(UExpr<UFpSort>, UExpr<UFpSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val onRef: TSContext.(UExpr<UAddressSort>, UExpr<UAddressSort>) -> UExpr<out USort> = shouldNotBeCalled,
     val desiredSort: TSContext.(USort, USort) -> USort = { _, _ -> error("Should not be called") },
+    val banSorts: TSContext.(UExpr<out USort>, UExpr<out USort>) -> Set<USort> = {_, _ -> emptySet() },
 ) {
 
     object Eq : TSBinaryOperator(
@@ -24,6 +25,22 @@ sealed class TSBinaryOperator(
         onFp = { lhs, rhs -> mkFpEqualExpr(lhs, rhs).not() },
         onRef = { lhs, rhs -> lhs.neq(rhs) },
         desiredSort = { lhs, _ -> lhs },
+        banSorts = { lhs, rhs ->
+            when {
+                lhs is TSWrappedValue ->
+                    // rhs.sort == addressSort is a mock not to cause undefined
+                    // behaviour with support of new language features.
+                    if (rhs is TSWrappedValue || rhs.sort == addressSort) emptySet() else TSTypeSystem.primitiveTypes
+                        .map(::typeToSort).toSet()
+                        .minus(rhs.sort)
+                rhs is TSWrappedValue ->
+                    // lhs.sort == addressSort explained as above.
+                    if (lhs.sort == addressSort) emptySet() else TSTypeSystem.primitiveTypes
+                        .map(::typeToSort).toSet()
+                        .minus(lhs.sort)
+                else -> emptySet()
+            }
+        }
     )
 
     object Add : TSBinaryOperator(
@@ -46,13 +63,17 @@ sealed class TSBinaryOperator(
     )
 
     internal operator fun invoke(lhs: UExpr<out USort>, rhs: UExpr<out USort>, scope: TSStepScope): UExpr<out USort> {
-        val lhsSort = lhs.sort
-        val rhsSort = rhs.sort
+        val bannedSorts = lhs.tctx.banSorts(lhs, rhs)
 
         fun apply(lhs: UExpr<out USort>, rhs: UExpr<out USort>): UExpr<out USort>? {
             val ctx = lhs.tctx
-            if (ctx.desiredSort(lhs.sort, rhs.sort) != lhs.sort) return null
-            assert(lhs.sort == rhs.sort)
+            val lhsSort = lhs.sort
+            val rhsSort = rhs.sort
+            assert(lhsSort == rhsSort)
+
+            if (lhsSort in bannedSorts) return null
+            if (ctx.desiredSort(lhsSort, rhsSort) != lhsSort) return null
+
             return when (lhs.sort) {
                 is UBoolSort -> ctx.onBool(lhs.cast(), rhs.cast())
                 is UBvSort -> ctx.onBv(lhs.cast(), rhs.cast())
@@ -62,6 +83,9 @@ sealed class TSBinaryOperator(
             }
         }
 
+        val lhsSort = lhs.sort
+        val rhsSort = rhs.sort
+
         val ctx = lhs.tctx
         val sort = ctx.desiredSort(lhsSort, rhsSort)
 

diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt
@@ -78,7 +78,7 @@ class TSExprTransformer(
      */
     private fun generateAdditionalExprs(): List<UExpr<out USort>> = with(ctx) {
         val newExpr = when (baseExpr.sort) {
-            addressSort -> addedExprCache.putOrNull(mkEq(asFp64(), boolToFpSort(asBool())))
+            addressSort -> addedExprCache.putOrNull(mkEq(fpToBoolSort(asFp64()), asBool()))
             else -> null
         }
 
@@ -101,7 +101,7 @@ class TSExprTransformer(
     fun asBool(): UExpr<KBoolSort> = exprCache.getOrPut(ctx.boolSort) {
         when (baseExpr.sort) {
             ctx.boolSort -> baseExpr
-            ctx.fp64Sort -> with(ctx) { mkIte(mkFpEqualExpr(baseExpr.cast(), mkFp64(1.0)), mkTrue(), mkFalse()) }
+            ctx.fp64Sort -> ctx.fpToBoolSort(baseExpr.cast())
             ctx.addressSort -> with(ctx) {
                 TSRefTransformer(ctx, boolSort).apply(baseExpr.cast()).cast()
             }

diff --git a/usvm-ts/src/main/kotlin/org/usvm/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt
@@ -1,5 +1,6 @@
 package org.usvm
 
+import io.ksmt.sort.KFp64Sort
 import org.usvm.memory.ULValue
 import org.usvm.memory.UWritableMemory
 
@@ -8,7 +9,12 @@ fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) {
     write(ref as ULValue<*, USort>, value as UExpr<USort>, value.uctx.trueExpr)
 }
 
-fun UContext<*>.boolToFpSort(expr: UExpr<UBoolSort>) = mkIte(expr, mkFp64(1.0), mkFp64(0.0))
+// Built-in KContext.bvToBool has identical implementation.
+fun UContext<*>.boolToFpSort(expr: UExpr<UBoolSort>) =
+    mkIte(expr, mkFp64(1.0), mkFp64(0.0))
+
+fun UContext<*>.fpToBoolSort(expr: UExpr<KFp64Sort>) =
+    mkIte(mkFpEqualExpr(expr, mkFp64(0.0)), mkFalse(), mkTrue())
 
 fun UExpr<*>.unwrapJoinedExpr(ctx: UContext<*>): UExpr<out USort> =
     if (this is UJoinedBoolExpr) ctx.mkAnd(exprs) else this

diff --git a/usvm-ts/src/test/resources/samples/TypeCoercion.ts b/usvm-ts/src/test/resources/samples/TypeCoercion.ts
@@ -50,10 +50,14 @@ class TypeCoercion {
     transitiveCoercionNoTypes(a, b, c): number {
         // @ts-ignore
         if (a == b) {
-            if (c && (a == c)) {
-                return 1
+            if (c != 0 && c != 1) {
+                if (c && (a == c)) {
+                    return 1
+                } else {
+                    return 2
+                }
             } else {
-                return 2
+                return 4
             }
         }