Some fixes to const pointers and clean up variable to pointer

src/col/vct/col/ast/Node.scala

@@ -157,10 +157,10 @@ final case class TPointer[G](element: Type[G], unique: Option[BigInt])(
 final case class TNonNullPointer[G](element: Type[G], unique: Option[BigInt])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullPointerImpl[G]
-final case class TConstPointer[G](pureElement: Type[G])(
+final case class TConstPointer[G](element: Type[G])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TConstPointerImpl[G]
-final case class TNonNullConstPointer[G](pureElement: Type[G])(
+final case class TNonNullConstPointer[G](element: Type[G])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullConstPointerImpl[G]
 
@@ -692,7 +692,7 @@ final case class ModelDo[G](
 @family
 sealed trait GlobalDeclaration[G]
     extends Declaration[G] with GlobalDeclarationImpl[G]
-final class HeapVariable[G](val t: Type[G])(implicit val o: Origin)
+final class HeapVariable[G](val t: Type[G], val init: Option[Expr[G]])(implicit val o: Origin)
     extends GlobalDeclaration[G] with HeapVariableImpl[G]
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin)
     extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
@@ -1484,6 +1484,8 @@ final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(
     extends Expr[G] with PointerAddImpl[G]
 final case class AddrOf[G](e: Expr[G])(implicit val o: Origin)
     extends Expr[G] with AddrOfImpl[G]
+final case class AddrOfConstCast[G](e: Expr[G])(implicit val o: Origin)
+  extends Expr[G] with AddrOfConstCastImpl[G]
 final case class FunctionOf[G](
     binding: Ref[G, Variable[G]],
     vars: Seq[Ref[G, Variable[G]]],

src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala

@@ -6,11 +6,14 @@ import vct.col.ast.ops.HeapVariableOps
 
 trait HeapVariableImpl[G] extends HeapVariableOps[G] {
   this: HeapVariable[G] =>
-  override def layout(implicit ctx: Ctx): Doc =
-    ctx.syntax match {
+  override def layout(implicit ctx: Ctx): Doc = {
+    val decl: Doc = ctx.syntax match {
       case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
         val (spec, decl) = t.layoutSplitDeclarator
-        spec <+> decl <> ctx.name(this) <> ";"
-      case _ => t.show <+> ctx.name(this) <> ";"
+        spec <+> decl <> ctx.name(this)
+      case _ => t.show <+> ctx.name(this)
+
     }
+    decl <> init.map(i => Text(" = ") <> i).getOrElse(Text("")) <> ";"
+  }
 }

src/col/vct/col/ast/expr/heap/read/AddrOfConstCastImpl.scala

@@ -0,0 +1,11 @@
+package vct.col.ast.expr.heap.read
+
+import vct.col.ast.{AddrOfConstCast, TConst}
+import vct.col.ast.ops.AddrOfConstCastOps
+import vct.col.print._
+
+trait AddrOfConstCastImpl[G] extends AddrOfConstCastOps[G] { this: AddrOfConstCast[G] =>
+  override lazy val t = TConst(e.t)
+
+  override def layout(implicit ctx: Ctx): Doc = Text("constCast(") <> e <> ")"
+}

src/col/vct/col/ast/expr/heap/read/AddrOfImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr.heap.read
 
-import vct.col.ast.{AddrOf, TPointer, Type, DerefPointer, AmbiguousSubscript}
+import vct.col.ast.{AddrOf, AddrOfConstCast, TPointer, TConstPointer, Type, DerefPointer, AmbiguousSubscript}
 import vct.col.print._
 import vct.col.ast.ops.AddrOfOps
 
@@ -10,6 +10,7 @@ trait AddrOfImpl[G] extends AddrOfOps[G] {
     e match {
       case DerefPointer(p) => p.t
       case AmbiguousSubscript(p, i) => p.t
+      case AddrOfConstCast(e) => TConstPointer(e.t)
       case _ => TPointer(e.t, None)
     }
   }

src/col/vct/col/ast/type/TConstPointerImpl.scala

@@ -5,12 +5,11 @@ import vct.col.ast.ops.TConstPointerOps
 import vct.col.print._
 
 trait TConstPointerImpl[G] extends TConstPointerOps[G] { this: TConstPointer[G] =>
-  val element: Type[G] = TConst[G](pureElement)
   val unique: Option[BigInt] = None
 
   val isConst = true
   val isNonNull = false
 
   override def layout(implicit ctx: Ctx): Doc =
-    Text("const_pointer") <> open <> pureElement <> close
+    Text("const_pointer") <> open <> element <> close
 }

src/col/vct/col/ast/type/TNonNullConstPointerImpl.scala

@@ -5,12 +5,11 @@ import vct.col.ast.ops.TNonNullConstPointerOps
 import vct.col.print._
 
 trait TNonNullConstPointerImpl[G] extends TNonNullConstPointerOps[G] { this: TNonNullConstPointer[G] =>
-  val element: Type[G] = TConst[G](pureElement)
   val unique: Option[BigInt] = None
 
   val isConst = true
   val isNonNull = true
 
   override def layout(implicit ctx: Ctx): Doc =
-    Text("constNonNullPointer") <> open <> pureElement <> close
+    Text("constNonNullPointer") <> open <> element <> close
 }

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -780,6 +780,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
         ActionApply(action, coerceArgs(args, action.decl))
       case ActionPerm(loc, perm) => ActionPerm(loc, rat(perm))
       case AddrOf(e) => AddrOf(e)
+      case AddrOfConstCast(e) => AddrOfConstCast(e)
       case ADTFunctionInvocation(typeArgs, ref, args) =>
         typeArgs match {
           case Some((adt, typeArgs)) =>
@@ -2415,7 +2416,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
         new CTranslationUnit(unit.declarations)
       case unit: CPPTranslationUnit[Pre] =>
         new CPPTranslationUnit(unit.declarations)
-      case variable: HeapVariable[Pre] => new HeapVariable(variable.t)
+      case variable: HeapVariable[Pre] =>
+        new HeapVariable(variable.t, variable.init.map(i => coerce(i, variable.t)))
       case rule: SimplificationRule[Pre] =>
         new SimplificationRule[Pre](bool(rule.axiom))
       case dataType: AxiomaticDataType[Pre] => dataType

src/rewrite/vct/rewrite/TypeQualifierCoercion.scala

@@ -1,12 +1,14 @@
 package vct.rewrite
 
-import vct.col.ast.{Expr, Type, _}
-import vct.col.origin.Origin
+import vct.col.ast._
+import vct.col.origin.{AbstractApplicable, AssignLocalOk, Origin, PanicBlame, TrueSatisfiable}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
 import vct.col.typerules.CoercingRewriter
+import vct.col.util.AstBuildHelpers._
 import vct.result.VerificationError.UserError
 import hre.util.ScopedStack
-import vct.col.ref.{LazyRef, Ref}
+import vct.col.ref.LazyRef
+import vct.col.util.SuccessionMap
 
 import scala.collection.mutable
 
@@ -47,15 +49,18 @@ case object TypeQualifierCoercion extends RewriterBuilder {
   def getUniqueMap[G](t: TClassUnique[G]): Map[InstanceField[G], BigInt] = {
     t.uniqueMap.map {case (ref, unique) => (ref.decl, unique)}.toMap
   }
-
-
 }
 
+/* This rewrite step removes type qualifiers TUnique, TConst and TClassUnique.
+ * Some of them were okay to coerce, thus we the node `UniquePointerCoercion` which the pass
+ * MakeUniqueMethodCopies removes again to make the coercion correct by adding method/function copies
+ */
 case class TypeQualifierCoercion[Pre <: Generation]()
   extends CoercingRewriter[Pre] {
 
   val uniqueClasses: mutable.Map[(Class[Pre], Map[InstanceField[Pre], BigInt]), Class[Post]] = mutable.Map()
   val uniqueField: mutable.Map[(InstanceField[Pre], Map[InstanceField[Pre], BigInt]), InstanceField[Post]] = mutable.Map()
+  private val constGlobalHeapsSucc: SuccessionMap[HeapVariable[Pre], Function[Post]] = SuccessionMap()
 
   def createUniqueClassCopy(original: Class[Pre], pointerInstanceFields: Map[InstanceField[Pre], BigInt]): Class[Post] = {
       globalDeclarations.declare({
@@ -89,6 +94,26 @@ case class TypeQualifierCoercion[Pre <: Generation]()
       })
   }
 
+  override def coerce(decl: Declaration[Pre]): Declaration[Pre] = decl match {
+    // Turn of coercions for a sec, otherwise we cannot use our constGlobalHeapsSucc successfully
+    case h: HeapVariable[Pre] if isConstElement(h.t) => h
+    case other => super.coerce(other)
+  }
+
+  override def postCoerce(d: Declaration[Pre]): Unit = d match {
+    case h: HeapVariable[Pre] if isConstElement(h.t) =>
+      val f = globalDeclarations.declare({
+        function(
+          blame = AbstractApplicable,
+          contractBlame = TrueSatisfiable,
+          returnType = dispatch(h.t),
+          body = h.init.map(dispatch)
+        )(h.o)
+      })
+      constGlobalHeapsSucc(h) = f
+    case other => allScopes.anySucceed(other, other.rewriteDefault())
+  }
+
   override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
     implicit o: Origin
   ): Expr[Post] = {
@@ -162,7 +187,25 @@ case class TypeQualifierCoercion[Pre <: Generation]()
             d.rewrite(ref = uniqueField(ref.decl, map).ref)
           case _ => d.rewriteDefault()
         }
-
+      case DerefHeapVariable(ref) if isConstElement(ref.decl.t) =>
+        functionInvocation(TrueSatisfiable, constGlobalHeapsSucc.ref(ref.decl))
+      case a@AddrOf(deref@DerefHeapVariable(ref)) if isConstElement(ref.decl.t) =>
+        implicit val o: Origin = a.o
+        val t = dispatch(ref.decl.t)
+        val v = new Variable[Post](TNonNullConstPointer(t))
+        val l = Local[Post](v.ref)
+        val newP = NewNonNullConstPointerArray(dispatch(ref.decl.t), const(1))(PanicBlame("Size >0"))(a.o)
+        ScopedExpr(Seq(v),
+          With[Post](Block(Seq(
+            Assign(l, newP)(AssignLocalOk),
+            Assume(DerefPointer(l)(PanicBlame("Not null & Size>0")) === dispatch(deref))
+          )),
+          l
+          )
+        )
+      case a@AddrOf(e) if isConstElement(e.t) =>
+        if(e.collectFirst {case Deref(_, _) => ()}.isDefined) throw DisallowedQualifiedType(e)
+        AddrOf(AddrOfConstCast(postCoerce(e)))
       case other => other.rewriteDefault()
     }
   }