CERT-9827: Rerun leaf timeouts with random seeds (#8188)

fcf493b367d992fa19a0aeaa1971a98f61e531d2

Author: nafur

lib/Shared/src/main/kotlin/config/Config.kt

@@ -3005,6 +3005,24 @@ object Config {
                 }"
         }
 
+        val retryOnLeafTimeout: ConfigType.BooleanCmdLine = object : ConfigType.BooleanCmdLine(
+            false,
+            Option(
+                "smt_retryOnLeafTimeout",
+                true,
+                "Reruns a timeouting leaf with a broader portfolio of solvers."
+            )
+        ), TransformationAgnosticConfig {}
+
+        val retryOnLeafTimeoutSolvers: ConfigType.SolverProgramCmdLine = object : ConfigType.SolverProgramCmdLine(
+            AllCommonAvailableSolversWithClOptions.toTypedArray(),
+            Option(
+                "smt_retryOnLeafTimeoutSolvers",
+                true,
+                "Solvers used for a rerun on timeouting leafs."
+            )
+        ), TransformationAgnosticConfig {}
+
         val NumOfUnsatCores: ConfigType.IntCmdLine = object : ConfigType.IntCmdLine(
             1,
             Option(

src/main/kotlin/verifier/LExpVCStats.kt

@@ -164,7 +164,7 @@ data class ResplitStatistic(
 @Serializable
 data class SplitStatistic(
     /** The location of the split in the split tree.  -1 indicates a failed split */
-    val address: List<Int>,
+    val address: String,
     /** splitName exactly as it is in Split<CoreTACProgram>.name. Also referred to as vcName */
     val splitName: String,
     val finalResult: String? = null,

src/main/kotlin/verifier/TACVerifier.kt

@@ -50,6 +50,7 @@ import smtlibutils.statistics.LearnedClausesFilterStatistics
 import smtlibutils.statistics.PreExecutionStatistics
 import solver.ConfigStatistics
 import solver.SMTCounterexampleModel
+import solver.SolverChoice
 import solver.SolverResult
 import spec.cvlast.CVLCmd
 import spec.cvlast.CVLExpDeclaredSymbolsCollector
@@ -184,7 +185,7 @@ class TACVerifier private constructor(
     ) {
         updateSplitStatistics(
             SplitStatistic(
-                address = address.asIntList,
+                address = address.name(),
                 vcFeatures = listOf(),
                 solvingEvent = ResplitStatistic(resplitTime),
                 timeToSolveSinceJarStart = TimeSinceStart(),
@@ -209,7 +210,7 @@ class TACVerifier private constructor(
 
         val splitStats = SplitStatistic(
             splitName = vcName,
-            address = address.asIntList,
+            address = address.name(),
             finalResult = LExpVCStatsLogger.getResultStr(checkerResult.satResult),
             timeout = timeout,
             smtSolvingWallTime = smtSolvingWallTime,
@@ -623,7 +624,7 @@ class TACVerifier private constructor(
                 vcGenStopWatch = MilliTimeElapserStopWatch(timeStatsRecorder, vcGenTimeTag),
                 solverStopWatch,
                 autoConfig,
-                localSettings
+                ((subProblem as? SplitTree.NodeWithInfo<*>)?.info as? LocalSettings) ?: localSettings
             )
             val finalResult = verifierResult.finalResult
             subProblem.setRunInfo(finalResult, verifierResult.elapsedTimeSeconds.seconds, timeout)
@@ -671,6 +672,24 @@ class TACVerifier private constructor(
                         problemQueue += subProblem.split(subProblemTAC)
                     }
                     continue
+                } else if (Config.Smt.retryOnLeafTimeout.get() && (subProblem.address !is SplitAddress.Rerun)) {
+                    val sub = LazySubProgram(
+                        splitTree,
+                        SplitAddress.Rerun(subProblem.lazySub.address)
+                    )
+                    val alreadyTried = smtFormulaCheckerResult.subResultsFlattened
+                        .mapNotNull { it.solverInstanceInfo?.solverConfig }
+                    val settings = localSettings.copy(
+                        solverProgramChoice = SolverChoice(
+                            Config.Smt.retryOnLeafTimeoutSolvers.get()
+                                .filter { it.solverInfo.getOptionForRandomSeed(1).isNotEmpty() }
+                                .flatMap { listOf(1, 2, 3).map { seed -> it.copy(randomSeed = seed) } }
+                                .filter { it !in alreadyTried }
+                                .map { it.copy(canBeSkipped = { _,_ -> false }) }
+                        )
+                    )
+                    logger.info { "Timed out on leaf ${sub.name}, rerunning with random seeds" }
+                    problemQueue.add(splitTree.NodeWithInfo(sub, subProblem.sideScore, settings))
                 } else {
                     // we dump timeouting leaves.
                     smtFormulaCheckerResult.let { last ->

src/main/kotlin/verifier/autoconfig/AutoConfigManager.kt

@@ -75,11 +75,11 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * their parent is also UNSAT. The propagation is recursive.
      */
     private fun propagateUNSAT(address: SplitAddress): Unit = synchronized(splitStatAndSolverConfigLock) {
-        if (address.asIntList.toString() !in stats.splitStatistics) {
+        if (address.name() !in stats.splitStatistics) {
             warn("The split with the address $address should be first added to ${::stats.name} before we propagate its unsat result")
             return
         }
-        if (!stats.splitStatistics[address.asIntList.toString()]!!.isEventuallyUNSAT()) {
+        if (!stats.splitStatistics[address.name()]!!.isEventuallyUNSAT()) {
             warn("Trying to propagate an unregistered UNSAT result of the split $address")
             return
         }
@@ -90,10 +90,10 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         if (address !is SplitAddress.Block) {
             return
         }
-        val siblingAddressStr = address.sibling().toString()
+        val siblingAddressStr = address.sibling().name()
         if (stats.splitStatistics[siblingAddressStr]?.isEventuallyUNSAT() == true) {
             val parentAddress = address.parent
-            val parentAddressStr = parentAddress.toString()
+            val parentAddressStr = parentAddress?.name() ?: "null"
             if (parentAddressStr !in stats.splitStatistics) {
                 warn("The parent address $parentAddressStr is not registered in ${::stats.name}")
                 return
@@ -110,12 +110,12 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * Sets the [finalResult] and [solvers] of the stats of [address] based on the stats of [matchingUnsat].
      */
     private fun markMatchingUnsat(address: SplitAddress, matchingUnsat: BasicSplitStatistics) = synchronized(splitStatAndSolverConfigLock) {
-        if(address.asIntList.toString() !in stats.splitStatistics) {
+        if(address.name() !in stats.splitStatistics) {
             warn("Trying to mark an address UNSAT that is not in ${::stats.name}: $address")
             return
         }
-        stats.splitStatistics[address.asIntList.toString()] =
-            stats.splitStatistics[address.asIntList.toString()]!!.copy(
+        stats.splitStatistics[address.name()] =
+            stats.splitStatistics[address.name()]!!.copy(
                 finalResult = matchingUnsat.finalResult,
                 solvers = matchingUnsat.solvers
             )
@@ -126,27 +126,29 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * it gets computed and stored in [stats].
      */
     private fun getDigest(address: SplitAddress, prog: CoreTACProgram): String = synchronized(splitStatAndSolverConfigLock) {
-        require(address.asIntList.toString() in stats.splitStatistics) {
-            "Trying to store a digest for a split ${address.asIntList} that is not registered yet"
+        val addressName = address.name()
+        require(addressName in stats.splitStatistics) {
+            "Trying to store a digest for a split ${addressName} that is not registered yet"
         }
-        if (stats.splitStatistics[address.asIntList.toString()]!!.tacStats.digest == null) {
+        if (stats.splitStatistics[addressName]!!.tacStats.digest == null) {
             val digest = BasicTACStatistics.computeDigest(prog)
-            stats.splitStatistics[address.asIntList.toString()] =
-                stats.splitStatistics[address.asIntList.toString()]!!.let {
+            stats.splitStatistics[addressName] =
+                stats.splitStatistics[addressName]!!.let {
                     it.copy(tacStats = it.tacStats.copy(digest = digest))
                 }
         }
-        return stats.splitStatistics[address.asIntList.toString()]!!.tacStats.digest!!
+        return stats.splitStatistics[addressName]!!.tacStats.digest!!
     }
 
     /**
      * Register the given [subProblem] in [stats] (storing just address, split name, and basic TAC statistics).
      */
     fun registerSplit(address: SplitAddress, name: String, subProblemTAC: CoreTACProgram) = synchronized(splitStatAndSolverConfigLock) {
-        if (address.asIntList.toString() !in stats.splitStatistics.keys) {
-            info("registering split ${address.asIntList}")
-            stats.splitStatistics[address.asIntList.toString()] = BasicSplitStatistics(
-                address = address.asIntList.toString(),
+        val addressName = address.name()
+        if (addressName !in stats.splitStatistics.keys) {
+            info("registering split ${address.name()}")
+            stats.splitStatistics[addressName] = BasicSplitStatistics(
+                address = addressName,
                 splitName = name,
                 tacStats = BasicTACStatistics.fromCoreTACProgram(subProblemTAC, Config.AutoconfigUseDigests.get()),
             )
@@ -164,7 +166,7 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         timeoutForSubProblem: Duration,
         solvingDuration: Duration,
     ) = synchronized(splitStatAndSolverConfigLock) {
-        val address = splitAddress.asIntList.toString()
+        val address = splitAddress.name()
         info("registering ${verifierResult.finalResult} result for split $address.")
         if(address !in stats.splitStatistics) {
             warn("Trying to register results for an unregistered split $address.")
@@ -262,7 +264,7 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         val loadedMatches = loadedStats?.splitStatistics?.values?.filter { tacStats.match(it.tacStats) } ?: listOf()
         //Splits we have already solved in this CVT run and which are matching the current split.
         val newMatches: List<BasicSplitStatistics> = if (learnFromCurrent) {
-            val splitAddressStr = splitAddress.asIntList.toString()
+            val splitAddressStr = splitAddress.name()
             synchronized(splitStatAndSolverConfigLock) {
                 stats.splitStatistics.values.filter { tacStats.match(it.tacStats) && it.address != splitAddressStr }
             }

src/main/kotlin/verifier/splits/SplitAddress.kt

@@ -37,15 +37,15 @@ sealed interface SplitAddress : HasKSerializable {
     val parent: SplitAddress?
     val isRoot get() = parent == null
     val depth: Int get() = (parent?.depth ?: -1) + 1
-    val asIntList : List<Int>
-    fun name() = asIntList.joinToString("_") { it.toString() }
+    val asList : List<String>
+    fun name() = asList.joinToString("_")
 
     fun fullInfo(): String
 
     @KSerializable
     data object Root : SplitAddress {
         override val parent = null
-        override val asIntList = emptyList<Int>()
+        override val asList = emptyList<String>()
         override fun fullInfo() = "ROOT"
         override fun toString() = name()
     }
@@ -59,18 +59,25 @@ sealed interface SplitAddress : HasKSerializable {
         @KSerializable
         data class MustPass(override val parent: SplitAddress, override val pivot: NBId) : Block {
             override fun sibling() = DontPass(parent, pivot)
-            override val asIntList = parent.asIntList + 0
+            override val asList = parent.asList + "0"
             override fun toString() = name()
         }
 
         @KSerializable
         data class DontPass(override val parent: SplitAddress, override val pivot: NBId) : Block {
             override fun sibling() = MustPass(parent, pivot)
-            override val asIntList = parent.asIntList + 1
+            override val asList = parent.asList + "1"
             override fun toString() = name()
         }
     }
 
+    @KSerializable
+    data class Rerun(override val parent: SplitAddress) : SplitAddress {
+        override val asList = parent.asList + "R"
+        override fun toString() = name()
+        override fun fullInfo() = "${name()}[rerun]"
+    }
+
     @KSerializable
     data class Assumption(
         override val parent: SplitAddress,
@@ -101,7 +108,7 @@ sealed interface SplitAddress : HasKSerializable {
         }
 
         // the +2 is for not interfering with the 0 and 1 splits of `Block`.
-        override val asIntList = parent.asIntList + (numericalCode + 2)
+        override val asList = parent.asList + "A${numericalCode}"
         override fun fullInfo() = "${name()}[$assumption]"
         override fun toString() = name()
     }
@@ -118,7 +125,7 @@ sealed interface SplitAddress : HasKSerializable {
         // will be 0000, and second 1000, which are very different splits. That's good for searching (probably)
         fun compareRevLexical(a: SplitAddress, b: SplitAddress) = run {
             require(a.depth == b.depth) // leaving this decision out of here.
-            (a.asIntList zip b.asIntList)
+            (a.asList zip b.asList)
                 .map { (i1, i2) -> i1.compareTo(i2) }
                 .lastOrNull { it != 0 } ?: 0
         }

src/main/kotlin/verifier/splits/SplitTree.kt

@@ -67,7 +67,7 @@ class SplitTree(val origCode: CoreTACProgram, private val splittingDepth: Int,
     /**
      * [Node]s are considered equal if their [address] (given in [lazySub]) is equal.
      */
-    inner class Node(val lazySub: LazySubProgram, val sideScore: SideScore<*>) {
+    open inner class Node(val lazySub: LazySubProgram, val sideScore: SideScore<*>) {
         val address get() = lazySub.address
         val name get() = lazySub.name
 
@@ -152,6 +152,12 @@ class SplitTree(val origCode: CoreTACProgram, private val splittingDepth: Int,
             sequenceOf(this) + children.get().orEmpty().asSequence().flatMap { it.nodeSequence }
     }
 
+    /**
+     * Extends [Node] with some arbitrary additional information [info].
+     */
+    inner class NodeWithInfo<T>(lazySub: LazySubProgram, sideScore: SideScore<*>, val info: T)
+        : Node(lazySub, sideScore)
+
     val nodeSequence get() = rootNode.nodeSequence
 
     companion object {

src/test/kotlin/verifier/SplitterHeuristicTest.kt

@@ -60,8 +60,8 @@ class SplitterHeuristicTest : WithTACSource {
                 assertTrue(a.split.sideScore >= b.split.sideScore)
             } else {
                 // prefer smaller address (reverse lexicographically)
-                val aa = a.split.address.asIntList.dropLast(1)
-                val ba = b.split.address.asIntList.dropLast(1)
+                val aa = a.split.address.asList.dropLast(1)
+                val ba = b.split.address.asList.dropLast(1)
                 val res = aa.zip(ba).map { (i1, i2) -> i1.compareTo(i2) }.lastOrNull { it != 0 } ?: 0
 
                 assertTrue(res <= 0)