From 2db7013eba0ba9e5efc7c7d2a4ad5c446104317d Mon Sep 17 00:00:00 2001
From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com>
Date: Mon, 30 Sep 2024 12:48:05 +0300
Subject: [PATCH] Minor refactoring

---
 .../main/kotlin/org/usvm/TSBinaryOperator.kt  | 21 ++++++++++---------
 .../kotlin/org/usvm/samples/TypeCoercion.kt   |  3 ++-
 .../org/usvm/util/TSMethodTestRunner.kt       |  1 +
 3 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt
index 2db24a0641..b3444c196d 100644
--- 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,13 +53,6 @@ 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 },
@@ -58,7 +60,6 @@ sealed class TSBinaryOperator(
 
     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
index 5099927788..9acba65bfb 100644
--- 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
index 1a59bebdf8..789255d0e1 100644
--- 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")
             }
         }