Skip to content

Commit

Permalink
Rewrite tests
Browse files Browse the repository at this point in the history
  • Loading branch information
Lipen committed Feb 19, 2025
1 parent a7c9864 commit e40180a
Show file tree
Hide file tree
Showing 3 changed files with 123 additions and 99 deletions.
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package org.usvm.machine.interpreter

import io.ksmt.utils.asExpr
import io.ksmt.utils.cast

Check warning

Code scanning / detekt

Detects unused imports Warning

Unused import
import mu.KotlinLogging
import org.jacodb.ets.base.EtsArrayAccess
import org.jacodb.ets.base.EtsAssignStmt
Expand All @@ -12,6 +13,7 @@ import org.jacodb.ets.base.EtsNopStmt
import org.jacodb.ets.base.EtsNullType
import org.jacodb.ets.base.EtsParameterRef
import org.jacodb.ets.base.EtsReturnStmt
import org.jacodb.ets.base.EtsStaticFieldRef
import org.jacodb.ets.base.EtsStmt
import org.jacodb.ets.base.EtsSwitchStmt
import org.jacodb.ets.base.EtsThis
Expand Down Expand Up @@ -169,6 +171,12 @@ class TsInterpreter(
memory.write(lValue, fakeExpr, guard = trueExpr)
}

is EtsStaticFieldRef -> {
val field = lhv.field
val lValue = TsStaticFieldLValue(field, expr.sort)
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
}

else -> TODO("Not yet implemented")
}

Expand Down
87 changes: 50 additions & 37 deletions usvm-ts/src/test/kotlin/org/usvm/samples/StaticFields.kt
Original file line number Diff line number Diff line change
Expand Up @@ -19,86 +19,99 @@ class StaticFields : TsMethodTestRunner() {
}

@Test
fun testStaticBasic() {
val method = getMethod("StaticBasic", "getValue")
fun testStaticNumber() {
val method = getMethod("StaticNumber", "getValue")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 42.0 }
{ r -> r.number == 10.0 },
)
}

@Test
fun testStaticModification() {
val method = getMethod("StaticModification", "incrementAndGet")
val method = getMethod("StaticModification", "incrementTwice")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 1.0 }
{ r -> r.number == 2.0 },
)
}

@Test
fun testStaticInheritance() {
val parentMethod = getMethod("ParentStatic", "getFamily")
val childMethod = getMethod("ChildStatic", "getChildFamily")
fun testStaticInheritanceParent() {
val method = getMethod("StaticChild", "getParentId")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 100.0 },
)
}

discoverProperties<TsValue.TsString>(
method = parentMethod,
{ r -> r.value == "Parent" }
@Test
fun testStaticInheritanceChild() {
val method = getMethod("StaticChild", "getChildId")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 200.0 },
)
}

discoverProperties<TsValue.TsString>(
method = childMethod,
{ r -> r.value == "Child" }
@Test
fun testStaticBooleanToggle() {
val method = getMethod("StaticBoolean", "toggleAndGet")
discoverProperties<TsValue.TsBoolean>(
method = method,
{ r -> r.value == false },
)
}

@Test
fun testStaticShadowing() {
val method = getMethod("ShadowChild", "getParentId")
fun testStaticArrayOperations() {
val method = getMethod("StaticArray", "pushTwice")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 100.0 }
{ r -> r.number == 5.0 },
)
}

@Test
fun testStaticInitializer() {
val method = getMethod("StaticInitializer", "getComputed")
fun testStaticNullInitialization() {
val method = getMethod("StaticNull", "initialize")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.number == 15.0 } // Sum of 1-5
{ r -> r.number == 5.0 },
)
}

