Minor refactoring

UnitTestBot · Sep 30, 2024 · 2db7013 · 2db7013
1 parent cbd2070
commit 2db7013
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 11 deletions.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt
@@ -19,6 +19,13 @@ sealed class TSBinaryOperator(
         desiredSort = { lhs, _ -> lhs }
     )
 
+    // Neq must not be applied to a pair of expressions generated while initial Neq application.
+    // For example,
+    // "a (untyped arg) != 1.0 (fp64 number)"
+    // can't yield
+    // "a (bool reg reading) != true", since "1.0.toBool() = true" is a new value for 1.0.
+    //
+    // So, that's the reason why banSorts in Neq throws out all primitive types except one of the expressions' one.
     object Neq : TSBinaryOperator(
         onBool = { lhs, rhs -> lhs.neq(rhs) },
         onBv = { lhs, rhs -> lhs.neq(rhs) },
@@ -30,12 +37,14 @@ sealed class TSBinaryOperator(
                 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
+                    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
+                    if (lhs.sort == addressSort) emptySet() else
+                        TSTypeSystem.primitiveTypes
                         .map(::typeToSort).toSet()
                         .minus(lhs.sort)
                 else -> emptySet()
@@ -44,21 +53,13 @@ sealed class TSBinaryOperator(
     )
 
     object Add : TSBinaryOperator(
-        onBool = { lhs, rhs ->
-            mkFpAddExpr(
-                fpRoundingModeSortDefaultValue(),
-                boolToFpSort(lhs),
-                boolToFpSort(rhs)
-            )
-        },
         onFp = { lhs, rhs -> mkFpAddExpr(fpRoundingModeSortDefaultValue(), lhs, rhs) },
         onBv = UContext<TSSizeSort>::mkBvAddExpr,
         desiredSort = { _, _ -> fp64Sort },
     )
 
     object And : TSBinaryOperator(
         onBool = UContext<TSSizeSort>::mkAnd,
-        onBv = UContext<TSSizeSort>::mkBvAndExpr,
         desiredSort = { _, _ -> boolSort },
     )
 

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/TypeCoercion.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/TypeCoercion.kt
@@ -67,13 +67,14 @@ class TypeCoercion : TSMethodTestRunner() {
 
     @Test
     fun testTransitiveCoercionNoTypes() {
-        discoverProperties<TSObject.Object, TSObject.Object, TSObject.Object, TSObject.TSNumber>(
+        discoverProperties<TSObject, TSObject, TSObject, TSObject.TSNumber>(
             methodIdentifier = MethodDescriptor(
                 fileName = "TypeCoercion.ts",
                 className = "TypeCoercion",
                 methodName = "transitiveCoercionNoTypes",
                 argumentsNumber = 3
             ),
+            // Too complicated to write property matchers, examine run log to verify the test.
         )
     }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt
@@ -174,6 +174,7 @@ open class TSMethodTestRunner : TestRunner<TSTest, MethodDescriptor, EtsType?, T
                 TSObject.TSNumber.Integer::class -> EtsNumberType
                 TSObject.UndefinedObject::class -> EtsUndefinedType
                 TSObject.Object::class -> EtsUnknownType
+                TSObject::class -> EtsUnknownType
                 else -> error("Should not be called")
             }
         }