Merge remote-tracking branch 'origin/dev' into InlinePallasContracts

src/col/vct/col/origin/Blame.scala

@@ -359,6 +359,16 @@ case class ContextEverywhereFailedInPost(
   override def inlineDescWithSource(node: String, failure: String): String =
     s"Context of `$node` may not hold in the postcondition, since $failure."
 }
+case class ContextEverywhereFailedInRunPost(
+    failure: ContractFailure,
+    node: RunMethod[_],
+) extends ContractedFailure with WithContractFailure {
+  override def baseCode: String = "contextRunPostFailed"
+  override def descInContext: String =
+    "Context may not hold in postcondition, since"
+  override def inlineDescWithSource(node: String, failure: String): String =
+    s"Context of `$node` may not hold in the postcondition, since $failure."
+}
 case class AutoValueLeakCheckFailed(
     failure: ContractFailure,
     node: ContractApplicable[_],

src/rewrite/vct/rewrite/EncodeByValueClassUsage.scala

@@ -212,11 +212,9 @@ case class EncodeByValueClassUsage[Pre <: Generation]() extends Rewriter[Pre] {
       case _ if inAssignment.nonEmpty => node.rewriteDefault()
       case Perm(ByValueClassLocation(e), p) =>
         unwrapClassPerm(dispatch(e), dispatch(p), e.t.asByValueClass.get)
-      case Perm(pl @ PointerLocation(dhv @ DerefHeapVariable(Ref(v))), p) =>
-        assert(
-          v.t.isInstanceOf[TNonNullPointer[Pre]],
-          "Frontends should ensure that HeapVariables are non-null pointers",
-        )
+      // Only doing this for TNonNullPointer pointers since those originate from the frontend and users can define heap variables of the normal TPointer pointer type
+      case Perm(pl @ PointerLocation(dhv @ DerefHeapVariable(Ref(v))), p)
+          if v.t.isInstanceOf[TNonNullPointer[Pre]] =>
         val t = v.t.asInstanceOf[TNonNullPointer[Pre]]
         if (t.element.asByValueClass.isDefined) {
           val newV: Ref[Post, HeapVariable[Post]] = succ(v)

src/rewrite/vct/rewrite/PropagateContextEverywhere.scala

@@ -24,6 +24,12 @@ case object PropagateContextEverywhere extends RewriterBuilder {
     override def blame(error: PostconditionFailed): Unit =
       app.blame.blame(ContextEverywhereFailedInPost(error.failure, app))
   }
+
+  case class ContextEverywhereRunPostconditionFailed(app: RunMethod[_])
+    extends Blame[PostconditionFailed] {
+    override def blame(error: PostconditionFailed): Unit =
+      app.blame.blame(ContextEverywhereFailedInRunPost(error.failure, app))
+  }
 }
 
 case class PropagateContextEverywhere[Pre <: Generation]()
@@ -60,6 +66,19 @@ case class PropagateContextEverywhere[Pre <: Generation]()
             }
           },
         ))
+      case runMethod: RunMethod[Pre] =>
+        allScopes.anyDeclare(allScopes.anySucceedOnly(
+          runMethod,
+          invariants.having(
+            invariants.top ++ unfoldStar(runMethod.contract.contextEverywhere)
+          ) {
+                runMethod.rewrite(blame =
+                  PostBlameSplit
+                    .left(ContextEverywhereRunPostconditionFailed(runMethod), runMethod.blame)
+                )
+          },
+        ))
+
       case other => rewriteDefault(other)
     }
 

src/rewrite/vct/rewrite/VariableToPointer.scala

@@ -48,7 +48,8 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
     SuccessionMap()
   val fieldMap: SuccessionMap[InstanceField[Pre], InstanceField[Post]] =
     SuccessionMap()
