More fixes for real applications #283

CaelmBleidd · 2025-05-30T06:29:09Z

No description provided.

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

+                    val resolvedArgs = expr.args.map { resolve(it) ?: return null }
+
+                    val staticInstances = scope.calcOnState {
+                        resolutionResult.properties.take(1).map { getStaticInstance(it.enclosingClass!!) }


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

+
+                require(resolutionResult is EtsPropertyResolution.Unique)
+
+                val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) }


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

        }

+        // Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,


usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt

@@ -72,11 +75,27 @@
                    .filterNot { it.isStatic }
                    .filterNot { it.name.startsWith("%AM") }
                    .filterNot { it.name == "build" }
+                    .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
+                    .filterNot { it.name == STATIC_INIT_METHOD_NAME }


usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt

@@ -72,11 +75,27 @@
                    .filterNot { it.isStatic }
                    .filterNot { it.name.startsWith("%AM") }
                    .filterNot { it.name == "build" }
+                    .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
+                    .filterNot { it.name == STATIC_INIT_METHOD_NAME }
+                    .filterNot { it.name == CONSTRUCTOR_NAME }


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

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

+                options,
+                targets,
+                timeStatisticsFactory =
+                    { timeStatistics },


usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

+                timeStatisticsFactory =
+                    { timeStatistics },
+                stepsStatisticsFactory =
+                    { stepsStatistics },


usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

+                stepsStatisticsFactory =
+                    { stepsStatistics },
+                coverageStatisticsFactory =
+                    { coverageStatistics },


usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

+                coverageStatisticsFactory =
+                    { coverageStatistics },
+                getCollectedStatesCount =
+                    { statesCollector.collectedStates.size }


usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

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

github-advanced-security

detekt found more than 20 potential problems in the proposed changes. Check the Files changed tab for more details.

Copilot

Pull Request Overview

This PR delivers a set of targeted fixes and enhancements to support real-world applications by updating matcher logic, improving test runners, refining property resolution, enhancing interpreter/expression handling, and bumping dependencies.

Adjusted matcher to include zero results and updated descriptions.
Enhanced test runners with finite timeouts, exception aggregation, and filtering.
Refactored field/method resolution APIs and added support for new expression and type patterns.
Improved interpreter performance and error handling; updated stop strategy logging.
Bumped jacodb dependency and minor formatting tweaks.

Reviewed Changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt	Fix analysis‐results matcher to include zero
usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt	Added TODO for fork limit
usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt	Adjusted test runner imports and default timeouts
usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt	Refactored Photos project test with exception collection
usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt	Mirrored test runner refactor for DemoCalc project
usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt	Commented out an error log for missing class resolution
usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt	Generalized `EtsFieldResolutionResult` to `EtsPropertyResolution`
usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt	Cached ancestor lookups in subtype check
usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt	Removed stray blank line
usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt	Improved unknown‐stmt handling and limited forks
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt	Added support for new expr types and TODO stubs
usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt	Wrapped stop strategy to log when finished
usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt	Added support for enum and generic types
usvm-core/src/main/kotlin/org/usvm/StepScope.kt	Reformatted `check` invocation
buildSrc/src/main/kotlin/Dependencies.kt	Bumped `jacodb` version

Comments suppressed due to low confidence (2)

usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt:21

The description says "Allow any number of results except zero" but the matcher now allows zero. Please update the description to reflect the new behavior.

) { it >= 0 }

usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt:74

This test collects exceptions but never asserts on them, so failures will be silently logged. Consider adding an assertion (e.g., assertTrue(exceptions.isEmpty())) to fail the test when exceptions occur.

Copilot · 2025-06-20T10:15:39Z

usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt

            }
        }
+
+        val exc = exceptions.groupBy { it }


Grouping by exception instance (it) will rarely group multiple exceptions together since each throwable is a distinct object. Consider grouping by exception class or message (it::class or it.message) to aggregate similar errors.

Suggested change

val exc = exceptions.groupBy { it }

val exc = exceptions.groupBy { it::class }

