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

TsTestResolver extended implementation #250

Merged
merged 12 commits into from
Feb 14, 2025
Merged

TsTestResolver extended implementation #250

Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
080b41c
Resolver draft
CaelmBleidd Feb 13, 2025
1ac46c8
Some fixes
CaelmBleidd Feb 13, 2025
94ee1ab
Fix tests
CaelmBleidd Feb 14, 2025
361ecc4
Remove redundant changes
CaelmBleidd Feb 14, 2025
d657361
Style fixes
CaelmBleidd Feb 14, 2025
fcaa059
Rename variable
CaelmBleidd Feb 14, 2025
44cf955
Rename TS to Ts, fix braces in when
Lipen Feb 14, 2025
d91e84a
Check via isFakeObject
Lipen Feb 14, 2025
12852c7
Add newline
Lipen Feb 14, 2025
d2ada6c
Remove unnecessary branch, use method.enclosingClass
Lipen Feb 14, 2025
e426c6f
Remove resolveUnknown
Lipen Feb 14, 2025
ca7b751
Format
Lipen Feb 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,26 @@
package org.usvm.api

import org.jacodb.ets.base.EtsStmt
import org.jacodb.ets.model.EtsClass
import org.jacodb.ets.model.EtsField
import org.jacodb.ets.model.EtsMethod

data class TsTest(
val parameters: List<TsObject>,
val method: EtsMethod,
val before: TsParametersState,
val after: TsParametersState,
val returnValue: TsObject,
val trace: List<EtsStmt>? = null,
)

data class TsParametersState(
val thisInstance: TsObject?,
val parameters: List<TsObject>,
val globals: Map<EtsClass, List<GlobalFieldValue>>,
)

data class GlobalFieldValue(val field: EtsField, val value: TsObject) // TODO is it right?????

open class TsMethodCoverage

object NoCoverage : TsMethodCoverage()
Expand Down
17 changes: 17 additions & 0 deletions usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,23 @@ class TsInterpreter(
)

val solver = ctx.solver<EtsType>()

val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics
val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)

state.pathConstraints += with(ctx) {
mkNot(
mkOr(
ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()),
ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue())
)
)
}

// TODO fix incorrect type streams
// val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, EtsClassType(method.enclosingClass))
// state.pathConstraints += thisTypeConstraint

val model = solver.check(state.pathConstraints).ensureSat().model
state.models = listOf(model)

Expand Down
2 changes: 1 addition & 1 deletion usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,4 +25,4 @@ class Null : TsMethodTestRunner() {
{ a, r -> a !is TsObject.TsNull && r.number == 2.0 },
)
}
}
}
227 changes: 0 additions & 227 deletions usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt
View file
Open in desktop

This file was deleted.

16 changes: 9 additions & 7 deletions ...otlin/org/usvm/util/TSMethodTestRunner.kt → ...otlin/org/usvm/util/TsMethodTestRunner.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
analysisResultsMatchers = analysisResultMatchers,
invariants = invariants,
extractValuesToCheck = { r -> r.parameters + r.returnValue },
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(typeTransformer(R::class)),
checkMode = CheckMode.MATCH_PROPERTIES,
coverageChecker = coverageChecker
Expand All @@ -72,7 +72,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
analysisResultsMatchers = analysisResultMatchers,
invariants = invariants,
extractValuesToCheck = { r -> r.parameters + r.returnValue },
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(typeTransformer(T::class), typeTransformer(R::class)),
checkMode = CheckMode.MATCH_PROPERTIES,
coverageChecker = coverageChecker
Expand All @@ -90,7 +90,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
analysisResultsMatchers = analysisResultMatchers,
invariants = invariants,
extractValuesToCheck = { r -> r.parameters + r.returnValue },
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(
typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class)
),
Expand All @@ -110,7 +110,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
analysisResultsMatchers = analysisResultMatchers,
invariants = invariants,
extractValuesToCheck = { r -> r.parameters + r.returnValue },
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(
typeTransformer(T1::class),
typeTransformer(T2::class),
Expand All @@ -133,7 +133,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
analysisResultsMatchers = analysisResultMatchers,
invariants = invariants,
extractValuesToCheck = { r -> r.parameters + r.returnValue },
extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
expectedTypesForExtractedValues = arrayOf(
typeTransformer(T1::class),
typeTransformer(T2::class),
Expand Down Expand Up @@ -173,6 +173,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT)
EtsClassType(signature)
}

TsObject.TsString::class -> EtsStringType
TsObject.TsNumber::class -> EtsNumberType
TsObject.TsNumber.Double::class -> EtsNumberType
Expand All @@ -188,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT)
EtsClassType(signature)
}

else -> error("Unsupported type: $klass")
}
}
Expand All @@ -196,8 +198,8 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
TsMachine(scene, options).use { machine ->
val states = machine.analyze(listOf(method))
states.map { state ->
val resolver = TsTestResolver(state)
resolver.resolve(method)
val resolver = TsTestResolver()
resolver.resolve(method, state)
}
}
}
Expand Down
Loading