Skip to content
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

Basic USVM TS type system with type coercion #215

Merged
merged 65 commits into from
Jan 29, 2025
Merged

Basic USVM TS type system with type coercion #215

merged 65 commits into from
Jan 29, 2025

Conversation

zishkaz
Copy link
Collaborator

@zishkaz zishkaz commented Sep 30, 2024

No description provided.

@zishkaz zishkaz requested a review from CaelmBleidd September 30, 2024 10:06
@zishkaz zishkaz self-assigned this Sep 30, 2024
@zishkaz zishkaz marked this pull request as draft September 30, 2024 11:40
github-advanced-security[bot]
github-advanced-security bot found potential problems Oct 2, 2024
View reviewed changes
Copy link

@github-advanced-security github-advanced-security bot left a comment

Choose a reason for hiding this comment

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

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

@zishkaz
Copy link
Collaborator Author

zishkaz commented Oct 3, 2024

This PR indirectly introduces a bug

@zishkaz zishkaz marked this pull request as ready for review October 3, 2024 08:24
CaelmBleidd
CaelmBleidd requested changes Oct 4, 2024
View reviewed changes
.github/workflows/build-and-run-tests.yml Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/StateForker.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/StateForker.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Outdated Show resolved Hide resolved
github-advanced-security[bot]
github-advanced-security bot found potential problems Oct 8, 2024
View reviewed changes
usvm-core/src/main/kotlin/org/usvm/Expressions.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSBinaryOperator.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSUnaryOperator.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/TSUnaryOperator.kt Fixed Show fixed Hide fixed
usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt Fixed Show fixed Hide fixed
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Fixed Show fixed Hide fixed
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Fixed Show fixed Hide fixed
@zishkaz zishkaz requested a review from CaelmBleidd October 9, 2024 11:24
CaelmBleidd
CaelmBleidd previously requested changes Oct 9, 2024
View reviewed changes
usvm-core/src/main/kotlin/org/usvm/Expressions.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt Outdated Show resolved Hide resolved
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Outdated Show resolved Hide resolved
github-advanced-security[bot]
github-advanced-security bot found potential problems Oct 17, 2024
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/TSExprTransformer.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt Fixed Show fixed Hide fixed
usvm-ts/src/main/kotlin/org/usvm/state/TSState.kt Fixed Show fixed Hide fixed
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt Outdated

private fun approximateParam(expr: UConcreteHeapRef, idx: Int, model: UModelBase<EtsType>): TSObject =
when (val tr = model.typeStreamOf(expr).take(1)) {
is TypesResult.SuccessfulTypesResult -> with (expr.tctx) {

Check warning

Code scanning / detekt

Reports spaces around parentheses

Unexpected spacing before "("
github-advanced-security[bot]
github-advanced-security bot found potential problems Dec 9, 2024
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/machine/TSTypeSystem.kt
}

val types = primitiveTypes.toMutableList()
return when (val remainingTypes = anyTypeStream.take(n - primitiveTypes.size)) {

Check warning

Code scanning / detekt

Braces do not comply with the specified policy Warning

Inconsistent braces, make sure all branches either have or don't have braces.
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprTransformer.kt Outdated
// (primitives can't be cast to ref in TypeScript type coercion)
addressSort -> {
val fpToBoolLink = mkEq(fpToBoolSort(asFp64()), asBool())
val boolToRefLink = mkEq(asBool(), (baseExpr as UExpr<UAddressSort>).neq(mkNullRef()))

Check warning

Code scanning / detekt

Reports multiple space usages

Unnecessary long whitespace
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExpressions.kt
@@ -0,0 +1,111 @@
package org.usvm.machine.expr

import io.ksmt.KAst

Check warning

Code scanning / detekt

Detects imports in non default order

Imports must be ordered in lexicographic order without any empty lines in-between with "java", "javax", "kotlin" and aliases in the end
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExpressions.kt Outdated
private fun coerce(
other: UExpr<out USort>,
action: CoerceAction,
): UExpr<out USort> = when (other) {

Check warning

Code scanning / detekt

Braces do not comply with the specified policy

Inconsistent braces, make sure all branches either have or don't have braces.
usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt
@@ -0,0 +1,151 @@
package org.usvm.machine.operator

import io.ksmt.utils.cast

Check warning

Code scanning / detekt

Detects imports in non default order

Imports must be ordered in lexicographic order without any empty lines in-between with "java", "javax", "kotlin" and aliases in the end
usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt
discoverProperties(
methodIdentifier: MethodDescriptor,
vararg analysisResultMatchers: (T1, T2, T3, T4, R?) -> Boolean,
protected inline fun <reified T1 : TSObject, reified T2 : TSObject, reified T3 : TSObject, reified T4 : TSObject, reified R : TSObject> discoverProperties(

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
discoverProperties(
methodIdentifier: MethodDescriptor,
vararg analysisResultMatchers: (T1, T2, T3, T4, R?) -> Boolean,
protected inline fun <reified T1 : TSObject, reified T2 : TSObject, reified T3 : TSObject, reified T4 : TSObject, reified R : TSObject> discoverProperties(

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
only KClass<TSObject> is available to match different objects.
However, this method is also used in parent TestRunner class
and passes here TSObject instances. So this check on current level is required.
*/

Check warning

Code scanning / detekt

Detect the alignment of the initial star in a block comment.

Initial star should align with start of block comment
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt
@@ -1,5 +1,6 @@
package org.usvm.util

import io.ksmt.utils.cast

Check warning

Code scanning / detekt

Detects imports in non default order

Imports must be ordered in lexicographic order without any empty lines in-between with "java", "javax", "kotlin" and aliases in the end
usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt
ctx: TSContext,
model: UModelBase<EtsType>,
): List<TSObject> = with(ctx) {
params.map { param ->

Check warning

Code scanning / detekt

Reports multiple space usages

Unnecessary long whitespace
@CaelmBleidd CaelmBleidd force-pushed the sergeyl/ts_typecoercion branch from 1eed307 to b58e886 Compare December 20, 2024 16:04
@CaelmBleidd CaelmBleidd changed the base branch from main to caelmbleidd/update_kotlin_version December 20, 2024 16:05
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/update_kotlin_version branch from 556fa95 to 703b36c Compare December 20, 2024 18:08
Base automatically changed from caelmbleidd/update_kotlin_version to main December 26, 2024 18:17
@CaelmBleidd CaelmBleidd requested review from Lipen and Saloed January 24, 2025 13:39
Lipen
Lipen approved these changes Jan 27, 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.

Very good!

@Lipen Lipen requested a review from CaelmBleidd January 27, 2025 17:18
Saloed
Saloed requested changes Jan 28, 2025
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/machine/TSContext.kt Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/TSContext.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/TSContext.kt Outdated Show resolved Hide resolved
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 Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TSExprResolver.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/operator/TSBinaryOperator.kt Outdated Show resolved Hide resolved
usvm-ts/src/main/kotlin/org/usvm/machine/state/TSState.kt Outdated Show resolved Hide resolved
@CaelmBleidd CaelmBleidd requested a review from Saloed January 28, 2025 13:10
@Lipen Lipen merged commit 3b6a01d into main Jan 29, 2025
6 checks passed
@Lipen Lipen deleted the sergeyl/ts_typecoercion branch January 29, 2025 14:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CaelmBleidd CaelmBleidd CaelmBleidd left review comments

@Lipen Lipen Lipen approved these changes

@Saloed Saloed Saloed approved these changes

Assignees

@zishkaz zishkaz

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@zishkaz @Lipen @Saloed @CaelmBleidd