Skip to content

Usvm competitions 2024: jacodb persistence #2703

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

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion gradle.properties
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ jakartaVersion=3.1.0
jacoDbVersion=1.4.1
# TODO left outdated here to avoid exceeding GitHub packages drive space,
# TODO run `gradle publishToMavenLocal -Pversion={usvmVersion}` locally in usvm project and update {usvmVersion} locally
usvmVersion=comp-231128-22
usvmVersion=comp-231129-22

# use latest Java 8 compaitable Spring and Spring Boot versions
springVersion=5.3.28
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import org.jacodb.approximation.Approximations
import org.jacodb.impl.features.InMemoryHierarchy
import org.objectweb.asm.Type
import org.usvm.PathSelectionStrategy
import org.usvm.PathSelectorFairnessStrategy
import org.usvm.SolverType
import org.usvm.UMachineOptions
import org.usvm.api.targets.JcTarget
Expand Down Expand Up @@ -85,12 +86,14 @@ fun runUsvmGeneration(

val jcContainer by lazy {
JcContainer(
usePersistence = true,
classpath = classpathFiles,
machineOptions = UMachineOptions(
// TODO usvm-sbft: if we have less than CONTEST_TEST_EXECUTION_TIMEOUT time left, we should try execute
// with smaller timeout, but instrumentation currently doesn't allow to change timeout for individual runs
timeout = generationTimeoutMillisWithoutCodegen.milliseconds - CONTEST_TEST_EXECUTION_TIMEOUT,
pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
pathSelectorFairnessStrategy = PathSelectorFairnessStrategy.COMPLETELY_FAIR,
solverType = SolverType.YICES,
)
) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ private val logger = KotlinLogging.logger {}

// TODO usvm-sbft-refactoring: copied from `usvm/usvm-jvm/test`, extract this class back to USVM project
class JcContainer private constructor(
usePersistence: Boolean,
classpath: List<File>,
machineOptions: UMachineOptions,
builder: JcSettings.() -> Unit,
Expand All @@ -29,8 +30,27 @@ class JcContainer private constructor(
val runner: UTestConcreteExecutor

init {
val cpPath = classpath.map { it.absolutePath }.sorted()

/**
* Persist jacodb cp to achieve:
* 1. Faster concrete executor initialization
* 2. Faster analysis for classes from the same cp
* */
val persistenceLocation = if (usePersistence) {
"jcdb-persistence-${cpPath.hashCode()}"
} else {
null
}

val (db, cp) = runBlocking {
val db = jacodb(builder)
val db = jacodb {
builder()

if (persistenceLocation != null) {
persistent(location = persistenceLocation, clearOnStart = false)
}
}
val cp = db.classpathWithApproximations(classpath, listOf(UnknownClasses))
db to cp
}
Expand All @@ -39,8 +59,9 @@ class JcContainer private constructor(
this.machine = JcMachine(cp, machineOptions)
this.runner = UTestConcreteExecutor(
JcRuntimeTraceInstrumenterFactory::class,
classpath.map { it.absolutePath },
cpPath,
cp,
persistenceLocation,
CONTEST_TEST_EXECUTION_TIMEOUT
)
runBlocking {
Expand All @@ -61,6 +82,7 @@ class JcContainer private constructor(
private val cache = HashMap<Pair<List<File>, UMachineOptions>, JcContainer>()

operator fun invoke(
usePersistence: Boolean,
classpath: List<File>,
machineOptions: UMachineOptions,
builder: JcSettings.() -> Unit,
Expand All @@ -70,7 +92,7 @@ class JcContainer private constructor(
// TODO usvm-sbft: right now max cache size is 1, do we need to increase it?
logger.info { "JcContainer cache miss" }
close()
JcContainer(classpath, machineOptions, builder).also { cache[cacheKey] = it }
JcContainer(usePersistence, classpath, machineOptions, builder).also { cache[cacheKey] = it }
}
}

Expand Down