Fix missed type assertions for fake objects

UnitTestBot · Feb 11, 2025 · 8acf1da · 8acf1da
1 parent f3720f0
commit 8acf1da
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt
@@ -663,7 +663,7 @@ class TSSimpleValueResolver(
     }
 
     override fun visit(value: EtsNullConstant): UExpr<out USort> = with(ctx) {
-        scope.calcOnState { mkTSNullValue() }
+        mkTSNullValue()
     }
 
     override fun visit(value: EtsUndefinedConstant): UExpr<out USort> = with(ctx) {

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt
@@ -186,6 +186,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -206,6 +207,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.fpTypeExpr or lhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -218,6 +220,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(lhsType.refTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -250,6 +253,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -270,6 +274,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.fpTypeExpr or rhsType.boolTypeExpr)
                                 // TODO: support objects
                             }
 
@@ -282,6 +287,7 @@ sealed interface TSBinaryOperator {
                                     )
                                 )
 
+                                scope.assert(rhsType.refTypeExpr)
                                 // TODO: support objects
 
                             }

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt
@@ -2,10 +2,10 @@ package org.usvm.samples
 
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.RepeatedTest
 import org.usvm.api.TSObject
 import org.usvm.util.TSMethodTestRunner
 import org.usvm.util.getResourcePath
-import kotlin.test.Test
 
 class Null : TSMethodTestRunner() {
 
@@ -16,7 +16,7 @@ class Null : TSMethodTestRunner() {
         EtsScene(listOf(file))
     }
 
-    @Test
+    @RepeatedTest(20)
     fun testIsNull() {
         val method = getMethod("Null", "isNull")
         discoverProperties<TSObject, TSObject.TSNumber>(