epfl-lara · vkuncak · Dec 1, 2023 · Nov 23, 2023
diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala
@@ -111,7 +111,8 @@ class EquivalenceChecker(override val trees: Trees,
                      unequivalent: Map[Identifier, UnequivalentData],
                      unsafe: Map[Identifier, UnsafeData],
                      // Candidates that will need to be manually inspected...
-                     unknowns: Map[Identifier, UnknownData],
+                     unknownsEquivalence: Map[Identifier, UnknownEquivalenceData],
+                     unknownsSafety: Map[Identifier, UnknownSafetyData],
                      // Incorrect signature
                      wrongs: Set[Identifier],
                      weights: Map[Identifier, Int])
@@ -121,18 +122,23 @@ class EquivalenceChecker(override val trees: Trees,
   // The list of counter-examples can be empty; the candidate is still invalid but a ctex could not be extracted
   // If the solvingInfo is None, the candidate has been pruned.
   case class UnequivalentData(ctexs: Seq[Ctex], solvingInfo: Option[SolvingInfo])
+
   case class UnsafeData(self: Seq[UnsafeCtex], auxiliaries: Map[Identifier, Seq[UnsafeCtex]])
   case class UnsafeCtex(kind: VCKind, pos: Position, ctex: Option[Seq[(ValDef, Expr)]], solvingInfo: SolvingInfo)
 
-  case class UnknownData(solvingInfo: SolvingInfo)
+  case class UnknownEquivalenceData(solvingInfo: SolvingInfo)
+
+  case class UnknownSafetyData(self: Seq[UnknownSafetyVC], auxiliaries: Map[Identifier, Seq[UnknownSafetyVC]])
+  case class UnknownSafetyVC(kind: VCKind, pos: Position, solvingInfo: SolvingInfo)
+
   // Note: fromCache and trivial are only relevant for valid candidates
   case class SolvingInfo(time: Long, solverName: Option[String], fromCache: Boolean, trivial: Boolean) {
     def withAddedTime(extra: Long): SolvingInfo = copy(time = time + extra)
   }
 
   def getCurrentResults(): Results = {
     val equiv = clusters.map { case (model, clst) => model -> clst.toSet }.toMap
-    Results(equiv, valid.toMap, unequivalent.toMap, unsafe.toMap, unknowns.toMap, signatureMismatch.toSet, models.toMap)
+    Results(equiv, valid.toMap, unequivalent.toMap, unsafe.toMap, unknownsEquivalence.toMap, unknownsSafety.toMap, signatureMismatch.toSet, models.toMap)
   }
   //endregion
 
@@ -236,7 +242,8 @@ class EquivalenceChecker(override val trees: Trees,
   private val valid = mutable.Map.empty[Identifier, ValidData]
   private val unequivalent = mutable.Map.empty[Identifier, UnequivalentData]
   private val unsafe = mutable.Map.empty[Identifier, UnsafeData]
-  private val unknowns = mutable.LinkedHashMap.empty[Identifier, UnknownData]
+  private val unknownsEquivalence = mutable.LinkedHashMap.empty[Identifier, UnknownEquivalenceData]
+  private val unknownsSafety = mutable.LinkedHashMap.empty[Identifier, UnknownSafetyData]
   private val signatureMismatch = mutable.ArrayBuffer.empty[Identifier]
   private val clusters = mutable.Map.empty[Identifier, mutable.ArrayBuffer[Identifier]]
 
@@ -260,32 +267,36 @@ class EquivalenceChecker(override val trees: Trees,
     val ordCtexs = ctexOrderedArguments(fun, pr)(counterex.vars)
     val fd = symbols.functions(fun)
     val ctexVars = ordCtexs.map(ctex => fd.params.zip(ctex))
-    if (allCandidates.contains(fun)) {
-      remainingCandidates -= fun
-      ordCtexs.foreach(addCtex)
-      val currUnsafeData = unsafe.getOrElse(fun, UnsafeData(Seq.empty, Map.empty))
-      val newUnsafeData = currUnsafeData.copy(self = currUnsafeData.self :+ UnsafeCtex(vc.kind, vc.getPos, ctexVars, extractSolvingInfo(analysis, fun, Seq.empty)))
-      unsafe += fun -> newUnsafeData
-      Some(Set(fun))
-    } else candidatesCallee.get(fun) match {
-      case Some(cands) =>
-        // This means this erroneous `fun` is called by all candidates in `cands`.
-        // Note: we do not add the ctexs with `addCtex`, because counterex corresponds to the signature of `fun` not necessarily `cand`
+    reportHelper(pr)(analysis, vc) {
+      fun =>
+        ordCtexs.foreach(addCtex)
+        val currUnsafeData = unsafe.getOrElse(fun, UnsafeData(Seq.empty, Map.empty))
+        val newUnsafeData = currUnsafeData.copy(self = currUnsafeData.self :+ UnsafeCtex(vc.kind, vc.getPos, ctexVars, extractSolvingInfo(analysis, fun, Seq.empty)))
+        unsafe += fun -> newUnsafeData
+    } { cand =>
+      // Note: we do not add the ctexs with `addCtex`, because counterex corresponds to the signature of `fun` not necessarily `cand`
+      val currUnsafeData = unsafe.getOrElse(cand, UnsafeData(Seq.empty, Map.empty))
+      val currUnsafeCtexs = currUnsafeData.auxiliaries.getOrElse(fun, Seq.empty)
+      val newUnsafeCtexs = currUnsafeCtexs :+ UnsafeCtex(vc.kind, vc.getPos, ctexVars, extractSolvingInfo(analysis, fun, Seq.empty))
+      val newUnsafeData = currUnsafeData.copy(auxiliaries = currUnsafeData.auxiliaries + (fun -> newUnsafeCtexs))
+      unsafe += cand -> newUnsafeData
+    }
+  }
 
-        // `cands` should be of size 1 because a function called by multiple candidates must be either a library fn or
-        // a provided function which are all assumed to be correct.
-        cands.foreach { cand =>
-          remainingCandidates -= cand
-          val currUnsafeData = unsafe.getOrElse(cand, UnsafeData(Seq.empty, Map.empty))
-          val currUnsafeCtexs = currUnsafeData.auxiliaries.getOrElse(fun, Seq.empty)
-          val newUnsafeCtexs = currUnsafeCtexs :+ UnsafeCtex(vc.kind, vc.getPos, ctexVars, extractSolvingInfo(analysis, fun, Seq.empty))
-          val newUnsafeData = currUnsafeData.copy(auxiliaries = currUnsafeData.auxiliaries + (fun -> newUnsafeCtexs))
-          unsafe += cand -> newUnsafeData
-        }
-        Some(cands)
-      case None =>
-        // Nobody knows about this function
-        None
+  def reportUnknown(pr: StainlessProgram)(analysis: VerificationAnalysis, vc: VC[pr.trees.type]): Option[Set[Identifier]] = {
+    val fun = vc.fid
+    reportHelper(pr)(analysis, vc) {
+      fun =>
+        remainingCandidates -= fun
+        val currUnknownData = unknownsSafety.getOrElse(fun, UnknownSafetyData(Seq.empty, Map.empty))
+        val newUnsafeData = currUnknownData.copy(self = currUnknownData.self :+ UnknownSafetyVC(vc.kind, vc.getPos, extractSolvingInfo(analysis, fun, Seq.empty)))
+        unknownsSafety += fun -> newUnsafeData
+    } { cand =>
+      val currUnknownData = unknownsSafety.getOrElse(cand, UnknownSafetyData(Seq.empty, Map.empty))
+      val currUnknownVCs = currUnknownData.auxiliaries.getOrElse(fun, Seq.empty)
+      val newUnknownVCs = currUnknownVCs :+ UnknownSafetyVC(vc.kind, vc.getPos, extractSolvingInfo(analysis, fun, Seq.empty))
+      val newUnknownData = currUnknownData.copy(auxiliaries = currUnknownData.auxiliaries + (fun -> newUnknownVCs))
+      unknownsSafety += cand -> newUnknownData
     }
   }
 
@@ -329,17 +340,17 @@ class EquivalenceChecker(override val trees: Trees,
           NextExamination.NewCandidate(candId, topN.head, strat, pruned.toMap)
         } else {
           // This candidate has been tested with all models, so put it pack into unknowns
-          unknowns += candId -> UnknownData(SolvingInfo(0L, None, false, false))
+          unknownsEquivalence += candId -> UnknownEquivalenceData(SolvingInfo(0L, None, false, false))
           pickNextExamination() match {
             case d@NextExamination.Done(_, _) => d.copy(pruned = pruned.toMap ++ d.pruned)
             case nc@NextExamination.NewCandidate(_, _, _, _) => nc.copy(pruned = pruned.toMap ++ nc.pruned)
           }
         }
       case None =>
-        if (unknowns.nonEmpty && unknowns.size < nbExaminedCandidates) {
-          nbExaminedCandidates = unknowns.size
-          remainingCandidates ++= unknowns.keys
-          unknowns.clear()
+        if (unknownsEquivalence.nonEmpty && unknownsEquivalence.size < nbExaminedCandidates) {
+          nbExaminedCandidates = unknownsEquivalence.size
+          remainingCandidates ++= unknownsEquivalence.keys
+          unknownsEquivalence.clear()
           pickNextExamination() match {
             case d@NextExamination.Done(_, _) => d.copy(pruned = pruned.toMap ++ d.pruned)
             case nc@NextExamination.NewCandidate(_, _, _, _) => nc.copy(pruned = pruned.toMap ++ nc.pruned)
@@ -447,7 +458,7 @@ class EquivalenceChecker(override val trees: Trees,
         } else {
           // oh no, manual inspection incoming
           examinationState = ExaminationState.PickNext
-          unknowns += cand -> UnknownData(solvingInfo.withAddedTime(currCumulativeSolvingTime))
+          unknownsEquivalence += cand -> UnknownEquivalenceData(solvingInfo.withAddedTime(currCumulativeSolvingTime))
           RoundConclusion.CandidateClassified(cand, Classification.Unknown, invalidPairs)
         }
       }
@@ -912,6 +923,35 @@ class EquivalenceChecker(override val trees: Trees,
 
   //region Miscellaneous
 
+  private def reportHelper(pr: StainlessProgram)
+                          (analysis: VerificationAnalysis, vc: VC[pr.trees.type])
+                          // Operations to perform if the function in question is the function checked
+                          // for equivalence (i.e. one that is passed to --comparefuns)
+                          (onMainFault: Identifier => Unit)
+                          // Operations to perform if the function in question is a function
+                          // called by the function checked for equivalence
+                          (onAuxiliaryFault: Identifier => Unit): Option[Set[Identifier]] = {
+    val fun = vc.fid
+    if (allCandidates.contains(fun)) {
+      remainingCandidates -= fun
+      onMainFault(fun)
+      Some(Set(fun))
+    } else candidatesCallee.get(fun) match {
+      case Some(cands) =>
+        // This means this erroneous or safety-unknown `fun` is called by all candidates in `cands`.
+        // `cands` should be of size 1 because a function called by multiple candidates must be either a library fn or
+        // a provided function which are all assumed to be correct.
+        cands.foreach { cand =>
+          remainingCandidates -= cand
+          onAuxiliaryFault(cand)
+        }
+        Some(cands)
+      case None =>
+        // Nobody knows about this function
+        None
+    }
+  }
+
   // Note: expects the ctex to have type parameter substituted with integer literals (as it is done in ctexOrderedArguments).
   private def addCtex(ctex: Seq[Expr]): Unit = {
     val currNbCtex = ctexsDb.map(_._2.size).sum

diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala
@@ -130,7 +130,9 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
       invalidVCsCands = counterExamples(gen).flatMap {
         case (vc, ctex) => ec.reportUnsafe(gen.program)(gen, vc, ctex).getOrElse(Set.empty)
       }.toSeq.distinct
+      unknownsSafetyCands = unknowns(gen).flatMap(ec.reportUnknown(gen.program)(gen, _).getOrElse(Set.empty)).toSeq.distinct
       _ = debugInvalidVCsCandidates(invalidVCsCands)
+      _ = debugUnknownsSafetyCandidates(unknownsSafetyCands)
       trRes <- equivCheck(ec)
     } yield buildAnalysis(ec)(ids, gen, trRes)
   }
@@ -156,24 +158,31 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
           solvingInfo.flatMap(_.solverName), "equivalence", fd.source))
     }
     val unsafe = trRes.unsafe.toSeq.sortBy(_._1).flatMap {
-      case (errn, ec.UnsafeData(_, _)) =>
+      case (errn, _) =>
         val fd = ec.symbols.getFunction(errn)
         Some(Record(errn, fd.getPos, 0L,
           Status.Equivalence(EquivalenceStatus.Unsafe),
           None, "safety", fd.source))
     }
+    val unknwsSafety = trRes.unknownsSafety.toSeq.sortBy(_._1).flatMap {
+      case (fnId, _) =>
+        val fd = ec.symbols.getFunction(fnId)
+        Some(Record(fnId, fd.getPos, 0L,
+          Status.Equivalence(EquivalenceStatus.UnknownSafety),
+          None, "safety", fd.source))
+    }
     val wrgs = trRes.wrongs.toSeq.sorted.map { wrong =>
       val fd = ec.symbols.getFunction(wrong)
       // No solver or time specified because it's a signature mismatch
       Record(wrong, fd.getPos, 0L, Status.Equivalence(EquivalenceStatus.Wrong), None, "equivalence", fd.source)
     }
-    val unknws = trRes.unknowns.toSeq.sortBy(_._1).map {
+    val unknwsEquiv = trRes.unknownsEquivalence.toSeq.sortBy(_._1).map {
       case (unknown, data) =>
         val fd = ec.symbols.getFunction(unknown)
-        Record(unknown, fd.getPos, data.solvingInfo.time, Status.Equivalence(EquivalenceStatus.Unknown), data.solvingInfo.solverName, "equivalence", fd.source)
+        Record(unknown, fd.getPos, data.solvingInfo.time, Status.Equivalence(EquivalenceStatus.UnknownEquivalence), data.solvingInfo.solverName, "equivalence", fd.source)
     }
 
-    val allRecords = genRecors ++ valid ++ unsafe ++ unequiv ++ wrgs ++ unknws
+    val allRecords = genRecors ++ valid ++ unsafe ++ unequiv ++ wrgs ++ unknwsSafety ++ unknwsEquiv
     new EquivalenceCheckingAnalysis(ids.toSet, allRecords, general.extractionSummary)
   }
 
@@ -231,6 +240,12 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
     }.toMap
   }
 
