Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update jacodb and refine dataflow accordingly #196

Merged
merged 10 commits into from
Jul 18, 2024
Merged

Conversation

Lipen
Copy link
Collaborator

@Lipen Lipen commented Jul 17, 2024

This PR updates jacodb to the latest neo branch version and also fixes/improves dataflow accordingly to API changes in jacodb.

Also a major change is that Traits now contain only functions. The reason for this is that functions look much more consistent than a combination of extension properties and functions.

@Lipen Lipen requested a review from CaelmBleidd July 17, 2024 15:51
@Lipen
Copy link
Collaborator Author

Lipen commented Jul 17, 2024

@CaelmBleidd should we also rename usvm-jvm-dataflow to a more logical usvm-dataflow-jvm (JVM-specific dataflow) in this PR, since we are going to add usvm-dataflow-ts in the future? Or we need a separate PR for this?

Copy link
Collaborator

@Saloed Saloed left a comment

Choose a reason for hiding this comment

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

Initialization failed in many tests:

JcCallGraphStatisticsTests > initializationError FAILED
    java.lang.IllegalStateException at JcCallGraphStatisticsTests.kt:14

@Lipen
Copy link
Collaborator Author

Lipen commented Jul 17, 2024

This extension requires `Usages` feature to be installed
java.lang.IllegalStateException: This extension requires `Usages` feature to be installed
	at org.jacodb.impl.features.JcUsages.usagesExt(UsagesExtension.kt:140)
	at org.usvm.machine.JcApplicationGraph$jcApplicationGraph$1.invokeSuspend(JcApplicationGraph.kt:21)
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33)
	at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106)
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284)
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85)
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59)
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source)
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38)
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source)
	at org.usvm.machine.JcApplicationGraph.<init>(JcApplicationGraph.kt:21)
	at org.usvm.machine.JcCallGraphStatisticsTests.<init>(JcCallGraphStatisticsTests.kt:14)
...
suspend fun JcClasspath.usagesExt(): SyncUsagesExtension {
    if (!db.isInstalled(Usages)) {
        throw IllegalStateException("This extension requires `Usages` feature to be installed")
    }
    return SyncUsagesExtension(hierarchyExt(), this)
}

@Lipen
Copy link
Collaborator Author

Lipen commented Jul 17, 2024

Seems like cp: JcClasspath that is passed to JcApplicationGraphImpl in tests is actually from the JacoDBContainer, where only InMemoryHierarchy feature is installed. I've added Usages feature here, tests pass locally (except the approximation tests, as expected), but probably @Saloed have to double-check whether it is correct.

Remove Usages in JacoDBContainer. Use SyncUsagesExtension directly
@Lipen Lipen merged commit 67d0262 into main Jul 18, 2024
1 check failed
@Lipen Lipen deleted the lipen/update-dataflow branch July 18, 2024 09:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants