Allow the use of pointers to things that are not a reference type

src/main/vct/main/stages/Transformation.scala

@@ -23,7 +23,7 @@ import vct.options.types.{Backend, PathOrStd}
 import vct.resources.Resources
 import vct.result.VerificationError.SystemError
 import vct.rewrite.adt.ImportSetCompat
-import vct.rewrite.{EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, SmtlibToProverTypes}
+import vct.rewrite.{EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, SmtlibToProverTypes, VariableToPointer}
 import vct.rewrite.lang.ReplaceSYCLTypes
 import vct.rewrite.veymont.{DeduplicateSeqGuards, EncodeSeqBranchUnanimity, EncodeSeqProg, EncodeUnpointedGuard, GenerateSeqProgPermissions, SplitSeqGuards}
 
@@ -209,6 +209,7 @@ case class SilverTransformation
     EncodeChar,
 
     CollectLocalDeclarations, // all decls in Scope
+    VariableToPointer, // should happen before ParBlockEncoder so it can distinguish between variables which can and can't altered in a parallel block
     DesugarPermissionOperators, // no PointsTo, \pointer, etc.
     ReadToValue, // resolve wildcard into fractional permission
     TrivialAddrOf,

src/rewrite/vct/rewrite/DesugarPermissionOperators.scala

@@ -91,7 +91,7 @@ case class DesugarPermissionOperators[Pre <: Generation]() extends Rewriter[Pre]
           const(0) <= PointerBlockOffset(dispatch(p))(FramedPtrBlockOffset) + dispatch(idx) &*
           PointerBlockOffset(dispatch(p))(FramedPtrBlockOffset) + dispatch(idx) < PointerBlockLength(dispatch(p))(FramedPtrBlockLength) &*
           Perm(PointerLocation(PointerAdd(dispatch(p), dispatch(idx))(FramedPtrOffset))(FramedPtrOffset), dispatch(perm))
-      case other => rewriteDefault(other)
+      case other => other.rewriteDefault()
     }
   }
 }

src/rewrite/vct/rewrite/TrivialAddrOf.scala

@@ -37,7 +37,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] {
       val (newPointer, newTarget, newValue) = rewriteAssign(target, value, assign.blame, assign.o)
       val newAssign = PreAssignExpression(PointerSubscript(newTarget, const[Post](0))(PanicBlame("Should always be accessible")), newValue)(assign.blame)
       With(newPointer, newAssign)
-    case other => rewriteDefault(other)
+    case other => other.rewriteDefault()
   }
 
   override def dispatch(s: Statement[Pre]): Statement[Post] = s match {
@@ -46,7 +46,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] {
       val (newPointer, newTarget, newValue) = rewriteAssign(target, value, assign.blame, assign.o)
       val newAssign = Assign(PointerSubscript(newTarget, const[Post](0))(PanicBlame("Should always be accessible")), newValue)(assign.blame)
       Block(Seq(newPointer, newAssign))
-    case other => rewriteDefault(other)
+    case other => other.rewriteDefault()
   }
 
   // TODO: AddressOff needs a more structured approach. Now you could assign a local structure to a pointer, and that pointer

src/rewrite/vct/rewrite/VariableToPointer.scala

@@ -0,0 +1,116 @@
+package vct.rewrite
+
+import vct.col.ast._
+import vct.col.ref._
+import vct.col.origin._
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
+import vct.col.util.AstBuildHelpers._
+import vct.col.util.SuccessionMap
+import vct.result.VerificationError.UserError
+
+import scala.collection.mutable
+
+case object VariableToPointer extends RewriterBuilder {
+  override def key: String = "variableToPointer"
+
+  override def desc: String = "Translate every local and field to a pointer such that it can have its address taken"
+
+  case class UnsupportedAddrOf(loc: Expr[_]) extends UserError {
+    override def code: String = "unsupportedAddrOf"
+
+    override def text: String = loc.o.messageInContext("Taking an address of this expression is not supported")
+  }
+}
+
+case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
+
+  import VariableToPointer._
+
+  val addressedSet: mutable.Set[Node[Pre]] = new mutable.HashSet[Node[Pre]]()
+  val heapVariableMap: SuccessionMap[HeapVariable[Pre], HeapVariable[Post]] = SuccessionMap()
+  val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] = SuccessionMap()
+  val fieldMap: SuccessionMap[InstanceField[Pre], InstanceField[Post]] = SuccessionMap()
+
+  override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = {
+    addressedSet.addAll(program.collect {
+      case AddrOf(Local(Ref(v))) if !v.t.isInstanceOf[TClass[Pre]] => v
+      case AddrOf(DerefHeapVariable(Ref(v))) if !v.t.isInstanceOf[TClass[Pre]] => v
+      case AddrOf(Deref(_, Ref(f))) if !f.t.isInstanceOf[TClass[Pre]] => f
+    })
+    super.dispatch(program)
+  }
+
+  override def dispatch(decl: Declaration[Pre]): Unit = decl match {
+    case v: HeapVariable[Pre] if addressedSet.contains(v) => heapVariableMap(v) = globalDeclarations.declare(new HeapVariable(TPointer(dispatch(v.t)))(v.o))
+    case v: Variable[Pre] if addressedSet.contains(v) => variableMap(v) = variables.declare(new Variable(TPointer(dispatch(v.t)))(v.o))
+    case f: InstanceField[Pre] if addressedSet.contains(f) => fieldMap(f) = classDeclarations.declare(new InstanceField(TPointer(dispatch(f.t)), f.flags.map { it => dispatch(it) })(f.o))
+    case other => allScopes.anySucceed(other, other.rewriteDefault())
+  }
+
+  override def dispatch(stat: Statement[Pre]): Statement[Post] = {
+    implicit val o: Origin = stat.o
+    stat match {
+      case s: Scope[Pre] => s.rewrite(locals = variables.dispatch(s.locals), body = Block(s.locals.filter { local => addressedSet.contains(local) }.map { local =>
+        implicit val o: Origin = local.o
+        Assign(Local[Post](variableMap.ref(local)), NewPointerArray(variableMap(local).t.asPointer.get.element, const(1))(PanicBlame("Size is > 0")))(PanicBlame("Initialisation should always succeed"))
+      } ++ Seq(dispatch(s.body))))
+      case i@Instantiate(cls, out) =>
+        Block(Seq(i.rewriteDefault()) ++ cls.decl.declarations.flatMap {
+          case f: InstanceField[Pre]  =>
+            if (f.t.asClass.isDefined) {
+              Seq(
+                Assign(Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame("Initialisation should always succeed")), NewPointerArray(fieldMap(f).t.asPointer.get.element, const(1))(PanicBlame("Size is > 0")))(PanicBlame("Initialisation should always succeed")),
+                Assign(PointerSubscript(Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame("Initialisation should always succeed")), const[Post](0))(PanicBlame("Size is > 0")), dispatch(NewObject[Pre](f.t.asClass.get.cls)))(PanicBlame("Initialisation should always succeed"))
+              )
+            } else if (addressedSet.contains(f)) {
+              Seq(Assign(Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame("Initialisation should always succeed")), NewPointerArray(fieldMap(f).t.asPointer.get.element, const(1))(PanicBlame("Size is > 0")))(PanicBlame("Initialisation should always succeed")))
+            } else {
+              Seq()
+            }
+          case _ => Seq()
+        })
+      case other => other.rewriteDefault()
+    }
+  }
+
+  override def dispatch(expr: Expr[Pre]): Expr[Post] = {
+    implicit val o: Origin = expr.o
+    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) =>
+        DerefPointer(Local[Post](variableMap.ref(v)))(PanicBlame("Should always be accessible"))
+      case deref@Deref(obj, Ref(f)) if addressedSet.contains(f) =>
+        DerefPointer(Deref[Post](dispatch(obj), fieldMap.ref(f))(deref.blame))(PanicBlame("Should always be accessible"))
+      case newObject@NewObject(Ref(cls)) =>
+        val obj = new Variable[Post](TClass(succ(cls)))
+        ScopedExpr(Seq(obj), With(Block(
+          Seq(assignLocal(obj.get, newObject.rewriteDefault())) ++ cls.declarations.flatMap {
+            case f: InstanceField[Pre] =>
+              if (f.t.asClass.isDefined) {
+                Seq(
+                  Assign(Deref[Post](obj.get, anySucc(f))(PanicBlame("Initialisation should always succeed")), dispatch(NewObject[Pre](f.t.asClass.get.cls)))(PanicBlame("Initialisation should always succeed"))
+                )
+              } else if (addressedSet.contains(f)) {
+                Seq(Assign(Deref[Post](obj.get, fieldMap.ref(f))(PanicBlame("Initialisation should always succeed")), NewPointerArray(fieldMap(f).t.asPointer.get.element, const(1))(PanicBlame("Size is > 0")))(PanicBlame("Initialisation should always succeed")))
+              } else {
+                Seq()
+              }
+            case _ => Seq()
+          }), obj.get))
+      case other => other.rewriteDefault()
+    }
+  }
+
+  override def dispatch(loc: Location[Pre]): Location[Post] = {
+    implicit val o: Origin = loc.o
+    loc match {
+      case HeapVariableLocation(Ref(v)) if addressedSet.contains(v) => PointerLocation(DerefHeapVariable[Post](heapVariableMap.ref(v))(PanicBlame("Should always be accessible")))(PanicBlame("Should always be accessible"))
+      case FieldLocation(obj, Ref(f)) if addressedSet.contains(f) => PointerLocation(Deref[Post](dispatch(obj), fieldMap.ref(f))(PanicBlame("Should always be accessible")))(PanicBlame("Should always be accessible"))
+      case PointerLocation(AddrOf(Deref(obj, Ref(f)))) /* if addressedSet.contains(f) always true */ => FieldLocation[Post](dispatch(obj), fieldMap.ref(f))
+      case PointerLocation(AddrOf(DerefHeapVariable(Ref(v)))) /* if addressedSet.contains(v) always true */ => HeapVariableLocation[Post](heapVariableMap.ref(v))
+      case PointerLocation(AddrOf(local@Local(_))) => throw UnsupportedAddrOf(local)
+      case other => other.rewriteDefault()
+    }
+  }
+}