+  private def unknowns(analysis: VerificationAnalysis) = {
+    analysis.vrs.collect {
+      case (vc, vcRes) if vcRes.isInconclusive => vc
+    }
+  }
+
   private def debugInvalidVCsCandidates(cands: Seq[Identifier]): Unit = {
     if (cands.nonEmpty) {
       context.reporter.whenDebug(DebugSectionEquivChk) { debug =>
@@ -241,6 +256,16 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
     }
   }
 
+  private def debugUnknownsSafetyCandidates(cands: Seq[Identifier]): Unit = {
+    if (cands.nonEmpty) {
+      context.reporter.whenDebug(DebugSectionEquivChk) { debug =>
+        debug(s"The following candidates were pruned for having unknowns VCs:")
+        val candsStr = cands.sorted.map(_.fullName).mkString("  ", "\n  ", "")
+        debug(candsStr)
+      }
+    }
+  }
+
   private def debugPruned(ec: EquivalenceChecker)(pruned: Map[Identifier, ec.PruningReason]): Unit = {
     def pretty(fn: Identifier, reason: ec.PruningReason): Seq[String] = {
       val rsonStr = reason match {
@@ -307,10 +332,12 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
       info(s"List of functions that are equivalent to model ${m.fullName}: ${lStr.mkString(", ")}")
     }
     val errns = res.unequivalent.keys.toSeq.map(_.fullName).sorted.mkString(", ")
-    val unknowns = res.unknowns.keys.toSeq.map(_.fullName).sorted.mkString(", ")
+    val unknownsSafety = res.unknownsSafety.keys.toSeq.map(_.fullName).sorted.mkString(", ")
+    val unknownsEquiv = res.unknownsEquivalence.keys.toSeq.map(_.fullName).sorted.mkString(", ")
     val wrongs = res.wrongs.toSeq.map(_.fullName).sorted.mkString(", ")
     info(s"List of erroneous functions: $errns")
-    info(s"List of timed-out functions: $unknowns")
+    info(s"List of timed-out functions (safety): $unknownsSafety")
+    info(s"List of timed-out functions (equivalence): $unknownsEquiv")
     info(s"List of wrong functions: $wrongs")
     info(s"Printing the final state:")
     res.valid.foreach { case (cand, data) =>
@@ -365,10 +392,14 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
       "position" -> Json.fromString(s"${data.pos.line}:${data.pos.col}"),
       "ctex" -> data.ctex.map(mapping => ctexJson(ec.Ctex(mapping, None))).getOrElse(Json.Null)
     ))
+    def unknownVCJson(data: ec.UnknownSafetyVC): Json = Json.fromFields(Seq(
+      "kind" -> Json.fromString(data.kind.name),
+      "position" -> Json.fromString(s"${data.pos.line}:${data.pos.col}"),
+    ))
 
     val equivs = res.equiv.map { case (m, l) => m.fullName -> l.map(_.fullName).toSeq.sorted }
       .toSeq.sortBy(_._1)
-    val unknowns = res.unknowns.keys.toSeq.map(_.fullName).sorted
+    val unknownsEquiv = res.unknownsEquivalence.keys.toSeq.map(_.fullName).sorted
     val wrongs = res.wrongs.toSeq.map(_.fullName).sorted
     val weights = res.weights.map { case (mod, w) => mod.fullName -> w }.toSeq
       .sortBy { case (mod, w) => (-w, mod) }
@@ -397,7 +428,18 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking
           )
         ))
       }),
