Merge branch 'master' into carbon-tests

docs/tutorial.md

@@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) {
 
 Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. 
 
-In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). 
+In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). 
 
 
 ## Interfaces
@@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY]
 To check the full list of flags available in Gobra, run the command
 ```bash
 java -jar gobra.jar -h
-```
+```

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/frontend/Desugar.scala

@@ -3736,7 +3736,7 @@ object Desugar {
       case t: Type.AdtClauseT =>
         val tAdt = Type.AdtT(t.adtT, t.context)
         val adt: in.AdtT = in.AdtT(nm.adt(tAdt), addrMod)
-        val fields: Vector[in.Field] = (t.fields map { case (key: String, typ: Type) =>
+        val fields: Vector[in.Field] = (t.fieldsWithTypes map { case (key: String, typ: Type) =>
           in.Field(nm.adtField(key, tAdt), typeD(typ, Addressability.mathDataStructureElement)(src), true)(src)
         }).toVector
         in.AdtClauseT(idName(t.decl.id, t.context.getTypeInfo), adt, fields, addrMod)

src/main/scala/viper/gobra/frontend/info/base/Type.scala

@@ -58,7 +58,17 @@ object Type {
 
   case class AdtT(decl: PAdtType, context: ExternalTypeInfo) extends Type
 
-  case class AdtClauseT(fields: Map[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type
+  case class AdtClauseT(fieldsToTypes: Map[String, Type], fields: Vector[String], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type {
+    require(fields.forall(fieldsToTypes.isDefinedAt), "there must be a type for each key")
+
+    def typeAt(idx: Int): Type = {
+      require(0 <= idx && idx < fields.size, s"index $idx is not within range of ADT fields (size ${fields.size})")
+      fieldsToTypes(fields(idx))
+    }
+
+    lazy val fieldsWithTypes: Vector[(String, Type)] = fields.map(f => (f, fieldsToTypes(f)))
+    lazy val fieldTypes: Vector[Type] = fieldsWithTypes.map(_._2)
+  }
 
   case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem")
 

src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala

@@ -184,7 +184,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
           if (elems.isEmpty) {
             successProp
           } else if (elems.exists(_.key.nonEmpty)) {
-            val tmap: Map[String, Type] = a.fields
+            val tmap: Map[String, Type] = a.fieldsToTypes
 
             failedProp("for adt literals either all or none elements must be keyed",
               !elems.forall(_.key.nonEmpty)) and
@@ -198,7 +198,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
               })
           } else if (elems.size == a.fields.size) {
             propForall(
-              elems.map(_.exp).zip(a.fields.values),
+              elems.map(_.exp).zip(a.fieldTypes),
               compositeValAssignableTo
             )
           } else {

src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala

@@ -94,9 +94,12 @@ trait NameResolution {
 
           case tree.parent.pair(decl: PAdtClause, adtDecl: PAdtType) => AdtClause(decl, adtDecl, this)
 
-          case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) => MatchVariable(decl, adt, this)
           case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchStmtCase, matchE: PMatchStatement)) =>
-            MatchVariable(decl, matchE.exp, this)
+            MatchVariable(decl, matchE.exp, this) // match full expression of match statement
+          case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchExpCase, matchE: PMatchExp)) =>
+            MatchVariable(decl, matchE.exp, this) // match full expression of match expression
+          case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) =>
+            MatchVariable(decl, adt, this) // match part of subexpression
 
           case c => Violation.violation(s"This case should be unreachable, but got $c")
         }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -145,8 +145,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
         case Some(p: ap.DomainFunction) => FunctionT(p.symb.args map p.symb.context.typ, p.symb.context.typ(p.symb.result))
 
         case Some(p: ap.AdtClause) =>
-          val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap
-          AdtClauseT(fields, p.symb.decl, p.symb.adtDecl, this)
+          val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ))
+          AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, this)
         case Some(p: ap.AdtField) =>
           p.symb match {
             case AdtDestructor(decl, _, context) => context.symbType(decl.typ)

src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala

@@ -157,8 +157,8 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
 
       // ADT clause is special since it is a type with a name that is not a named type
       case a: AdtClause =>
-        val types = a.fields.map(f => f.id.name -> a.context.symbType(f.typ)).toMap
-        AdtClauseT(types, a.decl, a.adtDecl, this)
+        val fields = a.fields.map(f => f.id.name -> a.context.symbType(f.typ))
+        AdtClauseT(fields.toMap, fields.map(_._1), a.decl, a.adtDecl, this)
 
       case BuiltInType(tag, _, _) => tag.typ
       case _ => violation(s"expected type, but got $id")

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -155,8 +155,8 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
         // ADT clause is special since it is a type with a name that is not a named type
         case Some(p: ap.AdtClause) =>
-          val types = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap
-          AdtClauseT(types, p.symb.decl, p.symb.adtDecl, p.symb.context)
+          val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ))
+          AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, p.symb.context)
 
         case _ => violation(s"expected type, but got $n")
       }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala

@@ -41,19 +41,19 @@ trait GhostIdTyping { this: TypeInfoImpl =>
     case func: DomainFunction => FunctionT(func.args map func.context.typ, func.context.typ(func.result.outs.head))
 
     case AdtClause(decl, adtDecl, context) =>
+      val fields = decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ))
       AdtClauseT(
-        decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ)).toMap,
+        fields.toMap,
+        fields.map(_._1),
         decl,
         adtDecl,
         context
       )
 
     case MatchVariable(decl, p, context) => p match {
       case PMatchAdt(clause, fields) =>
-        val argTypeWithIndex = context.symbType(clause).asInstanceOf[AdtClauseT].decl.args.flatMap(_.fields).map(_.typ).zipWithIndex
-        val fieldsWithIndex = fields.zipWithIndex
-        val fieldIndex = fieldsWithIndex.iterator.find(e => e._1 == decl).get._2
-        context.symbType(argTypeWithIndex.iterator.find(e => e._2 == fieldIndex).get._1)
+        val clauseT = context.symbType(clause).asInstanceOf[AdtClauseT]
+        clauseT.typeAt(fields.indexOf(decl))
 
       case e: PExpression => context.typ(e)
       case _ => violation("untypeable")

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala

@@ -54,8 +54,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
     case m: PMatchPattern => m match {
       case PMatchAdt(clause, fields) => symbType(clause) match {
         case t: AdtClauseT =>
-          val fieldTypes = fields map typ
-          val clauseFieldTypes = t.decl.args.flatMap(f => f.fields).map(f => symbType(f.typ))
+          val fieldTypes = fields.map(typ)
+          val clauseFieldTypes = t.fieldTypes
           error(m, s"Expected ${clauseFieldTypes.size} patterns, but got ${fieldTypes.size}", clauseFieldTypes.size != fieldTypes.size) ++
             fieldTypes.zip(clauseFieldTypes).flatMap(a => assignableTo.errors(a)(m))
         case _ => violation("Pattern matching only works on ADT Literals")
@@ -292,10 +292,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
             w eq _
           }
           val adtClauseT = underlyingType(typeSymbType(c)).asInstanceOf[AdtClauseT]
-          val flatFields = adtClauseT.decl.args.flatMap(f => f.fields)
-          if (index < flatFields.size) {
-            val field = flatFields(index)
-            typeSymbType(field.typ)
+          if (index < adtClauseT.fields.size) {
+            adtClauseT.typeAt(index)
           } else UnknownType // Error is found when PMatchADT is checked higher up the ADT
 
         case tree.parent.pair(_: PMatchExpCase, m: PMatchExp) => exprType(m.exp)

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/000651.gobra

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package test
+
+type A adt {
+	A_ {
+		a uint
+		b set[int]
+		c bool
+		d bool
+		e seq[int]
+	}
+}
+
+ghost
+decreases
+pure func f(x A) A {
+	return A_ {
+	a: x.a,
+	b: x.b,
+	c: x.c,
+	d: x.d,
+	e: x.e}
+}

src/test/resources/regressions/issues/000655.gobra

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package test
+
+// ##(-I ./000655/)
+import "pkg"
+
+ghost
+pure func foo(x pkg.List) bool {
+  return match x {
+    case pkg.Nil{}: true
+    case pkg.Cons{?head, pkg.Nil{}}: true
+    case _: false
+  }
+}

src/test/resources/regressions/issues/000655/pkg/f.gobra

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+type List adt {
+	Cons {
+		head int
+		tail List
+	}
+
+	Nil {}
+}
+

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
+    }
+}