Support OR operator (#245)

UnitTestBot · Feb 7, 2025 · 62b17f8 · 62b17f8
1 parent a682a99
commit 62b17f8
Show file tree

Hide file tree

Showing 6 changed files with 384 additions and 72 deletions.
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "deeaae6dbf"
+    const val jacodb = "ad9d0475be"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

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
@@ -170,6 +170,10 @@ class TSExprResolver(
         return resolveBinaryOperator(TSBinaryOperator.And, expr)
     }
 
+    override fun visit(expr: EtsOrExpr): UExpr<out USort>? {
+        return resolveBinaryOperator(TSBinaryOperator.Or, expr)
+    }
+
     override fun visit(expr: EtsNotEqExpr): UExpr<out USort>? {
         return resolveBinaryOperator(TSBinaryOperator.Neq, expr)
     }
@@ -319,11 +323,6 @@ class TSExprResolver(
         error("Not supported $expr")
     }
 
-    override fun visit(expr: EtsOrExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
-    }
-
     override fun visit(expr: EtsPostDecExpr): UExpr<out USort>? {
         logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
         error("Not supported $expr")

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
@@ -508,4 +508,56 @@ sealed interface TSBinaryOperator {
             }
         }
     }
+
+    data object Or : TSBinaryOperator {
+        override fun TSContext.onBool(
+            lhs: UExpr<UBoolSort>,
+            rhs: UExpr<UBoolSort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            return mkOr(lhs, rhs)
+        }
+
+        override fun TSContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TSContext.onRef(
+            lhs: UExpr<UAddressSort>,
+            rhs: UExpr<UAddressSort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun resolveFakeObject(
+            lhs: UExpr<out USort>,
+            rhs: UExpr<out USort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> = with(lhs.tctx) {
+            check(lhs.isFakeObject() || rhs.isFakeObject())
+
+            scope.calcOnState {
+                val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
+                iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
+            }
+        }
+
+        override fun internalResolve(
+            lhs: UExpr<out USort>,
+            rhs: UExpr<out USort>,
+            scope: TSStepScope,
+        ): UExpr<out USort> = with(lhs.tctx) {
+            check(!lhs.isFakeObject() && !rhs.isFakeObject())
+
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
+            scope.calcOnState {
+                iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
+            }
+        }
+    }
 }