diff --git a/examples/concepts/unique/arrays.c b/examples/concepts/unique/arrays.c new file mode 100644 index 0000000000..0c684806c7 --- /dev/null +++ b/examples/concepts/unique/arrays.c @@ -0,0 +1,15 @@ +/*@ + context_everywhere x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<3> @*/ int* x2){ + /*@ + loop_invariant 0 <= j && j <= n; + loop_invariant (\forall int i; 0<=i && i> s) + pure boolean uniqueS(seq> s) = (\forall int i;0<=i && i<|s|; (\forall int j;0<=j && j<|s|; (s[i] == s[j]) ==> i == j)); @@ -63,7 +63,7 @@ class ColoredTiles { } } - requires unique(res); + requires uniqueS(res); requires 0 <= j; requires j < |res|; ensures (\forall int y;0 <= y && y < j;!(prefix + res[y] == prefix + res[j])); @@ -78,9 +78,9 @@ class ColoredTiles { return; } - requires unique(ini); + requires uniqueS(ini); requires (\forall int y;0 <= y && y < |ini|;!(ini[y] == elm)); - ensures unique(ini + seq> { elm }); + ensures uniqueS(ini + seq> { elm }); void lemma_unique_add_one(seq> ini, seq elm) { seq> res = ini + seq> { elm }; @@ -119,11 +119,11 @@ class ColoredTiles { assert (|res[1]| == count[1]); assert (|res[2]| == count[2]); assert (|res[3]| == count[3]); - assert unique(res[0]); - assert unique(res[1]); - assert unique(res[2]); + assert uniqueS(res[0]); + assert uniqueS(res[1]); + assert uniqueS(res[2]); assert !(res[3][0][0] == res[3][1][0]); - assert unique(res[3]); + assert uniqueS(res[3]); int n=4; loop_invariant n>=4 && n<=i; @@ -131,7 +131,7 @@ class ColoredTiles { loop_invariant (\forall* int j;0<=j && j> last = seq> {}; count[n] = count[n-1]; @@ -144,10 +144,10 @@ class ColoredTiles { loop_invariant (\forall int y; 0<=y && y 0); loop_invariant (\forall int z;0<=z && z {false} + res[predN][z]))); loop_invariant (\forall int z;0<=z && z {false}); assert (\let int predN = n - 1; @@ -166,7 +166,7 @@ class ColoredTiles { loop_invariant (\forall int y;0<=y && y <|last|;validSequence(last[y],n)); loop_invariant (\forall int y;0<=y && y <|startBlock|;startBlock[y]); loop_invariant (\forall int z;0<=z && z <|last|;has_false_in_prefix(last[z],k-1)); - loop_invariant unique(last); + loop_invariant uniqueS(last); while(k < n){ int j = 0; seq> nxtblock = seq> {}; @@ -182,7 +182,7 @@ class ColoredTiles { loop_invariant (\forall int y;0<=y && y {false}) + res[n-k-1][y]); - loop_invariant unique(nxtblock); + loop_invariant uniqueS(nxtblock); while (j < |res[n-k-1]|){ seq nxtelm = (startBlock + seq {false}) + res[n-k-1][j]; lemma_uniqueness_implies_unequal(res[n-k-1],j,startBlock + seq {false}); @@ -211,7 +211,7 @@ class ColoredTiles { assert (\let int predI = i - 1; (\forall int y; 0<=y && y <|res[i-1]|;validSequence(res[predI][y],i-1)) // all sequences are valid ); - assert unique(res[i-1]); // all sequences are unique + assert uniqueS(res[i-1]); // all sequences are uniqueS return count[i-1]; } diff --git a/res/universal/res/adt/const_pointer.pvl b/res/universal/res/adt/const_pointer.pvl new file mode 100644 index 0000000000..11be76c8a2 --- /dev/null +++ b/res/universal/res/adt/const_pointer.pvl @@ -0,0 +1,27 @@ +adt `const_pointer` { + pure `const_pointer` const_pointer_of(seq b, int offset); + pure seq const_pointer_block(`const_pointer` p); + pure int const_pointer_offset(`const_pointer` p); + + // the block offset is valid wrt the length of the block + axiom (∀ `const_pointer` p; + const_pointer_offset(p) >= 0 && + const_pointer_offset(p) < |const_pointer_block(p)|); + + // const_pointer_of is injective: a (block, offset) pair indicates a unique const_pointer value + axiom (∀seq b, int offset; + {:const_pointer_block(const_pointer_of(b, offset)):} == b && + {:const_pointer_offset(const_pointer_of(b, offset)):} == offset); +} + +decreases; +pure A const_ptr_deref(`const_pointer` p) = + `const_pointer`.const_pointer_block(p)[`const_pointer`.const_pointer_offset(p)]; + +decreases; +requires 0 <= `const_pointer`.const_pointer_offset(p) + offset; +requires `const_pointer`.const_pointer_offset(p) + offset < |`const_pointer`.const_pointer_block(p)|; +pure `const_pointer` const_ptr_add(`const_pointer` p, int offset) = + `const_pointer`.const_pointer_of( + `const_pointer`.const_pointer_block(p), + `const_pointer`.const_pointer_offset(p) + offset); \ No newline at end of file diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 59d8d36153..0582e07886 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -129,14 +129,35 @@ final case class TUnion[G](types: Seq[Type[G]])( final case class TArray[G](element: Type[G])( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TArrayImpl[G] -final case class TPointer[G](element: Type[G])( - implicit val o: Origin = DiagnosticOrigin -) extends Type[G] with TPointerImpl[G] final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends Type[G] with TTypeImpl[G] final case class TVar[G](ref: Ref[G, Variable[G]])( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TVarImpl[G] +final case class TConst[G](inner: Type[G])( + implicit val o: Origin = DiagnosticOrigin +) extends Type[G] with TConstImpl[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])( + implicit val o: Origin = DiagnosticOrigin +) extends PointerType[G] with TPointerImpl[G] +final case class TUniquePointer[G](element: Type[G], id: BigInt)( + implicit val o: Origin = DiagnosticOrigin +) extends PointerType[G] with TUniquePointerImpl[G] +final case class TConstPointer[G](pureElement: Type[G])( + implicit val o: Origin = DiagnosticOrigin +) extends PointerType[G] with TConstPointerImpl[G] sealed trait CompositeType[G] extends Type[G] with CompositeTypeImpl[G] sealed trait SizedType[G] extends CompositeType[G] with SizedTypeImpl[G] @@ -325,10 +346,16 @@ final case class SpecIgnoreEnd[G]()(implicit val o: Origin) sealed trait NormallyCompletingStatement[G] extends Statement[G] with NormallyCompletingStatementImpl[G] +sealed trait AssignStmt[G] + extends NormallyCompletingStatement[G] with AssignStmtImpl[G] final case class Assign[G](target: Expr[G], value: Expr[G])( val blame: Blame[AssignFailed] )(implicit val o: Origin) - extends NormallyCompletingStatement[G] with AssignImpl[G] + extends AssignStmt[G] with AssignImpl[G] +final case class AssignInitial[G](target: Expr[G], value: Expr[G])( + val blame: Blame[AssignFailed] +)(implicit val o: Origin) + extends AssignStmt[G] with AssignInitialImpl[G] final case class Send[G](decl: SendDecl[G], delta: BigInt, res: Expr[G])( val blame: Blame[SendFailed] )(implicit val o: Origin) @@ -924,6 +951,42 @@ final case class CoercionSequence[G](coercions: Seq[Coercion[G]])( implicit val o: Origin ) extends Coercion[G] with CoercionSequenceImpl[G] +final case class CoerceBetweenUnique[G](sourceId: BigInt, targetId: BigInt, innerCoercion: Coercion[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniqueImpl[G] +final case class CoerceToUnique[G](source: Type[G], targetId: BigInt)( + implicit val o: Origin +) extends Coercion[G] with CoerceToUniqueImpl[G] +final case class CoerceFromUnique[G](target: Type[G], sourceId: BigInt)( + implicit val o: Origin +) extends Coercion[G] with CoerceFromUniqueImpl[G] + +final case class CoerceToUniquePointer[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceToUniquePointerImpl[G] +final case class CoerceFromUniquePointer[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceFromUniquePointerImpl[G] +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] + +final case class CoerceFromConst[G](target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceFromConstImpl[G] + final case class CoerceNothingSomething[G](target: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceNothingSomethingImpl[G] @@ -970,7 +1033,7 @@ final case class CoerceNullJavaClass[G]( extends Coercion[G] with CoerceNullJavaClassImpl[G] final case class CoerceNullAnyClass[G]()(implicit val o: Origin) extends Coercion[G] with CoerceNullAnyClassImpl[G] -final case class CoerceNullPointer[G](pointerElementType: Type[G])( +final case class CoerceNullPointer[G](target: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceNullPointerImpl[G] final case class CoerceNullEnum[G](targetEnum: Ref[G, Enum[G]])( @@ -1820,10 +1883,20 @@ final case class NewArray[G]( initialize: Boolean, )(val blame: Blame[ArraySizeError])(implicit val o: Origin) extends Expr[G] with NewArrayImpl[G] -final case class NewPointerArray[G](element: Type[G], size: Expr[G])( +sealed trait NewPointer[G] extends Expr[G] with NewPointerImpl[G] +final case class NewPointerArray[G](element: Type[G], size: Expr[G], unique: Option[BigInt])( val blame: Blame[ArraySizeError] )(implicit val o: Origin) - extends Expr[G] with NewPointerArrayImpl[G] + extends NewPointer[G] with NewPointerArrayImpl[G] +final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])( + val blame: Blame[ArraySizeError] +)(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) @@ -2571,6 +2644,12 @@ final case class CVolatile[G]()(implicit val o: Origin) extends CTypeQualifier[G] with CVolatileImpl[G] 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] @@ -2764,6 +2843,8 @@ final case class CLiteralArray[G](exprs: Seq[Expr[G]])(implicit val o: Origin) extends CExpr[G] with CLiteralArrayImpl[G] sealed trait CType[G] extends Type[G] with CTypeImpl[G] +sealed trait CPointerType[G] extends CType[G] with CPointerTypeImpl[G] + final case class TCInt[G]()(implicit val o: Origin = DiagnosticOrigin) extends IntType[G] with CType[G] with TCIntImpl[G] final case class TCFloat[G](exponent: Int, mantissa: Int)( @@ -2774,11 +2855,11 @@ final case class CPrimitiveType[G](specifiers: Seq[CDeclarationSpecifier[G]])( ) extends CType[G] with CPrimitiveTypeImpl[G] final case class CTPointer[G](innerType: Type[G])( implicit val o: Origin = DiagnosticOrigin -) extends CType[G] with CTPointerImpl[G] +) extends CPointerType[G] with CTPointerImpl[G] final case class CTArray[G](size: Option[Expr[G]], innerType: Type[G])( val blame: Blame[ArraySizeError] )(implicit val o: Origin = DiagnosticOrigin) - extends CType[G] with CTArrayImpl[G] + extends CPointerType[G] with CTArrayImpl[G] final case class CTStruct[G](ref: Ref[G, CGlobalDeclaration[G]])( implicit val o: Origin = DiagnosticOrigin ) extends CType[G] with CTStructImpl[G] diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala new file mode 100644 index 0000000000..0dbd690eab --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.expr.heap.alloc + +import vct.col.ast.{NewConstPointerArray, TConstPointer, Type} +import vct.col.ast.ops.NewConstPointerArrayOps +import vct.col.print._ + +trait NewConstPointerArrayImpl[G] extends NewConstPointerArrayOps[G] { this: NewConstPointerArray[G] => + override lazy val t: Type[G] = TConstPointer[G](element) +} diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala index 18bd2bfbf8..18eff28152 100644 --- a/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala +++ b/src/col/vct/col/ast/expr/heap/alloc/NewPointerArrayImpl.scala @@ -1,14 +1,11 @@ package vct.col.ast.expr.heap.alloc -import vct.col.ast.{NewPointerArray, TPointer, Type} +import vct.col.ast.{NewPointerArray, TPointer, TUniquePointer, Type} import vct.col.print._ import vct.col.ast.ops.NewPointerArrayOps trait NewPointerArrayImpl[G] extends NewPointerArrayOps[G] { this: NewPointerArray[G] => - override lazy val t: Type[G] = TPointer(element) - - override def precedence: Int = Precedence.POSTFIX - override def layout(implicit ctx: Ctx): Doc = - Text("new") <+> element <> "[" <> size <> "]" + override lazy val t: Type[G] = unique.map(TUniquePointer[G](element,_)) + .getOrElse(TPointer[G](element)) } diff --git a/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala b/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala new file mode 100644 index 0000000000..7b0e025145 --- /dev/null +++ b/src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala @@ -0,0 +1,16 @@ +package vct.col.ast.expr.heap.alloc + +import vct.col.ast.{Expr, NewPointer, Type} +import vct.col.origin.{ArraySizeError, Blame} +import vct.col.print._ + +trait NewPointerImpl[G] { + this: NewPointer[G] => + val blame: Blame[ArraySizeError] + val element: Type[G] + val size: Expr[G] + + override def precedence: Int = Precedence.POSTFIX + override def layout(implicit ctx: Ctx): Doc = + Text("new") <+> element <> "[" <> size <> "]" +} 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/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/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala new file mode 100644 index 0000000000..082a77b2ca --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceBetweenUnique, TUnique} +import vct.col.ast.ops.CoerceBetweenUniqueOps +import vct.col.print._ + +trait CoerceBetweenUniqueImpl[G] extends CoerceBetweenUniqueOps[G] { this: CoerceBetweenUnique[G] => + override def target = TUnique(innerCoercion.target, targetId) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala new file mode 100644 index 0000000000..6c5b0e4631 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.CoerceBetweenUniquePointer +import vct.col.ast.ops.CoerceBetweenUniquePointerOps +import vct.col.print._ + +trait CoerceBetweenUniquePointerImpl[G] extends CoerceBetweenUniquePointerOps[G] { this: CoerceBetweenUniquePointer[G] => + +} diff --git a/src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala similarity index 73% rename from src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala index c59f6f7056..98feea40b1 100644 --- a/src/col/vct/col/ast/unsorted/CoerceDecreasePrecisionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceDecreasePrecisionImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceDecreasePrecision import vct.col.ast.ops.CoerceDecreasePrecisionOps @@ -6,5 +6,4 @@ import vct.col.print._ trait CoerceDecreasePrecisionImpl[G] extends CoerceDecreasePrecisionOps[G] { this: CoerceDecreasePrecision[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? } diff --git a/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala new file mode 100644 index 0000000000..ce2ab38155 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceFromConst, TConst, Type} +import vct.col.ast.ops.CoerceFromConstOps +import vct.col.print._ + +trait CoerceFromConstImpl[G] extends CoerceFromConstOps[G] { this: CoerceFromConst[G] => + val source: Type[G] = TConst[G](target) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala new file mode 100644 index 0000000000..4dc7a5df7c --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.CoerceFromUnique +import vct.col.ast.ops.CoerceFromUniqueOps +import vct.col.print._ + +trait CoerceFromUniqueImpl[G] extends CoerceFromUniqueOps[G] { this: CoerceFromUnique[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala new file mode 100644 index 0000000000..9f35fd55c0 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.CoerceFromUniquePointer +import vct.col.ast.ops.CoerceFromUniquePointerOps +import vct.col.print._ + +trait CoerceFromUniquePointerImpl[G] extends CoerceFromUniquePointerOps[G] { this: CoerceFromUniquePointer[G] => + +} diff --git a/src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala similarity index 73% rename from src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala index b7ad3c115c..0c6b0212ae 100644 --- a/src/col/vct/col/ast/unsorted/CoerceIncreasePrecisionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceIncreasePrecisionImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceIncreasePrecision import vct.col.ast.ops.CoerceIncreasePrecisionOps @@ -6,5 +6,4 @@ import vct.col.print._ trait CoerceIncreasePrecisionImpl[G] extends CoerceIncreasePrecisionOps[G] { this: CoerceIncreasePrecision[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? } diff --git a/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala index d5ac3ea93b..6069bdc884 100644 --- a/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceNullPointerImpl.scala @@ -1,9 +1,8 @@ package vct.col.ast.family.coercion -import vct.col.ast.{CoerceNullPointer, TPointer} +import vct.col.ast.{CoerceNullPointer} import vct.col.ast.ops.CoerceNullPointerOps trait CoerceNullPointerImpl[G] extends CoerceNullPointerOps[G] { this: CoerceNullPointer[G] => - override def target: TPointer[G] = TPointer(pointerElementType) } diff --git a/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala new file mode 100644 index 0000000000..d810a94feb --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceToConst, TConst, Type} +import vct.col.ast.ops.CoerceToConstOps +import vct.col.print._ + +trait CoerceToConstImpl[G] extends CoerceToConstOps[G] { this: CoerceToConst[G] => + val target: Type[G] = TConst[G](source) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala new file mode 100644 index 0000000000..a8e306a7d0 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceToUnique, TUnique} +import vct.col.ast.ops.CoerceToUniqueOps +import vct.col.print._ + +trait CoerceToUniqueImpl[G] extends CoerceToUniqueOps[G] { this: CoerceToUnique[G] => + override def target = TUnique(source, targetId) +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala new file mode 100644 index 0000000000..1ef12bbd9f --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceToUniquePointer, TUniquePointer, Type} +import vct.col.ast.ops.CoerceToUniquePointerOps +import vct.col.print._ + +trait CoerceToUniquePointerImpl[G] extends CoerceToUniquePointerOps[G] { this: CoerceToUniquePointer[G] => + +} diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index 738aae3fdc..19c34c3745 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala @@ -67,6 +67,11 @@ trait CoercionImpl[G] extends CoercionFamilyOps[G] { case CoerceCVectorVector(_, _) => true case CoerceResourceResourceVal() => true case CoerceResourceValResource() => true + case CoerceFromConst(_) => true + case CoerceToConst(_) => true + case CoerceFromUnique(_, _) => true + case CoerceToUnique(_, _) => true + case CoerceBetweenUnique(_, _, inner) => inner.isPromoting case CoerceMapOption(inner, _, _) => inner.isPromoting case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting) case CoerceMapEither(inner, _, _) => diff --git a/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala b/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala index 3e9a24704f..3a611f82f8 100644 --- a/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala +++ b/src/col/vct/col/ast/lang/c/CPointerDeclaratorImpl.scala @@ -7,5 +7,5 @@ import vct.col.print.{Ctx, Doc} trait CPointerDeclaratorImpl[G] extends CPointerDeclaratorOps[G] { this: CPointerDeclarator[G] => override def layout(implicit ctx: Ctx): Doc = - inner.show <> Doc.fold(pointers)(_ <> _) + Doc.fold(pointers)(_ <> _) <> inner.show } diff --git a/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala b/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala new file mode 100644 index 0000000000..5e023b3746 --- /dev/null +++ b/src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.c + +import vct.col.ast.{CPointerType, Type} + +trait CPointerTypeImpl[G] { + this: CPointerType[G] => + + val innerType: Type[G] +} diff --git a/src/col/vct/col/ast/lang/c/CUniqueImpl.scala b/src/col/vct/col/ast/lang/c/CUniqueImpl.scala new file mode 100644 index 0000000000..cb42f004ec --- /dev/null +++ b/src/col/vct/col/ast/lang/c/CUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.c + +import vct.col.ast.CUnique +import vct.col.ast.ops.CUniqueOps +import vct.col.print._ + +trait CUniqueImpl[G] extends CUniqueOps[G] { this: CUnique[G] => + override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Text("unique<") <> i.toString() <> ">") +} diff --git a/src/col/vct/col/ast/statement/terminal/AssignImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignImpl.scala index f8079b4e50..4470576d6c 100644 --- a/src/col/vct/col/ast/statement/terminal/AssignImpl.scala +++ b/src/col/vct/col/ast/statement/terminal/AssignImpl.scala @@ -1,36 +1,8 @@ package vct.col.ast.statement.terminal -import vct.col.ast.{Assign, EndpointName, Local} -import vct.col.check.{CheckContext, CheckError, SeqProgEndpointAssign} -import vct.col.print._ +import vct.col.ast.Assign import vct.col.ast.ops.AssignOps +import vct.col.print._ -trait AssignImpl[G] - extends NormallyCompletingStatementImpl[G] with AssignOps[G] { - this: Assign[G] => - override def check(context: CheckContext[G]): Seq[CheckError] = - super.check(context) ++ - (target match { - case Local(ref) => - context.checkInWriteScope(context.roScopeReason, this, ref) - case EndpointName(_) if context.currentChoreography.isDefined => - Seq(SeqProgEndpointAssign(this)) - case _ => Nil - }) - - def layoutAsExpr(implicit ctx: Ctx): Doc = - Group( - target.show <+> - (if (ctx.syntax == Ctx.Silver) - ":=" - else - "=") <>> value - ) - - override def layout(implicit ctx: Ctx): Doc = - layoutAsExpr <> - (if (ctx.syntax == Ctx.Silver) - Empty - else - Text(";")) +trait AssignImpl[G] extends AssignOps[G] { this: Assign[G] => } diff --git a/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala new file mode 100644 index 0000000000..fd13a191f4 --- /dev/null +++ b/src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.statement.terminal + +import vct.col.ast.AssignInitial +import vct.col.ast.ops.AssignInitialOps +import vct.col.print._ + +trait AssignInitialImpl[G] extends AssignInitialOps[G] { this: AssignInitial[G] => + +} diff --git a/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala b/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala new file mode 100644 index 0000000000..319891f569 --- /dev/null +++ b/src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala @@ -0,0 +1,41 @@ +package vct.col.ast.statement.terminal + +import vct.col.ast.{AssignStmt, EndpointName, Expr, Local} +import vct.col.check.{CheckContext, CheckError, SeqProgEndpointAssign} +import vct.col.print._ +import vct.col.origin.{Blame, AssignFailed} + +trait AssignStmtImpl[G] + extends NormallyCompletingStatementImpl[G] { + this: AssignStmt[G] => + + val target: Expr[G] + val value: Expr[G] + val blame: Blame[AssignFailed] + + override def check(context: CheckContext[G]): Seq[CheckError] = + super.check(context) ++ + (target match { + case Local(ref) => + context.checkInWriteScope(context.roScopeReason, this, ref) + case EndpointName(_) if context.currentChoreography.isDefined => + Seq(SeqProgEndpointAssign(this)) + case _ => Nil + }) + + def layoutAsExpr(implicit ctx: Ctx): Doc = + Group( + target.show <+> + (if (ctx.syntax == Ctx.Silver) + ":=" + else + "=") <>> value + ) + + override def layout(implicit ctx: Ctx): Doc = + layoutAsExpr <> + (if (ctx.syntax == Ctx.Silver) + Empty + else + Text(";")) +} diff --git a/src/col/vct/col/ast/type/PointerTypeImpl.scala b/src/col/vct/col/ast/type/PointerTypeImpl.scala new file mode 100644 index 0000000000..b3590b0dc4 --- /dev/null +++ b/src/col/vct/col/ast/type/PointerTypeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.`type` + +import vct.col.ast.{PointerType, Type} + +trait PointerTypeImpl[G] { + this: PointerType[G] => + + val element: Type[G] +} diff --git a/src/col/vct/col/ast/type/TConstImpl.scala b/src/col/vct/col/ast/type/TConstImpl.scala new file mode 100644 index 0000000000..2024d2d913 --- /dev/null +++ b/src/col/vct/col/ast/type/TConstImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.`type` + +import vct.col.ast.TConst +import vct.col.ast.ops.TConstOps +import vct.col.print._ + +trait TConstImpl[G] extends TConstOps[G] { this: TConst[G] => + override def layout(implicit ctx: Ctx): Doc = Text("const") <+> inner +} diff --git a/src/col/vct/col/ast/type/TConstPointerImpl.scala b/src/col/vct/col/ast/type/TConstPointerImpl.scala new file mode 100644 index 0000000000..8ac8af2d45 --- /dev/null +++ b/src/col/vct/col/ast/type/TConstPointerImpl.scala @@ -0,0 +1,11 @@ +package vct.col.ast.`type` + +import vct.col.ast.{TConstPointer, TConst, Type} +import vct.col.ast.ops.TConstPointerOps +import vct.col.print._ + +trait TConstPointerImpl[G] extends TConstPointerOps[G] { this: TConstPointer[G] => + val element: Type[G] = TConst[G](pureElement) + override def layout(implicit ctx: Ctx): Doc = + Text("const_pointer") <> open <> element <> close +} diff --git a/src/col/vct/col/ast/type/TUniqueImpl.scala b/src/col/vct/col/ast/type/TUniqueImpl.scala new file mode 100644 index 0000000000..5f80efa8d4 --- /dev/null +++ b/src/col/vct/col/ast/type/TUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.`type` + +import vct.col.ast.TUnique +import vct.col.ast.ops.TUniqueOps +import vct.col.print._ + +trait TUniqueImpl[G] extends TUniqueOps[G] { this: TUnique[G] => + override def layout(implicit ctx: Ctx): Doc = Text("unique<") <> unique.toString <> ">" <+> inner +} diff --git a/src/col/vct/col/ast/type/TUniquePointerImpl.scala b/src/col/vct/col/ast/type/TUniquePointerImpl.scala new file mode 100644 index 0000000000..25a0f069b8 --- /dev/null +++ b/src/col/vct/col/ast/type/TUniquePointerImpl.scala @@ -0,0 +1,16 @@ +package vct.col.ast.`type` + +import vct.col.ast.TUniquePointer +import vct.col.ast.ops.TUniquePointerOps +import vct.col.print._ + +trait TUniquePointerImpl[G] extends TUniquePointerOps[G] { + this: TUniquePointer[G] => + override def layoutSplitDeclarator(implicit ctx: Ctx): (Doc, Doc) = { + val (spec, decl) = element.layoutSplitDeclarator + (spec, decl <> "*") + } + + override def layout(implicit ctx: Ctx): Doc = + Group(Text("unique_pointer") <> open <> element <> "," <> id.toString <> close) +} diff --git a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala index efdaf2191f..8f16385e7f 100644 --- a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala +++ b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala @@ -21,7 +21,7 @@ trait TypeImpl[G] extends TypeFamilyOps[G] { def asVector: Option[TVector[G]] = CoercionUtils.getAnyVectorCoercion(this).map(_._2) def asBag: Option[TBag[G]] = CoercionUtils.getAnyBagCoercion(this).map(_._2) - def asPointer: Option[TPointer[G]] = + def asPointer: Option[PointerType[G]] = CoercionUtils.getAnyPointerCoercion(this).map(_._2) def asArray: Option[TArray[G]] = CoercionUtils.getAnyArrayCoercion(this).map(_._2) 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/check/Check.scala b/src/col/vct/col/check/Check.scala index 18f66cfee7..f54804f387 100644 --- a/src/col/vct/col/check/Check.scala +++ b/src/col/vct/col/check/Check.scala @@ -250,7 +250,7 @@ case class SeqProgParticipant(s: Node[_]) extends CheckError { case class SeqProgNoParticipant(s: Node[_]) extends CheckError { val subcode = "seqProgNoParticipant" } -case class SeqProgEndpointAssign(a: Assign[_]) extends CheckError { +case class SeqProgEndpointAssign(a: AssignStmt[_]) extends CheckError { val subcode = "seqProgEndpointAssign" } case class SeqProgInstanceMethodPure(m: InstanceMethod[_]) extends CheckError { diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala index 1ab06e677a..ae3db74011 100644 --- a/src/col/vct/col/feature/FeatureRainbow.scala +++ b/src/col/vct/col/feature/FeatureRainbow.scala @@ -33,6 +33,7 @@ class FeatureRainbow[G] { case node: ArrayLocation[G] => Arrays case node: NewArray[G] => Arrays case node: NewPointerArray[G] => Arrays + case node: NewConstPointerArray[G] => return Seq(Arrays, AxiomaticLibraryType) case node: ArraySubscript[G] => Arrays case node: Length[G] => Arrays case node: TArray[G] => Arrays @@ -79,6 +80,8 @@ class FeatureRainbow[G] { case node: OptNoneTyped[G] => AxiomaticLibraryType case node: OptSomeTyped[G] => AxiomaticLibraryType case node: TNull[G] => AxiomaticLibraryType + case node: TVector[G] => AxiomaticLibraryType + case node: TConstPointer[G] => AxiomaticLibraryType case node: Assert[G] => BasicStatement case node: Assume[G] => BasicStatement @@ -505,7 +508,6 @@ class FeatureRainbow[G] { case node: TBag[G] => SilverAxiomaticLibraryType case node: TSeq[G] => SilverAxiomaticLibraryType case node: TSet[G] => SilverAxiomaticLibraryType - case node: TVector[G] => SilverAxiomaticLibraryType case node: SilverCurFieldPerm[G] => SilverSpecific case node: SilverCurPredPerm[G] => SilverSpecific diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index 85c9cc182a..91f9909fd4 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -328,11 +328,14 @@ case class PostconditionFailed( override def inlineDescWithSource(node: String, failure: String): String = s"Postcondition of `$node` may not hold, since $failure." } -case class TerminationMeasureFailed( + +sealed trait TerminationMeasureFailed extends ContractedFailure + +case class DecreaseTerminationMeasureFailed( applicable: ContractApplicable[_], - apply: Invocation[_], + apply: InvokingNode[_], measure: DecreasesClause[_], -) extends ContractedFailure with VerificationFailure { +) extends TerminationMeasureFailed { override def code: String = "decreasesFailed" override def position: String = measure.o.shortPositionText override def desc: String = @@ -344,6 +347,21 @@ case class TerminationMeasureFailed( override def inlineDesc: String = s"${apply.o.inlineContextText} may not terminate, since `${measure.o.inlineContextText}` is not decreased or not bounded" } + +case class CallTerminationMeasureFailed(apply: InvokingNode[_], + calledMethod: AbstractMethod[_], + ) extends TerminationMeasureFailed { + override def code: String = "callDecreasesFailed" + override def position: String = calledMethod.o.shortPositionText + override def desc: String = + Message.messagesInContext( + apply.o -> "The invocation does not terminate, since ...", + calledMethod.o -> "... this called method may not decrease.", + ) + override def inlineDesc: String = + s"The invocation ${apply.o.inlineContextText} may not terminate, since `${calledMethod.o.inlineContextText}` is not decreasing" +} + case class ContextEverywhereFailedInPost( failure: ContractFailure, node: ContractApplicable[_], 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 720f63286e..e9346e070f 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -1,16 +1,18 @@ package vct.col.resolve.lang +import com.typesafe.scalalogging.LazyLogging import hre.util.FuncTools 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 import vct.result.VerificationError.UserError -case object C { +case object C extends LazyLogging { implicit private val o: Origin = DiagnosticOrigin case class CTypeNotSupported(node: Option[Node[_]]) extends UserError { @@ -66,6 +68,22 @@ case object C { name: String, ) + def qualify[G](t: Type[G], q: CTypeQualifier[G]): Type[G] = { + 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)) + } + } + + def processPointer[G](p: CPointer[G], t: Type[G]): Type[G] = { + p.qualifiers.foldLeft(CTPointer[G](t)(p.o): Type[G])(qualify[G]) + } + def getDeclaratorInfo[G](decl: CDeclarator[G]): DeclaratorInfo[G] = decl match { case CPointerDeclarator(pointers, inner) => @@ -74,7 +92,7 @@ case object C { innerInfo.params, t => innerInfo.typeOrReturnType( - FuncTools.repeat[Type[G]](CTPointer(_), pointers.size, t) + pointers.foldLeft(t)((qt, p) => processPointer(p, qt)) ), innerInfo.name, ) @@ -82,17 +100,7 @@ case object C { val innerInfo = getDeclaratorInfo(inner) DeclaratorInfo( innerInfo.params, - t => innerInfo.typeOrReturnType(CTArray(size, t)(c.blame)), - innerInfo.name, - ) - case CPointerDeclarator(pointers, inner) => - val innerInfo = getDeclaratorInfo(inner) - DeclaratorInfo( - innerInfo.params, - t => - innerInfo.typeOrReturnType( - FuncTools.repeat[Type[G]](CTPointer(_), pointers.size, t) - ), + t => CTArray(size, t)(c.blame), innerInfo.name, ) case CTypeExtensionDeclarator(Seq(CTypeAttribute(name, Seq(size))), inner) @@ -125,34 +133,33 @@ case object C { DeclaratorInfo(params = None, typeOrReturnType = (t => t), name) } - def getSpecs[G]( - decl: CDeclarator[G], - acc: Seq[CDeclarationSpecifier[G]] = Nil, - ): Seq[CDeclarationSpecifier[G]] = - decl match { - case CTypeExtensionDeclarator(extensions, inner) => - getSpecs(inner, acc :+ CFunctionTypeExtensionModifier(extensions)) - case _ => acc - } - def getTypeFromTypeDef[G]( - decl: CDeclaration[G], + gdecl: CGlobalDeclaration[G], context: Option[Node[G]] = None, ): Type[G] = { + val decl = gdecl.decl val specs: Seq[CDeclarationSpecifier[G]] = decl.specs match { case CTypedef() +: remaining => remaining - case _ => ??? + case _ => throw CTypeNotSupported(context) } - // Need to get specifications from the init (can only have one init as typedef), since it can contain GCC Type extensions - getPrimitiveType(getSpecs(decl.inits.head.decl) ++ specs, context) + // Need to get specifications from the init (can only have one init as typedef) + if(decl.inits.size != 1) throw CTypeNotSupported(context) + val info = getDeclaratorInfo(decl.inits.head.decl) + val t = specs match { + case CStructDeclaration(_, _) +: Seq() => CTStruct[G](gdecl.ref) + case _ => getPrimitiveType(specs, context) + } + + info.typeOrReturnType(t) } def getPrimitiveType[G]( specs: Seq[CDeclarationSpecifier[G]], context: Option[Node[G]] = None, ): Type[G] = { + implicit val o: Origin = context.map(_.o).getOrElse(DiagnosticOrigin) val vectorSize: Option[Expr[G]] = specs.collect { case ext: CFunctionTypeExtensionModifier[G] => ext.extensions @@ -164,12 +171,12 @@ case object C { case _ => throw CTypeNotSupported(context) } - val filteredSpecs = specs.filter { - case _: CFunctionTypeExtensionModifier[G] => false; case _ => true - }.collect { case spec: CTypeSpecifier[G] => spec } + val (typeSpecs, qualifiers) = specs.filter { + case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false + }.partition { case _: CTypeSpecifier[G] => true; case _ => false } val t: Type[G] = - filteredSpecs match { + typeSpecs match { case Seq(CVoid()) => TVoid() case Seq(CChar()) => TChar() case CUnsigned() +: t if INTEGER_LIKE_TYPES.contains(t) => TCInt() @@ -181,7 +188,7 @@ case object C { case Seq(CBool()) => TBool() case Seq(defn @ CTypedefName(_)) => defn.ref.get match { - case RefTypeDef(decl) => getTypeFromTypeDef(decl.decl) + case RefTypeDef(decl) => getTypeFromTypeDef(decl) case _ => ??? } case Seq(CSpecificationType(typ)) => typ @@ -189,10 +196,13 @@ case object C { case spec +: _ => throw CTypeNotSupported(context.orElse(Some(spec))) case _ => throw CTypeNotSupported(context) } - vectorSize match { + val res = vectorSize match { case None => t case Some(size) => CTVector(size, t) } + + qualifiers.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } + .foldLeft(res)(qualify[G]) } def nameFromDeclarator(declarator: CDeclarator[_]): String = @@ -263,34 +273,31 @@ case object C { case _ => t } - def findPointerDeref[G]( + def findPointerDeref[G]( obj: Expr[G], name: String, ctx: ReferenceResolutionContext[G], blame: Blame[BuiltinError], ): Option[CDerefTarget[G]] = stripCPrimitiveType(obj.t) match { - case CTPointer(innerType: TNotAValue[G]) => - innerType.decl.get match { - case RefCStruct(decl) => getCStructDeref(decl, name) - case _ => None - } - case CTPointer(struct: CTStruct[G]) => - getCStructDeref(struct.ref.decl, name) - case CTArray(_, innerType: TNotAValue[G]) => - innerType.decl.get match { - case RefCStruct(decl) => getCStructDeref(decl, name) - case _ => None - } - case CTArray(_, struct: CTStruct[G]) => - getCStructDeref(struct.ref.decl, name) + case CTPointer(t) => findStruct(t, name) + case CTArray(_, t) => findStruct(t, name) + case _ => None + } + + def findStruct[G](t: Type[G], name: String): Option[CDerefTarget[G]] = t match { + case innerType: TNotAValue[G] => innerType.decl.get match { + case RefCStruct(decl) => getCStructDeref(decl, name) 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 { @@ -299,6 +306,28 @@ case object C { 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 888e6a4708..05a79b9e70 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() @@ -263,12 +264,23 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceBoolResource() => e case CoerceResourceResourceVal() => e case CoerceResourceValResource() => e + case CoerceFromConst(_) => e + case CoerceToConst(_) => e + case CoerceFromUnique(_, _) => e + case CoerceToUnique(_, _) => e + case CoerceBetweenUnique(_, _, _) => e case CoerceBoundIntFrac() => e case CoerceBoundIntZFrac(_) => e case CoerceBoundIntFloat(_, _) => e case CoerceJoinUnion(_, _, _) => e case CoerceSelectUnion(inner, _, _, _) => applyCoercion(e, inner) + case CoerceFromUniquePointer(_, _) => e + case CoerceToUniquePointer(_, _) => e + case CoerceBetweenUniquePointer(_, _) => e + case CoerceBetweenUniqueStruct(_, _) => e + case CoerceBetweenUniqueClass(_, _) => e + case CoerceSupports(_, _) => e case CoerceClassAnyClass(_, _) => e case CoerceJavaSupports(_, _) => e @@ -366,9 +378,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] = { @@ -540,7 +559,7 @@ abstract class CoercingRewriter[Pre <: Generation]() (ApplyCoercion(e, coercion)(coercionOrigin(e)), t) case None => throw IncoercibleText(e, s"two-dimensional array") } - def pointer(e: Expr[Pre]): (Expr[Pre], TPointer[Pre]) = + def pointer(e: Expr[Pre]): (Expr[Pre], PointerType[Pre]) = CoercionUtils.getAnyPointerCoercion(e.t) match { case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t) @@ -1552,8 +1571,10 @@ abstract class CoercingRewriter[Pre <: Generation]() Neq(coerce(left, sharedType), coerce(right, sharedType)) case na @ NewArray(element, dims, moreDims, initialize) => NewArray(element, dims.map(int), moreDims, initialize)(na.blame) - case na @ NewPointerArray(element, size) => - NewPointerArray(element, size)(na.blame) + case na @ NewPointerArray(element, size, unique) => + NewPointerArray(element, size, unique)(na.blame) + case nca @ NewConstPointerArray(element, size) => + NewConstPointerArray(element, size)(nca.blame) case NewObject(cls) => NewObject(cls) case NoPerm() => NoPerm() case Not(arg) => Not(bool(arg)) @@ -1970,6 +1991,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)) @@ -2132,14 +2154,8 @@ abstract class CoercingRewriter[Pre <: Generation]() implicit val o: Origin = stat.o stat match { case a @ Assert(assn) => Assert(res(assn))(a.blame) - case a @ Assign(target, value) => - try { - Assign(target, coerce(value, target.t, canCDemote = true))(a.blame) - } catch { - case err: Incoercible => - println(err.text) - throw err - } + case a @ Assign(target, value) => Assign(target, coerce(value, target.t, canCDemote = true))(a.blame) + case a @ AssignInitial(target, value) => AssignInitial(target, coerce(value, target.t, canCDemote = true))(a.blame) case Assume(assn) => Assume(bool(assn)) case Block(statements) => Block(statements) case Branch(branches) => @@ -2246,7 +2262,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 47295af0af..99934ff6ef 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -13,6 +13,33 @@ 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 (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, _), r) => + if(l == r) CoerceFromUniquePointer(source, target) else return None + case (l, TUnique(r, _)) => + if(l == r) CoerceToUniquePointer(source, target) else return None + case _ => return None + }) + } + def getAnyCoercion[G]( source: Type[G], target: Type[G], @@ -25,7 +52,55 @@ case object CoercionUtils { return Some(CoerceIdentity(source)) case (TNothing(), _) => CoerceNothingSomething(target) case (_, TAny()) => CoerceSomethingAny(source) - + case (TUnique(source, si), TUnique(target, ti)) => + val coercion = getAnyCoercion(source, target).getOrElse(return None) + if(si == ti) { + coercion + } else { + CoerceBetweenUnique(si, ti, coercion) + } + case (TUnique(source, si), target) => + if(source == target) { + CoerceFromUnique(source, si) + } else { + val inner = getAnyCoercion(source, target).getOrElse(return None) + CoercionSequence(Seq(CoerceFromUnique(source, si), inner)) + } + case (source, TUnique(target, ti)) => + if(source == target) { + CoerceToUnique(target, ti) + } else { + val inner = getAnyCoercion(source, target).getOrElse(return None) + CoercionSequence(Seq(inner, CoerceToUnique(target, ti))) + } + case (TConst(source), TConst(target)) => + getAnyCoercion(source, target).getOrElse(return None) + case (source, TConst(target)) => + if(source == target) { + source match { + case _: TRef[G] => return None + case _: PrimitiveType[G] => + case _: CompositeType[G] => + case _ => return None + } + CoerceToConst(target) + } else { + val inner = getAnyCoercion(source, target).getOrElse(return None) + CoercionSequence(Seq(inner, CoerceToConst(target))) + } + case (TConst(source), target) => + if(source == target) { + source match { + case _: TRef[G] => return None + case _: PrimitiveType[G] => + case _: CompositeType[G] => + case _ => return None + } + CoerceFromConst(source) + } else { + val inner = getAnyCoercion(source, target).getOrElse(return None) + CoercionSequence(Seq( CoerceFromConst(source), inner)) + } case (TResource(), TAnyValue()) => CoercionSequence(Seq( CoerceResourceResourceVal(), @@ -119,10 +194,12 @@ 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(), TPointer(target)) => CoerceNullPointer(target) - case (TNull(), CTPointer(target)) => CoerceNullPointer(target) + case (TNull(), target: PointerType[G]) => CoerceNullPointer(target) + case (TNull(), target: CPointerType[G]) => CoerceNullPointer(target) case (TNull(), TEnum(target)) => CoerceNullEnum(target) case (CTArray(_, innerType), TArray(element)) if element == innerType => @@ -135,22 +212,20 @@ case object CoercionUtils { case (source @ TOpenCLVector(lSize, innerType), TVector(rSize, element)) if element == innerType && lSize == rSize => CoerceCVectorVector(rSize, element) - case ( - CTPointer(innerType), - TPointer(element), - ) => // if element == innerType => - getAnyCoercion(element, innerType).getOrElse(return None) - case ( - TPointer(element), - CTPointer(innerType), - ) => // if element == innerType => - getAnyCoercion(element, innerType).getOrElse(return None) - case (CTArray(_, innerType), CTPointer(element)) => + case (s@CTPointer(innerLeft), t@CTPointer(innerRight)) => + getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None) + case (s@TPointer(innerLeft), t@TPointer(innerRight)) => + getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None) + case (s@CTPointer(innerLeft), t@TPointer(innerRight)) => + getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None) + case (s@TPointer(innerLeft), t@CTPointer(innerRight)) => + getPointerCoercion(s, t, innerLeft, innerRight).getOrElse(return None) + case (CTArray(_, innerType), t@CTPointer(element)) => if (element == innerType) { CoerceCArrayPointer(innerType) } else { CoercionSequence(Seq( CoerceCArrayPointer(element), - getAnyCoercion(element, innerType).getOrElse(return None), + getPointerCoercion(CTPointer(innerType), t, innerType, element).getOrElse(return None) )) } case (TFraction(), TZFraction()) => CoerceFracZFrac() @@ -214,14 +289,23 @@ case object CoercionUtils { case ( source @ TClass(sourceClass, Seq()), target @ TClass(targetClass, Seq()), - ) if source.transSupportArrows.exists { case (_, supp) => + ) if source.transSupportArrows().exists { case (_, supp) => 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), @@ -370,6 +454,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySeqCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySeqCoercion) + case t: TConst[G] => + getAnySeqCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSeq[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -378,6 +464,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySetCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySetCoercion) + case t: TConst[G] => + getAnySetCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSet[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -388,6 +476,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyVectorCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyVectorCoercion) + case t: TConst[G] => + getAnyVectorCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: CTVector[G] => Some(( CoerceCVectorVector(t.intSize, t.innerType), @@ -406,6 +496,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBagCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBagCoercion) + case t: TConst[G] => + getAnyBagCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TBag[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -416,6 +508,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySizedCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySizedCoercion) + case t: TConst[G] => + getAnySizedCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSeq[G] => Some((CoerceIdentity(source), t)) case t: TSet[G] => Some((CoerceIdentity(source), t)) case t: TBag[G] => Some((CoerceIdentity(source), t)) @@ -425,17 +519,18 @@ case object CoercionUtils { def getAnyPointerCoercion[G]( source: Type[G] - ): Option[(Coercion[G], TPointer[G])] = + ): Option[(Coercion[G], PointerType[G])] = source match { + case t: TConst[G] => + getAnyPointerCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} + case t: TUnique[G] => + getAnyPointerCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromUnique(t.inner, t.unique), c)), res)} case t: CPrimitiveType[G] => chainCCoercion(t, getAnyPointerCoercion) - case t: TPointer[G] => Some((CoerceIdentity(source), t)) - case t: CTPointer[G] => - Some((CoerceIdentity(source), TPointer(t.innerType))) - case t: CTArray[G] => - Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType))) + case t: PointerType[G] => Some((CoerceIdentity(source), t)) + case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType))) + case t: CTArray[G] => Some((CoerceCArrayPointer(t.innerType), TPointer(t.innerType))) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion) - case t: CPPTArray[G] => - Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType))) + case t: CPPTArray[G] => Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType))) case _: TNull[G] => val t = TPointer[G](TAnyValue()) Some((CoerceNullPointer(t), t)) @@ -447,6 +542,8 @@ case object CoercionUtils { ): Option[(Coercion[G], CTArray[G])] = source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyCArrayCoercion) + case t: TConst[G] => + getAnyCArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: CTArray[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -456,6 +553,8 @@ case object CoercionUtils { ): Option[(Coercion[G], CPPTArray[G])] = source match { case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyCPPArrayCoercion) + case t: TConst[G] => + getAnyCPPArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: CPPTArray[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -466,6 +565,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyArrayCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyArrayCoercion) + case t: TConst[G] => + getAnyArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case acc: SYCLTAccessor[G] => Some(( CoerceIdentity(source), @@ -490,6 +591,8 @@ case object CoercionUtils { ): Option[(Coercion[G], TArray[G])] = source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixArrayCoercion) + case t: TConst[G] => + getAnyMatrixArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMatrixArrayCoercion) case acc: SYCLTAccessor[G] if acc.dimCount >= 2 => @@ -518,6 +621,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyOptionCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyOptionCoercion) + case t: TConst[G] => + getAnyOptionCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TOption[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -526,6 +631,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMapCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMapCoercion) + case t: TConst[G] => + getAnyMapCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TMap[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -536,6 +643,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyTupleCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyTupleCoercion) + case t: TConst[G] => + getAnyTupleCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TTuple[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -546,6 +655,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyMatrixCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyMatrixCoercion) + case t: TConst[G] => + getAnyMatrixCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TMatrix[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -556,6 +667,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyModelCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyModelCoercion) + case t: TConst[G] => + getAnyModelCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TModel[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -566,7 +679,10 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyClassCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyClassCoercion) + 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) @@ -593,6 +709,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyEitherCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyEitherCoercion) + case t: TConst[G] => + getAnyEitherCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TEither[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -603,6 +721,8 @@ case object CoercionUtils { source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBitvecCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBitvecCoercion) + case t: TConst[G] => + getAnyBitvecCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSmtlibBitVector[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -614,6 +734,8 @@ case object CoercionUtils { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibFloatCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibFloatCoercion) + case t: TConst[G] => + getAnySmtlibFloatCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSmtlibFloatingPoint[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -625,6 +747,8 @@ case object CoercionUtils { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibArrayCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibArrayCoercion) + case t: TConst[G] => + getAnySmtlibArrayCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSmtlibArray[G] => Some((CoerceIdentity(source), t)) case _ => None } @@ -636,6 +760,8 @@ case object CoercionUtils { case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibSeqCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnySmtlibSeqCoercion) + case t: TConst[G] => + getAnySmtlibSeqCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TSmtlibSeq[G] => Some((CoerceIdentity(source), t)) case _ => None } diff --git a/src/col/vct/col/util/AstBuildHelpers.scala b/src/col/vct/col/util/AstBuildHelpers.scala index 5a718297f7..9adccefd1d 100644 --- a/src/col/vct/col/util/AstBuildHelpers.scala +++ b/src/col/vct/col/util/AstBuildHelpers.scala @@ -775,6 +775,10 @@ object AstBuildHelpers { implicit o: Origin ): Assign[G] = Assign(local, value)(AssignLocalOk) + def assignInitial[G](local: Local[G], value: Expr[G])( + implicit o: Origin + ): AssignInitial[G] = AssignInitial(local, value)(AssignLocalOk) + def assignField[G]( obj: Expr[G], field: Ref[G, InstanceField[G]], diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index f30f99ed19..f8d828c565 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -18,10 +18,7 @@ import vct.rewrite.lang.NoSupportSelfLoop import vct.col.rewrite.veymont.StructureCheck import vct.importer.{PathAdtImporter, Util} import vct.main.Main.TemporarilyUnsupported -import vct.main.stages.Transformation.{ - PassEventHandler, - TransformationCheckError, -} +import vct.main.stages.Transformation.{PassEventHandler, TransformationCheckError} import vct.options.Options import vct.options.types.{Backend, PathOrStd} import vct.resources.Resources @@ -37,6 +34,8 @@ import vct.rewrite.{ InlineTrivialLets, MonomorphizeClass, SmtlibToProverTypes, + TypeQualifierCoercion, + MakeUniqueMethodCopies, } import vct.rewrite.lang.ReplaceSYCLTypes import vct.rewrite.veymont._ @@ -307,6 +306,8 @@ case class SilverTransformation( // Replace leftover SYCL types ReplaceSYCLTypes, CFloatIntCoercion, + TypeQualifierCoercion, + MakeUniqueMethodCopies, ComputeBipGlue, InstantiateBipSynchronizations, EncodeBipPermissions, @@ -414,6 +415,7 @@ case class SilverTransformation( SmtlibToProverTypes, EnumToDomain, ImportArray.withArg(adtImporter), + ImportConstPointer.withArg(adtImporter), ImportPointer.withArg(adtImporter), ImportVector.withArg(adtImporter), ImportMapCompat.withArg(adtImporter), 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/antlr4/LangCParser.g4 b/src/parsers/antlr4/LangCParser.g4 index 932907f78d..c3951de2a0 100644 --- a/src/parsers/antlr4/LangCParser.g4 +++ b/src/parsers/antlr4/LangCParser.g4 @@ -355,6 +355,7 @@ typeQualifier | 'restrict' | 'volatile' | '_Atomic' + | valEmbedTypeQualifier ; functionSpecifier diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index c8a683e390..3842ef56ff 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -58,6 +58,8 @@ VAL_STRING: 'string'; 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 d7b73b3d24..cd560cb6c3 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -419,6 +419,11 @@ valModifier | langStatic # valStatic ; +valTypeQualifier + : 'unique' '<' langConstInt '>' # valUnique + | 'unique_pointer_field' '<' langId ',' langConstInt '>' # valUniquePointerField + ; + valArgList : valArg | valArg ',' valArgList @@ -461,3 +466,8 @@ valEmbedModifier : startSpec valModifier endSpec | {specLevel>0}? valModifier ; + + valEmbedTypeQualifier + : startSpec valTypeQualifier endSpec + | {specLevel>0}? valTypeQualifier + ; diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index f416e5980c..1112b0dd5b 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -290,6 +290,7 @@ case class CToCol[G]( case TypeQualifier1(_) => CRestrict() case TypeQualifier2(_) => CVolatile() case TypeQualifier3(_) => CAtomic() + case TypeQualifier4(spec) => convert(spec) } def convert( @@ -838,7 +839,9 @@ case class CToCol[G]( case SpecifierQualifierList0(t, tail) => convert(t) +: tail.map((e: SpecifierQualifierListContext) => convert(e)) .getOrElse(Nil) - case SpecifierQualifierList1(_, _) => ??(specifiers) + case SpecifierQualifierList1(t, tail) => + CTypeQualifierDeclarationSpecifier(convert(t)) +: tail.map((e: SpecifierQualifierListContext) => convert(e)) + .getOrElse(Nil) } def convert(implicit expr: CastExpressionContext): Expr[G] = @@ -1002,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 = @@ -1185,6 +1188,18 @@ case class CToCol[G]( case ValStatic(_) => collector.static += mod } + def convert(mod: ValEmbedTypeQualifierContext): CTypeQualifier[G] = + mod match { + case ValEmbedTypeQualifier0(_, mod, _) => convert(mod) + case ValEmbedTypeQualifier1(mod) => convert(mod) + } + + 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( implicit whiff: Option[ValEmbedWithContext], inner: Expr[G], diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index dcb8e47ab8..ec058d9cda 100644 --- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala +++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala @@ -60,7 +60,7 @@ case object EncodeArrayValues extends RewriterBuilder { } } - case class PointerArrayCreationFailed(arr: NewPointerArray[_]) + case class PointerArrayCreationFailed(arr: NewPointer[_]) extends Blame[InvocationFailure] { override def blame(error: InvocationFailure): Unit = error match { @@ -104,7 +104,10 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { : mutable.Map[(Type[Pre], Int, Int, Boolean), Procedure[Post]] = mutable .Map() - val pointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] = + val pointerArrayCreationMethods: mutable.Map[(Type[Pre], Option[BigInt]), Procedure[Post]] = + mutable.Map() + + val constPointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] = mutable.Map() val freeMethods: mutable.Map[Type[ @@ -117,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) } @@ -176,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 @@ -188,8 +195,8 @@ 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) + innerT match { + case innerT: TClass[Post] => unwrapStructPerm(access, innerT, o, makeStruct) case _ => Seq() } requiresT = @@ -210,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)) } @@ -399,6 +406,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { args = dimArgs, requires = UnitAccountedPredicate(requires), ensures = UnitAccountedPredicate(ensures), + decreases = Some(DecreasesClauseNoRecursion[Post]()) )(o.where(name = if (initialize) "make_array_initialized" @@ -504,7 +512,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { case _ => false } - def makePointerCreationMethodFor(elementType: Type[Pre]) = { + def makePointerCreationMethodFor(elementType: Type[Pre], unique: Option[BigInt], isConst: Boolean) = { implicit val o: Origin = arrayCreationOrigin // ar != null // ar.length == dim0 @@ -533,14 +541,16 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { (PointerBlockLength(result)(FramedPtrBlockLength) === sizeArg.get) &* (PointerBlockOffset(result)(FramedPtrBlockOffset) === zero) // Pointer location needs pointer add, not pointer subscript - ensures = - ensures &* makeStruct.makePerm( - i => - PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))( - FramedPtrOffset - ), - IteratedPtrInjective, - ) + if(!isConst) { + ensures = + ensures &* makeStruct.makePerm( + i => + PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))( + FramedPtrOffset + ), + IteratedPtrInjective, + ) + } ensures = if (!typeIsRef(elementType)) ensures @@ -557,15 +567,22 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { ensures else ensures &* foldStar(permFields.map(_._1)) - + val newElementType = dispatch(elementType) + val returnT = { + if(isConst) TConstPointer(newElementType) + else unique.map(TUniquePointer(newElementType, _)).getOrElse(TPointer(newElementType)) + } + val name = if(isConst)"make_const_pointer_array_" + elementType.toString + else "make_pointer_array_" + elementType.toString procedure( blame = AbstractApplicable, contractBlame = TrueSatisfiable, - returnType = TPointer(dispatch(elementType)), + returnType = returnT, args = Seq(sizeArg), requires = UnitAccountedPredicate(requires), ensures = UnitAccountedPredicate(ensures), - )(o.where(name = "make_pointer_array_" + elementType.toString)) + decreases = Some(DecreasesClauseNoRecursion[Post]()) + )(o.where(name = name)) })) } @@ -596,9 +613,9 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { Nil, Nil, )(ArrayCreationFailed(newArr)) - case newPointerArr @ NewPointerArray(element, size) => + case newPointerArr @ NewPointerArray(element, size, unique) => val method = pointerArrayCreationMethods - .getOrElseUpdate(element, makePointerCreationMethodFor(element)) + .getOrElseUpdate((element, unique), makePointerCreationMethodFor(element, unique, false)) ProcedureInvocation[Post]( method.ref, Seq(dispatch(size)), @@ -607,10 +624,20 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { Nil, Nil, )(PointerArrayCreationFailed(newPointerArr)) + case ncpa @ NewConstPointerArray(element, size) => + val method = constPointerArrayCreationMethods + .getOrElseUpdate((element), makePointerCreationMethodFor(element, None, true)) + ProcedureInvocation[Post]( + method.ref, + Seq(dispatch(size)), + Nil, + Nil, + Nil, + Nil, + )(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/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 008ab82b88..7d7a962c11 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -540,6 +540,8 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() ArraySubscript[Post](notInlined(arr), notInlined(index))( SubscriptAssignTarget )(target.o) + case PointerSubscript(arr, index) if arr.t.isInstanceOf[TConstPointer[_]] => + throw DisallowedAssignmentTarget(target) case PointerSubscript(arr, index) => PointerSubscript[Post](notInlined(arr), notInlined(index))( SubscriptAssignTarget diff --git a/src/rewrite/vct/rewrite/TrivialAddrOf.scala b/src/rewrite/vct/rewrite/TrivialAddrOf.scala index edc400f193..84026cf2ad 100644 --- a/src/rewrite/vct/rewrite/TrivialAddrOf.scala +++ b/src/rewrite/vct/rewrite/TrivialAddrOf.scala @@ -98,7 +98,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] { val newPointer = Eval( PreAssignExpression( newTarget, - NewPointerArray(newValue.t, const[Post](1))(PanicBlame("Size is > 0")), + NewPointerArray(newValue.t, const[Post](1), None)(PanicBlame("Size is > 0")), )(blame) ) (newPointer, newTarget, newValue) diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala new file mode 100644 index 0000000000..22f7073ba1 --- /dev/null +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -0,0 +1,441 @@ +package vct.rewrite + +import vct.col.ast.{Expr, _} +import vct.col.origin.Origin +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 { + override def code: String = "disallowedConstAssignment" + override def text: String = + target.o.messageInContext("Cannot assign to constant target.") +} + +case class DisallowedQualifiedType(target: Node[_]) extends UserError { + override def code: String = "disallowedQualifiedType" + override def text: String = + target.o.messageInContext("This qualified type is not allowed.") +} + +case class DisallowedQualifiedMethodCoercion(calledOrigin: Origin) extends UserError { + override def code: String = "disallowedQualifiedMethodCoercion" + override def text: String = + calledOrigin.messageInContext("The coercion of args with qualifiers for this method call is not allowed.") +} + +case class DisallowedQualifiedCoercion(calledOrigin: Origin, source: Type[_], target: Type [_]) extends UserError { + override def code: String = "disallowedQualifiedCoercion" + override def text: String = + calledOrigin.messageInContext(s"The coercion of $source to $target is not allowed.") +} + +case object TypeQualifierCoercion extends RewriterBuilder { + override def key: String = "TypeQualifierCoercion" + override def desc: String = + "Removes qualifiers from types." +} + +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] = { + coercion match { + case CoerceFromConst(_) => + case CoerceToConst(_) => + case CoerceToUnique(_, _) => + case CoerceFromUnique(_, _) => + case CoerceBetweenUnique(_, _, _) => + 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 + } + + 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 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() + } + + 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 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() + } + } + + 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 + } + + def getUnqualified(t: Type[Pre], info: InnerInfo = InnerInfo()): (InnerInfo, Type[Post]) = t match { + case TConst(_) | TUnique(_, _) if info.const || info.unique.isDefined => + throw DisallowedQualifiedType(t) + case TConst(it) => + info.const = true + getUnqualified(it, info) + case TUnique(it, id) => + info.unique = Some(id) + getUnqualified(it, info) + case _ => (info, dispatch(t)) + } + + def makePointer(t: Type[Pre]): Type[Post] = { + implicit val o: Origin = t.o + val (info, resType) = getUnqualified(t) + if(info.const) TConstPointer(resType) + else if (info.unique.isDefined) TUniquePointer(resType, info.unique.get) + else TPointer(resType) + } +} + +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)]) + + def addArgs(params: Seq[Variable[Pre]], args: Seq[Expr[Pre]]): Args = { + Args(params, containsUniqueCoerce(args)) + } + + def argsNoCoercions(args: Seq[Args]) : Boolean = args.forall(_.coercions.isEmpty) + + def removeCoercions(args: Seq[Expr[Pre]]): Seq[Expr[Post]] = args.map({ + case UniquePointerCoercion(e, t) => dispatch(e) + case e => dispatch(e) + }) + + def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] = + xs.zipWithIndex.collect { + case (UniquePointerCoercion(e, target), i) => (UniqueCoercion(e.t, target), i) + } + + def getCoercionMap(coercions: Seq[UniqueCoercion], calledOrigin: Origin): Map[Type[Pre], Type[Post]] = { + coercions.groupMapReduce[Type[Pre], Type[Post]]( + _.originalParamT)( + c => dispatch(c.givenArgT))( + // For any duplicates, we exit if they do not resolve to the same type + (l, r) => if(l == r) l else throw DisallowedQualifiedMethodCoercion(calledOrigin)) + } + + 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) => + // 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) => + if(inv.ref.decl == callee) throw DisallowedQualifiedMethodCoercion(calledOrigin) + inv.ref.decl.body.map(checkBody(_, callee, seenMethods.addOne(inv.ref.decl), calledOrigin)) + case inv: AnyFunctionInvocation[Pre] if !seenMethods.contains(inv.ref.decl) => + if(inv.ref.decl == callee) throw DisallowedQualifiedMethodCoercion(calledOrigin) + inv.ref.decl.body.map(checkBody(_, callee, seenMethods.addOne(inv.ref.decl), calledOrigin)) + } + } + + /* So we need to check the following things: + 1. Any args with a same type that is being coerced, needs to be coerced to the exact same type. + * This is also the case for any given, yields, and out args + 2. Any type that is coerced, cannot be contained in any other type + * 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], 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)) :++ 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, coercedResults, coercedArgs, calledOrigin) // Checks 2 + }) + // 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 + checkedCallees.addOne(original) + } + coercionMap + } + + // Instead of the regular procedure, we create an abstract procedure, which is the same, but with different types + def createAbstractProcedureCopy(original: Procedure[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Procedure[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) + }) + }) + } + } + + // Same for functions + 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({ + // We do copy body, otherwise functions could be different. + original.rewrite() + }) + }) + } + } + + 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) + } + + 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 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] => + 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) + } + + override def dispatch(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case inv: FunctionInvocation[Pre] => + rewriteFunctionInvocation(inv, None) + 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 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()) + } + case f: AbstractMethod[Pre] => callee.having(f){ + checkedCallees.clear() + allScopes.anySucceed(f, f.rewriteDefault()) + } + case other => allScopes.anySucceed(other, other.rewriteDefault()) + } +} diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala index 444e9eae6c..9086e62ce4 100644 --- a/src/rewrite/vct/rewrite/adt/ImportADT.scala +++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala @@ -38,6 +38,8 @@ case object ImportADT { case TRef() => "ref" case TArray(element) => "arr_" + typeText(element) case TPointer(element) => "ptr_" + typeText(element) + case TUniquePointer(element, unique) => "unique_ptr_" + unique.toString + "_" + typeText(element) + case TConstPointer(element) => "const_ptr_" + typeText(element) case TProcess() => "proc" case TModel(Ref(model)) => model.o.getPreferredNameOrElse().camel case TAxiomatic(Ref(adt), args) => diff --git a/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala b/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala new file mode 100644 index 0000000000..01d08693d9 --- /dev/null +++ b/src/rewrite/vct/rewrite/adt/ImportConstPointer.scala @@ -0,0 +1,186 @@ +package vct.col.rewrite.adt + +import vct.col.ast._ +import vct.col.origin._ +import vct.col.rewrite.Generation +import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const} + + +case object ImportConstPointer extends ImportADTBuilder("const_pointer") { + case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_]) + extends Blame[OptionNone] { + override def blame(error: OptionNone): Unit = inner.blame(PointerNull(expr)) + } + + case class PointerBoundsPreconditionFailed( + inner: Blame[PointerBounds], + expr: Node[_], + ) extends Blame[PreconditionFailed] { + override def blame(error: PreconditionFailed): Unit = + inner.blame(PointerBounds(expr)) + } + + case class DerefPointerBoundsPreconditionFailed( + inner: Blame[PointerDerefError], + expr: Expr[_], + ) extends Blame[PreconditionFailed] { + override def blame(error: PreconditionFailed): Unit = + inner.blame(PointerInsufficientPermission(expr)) + } + + case class PointerFieldInsufficientPermission( + inner: Blame[PointerInsufficientPermission], + expr: Expr[_], + ) extends Blame[InsufficientPermission] { + override def blame(error: InsufficientPermission): Unit = + inner.blame(PointerInsufficientPermission(expr)) + } +} + +case class ImportConstPointer[Pre <: Generation](importer: ImportADTImporter) + extends ImportADT[Pre](importer) { + import ImportConstPointer._ + + private lazy val pointerFile = parse("const_pointer") + + private lazy val pointerAdt = find[AxiomaticDataType[Post]]( + pointerFile, + "const_pointer", + ) + private lazy val pointerOf = find[ADTFunction[Post]](pointerAdt, "const_pointer_of") + private lazy val pointerBlock = find[ADTFunction[Post]]( + pointerAdt, + "const_pointer_block", + ) + private lazy val pointerOffset = find[ADTFunction[Post]]( + pointerAdt, + "const_pointer_offset", + ) + private lazy val pointerDeref = find[Function[Post]](pointerFile, "const_ptr_deref") + private lazy val pointerAdd = find[Function[Post]](pointerFile, "const_ptr_add") + + def isConstPointer(e: Expr[Pre]): Boolean = e.t match { + case TConstPointer(_) => true + case _ => false + } + + def getInner(t: Type[Pre]): Type[Pre] = t match { + case TConstPointer(inner) => inner + case _ => ??? + } + + override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( + implicit o: Origin + ): Expr[Post] = + coercion match { + case CoerceNullPointer(TConstPointer(_)) => OptNone() + case other => super.applyCoercion(e, other) + } + + override def postCoerce(t: Type[Pre]): Type[Post] = + t match { + case TConstPointer(inner) => TOption(TAxiomatic(pointerAdt.ref, Seq(dispatch(inner)))) + case other => other.rewriteDefault() + } + + override def postCoerce(location: Location[Pre]): Location[Post] = + location match { + case loc @ PointerLocation(pointer) if isConstPointer(pointer) => + ??? // Should not happen? + case other => other.rewriteDefault() + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case sub @ PointerSubscript(pointer, index) if isConstPointer(pointer) => + val inner = dispatch(getInner(pointer.t)) + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq( + FunctionInvocation[Post]( + ref = pointerAdd.ref, + args = Seq( + OptGet(dispatch(pointer))( + PointerNullOptNone(sub.blame, pointer) + ), + dispatch(index), + ), + typeArgs = Seq(inner), + Nil, + Nil, + )(NoContext(PointerBoundsPreconditionFailed(sub.blame, index))) + ), + typeArgs = Seq(inner), + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")) + case add @ PointerAdd(pointer, offset) if isConstPointer(pointer) => + val inner = dispatch(getInner(pointer.t)) + OptSome( + FunctionInvocation[Post]( + ref = pointerAdd.ref, + args = Seq( + OptGet(dispatch(pointer))(PointerNullOptNone(add.blame, pointer)), + dispatch(offset), + ), + typeArgs = Seq(inner), + Nil, + Nil, + )(NoContext(PointerBoundsPreconditionFailed(add.blame, pointer))) + ) + case deref @ DerefPointer(pointer) if isConstPointer(pointer) => +// val c_pointer = OptGet(dispatch(pointer))(PointerNullOptNone(sub.blame, pointer)) +// // val blame = NoContext(PointerBoundsPreconditionFailed(sub.blame, index)) +// SeqSubscript(c_pointer, dispatch(index))(PanicBlame("TODO: pointer subscript out of bounds")) + val inner = dispatch(getInner(pointer.t)) + FunctionInvocation[Post]( + ref = pointerDeref.ref, + args = Seq( + FunctionInvocation[Post]( + ref = pointerAdd.ref, + // Always index with zero, otherwise quantifiers with pointers do not get triggered + args = Seq( + OptGet(dispatch(pointer))( + PointerNullOptNone(deref.blame, pointer) + ), + const(0), + ), + typeArgs = Seq(inner), + Nil, + Nil, + )(NoContext( + DerefPointerBoundsPreconditionFailed(deref.blame, pointer) + )) + ), + typeArgs = Seq(inner), + Nil, + Nil, + )(PanicBlame("ptr_deref requires nothing.")) + case len @ PointerBlockLength(pointer) if isConstPointer(pointer) => + val inner = dispatch(getInner(pointer.t)) + Size(ADTFunctionInvocation[Post]( + typeArgs = Some((pointerAdt.ref, Seq(inner))), + ref = pointerBlock.ref, + args = Seq( + OptGet(dispatch(pointer))(PointerNullOptNone(len.blame, pointer)) + ), + )) + case off @ PointerBlockOffset(pointer) if isConstPointer(pointer) => + val inner = dispatch(getInner(pointer.t)) + ADTFunctionInvocation[Post]( + typeArgs = Some((pointerAdt.ref, Seq(inner))), + ref = pointerOffset.ref, + args = Seq( + OptGet(dispatch(pointer))(PointerNullOptNone(off.blame, pointer)) + ), + ) + case pointerLen @ PointerLength(pointer) if isConstPointer(pointer) => + postCoerce( + PointerBlockLength(pointer)(pointerLen.blame) - + PointerBlockOffset(pointer)(pointerLen.blame) + ) + case other => other.rewriteDefault() + } + } +} diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala index 2e81faf964..e426e90962 100644 --- a/src/rewrite/vct/rewrite/adt/ImportPointer.scala +++ b/src/rewrite/vct/rewrite/adt/ImportPointer.scala @@ -10,8 +10,8 @@ import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const} import scala.collection.mutable case object ImportPointer extends ImportADTBuilder("pointer") { - private def PointerField(t: Type[_]): Origin = - Origin(Seq(PreferredName(Seq(typeText(t))), LabelContext("pointer field"))) + private def PointerField(t: Type[_], uniqueId: Option[BigInt]): Origin = + Origin(Seq(PreferredName(Seq(typeText(t) + uniqueId.map(_.toString).getOrElse(""))), LabelContext("pointer field"))) case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_]) extends Blame[OptionNone] { @@ -75,14 +75,18 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) private lazy val pointerDeref = find[Function[Post]](pointerFile, "ptr_deref") private lazy val pointerAdd = find[Function[Post]](pointerFile, "ptr_add") - val pointerField: mutable.Map[Type[Post], SilverField[Post]] = mutable.Map() + val pointerField: mutable.Map[(Type[Post], Option[BigInt]), SilverField[Post]] = mutable.Map() private def getPointerField(ptr: Expr[Pre]): Ref[Post, SilverField[Post]] = { - val tElement = dispatch(ptr.t.asPointer.get.element) + val (tElementPre: Type[Pre], uniqueID) = ptr.t.asPointer.get match { + case TUniquePointer(e, i) => (e, Some(i)) + case TPointer(e) => (e, None) + } + val tElement = dispatch(tElementPre) pointerField.getOrElseUpdate( - tElement, { + (tElement, uniqueID), { globalDeclarations - .declare(new SilverField(tElement)(PointerField(tElement))) + .declare(new SilverField(tElement)(PointerField(tElement, uniqueID))) }, ).ref } @@ -98,6 +102,7 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter) override def postCoerce(t: Type[Pre]): Type[Post] = t match { case TPointer(_) => TOption(TAxiomatic(pointerAdt.ref, Nil)) + case TUniquePointer(_, _) => TOption(TAxiomatic(pointerAdt.ref, Nil)) case other => rewriteDefault(other) } 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/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala index 737d301e7c..f3e0d00d9f 100644 --- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala @@ -107,7 +107,7 @@ case object LangCPPToCol { kernelLambda.blame.blame(SYCLKernelLambdaFailure( KernelPostconditionFailed(failure, Right(kernelLambda)) )) - case TerminationMeasureFailed(applicable, apply, measure) => + case error: TerminationMeasureFailed => PanicBlame("Kernel lambdas do not have a termination measure yet") .blame(error) case ContextEverywhereFailedInPost(failure, node) => @@ -510,7 +510,7 @@ case object LangCPPToCol { (node.o, c.descInContext + ", since ..."), (failure.node.o, "... " + failure.descCompletion), ) - case TerminationMeasureFailed(_, _, _) => + case error: TerminationMeasureFailed => PanicBlame( "This kernel class constructor should always be able to terminate." ).blame(error) @@ -2737,11 +2737,11 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) (sizeOption, init.init) match { case (None, None) => throw WrongCPPType(decl) case (Some(size), None) => - val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame) + val newArr = NewPointerArray[Post](t, rw.dispatch(size), None)(cta.blame) Block(Seq(LocalDecl(v), assignLocal(v.get, newArr))) case (None, Some(CPPLiteralArray(exprs))) => val newArr = - NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame) + NewPointerArray[Post](t, c_const[Post](exprs.size), None)(cta.blame) Block( Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++ assignliteralArray(v, exprs, o) @@ -2752,7 +2752,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) if (realSize < exprs.size) logger.warn(s"Excess elements in array initializer: '${decl}'") val newArr = - NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame) + NewPointerArray[Post](t, c_const[Post](realSize), None)(cta.blame) Block( Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++ assignliteralArray(v, exprs.take(realSize.intValue), o) diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index b187e5f7f4..1a0abcfa31 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -54,7 +54,7 @@ case object LangCToCol { ) } - case class WrongCType(decl: CLocalDeclaration[_]) extends UserError { + case class WrongCType(decl: Declaration[_]) extends UserError { override def code: String = "wrongCType" override def text: String = decl.o @@ -391,17 +391,22 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def getBaseType[G](t: Type[G]): Type[G] = t match { - case CPrimitiveType(specs) => C.getPrimitiveType(specs) + 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 } - def castIsId(exprType: Type[Pre], castType: Type[Pre]): Boolean = - (castType, getBaseType(exprType)) match { + def castIsId(exprType: Type[Pre], castType: Type[Pre]): Boolean = { + (getBaseType(castType), getBaseType(exprType)) match { case (tc, te) if tc == te => true case (TCInt(), TBoundedInt(_, _)) => true case (TBoundedInt(_, _), TCInt()) => true case _ => false } + } def cast(c: CCast[Pre]): Expr[Post] = c match { @@ -413,8 +418,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) CastFloat[Post](rw.dispatch(c.expr), rw.dispatch(t))(c.o) case CCast( inv @ CInvocation(CLocal("__vercors_malloc"), Seq(arg), Nil, Nil), - CTPointer(t2), + tcast, ) => + val t2 = tcast match { + case CTPointer(t2) => t2 + case _ => throw UnsupportedMalloc(c) + } val (t1, size) = arg match { case SizeOf(t1) if castIsId(t1, t2) => (t1, c_const[Post](1)(c.o)) @@ -424,7 +433,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) (t1, rw.dispatch(r)) case _ => throw UnsupportedMalloc(c) } - NewPointerArray(rw.dispatch(t1), size)(ArrayMallocFailed(inv))(c.o) + NewPointerArray(rw.dispatch(t2), size, None)(ArrayMallocFailed(inv))(c.o) case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) => throw UnsupportedMalloc(c) case CCast(n @ Null(), t) if t.asPointer.isDefined => rw.dispatch(n) @@ -439,7 +448,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) implicit val o: Origin = cParam.o val varO = o.sourceName(C.getDeclaratorInfo(cParam.declarator).name) val cRef = RefCParam(cParam) - val tp = new TypeProperties(cParam.specifiers, cParam.declarator) + val tp = new TypeProperties(cParam.specifiers, cParam) kernelSpecifier match { case OpenCLKernel() => @@ -480,10 +489,9 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case GPULocal() => throw WrongGPUType(cParam) case GPUGlobal() => throw WrongGPUType(cParam) } - val specType = - cParam.specifiers.collectFirst { case t: CSpecificationType[Pre] => - rw.dispatch(t.t) - }.get + val prop = new TypeProperties(cParam.specifiers, cParam) + if(!prop.validCParam) throw WrongCType(cParam) + val specType = rw.dispatch(prop.mainType.get) cParam.drop() val v = @@ -644,12 +652,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val v = new Variable[Post](TCInt())(varO) dynamicSharedMemLengthVar(d) = v rw.variables.declare(v) -// val decl: Statement[Post] = LocalDecl(cNameSuccessor(d)) val assign: Statement[Post] = assignLocal( Local(cNameSuccessor(d).ref), NewPointerArray[Post]( getInnerType(cNameSuccessor(d).t), - Local(v.ref), + Local(v.ref), None )(PanicBlame("Shared memory sizes cannot be negative.")), ) declarations ++= Seq(cNameSuccessor(d)) @@ -657,13 +664,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) }) staticSharedMemNames.foreach { case (d, (size, blame)) => implicit val o: Origin = getCDecl(d).o -// val decl: Statement[Post] = LocalDecl(cNameSuccessor(d)) val assign: Statement[Post] = assignLocal( Local(cNameSuccessor(d).ref), // Since we set the size and blame together, we can assume the blame is not None NewPointerArray[Post]( getInnerType(cNameSuccessor(d).t), - CIntegerValue(size), + CIntegerValue(size), None )(blame.get), ) declarations ++= Seq(cNameSuccessor(d)) @@ -851,8 +857,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } class TypeProperties( - specs: Seq[CDeclarationSpecifier[Pre]], - decl: CDeclarator[Pre], + specs: Seq[CDeclarationSpecifier[Pre]], decl: Declaration[Pre] ) { var arrayOrPointer = false var global = false @@ -860,27 +865,39 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) var extern = false var innerType: Option[Type[Pre]] = None var arraySize: Option[Expr[Pre]] = None + var mainType: Option[Type[Pre]] = None + var sizeBlame: Option[Blame[ArraySizeError]] = None + var pure = false + var inline = false + var static = false specs.foreach { case GPULocal() => shared = true case GPUGlobal() => global = true - case CSpecificationType(CTPointer(t)) => + case CSpecificationType(t) if isPointerOrArray(t) => + val (inner, size, blame) = getInnerPointerInfo(t).get arrayOrPointer = true - innerType = Some(t) - case CSpecificationType(ctarr @ CTArray(size, t)) => + innerType = Some(inner) + mainType = Some(t) + sizeBlame = blame arraySize = size - innerType = Some(t) - sizeBlame = Some( - ctarr.blame - ) // we set the blame here, together with the size - arrayOrPointer = true + case CSpecificationType(t) => + mainType = Some(t) case CExtern() => extern = true - case _ => + case CPure() => pure = true + case CInline() => inline = true + case CStatic() => static = true + // We want to make sure we process everything + case _ => ??? } def isShared: Boolean = shared && !global def isGlobal: Boolean = !shared && global + def validNonGpu: Boolean = !global && !shared && mainType.isDefined + def validReturn: Boolean = validNonGpu && !static + def validCParam: Boolean = !pure && !inline && validNonGpu && !static + def validCLocal = validCParam } def addDynamicShared( @@ -894,7 +911,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } def addStaticShared( - decl: CDeclarator[Pre], cRef: CNameTarget[Pre], t: Type[Pre], o: Origin, @@ -921,7 +937,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) if (decl.decl.inits.size != 1) throw MultipleSharedMemoryDeclaration(decl) - val prop = new TypeProperties(decl.decl.specs, decl.decl.inits.head.decl) + val prop = new TypeProperties(decl.decl.specs, decl) if (!prop.shared) return false val init: CInit[Pre] = decl.decl.inits.head @@ -942,7 +958,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) !prop.extern ) { addStaticShared( - init.decl, cRef, prop.innerType.get, varO, @@ -958,7 +973,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) !prop.extern ) { addStaticShared( - init.decl, cRef, prop.innerType.get, varO, @@ -1073,12 +1087,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) ): Seq[Statement[Post]] = { implicit val o: Origin = origin (exprs.zipWithIndex.map { case (value, index) => - Assign[Post]( + // Since we model const arrays with sequences internally, we cannot assign to them, so we assume their values + Assume[Post]( AmbiguousSubscript(array.get, c_const(index))(PanicBlame( - "The explicit initialization of an array in C should never generate an assignment that exceeds the bounds of the array" - )), - rw.dispatch(value), - )(PanicBlame("Assignment for an explicit array initializer cannot fail.")) + "The explicit initialization of an array in C should never exceed the bounds of the array" + )) === rw.dispatch(value), + ) }) } @@ -1097,7 +1111,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case CLiteralArray(exprs) if exprs.size == size => Block(Seq( LocalDecl(v), - assignLocal( + assignInitial( v.get, LiteralVector[Post]( rw.dispatch(t.innerType), @@ -1112,43 +1126,40 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def rewriteArrayDeclaration( decl: CLocalDeclaration[Pre], cta: CTArray[Pre], + init: CInit[Pre] ): Statement[Post] = { - // LangTypesToCol makes it so that each declaration only has one init - val init = decl.decl.inits.head + implicit val o: Origin = decl.o val info = C.getDeclaratorInfo(init.decl) - implicit val o: Origin = init.o + val CTArray(sizeOption, oldT) = cta + val it = rw.dispatch(oldT) + val t = TPointer[Post](it) + val v = new Variable[Post](t)(o.sourceName(info.name)) + cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v + val newArrf = (size: Expr[Post]) => { + NewPointerArray[Post](it, size, None)(cta.blame) + } - decl.decl.specs match { - case Seq(CSpecificationType(cta @ CTArray(sizeOption, oldT))) => - val t = rw.dispatch(oldT) - val v = new Variable[Post](TPointer(t))(o.sourceName(info.name)) - cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v - - (sizeOption, init.init) match { - case (None, None) => throw WrongCType(decl) - case (Some(size), None) => - val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame) - Block(Seq(LocalDecl(v), assignLocal(v.get, newArr))) - case (None, Some(CLiteralArray(exprs))) => - val newArr = - NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame) - Block( - Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++ - assignliteralArray(v, exprs, o) - ) - case (Some(size), Some(CLiteralArray(exprs))) => - val realSize = isConstantInt(size).filter(_ >= 0) - .getOrElse(throw WrongCType(decl)) - if (realSize < exprs.size) - logger.warn(s"Excess elements in array initializer: '${decl}'") - val newArr = - NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame) - Block( - Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++ - assignliteralArray(v, exprs.take(realSize.intValue), o) - ) - case _ => throw WrongCType(decl) - } + (sizeOption, init.init) match { + case (None, None) => throw WrongCType(decl) + case (Some(size), None) => + val newArr = newArrf(rw.dispatch(size)) + Block(Seq(LocalDecl(v), assignInitial(v.get, newArr))) + case (None, Some(CLiteralArray(exprs))) => + val newArr = newArrf(c_const[Post](exprs.size)) + Block( + Seq(LocalDecl(v), assignInitial(v.get, newArr)) ++ + assignliteralArray(v, exprs, o) + ) + case (Some(size), Some(CLiteralArray(exprs))) => + val realSize = isConstantInt(size).filter(_ >= 0) + .getOrElse(throw WrongCType(decl)) + if (realSize < exprs.size) + logger.warn(s"Excess elements in array initializer: '${decl}'") + val newArr = newArrf(c_const[Post](realSize)) + Block( + Seq(LocalDecl(v), assignInitial(v.get, newArr)) ++ + assignliteralArray(v, exprs.take(realSize.intValue), o) + ) case _ => throw WrongCType(decl) } } @@ -1177,27 +1188,23 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) ) ).getOrElse(NewObject[Post](targetClass.ref)) - Block(Seq(LocalDecl(v), assignLocal(v.get, initialVal))) + Block(Seq(LocalDecl(v), assignInitial(v.get, initialVal))) } def rewriteLocal(decl: CLocalDeclaration[Pre]): Statement[Post] = { decl.drop() - decl.decl.specs.foreach { - case _: CSpecificationType[Pre] => - case _ => throw WrongCType(decl) - } - + val prop = new TypeProperties(decl.decl.specs, decl) + if(!prop.validCLocal) throw WrongCType(decl) // LangTypesToCol makes it so that each declaration only has one init val init = decl.decl.inits.head - val t = - decl.decl.specs.collectFirst { case t: CSpecificationType[Pre] => t.t } - .get match { + val t = prop.mainType.get match { case t: CTVector[Pre] if init.init.collect({ case _: CLiteralArray[Pre] => true }).isDefined => return rewriteVectorDeclaration(decl, t, init) - case t: CTArray[Pre] => return rewriteArrayDeclaration(decl, t) + case t: CTArray[Pre] => + return rewriteArrayDeclaration(decl, t, init) case t: CTStruct[Pre] => return rewriteStructDeclaration(decl, t) case t => rw.dispatch(t) } @@ -1207,7 +1214,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v implicit val o: Origin = init.o init.init.map(value => - Block(Seq(LocalDecl(v), assignLocal(v.get, rw.dispatch(value)))) + Block(Seq(LocalDecl(v), assignInitial(v.get, rw.dispatch(value)))) ).getOrElse(LocalDecl(v)) } @@ -1247,14 +1254,49 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(KernelBarrierFailure(barrier)) } - def isPointer(t: Type[Pre]): Boolean = getPointer(t).isDefined + def getInnerPointerInfo(t: Type[Pre]) : Option[(Type[Pre], Option[Expr[Pre]], Option[Blame[ArraySizeError]])] = + getBaseType(t) match { + case TPointer(it) => Some((it, None, None)) + case CTPointer(it) => Some((it, None, None)) + case a@CTArray(size, it) => Some((it, size, Some(a.blame))) + case _ => None + } + + def isVector(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t : CTVector[Pre] => true + case _ => false + } - def getPointer(t: Type[Pre]): Option[TPointer[Pre]] = + def isArray(t: Type[Pre]): Boolean = getBaseType(t) match { - case t @ TPointer(_) => Some(t) + case t : CTArray[Pre] => true + case _ => false + } + + def isStruct(t: Type[Pre]): Boolean = getStruct(t).isDefined + + def getStruct(t: Type[Pre]): Option[CTStruct[Pre]] = + getBaseType(t) match { + case t : CTStruct[Pre] => Some(t) case _ => None } + def isPointer(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t @ TPointer(_) => true + case t @ CTPointer(_) => true + case _ => false + } + + def isPointerOrArray(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t @ TPointer(_) => true + case t @ CTPointer(_) => true + case t @ CTArray(_, _) => true + case _ => false + } + def isNumeric(t: Type[Pre]): Boolean = getBaseType(t) match { case _: NumericType[Pre] => true @@ -1410,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]( @@ -1445,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, @@ -1489,8 +1533,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) Seq( LocalDecl(vCopy), LocalDecl(vValue), - assignLocal(vValue.get, value), - assignLocal(vCopy.get, NewObject[Post](targetClass.ref)), + assignInitial(vValue.get, value), + assignInitial(vCopy.get, NewObject[Post](targetClass.ref)), ) ++ fieldAssigns ), vCopy.get, @@ -1634,7 +1678,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val before: Statement[Post] = Block[Post](Seq( LocalDecl(rhs_val)(rhs.o), - assignLocal(rhs_val.get(rhs.o), rhs)(rhs.o), + assignInitial(rhs_val.get(rhs.o), rhs)(rhs.o), ))(assign.o) // Assign the correct values @@ -1664,12 +1708,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(assign.o) } - def isCPointer(t: Type[_]) = - getBaseType(t) match { - case CTPointer(_) => true - case _ => false - } - def indexVectors( e: Expr[Post], askedType: Type[Post], @@ -1707,7 +1745,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val v = new Variable[Post](e.t) val befores: Seq[Statement[Post]] = Seq( LocalDecl(v), - assignLocal(v.get, e), + assignInitial(v.get, e), ) (befores, v.get) } @@ -1936,7 +1974,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) (e.name, args, givenMap, yields) match { case (_, _, g, y) if g.nonEmpty || y.nonEmpty => - case ("__vercors_free", Seq(xs), _, _) if isCPointer(xs.t) => + case ("__vercors_free", Seq(xs), _, _) if isPointer(xs.t) => return FreePointer[Post](rw.dispatch(xs))(inv.blame)(inv.o) case _ => () } @@ -1972,8 +2010,9 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } } - def pointerType(t: CTPointer[Pre]): Type[Post] = { - TPointer(rw.dispatch(t.innerType)) + def pointerType(t: CPointerType[Pre]): Type[Post] = t match { + case CTPointer(innerType) => TPointer(rw.dispatch(innerType)) + case CTArray(_, innerType) => TPointer(rw.dispatch(innerType)) } def vectorType(t: CType[Pre]): Type[Post] = { @@ -1995,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 250b6d9eba..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) @@ -390,11 +388,13 @@ case class LangSpecificToCol[Pre <: Generation]( override def dispatch(t: Type[Pre]): Type[Post] = t match { case t: JavaTClass[Pre] => java.classType(t) + case t: CPointerType[Pre] => c.pointerType(t) case t: CTPointer[Pre] => c.pointerType(t) case t: CTVector[Pre] => c.vectorType(t) 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 6b7f9fe8eb..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) @@ -115,12 +125,14 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { implicit o: Origin ): (Seq[CDeclarationSpecifier[Post]], CDeclarator[Post]) = { val info = C.getDeclaratorInfo(declarator) - val baseType = C.getPrimitiveType(specifiers, context) - val otherSpecifiers = specifiers - .filter(!_.isInstanceOf[CTypeSpecifier[Pre]]).map(dispatch) - val newSpecifiers = + val (specs, otherSpecifiers) = specifiers + .partition({case _ : CTypeSpecifier[Pre] => true; case _: CTypeQualifierDeclarationSpecifier[Pre] => true; + case _ => false}) + val newOtherSpecifiers = otherSpecifiers.map(dispatch) + val baseType = C.getPrimitiveType(specs, context) + val newSpecifiers : Seq[CDeclarationSpecifier[LangTypesToCol.this.Post]] = CSpecificationType[Post](dispatch(info.typeOrReturnType(baseType))) +: - otherSpecifiers + newOtherSpecifiers val newDeclarator = info.params match { case Some(params) => @@ -202,6 +214,17 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { case CDeclaration(_, _, Seq(_: CStructDeclaration[Pre]), Seq()) => globalDeclarations .succeed(declaration, declaration.rewriteDefault()) + case decl@CDeclaration(_, _, Seq(td: CTypedef[Pre], struct: CStructDeclaration[Pre]), Seq(init)) => + val structDecl = + new CGlobalDeclaration[Post]( + CDeclaration[Post](dispatch(decl.contract), + dispatch(decl.kernelInvariant), + Seq(dispatch(struct)), Seq())(decl.o))(decl.o) + val structSpec = CStructSpecifier[Post](struct.name.get)(decl.o) + structSpec.ref = Some(RefCStruct(structDecl)) + + globalDeclarations + .succeed(declaration, structDecl) case decl => decl.inits.foreach(init => { implicit val o: Origin = init.o @@ -226,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/src/viper/viper/api/backend/SilverBackend.scala b/src/viper/viper/api/backend/SilverBackend.scala index d6de5f6324..fe85a4ac33 100644 --- a/src/viper/viper/api/backend/SilverBackend.scala +++ b/src/viper/viper/api/backend/SilverBackend.scala @@ -288,18 +288,10 @@ trait SilverBackend case PredicateNotWellformed(_, reason, _) => defer(reason) case FunctionTerminationError(node: Infoed, reason, _) => val apply = get[col.Invocation[_]](node) - apply.ref.decl.blame.blame(blame.TerminationMeasureFailed( - apply.ref.decl, - apply, - getDecreasesClause(reason), - )) + apply.ref.decl.blame.blame(getDecreasesBlame(apply, reason)) case MethodTerminationError(node: Infoed, reason, _) => - val apply = get[col.Invocation[_]](node) - apply.ref.decl.blame.blame(blame.TerminationMeasureFailed( - apply.ref.decl, - apply, - getDecreasesClause(reason), - )) + val apply = get[col.InvokingNode[_]](node) + apply.ref.decl.blame.blame(getDecreasesBlame(apply, reason)) case LoopTerminationError(node: Infoed, reason, _) => val decreases = get[col.DecreasesClause[_]](node) info(node).invariant.get.blame @@ -396,6 +388,19 @@ trait SilverBackend case _ => ??? } + def getDecreasesBlame(invoking: col.InvokingNode[_], reason: ErrorReason) : blame.TerminationMeasureFailed = { + reason match { + case TerminationConditionFalse(node: Infoed) => + val procedure = get[col.Procedure[_]](node) + blame.CallTerminationMeasureFailed(invoking, procedure) + case _ => blame.DecreaseTerminationMeasureFailed( + invoking.ref.decl, + invoking, + getDecreasesClause(reason), + ) + } + } + def getDecreasesClause(reason: ErrorReason): col.DecreasesClause[_] = reason match { case TerminationConditionFalse(node) => diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala new file mode 100644 index 0000000000..dad6a34f8f --- /dev/null +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -0,0 +1,453 @@ +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" + + vercors should verify using silicon in "same uniques pointer parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}""" + vercors should verify using silicon in "same uniques array parameter" c """void f(/*@ unique<1> @*/ int x0[], /*@ unique<1> @*/ int x1[]){x1 = x0;}""" + vercors should verify using silicon in "same uniques local" c """void f(){/*@ unique<1> @*/ int x0[2]; /*@ unique<1> @*/ int* x1; x1 = x0;}""" + 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; 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 + """#include + void f(){/*@ unique<1> @*/ int* x0; x0 = (/*@ unique<2> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}""" + + vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 1" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}""" + vercors should error withCode "disallowedQualifiedCoercion" in "diff uniques pointer of unique pointer - 2" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<1> @*/ int * /*@ unique<4> @*/ * x1; x0 = x1;}""" + vercors should error withCode "resolutionError:type" in "diff uniques pointer of unique pointer - 3" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0; /*@ unique<3> @*/ int * /*@ unique<2> @*/ * x1; x0 = x1;}""" + + vercors should error withCode "cTypeNotSupported" in "multiple uniques" c """void f(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}""" + vercors should error withCode "disallowedQualifiedCoercion" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}""" + vercors should error withCode "disallowedQualifiedCoercion" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}""" + vercors should error withCode "disallowedQualifiedCoercion" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}""" + vercors should error withCode "disallowedQualifiedCoercion" in "multiple uniques parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}""" + + vercors should verify using silicon in "Assign to init const" c """void f(){const int x = 2; /*@ assert x == 2; @*/}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local const" c """void f(){const int x; x = 0;}""" + 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 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;}""" + + vercors should error withCode "disallowedConstAssignment" in "Assign const pointer" c """void f(int* const y){int* const x; y = x;}""" + vercors should verify using silicon in "Assign element of const pointer" c + """/*@ context x!=NULL ** \pointer_length(x) == 1 ** Perm(&x[0], write); ensures x[0] == 1;@*/ + void f(int * const x){x[0] = 1;}""" + + vercors should verify using silicon in "Call non-unique procedure" 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) + h(x1); + } + + /*@ + 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 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 @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return x0[0] + x1[0]; + } + else { + 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); + } +} + +/*@ + 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); + 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 "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; +}""" + + 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 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(),