Support for qualified functions

src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.expr.misc
+
+import vct.col.ast.UniquePointerCoercion
+import vct.col.ast.ops.UniquePointerCoercionOps
+import vct.col.print._
+
+trait UniquePointerCoercionImpl[G] extends UniquePointerCoercionOps[G] { this: UniquePointerCoercion[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

src/parsers/antlr4/CParser.g4

@@ -20,4 +20,6 @@ specFalse: 'false';
 startSpec: LineStartSpec {specLevel++;} | BlockStartSpec {specLevel++;} | BlockStartSpecImmediate {specLevel++;};
 endSpec: EndSpec {specLevel--;};
 
-typeSpecifierWithPointerOrArray : typeSpecifier | typeSpecifier '[' ']' | typeSpecifier '*';
+typeSpecifierWithPointerOrArray : specifierQualifierList
+    | specifierQualifierList '[' ']'
+    | specifierQualifierList '*';

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

@@ -1005,11 +1005,11 @@ case class CToCol[G](
   def convert(t: TypeSpecifierWithPointerOrArrayContext): Type[G] =
     t match {
       case TypeSpecifierWithPointerOrArray0(typeSpec) =>
-        CPrimitiveType(Seq(convert(typeSpec)))
+        CPrimitiveType(convert(typeSpec))
       case TypeSpecifierWithPointerOrArray1(typeSpec, _, _) =>
-        CTArray(None, CPrimitiveType(Seq(convert(typeSpec))))(blame(t))
+        CTArray(None, CPrimitiveType(convert(typeSpec)))(blame(t))
       case TypeSpecifierWithPointerOrArray2(typeSpec, _) =>
-        CTPointer(CPrimitiveType(Seq(convert(typeSpec))))
+        CTPointer(CPrimitiveType(convert(typeSpec)))
     }
 
   def convert(id: LangIdContext): String =

src/rewrite/vct/rewrite/TypeQualifierCoercion.scala

@@ -251,12 +251,13 @@ case class MakeUniqueMethodCopies[Pre <: Generation]()
   }
 
   // Same for functions
-  def createAbstractFunctionCopy(original: Function[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Function[Post] = {
+  def createFunctionCopy(original: Function[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Function[Post] = {
     methodCopyTypes.having(typeCoerced) {
       globalDeclarations.declare({
         // Subtle, need to create variable scope, otherwise variables are already 'succeeded' in different copies.
         variables.scope({
-          original.rewrite(body = None)
+          // We do copy body, otherwise functions could be different.
+          original.rewrite()
         })
       })
     }
@@ -279,13 +280,46 @@ case class MakeUniqueMethodCopies[Pre <: Generation]()
     inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs)
   }
 
+  def rewriteFunctionInvocation(inv: FunctionInvocation[Pre], returnCoercion: Option[UniqueCoercion], anyReturnPointer: Boolean = false): FunctionInvocation[Post] = {
+    val f = inv.ref.decl
+    val allArgs: Seq[Args] = Seq(addArgs(f.args, inv.args))
+    if(argsNoCoercions(allArgs) && returnCoercion.isEmpty){
+      if(methodCopyTypes.nonEmpty){
+        val map = methodCopyTypes.top
+        // So we are already coercing. Let's see if we need to change anything.
+        if(f.args.exists(v => map.contains(v.t)) || map.contains(f.returnType) ) {
+          // So yes, we just use the same map we were already using
+          val newFunc: Function[Post] =
+            abstractFunction.getOrElseUpdate((f, map), createFunctionCopy(f, map))
+          val newArgs = removeCoercions(inv.args)
+          return inv.rewrite(ref = newFunc.ref, args=newArgs)
+        }
+      }
+
+      return inv.rewriteDefault()
+    }
+    // Coercing a function call, whilst we are already coercing seems quite complicated.
+    // So let's not do that for now.
+    if(methodCopyTypes.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o)
+
+    if(callee.top == f) throw DisallowedQualifiedMethodCoercion(inv.o)
+    // Yields and givens are not supported for now (is possible)
+    if(inv.givenMap.nonEmpty || inv.yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o)
+
+    val map = getCoercionMapAndCheck(allArgs, f.returnType, returnCoercion, anyReturnPointer, inv.o, f.body, f)
+    val newFunc: Function[Post] =
+      abstractFunction.getOrElseUpdate((f, map), createFunctionCopy(f, map))
+    val newArgs = removeCoercions(inv.args)
+    inv.rewrite(ref = newFunc.ref, args=newArgs)
+  }
+
   // For AmbiguousSubscript / DerefPointer we do not care about how the return type is coerced
   // so if we encounter invocations we communicate that.
   def rewriteAnyPointerReturn(e: Expr[Pre]): Expr[Post] = e match {
     case inv: ProcedureInvocation[Pre] =>
       rewriteProcedureInvocation(inv, None, anyReturnPointer=true)
-//    case inv: FunctionInvocation[Pre] =>
-//      rewriteFunctionInvocation(inv, None, anyReturnPointer=true)
+    case inv: FunctionInvocation[Pre] =>
+      rewriteFunctionInvocation(inv, None, anyReturnPointer=true)
     case e => dispatch(e)
   }
 
@@ -294,8 +328,9 @@ case class MakeUniqueMethodCopies[Pre <: Generation]()
     case inv: ProcedureInvocation[Pre] =>
       val returnCoercion = Some(UniqueCoercion(target, inv.t))
       rewriteProcedureInvocation(inv, returnCoercion)
-//    case inv: FunctionInvocation[Pre] =>
-    //      rewriteFunctionInvocation(inv, None, anyReturnPointer=true)
+    case inv: FunctionInvocation[Pre] =>
+      val returnCoercion = Some(UniqueCoercion(target, inv.t))
+          rewriteFunctionInvocation(inv, returnCoercion)
     case am@AmbiguousMinus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target))
     case am@AmbiguousPlus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target))
     case e => throw DisallowedQualifiedCoercion(e.o, e.t, target)
@@ -304,19 +339,8 @@ case class MakeUniqueMethodCopies[Pre <: Generation]()
   override def dispatch(e: Expr[Pre]): Expr[Post] = {
     implicit val o: Origin = e.o
     e match {
-      case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) =>
-        val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args))
-        if(argsNoCoercions(allArgs)) return inv.rewriteDefault()
-        if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o)
-        // Yields and givens are not supported
-        if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o)
-
-        val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, ???, ???, inv.o, f.decl.body, f.decl)
-        // Make sure we only create one copy per coercion mapping
-        val newFunc: Function[Post] =
-          abstractFunction.getOrElseUpdate((f.decl, map), createAbstractFunctionCopy(f.decl, map))
-        val newArgs = removeCoercions(args)
-        inv.rewrite(ref = newFunc.ref, args=newArgs)
+      case inv: FunctionInvocation[Pre] =>
+        rewriteFunctionInvocation(inv, None)
       case inv: ProcedureInvocation[Pre] =>
         rewriteProcedureInvocation(inv, None)
       // So this is awkward, but...

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

