From a084769ee9248069a21bef40773a65bf129c32e8 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 8 Aug 2024 14:24:19 +0200 Subject: [PATCH] Coerce return, support methods unique coercion, fix for void --- src/col/vct/col/ast/Node.scala | 4 + .../CoerceBetweenUniquePointerImpl.scala | 2 +- .../CoerceFromUniquePointerImpl.scala | 2 +- .../coercion}/CoerceToUniquePointerImpl.scala | 2 +- .../vct/col/typerules/CoercingRewriter.scala | 23 +- src/col/vct/col/typerules/CoercionUtils.scala | 22 +- src/main/vct/main/stages/Transformation.scala | 2 + .../vct/rewrite/EncodeArrayValues.scala | 15 +- .../vct/rewrite/TypeQualifierCoercion.scala | 231 ++++++++++----- src/rewrite/vct/rewrite/adt/ImportVoid.scala | 5 +- .../integration/examples/QualifierSpec.scala | 274 +++++++++++++++++- .../integration/meta/ExampleCoverage.scala | 1 + 12 files changed, 482 insertions(+), 101 deletions(-) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceBetweenUniquePointerImpl.scala (87%) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceFromUniquePointerImpl.scala (86%) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceToUniquePointerImpl.scala (87%) diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index b21b441ac4..19bbbb6cdb 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1878,6 +1878,10 @@ final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])( )(implicit val o: Origin) extends NewPointer[G] with NewConstPointerArrayImpl[G] +final case class UniquePointerCoercion[G](e: Expr[G], t: Type[G])( + implicit val o: Origin +) extends Expr[G] with UniquePointerCoercionImpl[G] + final case class FreePointer[G](pointer: Expr[G])( val blame: Blame[PointerFreeError] )(implicit val o: Origin) diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala similarity index 87% rename from src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala index 60a1d0e566..6c5b0e4631 100644 --- a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceBetweenUniquePointer import vct.col.ast.ops.CoerceBetweenUniquePointerOps diff --git a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala similarity index 86% rename from src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala index 1f56025840..9f35fd55c0 100644 --- a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceFromUniquePointer import vct.col.ast.ops.CoerceFromUniquePointerOps diff --git a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala similarity index 87% rename from src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala index d354a2beb9..1ef12bbd9f 100644 --- a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.{CoerceToUniquePointer, TUniquePointer, Type} import vct.col.ast.ops.CoerceToUniquePointerOps diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index fa894acf53..b65b5161b0 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -1,7 +1,7 @@ package vct.col.typerules import com.typesafe.scalalogging.LazyLogging -import hre.util.FuncTools +import hre.util.{FuncTools, ScopedStack} import vct.col.ast._ import vct.col.ast.rewrite.BaseCoercingRewriter import vct.col.ast.`type`.typeclass.TFloats @@ -53,6 +53,7 @@ abstract class CoercingRewriter[Pre <: Generation]() import CoercingRewriter._ type Post = Rewritten[Pre] + val resultType: ScopedStack[Type[Pre]] = ScopedStack() val coercedDeclaration: SuccessionMap[Declaration[Pre], Declaration[Pre]] = SuccessionMap() @@ -375,9 +376,16 @@ abstract class CoercingRewriter[Pre <: Generation]() def postCoerce(decl: Declaration[Pre]): Unit = allScopes.anySucceed(decl, decl.rewriteDefault()) override final def dispatch(decl: Declaration[Pre]): Unit = { - val coercedDecl = coerce(preCoerce(decl)) - coercedDeclaration(decl) = coercedDecl - postCoerce(coercedDecl) + def rewrite() : Unit = { + val coercedDecl = coerce(preCoerce(decl)) + coercedDeclaration(decl) = coercedDecl + postCoerce(coercedDecl) + } + decl match { + case m: AbstractMethod[Pre] => + resultType.having(m.returnType)({rewrite()}) + case _ => rewrite() + } } def coerce(node: Coercion[Pre]): Coercion[Pre] = { @@ -1981,6 +1989,7 @@ abstract class CoercingRewriter[Pre <: Generation]() UMinus(float(arg)), UMinus(rat(arg)), ) + case u: UniquePointerCoercion[Pre] => u case u @ Unfolding(pred, body) => Unfolding(pred, body)(u.blame) case UntypedLiteralBag(values) => val sharedType = Types.leastCommonSuperType(values.map(_.t)) @@ -2251,7 +2260,11 @@ abstract class CoercingRewriter[Pre <: Generation]() case Recv(ref) => Recv(ref) case r @ Refute(assn) => Refute(res(assn))(r.blame) case Return(result) => - Return(result) // TODO coerce return, make AmbiguousReturn? + if(resultType.nonEmpty){ + Return(coerce(result, resultType.top)) // TODO coerce return, make AmbiguousReturn? + } else { + Return(result) + } case Scope(locals, body) => Scope(locals, body) case send @ Send(decl, offset, resource) => Send(decl, offset, res(resource))(send.blame) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 50053d222d..6a63887c4d 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -13,14 +13,28 @@ case object CoercionUtils { def getCoercion[G](source: Type[G], target: Type[G]): Option[Coercion[G]] = getAnyCoercion(source, target).filter(_.isCPromoting) + // We don't want pointers to coerce just between anything, just some things we allow def getPointerCoercion[G](source: Type[G], target: Type[G], innerSource: Type[G], innerTarget: Type[G]) : Option[Coercion[G]] = { Some((innerSource, innerTarget) match { - case (i,l) if i == l => CoerceIdentity(source) - case (TUnique(l, lId), TUnique(r, rId)) => + case (l,r) if l == r => CoerceIdentity(source) + case (TCInt(), TInt()) => CoerceIdentity(source) + case (CPrimitiveType(specs), r) => + specs.collectFirst { case spec: CSpecificationType[G] => spec } match { + case Some(CSpecificationType(t)) => + return getPointerCoercion(source, target, t, r) + case None => return None + } + case (l, CPrimitiveType(specs)) => + specs.collectFirst { case spec: CSpecificationType[G] => spec } match { + case Some(CSpecificationType(t)) => + return getPointerCoercion(source, target, l, t) + case None => return None + } + case (TUnique(l, _), TUnique(r, _)) => if(l == r) CoerceBetweenUniquePointer(source, target) else return None - case (TUnique(l, lId), r) => + case (TUnique(l, _), r) => if(l == r) CoerceFromUniquePointer(source, target) else return None - case (TUnique(l, lId), r) => + case (l, TUnique(r, _)) => if(l == r) CoerceToUniquePointer(source, target) else return None case _ => return None }) diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index bd72d58daa..691825e2c7 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -35,6 +35,7 @@ import vct.rewrite.{ MonomorphizeClass, SmtlibToProverTypes, TypeQualifierCoercion, + MakeUniqueMethodCopies, } import vct.rewrite.lang.ReplaceSYCLTypes import vct.rewrite.veymont._ @@ -306,6 +307,7 @@ case class SilverTransformation( ReplaceSYCLTypes, CFloatIntCoercion, TypeQualifierCoercion, + MakeUniqueMethodCopies, ComputeBipGlue, InstantiateBipSynchronizations, EncodeBipPermissions, diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index 721c13f814..089f8ad471 100644 --- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala +++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala @@ -120,10 +120,14 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { ): (Procedure[Post], FreePointer[Pre] => PointerFreeFailed[Pre]) = { implicit val o: Origin = freeFuncOrigin var errors: Seq[Expr[Pre] => PointerFreeError] = Seq() + val innerT = t match { + case TPointer(it) => it + case TUniquePointer(it, _) => it + } val proc = globalDeclarations.declare({ val (vars, ptr) = variables.collect { - val a_var = new Variable[Post](TPointer(t))(o.where(name = "p")) + val a_var = new Variable[Post](t)(o.where(name = "p")) variables.declare(a_var) Local[Post](a_var.ref) } @@ -179,7 +183,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { IteratedPtrInjective, ) requiresT = - if (!typeIsRef(t)) + if (!typeIsRef(innerT)) requiresT else { // I think this error actually can never happen, since we require full write permission already @@ -192,7 +196,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { // If structure contains structs, the permission for those fields need to be released as well val permFields = t match { - case t: TClass[Post] => unwrapStructPerm(access, t, o, makeStruct) + case innerT: TClass[Post] => unwrapStructPerm(access, innerT, o, makeStruct) case _ => Seq() } requiresT = @@ -213,7 +217,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { body = None, requires = requiresPred, decreases = Some(DecreasesClauseNoRecursion[Post]()), - )(o.where("free_" + t.toString)) + )(o.where("free_" + innerT.toString)) }) (proc, (node: FreePointer[Pre]) => PointerFreeFailed(node, errors)) } @@ -633,8 +637,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { )(PointerArrayCreationFailed(ncpa)) case free @ FreePointer(xs) => val newXs = dispatch(xs) - val TPointer(t) = newXs.t - val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate(t, makeFree(t)) + val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate(newXs.t, makeFree(newXs.t)) ProcedureInvocation[Post](freeFunc.ref, Seq(newXs), Nil, Nil, Nil, Nil)( freeBlame(free) )(free.o) diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index de91fb7676..af97a4dd6a 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -2,10 +2,11 @@ package vct.rewrite import vct.col.ast.{Expr, _} import vct.col.origin.Origin -import vct.col.rewrite.{Generation, RewriterBuilder} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.typerules.CoercingRewriter import vct.result.VerificationError.UserError import hre.util.ScopedStack + import scala.collection.mutable case class DisallowedConstAssignment(target: Node[_]) extends UserError { @@ -39,15 +40,7 @@ case object TypeQualifierCoercion extends RewriterBuilder { } case class TypeQualifierCoercion[Pre <: Generation]() - extends CoercingRewriter[Pre] { - val methodCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() - val callee: ScopedStack[Declaration[Pre]] = ScopedStack() - val checkedCallees: mutable.Set[Declaration[Pre]] = mutable.Set() - - val abstractFunction: mutable.Map[(Function[Pre], Map[Type[Pre], Type[Post]]), Function[Post]] = mutable.Map() - val abstractProcedure: mutable.Map[(Procedure[Pre], Map[Type[Pre], Type[Post]]), Procedure[Post]] = mutable.Map() - - def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) + extends CoercingRewriter[Pre] { override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin @@ -58,14 +51,42 @@ case class TypeQualifierCoercion[Pre <: Generation]() case CoerceToUnique(_, _) => case CoerceFromUnique(_, _) => case CoerceBetweenUnique(_, _, _) => - case CoerceToUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) - case CoerceFromUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) - case CoerceBetweenUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) + case CoerceToUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) + case CoerceFromUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) + case CoerceBetweenUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) case _ => } - super.applyCoercion(e, coercion) + e } + override def postCoerce(t: Type[Pre]): Type[Post] = + t match { + case TConst(t) => dispatch(t) + case TUnique(_, _) => throw DisallowedQualifiedType(t) + case TPointer(it) => makePointer(it) + case other => other.rewriteDefault() + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case npa @ NewPointerArray(t, size, _) => + val (info, newT) = getUnqualified(t) + if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) + else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case other => other.rewriteDefault() + } + } + + override def postCoerce(s: Statement[Pre]): Statement[Post] = + s match { + case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) + case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o) + case other => other.rewriteDefault() + } + case class InnerInfo(){ var unique: Option[BigInt] = None var const: Boolean = false @@ -90,14 +111,25 @@ case class TypeQualifierCoercion[Pre <: Generation]() else if (info.unique.isDefined) TUniquePointer(resType, info.unique.get) else TPointer(resType) } +} - override def postCoerce(t: Type[Pre]): Type[Post] = getCopyType(t).getOrElse( - t match { - case TConst(t) => dispatch(t) - case TUnique(_, _) => throw DisallowedQualifiedType(t) - case TPointer(it) => makePointer(it) - case other => other.rewriteDefault() - }) +case object MakeUniqueMethodCopies extends RewriterBuilder { + override def key: String = "MakeUniqueMethodCopies" + override def desc: String = + "Makes copies of called function that are specialized for unique pointers." +} + +case class MakeUniqueMethodCopies[Pre <: Generation]() + extends Rewriter[Pre] { + val methodCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() + val callee: ScopedStack[Declaration[Pre]] = ScopedStack() + val checkedCallees: mutable.Set[Declaration[Pre]] = mutable.Set() + + val abstractFunction: mutable.Map[(Function[Pre], Map[Type[Pre], Type[Post]]), Function[Post]] = mutable.Map() + val abstractProcedure: mutable.Map[(Procedure[Pre], Map[Type[Pre], Type[Post]]), Procedure[Post]] = mutable.Map() + def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) + + override def dispatch(t: Type[Pre]): Type[Post] = getCopyType(t).getOrElse(t.rewriteDefault()) case class UniqueCoercion(givenArgT: Type[Pre], originalParamT: Type[Pre]) case class Args(originalParams: Seq[Variable[Pre]], coercions: Seq[(UniqueCoercion, BigInt)]) @@ -109,18 +141,13 @@ case class TypeQualifierCoercion[Pre <: Generation]() def argsNoCoercions(args: Seq[Args]) : Boolean = args.forall(_.coercions.isEmpty) def removeCoercions(args: Seq[Expr[Pre]]): Seq[Expr[Post]] = args.map({ - case ApplyCoercion(e, CoerceFromUniquePointer(_, _)) => dispatch(e) + case UniquePointerCoercion(e, t) => dispatch(e) case e => dispatch(e) }) def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] = xs.zipWithIndex.collect { - case (ApplyCoercion(_, CoerceFromUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) - case (ApplyCoercion(_, CoerceBetweenUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) - case (ApplyCoercion(_, CoerceToUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) + case (UniquePointerCoercion(e, target), i) => (UniqueCoercion(e.t, target), i) } def getCoercionMap(coercions: Seq[UniqueCoercion], calledOrigin: Origin): Map[Type[Pre], Type[Post]] = { @@ -131,20 +158,26 @@ case class TypeQualifierCoercion[Pre <: Generation]() (l, r) => if(l == r) l else throw DisallowedQualifiedMethodCoercion(calledOrigin)) } - def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { + def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedResults: Set[Type[Post]], + coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { // Check if any non-coerced arguments contain a coerced type args.zipWithIndex.foreach({ case (a, i) => - if(!coercedArgs.contains(i) && - ( a.collectFirst { case ApplyCoercion(_, CoerceFromUniquePointer(_, _)) => () }.isDefined || - coercedTypes.contains(a.t) || a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined) - ) { - throw DisallowedQualifiedMethodCoercion(calledOrigin) + // Look at non-coerced args + if(!coercedArgs.contains(i)) { + // An argument cannot contain coercions themselves + if(a.collectFirst { case _: UniquePointerCoercion[Pre] => () }.isDefined || + // The (sub)type cannot be coerced in another argument + a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined || + // The (sub)type cannot be the same as a resulting coercion + dispatch(a.t).collectFirst { case t: Type[Post] if coercedResults.contains(t) => () }.isDefined + ){ + throw DisallowedQualifiedMethodCoercion(calledOrigin) + } } }) } - // def checkBody(body: Node[Pre], callee: Declaration[Pre], seenMethods: mutable.Set[Declaration[Pre]], calledOrigin: Origin): Unit = { body.collect { case inv: AnyMethodInvocation[Pre] if !seenMethods.contains(inv.ref.decl) => @@ -163,21 +196,40 @@ case class TypeQualifierCoercion[Pre <: Generation]() * This rules out coercing pointer of pointers, but I see no easy around this at the time 3. If the call is recursive, we do not allow this. * Also if there is a recursive call, further down the call tree, it is not allowed. + 4. The output types need to be unique + 5. We cannot coerce towards a type, for which this type was already present and not coerced */ - def getCoercionMapAndCheck(allArgs: Seq[Args], returnType: Type[Pre], calledOrigin: Origin, + def getCoercionMapAndCheck(allArgs: Seq[Args], returnType: Type[Pre], returnCoercion: Option[UniqueCoercion], + anyReturnCoercion: Boolean, + calledOrigin: Origin, body: Option[Node[Pre]], original: Declaration[Pre] ): Map[Type[Pre], Type[Post]] = { - val coercions: Seq[UniqueCoercion] = allArgs.flatMap(f => f.coercions.view.map(_._1)) + val coercions: Seq[UniqueCoercion] = allArgs.flatMap(f => f.coercions.view.map(_._1)) :++ returnCoercion val coercionMap = getCoercionMap(coercions, calledOrigin) // Checks 1 val coercedTypes = coercionMap.keySet + val coercedResults = coercionMap.values.toSet + // Checks 4 + if(coercedResults.size != coercedTypes.size){ + throw DisallowedQualifiedMethodCoercion(calledOrigin) + } allArgs.foreach({ args => val coercedArgs = args.coercions.map(_._2).toSet - checkArgs(args.originalParams, coercedTypes, coercedArgs, calledOrigin) // Checks 2 + checkArgs(args.originalParams, coercedTypes, coercedResults, coercedArgs, calledOrigin) // Checks 2 }) - // check return type (also 2) - returnType.collectFirst{ - case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) } + // check return type if it not coerced (also 2) + // But not 1: if we have an explicit coercion (which is checked) + if(returnCoercion.isEmpty) { + // anyReturnCoercion means we are fine with a coerced return type. But no coerced subtype can be present though + val checkedSet = if(anyReturnCoercion) coercedTypes - returnType else coercedTypes + returnType.collectFirst { + case t: Type[Pre] if checkedSet.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) + } + // If the returnType is not coerced, it cannot be contained in any coerced Results + dispatch(returnType).collectFirst { + case t: Type[Post] if coercedResults.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) + } + } if(!checkedCallees.contains(original)) { // If the body of this functions calls the callee, we end up with recursion we do not want body.foreach(b => checkBody(b, callee.top, mutable.Set(original), calledOrigin)) // Checks 3 @@ -210,15 +262,48 @@ case class TypeQualifierCoercion[Pre <: Generation]() } } - override def postCoerce(e: Expr[Pre]): Expr[Post] = { + def rewriteProcedureInvocation(inv: ProcedureInvocation[Pre], returnCoercion: Option[UniqueCoercion], anyReturnPointer: Boolean = false): ProcedureInvocation[Post] = { + val f = inv.ref.decl + val allArgs: Seq[Args] = Seq(addArgs(f.args, inv.args), + addArgs(f.outArgs, inv.outArgs)) + if(argsNoCoercions(allArgs) && returnCoercion.isEmpty) return inv.rewriteDefault() + 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 newProc: Procedure[Post] = + abstractProcedure.getOrElseUpdate((f, map), createAbstractProcedureCopy(f, map)) + val newArgs = removeCoercions(inv.args) + val newOutArgs = removeCoercions(inv.outArgs) + inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) + } + + // 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 e => dispatch(e) + } + + // If the coerce contains an invocation, maybe it is valid, otherwise not + def rewriteCoerce(e: Expr[Pre], target: Type[Pre]): Expr[Post] = e match { + case inv: ProcedureInvocation[Pre] => + val returnCoercion = Some(UniqueCoercion(target, inv.t)) + rewriteProcedureInvocation(inv, returnCoercion) +// case inv: FunctionInvocation[Pre] => + // rewriteFunctionInvocation(inv, None, anyReturnPointer=true) + 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) + } + + override def dispatch(e: Expr[Pre]): Expr[Post] = { implicit val o: Origin = e.o e match { - case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) - case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) - case npa @ NewPointerArray(t, size, _) => - val (info, newT) = getUnqualified(t) - if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) - else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) => val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args)) if(argsNoCoercions(allArgs)) return inv.rewriteDefault() @@ -226,32 +311,41 @@ case class TypeQualifierCoercion[Pre <: Generation]() // 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) + 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@ProcedureInvocation(f, args, outArgs, typeArgs, givenMap, yields) => - val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args), - addArgs(f.decl.outArgs, outArgs)) - 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) - val newProc: Procedure[Post] = - abstractProcedure.getOrElseUpdate((f.decl, map), createAbstractProcedureCopy(f.decl, map)) - val newArgs = removeCoercions(args) - val newOutArgs = removeCoercions(outArgs) - inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) + case inv: ProcedureInvocation[Pre] => + rewriteProcedureInvocation(inv, None) + // So this is awkward, but... + // A lot of times we just coerced to 'pointer', as with subscripting. In this case we don't care if the return gets + // coerced. + case e@AmbiguousSubscript(p, _) => e.rewrite(collection=rewriteAnyPointerReturn(p)) + case e@DerefPointer(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@FreePointer(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerBlockLength(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerLength(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerBlockOffset(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@SharedMemSize(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + // We store the coercion for the return type + case u: UniquePointerCoercion[Pre] => rewriteCoerce(u.e, u.t) // TODO: consider doing exactly the same for any other abstractFunction/abstractMethod case other => other.rewriteDefault() } } - override def postCoerce(d: Declaration[Pre]): Unit = d match { + override def dispatch(s: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = s.o + s match { + case ev@Eval(e) => + ev.rewrite(rewriteAnyPointerReturn(e)) + case other => other.rewriteDefault() + } + } + + override def dispatch(d: Declaration[Pre]): Unit = d match { case f: AbstractFunction[Pre] => callee.having(f){ checkedCallees.clear() allScopes.anySucceed(f, f.rewriteDefault()) @@ -262,13 +356,4 @@ case class TypeQualifierCoercion[Pre <: Generation]() } case other => allScopes.anySucceed(other, other.rewriteDefault()) } - - - - override def postCoerce(s: Statement[Pre]): Statement[Post] = - s match { - case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) - case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o) - case other => other.rewriteDefault() - } } diff --git a/src/rewrite/vct/rewrite/adt/ImportVoid.scala b/src/rewrite/vct/rewrite/adt/ImportVoid.scala index 414bdfed90..66b3b496d3 100644 --- a/src/rewrite/vct/rewrite/adt/ImportVoid.scala +++ b/src/rewrite/vct/rewrite/adt/ImportVoid.scala @@ -38,7 +38,10 @@ case class ImportVoid[Pre <: Generation](importer: ImportADTImporter) override def postCoerce(stat: Statement[Pre]): Statement[Post] = stat match { - case ret @ Return(v @ Void()) => ret.rewrite(result = Void()(v.o)) + case ret @ Return(v @ Void()) => + ret.rewrite(result = Void()(v.o)) + case ret @ Return(ApplyCoercion(v @ Void(), CoerceIdentity(_))) => + ret.rewrite(result = Void()(v.o)) case other => rewriteDefault(other) } } diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index acfd3ce53a..e6ac89de1b 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -11,7 +11,7 @@ class QualifierSpec extends VercorsSpec { vercors should verify using silicon in "same uniques local with inits" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<1> @*/ int* x1; x1 = x0;}""" vercors should verify using silicon in "malloc uniques" c """#include - void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}""" + void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0; free(x0);}""" vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}""" vercors should error withCode "disallowedQualifiedCoercion" in "malloc different uniques" c @@ -33,9 +33,9 @@ class QualifierSpec extends VercorsSpec { vercors should error withCode "disallowedConstAssignment" in "Assign to param const" c """void f(const int x){x = 0;}""" vercors should verify using silicon in "Assign to init const array" c """void f(){const int x[2] = {0, 2}; /*@ assert x[1] == 2; @*/}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to local array of consts" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of consts" c """void f(){const int *x; x[0] = 1;}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of consts" c """void f(const int *x){x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local array of const" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of const" c """void f(){const int *x; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of const" c """void f(const int *x){x[0] = 1;}""" vercors should verify using silicon in "Assign const array to const pointer" c """void f(const int* y){const int x[2] = {0, 2}; y = x;}""" vercors should error withCode "resolutionError:type" in "Assign const array to non-const pointer" c """void f(int* y){const int x[2] = {0, 2}; x = y;}""" @@ -65,8 +65,8 @@ class QualifierSpec extends VercorsSpec { vercors should error withCode "disallowedQualifiedMethodCoercion" in "Recursive procedure call wrong uniques" c """/*@ context n > 0; - context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ if(n == 1){ @@ -76,12 +76,268 @@ int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){ return f(n-1, x1, x0); } }""" + + vercors should verify using silicon in "Recursive procedure call with uniques" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return x0[0] + x1[0]; + } + else { + return f(n-1, x0, x1); + } +}""" + + vercors should verify using silicon in "Recursive procedure call with uniques and coercion" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return f(n-1, x0, x1); + } } -class QualifierSpecWIP2 extends VercorsSpec { +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} +""" + vercors should verify using silicon in "Call procedure with multiple consistent coercions" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + return h(x0, x0) + h(x1, x1); } -class QualifierSpecWIP extends VercorsSpec { - +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4); + ensures \result == x[0] + y[0]; +@*/ +int h(int* x, int* y){ + return x[0] + y[0]; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Call procedure with multiple inconsistent coercions" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + return h(x0, x1); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4); + ensures \result == x[0] + y[0]; +@*/ +int h(int* x, int* y){ + return x[0] + y[0]; +}""" + + vercors should error withCode "resolutionError:type" in "Cannot coerce pointers of pointers" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0){ + /*@ unique<1> @*/ int y[1] = {1}; + /*@ unique<1> @*/ int* yy[1] = {y}; + return h(x0, yy); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context yy != NULL ** \pointer_length(yy) > 0 ** Perm(&yy[0], 1\4); + context yy[0] != NULL ** \pointer_length(yy[0]) > 0 ** Perm(&yy[0][0], 1\4); + ensures \result == x[0] + yy[0][0]; +@*/ +int h(int* x, int** yy){ + return x[0] + yy[0][0]; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Disallow coercion of types which are subtypes of other types" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0){ + int y[1] = {1}; + int* yy[1] = {y}; + return h(x0, yy); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context yy != NULL ** \pointer_length(yy) > 0 ** Perm(&yy[0], 1\4); + context yy[0] != NULL ** \pointer_length(yy[0]) > 0 ** Perm(&yy[0][0], 1\4); + ensures \result == x[0] + yy[0][0]; +@*/ +int h(int* x, int** yy){ + return x[0] + yy[0][0]; +}""" + + vercors should verify using silicon in "Indirect recursive procedure call with uniques and coercion" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return g(n-1, x0, x1); + } +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} + +/*@ + context n > 0; + context x != NULL ** \pointer_length(x) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x, /*@ unique<2> @*/ int* y){ + return f(n, x, y); +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Indirect recursive procedure call with uniques and coercion" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return g(n-1, x1, x0); + } +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} + +/*@ + context n > 0; + context x != NULL ** \pointer_length(x) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x, /*@ unique<2> @*/ int* y){ + return f(n, x, y); +}""" + + vercors should verify using silicon in "Call procedure which already has unique type" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, int* x1){ + return h(x0) + h(x1); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + ensures \result == x[0]; +@*/ +int h(/*@ unique<2> @*/ int* x){ + return x[0]; +}""" + + vercors should verify using silicon in "Call procedure which returns pointer" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, int* x1){ + int y = h(x0)[0]; + /*@ unique<1> @*/ int* yy = h(x0); + return h(x0)[0] + h(x1)[0]; +} + +/*@ + ensures \result == \old(x); +@*/ +int* h(int* x){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Call procedure with unsupported return type" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0){ + /*@ unique<2> @*/ int* yy = h(x0); +} + +/*@ + ensures \result == \old(x); +@*/ +int* h(int* x){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedCoercion" in "Returns non-unique when should" c """ +int* h(int /*@ unique<1> @*/ * x, int /*@ unique<2> @*/ * y){ + return x; +} +""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Arguments are same but should be unique" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0, int* x1){ + h(x0, x0); +} + +/*@ unique<1> @*/ int* h(int /*@ unique<1> @*/ * x, int /*@ unique<2> @*/ * y){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Return type cannot be same as coerced argument type" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0, int* x1){ + h(x0); +} + +/*@ unique<1> @*/ int* h(int /*@ unique<2> @*/ * y){ + return NULL; +}""" } \ No newline at end of file diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala index e5918fb39d..82cf5b39ed 100644 --- a/test/main/vct/test/integration/meta/ExampleCoverage.scala +++ b/test/main/vct/test/integration/meta/ExampleCoverage.scala @@ -36,6 +36,7 @@ class ExampleCoverage extends AnyFlatSpec { new PointerSpec(), new PredicatesSpec(), new PublicationsSpec(), + new QualifierSpec(), new RefuteSpec(), new SequencesSpec(), new SetsSpec(),