Merges branch 'master' into 'parallel-type-checking'

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

@@ -303,7 +303,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
   private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
       val startMs = System.currentTimeMillis()
-      val res = EitherT.right[Vector[VerifierError], Future, BackendVerifier.Task](Translator.translate(program, pkgInfo)(config))
+      val res = EitherT.fromEither[Future, Vector[VerifierError], BackendVerifier.Task](Future.successful(Translator.translate(program, pkgInfo)(config)))
       logger.debug {
         val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
         s"Viper encoding done, took ${durationS}s"

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/resources/regressions/issues/000659.gobra

@@ -0,0 +1,33 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue659
+
+type Node struct {
+    ok     bool
+}
+
+pred (s *Set)mem(){
+    acc(s) &&
+    acc(s.nodes) &&
+    forall i int:: i in domain(s.nodes) ==> acc(s.nodes[i])
+}
+
+type Set struct {
+    nodes map[int]*Node
+}
+
+requires s.mem()
+requires acc(n)
+requires !(k in unfolding s.mem() in domain(s.nodes))
+func (s *Set) add2(n *Node, k int){
+    unfold s.mem()
+    _,ok := s.nodes[0];
+    if ok {
+        s.nodes[k] = n
+        fold s.mem()
+        //:: ExpectedOutput(assert_error:assertion_error)
+        assert false // should fail
+        return
+    }
+}

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 = NextStepEitherT("Viper verification", encoding, (viperTask: BackendVerifier.Task) => {