From 3335ff9e19467e21c7d6ca1453e753f483b9ae11 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 3 Oct 2024 16:20:45 +0200 Subject: [PATCH] WIP unique fields --- src/col/vct/col/ast/Node.scala | 19 ++++++ .../col/ast/expr/heap/read/DerefImpl.scala | 21 +++++- .../col/ast/unsorted/CTStructUniqueImpl.scala | 9 +++ .../unsorted/CUniquePointerFieldImpl.scala | 9 +++ .../CoerceBetweenUniqueClassImpl.scala | 9 +++ .../CoerceBetweenUniqueStructImpl.scala | 9 +++ .../col/ast/unsorted/TClassUniqueImpl.scala | 9 +++ src/col/vct/col/resolve/ResolutionError.scala | 7 ++ src/col/vct/col/resolve/Resolve.scala | 37 +++++------ src/col/vct/col/resolve/lang/C.scala | 42 ++++++++---- .../vct/col/typerules/CoercingRewriter.scala | 2 + src/col/vct/col/typerules/CoercionUtils.scala | 14 +++- src/parsers/antlr4/SpecLexer.g4 | 1 + src/parsers/antlr4/SpecParser.g4 | 1 + .../vct/parsers/transform/CToCol.scala | 5 +- .../vct/rewrite/TypeQualifierCoercion.scala | 58 +++++++++++++++++ src/rewrite/vct/rewrite/lang/LangCToCol.scala | 35 +++++++--- .../vct/rewrite/lang/LangSpecificToCol.scala | 7 +- .../vct/rewrite/lang/LangTypesToCol.scala | 15 ++++- .../integration/examples/QualifierSpec.scala | 64 +++++++++++++++++++ 20 files changed, 323 insertions(+), 50 deletions(-) create mode 100644 src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 19bbbb6cdb..0582e07886 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -140,6 +140,13 @@ final case class TConst[G](inner: Type[G])( final case class TUnique[G](inner: Type[G], unique: BigInt)( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TUniqueImpl[G] +final case class CTStructUnique[G](inner: Type[G], fieldRef: Ref[G, CStructMemberDeclarator[G]], unique: BigInt)( + implicit val o: Origin = DiagnosticOrigin +) extends CType[G] with CTStructUniqueImpl[G] +final case class TClassUnique[G](inner: Type[G], fieldRef: Ref[G, InstanceField[G]], unique: BigInt)( + implicit val o: Origin = DiagnosticOrigin +) extends Type[G] with TClassUniqueImpl[G] + sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G] final case class TPointer[G](element: Type[G])( @@ -964,6 +971,14 @@ final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G]) implicit val o: Origin ) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G] +final case class CoerceBetweenUniqueClass[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniqueClassImpl[G] +final case class CoerceBetweenUniqueStruct[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniqueStructImpl[G] + + final case class CoerceToConst[G](source: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceToConstImpl[G] @@ -2631,6 +2646,10 @@ final case class CAtomic[G]()(implicit val o: Origin) extends CTypeQualifier[G] with CAtomicImpl[G] final case class CUnique[G](i: BigInt)(implicit val o: Origin) extends CTypeQualifier[G] with CUniqueImpl[G] +final case class CUniquePointerField[G](name: String, i: BigInt)(implicit val o: Origin) + extends CTypeQualifier[G] with CUniquePointerFieldImpl[G] { + var ref: Option[RefCStructField[G]] = None +} sealed trait CFunctionSpecifier[G] extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G] diff --git a/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala b/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala index 84ef4f7d4f..66b719507d 100644 --- a/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala +++ b/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala @@ -7,6 +7,9 @@ import vct.col.ast.{ Expr, FieldLocation, TClass, + TClassUnique, + TPointer, + TUnique, Type, Value, } @@ -17,8 +20,22 @@ import vct.col.ast.ops.DerefOps trait DerefImpl[G] extends ExprImpl[G] with DerefOps[G] { this: Deref[G] => - override def t: Type[G] = - obj.t.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t) + override def t: Type[G] = obj.t match { + case TClassUnique(inner, fieldRef, unique) if fieldRef.decl == ref.decl => + addUniquePointer(inner, unique) + case t => getT(t) + } + + def getT(classT: Type[G]): Type[G] = { + classT.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t) + } + + def addUniquePointer(inner: Type[G], unique: BigInt): Type[G] = { + getT(inner) match { + case TPointer(inner) => TPointer(TUnique(inner, unique)) + case _ => ??? + } + } override def check(context: CheckContext[G]): Seq[CheckError] = Check.inOrder( diff --git a/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala b/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala new file mode 100644 index 0000000000..a7731315e9 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CTStructUnique +import vct.col.ast.ops.CTStructUniqueOps +import vct.col.print._ + +trait CTStructUniqueImpl[G] extends CTStructUniqueOps[G] { this: CTStructUnique[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala b/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala new file mode 100644 index 0000000000..30f0308eb0 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CUniquePointerField +import vct.col.ast.ops.CUniquePointerFieldOps +import vct.col.print._ + +trait CUniquePointerFieldImpl[G] extends CUniquePointerFieldOps[G] { this: CUniquePointerField[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala new file mode 100644 index 0000000000..6a3aaecce9 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceBetweenUniqueClass +import vct.col.ast.ops.CoerceBetweenUniqueClassOps +import vct.col.print._ + +trait CoerceBetweenUniqueClassImpl[G] extends CoerceBetweenUniqueClassOps[G] { this: CoerceBetweenUniqueClass[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala new file mode 100644 index 0000000000..fa95827757 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceBetweenUniqueStruct +import vct.col.ast.ops.CoerceBetweenUniqueStructOps +import vct.col.print._ + +trait CoerceBetweenUniqueStructImpl[G] extends CoerceBetweenUniqueStructOps[G] { this: CoerceBetweenUniqueStruct[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala b/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala new file mode 100644 index 0000000000..8060f44485 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.TClassUnique +import vct.col.ast.ops.TClassUniqueOps +import vct.col.print._ + +trait TClassUniqueImpl[G] extends TClassUniqueOps[G] { this: TClassUnique[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/resolve/ResolutionError.scala b/src/col/vct/col/resolve/ResolutionError.scala index 61bef3850e..1d43854286 100644 --- a/src/col/vct/col/resolve/ResolutionError.scala +++ b/src/col/vct/col/resolve/ResolutionError.scala @@ -17,6 +17,13 @@ case class MultipleForwardDeclarationContractError( ) } +case class NotSupportedStructUniqueField(use: Node[_]) + extends ResolutionError { + override def text: String = + use.o.messageInContext(s"This use of unique_pointer_field is not supported") + override def code: String = "notSupportedStructUniqueField" +} + case class NoSuchNameError(kind: String, name: String, use: Node[_]) extends ResolutionError { override def text: String = diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 9b4753bb3e..da49ae3c6f 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -3,7 +3,7 @@ package vct.col.resolve import com.typesafe.scalalogging.LazyLogging import hre.data.BitString import hre.util.FuncTools -import vct.col.ast._ +import vct.col.ast.{CUniquePointerField, _} import vct.col.ast.util.Declarator import vct.col.check.CheckError import vct.col.origin._ @@ -11,23 +11,8 @@ import vct.col.resolve.ResolveReferences.scanScope import vct.col.ref.Ref import vct.col.resolve.ctx._ import vct.col.resolve.lang.{C, CPP, Java, LLVM, PVL, Spec} -import vct.col.resolve.Resolve.{ - MalformedBipAnnotation, - SpecContractParser, - SpecExprParser, - getLit, - isBip, -} -import vct.col.resolve.lang.JavaAnnotationData.{ - BipComponent, - BipData, - BipGuard, - BipInvariant, - BipPort, - BipPure, - BipStatePredicate, - BipTransition, -} +import vct.col.resolve.Resolve.{MalformedBipAnnotation, SpecContractParser, SpecExprParser, getLit, isBip} +import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipInvariant, BipPort, BipPure, BipStatePredicate, BipTransition} import vct.col.rewrite.InitialGeneration import vct.result.VerificationError.{Unreachable, UserError} @@ -188,6 +173,16 @@ case object ResolveTypes { case _ => ctx } + def addUniquePointerFieldRef[G](specifiers: Seq[CDeclarationSpecifier[G]], ctx: TypeResolutionContext[G], blameNode: Node[G]): Unit = { + val pf: Seq[CUniquePointerField[G]] = specifiers.collect + { case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) => s} + pf.foreach(f => + f.ref = Some(C.getUniquePointerStructFieldRef(specifiers, ctx).getOrElse( + throw NotSupportedStructUniqueField(blameNode) + )) + ) + } + def resolveOne[G](node: Node[G], ctx: TypeResolutionContext[G]): Unit = node match { case javaClass @ JavaNamedType(genericNames) => @@ -206,6 +201,12 @@ case object ResolveTypes { C.findCStruct(name, ctx) .getOrElse(throw NoSuchNameError("struct", name, t)) ) + case d: CParam[G] => addUniquePointerFieldRef(d.specifiers, ctx, d) + case d: CStructMemberDeclarator[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case d: CDeclaration[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case d: CFunctionDefinition[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case t: CPrimitiveType[G] => addUniquePointerFieldRef(t.specifiers, ctx, t) + case t @ CPPTypedefName(nestedName, _) => t.ref = Some(CPP.findCPPTypeName(nestedName, ctx).getOrElse( throw NoSuchNameError("class, struct, or namespace", nestedName, t) diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 9d2a45eb7d..e9346e070f 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -6,6 +6,7 @@ import vct.col.ast._ import vct.col.ast.`type`.typeclass.TFloats.{C_ieee754_32bit, C_ieee754_64bit} import vct.col.ast.util.ExpressionEqualityCheck.isConstantInt import vct.col.origin._ +import vct.col.ref.Ref import vct.col.resolve._ import vct.col.resolve.ctx._ import vct.col.typerules.Types @@ -71,6 +72,10 @@ case object C extends LazyLogging { q match { case CConst() => TConst(t)(q.o) case CUnique(i) => TUnique(t, i)(q.o) + case pf@CUniquePointerField(_, i) => + val field: CStructMemberDeclarator[G] = pf.ref.get.decls + val fieldRef: Ref[G, CStructMemberDeclarator[G]] = field.ref + CTStructUnique(t, fieldRef, i)(q.o) case _ => throw CTypeNotSupported(Some(q)) } } @@ -166,18 +171,10 @@ case object C extends LazyLogging { case _ => throw CTypeNotSupported(context) } - val (typeSpecs, nonTypeSpecs) = specs.filter { + val (typeSpecs, qualifiers) = specs.filter { case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false }.partition { case _: CTypeSpecifier[G] => true; case _ => false } - var unique: Option[BigInt] = None - var constant: Boolean = false - nonTypeSpecs.foreach({ - case CTypeQualifierDeclarationSpecifier(CUnique(i)) if unique.isEmpty => unique = Some(i) - case CTypeQualifierDeclarationSpecifier(CConst()) => constant = true - case _ => throw CTypeNotSupported(context) - }) - val t: Type[G] = typeSpecs match { case Seq(CVoid()) => TVoid() @@ -204,7 +201,7 @@ case object C extends LazyLogging { case Some(size) => CTVector(size, t) } - nonTypeSpecs.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } + qualifiers.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } .foldLeft(res)(qualify[G]) } @@ -294,12 +291,13 @@ case object C extends LazyLogging { case _ => None } case struct: CTStruct[G] => getCStructDeref(struct.ref.decl, name) + case struct: CTStructUnique[G] => findStruct(struct.inner, name) } def getCStructDeref[G]( decl: CGlobalDeclaration[G], name: String, - ): Option[CDerefTarget[G]] = + ): Option[RefCStructField[G]] = decl.decl match { case CDeclaration(_, _, Seq(CStructDeclaration(_, decls)), Seq()) => decls.flatMap(Referrable.from).collectFirst { @@ -308,6 +306,28 @@ case object C extends LazyLogging { case _ => None } + def getUniquePointerStructFieldRef[G]( + specs: Seq[CDeclarationSpecifier[G]], + ctx: TypeResolutionContext[G] + ): Option[RefCStructField[G]] = { + var pf: Option[CUniquePointerField[G]] = None + var struct: Option[CStructSpecifier[G]] = None + specs foreach { + case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) => + if(pf.isDefined) return None + pf = Some(s) + case s: CStructSpecifier[G] => + if(struct.isDefined) return None + struct = Some(s) + case _ => + } + if(pf.isEmpty || struct.isEmpty) return None + + val structRef: RefCStruct[G] = C.findCStruct(struct.get.name, ctx) + .getOrElse(return None) + C.getCStructDeref(structRef.decl, pf.get.name) + } + def openCLVectorAccessString[G]( access: String, typeSize: BigInt, diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index b65b5161b0..05a79b9e70 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -278,6 +278,8 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceFromUniquePointer(_, _) => e case CoerceToUniquePointer(_, _) => e case CoerceBetweenUniquePointer(_, _) => e + case CoerceBetweenUniqueStruct(_, _) => e + case CoerceBetweenUniqueClass(_, _) => e case CoerceSupports(_, _) => e case CoerceClassAnyClass(_, _) => e diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 6a63887c4d..99934ff6ef 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -194,6 +194,8 @@ case object CoercionUtils { case (TNull(), TArray(target)) => CoerceNullArray(target) case (TNull(), TClass(target, typeArgs)) => CoerceNullClass(target, typeArgs) + case (TNull(), TClassUnique(TClass(target, typeArgs), _, _)) => + CoerceNullClass(target, typeArgs) case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target) case (TNull(), TAnyClass()) => CoerceNullAnyClass() case (TNull(), target: PointerType[G]) => CoerceNullPointer(target) @@ -291,10 +293,19 @@ case object CoercionUtils { supp.cls.decl == targetClass.decl } => CoerceSupports(sourceClass, targetClass) - + case (source @ TClass(_, _), target@TClassUnique(innerT @ TClass(_, _), _, _)) if innerT == source => + CoerceBetweenUniqueClass(source, target) + case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@ TClass(_, _)) if innerS == target => + CoerceBetweenUniqueClass(source, target) + case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@TClassUnique(innerT @ TClass(_, _), _, _)) + if innerT == innerS => + CoerceBetweenUniqueClass(source, target) case (source @ TClass(sourceClass, typeArgs), TAnyClass()) => CoerceClassAnyClass(sourceClass, typeArgs) + case (source @ TClassUnique(TClass(sourceClass, typeArgs), _ ,_), TAnyClass()) => + CoerceClassAnyClass(sourceClass, typeArgs) + case ( source @ JavaTClass(sourceClass, Nil), target @ JavaTClass(targetClass, Nil), @@ -671,6 +682,7 @@ case object CoercionUtils { case t: TConst[G] => getAnyClassCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TClass[G] => Some((CoerceIdentity(source), t)) + case t: TClassUnique[G] => getAnyClassCoercion(t.inner) case t: TUnion[G] => val superType = Types.leastCommonSuperType(t.types) diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index c96d691c95..3842ef56ff 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -59,6 +59,7 @@ VAL_PURE: 'pure'; VAL_THREAD_LOCAL: 'thread_local'; VAL_BIP_ANNOTATION: 'bip_annotation'; VAL_UNIQUE: 'unique'; +VAL_UNIQUE_POINTER_FIELD: 'unique_pointer_field'; VAL_WITH: 'with'; VAL_THEN: 'then'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index cadae5d5eb..cd560cb6c3 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -421,6 +421,7 @@ valModifier valTypeQualifier : 'unique' '<' langConstInt '>' # valUnique + | 'unique_pointer_field' '<' langId ',' langConstInt '>' # valUniquePointerField ; valArgList diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index ca5a375b16..1112b0dd5b 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -1188,15 +1188,16 @@ case class CToCol[G]( case ValStatic(_) => collector.static += mod } - def convert(mod: ValEmbedTypeQualifierContext): CUnique[G] = + def convert(mod: ValEmbedTypeQualifierContext): CTypeQualifier[G] = mod match { case ValEmbedTypeQualifier0(_, mod, _) => convert(mod) case ValEmbedTypeQualifier1(mod) => convert(mod) } - def convert(implicit mod: ValTypeQualifierContext): CUnique[G] = + def convert(implicit mod: ValTypeQualifierContext): CTypeQualifier[G] = mod match { case ValUnique(_, _, uniqueId, _) => CUnique[G](convert(uniqueId)) + case ValUniquePointerField(_, _, name, _, uniqueId, _) => CUniquePointerField[G](convert(name), convert(uniqueId)) } def convertEmbedWith( diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index e0a04cea23..22f7073ba1 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -42,6 +42,46 @@ case object TypeQualifierCoercion extends RewriterBuilder { 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() +// val classCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() + + def createUniqueClassCopy(original: Class[Pre], pointerInstanceFields: Map[InstanceField[Pre], BigInt]): Class[Post] = { + globalDeclarations.declare({ + classDeclarations.scope({ + val decls = classDeclarations.collect { original.decls.foreach { d => + classDeclarations.declare[InstanceField[Post]] { d match { + case field: InstanceField[Pre] if pointerInstanceFields.contains(field) => + val unique = pointerInstanceFields(field) + val it = field.t match { + case TPointer(it) => it + case _ => ??? // Not allowed + } + val (info, innerResType) = getUnqualified(it) + if (info.const) ??? // Not allowed + val resType = TUniquePointer(innerResType, unique) + val resField = field.rewrite(t = resType) + uniqueField((field, pointerInstanceFields)) = resField + resField + case field: InstanceField[Pre] => + val resField = field.rewrite() + uniqueField((field, pointerInstanceFields)) = resField + resField + case _ => ??? // Not allowed + }} + }}._1 + original.rewrite(decls=decls) + }) + }) + } + + def getUniqueMap(t: TClassUnique[Pre]): (Map[InstanceField[Pre], BigInt], TClass[Pre]) = t.inner match { + case it: TClassUnique[Pre] => val (res, classT) = getUniqueMap(it) + if(res.contains(t.fieldRef.decl)) ??? // Not allowed + (res + (t.fieldRef.decl -> t.unique), classT) + case classT: TClass[Pre] => (Map(t.fieldRef.decl -> t.unique), classT) + } + override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin ): Expr[Post] = { @@ -54,6 +94,7 @@ case class TypeQualifierCoercion[Pre <: Generation]() 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 CoerceBetweenUniqueClass(_, t) => return UniquePointerCoercion(e, dispatch(t)) case _ => } e @@ -64,6 +105,11 @@ case class TypeQualifierCoercion[Pre <: Generation]() case TConst(t) => dispatch(t) case TUnique(_, _) => throw DisallowedQualifiedType(t) case TPointer(it) => makePointer(it) + case tu: TClassUnique[Pre] => + val (map, classT) = getUniqueMap(tu) + val c = classT.cls.decl + val uniqueClass = uniqueClasses.getOrElseUpdate((c,map), createUniqueClassCopy(c, map)) + classT.rewrite(cls = uniqueClass.ref) case other => other.rewriteDefault() } @@ -76,6 +122,18 @@ case class TypeQualifierCoercion[Pre <: Generation]() val (info, newT) = getUnqualified(t) if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case d@Deref(obj, ref) => + obj match { + // Always has an CoerceClassAnyClassCoercion + case ApplyCoercion(e, _) if e.t.isInstanceOf[TClassUnique[Pre]] => + val source = e.t.asInstanceOf[TClassUnique[Pre]] + d.rewriteDefault() + val (map, classT) = getUniqueMap(source) + if (!uniqueField.contains(ref.decl, map)) createUniqueClassCopy(classT.cls.decl, map) + d.rewrite(ref = uniqueField(ref.decl, map).ref) + case _ => d.rewriteDefault() + } + case other => other.rewriteDefault() } } diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 05eeb06872..1a0abcfa31 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -394,6 +394,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case CPrimitiveType(specs) => getBaseType(C.getPrimitiveType(specs, Some(t))) case TUnique(it, _) => getBaseType(it) case TConst(it) => getBaseType(it) + case TClassUnique(it, _, _) => getBaseType(it) + case CTStructUnique(it, _, _) => getBaseType(it) case _ => t } @@ -1272,10 +1274,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => false } - def isStruct(t: Type[Pre]): Boolean = + def isStruct(t: Type[Pre]): Boolean = getStruct(t).isDefined + + def getStruct(t: Type[Pre]): Option[CTStruct[Pre]] = getBaseType(t) match { - case t : CTStruct[Pre] => true - case _ => false + case t : CTStruct[Pre] => Some(t) + case _ => None } def isPointer(t: Type[Pre]): Boolean = @@ -1448,6 +1452,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val structRef = getBaseType(deref.struct.t) match { case CTPointer(CTStruct(struct)) => struct + case CTPointer(CTStructUnique(CTStruct(struct), fieldRef, unique)) => struct case t => throw WrongStructType(t) } Deref[Post]( @@ -1483,7 +1488,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(blame) )(struct.blame) member.specs.collectFirst { - case CSpecificationType(newStruct: CTStruct[Pre]) => + case CSpecificationType(specT) if isStruct(specT) => + val newStruct = getStruct(specT).get // We recurse, since a field is another struct Perm(loc, newPerm) &* unwrapStructPerm( loc, @@ -2028,9 +2034,18 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) TPointer(rw.dispatch(t.innerType)) } - def structType(t: CTStruct[Pre]): Type[Post] = { - val targetClass = - new LazyRef[Post, Class[Post]](cStructSuccessor(t.ref.decl)) - TClass[Post](targetClass, Seq())(t.o) - } -} + def structType(t: CType[Pre]): Type[Post] = t match { + case ts @ CTStruct(ref) => + val targetClass = + new LazyRef[Post, Class[Post]](cStructSuccessor(ref.decl)) + TClass[Post](targetClass, Seq())(t.o) + case CTStructUnique(CTStruct(ref), fieldRef, unique) => + val targetClass = + new LazyRef[Post, Class[Post]](cStructSuccessor(ref.decl)) + val targetField = + new LazyRef[Post, InstanceField[Post]](cStructFieldsSuccessor((ref.decl, fieldRef.decl))) + val tInner = TClass[Post](targetClass, Seq())(t.o) + TClassUnique[Post](tInner, targetField, unique)(t.o) + case _ => ??? + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 87ff3e3678..bafcccd2cd 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -324,7 +324,7 @@ case class LangSpecificToCol[Pre <: Generation]( case sizeof: SizeOf[Pre] => throw LangCToCol.UnsupportedSizeof(sizeof) case Perm(a @ AmbiguousLocation(expr), perm) - if c.getBaseType(expr.t).isInstanceOf[CTStruct[Pre]] => + if c.isStruct(expr.t) => c.getBaseType(expr.t) match { case structType: CTStruct[Pre] => c.unwrapStructPerm( @@ -366,9 +366,7 @@ case class LangSpecificToCol[Pre <: Generation]( case _ => } assign.target.t match { - case CPrimitiveType(specs) if specs.collectFirst { - case CSpecificationType(_: CTStruct[Pre]) => () - }.isDefined => + case t if c.isStruct(t) => c.assignStruct(assign) case CPPPrimitiveType(_) => cpp.preAssignExpr(assign) case _ => rewriteDefault(assign) @@ -396,6 +394,7 @@ case class LangSpecificToCol[Pre <: Generation]( case t: TOpenCLVector[Pre] => c.vectorType(t) case t: CTArray[Pre] => c.arrayType(t) case t: CTStruct[Pre] => c.structType(t) + case t: CTStructUnique[Pre] => c.structType(t) case t: CPPTArray[Pre] => cpp.arrayType(t) case other => rewriteDefault(other) } diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index 4d61cc7c86..c6826135eb 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -7,6 +7,7 @@ import vct.col.ref.{Ref, UnresolvedRef} import vct.col.resolve.ctx._ import vct.col.resolve.lang.{C, CPP} import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.SuccessionMap import vct.result.VerificationError.UserError import vct.rewrite.lang.LangTypesToCol.{EmptyInlineDecl, IncompleteTypeArgs} @@ -35,6 +36,12 @@ case object LangTypesToCol extends RewriterBuilder { } case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { + + val cStructFieldsSuccessor: SuccessionMap[ + (CStructMemberDeclarator[Pre]), + CStructMemberDeclarator[Post], + ] = SuccessionMap() + override def porcelainRefSucc[RefDecl <: Declaration[Rewritten[Pre]]]( ref: Ref[Pre, _] )(implicit tag: ClassTag[RefDecl]): Option[Ref[Rewritten[Pre], RefDecl]] = @@ -94,6 +101,9 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { dispatch(C.getPrimitiveType(specs, context = Some(t))) case t @ CPPPrimitiveType(specs) => dispatch(CPP.getBaseTypeFromSpecs(specs, context = Some(t))) + case t @ CTStructUnique(inner, fieldRef, unique) => + val fieldSucc: Ref[Post, CStructMemberDeclarator[Post]] = cStructFieldsSuccessor(fieldRef.decl).ref + t.rewrite(fieldRef = fieldSucc) case t @ SilverPartialTAxiomatic(Ref(adt), partialTypeArgs) => if (partialTypeArgs.map(_._1.decl).toSet != adt.typeArgs.toSet) throw IncompleteTypeArgs(t) @@ -239,8 +249,9 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { decl, context = Some(declaration), ) - cStructMemberDeclarators - .declare(declaration.rewrite(specs = specs, decls = Seq(newDecl))) + val newMember = declaration.rewrite(specs = specs, decls = Seq(newDecl)) + cStructFieldsSuccessor(declaration) = newMember + cStructMemberDeclarators.declare(newMember) }) case declaration: CFunctionDefinition[Pre] => implicit val o: Origin = declaration.o diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index ceec1aaf0a..dad6a34f8f 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -2,6 +2,69 @@ package vct.test.integration.examples import vct.test.integration.helper.VercorsSpec +class QualifierSpecWIP extends VercorsSpec { + vercors should verify using silicon in "Unique pointer field of struct containing unique struct" c """ + struct vec2 { + int* xxs; + }; + + struct vec { + int* xs; + /*@unique_pointer_field@*/ struct vec2 v; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs, /*@unique_pointer_field@*/ struct vec2 v){ + x1->xs = xs; + x1->v = v; + //@ assert xs != NULL; + return 0; + } + """ +} + +class StructQualifierSpec extends VercorsSpec { + vercors should verify using silicon in "Unique pointer field of struct" c """ + struct vec { + int* xs; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs){ + x1->xs = xs; + //@ assert xs != NULL; + return 0; + } + """ + + vercors should verify using silicon in "Unique pointer field of struct containing struct" c """ + struct vec2 { + int* xxs; + }; + + struct vec { + int* xs; + struct vec2 v; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs){ + x1->xs = xs; + //@ assert xs != NULL; + return 0; + } + """ +} + class QualifierSpec extends VercorsSpec { vercors should verify using silicon example "concepts/unique/arrays.c" @@ -123,6 +186,7 @@ ensures \result == 2*x0[0] + 2*x1[0]; @*/ int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){ return h(x0, x0) + h(x1, x1); + h(x0, x1); } /*@