@Test
fun testMultipleStatics() {
val method = getMethod("MultipleStatics", "getLogLength")
discoverProperties<TsValue.TsNumber>(
fun testStaticObjectOperations() {
val method = getMethod("StaticObject", "toggleAndGet")
discoverProperties<TsValue.TsClass>(
method = method,
// Initial state before any addEntry calls
{ r -> r.number == 0.0 }
{ r ->
(r.properties["enabled"] as TsValue.TsBoolean).value == true &&
(r.properties["count"] as TsValue.TsNumber).number == 1.0
},
{ r ->
(r.properties["enabled"] as TsValue.TsBoolean).value == false &&
(r.properties["count"] as TsValue.TsNumber).number == 2.0
},
)
}

@Test
fun testStaticObject() {
val method = getMethod("StaticObject", "checkEnabled")
discoverProperties<TsValue.TsBoolean>(
fun testStaticAccess() {
val method = getMethod("StaticAccess", "calculateSum")
discoverProperties<TsValue.TsNumber>(
method = method,
{ r -> r.value }
{ r -> r.number == 3.0 },
)
}

@Test
fun testStaticTypes() {
val method = getMethod("StaticTypes", "getTypeResults")
discoverProperties<TsValue.TsArray<*>>(
fun testStaticAccessSwap() {
val method = getMethod("StaticAccess", "swapAndGetValues")
discoverProperties<TsValue.TsArray<TsValue.TsNumber>>(
method = method,
{ r ->
(r.values[0] as TsValue.TsBoolean).value &&
(r.values[1] as TsValue.TsString).value == "Alice" &&
(r.values[2] as TsValue.TsNumber).number == 42.0
}
{ r -> r.values.map { it.number } == listOf(2.0, 1.0) },
)
}
}
127 changes: 65 additions & 62 deletions usvm-ts/src/test/resources/samples/StaticFields.ts
Original file line number Diff line number Diff line change
@@ -1,106 +1,109 @@
// @ts-nocheck
// noinspection JSUnusedGlobalSymbols

// Test: Basic static field access
class StaticBasic {
static value: number = 42;
// Test: Basic number static
class StaticNumber {
static value = 10;

getValue(): number {
return StaticBasic.value;
return StaticNumber.value;
}
}

// Test: Static field modification
// Test: Sequential static modifications with value persistence
class StaticModification {
static count: number = 0;
static count = 0;

incrementAndGet(): number {
incrementTwice(): number {
StaticModification.count++;
StaticModification.count++;
return StaticModification.count;
}
}

// Test: Inheritance with static fields
class ParentStatic {
static family: string = "Parent";
// Test: Inheritance shadowing
class StaticParent {
static id = 100;
}

class StaticChild extends StaticParent {
static id = 200;

getParentId(): number {
return StaticParent.id;
}

static getFamily(): string {
return ParentStatic.family;
getChildId(): number {
return StaticChild.id;
}
}

class ChildStatic extends ParentStatic {
static family: string = "Child";
// Test: Boolean static toggle
class StaticBoolean {
static flag = true;

static getChildFamily(): string {
return ChildStatic.family;
toggleAndGet(): boolean {
StaticBoolean.flag = !StaticBoolean.flag;
return StaticBoolean.flag;
}
}

// Test: Static field shadowing
class ShadowParent {
static id: number = 100;
// Test: Array static manipulation
class StaticArray {
static numbers = [1, 2, 3];

pushTwice(): number {
StaticArray.numbers.push(4);
StaticArray.numbers.push(5);
return StaticArray.numbers.length;
}
}

class ShadowChild extends ShadowParent {
static id: number = 200;
// Test: Null initialization and update
class StaticNull {
static value: number | null = null;

getParentId(): number {
return ShadowParent.id;
initialize(): number {
StaticNull.value = 5;
return StaticNull.value!;
}
}

// Test: Complex static initializer
class StaticInitializer {
static computed: number = (() => {
let sum = 0;
for (let i = 1; i <= 5; i++) sum += i;
return sum;
})();
// Test: Object static operations
class StaticObject {
static config: Config = {enabled: false, count: 0};

getComputed(): number {
return StaticInitializer.computed;
toggleAndGet(): Config {
StaticObject.config.flip()
StaticObject.config.increment();
return StaticObject.config;
}
}

// Test: Multiple static fields
class MultipleStatics {
static count: number = 0;
static readonly MAX: number = 100;
static log: string[] = [];
class Config {
enabled: boolean;
count: number;

static addEntry(entry: string): void {
MultipleStatics.log.push(entry);
flip(): void {
this.enabled = !this.enabled;
}

getLogLength(): number {
return MultipleStatics.log.length;
increment(): void {
this.count++;
}
}

// Test: Static object field
class StaticObject {
static config = {
enabled: true,
timeout: 3000
};
// Test: Field swapping
class StaticAccess {
static a = 1;
static b = 2;

checkEnabled(): boolean {
return StaticObject.config.enabled;
calculateSum(): number {
return StaticAccess.a + StaticAccess.b;
}
}

// Test: Static field type variations
class StaticTypes {
static flag: boolean = true;
static names: string[] = ["Alice", "Bob"];
static magicNumber: number = 42;

getTypeResults(): [boolean, string, number] {
return [
StaticTypes.flag,
StaticTypes.names[0],
StaticTypes.magicNumber
];
swapAndGetValues(): number[] {
[StaticAccess.a, StaticAccess.b] = [StaticAccess.b, StaticAccess.a];
return [StaticAccess.a, StaticAccess.b];
}
}

0 comments on commit e40180a

Please sign in to comment.