Skip to content

Commit 94d3bfe

Browse files
LipenLipen
authored
[usvm-ts] Support unary minus (#251)
1 parent 6933fab commit 94d3bfe

File tree

4 files changed

+199
-40
lines changed

4 files changed

+199
-40
lines changed

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

Lines changed: 17 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,6 @@ import org.jacodb.ets.base.EtsNotExpr
4040
import org.jacodb.ets.base.EtsNullConstant
4141
import org.jacodb.ets.base.EtsNullishCoalescingExpr
4242
import org.jacodb.ets.base.EtsNumberConstant
43-
import org.jacodb.ets.base.EtsNumberType
4443
import org.jacodb.ets.base.EtsOrExpr
4544
import org.jacodb.ets.base.EtsParameterRef
4645
import org.jacodb.ets.base.EtsPostDecExpr
@@ -61,9 +60,9 @@ import org.jacodb.ets.base.EtsTernaryExpr
6160
import org.jacodb.ets.base.EtsThis
6261
import org.jacodb.ets.base.EtsType
6362
import org.jacodb.ets.base.EtsTypeOfExpr
63+
import org.jacodb.ets.base.EtsUnaryExpr
6464
import org.jacodb.ets.base.EtsUnaryPlusExpr
6565
import org.jacodb.ets.base.EtsUndefinedConstant
66-
import org.jacodb.ets.base.EtsUnknownType
6766
import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
6867
import org.jacodb.ets.base.EtsValue
6968
import org.jacodb.ets.base.EtsVoidExpr
@@ -107,6 +106,18 @@ class TsExprResolver(
107106
return expr.accept(this)
108107
}
109108

109+
private fun resolveUnaryOperator(
110+
operator: TsUnaryOperator,
111+
expr: EtsUnaryExpr,
112+
): UExpr<out USort>? = resolveUnaryOperator(operator, expr.arg)
113+
114+
private fun resolveUnaryOperator(
115+
operator: TsUnaryOperator,
116+
arg: EtsEntity,
117+
): UExpr<out USort>? = resolveAfterResolved(arg) { resolved ->
118+
with(operator) { ctx.resolve(resolved, scope) }
119+
}
120+
110121
private fun resolveBinaryOperator(
111122
operator: TsBinaryOperator,
112123
expr: EtsBinaryExpr,
@@ -181,28 +192,13 @@ class TsExprResolver(
181192

182193
// region UNARY
183194

184-
override fun visit(expr: EtsNotExpr): UExpr<out USort>? = with(ctx) {
185-
resolveAfterResolved(expr.arg) { arg ->
186-
if (arg.sort == boolSort) {
187-
arg.asExpr(boolSort).not()
188-
} else {
189-
TsUnaryOperator.Not(arg, scope)
190-
}
191-
}
195+
override fun visit(expr: EtsNotExpr): UExpr<out USort>? {
196+
return resolveUnaryOperator(TsUnaryOperator.Not, expr)
192197
}
193198

194199
// TODO move into TsUnaryOperator
195-
override fun visit(expr: EtsNegExpr): UExpr<out USort>? = with(ctx) {
196-
if (expr.type is EtsNumberType) {
197-
val arg = resolve(expr.arg)?.asExpr(fp64Sort) ?: return null
198-
return mkFpNegationExpr(arg)
199-
}
200-
201-
if (expr.type is EtsUnknownType) {
202-
TODO()
203-
}
204-
205-
error("Unsupported expr type ${expr.type} for negation")
200+
override fun visit(expr: EtsNegExpr): UExpr<out USort>? {
201+
return resolveUnaryOperator(TsUnaryOperator.Neg, expr)
206202
}
207203

208204
override fun visit(expr: EtsUnaryPlusExpr): UExpr<out USort>? {

‎usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsUnaryOperator.kt‎

Lines changed: 105 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,119 @@
11
package org.usvm.machine.operator
22

3-
import io.ksmt.expr.KExpr
3+
import io.ksmt.sort.KFp64Sort
4+
import io.ksmt.utils.asExpr
5+
import org.usvm.UAddressSort
46
import org.usvm.UBoolSort
5-
import org.usvm.UBvSort
7+
import org.usvm.UConcreteHeapRef
68
import org.usvm.UExpr
7-
import org.usvm.UFpSort
89
import org.usvm.USort
910
import org.usvm.machine.TsContext
10-
import org.usvm.machine.expr.tctx
11+
import org.usvm.machine.expr.mkTruthyExpr
1112
import org.usvm.machine.interpreter.TsStepScope
1213

13-
sealed class TsUnaryOperator(
14-
val onBool: TsContext.(UExpr<UBoolSort>) -> UExpr<out USort> = shouldNotBeCalled,
15-
val onBv: TsContext.(UExpr<UBvSort>) -> UExpr<out USort> = shouldNotBeCalled,
16-
val onFp: TsContext.(UExpr<UFpSort>) -> UExpr<out USort> = shouldNotBeCalled,
17-
val desiredSort: TsContext.(USort) -> USort = { _ -> error("Should not be called") },
18-
) {
14+
sealed interface TsUnaryOperator {
1915

20-
data object Not : TsUnaryOperator(
21-
onBool = TsContext::mkNot,
22-
desiredSort = { boolSort },
23-
)
16+
fun TsContext.resolveBool(
17+
arg: UExpr<UBoolSort>,
18+
scope: TsStepScope,
19+
): UExpr<out USort>
2420

25-
internal operator fun invoke(operand: UExpr<out USort>, scope: TsStepScope): UExpr<out USort> = with(operand.tctx) {
26-
TODO()
21+
fun TsContext.resolveFp(
22+
arg: UExpr<KFp64Sort>,
23+
scope: TsStepScope,
24+
): UExpr<out USort>
25+
26+
fun TsContext.resolveRef(
27+
arg: UExpr<UAddressSort>,
28+
scope: TsStepScope,
29+
): UExpr<out USort>
30+
31+
fun TsContext.resolveFake(
32+
arg: UConcreteHeapRef,
33+
scope: TsStepScope,
34+
): UExpr<out USort>
35+
36+
fun TsContext.resolve(
37+
arg: UExpr<out USort>,
38+
scope: TsStepScope,
39+
): UExpr<out USort> {
40+
if (arg.isFakeObject()) {
41+
return resolveFake(arg, scope)
42+
}
43+
return when (arg.sort) {
44+
boolSort -> resolveBool(arg.asExpr(boolSort), scope)
45+
fp64Sort -> resolveFp(arg.asExpr(fp64Sort), scope)
46+
addressSort -> resolveRef(arg.asExpr(addressSort), scope)
47+
else -> TODO("Unsupported sort: ${arg.sort}")
48+
}
49+
}
50+
51+
data object Not : TsUnaryOperator {
52+
override fun TsContext.resolveBool(
53+
arg: UExpr<UBoolSort>,
54+
scope: TsStepScope,
55+
): UExpr<out USort> {
56+
return mkNot(arg)
57+
}
58+
59+
override fun TsContext.resolveFp(
60+
arg: UExpr<KFp64Sort>,
61+
scope: TsStepScope,
62+
): UExpr<out USort> {
63+
return mkNot(mkTruthyExpr(arg, scope))
64+
}
65+
66+
override fun TsContext.resolveRef(
67+
arg: UExpr<UAddressSort>,
68+
scope: TsStepScope,
69+
): UExpr<out USort> {
70+
return mkNot(mkTruthyExpr(arg, scope))
71+
}
72+
73+
override fun TsContext.resolveFake(
74+
arg: UConcreteHeapRef,
75+
scope: TsStepScope,
76+
): UExpr<out USort> {
77+
TODO("Not yet implemented")
78+
}
2779
}
2880

29-
companion object {
30-
private val shouldNotBeCalled: TsContext.(UExpr<out USort>) -> KExpr<out USort> =
31-
{ _ -> error("Should not be called") }
81+
data object Neg : TsUnaryOperator {
82+
override fun TsContext.resolveBool(
83+
arg: UExpr<UBoolSort>,
84+
scope: TsStepScope,
85+
): UExpr<out USort> {
86+
// -true = -1.0
87+
// -false = -0.0
88+
@Suppress("MagicNumber")
89+
return mkIte(arg, mkFp64(-1.0), mkFp64(-0.0))
90+
}
91+
92+
override fun TsContext.resolveFp(
93+
arg: UExpr<KFp64Sort>,
94+
scope: TsStepScope,
95+
): UExpr<out USort> {
96+
return mkFpNegationExpr(arg)
97+
}
98+
99+
override fun TsContext.resolveRef(
100+
arg: UExpr<UAddressSort>,
101+
scope: TsStepScope,
102+
): UExpr<out USort> {
103+
// -undefined = NaN
104+
if (arg == mkUndefinedValue()) {
105+
return mkFp64NaN()
106+
}
107+
108+
// TODO: convert to numeric value and then negate
109+
TODO("Not yet implemented")
110+
}
111+
112+
override fun TsContext.resolveFake(
113+
arg: UConcreteHeapRef,
114+
scope: TsStepScope,
115+
): UExpr<out USort> {
116+
TODO("Not yet implemented")
117+
}
32118
}
33119
}

‎usvm-ts/src/test/kotlin/org/usvm/samples/Neg.kt‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
package org.usvm.samples
2+
3+
import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME
4+
import org.jacodb.ets.model.EtsClassSignature
5+
import org.jacodb.ets.model.EtsScene
6+
import org.jacodb.ets.utils.loadEtsFileAutoConvert
7+
import org.junit.jupiter.api.Test
8+
import org.usvm.api.TsObject
9+
import org.usvm.util.TsMethodTestRunner
10+
import org.usvm.util.getResourcePath
11+
12+
class Neg : TsMethodTestRunner() {
13+
14+
override val scene: EtsScene = run {
15+
val name = "Neg.ts"
16+
val path = getResourcePath("/samples/$name")
17+
val file = loadEtsFileAutoConvert(path)
18+
EtsScene(listOf(file))
19+
}
20+
21+
@Test
22+
fun `test negateNumber`() {
23+
val method = getMethod("Neg", "negateNumber")
24+
discoverProperties<TsObject.TsNumber, TsObject.TsNumber>(
25+
method = method,
26+
{ x, r -> x.number.isNaN() && r.number.isNaN() },
27+
{ x, r -> x.number == 0.0 && r.number == 0.0 },
28+
{ x, r -> x.number > 0 && r.number == -x.number },
29+
{ x, r -> x.number < 0 && r.number == -x.number },
30+
invariants = arrayOf(
31+
{ x, r -> (x.number.isNaN() && r.number.isNaN()) || r.number == -x.number },
32+
)
33+
)
34+
}
35+
36+
@Test
37+
fun `test negateBoolean`() {
38+
val method = getMethod("Neg", "negateBoolean")
39+
discoverProperties<TsObject.TsBoolean, TsObject.TsNumber>(
40+
method = method,
41+
{ x, r -> x.value && r.number == -1.0 },
42+
{ x, r -> !x.value && r.number == -0.0 },
43+
)
44+
}
45+
46+
@Test
47+
fun `test negateUndefined`() {
48+
val method = getMethod("Neg", "negateUndefined")
49+
discoverProperties<TsObject.TsNumber>(
50+
method = method,
51+
{ r -> r.number.isNaN() },
52+
)
53+
}
54+
}

‎usvm-ts/src/test/resources/samples/Neg.ts‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
class Neg {
2+
negateNumber(x: number): number {
3+
let y = -x
4+
if (x != x) return y // -NaN == NaN
5+
if (x == 0) return y // -0 == 0
6+
if (x > 0) return y // -(x>0) == (x<0)
7+
if (x < 0) return y // -(x<0) == (x>0)
8+
// unreachable
9+
}
10+
11+
negateBoolean(x: boolean): number {
12+
let y = -x
13+
if (x) return y // -true == -1
14+
if (!x) return y // -false == -0
15+
// unreachable
16+
}
17+
18+
negateUndefined(): number {
19+
let x = undefined
20+
// @ts-ignore
21+
return -x // -undefined == NaN
22+
}
23+
}

0 commit comments

Comments
 (0)