Merge pull request #1085 from utwente-fmt/issue-742

fix #742: yields variables are not referencable in requires/context/c_e

src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala

@@ -10,9 +10,14 @@ trait ApplicableContractImpl[G] extends NodeFamilyImpl[G] { this: ApplicableCont
     this match {
       // Redundant match so this doesn't compile if we add a field to ApplicableContract
       case ApplicableContract(requires, ensures, contextEverywhere, signals, givenArgs, yieldsArgs, decreases) =>
-        f(context, requires) +: f(context.withPostcondition, ensures) +: f(context, contextEverywhere) +:
-          (signals.map(f(context, _)) ++ givenArgs.map(f(context, _)) ++ yieldsArgs.map(f(context, _)) ++
-          decreases.toSeq.map(f(context, _)))
+        f(context.withUndeclared(yieldsArgs), requires) +:
+          f(context.withPostcondition, ensures) +:
+          f(context.withUndeclared(yieldsArgs), contextEverywhere) +: (
+            signals.map(f(context, _)) ++
+              givenArgs.map(f(context, _)) ++
+              yieldsArgs.map(f(context, _)) ++
+              decreases.toSeq.map(f(context.withUndeclared(yieldsArgs), _))
+          )
     }
 
   def isEmpty: Boolean = this match {

src/col/vct/col/check/Check.scala

@@ -88,6 +88,7 @@ case object CheckContext {
 case class CheckContext[G]
 (
   scopes: Seq[CheckContext.ScopeFrame[G]] = Seq(),
+  undeclared: Seq[Seq[Declaration[G]]] = Nil,
   roScopes: Int = 0, roScopeReason: Option[Node[G]] = None,
   currentApplicable: Option[Applicable[G]] = None,
   inPostCondition: Boolean = false,
@@ -109,11 +110,14 @@ case class CheckContext[G]
   def withPostcondition: CheckContext[G] =
     copy(inPostCondition = true)
 
+  def withUndeclared(decls: Seq[Declaration[G]]): CheckContext[G] =
+    copy(undeclared = undeclared :+ decls)
+
   def inScope[Decl <: Declaration[G]](ref: Ref[G, Decl]): Boolean =
-    scopes.exists(_.contains(ref.decl))
+    !undeclared.exists(_.contains(ref.decl)) && scopes.exists(_.contains(ref.decl))
 
   def inWriteScope[Decl <: Declaration[G]](ref: Ref[G, Decl]): Boolean =
-    scopes.drop(roScopes).exists(_.contains(ref.decl))
+    !undeclared.exists(_.contains(ref.decl)) && scopes.drop(roScopes).exists(_.contains(ref.decl))
 
   def checkInScope[Decl <: Declaration[G]](use: Node[G], ref: Ref[G, Decl]): Seq[CheckError] =
     if(inScope(ref)) Nil

src/col/vct/col/resolve/Resolve.scala

@@ -194,14 +194,14 @@ case object ResolveReferences extends LazyLogging {
 
     val childErrors = node match {
       case l @ Let(binding, value, main) =>
-        val innerCtx = enterContext(node, ctx, inGPU).copy(checkContext = l.enterCheckContext(ctx.checkContext))
+        val innerCtx = enterContext(node, ctx, inGPU).withCheckContext(l.enterCheckContext(ctx.checkContext))
         resolve(binding, innerCtx) ++
         resolve(value, ctx) ++
         resolve(main, innerCtx)
       case _ =>
         val innerCtx = enterContext(node, ctx, inGPU)
         node.checkContextRecursor(ctx.checkContext, { (ctx, node) =>
-          resolve(node, innerCtx.copy(checkContext = ctx), inGPU)
+          resolve(node, innerCtx.withCheckContext(ctx), inGPU)
         }).flatten
     }
 

src/col/vct/col/resolve/ctx/ReferenceResolutionContext.scala

@@ -34,6 +34,14 @@ case class ReferenceResolutionContext[G]
   def declare(decls: Seq[Declaration[G]]): ReferenceResolutionContext[G] =
     copy(stack = decls.flatMap(Referrable.from) +: stack)
 
+  def withCheckContext(ctx: CheckContext[G]): ReferenceResolutionContext[G] = {
+    val filter = ctx.undeclared.flatten.flatMap(Referrable.from).toSet
+    copy(
+      checkContext = ctx,
+      stack = stack.map(_.filter(!filter.contains(_)))
+    )
+  }
+
   /* State predicates names are saved as expr's here because at the time this method is called, fields are not yet resolved.
      E.g. if in the code it says "@Guard(name = INIT)", where INIT is some static field, in the ast INIT is a LocalVariable.
      It is only after recursively visiting this annotation that INIT is resolved to a static field. So we save the expr

test/main/vct/test/integration/features/ResolutionSpec.scala

@@ -38,4 +38,13 @@ class ResolutionSpec extends VercorsSpec {
       static void bar() {}
     }
   """
+
+  vercors should error withCode "noSuchName" in "example where yields variable is named in precondition" pvl """
+    yields int[] indegree;
+    requires indegree != null ** indegree.length > 0;
+    requires Perm(indegree[0], write) ** indegree[0] == 0;
+    boolean m() {
+      assert \old(indegree[0]) == 0;
+    }
+  """
 }