-      "timeout" -> Json.fromValues(unknowns.sorted.map(Json.fromString)),
+      "unknownSafety" -> Json.fromValues(res.unknownsSafety.toSeq.sortBy(_._1).map { case (cand, data) =>
+        Json.fromFields(Seq(
+          "function" -> Json.fromString(cand.fullName),
+          "self" -> Json.fromValues(data.self.map(unknownVCJson)),
+          "auxiliaries" -> Json.fromFields(
+            data.auxiliaries.toSeq.map { case (aux, ctexs) =>
+              aux.fullName -> Json.fromValues(ctexs.map(unknownVCJson))
+            }.sortBy(_._1)
+          )
+        ))
+      }),
+      "unknownEquivalence" -> Json.fromValues(unknownsEquiv.sorted.map(Json.fromString)),
       "wrong" -> Json.fromValues(wrongs.sorted.map(Json.fromString)),
       "weights" -> Json.fromFields(weights.map { case (mod, w) => mod -> Json.fromInt(w) })
     ))

diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala
@@ -44,7 +44,7 @@ object EquivalenceCheckingReport {
 
     def isInconclusive: Boolean = this match {
       case Verification(status) => status.isInconclusive
-      case Equivalence(EquivalenceStatus.Unknown) => true
+      case Equivalence(EquivalenceStatus.UnknownSafety | EquivalenceStatus.UnknownEquivalence) => true
       case _ => false
     }
   }
