From 2ac8cbd336678b0e8891807957049923ea9da97a Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 15:35:52 +0300 Subject: [PATCH 1/6] Switch to a new ETS model --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- usvm-ts-dataflow/build.gradle.kts | 1 + .../usvm/dataflow/ts/graph/BackwardGraph.kt | 2 +- .../dataflow/ts/graph/EtsApplicationGraph.kt | 33 +- .../org/usvm/dataflow/ts/infer/AccessPath.kt | 22 +- .../org/usvm/dataflow/ts/infer/Alias.kt | 42 +-- .../usvm/dataflow/ts/infer/AnalyzerEvent.kt | 2 +- .../dataflow/ts/infer/ApplicationGraph.kt | 31 +- .../dataflow/ts/infer/BackwardAnalyzer.kt | 5 +- .../ts/infer/BackwardFlowFunctions.kt | 66 ++-- .../org/usvm/dataflow/ts/infer/EtsTypeFact.kt | 35 +- .../usvm/dataflow/ts/infer/ForwardAnalyzer.kt | 6 +- .../dataflow/ts/infer/ForwardFlowFunctions.kt | 73 ++-- .../org/usvm/dataflow/ts/infer/KnownType.kt | 26 ++ .../usvm/dataflow/ts/infer/LiveVariables.kt | 40 +-- .../dataflow/ts/infer/TypeFactProcessor.kt | 6 +- .../org/usvm/dataflow/ts/infer/TypeGuesser.kt | 2 +- .../dataflow/ts/infer/TypeInferenceManager.kt | 34 +- .../ts/infer/annotation/EtsSceneAnnotator.kt | 30 +- .../ts/infer/annotation/ExprTypeAnnotator.kt | 134 +++---- .../ts/infer/annotation/StmtTypeAnnotator.kt | 43 +-- .../ts/infer/annotation/TypeScheme.kt | 2 +- .../ts/infer/annotation/TypeSchemes.kt | 4 +- .../ts/infer/annotation/ValueTypeAnnotator.kt | 33 +- .../org/usvm/dataflow/ts/infer/cli/Dump.kt | 4 +- .../dataflow/ts/infer/dto/EtsTypeToDto.kt | 97 ++--- .../dataflow/ts/infer/dto/EtsValueToDto.kt | 33 +- .../ts/infer/verify/VerificationResult.kt | 2 +- .../collectors/ClassSummaryCollector.kt | 8 +- .../verify/collectors/StmtSummaryCollector.kt | 74 ++-- .../verify/collectors/SummaryCollector.kt | 36 +- .../ts/infer/verify/collectors/Utils.kt | 12 +- .../org/usvm/dataflow/ts/util/EtsTraits.kt | 57 +-- .../org/usvm/dataflow/ts/util/RealLocals.kt | 4 +- .../usvm/dataflow/ts/util/ToStringLimited.kt | 13 +- .../kotlin/org/usvm/dataflow/ts/util/Utils.kt | 8 +- .../ts/test/EtsProjectAnalysisTest.kt | 2 +- .../org/usvm/dataflow/ts/test/EtsSceneTest.kt | 73 ++-- .../dataflow/ts/test/EtsTypeAnnotationTest.kt | 193 ---------- .../dataflow/ts/test/EtsTypeInferenceTest.kt | 31 +- .../ts/test/EtsTypeResolverWithAstTest.kt | 2 +- .../dataflow/ts/test/utils/AbcProjects.kt | 6 +- .../ts/test/utils/ClassMatcherStatistics.kt | 24 +- .../ts/test/utils/ExpectedTypesExtractor.kt | 2 +- .../ts/test/utils/TypeInferenceStatistics.kt | 51 +-- .../org/usvm/dataflow/ts/test/utils/Utils.kt | 4 +- .../src/main/kotlin/org/usvm/api/TsTest.kt | 2 +- .../kotlin/org/usvm/api/targets/TsTarget.kt | 2 +- .../org/usvm/machine/TsApplicationGraph.kt | 2 +- .../kotlin/org/usvm/machine/TsComponents.kt | 2 +- .../main/kotlin/org/usvm/machine/TsContext.kt | 19 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 2 +- .../kotlin/org/usvm/machine/TsTransformer.kt | 2 +- .../kotlin/org/usvm/machine/TsTypeSystem.kt | 12 +- .../org/usvm/machine/expr/TsExprResolver.kt | 215 ++++++----- .../usvm/machine/interpreter/TsInterpreter.kt | 48 +-- .../org/usvm/machine/interpreter/TsStatic.kt | 9 +- .../org/usvm/machine/state/TsMethodResult.kt | 2 +- .../kotlin/org/usvm/machine/state/TsState.kt | 11 +- .../org/usvm/machine/state/TsStateUtils.kt | 2 +- .../kotlin/org/usvm/machine/types/FakeType.kt | 2 +- .../kotlin/org/usvm/util/EtsFieldResolver.kt | 10 +- .../main/kotlin/org/usvm/util/LValueUtil.kt | 2 +- .../src/main/kotlin/org/usvm/util/Utils.kt | 4 +- .../src/test/kotlin/org/usvm/samples/And.kt | 337 +++++------------- .../test/kotlin/org/usvm/samples/Arrays.kt | 2 + .../src/test/kotlin/org/usvm/samples/Call.kt | 4 +- .../src/test/kotlin/org/usvm/samples/Or.kt | 18 +- .../kotlin/org/usvm/samples/StaticFields.kt | 11 +- .../test/kotlin/org/usvm/util/ObjectClass.kt | 18 +- .../org/usvm/util/TsMethodTestRunner.kt | 24 +- .../kotlin/org/usvm/util/TsTestResolver.kt | 36 +- usvm-ts/src/test/resources/samples/Call.ts | 2 +- .../src/test/resources/samples/FieldAccess.ts | 2 +- .../test/resources/samples/StaticFields.ts | 18 +- 75 files changed, 934 insertions(+), 1296 deletions(-) create mode 100644 usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/KnownType.kt delete mode 100644 usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeAnnotationTest.kt diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 3afcde4e73..69ef670c9d 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "6ec737ce76" + const val jacodb = "3b6a17f000" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" diff --git a/usvm-ts-dataflow/build.gradle.kts b/usvm-ts-dataflow/build.gradle.kts index 2da676a1e1..fb819699d4 100644 --- a/usvm-ts-dataflow/build.gradle.kts +++ b/usvm-ts-dataflow/build.gradle.kts @@ -16,6 +16,7 @@ dependencies { api(Libs.jacodb_api_common) api(Libs.jacodb_ets) + implementation(Libs.jacodb_core) implementation(Libs.jacodb_taint_configuration) implementation(Libs.kotlinx_collections) implementation(Libs.kotlinx_serialization_json) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt index 47b2c9eccb..433d67b539 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/BackwardGraph.kt @@ -16,9 +16,9 @@ package org.usvm.dataflow.ts.graph -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt private class BackwardEtsApplicationGraphImpl( val forward: EtsApplicationGraph, diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt index 8da3b9bf20..49e37a1d65 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt @@ -17,19 +17,20 @@ package org.usvm.dataflow.ts.graph import mu.KotlinLogging -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.UNKNOWN_FILE_NAME +import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.Maybe +import org.jacodb.ets.utils.UNKNOWN_FILE_NAME import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.onSome import org.usvm.dataflow.graph.ApplicationGraph @@ -136,10 +137,10 @@ class EtsApplicationGraphImpl( override fun callees(node: EtsStmt): Sequence { val expr = node.callExpr ?: return emptySequence() - val callee = expr.method + val callee = expr.callee // Note: the resolving code below expects that at least the current method signature is known. - check(node.method.enclosingClass.isIdeal()) { + check(node.method.signature.enclosingClass.isIdeal()) { "Incomplete signature in method: ${node.method}" } @@ -154,7 +155,7 @@ class EtsApplicationGraphImpl( } if (prevStmt is EtsAssignStmt && prevStmt.rhv is EtsNewExpr) { - val cls = prevStmt.rhv.type + val cls = (prevStmt.rhv as EtsNewExpr).type if (cls !is EtsClassType) { return emptySequence() } @@ -223,7 +224,7 @@ class EtsApplicationGraphImpl( // If the callee signature is not ideal, resolve it via a partial match... check(!callee.enclosingClass.isIdeal()) - val cls = lookupClassWithIdealSignature(node.method.enclosingClass).let { + val cls = lookupClassWithIdealSignature(node.method.signature.enclosingClass).let { if (it.isNone) { error("Could not find the enclosing class: ${node.method.enclosingClass}") } @@ -250,10 +251,18 @@ class EtsApplicationGraphImpl( // try to *uniquely* resolve the callee via a partial signature match: val resolved = projectMethodsByName[callee.name].orEmpty() .asSequence() - .filter { compareClassSignatures(it.enclosingClass, callee.enclosingClass) != ComparisonResult.NotEqual } + .filter { + compareClassSignatures( + it.signature.enclosingClass, + callee.enclosingClass + ) != ComparisonResult.NotEqual + } // Note: exclude current class: .filterNot { - compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual + compareClassSignatures( + it.signature.enclosingClass, + node.method.signature.enclosingClass + ) != ComparisonResult.NotEqual } .toList() if (resolved.isEmpty()) { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt index e188307ec7..1e59448726 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AccessPath.kt @@ -1,17 +1,17 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAwaitExpr -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsConstant -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAwaitExpr +import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsConstant +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsValue data class AccessPath(val base: AccessPathBase, val accesses: List) { operator fun plus(accessor: Accessor) = AccessPath(base, accesses + accessor) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt index def121b407..a79f278fff 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt @@ -1,27 +1,27 @@ package org.usvm.dataflow.ts.infer import mu.KotlinLogging -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBinaryExpr -import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsConstant -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsInstanceOfExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNewArrayExpr -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsUnaryExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsConstant +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsUnaryExpr import org.usvm.dataflow.ts.infer.MethodAliasInfoImpl.Allocation private val logger = KotlinLogging.logger {} @@ -425,7 +425,7 @@ class MethodAliasInfoImpl( is EtsInstanceCallExpr -> { initEntity(entity.instance) - newString(entity.method.name) + newString(entity.callee.name) entity.args.forEach { initEntity(it) } } } @@ -516,7 +516,7 @@ class MethodAliasInfoImpl( } } - val root = method.cfg.stmts[0] + val root = method.cfg.stmts.first() postOrderDfs(root) order.reverse() diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt index c44ebbb026..33d3a6471f 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/AnalyzerEvent.kt @@ -1,7 +1,7 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt import org.usvm.dataflow.ifds.Vertex sealed interface AnalyzerEvent diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt index 4493764869..46308f1615 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ApplicationGraph.kt @@ -16,11 +16,11 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsInstLocation -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStmtLocation import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl @@ -41,8 +41,8 @@ class EtsApplicationGraphWithExplicitEntryPoint( override fun exitPoints(method: EtsMethod): Sequence = graph.exitPoints(method) - private fun methodEntryPoint(method: EtsMethod) = - EtsNopStmt(EtsInstLocation(method, index = -1)) + private fun methodEntryPoint(method: EtsMethod): EtsStmt = + EtsNopStmt(EtsStmtLocation(method, index = -1)) override fun entryPoints(method: EtsMethod): Sequence = sequenceOf(methodEntryPoint(method)) @@ -51,28 +51,21 @@ class EtsApplicationGraphWithExplicitEntryPoint( override fun callees(node: EtsStmt): Sequence = graph.callees(node) override fun successors(node: EtsStmt): Sequence { - val method = methodOf(node) - val methodEntry = methodEntryPoint(method) - - if (node == methodEntry) { - return graph.entryPoints(method) + if (node.location.index == -1) { + require(node is EtsNopStmt) + return graph.entryPoints(node.method) } - return graph.successors(node) } override fun predecessors(node: EtsStmt): Sequence { - val method = methodOf(node) - val methodEntry = methodEntryPoint(method) - - if (node == methodEntry) { + if (node.location.index == -1) { + require(node is EtsNopStmt) return emptySequence() } - - if (node in graph.entryPoints(method)) { - return sequenceOf(methodEntry) + if (node.location.index == 0) { + return entryPoints(node.method) } - return graph.predecessors(node) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt index 46b272cddd..f816ae35c5 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardAnalyzer.kt @@ -1,10 +1,9 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType import org.jacodb.impl.cfg.graphs.GraphDominators -import org.usvm.dataflow.graph.ApplicationGraph import org.usvm.dataflow.ifds.Analyzer import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Vertex diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt index 8b87350158..b2f331a8ae 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/BackwardFlowFunctions.kt @@ -1,28 +1,27 @@ package org.usvm.dataflow.ts.infer import mu.KotlinLogging -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsEqExpr -import org.jacodb.ets.base.EtsFieldRef -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsInExpr -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsLValue -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsEqExpr +import org.jacodb.ets.model.EtsFieldRef +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.callExpr import org.jacodb.impl.cfg.graphs.GraphDominators import org.usvm.dataflow.ifds.FlowFunction @@ -212,7 +211,8 @@ class BackwardFlowFunctions( if (returnValue != null) { val variable = returnValue.toBase() val type = if (doAddKnownTypes) { - EtsTypeFact.from(returnValue.type).fixAnyToUnknown() + val knownType = returnValue.tryGetKnownType(current.method) + EtsTypeFact.from(knownType).fixAnyToUnknown() } else { EtsTypeFact.UnknownEtsTypeFact } @@ -241,14 +241,8 @@ class BackwardFlowFunctions( // Case `x... := y` // ∅ |= y:unknown val type = if (doAddKnownTypes) { - EtsTypeFact.from(current.rhv.type).let { - // Note: convert Any to Unknown, because intersection with Any is Any - if (it is EtsTypeFact.AnyEtsTypeFact) { - EtsTypeFact.UnknownEtsTypeFact - } else { - it - } - } + val knownType = current.rhv.tryGetKnownType(current.method) + EtsTypeFact.from(knownType).fixAnyToUnknown() } else { EtsTypeFact.UnknownEtsTypeFact } @@ -283,13 +277,7 @@ class BackwardFlowFunctions( } } - val lhv = when (val l = current.lhv) { - is EtsLValue -> l.toPath() - else -> { - logger.info { "TODO backward assign zero: $current" } - error("Unexpected LHV in assignment: $current") - } - } + val lhv = current.lhv.toPath() // Handle new possible facts for LHS: if (lhv.accesses.isNotEmpty()) { @@ -543,7 +531,7 @@ class BackwardFlowFunctions( val objectWithMethod = EtsTypeFact.ObjectEtsTypeFact( cls = null, properties = mapOf( - callExpr.method.name to EtsTypeFact.FunctionEtsTypeFact + callExpr.callee.name to EtsTypeFact.FunctionEtsTypeFact ) ) result += TypedVariable(path, objectWithMethod) @@ -552,7 +540,7 @@ class BackwardFlowFunctions( if (doAddKnownTypes) { // f(x:T) |= x:T, where T is the type of the argument in f's signature for ((index, arg) in callExpr.args.withIndex()) { - val param = callExpr.method.parameters.getOrNull(index) ?: continue + val param = callExpr.callee.parameters.getOrNull(index) ?: continue val base = arg.toBase() val type = EtsTypeFact.from(param.type) result += TypedVariable(base, type) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt index 105c0c52de..2951f9905a 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/EtsTypeFact.kt @@ -1,23 +1,22 @@ package org.usvm.dataflow.ts.infer import mu.KotlinLogging -import org.jacodb.ets.base.ANONYMOUS_CLASS_PREFIX -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsFunctionType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnionType -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.base.INSTANCE_INIT_METHOD_NAME -import org.usvm.dataflow.ts.util.sortedBy +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.usvm.dataflow.ts.util.toStringLimited private val logger = KotlinLogging.logger {} @@ -86,7 +85,7 @@ sealed interface EtsTypeFact { cls: EtsType?, properties: Map, ): ObjectEtsTypeFact { - if (cls is EtsUnclearRefType && cls.name == "Object") { + if (cls is EtsUnclearRefType && cls.typeName == "Object") { return ObjectEtsTypeFact(null, properties) } return ObjectEtsTypeFact(cls, properties) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt index 8413b5da2b..18aa7f6da8 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardAnalyzer.kt @@ -1,9 +1,9 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ifds.Analyzer import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Vertex diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt index d42dc4bf4f..322d37f046 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/ForwardFlowFunctions.kt @@ -1,35 +1,36 @@ package org.usvm.dataflow.ts.infer import mu.KotlinLogging -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArithmeticExpr -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsAwaitExpr -import org.jacodb.ets.base.EtsBooleanConstant -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsFieldRef -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNegExpr -import org.jacodb.ets.base.EtsNewArrayExpr -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsNotExpr -import org.jacodb.ets.base.EtsNullConstant -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsRelationExpr -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedConstant -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArithmeticExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsAwaitExpr +import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFieldRef +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNegExpr +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNotExpr +import org.jacodb.ets.model.EtsNullConstant +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsRelationExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedConstant +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.getLocals import org.usvm.dataflow.ifds.FlowFunction import org.usvm.dataflow.ifds.FlowFunctions import org.usvm.dataflow.ts.graph.EtsApplicationGraph @@ -80,7 +81,7 @@ class ForwardFlowFunctions( val result = mutableListOf(Zero) if (doAddKnownTypes) { - val fakeLocals = method.locals.toSet() - method.getRealLocals() + val fakeLocals = method.getLocals() - method.getRealLocals() for ((base, type) in initialTypes) { if (base is AccessPathBase.Local) { @@ -265,6 +266,10 @@ class ForwardFlowFunctions( } } + is EtsArrayAccess -> { + // TODO + } + is EtsArithmeticExpr -> { result += TypedVariable(lhv, EtsTypeFact.NumberEtsTypeFact) result += TypedVariable(lhv, EtsTypeFact.StringEtsTypeFact) @@ -480,8 +485,8 @@ class ForwardFlowFunctions( val result = mutableListOf(fact) // skip duplicate fields // if (fact.variable.accesses.firstOrNull() != a) { - val path1 = lhv + fact.variable.accesses - result += TypedVariable(path1, fact.type) + val path1 = lhv + fact.variable.accesses + result += TypedVariable(path1, fact.type) // } val aliases = preAliases.getAliases(x).filter { @@ -494,9 +499,9 @@ class ForwardFlowFunctions( for (z in aliases) { // skip duplicate fields // if (z.accesses.firstOrNull() != a) { - // TODO: what about z.accesses.last == a ? - val path2 = z + a + fact.variable.accesses - result += TypedVariable(path2, fact.type) + // TODO: what about z.accesses.last == a ? + val path2 = z + a + fact.variable.accesses + result += TypedVariable(path2, fact.type) // } } return result @@ -547,7 +552,7 @@ class ForwardFlowFunctions( // `x := f()` if (callStatement is EtsAssignStmt) { val left = callStatement.lhv.toPath() - val type = EtsTypeFact.from(callExpr.method.returnType.unwrapPromise()) + val type = EtsTypeFact.from(callExpr.callee.returnType.unwrapPromise()) addTypes(left, type, result) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/KnownType.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/KnownType.kt new file mode 100644 index 0000000000..17a8437b72 --- /dev/null +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/KnownType.kt @@ -0,0 +1,26 @@ +package org.usvm.dataflow.ts.infer + +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.dataflow.ts.util.type + +fun EtsEntity.tryGetKnownType(method: EtsMethod): EtsType { + if (this is EtsLocal) { + return type + } + + if (this is EtsParameterRef) { + return method.parameters[index].type + } + + if (this is EtsThis) { + method.enclosingClass?.type?.let { return it } + } + + return EtsUnknownType +} diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt index 6420c0ca60..2b9a715a65 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/LiveVariables.kt @@ -1,25 +1,23 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBinaryExpr -import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsInstanceOfExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsTernaryExpr -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.base.EtsUnaryExpr -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsUnaryExpr +import org.jacodb.ets.model.EtsValue import java.util.BitSet interface LiveVariables { @@ -48,7 +46,6 @@ class LiveVariablesImpl( is EtsCallExpr -> this.used() is EtsCastExpr -> arg.used() is EtsInstanceOfExpr -> arg.used() - is EtsTernaryExpr -> condition.used() + thenExpr.used() + elseExpr.used() else -> emptyList() } @@ -98,8 +95,7 @@ class LiveVariablesImpl( is EtsCallStmt -> stmt.expr.used() is EtsReturnStmt -> stmt.returnValue?.used().orEmpty() is EtsIfStmt -> stmt.condition.used() - is EtsSwitchStmt -> stmt.arg.used() - is EtsThrowStmt -> stmt.arg.used() + is EtsThrowStmt -> stmt.exception.used() else -> emptyList() } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt index 7ad9e6b5f7..12af9a763b 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeFactProcessor.kt @@ -17,10 +17,10 @@ package org.usvm.dataflow.ts.infer import mu.KotlinLogging -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ts.infer.EtsTypeFact.AnyEtsTypeFact import org.usvm.dataflow.ts.infer.EtsTypeFact.ArrayEtsTypeFact import org.usvm.dataflow.ts.infer.EtsTypeFact.BooleanEtsTypeFact diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt index 2593977f53..ae0dbd9024 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeGuesser.kt @@ -16,8 +16,8 @@ package org.usvm.dataflow.ts.infer -import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsScene class TypeGuesser( diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt index a7bcb78dff..d746b2525e 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt @@ -12,17 +12,18 @@ import kotlinx.coroutines.newSingleThreadContext import kotlinx.coroutines.runBlocking import kotlinx.coroutines.withTimeout import mu.KotlinLogging -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.INSTANCE_INIT_METHOD_NAME -import org.jacodb.ets.graph.findDominators import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.impl.cfg.graphs.GraphDominators +import org.jacodb.impl.cfg.graphs.findDominators import org.usvm.dataflow.ifds.ControlEvent import org.usvm.dataflow.ifds.Edge import org.usvm.dataflow.ifds.Manager @@ -344,11 +345,20 @@ class TypeInferenceManager( private fun getInferredCombinedThisTypes( methodTypeScheme: Map>, ): Map { + val classBySignature = graph.cp.projectAndSdkClasses + .groupByTo(hashMapOf()) { it.signature } + + val allClasses = methodTypeScheme.keys + .map { it.signature.enclosingClass } + .distinct() + .map { sig -> classBySignature[sig].orEmpty().first() } + .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) } + val forwardSummariesByClass = forwardSummaries - .entries.groupByTo(hashMapOf()) { (method, _) -> method.enclosingClass } + .entries.groupByTo(hashMapOf()) { (method, _) -> method.signature.enclosingClass } - return graph.cp.projectClasses.mapNotNull { cls -> - val combinedBackwardType = (cls.methods + cls.ctor) + return allClasses.mapNotNull { cls -> + val combinedBackwardType = cls.methods .mapNotNull { methodTypeScheme[it] } .mapNotNull { facts -> facts[AccessPathBase.This] }.reduceOrNull { acc, type -> typeProcessor.intersect(acc, type) ?: run { @@ -643,7 +653,7 @@ class TypeInferenceManager( // intersect(this:object, type:string) if (cls == EtsStringType) return type - if (cls is EtsUnclearRefType && cls.name == "String") return type + if (cls is EtsUnclearRefType && cls.typeName == "String") return type if (cls != null) return null val intersectionProperties = properties diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/EtsSceneAnnotator.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/EtsSceneAnnotator.kt index fbd1323da0..5252c4c9e8 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/EtsSceneAnnotator.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/EtsSceneAnnotator.kt @@ -18,23 +18,20 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsGotoStmt -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsRawStmt -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.graph.EtsCfg +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsRawStmt +import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt fun EtsScene.annotateWithTypes(scheme: TypeScheme): EtsScene = EtsSceneAnnotator(this, scheme).annotate() @@ -65,7 +62,6 @@ class EtsSceneAnnotator( signature = signature, fields = fields, methods = methods.map { it.annotateWithTypes() }, - ctor = ctor.annotateWithTypes(), superClass = superClass, // TODO: replace with inferred superclass typeParameters = typeParameters, modifiers = modifiers, @@ -77,7 +73,6 @@ class EtsSceneAnnotator( return EtsMethodImpl( signature = signature, typeParameters = typeParameters, - locals = locals, modifiers = modifiers, decorators = decorators, ).also { method -> @@ -92,7 +87,8 @@ class EtsSceneAnnotator( val newStmt = relocated[stmt] ?: error("Unprocessed stmt") newStmt to cfg.successors(stmt).map { relocated[it] ?: error("Unprocessed stmt") }.toList() } - method._cfg = EtsCfg(relocated.values.toList(), successorMap.toMap()) + // TODO: method._cfg = EtsCfg(relocated.values.toList(), successorMap.toMap()) + TODO() } } @@ -112,15 +108,9 @@ class EtsSceneAnnotator( override fun visit(stmt: EtsThrowStmt): EtsStmt = stmt.copy(location = stmt.location.copy(method = to)) - override fun visit(stmt: EtsGotoStmt): EtsStmt = - EtsGotoStmt(location = stmt.location.copy(method = to)) - override fun visit(stmt: EtsIfStmt): EtsStmt = stmt.copy(location = stmt.location.copy(method = to)) - override fun visit(stmt: EtsSwitchStmt): EtsStmt = - stmt.copy(location = stmt.location.copy(method = to)) - override fun visit(stmt: EtsRawStmt): EtsStmt = stmt.copy(location = stmt.location.copy(method = to)) } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt index cd0456d6d0..671630302d 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt @@ -16,59 +16,56 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsAddExpr -import org.jacodb.ets.base.EtsAndExpr -import org.jacodb.ets.base.EtsAwaitExpr -import org.jacodb.ets.base.EtsBitAndExpr -import org.jacodb.ets.base.EtsBitNotExpr -import org.jacodb.ets.base.EtsBitOrExpr -import org.jacodb.ets.base.EtsBitXorExpr -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsCommaExpr -import org.jacodb.ets.base.EtsDeleteExpr -import org.jacodb.ets.base.EtsDivExpr -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsEqExpr -import org.jacodb.ets.base.EtsExpExpr -import org.jacodb.ets.base.EtsExpr -import org.jacodb.ets.base.EtsGtEqExpr -import org.jacodb.ets.base.EtsGtExpr -import org.jacodb.ets.base.EtsInExpr -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsInstanceOfExpr -import org.jacodb.ets.base.EtsLeftShiftExpr -import org.jacodb.ets.base.EtsLengthExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsLtEqExpr -import org.jacodb.ets.base.EtsLtExpr -import org.jacodb.ets.base.EtsMulExpr -import org.jacodb.ets.base.EtsNegExpr -import org.jacodb.ets.base.EtsNewArrayExpr -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsNotEqExpr -import org.jacodb.ets.base.EtsNotExpr -import org.jacodb.ets.base.EtsNullishCoalescingExpr -import org.jacodb.ets.base.EtsOrExpr -import org.jacodb.ets.base.EtsPostDecExpr -import org.jacodb.ets.base.EtsPostIncExpr -import org.jacodb.ets.base.EtsPreDecExpr -import org.jacodb.ets.base.EtsPreIncExpr -import org.jacodb.ets.base.EtsPtrCallExpr -import org.jacodb.ets.base.EtsRemExpr -import org.jacodb.ets.base.EtsRightShiftExpr -import org.jacodb.ets.base.EtsStaticCallExpr -import org.jacodb.ets.base.EtsStrictEqExpr -import org.jacodb.ets.base.EtsStrictNotEqExpr -import org.jacodb.ets.base.EtsSubExpr -import org.jacodb.ets.base.EtsTernaryExpr -import org.jacodb.ets.base.EtsTypeOfExpr -import org.jacodb.ets.base.EtsUnaryPlusExpr -import org.jacodb.ets.base.EtsUnsignedRightShiftExpr -import org.jacodb.ets.base.EtsValue -import org.jacodb.ets.base.EtsVoidExpr -import org.jacodb.ets.base.EtsYieldExpr +import org.jacodb.ets.model.EtsAddExpr +import org.jacodb.ets.model.EtsAndExpr +import org.jacodb.ets.model.EtsAwaitExpr +import org.jacodb.ets.model.EtsBitAndExpr +import org.jacodb.ets.model.EtsBitNotExpr +import org.jacodb.ets.model.EtsBitOrExpr +import org.jacodb.ets.model.EtsBitXorExpr +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsDeleteExpr +import org.jacodb.ets.model.EtsDivExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsEqExpr +import org.jacodb.ets.model.EtsExpExpr +import org.jacodb.ets.model.EtsExpr +import org.jacodb.ets.model.EtsGtEqExpr +import org.jacodb.ets.model.EtsGtExpr +import org.jacodb.ets.model.EtsInExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLeftShiftExpr +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsLtEqExpr +import org.jacodb.ets.model.EtsLtExpr +import org.jacodb.ets.model.EtsMulExpr +import org.jacodb.ets.model.EtsNegExpr +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNotEqExpr +import org.jacodb.ets.model.EtsNotExpr +import org.jacodb.ets.model.EtsNullishCoalescingExpr +import org.jacodb.ets.model.EtsOrExpr +import org.jacodb.ets.model.EtsPostDecExpr +import org.jacodb.ets.model.EtsPostIncExpr +import org.jacodb.ets.model.EtsPreDecExpr +import org.jacodb.ets.model.EtsPreIncExpr +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRemExpr +import org.jacodb.ets.model.EtsRightShiftExpr import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsStrictEqExpr +import org.jacodb.ets.model.EtsStrictNotEqExpr +import org.jacodb.ets.model.EtsSubExpr +import org.jacodb.ets.model.EtsTypeOfExpr +import org.jacodb.ets.model.EtsUnaryPlusExpr +import org.jacodb.ets.model.EtsUnsignedRightShiftExpr +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.model.EtsVoidExpr +import org.jacodb.ets.model.EtsYieldExpr class ExprTypeAnnotator( private val scene: EtsScene, @@ -89,8 +86,6 @@ class ExprTypeAnnotator( override fun visit(expr: EtsNewArrayExpr) = expr - override fun visit(expr: EtsLengthExpr) = expr - override fun visit(expr: EtsCastExpr) = expr.copy( arg = annotate(expr.arg) ) @@ -272,41 +267,30 @@ class ExprTypeAnnotator( ) override fun visit(expr: EtsInstanceCallExpr): EtsExpr { - val baseInferred = annotate(expr.instance) as EtsLocal - val argsInferred = expr.args.map { annotate(it) } + val baseInferred = annotate(expr.instance) as EtsLocal // safe cast + val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast val methodInferred = when (val baseType = baseInferred.type) { is EtsClassType -> { val etsClass = scene.projectAndSdkClasses.find { it.signature == baseType.signature } ?: return expr.copy(instance = baseInferred, args = argsInferred) - val callee = etsClass.methods.find { it.signature == expr.method } + val callee = etsClass.methods.find { it.signature == expr.callee } ?: return expr.copy(instance = baseInferred, args = argsInferred) callee.signature } - else -> expr.method + else -> expr.callee } - return EtsInstanceCallExpr(baseInferred, methodInferred, argsInferred) + return expr.copy(instance = baseInferred, callee = methodInferred, args = argsInferred) } override fun visit(expr: EtsStaticCallExpr): EtsExpr { - val argsInferred = expr.args.map { annotate(it) } - return EtsStaticCallExpr(expr.method, argsInferred) + val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast + return expr.copy(args = argsInferred) } override fun visit(expr: EtsPtrCallExpr): EtsExpr { - val ptrInferred = annotate(expr.ptr) as EtsLocal - val argsInferred = expr.args.map { annotate(it) } - return EtsPtrCallExpr(ptrInferred, expr.method, argsInferred) + val ptrInferred = annotate(expr.ptr) as EtsLocal // safe cast + val argsInferred = expr.args.map { annotate(it) as EtsLocal } // safe cast + return expr.copy(ptr = ptrInferred, args = argsInferred) } - - override fun visit(expr: EtsCommaExpr) = expr.copy( - left = annotate(expr.left), - right = annotate(expr.right), - ) - - override fun visit(expr: EtsTernaryExpr) = expr.copy( - condition = annotate(expr.condition), - thenExpr = annotate(expr.thenExpr), - elseExpr = annotate(expr.elseExpr), - ) } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/StmtTypeAnnotator.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/StmtTypeAnnotator.kt index 49b56f971a..e7ed5952ce 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/StmtTypeAnnotator.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/StmtTypeAnnotator.kt @@ -16,20 +16,20 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsExpr -import org.jacodb.ets.base.EtsGotoStmt -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsRawStmt -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsExpr +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsLValue +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsRawStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsValue class StmtTypeAnnotator( private val valueAnnotator: ValueTypeAnnotator, @@ -49,7 +49,7 @@ class StmtTypeAnnotator( override fun visit(stmt: EtsNopStmt) = stmt override fun visit(stmt: EtsAssignStmt) = stmt.copy( - lhv = annotate(stmt.lhv), + lhv = annotate(stmt.lhv) as EtsLValue, // safe cast rhv = annotate(stmt.rhv), ) @@ -58,22 +58,15 @@ class StmtTypeAnnotator( ) override fun visit(stmt: EtsReturnStmt) = stmt.copy( - returnValue = stmt.returnValue?.let { annotate(it) } + returnValue = stmt.returnValue?.let { annotate(it) as EtsLocal } // safe cast ) override fun visit(stmt: EtsThrowStmt) = stmt.copy( - arg = annotate(stmt.arg) + exception = annotate(stmt.exception) as EtsLocal // safe cast ) - override fun visit(stmt: EtsGotoStmt) = stmt - override fun visit(stmt: EtsIfStmt) = stmt.copy( - condition = annotate(stmt.condition) - ) - - override fun visit(stmt: EtsSwitchStmt) = stmt.copy( - arg = annotate(stmt.arg), - cases = stmt.cases.map { annotate(it) }, + condition = annotate(stmt.condition) as EtsLocal // safe cast ) override fun visit(stmt: EtsRawStmt): EtsStmt = stmt diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeScheme.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeScheme.kt index e3f0909966..9a1429b9b9 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeScheme.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeScheme.kt @@ -16,8 +16,8 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ts.infer.AccessPathBase interface MethodTypeScheme { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeSchemes.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeSchemes.kt index cd7848b859..f10bdb4823 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeSchemes.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeSchemes.kt @@ -16,8 +16,8 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ts.infer.AccessPathBase import org.usvm.dataflow.ts.infer.TypeInferenceResult import org.usvm.dataflow.ts.infer.toType @@ -47,7 +47,7 @@ class InferredTypeScheme( } override fun thisType(method: EtsMethod): EtsType? = - typeInferenceResult.inferredCombinedThisType[method.enclosingClass]?.toType() + typeInferenceResult.inferredCombinedThisType[method.signature.enclosingClass]?.toType() } class MethodTypeSchemeImpl( diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ValueTypeAnnotator.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ValueTypeAnnotator.kt index 71dd18e22a..127b2801ab 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ValueTypeAnnotator.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ValueTypeAnnotator.kt @@ -16,16 +16,15 @@ package org.usvm.dataflow.ts.infer.annotation -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsValue import org.usvm.dataflow.ts.infer.AccessPathBase class ValueTypeAnnotator( @@ -47,15 +46,17 @@ class ValueTypeAnnotator( override fun visit(value: EtsLocal): EtsLocal = value.annotate(AccessPathBase.Local(value.name)) { copy(type = it) } - override fun visit(value: EtsThis): EtsValue = - (thisType as? EtsClassType)?.let { value.copy(type = it) } - ?: value.annotate(AccessPathBase.This) { copy(type = it) } + override fun visit(value: EtsThis): EtsValue = value + // TODO: old code: + // (thisType as? EtsClassType)?.let { value.copy(type = it) } + // ?: value.annotate(AccessPathBase.This) { copy(type = it) } - override fun visit(value: EtsParameterRef) = - value.annotate(AccessPathBase.Arg(value.index)) { copy(type = it) } + override fun visit(value: EtsParameterRef) = value + // TODO: old code: + // value.annotate(AccessPathBase.Arg(value.index)) { copy(type = it) } override fun visit(value: EtsArrayAccess): EtsArrayAccess { - val arrayInferred = value.array.accept(this) + val arrayInferred = value.array.accept(this) as EtsLocal // safe cast val arrayType = arrayInferred.type as? EtsArrayType ?: return value val indexInferred = value.index.accept(this) return EtsArrayAccess(arrayInferred, indexInferred, arrayType.elementType) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/Dump.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/Dump.kt index 2241913bcc..812a3706e6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/Dump.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/Dump.kt @@ -20,8 +20,8 @@ import kotlinx.serialization.ExperimentalSerializationApi import kotlinx.serialization.json.Json import kotlinx.serialization.json.encodeToStream import mu.KotlinLogging -import org.jacodb.ets.base.ANONYMOUS_CLASS_PREFIX -import org.jacodb.ets.base.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.usvm.dataflow.ts.infer.TypeInferenceResult import org.usvm.dataflow.ts.infer.dto.toDto import java.nio.file.Path diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt index 3268ce6bce..ff2229a0e7 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt @@ -16,25 +16,6 @@ package org.usvm.dataflow.ts.infer.dto -import org.jacodb.ets.base.EtsAliasType -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsFunctionType -import org.jacodb.ets.base.EtsGenericType -import org.jacodb.ets.base.EtsLiteralType -import org.jacodb.ets.base.EtsNeverType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsTupleType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnionType -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.base.EtsVoidType import org.jacodb.ets.dto.AliasTypeDto import org.jacodb.ets.dto.AnyTypeDto import org.jacodb.ets.dto.ArrayTypeDto @@ -42,8 +23,8 @@ import org.jacodb.ets.dto.BooleanTypeDto import org.jacodb.ets.dto.ClassTypeDto import org.jacodb.ets.dto.FunctionTypeDto import org.jacodb.ets.dto.GenericTypeDto +import org.jacodb.ets.dto.IntersectionTypeDto import org.jacodb.ets.dto.LiteralTypeDto -import org.jacodb.ets.dto.LocalDto import org.jacodb.ets.dto.LocalSignatureDto import org.jacodb.ets.dto.NeverTypeDto import org.jacodb.ets.dto.NullTypeDto @@ -57,6 +38,26 @@ import org.jacodb.ets.dto.UndefinedTypeDto import org.jacodb.ets.dto.UnionTypeDto import org.jacodb.ets.dto.UnknownTypeDto import org.jacodb.ets.dto.VoidTypeDto +import org.jacodb.ets.model.EtsAliasType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsLiteralType +import org.jacodb.ets.model.EtsNeverType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsVoidType fun EtsType.toDto(): TypeDto = accept(EtsTypeToDto) @@ -73,8 +74,27 @@ private object EtsTypeToDto : EtsType.Visitor { return UnionTypeDto(types = type.types.map { it.accept(this) }) } - override fun visit(type: EtsTupleType): TypeDto { - return TupleTypeDto(types = type.types.map { it.accept(this) }) + override fun visit(type: EtsIntersectionType): TypeDto { + return IntersectionTypeDto(types = type.types.map { it.accept(this) }) + } + + override fun visit(type: EtsGenericType): TypeDto { + return GenericTypeDto( + name = type.typeName, + defaultType = type.defaultType?.toDto(), + constraint = type.constraint?.toDto(), + ) + } + + override fun visit(type: EtsAliasType): TypeDto { + return AliasTypeDto( + name = type.name, + originalType = type.originalType.toDto(), + signature = LocalSignatureDto( + type.signature.name, + type.signature.method.toDto(), + ), + ) } override fun visit(type: EtsBooleanType): TypeDto { @@ -134,9 +154,9 @@ private object EtsTypeToDto : EtsType.Visitor { ) } - override fun visit(type: EtsFunctionType): TypeDto { - return FunctionTypeDto( - signature = type.method.toDto(), + override fun visit(type: EtsUnclearRefType): TypeDto { + return UnclearReferenceTypeDto( + name = type.typeName, typeParameters = type.typeParameters.map { it.toDto() }, ) } @@ -148,29 +168,14 @@ private object EtsTypeToDto : EtsType.Visitor { ) } - override fun visit(type: EtsUnclearRefType): TypeDto { - return UnclearReferenceTypeDto( - name = type.typeName, - typeParameters = type.typeParameters.map { it.toDto() }, - ) - } - - override fun visit(type: EtsGenericType): TypeDto { - return GenericTypeDto( - name = type.typeName, - defaultType = type.defaultType?.toDto(), - constraint = type.constraint?.toDto(), - ) + override fun visit(type: EtsTupleType): TypeDto { + return TupleTypeDto(types = type.types.map { it.accept(this) }) } - override fun visit(type: EtsAliasType): TypeDto { - return AliasTypeDto( - name = type.name, - originalType = type.originalType.toDto(), - signature = LocalSignatureDto( - type.signature.name, - type.signature.method.toDto(), - ), + override fun visit(type: EtsFunctionType): TypeDto { + return FunctionTypeDto( + signature = type.signature.toDto(), + typeParameters = type.typeParameters.map { it.toDto() }, ) } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt index 53482c5900..da690dc084 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt @@ -16,18 +16,6 @@ package org.usvm.dataflow.ts.infer.dto -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsBooleanConstant -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNullConstant -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsUndefinedConstant -import org.jacodb.ets.base.EtsValue import org.jacodb.ets.dto.ArrayRefDto import org.jacodb.ets.dto.BooleanTypeDto import org.jacodb.ets.dto.ConstantDto @@ -41,6 +29,20 @@ import org.jacodb.ets.dto.StringTypeDto import org.jacodb.ets.dto.ThisRefDto import org.jacodb.ets.dto.UndefinedTypeDto import org.jacodb.ets.dto.ValueDto +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsConstant +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNullConstant +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsUndefinedConstant +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsValue fun EtsValue.toDto(): ValueDto = accept(EtsValueToDto) @@ -52,6 +54,13 @@ private object EtsValueToDto : EtsValue.Visitor { ) } + override fun visit(value: EtsConstant): ValueDto { + return ConstantDto( + value = value.toString(), + type = value.type.toDto(), + ) + } + override fun visit(value: EtsStringConstant): ValueDto { return ConstantDto( value = value.value, diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/VerificationResult.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/VerificationResult.kt index da90b7dfc5..4825049e4f 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/VerificationResult.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/VerificationResult.kt @@ -16,8 +16,8 @@ package org.usvm.dataflow.ts.infer.verify -import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsUnknownType import org.usvm.dataflow.ts.infer.annotation.MethodTypeSchemeImpl import org.usvm.dataflow.ts.infer.annotation.TypeScheme import org.usvm.dataflow.ts.infer.annotation.TypeSchemeImpl diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ClassSummaryCollector.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ClassSummaryCollector.kt index fe7c21c9fb..b0a9ce0e90 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ClassSummaryCollector.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ClassSummaryCollector.kt @@ -20,14 +20,12 @@ import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsMethod class ClassSummaryCollector( - val methodSummaries: MutableMap = mutableMapOf(), + val methodSummaries: MutableMap = hashMapOf(), ) { fun collect(clazz: EtsClass) { clazz.methods.forEach { method -> - val stmtCollector = StmtSummaryCollector( - method.signature, - methodSummaries.computeIfAbsent(method) { MethodVerificationSummary() } - ) + val summary = methodSummaries.computeIfAbsent(method) { MethodVerificationSummary() } + val stmtCollector = StmtSummaryCollector(method, summary) method.cfg.stmts.forEach { it.accept(stmtCollector) } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt index e25907973d..b53fcb1ba6 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt @@ -16,37 +16,34 @@ package org.usvm.dataflow.ts.infer.verify.collectors -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBinaryExpr -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsExpr -import org.jacodb.ets.base.EtsGotoStmt -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsInstanceOfExpr -import org.jacodb.ets.base.EtsLengthExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsPtrCallExpr -import org.jacodb.ets.base.EtsRawStmt -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStaticCallExpr -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsTernaryExpr -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.base.EtsUnaryExpr -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsExpr +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRawStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsUnaryExpr +import org.jacodb.ets.model.EtsValue class StmtSummaryCollector( - override val method: EtsMethodSignature, + override val method: EtsMethod, override val verificationSummary: MethodVerificationSummary, ) : SummaryCollector, EtsStmt.Visitor, @@ -89,22 +86,13 @@ class StmtSummaryCollector( } override fun visit(stmt: EtsThrowStmt) { - collect(stmt.arg) - } - - override fun visit(stmt: EtsGotoStmt) { - // do nothing + collect(stmt.exception) } override fun visit(stmt: EtsIfStmt) { collect(stmt.condition) } - override fun visit(stmt: EtsSwitchStmt) { - collect(stmt.arg) - stmt.cases.forEach { collect(it) } - } - override fun visit(stmt: EtsRawStmt) { // do nothing } @@ -154,12 +142,6 @@ class StmtSummaryCollector( collect(expr.right) } - is EtsTernaryExpr -> { - collect(expr.condition) - collect(expr.thenExpr) - collect(expr.elseExpr) - } - is EtsInstanceCallExpr -> { collect(expr.instance) requireObjectOrUnknown(expr.instance, expr) @@ -175,10 +157,6 @@ class StmtSummaryCollector( expr.args.forEach { collect(it) } } - is EtsLengthExpr -> { - collect(expr.arg) - } - is EtsInstanceOfExpr -> { collect(expr.arg) } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/SummaryCollector.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/SummaryCollector.kt index 909eb1fb0c..27a62d1cb7 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/SummaryCollector.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/SummaryCollector.kt @@ -16,16 +16,17 @@ package org.usvm.dataflow.ts.infer.verify.collectors -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsRefType -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsValue -import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsValue import org.usvm.dataflow.ts.infer.AccessPathBase import org.usvm.dataflow.ts.infer.toBase +import org.usvm.dataflow.ts.infer.tryGetKnownType data class TypeError( val value: EtsValue, @@ -47,24 +48,26 @@ data class MethodVerificationSummary( ) interface SummaryCollector { - val method: EtsMethodSignature + val method: EtsMethod val verificationSummary: MethodVerificationSummary fun yield(parameter: EtsParameterRef) { - if (!parameter.type.isUnresolved) { + val type = parameter.tryGetKnownType(method) + if (!type.isUnresolved) { verificationSummary.entitySummaries .computeIfAbsent(AccessPathBase.Arg(parameter.index)) { EntityVerificationSummary.empty() } .types - .add(parameter.type) + .add(type) } } fun yield(local: EtsLocal) { - if (!local.type.isUnresolved) { + val type = local.type + if (!type.isUnresolved) { verificationSummary.entitySummaries .computeIfAbsent(AccessPathBase.Local(local.name)) { EntityVerificationSummary.empty() } .types - .add(local.type) + .add(type) } } @@ -72,15 +75,16 @@ interface SummaryCollector { verificationSummary.entitySummaries .computeIfAbsent(AccessPathBase.This) { EntityVerificationSummary.empty() } .types - .add(etsThis.type) + .add(etsThis.tryGetKnownType(method)) } fun requireObjectOrUnknown(value: EtsValue, enclosingExpr: EtsEntity) { - if (!value.type.isUnresolved && value.type !is EtsRefType) { + val type = value.tryGetKnownType(method) + if (!type.isUnresolved && type !is EtsRefType) { verificationSummary.entitySummaries .computeIfAbsent(value.toBase()) { EntityVerificationSummary.empty() } .errors - .add(TypeError(value, enclosingExpr, "$value type should be a reference type, found ${value.type}")) + .add(TypeError(value, enclosingExpr, "$value type should be a reference type, found $type")) } } } diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/Utils.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/Utils.kt index 1af50591af..7fc9ca598b 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/Utils.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/Utils.kt @@ -16,14 +16,14 @@ package org.usvm.dataflow.ts.infer.verify.collectors -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsTupleType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnionType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType val EtsType.isUnresolved: Boolean get() = when (this) { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt index 81820a9f0a..9bc2c3d728 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/EtsTraits.kt @@ -21,31 +21,31 @@ import org.jacodb.api.common.cfg.CommonAssignInst import org.jacodb.api.common.cfg.CommonCallExpr import org.jacodb.api.common.cfg.CommonExpr import org.jacodb.api.common.cfg.CommonValue -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBinaryExpr -import org.jacodb.ets.base.EtsBooleanConstant -import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsConstant -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsImmediate -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsNewArrayExpr -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsUnaryExpr -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsConstant +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsImmediate +import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsUnaryExpr +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.getOperands import org.jacodb.ets.utils.getValues @@ -80,12 +80,17 @@ class EtsTraits : Traits { } override fun getThisInstance(method: EtsMethod): EtsThis { - return EtsThis(EtsClassType(method.signature.enclosingClass)) + return EtsThis( + type = EtsClassType(method.signature.enclosingClass), + ) } override fun getArgument(param: CommonMethodParameter): EtsParameterRef { check(param is EtsMethodParameter) - return EtsParameterRef(index = param.index, type = param.type) + return EtsParameterRef( + index = param.index, + type = param.type, + ) } override fun getArgumentsOf(method: EtsMethod): List { @@ -94,7 +99,7 @@ class EtsTraits : Traits { override fun getCallee(callExpr: CommonCallExpr): EtsMethod { check(callExpr is EtsCallExpr) - return EtsMethodImpl(callExpr.method) + return EtsMethodImpl(callExpr.callee) } override fun getCallExpr(statement: EtsStmt): EtsCallExpr? { @@ -222,8 +227,6 @@ class EtsTraits : Traits { fun EtsEntity.toPathOrNull(): AccessPath? = when (this) { is EtsImmediate -> AccessPath(this, emptyList()) - is EtsThis -> AccessPath(this, emptyList()) - is EtsParameterRef -> AccessPath(this, emptyList()) is EtsArrayAccess -> { diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/RealLocals.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/RealLocals.kt index 30bb4c1e0d..06fa6ea4ab 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/RealLocals.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/RealLocals.kt @@ -1,7 +1,7 @@ package org.usvm.dataflow.ts.util -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsLocal +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod private val realLocalsCache: MutableMap> = hashMapOf() diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/ToStringLimited.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/ToStringLimited.kt index 90314c411b..0e0191d34c 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/ToStringLimited.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/ToStringLimited.kt @@ -16,9 +16,10 @@ package org.usvm.dataflow.ts.util -import org.jacodb.ets.base.EtsTupleType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnionType +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType import org.usvm.dataflow.ts.infer.EtsTypeFact fun EtsType.toStringLimited(): String { @@ -47,6 +48,12 @@ private object ToStringLimited : EtsType.Visitor.Default { }.limit() } + override fun visit(type: EtsIntersectionType): String { + return type.types.joinToString(" | ") { + it.accept(this) + }.limit() + } + override fun visit(type: EtsTupleType): String { return type.types.joinToString(", ", prefix = "[", postfix = "]") { it.accept(this) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt index f2adcbf082..04370daafd 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/util/Utils.kt @@ -16,8 +16,9 @@ package org.usvm.dataflow.ts.util -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsType import org.usvm.dataflow.ts.infer.EtsTypeFact fun EtsType.unwrapPromise(): EtsType { @@ -53,3 +54,6 @@ fun T.toStringLimited(): String { s } } + +val EtsClass.type: EtsClassType + get() = EtsClassType(signature, typeParameters) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt index 194229d182..6c25443aea 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt @@ -17,7 +17,7 @@ package org.usvm.dataflow.ts.test import mu.KotlinLogging -import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsSceneTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsSceneTest.kt index 5ed683007b..75cb5bd4a9 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsSceneTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsSceneTest.kt @@ -16,29 +16,29 @@ package org.usvm.dataflow.ts.test -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsInstLocation -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsVoidType -import org.jacodb.ets.graph.EtsCfg +import org.jacodb.ets.model.BasicBlock +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBlockCfg +import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldImpl import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsFieldSubSignature import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmtLocation +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsVoidType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl import kotlin.test.Test import kotlin.test.assertEquals @@ -59,10 +59,8 @@ class EtsSceneTest { val fieldName = EtsFieldImpl( signature = EtsFieldSignature( enclosingClass = classCatSignature, - sub = EtsFieldSubSignature( - name = "name", - type = EtsStringType, - ) + name = "name", + type = EtsStringType, ) ) val methodMeow = EtsMethodImpl( @@ -84,8 +82,7 @@ class EtsSceneTest { val classCat = EtsClassImpl( signature = classCatSignature, fields = listOf(fieldName), - methods = listOf(methodMeow), - ctor = ctorCat, + methods = listOf(ctorCat, methodMeow), ) val fileCat = EtsFile( signature = fileCatSignature, @@ -105,10 +102,8 @@ class EtsSceneTest { val fieldCats = EtsFieldImpl( signature = EtsFieldSignature( enclosingClass = classBoxSignature, - sub = EtsFieldSubSignature( - name = "cats", - type = EtsArrayType(EtsClassType(classCatSignature), 1), - ) + name = "cats", + type = EtsArrayType(EtsClassType(classCatSignature), 1), ) ) val methodTouch = EtsMethodImpl( @@ -122,32 +117,39 @@ class EtsSceneTest { var index = 0 val stmts = listOf( EtsAssignStmt( - location = EtsInstLocation(it, index++), + location = EtsStmtLocation(it, index++), lhv = EtsLocal("this", EtsClassType(classBoxSignature)), rhv = EtsThis(EtsClassType(classBoxSignature)), ), EtsCallStmt( - location = EtsInstLocation(it, index++), + location = EtsStmtLocation(it, index++), expr = EtsInstanceCallExpr( instance = EtsLocal("this", EtsClassType(classBoxSignature)), - method = methodMeow.signature, + callee = methodMeow.signature, args = emptyList(), + type = methodMeow.signature.returnType, ) ), EtsReturnStmt( - location = EtsInstLocation(it, index++), + location = EtsStmtLocation(it, index++), returnValue = null, ) ) check(index == stmts.size) - val successors = mapOf( - stmts[0] to listOf(stmts[1]), - stmts[1] to listOf(stmts[2]), + val blocks = listOf( + BasicBlock( + id = 0, + statements = stmts, + ), + ) + val successors: Map> = mapOf( + 0 to listOf(), ) - it._cfg = EtsCfg( - stmts = stmts, - successorMap = successors, + val cfg = EtsBlockCfg( + blocks = blocks, + successors = successors, ) + it._cfg = cfg } val ctorBox = EtsMethodImpl( signature = EtsMethodSignature( @@ -160,8 +162,7 @@ class EtsSceneTest { val classBox = EtsClassImpl( signature = classBoxSignature, fields = listOf(fieldCats), - methods = listOf(methodTouch), - ctor = ctorBox, + methods = listOf(ctorBox, methodTouch), ) val fileBox = EtsFile( signature = fileBoxSignature, diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeAnnotationTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeAnnotationTest.kt deleted file mode 100644 index 17b53cbfbd..0000000000 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeAnnotationTest.kt +++ /dev/null @@ -1,193 +0,0 @@ -/* - * Copyright 2022 UnitTestBot contributors (utbot.org) - *

- * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - *

- * http://www.apache.org/licenses/LICENSE-2.0 - *

- * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package org.usvm.dataflow.ts.test - -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsAddExpr -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsInstLocation -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.graph.EtsCfg -import org.jacodb.ets.model.EtsClassImpl -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsDecorator -import org.jacodb.ets.model.EtsFile -import org.jacodb.ets.model.EtsFileSignature -import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsMethodParameter -import org.jacodb.ets.model.EtsMethodSignature -import org.jacodb.ets.model.EtsModifiers -import org.jacodb.ets.model.EtsScene -import org.usvm.dataflow.ts.infer.AccessPathBase -import org.usvm.dataflow.ts.infer.EtsTypeFact -import org.usvm.dataflow.ts.infer.TypeInferenceResult -import org.usvm.dataflow.ts.infer.annotation.InferredTypeScheme -import org.usvm.dataflow.ts.infer.annotation.annotateWithTypes -import org.usvm.dataflow.ts.infer.verify.VerificationResult -import org.usvm.dataflow.ts.infer.verify.verify -import kotlin.test.Test -import kotlin.test.assertEquals -import kotlin.test.assertIs - -class EtsTypeAnnotationTest { - - @Test - fun `test EtsTypeAnnotator`() { - val typeInferenceResult = TypeInferenceResult( - inferredTypes = mapOf( - mainMethod to mapOf( - AccessPathBase.Arg(1) to EtsTypeFact.StringEtsTypeFact, - AccessPathBase.Arg(2) to EtsTypeFact.NumberEtsTypeFact, - AccessPathBase.Local("v1") to EtsTypeFact.StringEtsTypeFact, - AccessPathBase.Local("v2") to EtsTypeFact.NumberEtsTypeFact, - AccessPathBase.Local("v3") to EtsTypeFact.StringEtsTypeFact, - ) - ), - inferredReturnType = mapOf( - mainMethod to EtsTypeFact.StringEtsTypeFact, - ), - inferredCombinedThisType = mapOf( - mainClassSignature to EtsTypeFact.ObjectEtsTypeFact( - cls = EtsClassType(mainClassSignature), - properties = mapOf(), - ) - ) - ) - - val annotatedScene = sampleScene.annotateWithTypes(InferredTypeScheme(typeInferenceResult)) - - val verificationResult = verify(annotatedScene) - assertIs(verificationResult) - - with(verificationResult) { - val methodScheme = scheme.methodSchemes().single() - - assertEquals(EtsStringType, methodScheme.typeOf(AccessPathBase.Arg(1))) - assertEquals(EtsNumberType, methodScheme.typeOf(AccessPathBase.Arg(2))) - - assertEquals(EtsStringType, methodScheme.typeOf(AccessPathBase.Local("v1"))) - assertEquals(EtsNumberType, methodScheme.typeOf(AccessPathBase.Local("v2"))) - assertEquals(EtsStringType, methodScheme.typeOf(AccessPathBase.Local("v3"))) - } - } - - private val mainTs = EtsFileSignature( - projectName = "sampleProject", - fileName = "main.ts", - ) - - private val mainClassSignature = EtsClassSignature( - name = "MainClass", - file = mainTs, - namespace = null, - ) - - private val mainMethodSignature = EtsMethodSignature( - enclosingClass = mainClassSignature, - name = "mainMethod", - parameters = parameters(2), - returnType = EtsUnknownType, - ) - - private val mainMethod = buildMethod(mainMethodSignature) { - val arg1 = EtsParameterRef(1, EtsUnknownType) - val arg2 = EtsParameterRef(2, EtsUnknownType) - val v1 = EtsLocal("v1", EtsUnknownType) - val v2 = EtsLocal("v2", EtsUnknownType) - val v3 = EtsLocal("v3", EtsUnknownType) - - push(EtsAssignStmt(location, v1, arg1)) - push(EtsAssignStmt(location, v2, arg2)) - push(EtsAssignStmt(location, v3, EtsAddExpr(EtsUnknownType, v1, v2))) - push(EtsReturnStmt(location, v3)) - } - - private val mainClassCtorSignature = EtsMethodSignature( - enclosingClass = mainClassSignature, - name = CONSTRUCTOR_NAME, - parameters = parameters(1), - returnType = EtsUnknownType, - ) - - private val mainClassCtor = buildMethod(mainClassCtorSignature) { - val etsThis = EtsThis(EtsClassType(mainClassSignature)) - push(EtsReturnStmt(location, etsThis)) - } - - private val mainClass = EtsClassImpl( - signature = mainClassSignature, - fields = listOf(), - methods = listOf(mainMethod), - ctor = mainClassCtor, - superClass = null, - ) - - private val mainFile = EtsFile( - signature = mainTs, - classes = listOf(mainClass), - namespaces = listOf(), - ) - - private val sampleScene = EtsScene(listOf(mainFile), sdkFiles = emptyList()) - - private class CfgBuilderContext( - val method: EtsMethod, - ) { - private val stmts = mutableListOf() - private val successorsMap = mutableMapOf>() - - fun build(): EtsCfg = EtsCfg(stmts, successorsMap) - - fun push(stmt: EtsStmt) { - stmts.lastOrNull()?.let { link(it, stmt) } - successorsMap[stmt] = mutableListOf() - stmts.add(stmt) - } - - fun link(from: EtsStmt, to: EtsStmt) { - successorsMap.getOrPut(from, ::mutableListOf).add(to) - } - - val location: EtsInstLocation - get() = EtsInstLocation(method, stmts.size) - } - - private fun buildMethod( - signature: EtsMethodSignature, - cfgBuilder: CfgBuilderContext.() -> Unit, - ) = object : EtsMethod { - override val signature = signature - override val typeParameters: List = emptyList() - override val modifiers: EtsModifiers = EtsModifiers.EMPTY - override val decorators: List = emptyList() - override val locals: List = emptyList() - override val cfg = CfgBuilderContext(this).apply(cfgBuilder).build() - } - - private fun parameters(n: Int) = List(n) { - EtsMethodParameter(it, "a$it", EtsUnknownType) - } -} diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt index b61a9010fa..866eb40e7b 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt @@ -22,17 +22,18 @@ import kotlinx.coroutines.runInterruptible import kotlinx.coroutines.withTimeout import kotlinx.serialization.SerializationException import mu.KotlinLogging -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.dto.EtsFileDto import org.jacodb.ets.dto.toEtsFile import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.getLocals import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test @@ -288,9 +289,9 @@ class EtsTypeInferenceTest { val graph = createApplicationGraph(project) val entrypoints = project.projectClasses - .flatMap { it.methods + it.ctor } + .flatMap { it.methods } .filter { it.isPublic || it.name == CONSTRUCTOR_NAME } - .filter { !it.enclosingClass.name.startsWith("AnonymousClass") } + .filter { !it.signature.enclosingClass.name.startsWith("AnonymousClass") } println("entrypoints: (${entrypoints.size})") entrypoints.forEach { println(" ${it.signature.enclosingClass.name}::${it.name}") @@ -326,13 +327,13 @@ class EtsTypeInferenceTest { println("=".repeat(42)) println("Inferred types WITHOUT guesser: ") for ((method, types) in resultWithoutGuessed.inferredTypes) { - println(method.enclosingClass.name to types) + println(method.signature.enclosingClass.name to types) } println("=".repeat(42)) println("Inferred types with guesser: ") for ((method, types) in resultWithGuessed.inferredTypes) { - println(method.enclosingClass.name to types) + println(method.signature.enclosingClass.name to types) } } @@ -391,7 +392,7 @@ class EtsTypeInferenceTest { val result = manager.analyze(listOf(entrypoint), doAddKnownTypes = false) val inferredTypes = result.inferredTypes[inferMethod] - ?: error("No inferred types for method ${inferMethod.enclosingClass.name}::${inferMethod.name}") + ?: error("No inferred types for method ${inferMethod.signature.enclosingClass.name}::${inferMethod.name}") for ((position, expected) in expectedTypeString.sortedByBase()) { val inferred = inferredTypes[position] @@ -493,7 +494,7 @@ class EtsTypeInferenceTest { buildString { appendLine("Inferred return types: ${result.inferredReturnType.size}") for ((method, returnType) in result.inferredReturnType.sortedBy { it.key.toString() }) { - appendLine("${method.enclosingClass.name}::${method.name}: ${returnType.toStringLimited()}") + appendLine("${method.signature.enclosingClass.name}::${method.name}: ${returnType.toStringLimited()}") } } } @@ -519,7 +520,7 @@ class EtsTypeInferenceTest { var numLostNormal = 0 var numBetterThanUnknown = 0 - for (local in method.locals) { + for (local in method.getLocals()) { val inferredType = inferredTypes[AccessPathBase.Local(local.name)]?.toType() val verdict = if (inferredType != null) { if (local.type.isUnknown()) { @@ -559,7 +560,7 @@ class EtsTypeInferenceTest { logger.info { buildString { - appendLine("Local type matching for ${method.enclosingClass.name}::${method.name}:") + appendLine("Local type matching for ${method.signature.enclosingClass.name}::${method.name}:") appendLine(" Matched normal: $numMatchedNormal") appendLine(" Matched unknown: $numMatchedUnknown") appendLine(" Mismatched normal: $numMismatchedNormal") diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverWithAstTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverWithAstTest.kt index b3a6b95771..2a489de0bb 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverWithAstTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverWithAstTest.kt @@ -320,7 +320,7 @@ class EtsTypeResolverWithAstTest { astMethods.forEach { m -> val expectedTypes = ExpectedTypesExtractor(graphAst.cp).extractTypes(m) val abcMethod = abcMethods.singleOrNull { - it.name == m.name && it.enclosingClass.name == m.enclosingClass.name + it.name == m.name && it.signature.enclosingClass.name == m.signature.enclosingClass.name } ?: return@forEach val actualTypes = MethodTypesFacts.from(result, m) classMatcherStatistics.calculateStats( diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt index 4b442b5aea..595c52d347 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt @@ -32,9 +32,9 @@ import kotlin.io.path.exists import kotlin.test.assertTrue object AbcProjects { - private const val yourPrefixForTestFolders = "" - private const val testProjectsVersion = "" - private const val pathToSDK = "" + private const val yourPrefixForTestFolders = "REPLACE_ME" + private const val testProjectsVersion = "REPLACE_ME" + private const val pathToSDK = "REPLACE_ME" @JvmStatic fun projectAvailable(): Boolean { diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt index bc46262364..e1f7801560 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt @@ -17,18 +17,18 @@ package org.usvm.dataflow.ts.test.utils import mu.KotlinLogging -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsFunctionType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.usvm.dataflow.ts.graph.EtsApplicationGraph diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ExpectedTypesExtractor.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ExpectedTypesExtractor.kt index 4161fb465c..a20bf1b90e 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ExpectedTypesExtractor.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ExpectedTypesExtractor.kt @@ -9,7 +9,7 @@ class ExpectedTypesExtractor( fun extractTypes(method: EtsMethod): MethodTypes { val returnType = method.returnType val argumentsTypes = method.parameters.map { it.type } - val thisType = scene.getEtsClassType(method.enclosingClass) + val thisType = scene.getEtsClassType(method.signature.enclosingClass) return MethodTypes(thisType, argumentsTypes, returnType) } } diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt index a0a4c094d5..6fdd5f66fd 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt @@ -16,26 +16,27 @@ package org.usvm.dataflow.ts.test.utils -import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME -import org.jacodb.ets.base.DEFAULT_ARK_METHOD_NAME -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsFunctionType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnionType -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.base.INSTANCE_INIT_METHOD_NAME -import org.jacodb.ets.base.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.getLocals import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.infer.AccessPathBase import org.usvm.dataflow.ts.infer.EtsTypeFact @@ -77,7 +78,7 @@ class TypeInferenceStatistics { graph: EtsApplicationGraph, ) { overallTypes += 1 // thisType - overallTypes += method.parameters.size + method.locals.size + overallTypes += method.parameters.size + method.getLocals().size methodTypeFacts.apply { if (combinedThisFact == null @@ -91,7 +92,7 @@ class TypeInferenceStatistics { } } - val thisType = graph.cp.getEtsClassType(method.enclosingClass) + val thisType = graph.cp.getEtsClassType(method.signature.enclosingClass) val argTypes = method.parameters.map { it.type } val locals = method.getRealLocals().filterNot { it.name == "this" } @@ -344,7 +345,7 @@ class TypeInferenceStatistics { return InferenceStatus.TYPE_INFO_FOUND_PREV_KNOWN } - val typeName = fact.cls!!.typeName + val typeName = fact.cls.typeName if ((type is EtsClassType || type is EtsUnclearRefType) && type.typeName == typeName) { exactTypeInferredCorrectlyPreviouslyKnown++ @@ -501,7 +502,7 @@ class TypeInferenceStatistics { noTypesInferred .filterNot { it.name == INSTANCE_INIT_METHOD_NAME || it.name == STATIC_INIT_METHOD_NAME } - .filterNot { it.name == DEFAULT_ARK_METHOD_NAME && it.enclosingClass.name == DEFAULT_ARK_CLASS_NAME } + .filterNot { it.name == DEFAULT_ARK_METHOD_NAME && it.signature.enclosingClass.name == DEFAULT_ARK_CLASS_NAME } .sortedBy { it.signature.toString() } .forEach { appendLine(it) @@ -573,7 +574,7 @@ data class MethodTypesFacts( m: EtsMethod, ): MethodTypesFacts { val combinedThisFact = result.inferredCombinedThisType.entries.firstOrNull { - it.key.name == m.enclosingClass.name + it.key.name == m.signature.enclosingClass.name }?.value val factsForMethod = result.inferredTypes.entries.singleOrNull { @@ -601,7 +602,7 @@ data class MethodTypesFacts( // TODO hack because of an issue with signatures private val compareByMethodNameAndEnclosingClass = { fst: EtsMethod, snd: EtsMethod -> - fst.name === snd.name && fst.enclosingClass.name === snd.enclosingClass.name + fst.name === snd.name && fst.signature.enclosingClass.name === snd.signature.enclosingClass.name } private fun EtsTypeFact.matchesWith(type: EtsType): Boolean { diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/Utils.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/Utils.kt index b8d9ef1b14..9a135964ba 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/Utils.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/Utils.kt @@ -16,10 +16,10 @@ package org.usvm.dataflow.ts.test.utils -import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME -import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME fun EtsScene.getEtsClassType(signature: EtsClassSignature): EtsClassType? { if (signature.name == DEFAULT_ARK_CLASS_NAME || signature.name.isBlank()) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt index 9f1e936dfe..ccf3478710 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt @@ -1,9 +1,9 @@ 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 +import org.jacodb.ets.model.EtsStmt data class TsTest( val method: EtsMethod, diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt b/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt index 34336de639..3a6d532c92 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt @@ -1,6 +1,6 @@ package org.usvm.api.targets -import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsStmt import org.usvm.targets.UTarget class TsTarget : UTarget() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt index c6a0d84110..6e4c94c7d3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsApplicationGraph.kt @@ -1,8 +1,8 @@ package org.usvm.machine -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl import org.usvm.statistics.ApplicationGraph diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt index 45dba63d90..5030e7daf7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt @@ -3,7 +3,7 @@ package org.usvm.machine import io.ksmt.solver.yices.KYicesSolver import io.ksmt.solver.z3.KZ3Solver import io.ksmt.symfpu.solver.KSymFpuSolver -import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsType import org.usvm.SolverType import org.usvm.UBv32SizeExprProvider import org.usvm.UComponents diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 6812ec3295..54537b9226 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -2,16 +2,17 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsRefType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnionType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType +import org.jacodb.ets.model.EtsUnknownType import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 31f1001254..972f346c6e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -1,8 +1,8 @@ package org.usvm.machine -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt import org.usvm.CoverageZone import org.usvm.StateCollectionStrategy import org.usvm.UMachine diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTransformer.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsTransformer.kt index 5d4f78bb34..f95bc43625 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTransformer.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsTransformer.kt @@ -1,6 +1,6 @@ package org.usvm.machine -import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsType import org.usvm.UComposer import org.usvm.UContext import org.usvm.UTransformer diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt index 2d11c6e145..c9aaadf641 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsTypeSystem.kt @@ -1,12 +1,12 @@ package org.usvm.machine -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsPrimitiveType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsPrimitiveType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType import org.usvm.types.TypesResult import org.usvm.types.TypesResult.Companion.toTypesResult import org.usvm.types.USupportTypeStream diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index ed36cb3f35..56b7a0adec 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -3,78 +3,76 @@ package org.usvm.machine.expr import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import mu.KotlinLogging -import org.jacodb.ets.base.EtsAddExpr -import org.jacodb.ets.base.EtsAndExpr -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsAwaitExpr -import org.jacodb.ets.base.EtsBinaryExpr -import org.jacodb.ets.base.EtsBitAndExpr -import org.jacodb.ets.base.EtsBitNotExpr -import org.jacodb.ets.base.EtsBitOrExpr -import org.jacodb.ets.base.EtsBitXorExpr -import org.jacodb.ets.base.EtsBooleanConstant -import org.jacodb.ets.base.EtsCastExpr -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsCommaExpr -import org.jacodb.ets.base.EtsDeleteExpr -import org.jacodb.ets.base.EtsDivExpr -import org.jacodb.ets.base.EtsEntity -import org.jacodb.ets.base.EtsEqExpr -import org.jacodb.ets.base.EtsExpExpr -import org.jacodb.ets.base.EtsGtEqExpr -import org.jacodb.ets.base.EtsGtExpr -import org.jacodb.ets.base.EtsInExpr -import org.jacodb.ets.base.EtsInstanceCallExpr -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsInstanceOfExpr -import org.jacodb.ets.base.EtsLeftShiftExpr -import org.jacodb.ets.base.EtsLengthExpr -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsLtEqExpr -import org.jacodb.ets.base.EtsLtExpr -import org.jacodb.ets.base.EtsMulExpr -import org.jacodb.ets.base.EtsNegExpr -import org.jacodb.ets.base.EtsNewArrayExpr -import org.jacodb.ets.base.EtsNewExpr -import org.jacodb.ets.base.EtsNotEqExpr -import org.jacodb.ets.base.EtsNotExpr -import org.jacodb.ets.base.EtsNullConstant -import org.jacodb.ets.base.EtsNullishCoalescingExpr -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsOrExpr -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsPostDecExpr -import org.jacodb.ets.base.EtsPostIncExpr -import org.jacodb.ets.base.EtsPreDecExpr -import org.jacodb.ets.base.EtsPreIncExpr -import org.jacodb.ets.base.EtsPtrCallExpr -import org.jacodb.ets.base.EtsRemExpr -import org.jacodb.ets.base.EtsRightShiftExpr -import org.jacodb.ets.base.EtsStaticCallExpr -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStrictEqExpr -import org.jacodb.ets.base.EtsStrictNotEqExpr -import org.jacodb.ets.base.EtsStringConstant -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsSubExpr -import org.jacodb.ets.base.EtsTernaryExpr -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsTypeOfExpr -import org.jacodb.ets.base.EtsUnaryExpr -import org.jacodb.ets.base.EtsUnaryPlusExpr -import org.jacodb.ets.base.EtsUndefinedConstant -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.base.EtsUnsignedRightShiftExpr -import org.jacodb.ets.base.EtsValue -import org.jacodb.ets.base.EtsVoidExpr -import org.jacodb.ets.base.EtsYieldExpr -import org.jacodb.ets.base.STATIC_INIT_METHOD_NAME -import org.jacodb.ets.base.UNKNOWN_CLASS_NAME +import org.jacodb.ets.model.EtsAddExpr +import org.jacodb.ets.model.EtsAndExpr +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsAwaitExpr +import org.jacodb.ets.model.EtsBinaryExpr +import org.jacodb.ets.model.EtsBitAndExpr +import org.jacodb.ets.model.EtsBitNotExpr +import org.jacodb.ets.model.EtsBitOrExpr +import org.jacodb.ets.model.EtsBitXorExpr +import org.jacodb.ets.model.EtsBooleanConstant +import org.jacodb.ets.model.EtsCastExpr +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsConstant +import org.jacodb.ets.model.EtsDeleteExpr +import org.jacodb.ets.model.EtsDivExpr +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsEqExpr +import org.jacodb.ets.model.EtsExpExpr import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsGtEqExpr +import org.jacodb.ets.model.EtsGtExpr +import org.jacodb.ets.model.EtsInExpr +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsInstanceOfExpr +import org.jacodb.ets.model.EtsLeftShiftExpr +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsLtEqExpr +import org.jacodb.ets.model.EtsLtExpr import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsMulExpr +import org.jacodb.ets.model.EtsNegExpr +import org.jacodb.ets.model.EtsNewArrayExpr +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsNotEqExpr +import org.jacodb.ets.model.EtsNotExpr +import org.jacodb.ets.model.EtsNullConstant +import org.jacodb.ets.model.EtsNullishCoalescingExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsOrExpr +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPostDecExpr +import org.jacodb.ets.model.EtsPostIncExpr +import org.jacodb.ets.model.EtsPreDecExpr +import org.jacodb.ets.model.EtsPreIncExpr +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRemExpr +import org.jacodb.ets.model.EtsRightShiftExpr +import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStrictEqExpr +import org.jacodb.ets.model.EtsStrictNotEqExpr +import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsSubExpr +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsTypeOfExpr +import org.jacodb.ets.model.EtsUnaryExpr +import org.jacodb.ets.model.EtsUnaryPlusExpr +import org.jacodb.ets.model.EtsUndefinedConstant +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsUnsignedRightShiftExpr +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.model.EtsVoidExpr +import org.jacodb.ets.model.EtsYieldExpr +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -82,6 +80,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.allocateArray +import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope @@ -182,17 +181,20 @@ class TsExprResolver( // region CONSTANT - override fun visit(value: EtsBooleanConstant): UExpr { + override fun visit(value: EtsConstant): UExpr? { return simpleValueResolver.visit(value) } - override fun visit(value: EtsNumberConstant): UExpr { + override fun visit(value: EtsStringConstant): UExpr? { return simpleValueResolver.visit(value) } - override fun visit(value: EtsStringConstant): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + override fun visit(value: EtsBooleanConstant): UExpr { + return simpleValueResolver.visit(value) + } + + override fun visit(value: EtsNumberConstant): UExpr { + return simpleValueResolver.visit(value) } override fun visit(value: EtsNullConstant): UExpr { @@ -350,11 +352,6 @@ class TsExprResolver( error("Not supported $expr") } - override fun visit(expr: EtsCommaExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") - } - // endregion // region RELATION @@ -433,7 +430,7 @@ class TsExprResolver( override fun visit(expr: EtsInstanceCallExpr): UExpr? = with(ctx) { if (expr.instance.name == "Number") { - if (expr.method.name == "isNaN") { + if (expr.callee.name == "isNaN") { return resolveAfterResolved(expr.args.single()) { arg -> handleNumberIsNaN(arg) } @@ -441,13 +438,13 @@ class TsExprResolver( } resolveInvoke( - method = expr.method, + method = expr.callee, instance = expr.instance, arguments = { expr.args }, - argumentTypes = { expr.method.parameters.map { it.type } }, + argumentTypes = { expr.callee.parameters.map { it.type } }, ) { args -> doWithState { - val method = resolveInstanceCall(expr.instance, expr.method) + val method = resolveInstanceCall(expr.instance, expr.callee) check(args.size == method.parametersWithThisCount) pushSortsForArguments(expr.instance, expr.args, localToIdx) @@ -459,7 +456,7 @@ class TsExprResolver( } override fun visit(expr: EtsStaticCallExpr): UExpr? = with(ctx) { - if (expr.method.name == "Number" && expr.method.enclosingClass.name == "") { + if (expr.callee.name == "Number" && expr.callee.enclosingClass.name == "") { check(expr.args.size == 1) { "Number constructor should have exactly one argument" } return resolveAfterResolved(expr.args.single()) { mkNumericExpr(it, scope) @@ -467,10 +464,10 @@ class TsExprResolver( } resolveInvoke( - method = expr.method, + method = expr.callee, instance = null, arguments = { expr.args }, - argumentTypes = { expr.method.parameters.map { it.type } }, + argumentTypes = { expr.callee.parameters.map { it.type } }, ) { args -> // TODO: IMPORTANT do not forget to fill sorts of arguments map TODO("Unsupported static methods") @@ -489,7 +486,7 @@ class TsExprResolver( // Perfect signature: if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) { val clazz = ctx.scene.projectAndSdkClasses.single { it.name == method.enclosingClass.name } - return (clazz.methods + clazz.ctor).single { it.name == method.name } + return clazz.methods.single { it.name == method.name } } // Unknown signature: @@ -499,15 +496,15 @@ class TsExprResolver( .filter { it.name == instanceType.signature.name } if (classes.size == 1) { val clazz = classes.single() - return (clazz.methods + clazz.ctor).single { it.name == method.name } + return clazz.methods.single { it.name == method.name } } val methods = classes - .flatMap { it.methods + it.ctor } + .flatMap { it.methods } .filter { it.name == method.name } if (methods.size == 1) return methods.single() } else { val methods = ctx.scene.projectAndSdkClasses - .flatMap { it.methods + it.ctor } + .flatMap { it.methods } .filter { it.name == method.name } if (methods.size == 1) return methods.single() } @@ -761,23 +758,13 @@ class TsExprResolver( blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type ) - val address = memory.allocateArray(expr.type, sizeSort, bvSize) - memory.types.allocate(address.address, expr.type) + val arrayType = EtsArrayType(EtsUnknownType, 1) // TODO: expr.type + val address = memory.allocateArray(arrayType, sizeSort, bvSize) address } } - override fun visit(expr: EtsLengthExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") - } - - override fun visit(expr: EtsTernaryExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") - } - // endregion // TODO incorrect implementation @@ -798,7 +785,8 @@ class TsSimpleValueResolver( val localIdx = localToIdx(currentMethod, local) val sort = scope.calcOnState { - getOrPutSortForLocal(localIdx, local.type) + val type = local.tryGetKnownType(currentMethod) + getOrPutSortForLocal(localIdx, type) } // If we are not in the entrypoint, all correct values are already resolved and we can just return @@ -859,6 +847,16 @@ class TsSimpleValueResolver( return scope.calcOnState { memory.read(lValue) } } + override fun visit(value: EtsConstant): UExpr = with(ctx) { + logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } + error("Not supported $value") + } + + override fun visit(value: EtsStringConstant): UExpr = with(ctx) { + logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } + error("Not supported $value") + } + override fun visit(value: EtsBooleanConstant): UExpr = with(ctx) { mkBool(value.value) } @@ -867,11 +865,6 @@ class TsSimpleValueResolver( mkFp64(value.value) } - override fun visit(value: EtsStringConstant): UExpr = with(ctx) { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") - } - override fun visit(value: EtsNullConstant): UExpr = with(ctx) { mkTsNullValue() } @@ -885,12 +878,10 @@ class TsSimpleValueResolver( } override fun visit(value: EtsInstanceFieldRef): UExpr = with(ctx) { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + error("Should not be called") } override fun visit(value: EtsStaticFieldRef): UExpr = with(ctx) { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + error("Should not be called") } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 478a9d2878..fe60350ab7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -1,26 +1,24 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr -import org.jacodb.ets.base.EtsArrayAccess -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCallStmt -import org.jacodb.ets.base.EtsGotoStmt -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsInstanceFieldRef -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNopStmt -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStaticFieldRef -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsThrowStmt -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsValue +import org.jacodb.ets.model.EtsArrayAccess +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsInstanceFieldRef +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.StepResult import org.usvm.StepScope @@ -86,9 +84,7 @@ class TsInterpreter( is EtsAssignStmt -> visitAssignStmt(scope, stmt) is EtsCallStmt -> visitCallStmt(scope, stmt) is EtsThrowStmt -> visitThrowStmt(scope, stmt) - is EtsGotoStmt -> visitGotoStmt(scope, stmt) is EtsNopStmt -> visitNopStmt(scope, stmt) - is EtsSwitchStmt -> visitSwitchStmt(scope, stmt) else -> error("Unknown stmt: $stmt") } @@ -105,7 +101,7 @@ class TsInterpreter( ctx.mkTruthyExpr(expr, scope) } - val (negStmt, posStmt) = applicationGraph.successors(stmt).take(2).toList() + val (posStmt, negStmt) = applicationGraph.successors(stmt).take(2).toList() scope.forkWithBlackList( boolExpr, @@ -239,18 +235,10 @@ class TsInterpreter( TODO() } - private fun visitGotoStmt(scope: TsStepScope, stmt: EtsGotoStmt) { - TODO() - } - private fun visitNopStmt(scope: TsStepScope, stmt: EtsNopStmt) { TODO() } - private fun visitSwitchStmt(scope: TsStepScope, stmt: EtsSwitchStmt) { - TODO() - } - private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver = TsExprResolver(ctx, scope, ::mapLocalToIdx) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt index 50d8f813b7..41b7254da6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt @@ -1,10 +1,9 @@ package org.usvm.machine.interpreter -import org.jacodb.ets.base.EtsBooleanType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsFieldSubSignature import org.usvm.UBoolSort import org.usvm.UHeapRef import org.usvm.collection.field.UFieldLValue @@ -30,10 +29,8 @@ private fun mkStaticFieldsInitializedFlag( ): UFieldLValue { val field = EtsFieldSignature( enclosingClass = clazz, - sub = EtsFieldSubSignature( - name = "__initialized__", - type = EtsBooleanType, - ), + name = "__initialized__", + type = EtsBooleanType, ) return mkFieldLValue(instance.ctx.boolSort, instance, field) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt index d99e0a7127..844ed9963b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt @@ -1,7 +1,7 @@ package org.usvm.machine.state -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 6278fcc312..892b49c0e4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -1,11 +1,12 @@ package org.usvm.machine.state -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsValue import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsValue import org.usvm.PathNode import org.usvm.UCallStack import org.usvm.UConcreteHeapRef @@ -72,7 +73,7 @@ class TsState( fun pushSortsForArguments(instance: EtsLocal?, args: List, localToIdx: (EtsMethod, EtsValue) -> Int) { val argSorts = args.map { arg -> val localIdx = localToIdx(lastEnteredMethod, arg) - getOrPutSortForLocal(localIdx, arg.type) + getOrPutSortForLocal(localIdx, if (arg is EtsLocal) arg.type else EtsUnknownType) // TODO: type } val instanceIdx = instance?.let { localToIdx(lastEnteredMethod, it) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index cf34fc2fbc..13f199cffc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -1,7 +1,7 @@ package org.usvm.machine.state -import org.jacodb.ets.base.EtsStmt import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.utils.getDeclaredLocals import org.usvm.UExpr import org.usvm.USort diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt index efe0acf425..d31e177c1c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeType.kt @@ -1,6 +1,6 @@ package org.usvm.machine.types -import org.jacodb.ets.base.EtsType +import org.jacodb.ets.model.EtsType import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.USort diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index 9751cf643c..76a0e6c62c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -1,12 +1,12 @@ package org.usvm.util -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.UNKNOWN_CLASS_NAME +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.machine.TsContext fun TsContext.resolveEtsField( @@ -34,7 +34,7 @@ fun TsContext.resolveEtsField( } is EtsUnclearRefType -> { - val field = tryGetSingleField(scene, instanceType.name, field.name) + val field = tryGetSingleField(scene, instanceType.typeName, field.name) if (field != null) return field } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt index 08c33868fa..6a3b7a317b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -1,6 +1,6 @@ package org.usvm.util -import org.jacodb.ets.base.EtsArrayType +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsFieldSignature import org.usvm.UExpr import org.usvm.UHeapRef diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt index 8790e94910..ab7ea20c7f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt @@ -1,9 +1,9 @@ package org.usvm.util import io.ksmt.sort.KFp64Sort -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsType import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsType import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.UHeapRef diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt index f2ca772be0..130b2dbd27 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt @@ -1,47 +1,30 @@ package org.usvm.samples -import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME -import org.jacodb.ets.base.EtsAndExpr -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsInstLocation -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNotEqExpr -import org.jacodb.ets.base.EtsNumberConstant -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsParameterRef -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsStmt -import org.jacodb.ets.base.EtsThis -import org.jacodb.ets.base.EtsUnknownType import org.jacodb.ets.dsl.and import org.jacodb.ets.dsl.const import org.jacodb.ets.dsl.local +import org.jacodb.ets.dsl.neq +import org.jacodb.ets.dsl.not import org.jacodb.ets.dsl.param import org.jacodb.ets.dsl.program import org.jacodb.ets.dsl.thisRef import org.jacodb.ets.dsl.toBlockCfg -import org.jacodb.ets.graph.EtsCfg -import org.jacodb.ets.graph.linearize -import org.jacodb.ets.graph.toEtsBlockCfg +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.getLocals +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.toEtsBlockCfg import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner import org.usvm.util.isTruthy -private fun EtsMethodParameter.toRef(): EtsParameterRef { - return EtsParameterRef(index, type) -} - class And : TsMethodTestRunner() { private val className = this::class.simpleName!! @@ -82,7 +65,6 @@ class And : TsMethodTestRunner() { } val blockCfg = prog.toBlockCfg() - val locals = mutableListOf() val method = EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = classSignature, @@ -93,14 +75,11 @@ class And : TsMethodTestRunner() { ), returnType = EtsNumberType, ), - locals = locals, ) + method.enclosingClass = scene.projectClasses.first { it.name == DEFAULT_ARK_CLASS_NAME } val etsBlockCfg = blockCfg.toEtsBlockCfg(method) - val etsCfg = etsBlockCfg.linearize() - - method._cfg = etsCfg - locals += method.getLocals() + method._cfg = etsBlockCfg discoverProperties( method = method, @@ -128,12 +107,42 @@ class And : TsMethodTestRunner() { // } // + val prog = program { + assign(local("a"), param(0)) + assign(local("b"), param(1)) + assign(local("this"), thisRef()) + ifStmt(and(local("a"), local("b"))) { + ret(const(1.0)) + } + ifStmt(and(local("a"), neq(local("b"), local("b")))) { + ret(const(2.0)) + } + ifStmt(local("a")) { + ret(const(3.0)) + } + ifStmt(and(neq(local("a"), local("a")), local("b"))) { + ret(const(4.0)) + } + ifStmt(and(neq(local("a"), local("a")), neq(local("b"), local("b")))) { + ret(const(5.0)) + } + ifStmt(neq(local("a"), local("a"))) { + ret(const(6.0)) + } + ifStmt(local("b")) { + ret(const(7.0)) + } + ifStmt(neq(local("b"), local("b"))) { + ret(const(8.0)) + } + ret(const(9.0)) + } + val blockCfg = prog.toBlockCfg() + val methodParameters = listOf( EtsMethodParameter(0, "a", EtsNumberType), EtsMethodParameter(1, "b", EtsNumberType), ) - val locals = mutableListOf() - val method = EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = classSignature, @@ -141,91 +150,11 @@ class And : TsMethodTestRunner() { parameters = methodParameters, returnType = EtsNumberType, ), - locals = locals, ) - val statements = mutableListOf() - val successorMap = mutableMapOf>() - val loc = { EtsInstLocation(method, statements.size) } - - val localA = methodParameters[0].let { param -> - EtsLocal(param.name, param.type) - } - val localB = methodParameters[1].let { param -> - EtsLocal(param.name, param.type) - } - val localThis = EtsLocal("this", EtsClassType(classSignature)) + method.enclosingClass = scene.projectClasses.first { it.name == DEFAULT_ARK_CLASS_NAME } - val assA = EtsAssignStmt(loc(), localA, methodParameters[0].toRef()).also { statements += it } - val assB = EtsAssignStmt(loc(), localB, methodParameters[1].toRef()).also { statements += it } - val assThis = EtsAssignStmt(loc(), localThis, EtsThis(EtsClassType(classSignature))).also { statements += it } - - // %0 := a && b - val local0 = EtsLocal("%0", EtsUnknownType) - val ass0 = EtsAssignStmt(loc(), local0, EtsAndExpr(EtsUnknownType, localA, localB)).also { statements += it } - val if0 = EtsIfStmt(loc(), local0).also { statements += it } - val ret1 = EtsReturnStmt(loc(), EtsNumberConstant(1.0)).also { statements += it } - // %1 := (b != b) - val local1 = EtsLocal("%1", EtsUnknownType) - val ass1 = EtsAssignStmt(loc(), local1, EtsNotEqExpr(localB, localB)).also { statements += it } - // %2 := a && %1 == a && (b != b) - val local2 = EtsLocal("%2", EtsUnknownType) - val ass2 = EtsAssignStmt(loc(), local2, EtsAndExpr(EtsUnknownType, localA, local1)).also { statements += it } - val if2 = EtsIfStmt(loc(), local2).also { statements += it } - val ret2 = EtsReturnStmt(loc(), EtsNumberConstant(2.0)).also { statements += it } - val ifA = EtsIfStmt(loc(), localA).also { statements += it } - val ret3 = EtsReturnStmt(loc(), EtsNumberConstant(3.0)).also { statements += it } - // %3 := (a != a) - val local3 = EtsLocal("%3", EtsUnknownType) - val ass3 = EtsAssignStmt(loc(), local3, EtsNotEqExpr(localA, localA)).also { statements += it } - // %4 := %3 && b == (a != a) && b - val local4 = EtsLocal("%4", EtsUnknownType) - val ass4 = EtsAssignStmt(loc(), local4, EtsAndExpr(EtsUnknownType, local3, localB)).also { statements += it } - val if4 = EtsIfStmt(loc(), local4).also { statements += it } - val ret4 = EtsReturnStmt(loc(), EtsNumberConstant(4.0)).also { statements += it } - // %5 := %3 && %1 == (a != a) && (b != b) - val local5 = EtsLocal("%5", EtsUnknownType) - val ass5 = EtsAssignStmt(loc(), local5, EtsAndExpr(EtsUnknownType, local3, local1)).also { statements += it } - val if5 = EtsIfStmt(loc(), local5).also { statements += it } - val ret5 = EtsReturnStmt(loc(), EtsNumberConstant(5.0)).also { statements += it } - val if3 = EtsIfStmt(loc(), local3).also { statements += it } - val ret6 = EtsReturnStmt(loc(), EtsNumberConstant(6.0)).also { statements += it } - val ifB = EtsIfStmt(loc(), localB).also { statements += it } - val ret7 = EtsReturnStmt(loc(), EtsNumberConstant(7.0)).also { statements += it } - val if1 = EtsIfStmt(loc(), local1).also { statements += it } - val ret8 = EtsReturnStmt(loc(), EtsNumberConstant(8.0)).also { statements += it } - val ret9 = EtsReturnStmt(loc(), EtsNumberConstant(9.0)).also { statements += it } - - // Note: for if-statements, successors must be (falseBranch, trueBranch) !!! - successorMap[assA] = listOf(assB) - successorMap[assB] = listOf(assThis) - successorMap[assThis] = listOf(ass0) - successorMap[ass0] = listOf(if0) - successorMap[if0] = listOf(ass1, ret1) - successorMap[ass1] = listOf(ass2) - successorMap[ass2] = listOf(if2) - successorMap[if2] = listOf(ifA, ret2) - successorMap[ifA] = listOf(ass3, ret3) - successorMap[ass3] = listOf(ass4) - successorMap[ass4] = listOf(if4) - successorMap[if4] = listOf(ass5, ret4) - successorMap[ass5] = listOf(if5) - successorMap[if5] = listOf(if3, ret5) - successorMap[if3] = listOf(ifB, ret6) - successorMap[ifB] = listOf(if1, ret7) - successorMap[if1] = listOf(ret9, ret8) - - successorMap[ret1] = emptyList() - successorMap[ret2] = emptyList() - successorMap[ret3] = emptyList() - successorMap[ret4] = emptyList() - successorMap[ret5] = emptyList() - successorMap[ret6] = emptyList() - successorMap[ret7] = emptyList() - successorMap[ret8] = emptyList() - successorMap[ret9] = emptyList() - - method._cfg = EtsCfg(statements, successorMap) - locals += method.getLocals() + val etsBlockCfg = blockCfg.toEtsBlockCfg(method) + method._cfg = etsBlockCfg discoverProperties( method = method, @@ -255,12 +184,33 @@ class And : TsMethodTestRunner() { // } // + val prog = program { + assign(local("a"), param(0)) + assign(local("b"), param(1)) + assign(local("this"), thisRef()) + ifStmt(and(local("a"), local("b"))) { + ret(const(1.0)) + } + ifStmt(and(local("a"), neq(local("b"), local("b")))) { + ret(const(2.0)) + } + ifStmt(local("a")) { + ret(const(3.0)) + } + ifStmt(local("b")) { + ret(const(4.0)) + } + ifStmt(neq(local("b"), local("b"))) { + ret(const(5.0)) + } + ret(const(6.0)) + } + val blockCfg = prog.toBlockCfg() + val methodParameters = listOf( EtsMethodParameter(0, "a", EtsBooleanType), EtsMethodParameter(1, "b", EtsNumberType), ) - val locals = mutableListOf() - val method = EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = classSignature, @@ -268,67 +218,11 @@ class And : TsMethodTestRunner() { parameters = methodParameters, returnType = EtsNumberType, ), - locals = locals, ) - val statements = mutableListOf() - val successorMap = mutableMapOf>() - val loc = { EtsInstLocation(method, statements.size) } - - val localA = methodParameters[0].let { param -> - EtsLocal(param.name, param.type) - } - val localB = methodParameters[1].let { param -> - EtsLocal(param.name, param.type) - } - val localThis = EtsLocal("this", EtsClassType(classSignature)) + method.enclosingClass = scene.projectClasses.first { it.name == DEFAULT_ARK_CLASS_NAME } - val assA = EtsAssignStmt(loc(), localA, methodParameters[0].toRef()).also { statements += it } - val assB = EtsAssignStmt(loc(), localB, methodParameters[1].toRef()).also { statements += it } - val assThis = EtsAssignStmt(loc(), localThis, EtsThis(EtsClassType(classSignature))).also { statements += it } - - // %0 := a && b - val local0 = EtsLocal("%0", EtsUnknownType) - val ass0 = EtsAssignStmt(loc(), local0, EtsAndExpr(EtsUnknownType, localA, localB)).also { statements += it } - val if0 = EtsIfStmt(loc(), local0).also { statements += it } - val ret1 = EtsReturnStmt(loc(), EtsNumberConstant(1.0)).also { statements += it } - // %1 := (b != b) - val local1 = EtsLocal("%1", EtsUnknownType) - val ass1 = EtsAssignStmt(loc(), local1, EtsNotEqExpr(localB, localB)).also { statements += it } - // %2 := a && %1 == a && (b != b) - val local2 = EtsLocal("%2", EtsUnknownType) - val ass2 = EtsAssignStmt(loc(), local2, EtsAndExpr(EtsUnknownType, localA, local1)).also { statements += it } - val if2 = EtsIfStmt(loc(), local2).also { statements += it } - val ret2 = EtsReturnStmt(loc(), EtsNumberConstant(2.0)).also { statements += it } - val ifA = EtsIfStmt(loc(), localA).also { statements += it } - val ret3 = EtsReturnStmt(loc(), EtsNumberConstant(3.0)).also { statements += it } - val ifB = EtsIfStmt(loc(), localB).also { statements += it } - val ret4 = EtsReturnStmt(loc(), EtsNumberConstant(4.0)).also { statements += it } - val if1 = EtsIfStmt(loc(), local1).also { statements += it } - val ret5 = EtsReturnStmt(loc(), EtsNumberConstant(5.0)).also { statements += it } - val ret6 = EtsReturnStmt(loc(), EtsNumberConstant(6.0)).also { statements += it } - - // Note: for if-statements, successors must be (falseBranch, trueBranch) !!! - successorMap[assA] = listOf(assB) - successorMap[assB] = listOf(assThis) - successorMap[assThis] = listOf(ass0) - successorMap[ass0] = listOf(if0) - successorMap[if0] = listOf(ass1, ret1) - successorMap[ass1] = listOf(ass2) - successorMap[ass2] = listOf(if2) - successorMap[if2] = listOf(ifA, ret2) - successorMap[ifA] = listOf(ifB, ret3) - successorMap[ifB] = listOf(if1, ret4) - successorMap[if1] = listOf(ret6, ret5) - - successorMap[ret1] = emptyList() - successorMap[ret2] = emptyList() - successorMap[ret3] = emptyList() - successorMap[ret4] = emptyList() - successorMap[ret5] = emptyList() - successorMap[ret6] = emptyList() - - method._cfg = EtsCfg(statements, successorMap) - locals += method.getLocals() + val etsBlockCfg = blockCfg.toEtsBlockCfg(method) + method._cfg = etsBlockCfg discoverProperties( method = method, @@ -350,17 +244,38 @@ class And : TsMethodTestRunner() { // if (a) return 2 // if ((a != a) && b) return 3.0 // if ((a != a) && !b) return 4.0 - // if (b) return 3 - // return 4 + // if (b) return 5 + // return 6 // } // + val prog = program { + assign(local("a"), param(0)) + assign(local("b"), param(1)) + assign(local("this"), thisRef()) + ifStmt(and(local("a"), local("b"))) { + ret(const(1.0)) + } + ifStmt(local("a")) { + ret(const(2.0)) + } + ifStmt(and(neq(local("a"), local("a")), local("b"))) { + ret(const(3.0)) + } + ifStmt(and(neq(local("a"), local("a")), not(local("b")))) { + ret(const(4.0)) + } + ifStmt(local("b")) { + ret(const(5.0)) + } + ret(const(6.0)) + } + val blockCfg = prog.toBlockCfg() + val methodParameters = listOf( EtsMethodParameter(0, "a", EtsNumberType), EtsMethodParameter(1, "b", EtsBooleanType), ) - val locals = mutableListOf() - val method = EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = classSignature, @@ -368,67 +283,11 @@ class And : TsMethodTestRunner() { parameters = methodParameters, returnType = EtsNumberType, ), - locals = locals, ) - val statements = mutableListOf() - val successorMap = mutableMapOf>() - val loc = { EtsInstLocation(method, statements.size) } - - val localA = methodParameters[0].let { param -> - EtsLocal(param.name, param.type) - } - val localB = methodParameters[1].let { param -> - EtsLocal(param.name, param.type) - } - val localThis = EtsLocal("this", EtsClassType(classSignature)) + method.enclosingClass = scene.projectClasses.first { it.name == DEFAULT_ARK_CLASS_NAME } - val assA = EtsAssignStmt(loc(), localA, methodParameters[0].toRef()).also { statements += it } - val assB = EtsAssignStmt(loc(), localB, methodParameters[1].toRef()).also { statements += it } - val assThis = EtsAssignStmt(loc(), localThis, EtsThis(EtsClassType(classSignature))).also { statements += it } - - // %0 := a && b - val local0 = EtsLocal("%0", EtsUnknownType) - val ass0 = EtsAssignStmt(loc(), local0, EtsAndExpr(EtsUnknownType, localA, localB)).also { statements += it } - val if0 = EtsIfStmt(loc(), local0).also { statements += it } - val ret1 = EtsReturnStmt(loc(), EtsNumberConstant(1.0)).also { statements += it } - val ifA = EtsIfStmt(loc(), localA).also { statements += it } - val ret2 = EtsReturnStmt(loc(), EtsNumberConstant(2.0)).also { statements += it } - // %1 := (a != a) - val local1 = EtsLocal("%1", EtsUnknownType) - val ass1 = EtsAssignStmt(loc(), local1, EtsNotEqExpr(localA, localA)).also { statements += it } - // %2 := %1 && b == (a != a) && b - val local2 = EtsLocal("%2", EtsUnknownType) - val ass2 = EtsAssignStmt(loc(), local2, EtsAndExpr(EtsUnknownType, local1, localB)).also { statements += it } - val if2 = EtsIfStmt(loc(), local2).also { statements += it } - val ret3 = EtsReturnStmt(loc(), EtsNumberConstant(3.0)).also { statements += it } - val if1 = EtsIfStmt(loc(), local1).also { statements += it } - val ret4 = EtsReturnStmt(loc(), EtsNumberConstant(4.0)).also { statements += it } - val ifB = EtsIfStmt(loc(), localB).also { statements += it } - val ret5 = EtsReturnStmt(loc(), EtsNumberConstant(5.0)).also { statements += it } - val ret6 = EtsReturnStmt(loc(), EtsNumberConstant(6.0)).also { statements += it } - - // Note: for if-statements, successors must be (falseBranch, trueBranch) !!! - successorMap[assA] = listOf(assB) - successorMap[assB] = listOf(assThis) - successorMap[assThis] = listOf(ass0) - successorMap[ass0] = listOf(if0) - successorMap[if0] = listOf(ifA, ret1) - successorMap[ifA] = listOf(ass1, ret2) - successorMap[ass1] = listOf(ass2) - successorMap[ass2] = listOf(if2) - successorMap[if2] = listOf(if1, ret3) - successorMap[if1] = listOf(ifB, ret4) - successorMap[ifB] = listOf(ret6, ret5) - - successorMap[ret1] = emptyList() - successorMap[ret2] = emptyList() - successorMap[ret3] = emptyList() - successorMap[ret4] = emptyList() - successorMap[ret5] = emptyList() - successorMap[ret6] = emptyList() - - method._cfg = EtsCfg(statements, successorMap) - locals += method.getLocals() + val etsBlockCfg = blockCfg.toEtsBlockCfg(method) + method._cfg = etsBlockCfg discoverProperties( method = method, diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt index acdb983baf..142fa0b79a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Arrays.kt @@ -1,10 +1,12 @@ package org.usvm.samples import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner +@Disabled("Arrays are not fully supported, tests are unstable on CI") class Arrays : TsMethodTestRunner() { private val className = this::class.simpleName!! diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt index cd0327f0a6..c2e0e4eead 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt @@ -27,7 +27,7 @@ class Call : TsMethodTestRunner() { method = method, { n, r -> n.number.isNaN() && r.number == 0.0 }, { n, r -> n.number < 0.0 && r.number == -1.0 }, - { n, r -> n.number > 10.0 && r.number == -2.0 }, + { n, r -> n.number > 10.0 && r.number == -100.0 }, { n, r -> n.number == 0.0 && r.number == 1.0 }, { n, r -> n.number == 1.0 && r.number == 1.0 }, { n, r -> n.number > 0 && n.number != 1.0 && n.number <= 10.0 && fib(n.number) == r.number }, @@ -41,7 +41,7 @@ class Call : TsMethodTestRunner() { fun fib(n: Double): Double { if (n.isNaN()) return 0.0 if (n < 0) return -1.0 - if (n > 10) return -2.0 + if (n > 10) return -100.0 if (n == 0.0) return 1.0 if (n == 1.0) return 1.0 return fib(n - 1.0) + fib(n - 2.0) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt index 5a22d67ac6..b7eaea3952 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Or.kt @@ -1,8 +1,5 @@ package org.usvm.samples -import org.jacodb.ets.base.DEFAULT_ARK_CLASS_NAME -import org.jacodb.ets.base.EtsLocal -import org.jacodb.ets.base.EtsNumberType import org.jacodb.ets.dsl.const import org.jacodb.ets.dsl.eq import org.jacodb.ets.dsl.local @@ -12,14 +9,14 @@ import org.jacodb.ets.dsl.param import org.jacodb.ets.dsl.program import org.jacodb.ets.dsl.thisRef import org.jacodb.ets.dsl.toBlockCfg -import org.jacodb.ets.graph.linearize -import org.jacodb.ets.graph.toEtsBlockCfg import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.getLocals +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.toEtsBlockCfg import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner @@ -110,7 +107,6 @@ class Or : TsMethodTestRunner() { println("Program:\n${prog.toText()}") val blockCfg = prog.toBlockCfg() - val locals = mutableListOf() val method = EtsMethodImpl( signature = EtsMethodSignature( enclosingClass = classSignature, @@ -121,15 +117,11 @@ class Or : TsMethodTestRunner() { ), returnType = EtsNumberType, ), - locals = locals, ) + method.enclosingClass = scene.projectClasses.first { it.name == DEFAULT_ARK_CLASS_NAME } val etsBlockCfg = blockCfg.toEtsBlockCfg(method) - val etsCfg = etsBlockCfg.linearize() - - method._cfg = etsCfg - locals.clear() - locals += method.getLocals() + method._cfg = etsBlockCfg discoverProperties( method = method, diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticFields.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticFields.kt index c507346ce6..680557cf87 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/StaticFields.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/StaticFields.kt @@ -6,11 +6,12 @@ import org.junit.jupiter.api.Test import org.usvm.api.TsValue import org.usvm.util.TsMethodTestRunner +@Disabled("Statics are not fully supported, yet") class StaticFields : TsMethodTestRunner() { private val className = this::class.simpleName!! - override val scene: EtsScene = loadSampleScene(className, useArkAnalyzerTypeInference = true) + override val scene: EtsScene = loadSampleScene(className) @Test fun `test static access get`() { @@ -24,9 +25,9 @@ class StaticFields : TsMethodTestRunner() { @Test fun `test static default value`() { val method = getMethod("StaticDefault", "getValue") - discoverProperties( + discoverProperties( method = method, - { r -> r.number == 0.0 }, + { r -> r == TsValue.TsUndefined }, ) } @@ -112,7 +113,7 @@ class StaticFields : TsMethodTestRunner() { method = method, { r -> (r.properties["enabled"] as TsValue.TsBoolean).value == true && - (r.properties["count"] as TsValue.TsNumber).number == 2.0 + (r.properties["count"] as TsValue.TsNumber).number == 15.0 }, ) } @@ -122,7 +123,7 @@ class StaticFields : TsMethodTestRunner() { val method = getMethod("StaticAccess", "calculateSum") discoverProperties( method = method, - { r -> r.number == 3.0 }, + { r -> r.number == 15.0 }, ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt b/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt index 9bb0f46989..0866a3a85a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/ObjectClass.kt @@ -1,27 +1,17 @@ package org.usvm.util -import org.jacodb.ets.base.CONSTRUCTOR_NAME -import org.jacodb.ets.base.EtsClassType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFileSignature -import org.jacodb.ets.model.EtsMethodImpl -import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.utils.createConstructor fun createObjectClass(): EtsClass { - val cls = EtsClassSignature("Object", EtsFileSignature.DEFAULT) + val cls = EtsClassSignature("Object", EtsFileSignature.UNKNOWN) + val ctor = createConstructor(cls) return EtsClassImpl( signature = cls, fields = emptyList(), - methods = emptyList(), - ctor = EtsMethodImpl( - EtsMethodSignature( - enclosingClass = cls, - name = CONSTRUCTOR_NAME, - parameters = emptyList(), - returnType = EtsClassType(cls), - ) - ), + methods = listOf(ctor), ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 499e96eac6..7b1c9a2bca 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -1,19 +1,19 @@ package org.usvm.util -import org.jacodb.ets.base.EtsAnyType -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnknownType +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.TestInstance import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS @@ -188,7 +188,7 @@ abstract class TsMethodTestRunner : TestRunner { // TODO incorrect - val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT) + val signature = EtsClassSignature(it.toString(), EtsFileSignature.UNKNOWN) EtsClassType(signature) } @@ -206,7 +206,7 @@ abstract class TsMethodTestRunner : TestRunner { // TODO incorrect - val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT) + val signature = EtsClassSignature("Exception", EtsFileSignature.UNKNOWN) EtsClassType(signature) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index f96afcfa01..37a21388c8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -2,25 +2,25 @@ package org.usvm.util import io.ksmt.expr.KBitVec32Value import io.ksmt.utils.asExpr -import org.jacodb.ets.base.EtsArrayType -import org.jacodb.ets.base.EtsBooleanType -import org.jacodb.ets.base.EtsClassType -import org.jacodb.ets.base.EtsLiteralType -import org.jacodb.ets.base.EtsNeverType -import org.jacodb.ets.base.EtsNullType -import org.jacodb.ets.base.EtsNumberType -import org.jacodb.ets.base.EtsPrimitiveType -import org.jacodb.ets.base.EtsRefType -import org.jacodb.ets.base.EtsStringType -import org.jacodb.ets.base.EtsType -import org.jacodb.ets.base.EtsUnclearRefType -import org.jacodb.ets.base.EtsUndefinedType -import org.jacodb.ets.base.EtsUnknownType -import org.jacodb.ets.base.EtsVoidType -import org.jacodb.ets.base.UNKNOWN_CLASS_NAME +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldImpl +import org.jacodb.ets.model.EtsLiteralType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNeverType +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsPrimitiveType +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.model.EtsVoidType +import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr @@ -187,7 +187,7 @@ open class TsTestStateResolver( return when (type) { // TODO add better support is EtsUnclearRefType -> { - val cls = ctx.scene.projectAndSdkClasses.single { it.name == type.name } + val cls = ctx.scene.projectAndSdkClasses.single { it.name == type.typeName } resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, cls.type) } @@ -236,7 +236,7 @@ open class TsTestStateResolver( fun resolveThisInstance(): TsValue? { val parametersCount = method.parameters.size val ref = mkRegisterStackLValue(ctx.addressSort, parametersCount) // TODO check for statics - val type = EtsClassType(method.enclosingClass) + val type = EtsClassType(method.signature.enclosingClass) return resolveLValue(ref, type) } diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts index e2ff4fbfe0..13dce52560 100644 --- a/usvm-ts/src/test/resources/samples/Call.ts +++ b/usvm-ts/src/test/resources/samples/Call.ts @@ -13,7 +13,7 @@ class Call { fib(n: number): number { if (n != n) return 0 if (n < 0) return -1 - if (n > 10) return -2 + if (n > 10) return -100 if (n == 0) return 1 if (n == 1) return 1 return this.fib(n - 1) + this.fib(n - 2) diff --git a/usvm-ts/src/test/resources/samples/FieldAccess.ts b/usvm-ts/src/test/resources/samples/FieldAccess.ts index f4acd63777..d65eff3762 100644 --- a/usvm-ts/src/test/resources/samples/FieldAccess.ts +++ b/usvm-ts/src/test/resources/samples/FieldAccess.ts @@ -54,7 +54,7 @@ class FieldAccess { return this.createObject().x; } - private createObject(): {x: number} { + private createObject(): { x: number } { return {x: 42}; } diff --git a/usvm-ts/src/test/resources/samples/StaticFields.ts b/usvm-ts/src/test/resources/samples/StaticFields.ts index 2226d608e0..4589f1786d 100644 --- a/usvm-ts/src/test/resources/samples/StaticFields.ts +++ b/usvm-ts/src/test/resources/samples/StaticFields.ts @@ -5,7 +5,7 @@ class StaticNumber { static value = 10; - getValue(): number { + static getValue(): number { return this.value; } } @@ -14,7 +14,7 @@ class StaticNumber { class StaticDefault { static value: number; - getValue(): number { + static getValue(): number { return this.value; } } @@ -38,7 +38,7 @@ class StaticBase { class StaticDerived extends StaticBase { static f = 42; - getId(): number { + static getId(): number { return this.id + this.f; } } @@ -59,7 +59,7 @@ class StaticChild extends StaticParent { return StaticChild.id; } - getId(): number { + static getId(): number { return this.id; } } @@ -97,12 +97,16 @@ class StaticNull { // Test: Object static operations class StaticObject { - static config: Config = {enabled: false, count: 0}; + static config: Config = {enabled: true, count: 10}; static modifyAndGet(): Config { + this.config.increment(); + this.config.increment(); this.config.increment(); this.config.flip(); this.config.increment(); + this.config.increment(); + this.config.flip(); return this.config; } } @@ -122,8 +126,8 @@ class Config { // Test: Field swapping class StaticAccess { - static a = 1; - static b = 2; + static a = 5; + static b = 10; static calculateSum(): number { return this.a + this.b; From eb114fc347ac36fdd38ffe4ca37e8ef54830db7c Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 15:52:28 +0300 Subject: [PATCH 2/6] Cleanup --- usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt | 2 -- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 1 - .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 1 - .../main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt | 1 - usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | 1 - usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt | 1 - usvm-ts/src/test/kotlin/org/usvm/samples/And.kt | 1 - usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 3 --- 8 files changed, 11 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 54537b9226..ebe5db9927 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -9,7 +9,6 @@ import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType @@ -30,7 +29,6 @@ import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.FakeType import org.usvm.types.UTypeStream -import org.usvm.types.single import org.usvm.util.mkFieldLValue import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 76793125b6..7caf5eaf6b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -12,7 +12,6 @@ import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.FakeType -import org.usvm.types.single import org.usvm.util.boolToFp fun TsContext.mkTruthyExpr( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 56b7a0adec..77c47f8c96 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -97,7 +97,6 @@ import org.usvm.machine.types.FakeType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort -import org.usvm.types.single import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 048d18cbf9..87a34faf7c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -17,7 +17,6 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.FakeType import org.usvm.machine.types.iteWriteIntoFakeObject -import org.usvm.types.single import org.usvm.util.boolToFp sealed interface TsBinaryOperator { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 892b49c0e4..60a48b15a7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -13,7 +13,6 @@ import org.usvm.UConcreteHeapRef import org.usvm.USort import org.usvm.UState import org.usvm.api.targets.TsTarget -import org.usvm.collections.immutable.getOrPut import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.collections.immutable.persistentHashMapOf diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index cb26e56330..c721f04c01 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -15,7 +15,6 @@ import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.memory.ULValue -import org.usvm.types.single fun TsContext.mkFakeValue( scope: TsStepScope, diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt index 130b2dbd27..ef1ae692b6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/And.kt @@ -15,7 +15,6 @@ import org.jacodb.ets.model.EtsMethodImpl import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsNumberType -import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.toEtsBlockCfg diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 37a21388c8..0022a4d81c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -33,7 +33,6 @@ import org.usvm.api.TsValue import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort -import org.usvm.machine.expr.extractBool import org.usvm.machine.expr.extractDouble import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -43,8 +42,6 @@ import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.mkSizeExpr import org.usvm.model.UModelBase -import org.usvm.types.first -import org.usvm.types.single class TsTestResolver { fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) { From f23e37bd046a20ba4b2c6652f54535c70b566ac4 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 15:55:02 +0300 Subject: [PATCH 3/6] Split long lines --- .../dataflow/ts/test/EtsTypeInferenceTest.kt | 38 ++++++++++++++----- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt index 866eb40e7b..57170b702e 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt @@ -22,17 +22,17 @@ import kotlinx.coroutines.runInterruptible import kotlinx.coroutines.withTimeout import kotlinx.serialization.SerializationException import mu.KotlinLogging -import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringConstant import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnknownType -import org.jacodb.ets.dto.EtsFileDto -import org.jacodb.ets.dto.toEtsFile -import org.jacodb.ets.model.EtsFile -import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.getLocals import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Disabled @@ -392,7 +392,11 @@ class EtsTypeInferenceTest { val result = manager.analyze(listOf(entrypoint), doAddKnownTypes = false) val inferredTypes = result.inferredTypes[inferMethod] - ?: error("No inferred types for method ${inferMethod.signature.enclosingClass.name}::${inferMethod.name}") + ?: error( + "No inferred types for method ${ + inferMethod.signature.enclosingClass.name + }::${inferMethod.name}" + ) for ((position, expected) in expectedTypeString.sortedByBase()) { val inferred = inferredTypes[position] @@ -493,16 +497,30 @@ class EtsTypeInferenceTest { logger.info { buildString { appendLine("Inferred return types: ${result.inferredReturnType.size}") - for ((method, returnType) in result.inferredReturnType.sortedBy { it.key.toString() }) { - appendLine("${method.signature.enclosingClass.name}::${method.name}: ${returnType.toStringLimited()}") + val res = result.inferredReturnType.sortedBy { it.key.toString() } + for ((method, returnType) in res) { + appendLine( + "${ + method.signature.enclosingClass.name + }::${ + method.name + }: ${ + returnType.toStringLimited() + }" + ) } } } logger.info { buildString { appendLine("Inferred combined this types: ${result.inferredCombinedThisType.size}") - for ((clazz, thisType) in result.inferredCombinedThisType.sortedBy { it.key.toString() }) { - appendLine("${clazz.name} in ${clazz.file}: ${thisType.toStringLimited()}") + val res = result.inferredCombinedThisType.sortedBy { it.key.toString() } + for ((clazz, thisType) in res) { + appendLine( + "${clazz.name} in ${clazz.file}: ${ + thisType.toStringLimited() + }" + ) } } } From 48c4d8577a0e5956e547e9c8a5a7e9f68573dff8 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 15:57:08 +0300 Subject: [PATCH 4/6] Format --- .../dataflow/ts/graph/EtsApplicationGraph.kt | 1 - .../dataflow/ts/infer/dto/EtsValueToDto.kt | 1 - .../verify/collectors/StmtSummaryCollector.kt | 1 - .../dataflow/ts/test/EtsProjectAnalysisTest.kt | 2 +- .../dataflow/ts/test/EtsTypeInferenceTest.kt | 18 +++++++++++++++--- .../ts/test/utils/ClassMatcherStatistics.kt | 4 ++-- .../ts/test/utils/PerformanceReport.kt | 1 - .../ts/test/utils/TypeInferenceStatistics.kt | 4 ++-- 8 files changed, 20 insertions(+), 12 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt index 49e37a1d65..7dc2021bbf 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt @@ -25,7 +25,6 @@ import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsNewExpr -import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.utils.CONSTRUCTOR_NAME diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt index da690dc084..2d9dd20d8b 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt @@ -41,7 +41,6 @@ import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStringConstant import org.jacodb.ets.model.EtsThis import org.jacodb.ets.model.EtsUndefinedConstant -import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue fun EtsValue.toDto(): ValueDto = accept(EtsValueToDto) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt index b53fcb1ba6..48787b7107 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt +++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt @@ -28,7 +28,6 @@ import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsInstanceOfExpr import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsPtrCallExpr diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt index 6c25443aea..84d9f04225 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsProjectAnalysisTest.kt @@ -17,10 +17,10 @@ package org.usvm.dataflow.ts.test import mu.KotlinLogging -import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt import org.junit.jupiter.api.Test import org.junit.jupiter.api.condition.EnabledIf import org.usvm.dataflow.ifds.SingletonUnit diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt index 57170b702e..6cbb19c686 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeInferenceTest.kt @@ -496,7 +496,11 @@ class EtsTypeInferenceTest { } logger.info { buildString { - appendLine("Inferred return types: ${result.inferredReturnType.size}") + appendLine( + "Inferred return types: ${ + result.inferredReturnType.size + }" + ) val res = result.inferredReturnType.sortedBy { it.key.toString() } for ((method, returnType) in res) { appendLine( @@ -513,7 +517,11 @@ class EtsTypeInferenceTest { } logger.info { buildString { - appendLine("Inferred combined this types: ${result.inferredCombinedThisType.size}") + appendLine( + "Inferred combined this types: ${ + result.inferredCombinedThisType.size + }" + ) val res = result.inferredCombinedThisType.sortedBy { it.key.toString() } for ((clazz, thisType) in res) { appendLine( @@ -578,7 +586,11 @@ class EtsTypeInferenceTest { logger.info { buildString { - appendLine("Local type matching for ${method.signature.enclosingClass.name}::${method.name}:") + appendLine( + "Local type matching for ${ + method.signature.enclosingClass.name + }::${method.name}:" + ) appendLine(" Matched normal: $numMatchedNormal") appendLine(" Matched unknown: $numMatchedUnknown") appendLine(" Mismatched normal: $numMismatchedNormal") diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt index e1f7801560..1a62f3b7aa 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/ClassMatcherStatistics.kt @@ -22,15 +22,15 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnknownType -import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsScene import org.usvm.dataflow.ts.graph.EtsApplicationGraph import org.usvm.dataflow.ts.infer.AccessPathBase import org.usvm.dataflow.ts.infer.EtsTypeFact diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt index b45207c4df..37a73c3df9 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/PerformanceReport.kt @@ -21,7 +21,6 @@ import kotlin.time.Duration import kotlin.time.DurationUnit import kotlin.time.measureTimedValue - data class PerformanceReport( val projectId: String, val maxTime: Duration, diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt index 6fdd5f66fd..84d7fa0356 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt @@ -22,16 +22,16 @@ import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsParameterRef import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType -import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME From c3c2524b5d00dbc26199459bc5b2576111b0a976 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 15:58:17 +0300 Subject: [PATCH 5/6] Split long lines --- .../dataflow/ts/test/utils/TypeInferenceStatistics.kt | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt index 84d7fa0356..0307889ad9 100644 --- a/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt +++ b/usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/TypeInferenceStatistics.kt @@ -501,8 +501,14 @@ class TypeInferenceStatistics { appendLine("No types inferred for methods:") noTypesInferred - .filterNot { it.name == INSTANCE_INIT_METHOD_NAME || it.name == STATIC_INIT_METHOD_NAME } - .filterNot { it.name == DEFAULT_ARK_METHOD_NAME && it.signature.enclosingClass.name == DEFAULT_ARK_CLASS_NAME } + .filterNot { + it.name == INSTANCE_INIT_METHOD_NAME + || it.name == STATIC_INIT_METHOD_NAME + } + .filterNot { + it.name == DEFAULT_ARK_METHOD_NAME + && it.signature.enclosingClass.name == DEFAULT_ARK_CLASS_NAME + } .sortedBy { it.signature.toString() } .forEach { appendLine(it) From 8dcef8929d2850c0cb3069bd5f3e59a136633dc3 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 17 Apr 2025 16:08:48 +0300 Subject: [PATCH 6/6] Fix rebase --- .../main/kotlin/org/usvm/machine/TsContext.kt | 1 + .../kotlin/org/usvm/machine/expr/ExprUtil.kt | 1 + .../org/usvm/machine/expr/TsExprResolver.kt | 5 +---- .../usvm/machine/operator/TsBinaryOperator.kt | 18 ++++++++---------- .../kotlin/org/usvm/machine/state/TsState.kt | 1 + .../org/usvm/machine/types/FakeExprUtil.kt | 1 + .../kotlin/org/usvm/util/TsTestResolver.kt | 3 +++ 7 files changed, 16 insertions(+), 14 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index ebe5db9927..ce40dcf902 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -29,6 +29,7 @@ import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.FakeType import org.usvm.types.UTypeStream +import org.usvm.types.single import org.usvm.util.mkFieldLValue import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 7caf5eaf6b..76793125b6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -12,6 +12,7 @@ import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.FakeType +import org.usvm.types.single import org.usvm.util.boolToFp fun TsContext.mkTruthyExpr( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 77c47f8c96..8b5e813e0d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -93,7 +93,6 @@ import org.usvm.machine.state.TsState import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount -import org.usvm.machine.types.FakeType import org.usvm.machine.types.mkFakeValue import org.usvm.memory.ULValue import org.usvm.sizeSort @@ -665,9 +664,7 @@ class TsExprResolver( // TODO: handle "length" property for arrays inside fake objects if (value.field.name == "length" && instanceRef.isFakeObject()) { - val fakeType = scope.calcOnState { - memory.types.getTypeStream(instanceRef).single() as FakeType - } + val fakeType = instanceRef.getFakeType(scope) if (fakeType.refTypeExpr.isTrue) { val refLValue = getIntermediateRefLValue(instanceRef.address) val obj = scope.calcOnState { memory.read(refLValue) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 87a34faf7c..39868d00be 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -8,14 +8,12 @@ import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.USort import org.usvm.api.makeSymbolicPrimitive -import org.usvm.api.typeStreamOf import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUndefinedSort import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint -import org.usvm.machine.types.FakeType import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.boolToFp @@ -113,8 +111,8 @@ sealed interface TsBinaryOperator { when { lhs.isFakeObject() && rhs.isFakeObject() -> { - val lhsType = memory.typeStreamOf(lhs).single() as FakeType - val rhsType = memory.typeStreamOf(rhs).single() as FakeType + val lhsType = lhs.getFakeType(scope) + val rhsType = rhs.getFakeType(scope) scope.assert( mkAnd( @@ -167,7 +165,7 @@ sealed interface TsBinaryOperator { } lhs.isFakeObject() -> { - val lhsType = memory.typeStreamOf(lhs).single() as FakeType + val lhsType = lhs.getFakeType(scope) scope.assert(lhsType.mkExactlyOneTypeConstraint(ctx)) @@ -234,7 +232,7 @@ sealed interface TsBinaryOperator { } rhs.isFakeObject() -> { - val rhsType = memory.typeStreamOf(rhs).single() as FakeType + val rhsType = rhs.getFakeType(scope) scope.assert(rhsType.mkExactlyOneTypeConstraint(ctx)) @@ -428,8 +426,8 @@ sealed interface TsBinaryOperator { return scope.calcOnState { when { lhs.isFakeObject() && rhs.isFakeObject() -> { - val lhsType = memory.typeStreamOf(lhs).single() as FakeType - val rhsType = memory.typeStreamOf(rhs).single() as FakeType + val lhsType = lhs.getFakeType(scope) + val rhsType = rhs.getFakeType(scope) scope.assert( mkAnd( @@ -442,7 +440,7 @@ sealed interface TsBinaryOperator { } lhs.isFakeObject() -> { - val lhsType = memory.typeStreamOf(lhs).single() as FakeType + val lhsType = lhs.getFakeType(scope) val condition = when (rhs.sort) { boolSort -> lhsType.boolTypeExpr @@ -456,7 +454,7 @@ sealed interface TsBinaryOperator { } rhs.isFakeObject() -> { - val rhsType = memory.typeStreamOf(rhs).single() as FakeType + val rhsType = rhs.getFakeType(scope) scope.assert(rhsType.mkExactlyOneTypeConstraint(ctx)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 60a48b15a7..892b49c0e4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -13,6 +13,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.USort import org.usvm.UState import org.usvm.api.targets.TsTarget +import org.usvm.collections.immutable.getOrPut import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.collections.immutable.persistentHashMapOf diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index c721f04c01..cb26e56330 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -15,6 +15,7 @@ import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.memory.ULValue +import org.usvm.types.single fun TsContext.mkFakeValue( scope: TsStepScope, diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 0022a4d81c..37a21388c8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -33,6 +33,7 @@ import org.usvm.api.TsValue import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.extractBool import org.usvm.machine.expr.extractDouble import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -42,6 +43,8 @@ import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.URegisterStackLValue import org.usvm.mkSizeExpr import org.usvm.model.UModelBase +import org.usvm.types.first +import org.usvm.types.single class TsTestResolver { fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) {