-  val noTransform: ScopedStack[Unit] = ScopedStack()
+  val noTransform: ScopedStack[scala.collection.Set[Variable[Pre]]] =
+    ScopedStack()
 
   override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = {
     // TODO: Replace the asByReferenceClass checks with something that more clearly communicates that we want to exclude all reference types
@@ -72,6 +73,7 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
         globalDeclarations.succeed(func, func.rewriteDefault())
       }
       case proc: Procedure[Pre] => {
+        val skipVars = mutable.Set[Variable[Pre]]()
         val extraVars = mutable.ArrayBuffer[(Variable[Post], Variable[Post])]()
         // Relies on args being evaluated before body
         allScopes.anySucceed(
@@ -84,6 +86,7 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
                   if (addressedSet.contains(v)) {
                     variableMap(v) =
                       new Variable(TNonNullPointer(dispatch(v.t)))(v.o)
+                    skipVars += v
                     extraVars += ((newV, variableMap(v)))
                   }
                 }
@@ -114,7 +117,9 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
                 }
               }
             },
-            contract = { noTransform.having(()) { dispatch(proc.contract) } },
+            contract = {
+              noTransform.having(skipVars) { dispatch(proc.contract) }
+            },
           ),
         )
       }
@@ -199,14 +204,13 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
 
   override def dispatch(expr: Expr[Pre]): Expr[Post] = {
     implicit val o: Origin = expr.o
-    if (noTransform.nonEmpty)
-      return expr.rewriteDefault()
     expr match {
       case deref @ DerefHeapVariable(Ref(v)) if addressedSet.contains(v) =>
         DerefPointer(
           DerefHeapVariable[Post](heapVariableMap.ref(v))(deref.blame)
         )(PanicBlame("Should always be accessible"))
-      case Local(Ref(v)) if addressedSet.contains(v) =>
+      case Local(Ref(v))
+          if addressedSet.contains(v) && !noTransform.exists(_.contains(v)) =>
         DerefPointer(Local[Post](variableMap.ref(v)))(PanicBlame(
           "Should always be accessible"
         ))
@@ -251,14 +255,34 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
             obj.get,
           ),
         )
+      case Perm(PointerLocation(AddrOf(DerefHeapVariable(Ref(v)))), perm)
+          if addressedSet.contains(v) =>
+        val newPerm = dispatch(perm)
+        Star(
+          Perm(HeapVariableLocation[Post](heapVariableMap.ref(v)), newPerm),
+          Perm(
+            PointerLocation(DerefHeapVariable[Post](heapVariableMap.ref(v))(
+              PanicBlame("Access is framed")
+            ))(PanicBlame("Cannot be null")),
+            newPerm,
+          ),
+        )
+      case Value(PointerLocation(AddrOf(DerefHeapVariable(Ref(v)))))
+          if addressedSet.contains(v) =>
+        Star(
+          Value(HeapVariableLocation[Post](heapVariableMap.ref(v))),
+          Value(
+            PointerLocation(DerefHeapVariable[Post](heapVariableMap.ref(v))(
+              PanicBlame("Access is framed")
+            ))(PanicBlame("cannot be null"))
+          ),
+        )
       case other => other.rewriteDefault()
     }
   }
 
   override def dispatch(loc: Location[Pre]): Location[Post] = {
     implicit val o: Origin = loc.o
-    if (noTransform.nonEmpty)
-      return loc.rewriteDefault()
     loc match {
       case HeapVariableLocation(Ref(v)) if addressedSet.contains(v) =>
         PointerLocation(

test/main/vct/test/integration/examples/ForkJoinSpec.scala

@@ -9,4 +9,27 @@ class ForkJoinSpec extends VercorsSpec {
   vercors should verify using anyBackend example "concepts/forkjoin/fibonacci.pvl"
   vercors should verify using anyBackend examples("concepts/forkjoin/OwickiGries.pvl", "concepts/forkjoin/Worker.pvl")
   vercors should error withCode "runnableMethodMissing" example "concepts/forkjoin/TestFork.pvl"
+  vercors should verify using anyBackend in "The context_everywhere of a run method" pvl
+    """
+    pure int f();
+
+    class C {
+      context_everywhere f() == 3;
+      run {
+        assert f() == 3;
+      }
+    }
+
+    requires f() == 3;
+    void main() {
+        C c = new C();
+        fork c;
+        join c;
+    }
+    """
+
+
+
+
+
 }