Merge pull request viperproject#658 from viperproject/auto-update-sub…

…modules

Update Submodules

src/main/resources/stubs/strconv/atoi.gobra

@@ -44,6 +44,7 @@ pure func (e *NumError) Unwrap() error { return e.Err }
 ghost
 requires exp >= 0
 ensures res == (exp == 0 ? 1 : (base * Exp(base, exp - 1)))
+decreases exp
 pure func Exp(base int, exp int) (res int) {
 	return exp == 0 ? 1 : (base * Exp(base, exp - 1))
 }

src/main/resources/stubs/strings/strings.gobra

@@ -202,6 +202,7 @@ func Map(mapping func(rune) rune, s string) string
 // the result of (len(s) * count) overflows.
 requires count >= 0
 ensures res == (count == 0? "" : s + Repeat(s, count - 1))
+decreases count
 pure func Repeat(s string, count int) (res string) /*{
 	if count == 0 {
 		return ""

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())
     }

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"
 

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
   }
 

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

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
   }
 

src/test/resources/regressions/features/closures/closures-calldesc2.gobra

@@ -33,6 +33,7 @@ func hof(ghost cs Calls, f func(ghost seq[int], int)int)(res int) {
 
 ghost
 ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)])
+decreases len(s)
 pure func seqSum(s seq[int]) (res int) {
     return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)]))
 }

src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra

@@ -112,6 +112,7 @@ func test2() {
 
 ghost
 ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)])
+decreases len(s)
 pure func seqSum(s seq[int]) (res int) {
     return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)]))
 }

src/test/scala/viper/gobra/DetailedBenchmarkTests.scala

@@ -142,7 +142,7 @@ class DetailedBenchmarkTests extends BenchmarkTests {
       val c = config.get
       assert(c.packageInfoInputMap.size == 1)
       val pkgInfo = c.packageInfoInputMap.keys.head
-      Right(Translator.translate(program, pkgInfo)(c))
+      Translator.translate(program, pkgInfo)(c)
     })
 
     private val verifying = NextStep("Viper verification", encoding, (viperTask: BackendVerifier.Task) => {