From 5cf8cde7b8ecec2fa7fb64523faae5a009aa2dcc Mon Sep 17 00:00:00 2001 From: mario-bucev Date: Fri, 1 Dec 2023 09:50:31 +0100 Subject: [PATCH] Equivalence checker: add 'unknown safety' category (#1488) --- .../equivchk/EquivalenceChecker.scala | 110 ++++++++++++------ .../EquivalenceCheckingComponent.scala | 58 +++++++-- .../equivchk/EquivalenceCheckingReport.scala | 8 +- .../equivalence/addHorn/test_conf.json | 3 +- .../equivalence/boardgame/test_conf_1.json | 3 +- .../equivalence/boardgame/test_conf_2.json | 3 +- .../equivalence/cloudSculpting/test_conf.json | 3 +- .../benchmarks/equivalence/dup/test_conf.json | 3 +- .../equivalence/factorial/test_conf.json | 3 +- .../equivalence/fibonacci/test_conf.json | 3 +- .../equivalence/foolproof/test_conf.json | 3 +- .../fullAlternation/test_conf.json | 3 +- .../equivalence/funnyarith1/test_conf.json | 3 +- .../equivalence/funnyarith2/test_conf.json | 3 +- .../equivalence/funnyarith3/test_conf.json | 3 +- .../halfAlternation/test_conf.json | 3 +- .../equivalence/i1264/test_conf.json | 3 +- .../equivalence/inlining/test_conf.json | 3 +- .../equivalence/isSorted/test_conf.json | 3 +- .../equivalence/iseven1/test_conf.json | 3 +- .../equivalence/iseven2/test_conf.json | 3 +- .../equivalence/limit1/test_conf.json | 3 +- .../equivalence/limit2/test_conf.json | 3 +- .../equivalence/limit3/test_conf.json | 3 +- .../equivalence/max1/test_conf.json | 3 +- .../equivalence/max2/test_conf.json | 3 +- .../equivalence/max3/test_conf.json | 3 +- .../equivalence/pascal/test_conf.json | 3 +- .../equivalence/separate/test_conf_1.json | 3 +- .../equivalence/separate/test_conf_2.json | 3 +- .../equivalence/sigma/test_conf.json | 3 +- .../benchmarks/equivalence/sum/test_conf.json | 3 +- .../unfoldingSorted/test_conf.json | 3 +- .../equivalence/uniq1/test_conf.json | 3 +- .../equivalence/uniq2/test_conf.json | 3 +- .../equivalence/unknownSafety/Candidate.scala | 52 +++++++++ .../equivalence/unknownSafety/Model.scala | 33 ++++++ .../unknownSafety/test_conf_1.json | 19 +++ .../unknownSafety/test_conf_2.json | 19 +++ .../unknownSafety/test_conf_3.json | 19 +++ .../equivalence/unrolling/test_conf.json | 3 +- .../equivalence/unused/test_conf.json | 3 +- .../equivalence/whac-a-fun/test_conf_1.json | 3 +- .../equivalence/whac-a-fun/test_conf_2.json | 3 +- .../equivalence/whac-a-fun/test_conf_3.json | 3 +- .../equivalence/whac-a-fun/test_conf_4.json | 3 +- .../equivalence/whac-a-fun/test_conf_5.json | 3 +- .../equivalence/whac-a-fun/test_conf_6.json | 3 +- .../stainless/equivchk/EquivChkSuite.scala | 13 ++- 49 files changed, 360 insertions(+), 91 deletions(-) create mode 100644 frontends/benchmarks/equivalence/unknownSafety/Candidate.scala create mode 100644 frontends/benchmarks/equivalence/unknownSafety/Model.scala create mode 100644 frontends/benchmarks/equivalence/unknownSafety/test_conf_1.json create mode 100644 frontends/benchmarks/equivalence/unknownSafety/test_conf_2.json create mode 100644 frontends/benchmarks/equivalence/unknownSafety/test_conf_3.json diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala index 8cb9a95ac9..2b612ad7ae 100644 --- 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,10 +122,15 @@ 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) @@ -132,7 +138,7 @@ class EquivalenceChecker(override val trees: Trees, 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 index f27e02d3b5..31397852cc 100644 --- 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 index 4b454dfb68..95c2aa7d39 100644 --- 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 index c5f8a4b3bf..3d374e8853 100644 --- 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": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/boardgame/test_conf_1.json b/frontends/benchmarks/equivalence/boardgame/test_conf_1.json index d38a6f6551..b3df7b3d2d 100644 --- 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": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/boardgame/test_conf_2.json b/frontends/benchmarks/equivalence/boardgame/test_conf_2.json index 80940dfcfc..2517ee5e2f 100644 --- 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": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/cloudSculpting/test_conf.json b/frontends/benchmarks/equivalence/cloudSculpting/test_conf.json index 75c2691aa3..ec368fc8bf 100644 --- 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": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/dup/test_conf.json b/frontends/benchmarks/equivalence/dup/test_conf.json index 4bd6cd0b3c..00030d5c5e 100644 --- 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 index 899d5ecb2a..d9c658f3f5 100644 --- 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": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/fibonacci/test_conf.json b/frontends/benchmarks/equivalence/fibonacci/test_conf.json index d0c3eedcf0..5868cb1465 100644 --- a/frontends/benchmarks/equivalence/fibonacci/test_conf.json +++ b/frontends/benchmarks/equivalence/fibonacci/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/foolproof/test_conf.json b/frontends/benchmarks/equivalence/foolproof/test_conf.json index f2375ccbf9..5f93a8d4cb 100644 --- a/frontends/benchmarks/equivalence/foolproof/test_conf.json +++ b/frontends/benchmarks/equivalence/foolproof/test_conf.json @@ -19,7 +19,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/fullAlternation/test_conf.json b/frontends/benchmarks/equivalence/fullAlternation/test_conf.json index 3abbbc221c..9e7b8bb4d0 100644 --- a/frontends/benchmarks/equivalence/fullAlternation/test_conf.json +++ b/frontends/benchmarks/equivalence/fullAlternation/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/funnyarith1/test_conf.json b/frontends/benchmarks/equivalence/funnyarith1/test_conf.json index 494affb44d..e4c1198490 100644 --- a/frontends/benchmarks/equivalence/funnyarith1/test_conf.json +++ b/frontends/benchmarks/equivalence/funnyarith1/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/funnyarith2/test_conf.json b/frontends/benchmarks/equivalence/funnyarith2/test_conf.json index 47cbda3531..63619a8608 100644 --- a/frontends/benchmarks/equivalence/funnyarith2/test_conf.json +++ b/frontends/benchmarks/equivalence/funnyarith2/test_conf.json @@ -17,7 +17,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/funnyarith3/test_conf.json b/frontends/benchmarks/equivalence/funnyarith3/test_conf.json index 494affb44d..e4c1198490 100644 --- a/frontends/benchmarks/equivalence/funnyarith3/test_conf.json +++ b/frontends/benchmarks/equivalence/funnyarith3/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/halfAlternation/test_conf.json b/frontends/benchmarks/equivalence/halfAlternation/test_conf.json index c84f5ee410..0e9ec7dce5 100644 --- a/frontends/benchmarks/equivalence/halfAlternation/test_conf.json +++ b/frontends/benchmarks/equivalence/halfAlternation/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/i1264/test_conf.json b/frontends/benchmarks/equivalence/i1264/test_conf.json index 851584311f..8b6b5f7924 100644 --- a/frontends/benchmarks/equivalence/i1264/test_conf.json +++ b/frontends/benchmarks/equivalence/i1264/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/inlining/test_conf.json b/frontends/benchmarks/equivalence/inlining/test_conf.json index 856fca882f..106ac53632 100644 --- a/frontends/benchmarks/equivalence/inlining/test_conf.json +++ b/frontends/benchmarks/equivalence/inlining/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/isSorted/test_conf.json b/frontends/benchmarks/equivalence/isSorted/test_conf.json index 78cb7ce0e5..d7e693f272 100644 --- a/frontends/benchmarks/equivalence/isSorted/test_conf.json +++ b/frontends/benchmarks/equivalence/isSorted/test_conf.json @@ -26,7 +26,8 @@ "IsSorted.isSortedA" ], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/iseven1/test_conf.json b/frontends/benchmarks/equivalence/iseven1/test_conf.json index 18cc3b300f..cc6e06f1f3 100644 --- a/frontends/benchmarks/equivalence/iseven1/test_conf.json +++ b/frontends/benchmarks/equivalence/iseven1/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/iseven2/test_conf.json b/frontends/benchmarks/equivalence/iseven2/test_conf.json index 18cc3b300f..cc6e06f1f3 100644 --- a/frontends/benchmarks/equivalence/iseven2/test_conf.json +++ b/frontends/benchmarks/equivalence/iseven2/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/limit1/test_conf.json b/frontends/benchmarks/equivalence/limit1/test_conf.json index 210ddf9881..6665b95f09 100644 --- a/frontends/benchmarks/equivalence/limit1/test_conf.json +++ b/frontends/benchmarks/equivalence/limit1/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/limit2/test_conf.json b/frontends/benchmarks/equivalence/limit2/test_conf.json index d6895aecf3..cf75a0ad03 100644 --- a/frontends/benchmarks/equivalence/limit2/test_conf.json +++ b/frontends/benchmarks/equivalence/limit2/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/limit3/test_conf.json b/frontends/benchmarks/equivalence/limit3/test_conf.json index 1de1d0d1f5..76d685c226 100644 --- a/frontends/benchmarks/equivalence/limit3/test_conf.json +++ b/frontends/benchmarks/equivalence/limit3/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/max1/test_conf.json b/frontends/benchmarks/equivalence/max1/test_conf.json index e16c08f606..999717d355 100644 --- a/frontends/benchmarks/equivalence/max1/test_conf.json +++ b/frontends/benchmarks/equivalence/max1/test_conf.json @@ -23,7 +23,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/max2/test_conf.json b/frontends/benchmarks/equivalence/max2/test_conf.json index 22300a5f6c..cb5a9cc3d5 100644 --- a/frontends/benchmarks/equivalence/max2/test_conf.json +++ b/frontends/benchmarks/equivalence/max2/test_conf.json @@ -27,7 +27,8 @@ "Candidate5.max" ], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/max3/test_conf.json b/frontends/benchmarks/equivalence/max3/test_conf.json index b0897df7c4..1cb5d710dd 100644 --- a/frontends/benchmarks/equivalence/max3/test_conf.json +++ b/frontends/benchmarks/equivalence/max3/test_conf.json @@ -11,7 +11,8 @@ "equivalent": [], "unequivalent": [], "unsafe": [], - "timeout": ["Candidate.max"], + "unknownSafety": [], + "unknownEquivalence": ["Candidate.max"], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/pascal/test_conf.json b/frontends/benchmarks/equivalence/pascal/test_conf.json index 5407773196..99d6578aaf 100644 --- a/frontends/benchmarks/equivalence/pascal/test_conf.json +++ b/frontends/benchmarks/equivalence/pascal/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/separate/test_conf_1.json b/frontends/benchmarks/equivalence/separate/test_conf_1.json index 16edb38424..20cc4342e5 100644 --- a/frontends/benchmarks/equivalence/separate/test_conf_1.json +++ b/frontends/benchmarks/equivalence/separate/test_conf_1.json @@ -22,7 +22,8 @@ "Candidate2.separate" ], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/separate/test_conf_2.json b/frontends/benchmarks/equivalence/separate/test_conf_2.json index 8d55cf2ae6..6a73fd3e64 100644 --- a/frontends/benchmarks/equivalence/separate/test_conf_2.json +++ b/frontends/benchmarks/equivalence/separate/test_conf_2.json @@ -18,7 +18,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": ["Candidate2.separate"], + "unknownSafety": [], + "unknownEquivalence": ["Candidate2.separate"], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/sigma/test_conf.json b/frontends/benchmarks/equivalence/sigma/test_conf.json index cd8f052520..9c7cfcc849 100644 --- a/frontends/benchmarks/equivalence/sigma/test_conf.json +++ b/frontends/benchmarks/equivalence/sigma/test_conf.json @@ -10,7 +10,8 @@ "equivalent": [], "unequivalent": [], "unsafe": [], - "timeout": ["Candidate.sigma"], + "unknownSafety": [], + "unknownEquivalence": ["Candidate.sigma"], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/sum/test_conf.json b/frontends/benchmarks/equivalence/sum/test_conf.json index c52874076f..0451bb061b 100644 --- a/frontends/benchmarks/equivalence/sum/test_conf.json +++ b/frontends/benchmarks/equivalence/sum/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unfoldingSorted/test_conf.json b/frontends/benchmarks/equivalence/unfoldingSorted/test_conf.json index 9db007795e..b8c86a2ab3 100644 --- a/frontends/benchmarks/equivalence/unfoldingSorted/test_conf.json +++ b/frontends/benchmarks/equivalence/unfoldingSorted/test_conf.json @@ -24,7 +24,8 @@ "Candidate4.unfoldingSorted" ], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [ "Candidate2.unfoldingSorted" ] diff --git a/frontends/benchmarks/equivalence/uniq1/test_conf.json b/frontends/benchmarks/equivalence/uniq1/test_conf.json index d0077de36f..d6e96f9d64 100644 --- a/frontends/benchmarks/equivalence/uniq1/test_conf.json +++ b/frontends/benchmarks/equivalence/uniq1/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/uniq2/test_conf.json b/frontends/benchmarks/equivalence/uniq2/test_conf.json index 5e13014050..8a65719355 100644 --- a/frontends/benchmarks/equivalence/uniq2/test_conf.json +++ b/frontends/benchmarks/equivalence/uniq2/test_conf.json @@ -26,7 +26,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unknownSafety/Candidate.scala b/frontends/benchmarks/equivalence/unknownSafety/Candidate.scala new file mode 100644 index 0000000000..3a49803988 --- /dev/null +++ b/frontends/benchmarks/equivalence/unknownSafety/Candidate.scala @@ -0,0 +1,52 @@ +import stainless.lang._ +import stainless.collection._ + +object Candidate { + + def zero(x: BigInt): BigInt = { + require(x >= 0) + if (x > 0) zero(x - 1) + else x + } + + def add(x: BigInt, y: BigInt): BigInt = { + if (x >= 0) { + val z = zero(x) + assert(z == 0) // timeout + } + x + y + } + + ///////////////////////////////////// + + def isEvenTopLvl(x: BigInt): Boolean = isEven(x) + + def isEven(x: BigInt): Boolean = { + decreases(if (x <= 0) BigInt(0) else x) + if (x >= 0) { + assert(zero(x) == 0) // timeout + } + if (x < 0) false + else if (x == 0) true + else !isOdd(x - 1) + } + + def isOdd(x: BigInt): Boolean = { + decreases(if (x <= 0) BigInt(0) else x) + if (x <= 0) false + else if (x == 1) true + else !isEven(x - 1) + } + + ///////////////////////////////////// + + def isSorted(xs: List[BigInt]): Boolean = xs match { + case Nil() => true + case Cons(h, Nil()) => + if (h >= 0) { + assert(zero(h) == 0) // timeout + } + true + case Cons(h1, Cons(h2, t)) => h1 <= h2 && isSorted(t) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unknownSafety/Model.scala b/frontends/benchmarks/equivalence/unknownSafety/Model.scala new file mode 100644 index 0000000000..1f127e7386 --- /dev/null +++ b/frontends/benchmarks/equivalence/unknownSafety/Model.scala @@ -0,0 +1,33 @@ +import stainless.lang._ +import stainless.collection._ + +object Model { + + def add(x: BigInt, y: BigInt): BigInt = x + y + + ///////////////////////////////////// + + def isEvenTopLvl(x: BigInt): Boolean = isEven(x) + + def isEven(x: BigInt): Boolean = { + decreases(if (x <= 0) BigInt(0) else x) + if (x < 0) false + else if (x == 0) true + else !isOdd(x - 1) + } + + def isOdd(x: BigInt): Boolean = { + decreases(if (x <= 0) BigInt(0) else x) + if (x <= 0) false + else if (x == 1) true + else !isEven(x - 1) + } + + ///////////////////////////////////// + + def isSorted(xs: List[BigInt]): Boolean = xs match { + case Nil() => true + case Cons(_, Nil()) => true + case Cons(h1, Cons(h2, t)) => h1 <= h2 && isSorted(t) + } +} \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unknownSafety/test_conf_1.json b/frontends/benchmarks/equivalence/unknownSafety/test_conf_1.json new file mode 100644 index 0000000000..da3eaef348 --- /dev/null +++ b/frontends/benchmarks/equivalence/unknownSafety/test_conf_1.json @@ -0,0 +1,19 @@ +{ + "models": [ + "Model.add" + ], + "comparefuns": [ + "Candidate.add" + ], + "tests": [], + "outcome": { + "equivalent": [], + "unequivalent": [], + "unsafe": [], + "unknownSafety": [ + "Candidate.add" + ], + "unknownEquivalence": [], + "wrong": [] + } +} \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unknownSafety/test_conf_2.json b/frontends/benchmarks/equivalence/unknownSafety/test_conf_2.json new file mode 100644 index 0000000000..40126d8bc2 --- /dev/null +++ b/frontends/benchmarks/equivalence/unknownSafety/test_conf_2.json @@ -0,0 +1,19 @@ +{ + "models": [ + "Model.isEvenTopLvl" + ], + "comparefuns": [ + "Candidate.isEvenTopLvl" + ], + "tests": [], + "outcome": { + "equivalent": [], + "unequivalent": [], + "unsafe": [], + "unknownSafety": [ + "Candidate.isEvenTopLvl" + ], + "unknownEquivalence": [], + "wrong": [] + } +} \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unknownSafety/test_conf_3.json b/frontends/benchmarks/equivalence/unknownSafety/test_conf_3.json new file mode 100644 index 0000000000..a782d530f7 --- /dev/null +++ b/frontends/benchmarks/equivalence/unknownSafety/test_conf_3.json @@ -0,0 +1,19 @@ +{ + "models": [ + "Model.isSorted" + ], + "comparefuns": [ + "Candidate.isSorted" + ], + "tests": [], + "outcome": { + "equivalent": [], + "unequivalent": [], + "unsafe": [], + "unknownSafety": [ + "Candidate.isSorted" + ], + "unknownEquivalence": [], + "wrong": [] + } +} \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unrolling/test_conf.json b/frontends/benchmarks/equivalence/unrolling/test_conf.json index 936c66e3e7..4ee46d9346 100644 --- a/frontends/benchmarks/equivalence/unrolling/test_conf.json +++ b/frontends/benchmarks/equivalence/unrolling/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/unused/test_conf.json b/frontends/benchmarks/equivalence/unused/test_conf.json index 3b1b168f73..4e476d6b94 100644 --- a/frontends/benchmarks/equivalence/unused/test_conf.json +++ b/frontends/benchmarks/equivalence/unused/test_conf.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_1.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_1.json index 91d601bd27..be54a7483d 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_1.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_1.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_2.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_2.json index 6de85a6543..96f1ca61d1 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_2.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_2.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_3.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_3.json index 31e3e46f1c..a1bef7c775 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_3.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_3.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_4.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_4.json index 7e68a4c2b8..51c9ef8110 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_4.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_4.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_5.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_5.json index 9c0aa3f5f9..5f001fab9f 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_5.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_5.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_6.json b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_6.json index a50e9b919f..80ad356a8f 100644 --- a/frontends/benchmarks/equivalence/whac-a-fun/test_conf_6.json +++ b/frontends/benchmarks/equivalence/whac-a-fun/test_conf_6.json @@ -16,7 +16,8 @@ ], "unequivalent": [], "unsafe": [], - "timeout": [], + "unknownSafety": [], + "unknownEquivalence": [], "wrong": [] } } \ No newline at end of file diff --git a/frontends/common/src/it/scala/stainless/equivchk/EquivChkSuite.scala b/frontends/common/src/it/scala/stainless/equivchk/EquivChkSuite.scala index 9b9e9337b2..0ed6bf8218 100644 --- a/frontends/common/src/it/scala/stainless/equivchk/EquivChkSuite.scala +++ b/frontends/common/src/it/scala/stainless/equivchk/EquivChkSuite.scala @@ -74,7 +74,8 @@ class EquivChkSuite extends ComponentTestSuite { acc.copy(equiv = acc.equiv + (mod.fullName -> (currCluster + fn))) case Status.Equivalence(EquivalenceStatus.Unequivalent) => acc.copy(unequivalent = acc.unequivalent + fn) case Status.Equivalence(EquivalenceStatus.Unsafe) => acc.copy(unsafe = acc.unsafe + fn) - case Status.Equivalence(EquivalenceStatus.Unknown) => acc.copy(timeout = acc.timeout + fn) + case Status.Equivalence(EquivalenceStatus.UnknownSafety) => acc.copy(unknownSafety = acc.unknownSafety + fn) + case Status.Equivalence(EquivalenceStatus.UnknownEquivalence) => acc.copy(unknownEquivalence = acc.unknownEquivalence + fn) case Status.Equivalence(EquivalenceStatus.Wrong) => acc.copy(wrong = acc.wrong + fn) case Status.Verification(_) => acc } @@ -88,12 +89,13 @@ object EquivChkSuite extends ConfigurableTests { case class Results(equiv: Map[String, Set[String]], unequivalent: Set[String], unsafe: Set[String], - timeout: Set[String], + unknownSafety: Set[String], + unknownEquivalence: Set[String], wrong: Set[String]) object Results { def empty: Results = - Results(Map.empty, Set.empty, Set.empty, Set.empty, Set.empty) + Results(Map.empty, Set.empty, Set.empty, Set.empty, Set.empty, Set.empty) } case class TestConf(models: Set[String], @@ -135,8 +137,9 @@ object EquivChkSuite extends ConfigurableTests { }.toMap val unequivalent = jsonObj.getStringArrayOrCry("unequivalent").toSet val unsafe = jsonObj.getStringArrayOrCry("unsafe").toSet - val timeout = jsonObj.getStringArrayOrCry("timeout").toSet + val unknownSafety = jsonObj.getStringArrayOrCry("unknownSafety").toSet + val unknownEquiv = jsonObj.getStringArrayOrCry("unknownEquivalence").toSet val wrong = jsonObj.getStringArrayOrCry("wrong").toSet - Results(equiv, unequivalent, unsafe, timeout, wrong) + Results(equiv, unequivalent, unsafe, unknownSafety, unknownEquiv, wrong) } }