diff --git a/bin/package-standalone.sh b/bin/package-standalone.sh index e708f7b912..fcd864a65c 100755 --- a/bin/package-standalone.sh +++ b/bin/package-standalone.sh @@ -37,7 +37,7 @@ Z3_WIN_NAME="z3-$Z3_VERSION-x64-win.zip" CVC5_GITHUB_URL="https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION" CVC5_LICENSES_URL="https://raw.githubusercontent.com/cvc5/cvc5/main/licenses/" -CVC5_LICENSES=("antlr3-LICENSE" "gpl-3.0.txt" "lgpl-3.0.txt") +CVC5_LICENSES=("minisat-LICENSE" "gpl-3.0.txt" "lgpl-3.0.txt") CVC5_LINUX_NAME="cvc5-Linux" CVC5_MAC_ARM64_NAME="cvc5-macOS-arm64" CVC5_MAC_X64_NAME="cvc5-macOS" diff --git a/build.sbt b/build.sbt index 36cd446451..8502d8529a 100644 --- a/build.sbt +++ b/build.sbt @@ -278,7 +278,7 @@ val scriptSettings: Seq[Setting[_]] = Seq( def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) // lazy val inox = RootProject(file("../inox")) -lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "ae3eb97aaf50696bf416104ceae5b5d85be334db") +lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "3b02dcf4308f9e8d74ea82304bd651be8e93517f") lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc") // Allow integration test to use facilities from regular tests diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala index a06bd9bf2c..3a4fd71aa1 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] ) /** @@ -77,12 +78,24 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => /** Filter, sort & process rows. */ 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) + val rows = for { + 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) => f"smt-lib-$v" + case None => "" + } + contents = Position.smartPos(pos) +: (name +: ((extra :+ f"${time / 1000d}%3.1f" ) :+ t)) } yield Row(contents map { str => Cell(withColor(str, level)) }) + + // Delete the last cell if all are empty (i.e., the debug smt flag is false, and so smt-lib-id is empty) + val colorRegex = "\u001B\\[[;\\d]*m".r + if rows.forall(r => colorRegex.replaceAllIn(r.cells.last.vString, "").isBlank()) then { + rows.map(r => Row(r.cells.dropRight(1))) + } else { + rows + } } private def withColor(str: String, level: Level)(using inox.Context): String = @@ -105,7 +118,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 +127,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) }