-
Notifications
You must be signed in to change notification settings - Fork 25
[TS] Add and refactor ops #322
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pull Request Overview
This PR adds new TypeScript operators and refactors existing operator implementations to improve test structure and maintainability. The changes primarily focus on expanding operator coverage, improving naming consistency, and restructuring test organization.
Key changes include:
- Addition of new operators: VoidOperator, UnaryPlus, NullishCoalescing, InOperator, DeleteOperator, and Bitwise operators
- Refactoring of existing operator tests to use more consistent naming patterns and utility functions
- Movement of Truthy and Strings classes from root samples to lang package
- Introduction of utility functions for test comparisons and DSL method building
Reviewed Changes
Copilot reviewed 82 out of 92 changed files in this pull request and generated 4 comments.
Show a summary per file
File | Description |
---|---|
VoidOperator.ts | New operator test covering void operator behavior |
UnaryPlus.ts | New operator test for unary plus conversion |
NullishCoalescing.ts | New operator test for nullish coalescing (??) |
InOperator.ts | New operator test for 'in' operator |
DeleteOperator.ts | New operator test for delete operator |
Bitwise.ts | New operator tests for bitwise operations |
Remainder.ts | Refactored remainder operator tests with cleaner structure |
Or.ts | Simplified logical OR operator tests |
Neg.ts | Enhanced negation operator tests with additional cases |
And.ts | Comprehensive refactor with manual DSL method building |
Equality.ts | Expanded equality tests with new comparison cases |
TypeOf.ts | Moved and renamed from Strings to proper location |
Less.ts | Minor formatting and utility function updates |
Util.kt | New utility functions for number comparisons |
TsMethodTestRunner.kt | Enhanced test runner with better method resolution |
Multiple test files | Consistent adoption of new utility functions and naming patterns |
Comments suppressed due to low confidence (1)
usvm-ts/src/test/kotlin/org/usvm/samples/operators/And.kt:144
- [nitpick] This TODO comment appears multiple times in the file. Consider either implementing the missing falsy value handling or creating a more specific issue reference to track this work.
ret(const(5))
let x = 42; | ||
let res = delete x; | ||
|
||
if (res === false && x === 42) return 1; // welcome to JavaScript |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
[nitpick] The comment '// welcome to JavaScript' is informal and doesn't explain the JavaScript-specific behavior. Consider a more descriptive comment like '// delete on local variables returns false in JavaScript'.
if (res === false && x === 42) return 1; // welcome to JavaScript | |
if (res === false && x === 42) return 1; // delete on local variables returns false in JavaScript |
Copilot uses AI. Check for mistakes.
infix fun Double.eq(other: Int): Boolean { | ||
return this eq other.toDouble() | ||
infix fun Double.eq(other: Double): Boolean { | ||
return (this - other).absoluteValue <= Double.MIN_VALUE |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Using Double.MIN_VALUE as epsilon for floating-point comparison is incorrect. Double.MIN_VALUE is the smallest positive nonzero value, which is extremely small (4.9e-324). This could cause precision issues. Consider using a more appropriate epsilon like 1e-9 or Double.MIN_VALUE * Math.pow(2, 52).
return (this - other).absoluteValue <= Double.MIN_VALUE | |
return (this - other).absoluteValue <= 1e-9 |
Copilot uses AI. Check for mistakes.
val rightBv = mkFpToBvExpr(fpRoundingModeSortDefaultValue(), rightNum.asExpr(fp64Sort), 32, true) | ||
|
||
// Mask the shift amount to 5 bits (0-31) | ||
val shiftAmount = mkBvAndExpr(rightBv, mkBv(0x1F, 32u)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why? What is it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Because you can't shift by larger amount in JavaScript. The RHS of any shift operation gets truncated to 5 least significant bits. For example, 1 << 4 == 16
and 1 << 36 == 32
, since in the number 36
only the 5 last bits are used, which correspond to 00100_2 = 4
.
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
Outdated
Show resolved
Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
Outdated
Show resolved
Hide resolved
@@ -779,8 +805,12 @@ class TsInterpreter( | |||
|
|||
val parameterType = param.type | |||
if (parameterType is EtsRefType) { | |||
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue())) | |||
state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This one is better to extract as an optional behaviour
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not relevant to this PR. I only moved these constraints from below because there is a premature return and in some cases these constraints were not declared. If not this bug, I would not even touch them.
In all existing tests, these constraints (non-nullness of ref-params) seems to be required, or rather, it is unclear what will break without them (I bet many things rely on this). So making this optional would require adding the infrastructure for options and also the tests that explicitly turn off this behaviour. All of this deviates from this PR (which is already big, and only "operations"-related), so it is better to make a separate one.
Rebased and fixed according to review comments. |
This PR adds new operators and refactor existing ones.