Merge branch 'master' into quantified-magic-wand-maps

src/main/scala/viper/silver/parser/MacroExpander.scala

@@ -10,6 +10,7 @@ import viper.silver.ast.{FilePosition, Position, SourcePosition}
 import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder}
 import viper.silver.verifier.{ParseError, ParseReport, ParseWarning}
 
+import java.util
 import scala.collection.mutable
 
 case class MacroException(msg: String, pos: (Position, Position)) extends Exception
@@ -178,9 +179,16 @@ object MacroExpander {
     // Store the replacements from normal variable to freshly generated variable
     val renamesMap = mutable.Map.empty[String, String]
     var scopeAtMacroCall = Set.empty[String]
-    val scopeOfExpandedMacros = mutable.Set.empty[String]
+    val scopeOfExpandedMacros = new util.IdentityHashMap[PScope, mutable.Set[String]]()
+    var currentMacroScope: PScope = null
 
-    def scope: Set[String] = scopeAtMacroCall ++ scopeOfExpandedMacros
+    def scope: Set[String] = {
+      if (scopeOfExpandedMacros.containsKey(currentMacroScope)) {
+        scopeAtMacroCall ++ scopeOfExpandedMacros.get(currentMacroScope)
+      } else {
+        scopeAtMacroCall
+      }
+    }
 
     // Handy method to get a macro from its name string
     def getMacroByName(name: PIdnUse): PDefine = getMacro(name) match {
@@ -279,7 +287,7 @@ object MacroExpander {
           val freshVarName = getFreshVarName(varDecl.name)
 
           // Update scope
-          scopeOfExpandedMacros += freshVarName
+          scopeOfExpandedMacros.get(currentMacroScope) += freshVarName
           renamesMap += varDecl.name -> freshVarName
 
           // Create a variable with new name to substitute the previous one
@@ -289,7 +297,7 @@ object MacroExpander {
         } else {
 
           // Update scope
-          scopeOfExpandedMacros += varDecl.name
+          scopeOfExpandedMacros.get(currentMacroScope) += varDecl.name
 
           // Return the same variable
           varDecl
@@ -380,6 +388,49 @@ object MacroExpander {
 
           val newNode = try {
             scopeAtMacroCall = NameAnalyser().namesInScope(program, Some(macroCall))
+            ctx.parent match {
+              case s: PScope => currentMacroScope = s
+              case n => currentMacroScope = customGetEnclosingScope(n).get
+            }
+            if (!scopeOfExpandedMacros.containsKey(currentMacroScope)) {
+              scopeOfExpandedMacros.put(currentMacroScope, mutable.Set.empty)
+            }
+
+            // Since we're working on a parse AST that is in the process of being rewritten, some nodes don't have
+            // their parent node set (or they have it set incorrectly). As a result, n.getEnclosingScope may not
+            // work properly. Since we need this functionality, we re-implement it here using information from the
+            // context, in particular, the ancestors of the current node.
+            def customGetEnclosingScope(target: PNode): Option[PScope] = {
+              var foundTarget = false
+              for (current <- ctx.ancestorList.reverseIterator) {
+                if (foundTarget) {
+                  current match {
+                    case s: PScope => return Some(s)
+                    case _ =>
+                  }
+                } else {
+                  if (current eq target) {
+                    foundTarget = true
+                  }
+                }
+              }
+              return None
+            }
+
+            def allExpandedNamesOfAllSuperScopes(s: PScope): Unit = {
+              if (scopeOfExpandedMacros.containsKey(s)) {
+                scopeOfExpandedMacros.get(currentMacroScope) ++= scopeOfExpandedMacros.get(s)
+              }
+              customGetEnclosingScope(s) match {
+                case Some(s) => allExpandedNamesOfAllSuperScopes(s)
+                case _ =>
+              }
+            }
+
+            // If scopeOfExpandedMacros contains superscopes of s, these names are also visible in the current scope,
+            // and we have to add them to scopeOfExpandedMacros for the current scope.
+            allExpandedNamesOfAllSuperScopes(currentMacroScope)
+
             arguments.foreach(_.foreach(
               StrategyBuilder.SlimVisitor[PNode] {
                 case id: PIdnDef => scopeAtMacroCall += id.name

src/main/scala/viper/silver/parser/Resolver.scala

@@ -7,6 +7,7 @@
 package viper.silver.parser
 
 import viper.silver.FastMessaging
+import viper.silver.parser.PKw.Requires
 
 import scala.collection.mutable
 
@@ -685,8 +686,13 @@ case class TypeChecker(names: NameAnalyser) {
                           check(fd.typ)
                           fd.formalArgs foreach (a => check(a.typ))
                         }
-                        if (pfa.isDescendant[PAxiom] && pfn.pres.length != 0)
+                        if (pfa.isDescendant[PAxiom] && pfn.pres.toSeq.exists(pre => pre.k.rs == Requires)) {
+                          // A domain axiom, which must always be well-defined, is calling a function that has at least
+                          // one real precondition (i.e., not just a requires clause or something similar that's
+                          // temporarily represented as a precondition), which means that the call may not always be
+                          // well-defined. This is not allowed.
                           issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom")
+                        }
 
                       case pdf: PDomainFunction =>
                         val domain = pdf.domain

src/test/resources/all/issues/silicon/0847.vpr

@@ -0,0 +1,68 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function f1(i: Int): Int
+    decreases i
+    requires i > -2
+{
+    i > 0 ? 1 + f1(i - 1) : 0
+}
+
+function f2(i: Int): Int
+    decreases i
+{
+    i > 0 ? 1 + f2(i - 1) : 0
+}
+
+function f3(i: Int): Int
+    decreases i
+    ensures result >= 0
+{
+    i > 0 ? 1 + f3(i - 1) : 0
+}
+
+function f4(i: Int): Int
+    ensures result >= 0
+    decreases _
+{
+    i > 0 ? 1 + f4(i - 1) : 0
+}
+
+function f5(i: Int): Int
+    requires i > -2
+    decreases i
+    ensures result >= 0
+{
+    i > 0 ? 1 + f5(i - 1) : 0
+}
+
+domain t {
+    function fAlias1(Int): Int
+    function fAlias2(Int): Int
+    function fAlias3(Int): Int
+    function fAlias4(Int): Int
+    function fAlias5(Int): Int
+
+    axiom {
+        //:: ExpectedOutput(typechecker.error)
+        forall i: Int :: f1(i) == fAlias1(i)
+    }
+
+    axiom {
+        forall i: Int :: f2(i) == fAlias2(i)
+    }
+
+    axiom {
+        forall i: Int :: f3(i) == fAlias3(i)
+    }
+
+    axiom {
+        forall i: Int :: f4(i) == fAlias4(i)
+    }
+
+    axiom {
+        //:: ExpectedOutput(typechecker.error)
+        forall i: Int :: f5(i) == fAlias5(i)
+    }
+}

src/test/resources/all/issues/silver/0803.vpr

@@ -0,0 +1,30 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+define m1(res) {
+  res := var_m2
+}
+
+define m2(res) {
+  var var_m2: Int
+
+  var v0_1: Int
+  {
+    m1(v0_1)
+  }
+
+  res := var_m2
+}
+
+method caller() returns (value: Int)
+{
+  var res: Int
+  {
+    m2(res)
+  }
+  var value2: Int
+  {
+    m2(res)
+  }
+  value := res
+}