From 529f4b4609f0f84007e9ae5fe40e4281bdc4aad8 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 8 Aug 2024 17:15:05 +0200 Subject: [PATCH] Support for qualified functions --- .../expr/misc/UniquePointerCoercionImpl.scala | 9 +++ src/parsers/antlr4/CParser.g4 | 4 +- .../vct/parsers/transform/CToCol.scala | 6 +- .../vct/rewrite/TypeQualifierCoercion.scala | 62 +++++++++++++------ .../integration/examples/QualifierSpec.scala | 46 ++++++++++++++ 5 files changed, 104 insertions(+), 23 deletions(-) create mode 100644 src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala diff --git a/src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala b/src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala new file mode 100644 index 0000000000..edaef3834a --- /dev/null +++ b/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 = ??? +} diff --git a/src/parsers/antlr4/CParser.g4 b/src/parsers/antlr4/CParser.g4 index ad2e6b3e60..6a59d3f4b9 100644 --- a/src/parsers/antlr4/CParser.g4 +++ b/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 '*'; \ No newline at end of file +typeSpecifierWithPointerOrArray : specifierQualifierList + | specifierQualifierList '[' ']' + | specifierQualifierList '*'; \ No newline at end of file diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index d9969964c0..ca5a375b16 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/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 = diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index af97a4dd6a..e0a04cea23 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/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... diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index e6ac89de1b..ceec1aaf0a 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/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 @*/ 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 @*/ 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]; + @*/ + """ } \ No newline at end of file