Skip to content

Commit a6ae617

Browse files
committed
Operators implementation
1 parent d0ce04d commit a6ae617

File tree

2 files changed

+9
-6
lines changed

2 files changed

+9
-6
lines changed

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,6 @@ import org.usvm.util.mkFieldLValue
116116
import org.usvm.util.mkRegisterStackLValue
117117
import org.usvm.util.resolveEtsField
118118
import org.usvm.util.throwExceptionWithoutStackFrameDrop
119-
import org.usvm.util.type
120119

121120
private val logger = KotlinLogging.logger {}
122121

@@ -412,13 +411,17 @@ class TsExprResolver(
412411
}
413412

414413
override fun visit(expr: EtsLtEqExpr): UExpr<out USort>? {
415-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
416-
error("Not supported $expr")
414+
val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null
415+
val lt = resolve(EtsLtExpr(expr.left, expr.right)) ?: return null
416+
417+
return ctx.mkOr(eq.asExpr(ctx.boolSort), lt.asExpr(ctx.boolSort))
417418
}
418419

419420
override fun visit(expr: EtsGtEqExpr): UExpr<out USort>? {
420-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
421-
error("Not supported $expr")
421+
val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null
422+
val gt = resolve(EtsGtExpr(expr.left, expr.right)) ?: return null
423+
424+
return ctx.mkOr(eq.asExpr(ctx.boolSort), gt.asExpr(ctx.boolSort))
422425
}
423426

424427
override fun visit(expr: EtsInExpr): UExpr<out USort>? {

usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -342,7 +342,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
342342
pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
343343
exceptionsPropagation = true,
344344
timeout = Duration.INFINITE,
345-
stepsFromLastCovered = 50000L,
345+
stepsFromLastCovered = 3500L,
346346
solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
347347
typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
348348
)

0 commit comments

Comments
 (0)