@@ -340,4 +340,50 @@ int f(int n, /*@ unique<1> @*/ int* x0, int* x1){
 /*@ unique<1> @*/ int* h(int /*@ unique<2> @*/ * y){
   return NULL;
 }"""
+
+  vercors should verify using silicon in "Call function in contract, which needs coercion" c """/*@
+  context n > 0;
+  context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], 1\2));
+  context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
+  @*/
+  int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
+    //@ assert h(x0, x1) == x0[0] + x1[0];
+    //@ assert g(x0, x1) == x0[0] + x1[0];
+    return 0;
+  }
+
+  /*@
+    context x0 != NULL ** \pointer_length(x0) > 0 ** Perm(&x0[0], 1\4);
+    context x1 != NULL ** \pointer_length(x1) > 0 ** Perm(&x1[0], 1\4);
+    ensures \result == h(x0, x1);
+  @*/
+  int g(int* x0, /*@ unique<2> @*/ int* x1){
+    return x0[0] + x1[0];
+  }
+
+
+  /*@
+    requires x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4);
+    requires y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4);
+    ensures \result == x[0]+y[0];
+  pure int h(int* x, unique<2>int * y) = x[0]+y[0];
+  @*/
+"""
+
+  vercors should verify using silicon in "Call non-unique function" c """/*@
+  context n > 0;
+  context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(&x0[i], 1\2));
+  context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(&x1[i], 1\2));
+  @*/
+  int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
+    //@ assert h(x0) + h(x1) == x0[0] + x1[0];
+    return 0;
+  }
+
+  /*@
+    requires x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2);
+    ensures \result == x[0];
+  pure int h(int* x) = x[0];
+  @*/
+  """
 }