@@ -54,7 +54,8 @@ object EquivalenceCheckingReport {
     case Unequivalent
     case Unsafe
     case Wrong
-    case Unknown
+    case UnknownSafety
+    case UnknownEquivalence
   }
 
   case class Record(id: Identifier, pos: inox.utils.Position, time: Long,
@@ -90,7 +91,8 @@ class EquivalenceCheckingReport(override val results: Seq[EquivalenceCheckingRep
         case Status.Equivalence(EquivalenceStatus.Wrong) => "signature mismatch"
         case Status.Equivalence(EquivalenceStatus.Unequivalent) => "not equivalent"
         case Status.Equivalence(EquivalenceStatus.Unsafe) => "unsafe"
-        case Status.Equivalence(EquivalenceStatus.Unknown) => "unknown"
+        case Status.Equivalence(EquivalenceStatus.UnknownSafety) => "unknown safety"
+        case Status.Equivalence(EquivalenceStatus.UnknownEquivalence) => "unknown equivalence"
       }
       val level = levelOf(status)
       val solver = solverName getOrElse ""

diff --git a/frontends/benchmarks/equivalence/addHorn/test_conf.json b/frontends/benchmarks/equivalence/addHorn/test_conf.json
@@ -16,7 +16,8 @@
     ],
     "unequivalent": [],
     "unsafe": [],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": []
   }
 }
