Merge branch 'master' of https://github.com/viperproject/silver

build.sbt

@@ -54,6 +54,8 @@ lazy val silver = (project in file("."))
     libraryDependencies += "org.jgrapht" % "jgrapht-core" % "1.5.0",                            // Graphs
     libraryDependencies += "org.slf4j" % "slf4j-api" % "1.7.30",                                // Logging
     libraryDependencies += "ch.qos.logback" % "logback-classic" % "1.2.3",                      // Logging
+    libraryDependencies += "com.lihaoyi" %% "requests" % "0.3.0",                               // Data collection
+    libraryDependencies += "com.lihaoyi" %% "upickle" % "1.0.0",                                // Data collection
 
     // Test settings.
     Test / parallelExecution := false,

src/main/resources/import/decreases/all.vpr

@@ -5,7 +5,7 @@ import "bool.vpr"
 import "int.vpr"
 import "multiset.vpr"
 import "predicate_instance.vpr"
-import "rational.vpr"
+import "perm.vpr"
 import "ref.vpr"
 import "seq.vpr"
 import "set.vpr"

src/main/resources/import/decreases/multiset.vpr

@@ -3,7 +3,7 @@
 
 import "declaration.vpr"
 
-domain MuliSetWellFoundedOrder[S]{
+domain MultiSetWellFoundedOrder[S]{
     //MultiSet
     axiom multiset_ax_dec{
         forall mSet1: Multiset[S], mSet2: Multiset[S] :: {decreasing(mSet1, mSet2)}

src/main/resources/import/decreases/perm.vpr

@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain PermWellFoundedOrder{
+	//Rationals
+    axiom rational_ax_dec{
+        forall int1: Perm, int2: Perm :: {decreasing(int1, int2)}
+            (int1 <= int2 - 1/1) ==> decreasing(int1, int2)
+    }
+    axiom rational_ax_bound{
+        forall int1: Perm :: {bounded(int1)}
+            int1 >= 0/1 ==> bounded(int1)
+    }
+}

src/main/scala/viper/silver/ast/Expression.scala

@@ -455,6 +455,7 @@ case class PredicateAccess(args: Seq[Exp], predicateName: String)
 
   def loc(p:Program) = p.findPredicate(predicateName)
   lazy val typ = Bool
+  override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
 
   /** The body of the predicate with the arguments instantiated correctly. */
   def predicateBody(program : Program, scope: Set[String]) = {

src/main/scala/viper/silver/ast/Position.scala

@@ -12,10 +12,13 @@ import java.nio.file.Path
 import viper.silver.parser.FastParser
 
 /** A trait describing the position of occurrence of an AST node. */
-sealed trait Position
+sealed trait Position {
+  def deltaColumn(delta: Int): Position
+}
 
 /** Describes ''no location'' for cases where a `Position` is expected, but not available. */
 case object NoPosition extends Position {
+  override def deltaColumn(delta: Int) = this
   override def toString = "<no position>"
 }
 
@@ -25,6 +28,13 @@ trait HasLineColumn extends Position {
 
   def column: Int
 
+  def <=(other: HasLineColumn): Boolean = {
+    if (line < other.line) true
+    else if (line > other.line) false
+    else column <= other.column
+  }
+
+  def deltaColumn(delta: Int): HasLineColumn
   override def toString = s"$line.$column"
 }
 
@@ -35,7 +45,9 @@ trait HasIdentifier extends HasLineColumn {
   def id: String
 }
 
-case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn
+case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn {
+  override def deltaColumn(delta: Int) = LineColumnPosition(line, column + delta)
+}
 
 /** Represents a source code position by referencing a file, a line and a column.
   * Optionally, an additional end position can be specified.
@@ -57,6 +69,7 @@ trait AbstractSourcePosition extends HasLineColumn {
   private def lineColComponent(lc_pos: HasLineColumn) =
     s"${lc_pos.line}.${lc_pos.column}"
 
+  override def deltaColumn(delta: Int): AbstractSourcePosition
   override def toString: String = end match {
     case None =>
       s"$fileComponent${lineColComponent(start)}"
@@ -79,12 +92,16 @@ object AbstractSourcePosition {
 class SourcePosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn])
   extends AbstractSourcePosition with StructuralEquality {
 
+  override def deltaColumn(delta: Int): SourcePosition =
+    new SourcePosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)))
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: Nil
 }
 
 class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn], val id: String)
   extends AbstractSourcePosition with StructuralEquality with HasIdentifier {
+  override def deltaColumn(delta: Int): IdentifierPosition =
+    new IdentifierPosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)), id)
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: id :: Nil
 }
@@ -122,13 +139,19 @@ case class TranslatedPosition(pos: AbstractSourcePosition) extends AbstractSourc
   val file: Path = pos.file
   val start: HasLineColumn = pos.start
   val end: Option[HasLineColumn] = pos.end
+  override def deltaColumn(delta: Int): TranslatedPosition =
+    new TranslatedPosition(pos.deltaColumn(delta))
 }
 
 case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.input.Position with HasLineColumn {
   override lazy val line: Int = vline
   override lazy val column: Int = col
   override lazy val lineContents: String = toString
   override lazy val toString: String = s"${file.getFileName}@$vline.$col"
+  override def deltaColumn(delta: Int): FilePosition = FilePosition(file, vline, col + delta)
+}
+object FilePosition {
+  def apply(pos: (Int, Int))(implicit file: Path): FilePosition = FilePosition(file, pos._1, pos._2)
 }
 
 /**
@@ -138,4 +161,5 @@ case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.i
   */
 case class VirtualPosition(identifier: String) extends Position {
   override def toString: String = identifier
+  override def deltaColumn(delta: Int): VirtualPosition = this
 }

src/main/scala/viper/silver/ast/Program.scala

@@ -214,18 +214,20 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     }
 
     def checkNamesInScope(currentScope: Scope, dMap: immutable.HashMap[String, Declaration]) : Seq[ConsistencyError] = {
-      var declarationMap = dMap
+      var newMap = immutable.HashMap.empty[String, Declaration]
       var s: Seq[ConsistencyError] = Seq.empty[ConsistencyError]
       //check name declarations
       currentScope.scopedDecls.foreach(l=> {
         if(!Consistency.validUserDefinedIdentifier(l.name))
           s :+= ConsistencyError(s"${l.name} is not a valid identifier.", l.pos)
 
-        declarationMap.get(l.name) match {
-          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier ${l.name} found.", l.pos)
-          case None => declarationMap += (l.name -> l)
+        newMap.get(l.name) match {
+          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier `${l.name}` found.", l.pos)
+          case None => newMap += (l.name -> l)
         }
       })
+      // Override duplicate keys in old map
+      val declarationMap = dMap ++ newMap
 
       //check name uses
       Visitor.visitOpt(currentScope.asInstanceOf[Node], Nodes.subnodes){ n => {
@@ -268,7 +270,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
 
   lazy val groundTypeInstances = DomainInstances.findNecessaryTypeInstances(this)
 
-  lazy val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods
+  val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods ++ extensions
 
   def findFieldOptionally(name: String): Option[Field] = this.fieldsByName.get(name)
 
@@ -409,11 +411,13 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   }
 
   def deepCollectInBody[A](f: PartialFunction[Node, A]): Seq[A] = body match {
+    case null => Nil
+    case None => Nil
     case Some(actualBody) => actualBody.deepCollect(f)
-    case None => Seq()
   }
 
-  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns
+  def labels: Seq[Label] = deepCollectInBody { case l: Label => l }
+  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns ++ labels
 
   override lazy val check: Seq[ConsistencyError] =
     pres.flatMap(Consistency.checkPre) ++
@@ -444,19 +448,6 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   def toCfg(simplify: Boolean = true, detect: Boolean = true): SilverCfg = CfgGenerator.methodToCfg(this, simplify, detect)
 }
 
-object MethodWithLabelsInScope {
-  def apply(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Seq[LocalVarDecl], pres: Seq[Exp], posts: Seq[Exp], body: Option[Seqn])
-                 (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): Method = {
-    val newBody = body match {
-      case Some(actualBody) =>
-        val newScopedDecls = actualBody.scopedSeqnDeclarations ++ actualBody.deepCollect({case l: Label => l})
-        Some(actualBody.copy(scopedSeqnDeclarations = newScopedDecls)(actualBody.pos, actualBody.info, actualBody.errT))
-      case _ => body
-    }
-    Method(name, formalArgs, formalReturns, pres, posts, newBody)(pos, info, errT)
-  }
-}
-
 /** A function declaration */
 case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres: Seq[Exp], posts: Seq[Exp], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Member with FuncLike with Contracted {
   override lazy val check : Seq[ConsistencyError] =
@@ -826,7 +817,7 @@ object BackendFunc {
 /**
   * The Extension Member trait provides the way to expand the Ast to include new Top Level declarations
   */
-trait ExtensionMember extends Member{
+trait ExtensionMember extends Member with Serializable {
   def extensionSubnodes: Seq[Node]
   def prettyPrint: PrettyPrintPrimitives#Cont
 }

src/main/scala/viper/silver/ast/Statement.scala

@@ -85,7 +85,7 @@ case class MethodCall(methodName: String, args: Seq[Exp], targets: Seq[LocalVar]
     if(!Consistency.noResult(this))
       s :+= ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)
     if (!Consistency.noDuplicates(targets))
-      s :+= ConsistencyError("Targets are not allowed to have duplicates", targets.head.pos)
+      s :+= ConsistencyError("Targets are not allowed to have duplicates", pos)
     s ++= args.flatMap(Consistency.checkPure)
     s
   }