Skip to content

Input arrays support #285

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.

Sign up for GitHub

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

Jump to bottom
Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Input arrays support #285

wants to merge 3 commits into from

Conversation

CaelmBleidd
Copy link
Member

@CaelmBleidd CaelmBleidd commented Jun 3, 2025 •
edited
Loading

The following changes were made:

  1. New matchers for tests supporting executions number checker
  2. Support for arrays as parameters
  3. Register fake objects creation to support their restoration during model resolving
  4. Reading by negative indices and indices out of range are prohibited. We'll treat this operation as an error

github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 4, 2025
View reviewed changes
github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 5, 2025
View reviewed changes
usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
check(fakeObject.isFakeObject())

val fakeType = fakeObject.getFakeType(finalStateMemory)
return@map when {

Check warning

Code scanning / detekt

Braces do not comply with the specified policy Warning test

Inconsistent braces, make sure all branches either have or don't have braces.
github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 6, 2025
View reviewed changes
github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 6, 2025
View reviewed changes
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
invariants = invariants,
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(
typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class)

Check warning

Code scanning / detekt

Reports incorrect argument list wrapping Warning test

Argument should be on a separate line (unless all arguments can fit a single line)
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
invariants = invariants,
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(
typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class)

Check warning

Code scanning / detekt

Reports incorrect argument list wrapping Warning test

Argument should be on a separate line (unless all arguments can fit a single line)
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -139,6 +199,30 @@
)
}

protected inline fun <reified T1 : TsTestValue, reified T2 : TsTestValue, reified T3 : TsTestValue, reified R : TsTestValue> checkMatches(

Check warning

Code scanning / detekt

Reports lines with exceeded length Warning test

Exceeded max line length (120)
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -139,6 +199,30 @@
)
}

protected inline fun <reified T1 : TsTestValue, reified T2 : TsTestValue, reified T3 : TsTestValue, reified R : TsTestValue> checkMatches(

Check warning

Code scanning / detekt

Line detected, which is longer than the defined maximum line length in the code style. Warning test

Line detected, which is longer than the defined maximum line length in the code style.
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -163,6 +247,31 @@
)
}

protected inline fun <reified T1 : TsTestValue, reified T2 : TsTestValue, reified T3 : TsTestValue, reified T4 : TsTestValue, reified R : TsTestValue> checkMatches(

Check warning

Code scanning / detekt

Reports lines with exceeded length Warning test

Exceeded max line length (120)
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -163,6 +247,31 @@
)
}

protected inline fun <reified T1 : TsTestValue, reified T2 : TsTestValue, reified T3 : TsTestValue, reified T4 : TsTestValue, reified R : TsTestValue> checkMatches(

Check warning

Code scanning / detekt

Line detected, which is longer than the defined maximum line length in the code style. Warning test

Line detected, which is longer than the defined maximum line length in the code style.
usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt
@@ -20,6 +20,11 @@
matcherFailedMessage = { _ -> "No analysis results received" }
) { it > 0 }

val noResultsExpected = AnalysisResultsNumberMatcher(
description = "No executions expected",
matcherFailedMessage = { it -> "Expected no analysis results, but $it executions were found" }

Check warning

Code scanning / detekt

Declaring lambda parameters as `it` is redundant. Warning test

This explicit usage of it as the lambda parameter name can be omitted.
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/input_arrays branch from ac893b9 to 163e637 Compare June 6, 2025 14:12
@CaelmBleidd CaelmBleidd requested a review from Lipen June 6, 2025 14:12
@CaelmBleidd CaelmBleidd marked this pull request as ready for review June 6, 2025 14:12
github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 6, 2025
View reviewed changes
Lipen
Lipen reviewed Jun 6, 2025
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
)

// If we want to get length from a fake object, we assume that it is an array.
scope.assert(fakeType.refTypeExpr)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why assert and not pathConstraints += ...?

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -809,7 +901,12 @@ class TsExprResolver(
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
)

val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type
val arrayType = expr.type as EtsArrayType
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This cast might fail.

Lipen
Lipen approved these changes Jun 9, 2025
View reviewed changes
Copy link
Member

@Lipen Lipen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks solid 🪨

github-advanced-security[bot]
github-advanced-security bot found potential problems Jun 9, 2025
View reviewed changes
usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -76,6 +87,33 @@
return TsTest(method, before, after, result, trace = emptyList())
}

private fun prepareForResolve(state: TsState) {
state.lValuesToAllocatedFakeObjects.forEach { (lValue, fakeObject) ->
when (lValue) {

Check warning

Code scanning / detekt

Braces do not comply with the specified policy Warning test

Inconsistent braces, make sure all branches either have or don't have braces.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Lipen Lipen Lipen approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@CaelmBleidd @Lipen