From 9772277565341634a700d78da22ad67aedd6557d Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 3 Jul 2023 12:03:33 +0200 Subject: [PATCH] improves reporting of consistency errors and errors resulting from applying Viper transformers --- src/main/scala/viper/gobra/Gobra.scala | 2 +- .../scala/viper/gobra/reporting/Message.scala | 8 +++++ .../viper/gobra/reporting/Reporter.scala | 1 + .../viper/gobra/reporting/VerifierError.scala | 6 +++- .../viper/gobra/translator/Translator.scala | 35 ++++++++++++++----- 5 files changed, 42 insertions(+), 10 deletions(-) diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index cb9e18620..3012d1d16 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -293,7 +293,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = { if (config.shouldViperEncode) { - Right(Translator.translate(program, pkgInfo)(config)) + Translator.translate(program, pkgInfo)(config) } else { Left(Vector()) } diff --git a/src/main/scala/viper/gobra/reporting/Message.scala b/src/main/scala/viper/gobra/reporting/Message.scala index 61530d91b..418e8e4db 100644 --- a/src/main/scala/viper/gobra/reporting/Message.scala +++ b/src/main/scala/viper/gobra/reporting/Message.scala @@ -173,6 +173,14 @@ case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAs lazy val vprAstFormatted: String = silver.ast.pretty.FastPrettyPrinter.pretty(vprAst()) } +case class TransformerFailureMessage(inputs: Vector[String], result: Vector[VerifierError]) extends GobraMessage { + override val name: String = s"transformer_failure_message" + + override def toString: String = s"transformer_failure_message(" + + s"files=$inputs, " + + s"failures=${result.map(_.toString).mkString(",")})" +} + case class ChoppedViperMessage(inputs: Vector[String], idx: Int, vprAst: () => vpr.Program, backtrack: () => BackTranslator.BackTrackInfo) extends GobraMessage { override val name: String = s"chopped_viper_message" diff --git a/src/main/scala/viper/gobra/reporting/Reporter.scala b/src/main/scala/viper/gobra/reporting/Reporter.scala index f4cffc761..0c6d7cb66 100644 --- a/src/main/scala/viper/gobra/reporting/Reporter.scala +++ b/src/main/scala/viper/gobra/reporting/Reporter.scala @@ -66,6 +66,7 @@ case class FileWriterReporter(name: String = "filewriter_reporter", } case m:ParserErrorMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) case m:TypeCheckFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) + case m:TransformerFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) case _ => // ignore } diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala index 858c2f2ae..a2877f4cb 100644 --- a/src/main/scala/viper/gobra/reporting/VerifierError.scala +++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala @@ -56,11 +56,15 @@ case class DiamondError(message: String) extends VerifierError { val id = "diamond_error" } -case class TimeoutError(message: String) extends VerifierError { +case class TimeoutError(message: String) extends VerifierError { val position: Option[SourcePosition] = None val id = "timeout_error" } +case class ConsistencyError(message: String, position: Option[SourcePosition]) extends VerifierError { + val id = "consistency_error" +} + sealed trait VerificationError extends VerifierError { def info: Source.Verifier.Info diff --git a/src/main/scala/viper/gobra/translator/Translator.scala b/src/main/scala/viper/gobra/translator/Translator.scala index 537b7d94f..63334f790 100644 --- a/src/main/scala/viper/gobra/translator/Translator.scala +++ b/src/main/scala/viper/gobra/translator/Translator.scala @@ -10,17 +10,28 @@ package viper.gobra.translator import viper.gobra.ast.internal.Program import viper.gobra.backend.BackendVerifier import viper.gobra.frontend.{Config, PackageInfo} -import viper.gobra.reporting.GeneratedViperMessage +import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError} import viper.gobra.translator.context.DfltTranslatorConfig import viper.gobra.translator.encodings.programs.ProgramsImpl import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer} import viper.gobra.util.Violation +import viper.silver.ast.{AbstractSourcePosition, SourcePosition} import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.verifier.AbstractError import viper.silver.{ast => vpr} object Translator { - def translate(program: Program, pkgInfo: PackageInfo)(config: Config): BackendVerifier.Task = { + private def createConsistencyErrors(errs: Seq[AbstractError]): Vector[ConsistencyError] = + errs.map(err => { + val pos = err.pos match { + case sp: AbstractSourcePosition => Some(new SourcePosition(sp.file, sp.start, sp.end)) + case _ => None + } + ConsistencyError(err.readableMessage, pos) + }).toVector + + def translate(program: Program, pkgInfo: PackageInfo)(config: Config): Either[Vector[VerifierError], BackendVerifier.Task] = { val translationConfig = new DfltTranslatorConfig() val programTranslator = new ProgramsImpl() val task = programTranslator.translate(program)(translationConfig) @@ -30,17 +41,25 @@ object Translator { new TerminationTransformer ) - val transformedTask = transformers.foldLeft(task) { - case (t, transformer) => transformer.transform(t) - .fold(errs => Violation.violation(s"Applying transformer ${transformer.getClass.getSimpleName} resulted in errors: ${errs.toString}"), identity) + val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) { + case (Right(t), transformer) => transformer.transform(t).left.map(createConsistencyErrors) + case (errs, _) => errs } if (config.checkConsistency) { - val errors = transformedTask.program.checkTransitively - if (errors.nonEmpty) Violation.violation(errors.toString) + transformedTask + .flatMap(task => { + val consistencyErrs = task.program.checkTransitively + if (consistencyErrs.isEmpty) Right(()) + else Left(createConsistencyErrors(consistencyErrs)) + }) + .left.map(errs => Violation.violation(errs.toString)) } - config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => sortAst(transformedTask.program), () => transformedTask.backtrack) + val inputs = config.packageInfoInputMap(pkgInfo).map(_.name) + transformedTask.fold( + errs => config.reporter report TransformerFailureMessage(inputs, errs), + task => config.reporter report GeneratedViperMessage(config.taskName, inputs, () => sortAst(task.program), () => task.backtrack)) transformedTask }