Copilot · 2025-06-20T10:15:39Z

usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt

+        val exc = exceptions.groupBy { it }
+        println(
+            exc.values.sortedBy
+            { it.size }.asReversed().map
+            { it.first() })


Same grouping issue as in Photos.kt: grouping by the exception instance won't cluster similar errors. Use a meaningful key like exception class or message for grouping.

Suggested change

val exc = exceptions.groupBy { it }

println(

exc.values.sortedBy

{ it.size }.asReversed().map

{ it.first() })

val exc = exceptions.groupBy { it::class }

println(

exc.entries.sortedBy

{ it.value.size }.asReversed().map

{ "${it.key}: ${it.value.size} occurrences" })

Copilot · 2025-06-20T10:15:40Z

usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt

@@ -259,4 +259,5 @@ data class UMachineOptions(
     * Limit loop iterations.
     * */
    val loopIterationLimit: Int? = null,
+    // TODO fork limit


[nitpick] The TODO comment indicates an unimplemented feature. It may help to add context or link to an issue, or implement the fork limit feature now to avoid leaving untracked work.

Suggested change

// TODO fork limit

/**

* Limit the number of forks that can be created. If null, no limit is applied.

*/

val forkLimit: Int? = null,

CaelmBleidd changed the title ~~Caelmbleidd/fixes~~ More fixes for real applications May 30, 2025

github-advanced-security bot found potential problems May 30, 2025

View reviewed changes

CaelmBleidd force-pushed the caelmbleidd/fixes branch from 5ed9332 to eb8e80e Compare June 3, 2025 14:39

CaelmBleidd changed the base branch from main to caelmbleidd/input_arrays June 11, 2025 08:58

CaelmBleidd force-pushed the caelmbleidd/input_arrays branch from 87b841b to 4994227 Compare June 18, 2025 10:28

Base automatically changed from caelmbleidd/input_arrays to main June 18, 2025 10:48

CaelmBleidd force-pushed the caelmbleidd/fixes branch from d98fbfb to 558a624 Compare June 18, 2025 13:16

github-advanced-security bot found potential problems Jun 18, 2025

View reviewed changes

CaelmBleidd and others added 13 commits June 18, 2025 16:57

Hacks

89ed53e

More hacks

069cb78

Some more fixes

f85ef55

Tmp commit

51f5b9f

Input arrays support

545887c

Format

f6c17c4

Operators implementation

db952f6

Some hacks

911e8ca

Fix a class signature lookup

a07c653

Support simple casts

201e5f4

Clear logs

f8fd3fa

Add todo

59393c2

Rebase fix

0f18a8c

CaelmBleidd force-pushed the caelmbleidd/fixes branch from 558a624 to 0f18a8c Compare June 18, 2025 14:00

Tmp changes

bb4df1f

github-advanced-security bot found potential problems Jun 19, 2025

View reviewed changes

CaelmBleidd added 2 commits June 20, 2025 11:56

Some fixes

7b1bcd8

Fix mocker return value

c3e5fe0

CaelmBleidd requested a review from Copilot June 20, 2025 10:13

Copilot AI reviewed Jun 20, 2025

View reviewed changes


		require(resolutionResult is EtsPropertyResolution.Unique)

		val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) }

		}

		// Если мы записали что-то в объект в виде bool, а потом считали это из поля bool \| null, то здесь будет unresolvedSort,

	val exc = exceptions.groupBy { it }
	val exc = exceptions.groupBy { it::class }

-    // TODO fork limit
+    /**
+     * Limit the number of forks that can be created. If null, no limit is applied.
+     */
+    val forkLimit: Int? = null,

More fixes for real applications #283

Are you sure you want to change the base?

More fixes for real applications #283

Uh oh!

Conversation

CaelmBleidd commented May 30, 2025

Uh oh!

Check warning

Check warning

Check warning

Uh oh!

Check warning

Check warning

Uh oh!

Check warning

Check warning

Check warning

Check warning

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-advanced-security bot left a comment

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Copilot AI Jun 20, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jun 20, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Jun 20, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!