From dde79327f15a08a2286d27c99f8c240435e9d482 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 12 Apr 2024 16:45:16 +0200 Subject: [PATCH] add SMT lib file id to the report for each VC when debug=smt is enabled --- core/src/main/scala/stainless/Report.scala | 15 ++++++++---- .../equivchk/EquivalenceChecker.scala | 2 +- .../EquivalenceCheckingComponent.scala | 2 +- .../equivchk/EquivalenceCheckingReport.scala | 2 +- .../evaluators/EvaluatorReport.scala | 2 +- .../scala/stainless/genc/GenCComponent.scala | 2 +- .../termination/TerminationReport.scala | 2 +- .../scala/stainless/testgen/GenCTestGen.scala | 2 +- .../stainless/testgen/ScalaTestGen.scala | 2 +- .../verification/CoqVerificationChecher.scala | 4 ++-- .../verification/VerificationAnalysis.scala | 3 ++- .../verification/VerificationCache.scala | 4 ++-- .../verification/VerificationChecker.scala | 24 +++++++++---------- .../verification/VerificationComponent.scala | 6 ++--- .../verification/VerificationConditions.scala | 3 ++- .../verification/VerificationReport.scala | 6 ++--- 16 files changed, 44 insertions(+), 37 deletions(-) diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala index a06bd9bf2c..3da5a1cf7e 100644 --- a/core/src/main/scala/stainless/Report.scala +++ b/core/src/main/scala/stainless/Report.scala @@ -33,7 +33,8 @@ case class RecordRow( pos: Position, level: Level.Type, extra: Seq[String], - time: Long + time: Long, + smtLibId: Option[Int] ) /** @@ -78,10 +79,14 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => private def processRows(full: Boolean)(using ctx: inox.Context): Seq[Row] = { val printUniqueName = ctx.options.findOptionOrDefault(inox.ast.optPrintUniqueIds) for { - RecordRow(id, pos, level, extra, time) <- annotatedRows.sortBy(r => r.id -> r.pos) + RecordRow(id, pos, level, extra, time, smtLibId) <- annotatedRows.sortBy(r => r.id -> r.pos) if full || level != Level.Normal name = if (printUniqueName) id.uniqueName else id.name - contents = Position.smartPos(pos) +: (name +: (extra :+ f"${time / 1000d}%3.1f")) + t = smtLibId match { + case Some(v) => (extra :+ f"${time / 1000d}%3.1f" ) :+ f"smt-lib-$v" + case None => extra :+ f"${time / 1000d}%3.1f" + } + contents = Position.smartPos(pos) +: (name +: t) } yield Row(contents map { str => Cell(withColor(str, level)) }) } @@ -105,7 +110,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => def hasError(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match { case None => false case Some(i) => annotatedRows.exists(elem => elem match { - case RecordRow(id, pos, level, extra, time) => { + case RecordRow(id, pos, level, extra, time, smtLibId) => { (level == Level.Error && id == i) } }) @@ -114,7 +119,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => def hasUnknown(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match { case None => false case Some(i) => annotatedRows.exists(elem => elem match { - case RecordRow(id, pos, level, extra, time) => level == Level.Warning && id == i + case RecordRow(id, pos, level, extra, time, smtLibId) => level == Level.Warning && id == i }) } diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala index 11dd21655d..226c5da46a 100644 --- a/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala +++ b/core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala @@ -467,7 +467,7 @@ class EquivalenceChecker(override val trees: Trees, val report = analysis.toReport val allCtexs = analysis.vrs.collect { - case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => + case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => ctexOrderedArguments(vc.fid, model.program)(model.vars).map(vc.fid -> _) }.flatten.groupMap(_._1)(_._2) diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala index 31397852cc..21b15b8e12 100644 --- a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala +++ b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingComponent.scala @@ -235,7 +235,7 @@ class EquivalenceCheckingRun private(override val component: EquivalenceChecking private def counterExamples(analysis: VerificationAnalysis) = { analysis.vrs.collect { - case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => + case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => vc -> model }.toMap } diff --git a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala index 95c2aa7d39..563e483269 100644 --- a/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala +++ b/core/src/main/scala/stainless/equivchk/EquivalenceCheckingReport.scala @@ -97,7 +97,7 @@ class EquivalenceCheckingReport(override val results: Seq[EquivalenceCheckingRep val level = levelOf(status) val solver = solverName getOrElse "" val extra = Seq(kind, statusName, solver) - RecordRow(id, pos, level, extra, time) + RecordRow(id, pos, level, extra, time, None) } lazy val totalConditions: Int = results.size lazy val totalTime: Long = results.map(_.time).sum diff --git a/core/src/main/scala/stainless/evaluators/EvaluatorReport.scala b/core/src/main/scala/stainless/evaluators/EvaluatorReport.scala index dfabef26ba..cd3812d779 100644 --- a/core/src/main/scala/stainless/evaluators/EvaluatorReport.scala +++ b/core/src/main/scala/stainless/evaluators/EvaluatorReport.scala @@ -57,7 +57,7 @@ class EvaluatorReport(val results: Seq[EvaluatorReport.Record], val sources: Set override lazy val annotatedRows = results map { case Record(id, pos, status, time) => - RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time) + RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time, None) } private lazy val totalTime = (results map { _.time }).sum diff --git a/core/src/main/scala/stainless/genc/GenCComponent.scala b/core/src/main/scala/stainless/genc/GenCComponent.scala index 67eb7dc10d..53a46b1a19 100644 --- a/core/src/main/scala/stainless/genc/GenCComponent.scala +++ b/core/src/main/scala/stainless/genc/GenCComponent.scala @@ -131,7 +131,7 @@ case class GenCReport(results: Seq[Record], sources: Set[Identifier], override v override val name = GenCComponent.name override def annotatedRows: Seq[RecordRow] = results.map { - case Record(id, pos, status, time) => RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time) + case Record(id, pos, status, time) => RecordRow(id, pos, levelOf(status), Seq(descriptionOf(status)), time, None) } protected def build(results: Seq[Record], sources: Set[Identifier]): GenCReport = diff --git a/core/src/main/scala/stainless/termination/TerminationReport.scala b/core/src/main/scala/stainless/termination/TerminationReport.scala index 728852cf62..682c9f25ba 100644 --- a/core/src/main/scala/stainless/termination/TerminationReport.scala +++ b/core/src/main/scala/stainless/termination/TerminationReport.scala @@ -68,7 +68,7 @@ class TerminationReport(val results: Seq[TerminationReport.Record], val sources: val symbol = if (status.isTerminating) "\u2713" else "\u2717" val extra = Seq(s"$symbol") - RecordRow(id, pos, level, extra, 0L) + RecordRow(id, pos, level, extra, 0L, None) } private def levelOf(status: Status) = status match { diff --git a/core/src/main/scala/stainless/testgen/GenCTestGen.scala b/core/src/main/scala/stainless/testgen/GenCTestGen.scala index 75d8df66c0..064c8d1da4 100644 --- a/core/src/main/scala/stainless/testgen/GenCTestGen.scala +++ b/core/src/main/scala/stainless/testgen/GenCTestGen.scala @@ -19,7 +19,7 @@ object GenCTestGen { (res: Map[VC[p.trees.type], VCResult[p.Model]]) (using ctx: inox.Context): Unit = { val counterExs = res.toSeq.collect { - case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => (vc, model) + case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => (vc, model) } if (counterExs.isEmpty) { return diff --git a/core/src/main/scala/stainless/testgen/ScalaTestGen.scala b/core/src/main/scala/stainless/testgen/ScalaTestGen.scala index 198583db8b..77c17e1084 100644 --- a/core/src/main/scala/stainless/testgen/ScalaTestGen.scala +++ b/core/src/main/scala/stainless/testgen/ScalaTestGen.scala @@ -25,7 +25,7 @@ object ScalaTestGen { (res: Map[VC[p.trees.type], VCResult[p.Model]]) (using ctx: inox.Context): Unit = { val counterExs = res.toSeq.collect { - case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _)) => (vc, model) + case (vc, VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), _, _, _)) => (vc, model) } if (counterExs.isEmpty) { return diff --git a/core/src/main/scala/stainless/verification/CoqVerificationChecher.scala b/core/src/main/scala/stainless/verification/CoqVerificationChecher.scala index 0f318a4e4e..a4cfd1cf93 100644 --- a/core/src/main/scala/stainless/verification/CoqVerificationChecher.scala +++ b/core/src/main/scala/stainless/verification/CoqVerificationChecher.scala @@ -38,7 +38,7 @@ trait CoqVerificationChecker { self => val pCoq = CoqEncoder.transformProgram(program, context) CoqIO.makeOutputDirectory() val files = CoqIO.writeToCoqFile(pCoq.map { case (id, name, com) => (name, com) } ) - val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None) + val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None, None) val vcs: Seq[VC] = pCoq map { case(fun, _, _) => VC(getFunction(fun).fullBody, fun, VCKind.CoqMethod, true).setPos(symbols.getFunction(fun)) } @@ -76,7 +76,7 @@ trait CoqVerificationChecker { self => case Failure(e) => reporter.internalError(e) } - vc -> VCResult(vcres, None, Some(time)) + vc -> VCResult(vcres, None, Some(time), None) }}.toMap initMap ++ res } diff --git a/core/src/main/scala/stainless/verification/VerificationAnalysis.scala b/core/src/main/scala/stainless/verification/VerificationAnalysis.scala index a7934a9d0a..88f11ccc52 100644 --- a/core/src/main/scala/stainless/verification/VerificationAnalysis.scala +++ b/core/src/main/scala/stainless/verification/VerificationAnalysis.scala @@ -22,7 +22,8 @@ trait VerificationAnalysis extends AbstractAnalysis { val time = vr.time.getOrElse(0L) // TODO make time mandatory (?) val status = VerificationReport.Status(program)(vr.status) val source = symbols.getFunction(vc.fid).source - VerificationReport.Record(vc.fid, vc.getPos, time, status, vr.solverName, vc.kind.name, derivedFrom = source) + val smtFileId = vr.smtLibFileId + VerificationReport.Record(vc.fid, vc.getPos, time, status, vr.solverName, vc.kind.name, derivedFrom = source, smtId = smtFileId) } override val name = VerificationComponent.name diff --git a/core/src/main/scala/stainless/verification/VerificationCache.scala b/core/src/main/scala/stainless/verification/VerificationCache.scala index 8fb7529494..dfed78709a 100644 --- a/core/src/main/scala/stainless/verification/VerificationCache.scala +++ b/core/src/main/scala/stainless/verification/VerificationCache.scala @@ -61,7 +61,7 @@ trait VerificationCache extends VerificationChecker { self => debugVC(vc, origVC) reporter.debug("--------------") } - VCResult(VCStatus.ValidFromCache, None, None) + VCResult(VCStatus.ValidFromCache, None, None, None) } else { reporter.synchronized { reporter.debug(s"Cache miss: '${vc.kind}' VC for ${vc.fid.asString} @${vc.getPos}...") @@ -94,7 +94,7 @@ trait VerificationCache extends VerificationChecker { self => // Update the result with the correct processing time tryResult match { case Failure(e) => reporter.internalError(e) - case Success(VCResult(status, solver, _)) => VCResult(status, solver, Some(time)) + case Success(VCResult(status, solver, _, smtLibFileId)) => VCResult(status, solver, Some(time), smtLibFileId) } } } diff --git a/core/src/main/scala/stainless/verification/VerificationChecker.scala b/core/src/main/scala/stainless/verification/VerificationChecker.scala index b7fc05f077..933580ee8c 100644 --- a/core/src/main/scala/stainless/verification/VerificationChecker.scala +++ b/core/src/main/scala/stainless/verification/VerificationChecker.scala @@ -117,7 +117,7 @@ trait VerificationChecker { self => } } - private lazy val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None) + private lazy val unknownResult: VCResult = VCResult(VCStatus.Unknown, None, None, None) def checkVCs(vcs: Seq[VC], stopWhen: VCResult => Boolean = defaultStop): Future[Map[VC, VCResult]] = { if (!VerificationChecker.startedVerification.getAndSet(true)) reporter.info("Starting verification...") @@ -280,7 +280,7 @@ trait VerificationChecker { self => import SolverResponses._ val cond = vc.condition if (cond == BooleanLiteral(true)) { - return VCResult(VCStatus.Trivial, None, None) + return VCResult(VCStatus.Trivial, None, None, None) } val s = sf.getNewSolver() @@ -300,10 +300,10 @@ trait VerificationChecker { self => s.check(Model) } } - + val vcres = tryRes match { case _ if interruptManager.isInterrupted => - VCResult(VCStatus.Cancelled, Some(s.name), Some(time)) + VCResult(VCStatus.Cancelled, Some(s.name), Some(time), s.getSmtLibFileId) case Success(res) => res match { case Unknown => @@ -313,35 +313,35 @@ trait VerificationChecker { self => case _ => VCStatus.Unknown } case _ => VCStatus.Unknown - }, Some(s.name), Some(time)) + }, Some(s.name), Some(time), s.getSmtLibFileId) case Unsat if !vc.satisfiability => - VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time)) + VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId) case SatWithModel(model) if checkModels && vc.kind.isInstanceOf[VCKind.AdtInvariant] => val VCKind.AdtInvariant(invId) = vc.kind: @unchecked val status = checkAdtInvariantModel(vc, invId, model) - VCResult(status, s.getResultSolver.map(_.name), Some(time)) + VCResult(status, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId) case SatWithModel(model) if !vc.satisfiability => - VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s.getResultSolver.map(_.name), Some(time)) + VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId) case Sat if vc.satisfiability => - VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time)) + VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId) case Unsat if vc.satisfiability => - VCResult(VCStatus.Invalid(VCStatus.Unsatisfiable), s.getResultSolver.map(_.name), Some(time)) + VCResult(VCStatus.Invalid(VCStatus.Unsatisfiable), s.getResultSolver.map(_.name), Some(time), s.getSmtLibFileId) case _ => sys.error(s"Unreachable: $res") } case Failure(u: inox.Unsupported) => reporter.warning(u.getMessage) - VCResult(VCStatus.Unsupported, Some(s.name), Some(time)) + VCResult(VCStatus.Unsupported, Some(s.name), Some(time), s.getSmtLibFileId) case Failure(e @ NotWellFormedException(d, info)) => reporter.error(d.getPos, e.getMessage) - VCResult(VCStatus.Crashed, Some(s.name), Some(time)) + VCResult(VCStatus.Crashed, Some(s.name), Some(time), s.getSmtLibFileId) case Failure(e) => reporter.internalError(e) } diff --git a/core/src/main/scala/stainless/verification/VerificationComponent.scala b/core/src/main/scala/stainless/verification/VerificationComponent.scala index f0bf555b48..c6a83541bf 100644 --- a/core/src/main/scala/stainless/verification/VerificationComponent.scala +++ b/core/src/main/scala/stainless/verification/VerificationComponent.scala @@ -116,11 +116,11 @@ class VerificationRun private(override val component: VerificationComponent.type val opaqueEncoder = inox.transformers.ProgramEncoder(vcGenEncoder.targetProgram)(OpaqueChooseInjector(vcGenEncoder.targetProgram)) val res: Future[Map[VC[p.trees.type], VCResult[p.Model]]] = if (context.options.findOptionOrDefault(optAdmitVCs)) { - Future(vcs.map(vc => vc -> VCResult(VCStatus.Admitted, None, None)).toMap) + Future(vcs.map(vc => vc -> VCResult(VCStatus.Admitted, None, None, None)).toMap) } else { VerificationChecker.verify(opaqueEncoder.targetProgram, context)(vcs).map(_.view.mapValues { - case VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s, t) => - VCResult(VCStatus.Invalid(VCStatus.CounterExample(model.encode(opaqueEncoder.reverse.andThen(vcGenEncoder.reverse)))), s, t) + case VCResult(VCStatus.Invalid(VCStatus.CounterExample(model)), s, t, smtid) => + VCResult(VCStatus.Invalid(VCStatus.CounterExample(model.encode(opaqueEncoder.reverse.andThen(vcGenEncoder.reverse)))), s, t, smtid) case res => res.asInstanceOf[VCResult[p.Model]] }.toMap) } diff --git a/core/src/main/scala/stainless/verification/VerificationConditions.scala b/core/src/main/scala/stainless/verification/VerificationConditions.scala index a20bc4ddca..b89db0bdf0 100644 --- a/core/src/main/scala/stainless/verification/VerificationConditions.scala +++ b/core/src/main/scala/stainless/verification/VerificationConditions.scala @@ -112,7 +112,8 @@ object VCStatus { case class VCResult[+Model]( status: VCStatus[Model], solverName: Option[String], - time: Option[Long] + time: Option[Long], + smtLibFileId: Option[Int] ) { def isValid = status == VCStatus.Valid || isValidFromCache || isTrivial def isValidFromCache = status == VCStatus.ValidFromCache diff --git a/core/src/main/scala/stainless/verification/VerificationReport.scala b/core/src/main/scala/stainless/verification/VerificationReport.scala index b3820fc86a..76872cb9b3 100644 --- a/core/src/main/scala/stainless/verification/VerificationReport.scala +++ b/core/src/main/scala/stainless/verification/VerificationReport.scala @@ -51,7 +51,7 @@ object VerificationReport { case class Record( id: Identifier, pos: inox.utils.Position, time: Long, status: Status, solverName: Option[String], kind: String, - derivedFrom: Identifier + derivedFrom: Identifier, smtId: Option[Int] ) extends AbstractReportHelper.Record given recordDecoder: Decoder[Record] = deriveDecoder @@ -84,12 +84,12 @@ class VerificationReport(val results: Seq[VerificationReport.Record], val source override val name = VerificationComponent.name override lazy val annotatedRows = results map { - case Record(id, pos, time, status, solverName, kind, _) => + case Record(id, pos, time, status, solverName, kind, _, smtId) => val level = levelOf(status) val solver = solverName getOrElse "" val extra = Seq(kind, status.name, solver) - RecordRow(id, pos, level, extra, time) + RecordRow(id, pos, level, extra, time, smtId) }