Merge remote-tracking branch 'origin/dev' into c-int-bool-coercion

examples/concepts/c/tagged_struct.c

@@ -7,9 +7,6 @@ struct FElement { struct Element e; float *d; };
 
 void print_int(int v);
 
-//@ context_everywhere Perm(INT_TAG, read);
-//@ context_everywhere Perm(FLOAT_TAG, read);
-//@ context_everywhere INT_TAG != FLOAT_TAG;
 void baz() {
     int a = 1; // o6
     float f; // o7

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

@@ -159,10 +159,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]
 
@@ -696,8 +696,9 @@ 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)
-    extends GlobalDeclaration[G] with HeapVariableImpl[G]
+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]
 @scopes[Variable]
@@ -1497,6 +1498,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,15 @@ 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 {
-      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) <> ";"
-    }
+  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)
+
+      }
+    decl <> init.map(i => Text(" = ") <> i).getOrElse(Text("")) <> ";"
+  }
 }

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

@@ -0,0 +1,12 @@
+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,14 @@
 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 +18,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

@@ -6,12 +6,11 @@ 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

@@ -6,12 +6,11 @@ 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

@@ -783,6 +783,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)) =>
@@ -2422,7 +2423,11 @@ 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/parsers/antlr4/LangCParser.g4

@@ -90,8 +90,8 @@ unaryExpression
     :   '++' unaryExpression
     |   '--' unaryExpression
     |   unaryOperator castExpression
-    |   'sizeof' unaryExpression
     |   'sizeof' '(' typeName ')'
+    |   'sizeof' unaryExpression
     |   '_Alignof' '(' typeName ')'
     |   '&&'  clangIdentifier // GCC extension address of label
     |   postfixExpression

src/parsers/vct/parsers/transform/CToCol.scala

@@ -891,8 +891,8 @@ case class CToCol[G](
           case "~" => BitNot(convert(arg), 0, signed = true)(blame(expr))
           case "!" => col.Not(convert(arg))
         }
-      case UnaryExpression3(_, _) => ??(expr)
-      case UnaryExpression4(_, _, tname, _) => SizeOf(convert(tname))
+      case UnaryExpression4(_, _) => ??(expr)
+      case UnaryExpression3(_, _, tname, _) => SizeOf(convert(tname))
       case UnaryExpression5(_, _, _, _) => ??(expr)
       case UnaryExpression6(_, _) => ??(expr)
       case UnaryExpression7(inner) => convert(inner)

src/rewrite/vct/rewrite/TypeQualifierCoercion.scala

@@ -1,12 +1,20 @@
 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
 
@@ -57,9 +65,12 @@ 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] {
 
@@ -71,6 +82,8 @@ case class TypeQualifierCoercion[Pre <: Generation]()
     (InstanceField[Pre], Map[InstanceField[Pre], BigInt]),
     InstanceField[Post],
   ] = mutable.Map()
+  private val constGlobalHeapsSucc
+      : SuccessionMap[HeapVariable[Pre], Function[Post]] = SuccessionMap()
 
   def createUniqueClassCopy(
       original: Class[Pre],
@@ -116,6 +129,28 @@ 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] = {
@@ -208,7 +243,35 @@ 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()
     }
   }