diff --git a/frontends/benchmarks/equivalence/boardgame/test_conf_1.json b/frontends/benchmarks/equivalence/boardgame/test_conf_1.json
@@ -26,7 +26,8 @@
       "Candidate4.validCitySettlement"
     ],
     "unsafe": [],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": []
   }
 }
diff --git a/frontends/benchmarks/equivalence/boardgame/test_conf_2.json b/frontends/benchmarks/equivalence/boardgame/test_conf_2.json
@@ -33,7 +33,8 @@
     "unsafe": [
       "Candidate3.adjacencyBonus"
     ],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": []
   }
 }
diff --git a/frontends/benchmarks/equivalence/cloudSculpting/test_conf.json b/frontends/benchmarks/equivalence/cloudSculpting/test_conf.json
@@ -18,7 +18,8 @@
     ],
     "unequivalent": [],
     "unsafe": [],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": []
   }
 }
diff --git a/frontends/benchmarks/equivalence/dup/test_conf.json b/frontends/benchmarks/equivalence/dup/test_conf.json
@@ -26,7 +26,8 @@
       "Candidate4.dup"
     ],
     "unsafe": [],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": [
       "Candidate3.dup"
     ]

diff --git a/frontends/benchmarks/equivalence/factorial/test_conf.json b/frontends/benchmarks/equivalence/factorial/test_conf.json
@@ -16,7 +16,8 @@
     ],
     "unequivalent": [],
     "unsafe": [],
-    "timeout": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
     "wrong": []
   }
 }