From 68ec4908c09637b1933f7ed5eed0bb4b95db77b3 Mon Sep 17 00:00:00 2001 From: Lars Date: Fri, 12 Jan 2024 11:24:43 +0100 Subject: [PATCH] First try at adding vectors --- res/universal/res/adt/vector.pvl | 8 ++ src/col/vct/col/ast/Node.scala | 4 + .../ambiguous/AmbiguousSubscriptImpl.scala | 2 + .../literal/build/LiteralVectorImpl.scala | 13 ++ .../op/collection/VectorSubscriptImpl.scala | 12 ++ .../family/coercion/CoerceMapVectorImpl.scala | 8 ++ src/col/vct/col/ast/type/TSetImpl.scala | 2 +- src/col/vct/col/ast/type/TVectorImpl.scala | 10 ++ .../vct/col/ast/type/typeclass/TypeImpl.scala | 1 + src/col/vct/col/feature/FeatureRainbow.scala | 2 + src/col/vct/col/origin/Blame.scala | 13 ++ .../vct/col/typerules/CoercingRewriter.scala | 12 +- src/col/vct/col/typerules/CoercionUtils.scala | 9 ++ src/col/vct/col/typerules/Types.scala | 2 + src/main/vct/main/stages/Transformation.scala | 1 + src/parsers/antlr4/SpecLexer.g4 | 1 + src/parsers/antlr4/SpecParser.g4 | 3 + .../vct/parsers/transform/PVLToCol.scala | 2 + src/rewrite/vct/rewrite/Disambiguate.scala | 1 + src/rewrite/vct/rewrite/ParBlockEncoder.scala | 2 + .../ResolveExpressionSideEffects.scala | 8 ++ src/rewrite/vct/rewrite/adt/ImportADT.scala | 1 + .../vct/rewrite/adt/ImportVector.scala | 135 ++++++++++++++++++ 23 files changed, 250 insertions(+), 2 deletions(-) create mode 100644 res/universal/res/adt/vector.pvl create mode 100644 src/col/vct/col/ast/expr/literal/build/LiteralVectorImpl.scala create mode 100644 src/col/vct/col/ast/expr/op/collection/VectorSubscriptImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceMapVectorImpl.scala create mode 100644 src/col/vct/col/ast/type/TVectorImpl.scala create mode 100644 src/rewrite/vct/rewrite/adt/ImportVector.scala diff --git a/res/universal/res/adt/vector.pvl b/res/universal/res/adt/vector.pvl new file mode 100644 index 0000000000..0821b63e5d --- /dev/null +++ b/res/universal/res/adt/vector.pvl @@ -0,0 +1,8 @@ +adt `vector` { + pure T vector_loc(`vector` v, int i); +} + + decreases; + requires 0 <= i; + requires i < 4; +pure T v4loc(`vector` a, int i) = `vector`.vector_loc(a, i); \ 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 84a9b01eab..127b2ae90c 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -129,6 +129,7 @@ final case class TOption[G](element: Type[G])(implicit val o: Origin = Diagnosti final case class TTuple[G](elements: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TTupleImpl[G] final case class TEither[G](left: Type[G], right: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TEitherImpl[G] final case class TMatrix[G](element: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TMatrixImpl[G] +final case class TVector[G](element: Type[G], size: BigInt)(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TVectorImpl[G] sealed trait PrimitiveType[G] extends Type[G] with PrimitiveTypeImpl[G] final case class TAny[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TAnyImpl[G] @@ -417,6 +418,7 @@ final case class CoerceMapTuple[G](inner: Seq[Coercion[G]], sourceTypes: Seq[Typ final case class CoerceMapEither[G](inner: (Coercion[G], Coercion[G]), sourceTypes: (Type[G], Type[G]), targetTypes: (Type[G], Type[G]))(implicit val o: Origin) extends Coercion[G] with CoerceMapEitherImpl[G] final case class CoerceMapSeq[G](inner: Coercion[G], sourceSeqElement: Type[G], targetSeqElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapSeqImpl[G] final case class CoerceMapSet[G](inner: Coercion[G], sourceSetElement: Type[G], targetSetElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapSetImpl[G] +final case class CoerceMapVector[G](inner: Coercion[G], sourceVectorElement: Type[G], targetVectorElement: Type[G], size: BigInt)(implicit val o: Origin) extends Coercion[G] with CoerceMapVectorImpl[G] final case class CoerceMapBag[G](inner: Coercion[G], sourceBagElement: Type[G], targetBagElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapBagImpl[G] final case class CoerceMapMatrix[G](inner: Coercion[G], sourceMatrixElement: Type[G], targetMatrixElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapMatrixImpl[G] final case class CoerceMapMap[G](inner: Coercion[G], sourceTypes: (Type[G], Type[G]), targetTypes: (Type[G], Type[G]))(implicit val o: Origin) extends Coercion[G] with CoerceMapMapImpl[G] @@ -440,6 +442,7 @@ final case class LiteralSet[G](element: Type[G], values: Seq[Expr[G]])(implicit final case class LiteralBag[G](element: Type[G], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralBagImpl[G] final case class LiteralTuple[G](ts: Seq[Type[G]], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralTupleImpl[G] final case class LiteralMap[G](k: Type[G], v: Type[G], values: Seq[(Expr[G], Expr[G])])(implicit val o: Origin) extends Expr[G] with LiteralMapImpl[G] +final case class LiteralVector[G](element: Type[G], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralVectorImpl[G] final case class UntypedLiteralSeq[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralSeqImpl[G] final case class UntypedLiteralSet[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralSetImpl[G] final case class UntypedLiteralBag[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralBagImpl[G] @@ -646,6 +649,7 @@ final case class FreePointer[G](pointer: Expr[G])(val blame: Blame[PointerFreeEr final case class Old[G](expr: Expr[G], at: Option[Ref[G, LabelDecl[G]]])(val blame: Blame[LabelNotReached])(implicit val o: Origin) extends Expr[G] with OldImpl[G] final case class AmbiguousSubscript[G](collection: Expr[G], index: Expr[G])(val blame: Blame[FrontendSubscriptError])(implicit val o: Origin) extends Expr[G] with AmbiguousSubscriptImpl[G] final case class SeqSubscript[G](seq: Expr[G], index: Expr[G])(val blame: Blame[SeqBoundFailure])(implicit val o: Origin) extends Expr[G] with SeqSubscriptImpl[G] +final case class VectorSubscript[G](seq: Expr[G], index: Expr[G])(val blame: Blame[VectorBoundFailure])(implicit val o: Origin) extends Expr[G] with VectorSubscriptImpl[G] final case class ArraySubscript[G](arr: Expr[G], index: Expr[G])(val blame: Blame[ArraySubscriptError])(implicit val o: Origin) extends Expr[G] with ArraySubscriptImpl[G] final case class PointerSubscript[G](pointer: Expr[G], index: Expr[G])(val blame: Blame[PointerSubscriptError])(implicit val o: Origin) extends Expr[G] with PointerSubscriptImpl[G] final case class Length[G](arr: Expr[G])(val blame: Blame[ArrayNull])(implicit val o: Origin) extends Expr[G] with LengthImpl[G] diff --git a/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala b/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala index ebe92c8b0c..fa37731f0b 100644 --- a/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala +++ b/src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala @@ -8,6 +8,7 @@ import vct.col.ast.ops.AmbiguousSubscriptOps trait AmbiguousSubscriptImpl[G] extends AmbiguousSubscriptOps[G] { this: AmbiguousSubscript[G] => def isSeqOp: Boolean = CoercionUtils.getAnySeqCoercion(collection.t).isDefined + def isVectorOp: Boolean = CoercionUtils.getAnyVectorCoercion(collection.t).isDefined def isArrayOp: Boolean = CoercionUtils.getAnyArrayCoercion(collection.t).isDefined def isCArrayOp: Boolean = CoercionUtils.getAnyCArrayCoercion(collection.t).isDefined def isCPPArrayOp: Boolean = CoercionUtils.getAnyCPPArrayCoercion(collection.t).isDefined @@ -16,6 +17,7 @@ trait AmbiguousSubscriptImpl[G] extends AmbiguousSubscriptOps[G] { this: Ambiguo override lazy val t: Type[G] = if (isSeqOp) collection.t.asSeq.get.element + else if (isVectorOp) collection.t.asVector.get.element else if (isArrayOp) collection.t.asArray.get.element else if (isCArrayOp) collection.t.asCArray.get.innerType else if (isCPPArrayOp) collection.t.asCPPArray.get.innerType diff --git a/src/col/vct/col/ast/expr/literal/build/LiteralVectorImpl.scala b/src/col/vct/col/ast/expr/literal/build/LiteralVectorImpl.scala new file mode 100644 index 0000000000..8ff541fda1 --- /dev/null +++ b/src/col/vct/col/ast/expr/literal/build/LiteralVectorImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.expr.literal.build + +import vct.col.ast.{LiteralVector, TVector, Type} +import vct.col.print.{Ctx, Doc, Group, Precedence, Text} +import vct.col.ast.ops.LiteralVectorOps + +trait LiteralVectorImpl[G] extends LiteralVectorOps[G] { this: LiteralVector[G] => + override def t: Type[G] = TVector(element, values.size) + + override def precedence: Int = Precedence.POSTFIX + override def layout(implicit ctx: Ctx): Doc = + Group(Text("vector<") <> element <> "," <> values.size.toString <> ">{" <> Doc.args(values) <> "}") +} diff --git a/src/col/vct/col/ast/expr/op/collection/VectorSubscriptImpl.scala b/src/col/vct/col/ast/expr/op/collection/VectorSubscriptImpl.scala new file mode 100644 index 0000000000..c63e387f4c --- /dev/null +++ b/src/col/vct/col/ast/expr/op/collection/VectorSubscriptImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.expr.op.collection + +import vct.col.ast.{VectorSubscript, Type} +import vct.col.print.{Ctx, Doc, Precedence, Group} +import vct.col.ast.ops.VectorSubscriptOps + +trait VectorSubscriptImpl[G] extends VectorSubscriptOps[G] { this: VectorSubscript[G] => + override def t: Type[G] = seq.t.asVector.get.element + + override def precedence: Int = Precedence.POSTFIX + override def layout(implicit ctx: Ctx): Doc = Group(assoc(seq) <> "[" <> Doc.arg(index) <> "]") +} \ No newline at end of file diff --git a/src/col/vct/col/ast/family/coercion/CoerceMapVectorImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceMapVectorImpl.scala new file mode 100644 index 0000000000..80fe9ff0f6 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceMapVectorImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceMapVector, TVector} +import vct.col.ast.ops.CoerceMapVectorOps + +trait CoerceMapVectorImpl[G] extends CoerceMapVectorOps[G] { this: CoerceMapVector[G] => + override def target: TVector[G] = TVector(targetVectorElement, size) +} diff --git a/src/col/vct/col/ast/type/TSetImpl.scala b/src/col/vct/col/ast/type/TSetImpl.scala index 0f2a8f1336..a906060f9c 100644 --- a/src/col/vct/col/ast/type/TSetImpl.scala +++ b/src/col/vct/col/ast/type/TSetImpl.scala @@ -6,5 +6,5 @@ import vct.col.ast.ops.TSetOps trait TSetImpl[G] extends TSetOps[G] { this: TSet[G] => override def layout(implicit ctx: Ctx): Doc = - Group(Text("seq") <> open <> Doc.arg(element) <> close) + Group(Text("set") <> open <> Doc.arg(element) <> close) } \ No newline at end of file diff --git a/src/col/vct/col/ast/type/TVectorImpl.scala b/src/col/vct/col/ast/type/TVectorImpl.scala new file mode 100644 index 0000000000..c921fc5ef9 --- /dev/null +++ b/src/col/vct/col/ast/type/TVectorImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.`type` + +import vct.col.ast.TVector +import vct.col.ast.ops.TVectorOps +import vct.col.print.{Ctx, Doc, Group, Text} + +trait TVectorImpl[G] extends TVectorOps[G] { this: TVector[G] => + override def layout(implicit ctx: Ctx): Doc = + Group(Text("vector") <> open <> Doc.arg(element) <> "," <> size.toString <> close) +} \ No newline at end of file diff --git a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala index 2ef0e5e572..05a839677b 100644 --- a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala +++ b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala @@ -16,6 +16,7 @@ trait TypeImpl[G] extends TypeFamilyOps[G] { this: Type[G] => def asSeq: Option[TSeq[G]] = CoercionUtils.getAnySeqCoercion(this).map(_._2) def asSet: Option[TSet[G]] = CoercionUtils.getAnySetCoercion(this).map(_._2) + 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]] = CoercionUtils.getAnyPointerCoercion(this).map(_._2) def asArray: Option[TArray[G]] = CoercionUtils.getAnyArrayCoercion(this).map(_._2) diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala index e65252f085..dc47c7a92e 100644 --- a/src/col/vct/col/feature/FeatureRainbow.scala +++ b/src/col/vct/col/feature/FeatureRainbow.scala @@ -486,6 +486,7 @@ class FeatureRainbow[G] { case node: LiteralSet[G] => SilverAxiomaticLibraryType case node: SeqMember[G] => SilverAxiomaticLibraryType case node: SeqSubscript[G] => SilverAxiomaticLibraryType + case node: VectorSubscript[G] => SilverAxiomaticLibraryType case node: SeqUpdate[G] => SilverAxiomaticLibraryType case node: SetIntersection[G] => SilverAxiomaticLibraryType case node: SetMember[G] => SilverAxiomaticLibraryType @@ -502,6 +503,7 @@ 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 cb7ec89e09..461ec92211 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -409,6 +409,19 @@ case class SeqBoundExceedsLength(node: SeqSubscript[_]) extends SeqBoundFailure override def inlineDescWithSource(source: String): String = s"The index in `$source` may exceed the length of the sequence." } +sealed trait VectorBoundFailure extends FrontendSubscriptError with BuiltinError +case class VectorBoundNegative(node: VectorSubscript[_]) extends VectorBoundFailure with NodeVerificationFailure { + override def code: String = "vecIndexNegative" + override def descInContext: String = "The index in this vector subscript may be negative." + override def inlineDescWithSource(source: String): String = s"The index in `$source` may be negative." +} +case class VectorBoundExceedsLength(node: VectorSubscript[_]) extends VectorBoundFailure with NodeVerificationFailure { + override def code: String = "vecIndexExceedsLength" + override def descInContext: String = "The index in this vector subscript may exceed the length of the vector." + override def inlineDescWithSource(source: String): String = s"The index in `$source` may exceed the length of the vector." +} + + sealed trait ForkFailure extends VerificationFailure case class ForkNull(node: Fork[_]) extends ForkFailure with NodeVerificationFailure { override def code: String = "forkNull" diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index a275600c4a..b4958f9908 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -340,6 +340,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t) case None => throw IncoercibleText(e, s"set") } + def vector(e: Expr[Pre]): (Expr[Pre], TVector[Pre]) = + CoercionUtils.getAnyVectorCoercion(e.t) match { + case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t) + case None => throw IncoercibleText(e, s"set") + } def bag(e: Expr[Pre]): (Expr[Pre], TBag[Pre]) = CoercionUtils.getAnyBagCoercion(e.t) match { case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t) @@ -680,8 +685,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite ) case AmbiguousResult() => e case sub @ AmbiguousSubscript(collection, index) => - firstOk(e, s"Expected collection to be a sequence, array, pointer or map, but got ${collection.t}.", + firstOk(e, s"Expected collection to be a sequence, vector, array, pointer or map, but got ${collection.t}.", AmbiguousSubscript(seq(collection)._1, int(index))(sub.blame), + AmbiguousSubscript(vector(collection)._1, int(index))(sub.blame), AmbiguousSubscript(array(collection)._1, int(index))(sub.blame), AmbiguousSubscript(pointer(collection)._1, int(index))(sub.blame), AmbiguousSubscript(map(collection)._1, coerce(index, map(collection)._2.key))(sub.blame), @@ -905,6 +911,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite LiteralSeq(element, values.map(coerce(_, element))) case LiteralSet(element, values) => LiteralSet(element, values.map(coerce(_, element))) + case LiteralVector(element, values) => + LiteralVector(element, values.map(coerce(_, element))) case LiteralTuple(ts, values) => LiteralTuple(ts, values.zip(ts).map { case (v, t) => coerce(v, t) @@ -1396,6 +1404,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite VectorCompare(coerce(coercedLeft, seqType), coerce(coercedRight, seqType)) case VectorRepeat(e) => VectorRepeat(e) + case get @ VectorSubscript(xs, index) => + VectorSubscript(vector(xs)._1, int(index))(get.blame) case VectorSum(indices, vec) => VectorSum(coerce(indices, TSeq[Pre](TInt())), coerce(vec, TSeq[Pre](TRational()))) case Void() => diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index baade080b2..507bb25fa0 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -51,6 +51,8 @@ case object CoercionUtils { CoerceMapSeq(getAnyCoercion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget) case (TSet(innerSource), TSet(innerTarget)) => CoerceMapSet(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget) + case (TVector(innerSource, sizeSource), TVector(innerTarget, sizeTarget)) if sizeSource == sizeTarget => + CoerceMapVector(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget, sizeTarget) case (TBag(innerSource), TBag(innerTarget)) => CoerceMapBag(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget) case (TMatrix(innerSource), TMatrix(innerTarget)) => @@ -258,6 +260,13 @@ case object CoercionUtils { case _ => None } + def getAnyVectorCoercion[G](source: Type[G]): Option[(Coercion[G], TVector[G])] = source match { + case t: CPrimitiveType[G] => chainCCoercion(t, getAnyVectorCoercion) + case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyVectorCoercion) + case t: TVector[G] => Some((CoerceIdentity(source), t)) + case _ => None + } + def getAnyBagCoercion[G](source: Type[G]): Option[(Coercion[G], TBag[G])] = source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBagCoercion) case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBagCoercion) diff --git a/src/col/vct/col/typerules/Types.scala b/src/col/vct/col/typerules/Types.scala index cd50410071..b691a06bf0 100644 --- a/src/col/vct/col/typerules/Types.scala +++ b/src/col/vct/col/typerules/Types.scala @@ -40,6 +40,8 @@ object Types { TSeq(leastCommonSuperType(left, right)) case (TSet(left), TSet(right)) => TSet(leastCommonSuperType(left, right)) + case (TVector(left, sizeLeft), TVector(right, sizeRight)) if sizeLeft == sizeRight => + TVector(leastCommonSuperType(left, right), sizeLeft) case (TBag(left), TBag(right)) => TBag(leastCommonSuperType(left, right)) case (TMatrix(left), TMatrix(right)) => diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index c95973ca3a..b650ffe7f4 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -280,6 +280,7 @@ case class SilverTransformation EnumToDomain, ImportArray.withArg(adtImporter), ImportPointer.withArg(adtImporter), + ImportVector.withArg(adtImporter), ImportMapCompat.withArg(adtImporter), ImportEither.withArg(adtImporter), ImportTuple.withArg(adtImporter), diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index 7cbd85c12a..1c24b178e4 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -41,6 +41,7 @@ VAL_REF: 'ref'; VAL_RATIONAL: 'rational'; VAL_SEQ: 'seq'; VAL_SET: 'set'; +VAL_VECTOR: 'vector'; VAL_BAG: 'bag'; VAL_POINTER: 'pointer'; VAL_MAP: 'map'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index 3715fd6cd9..3b0fad167c 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -3,6 +3,7 @@ parser grammar SpecParser; /** imported grammar rules langExpr + langConstInt langId langType langModifier @@ -156,6 +157,7 @@ valMapPairs valPrimaryCollectionConstructor : 'seq' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralSeq | 'set' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralSet + | 'vector' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralVector | 'set' '<' langType '>' '{' langExpr '|' valSetCompSelectors ';' langExpr '}' # valSetComprehension | 'bag' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralBag | 'map' '<' langType ',' langType '>' '{' valMapPairs? '}' # valTypedLiteralMap @@ -338,6 +340,7 @@ valType : ('resource' | 'process' | 'frac' | 'zfrac' | 'rational' | 'bool' | 'ref' | 'any' | 'nothing' | 'string') # valPrimaryType | 'seq' '<' langType '>' # valSeqType | 'set' '<' langType '>' # valSetType + | 'vector' '<' langType ',' langConstInt '>' # valVectorType | 'bag' '<' langType '>' # valBagType | 'option' '<' langType '>' # valOptionType | 'map' '<' langType ',' langType '>' # valMapType diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 4955f71e7f..08fb8645b9 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -1009,6 +1009,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, } case ValSeqType(_, _, element, _) => TSeq(convert(element)) case ValSetType(_, _, element, _) => TSet(convert(element)) + case ValVectorType(_, _, element, _, size, _) => TVector(convert(element), convert(size)) case ValBagType(_, _, element, _) => TBag(convert(element)) case ValOptionType(_, _, element, _) => TOption(convert(element)) case ValMapType(_, _, key, _, value, _) => TMap(convert(key), convert(value)) @@ -1041,6 +1042,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, def convert(implicit e: ValPrimaryCollectionConstructorContext): Expr[G] = e match { case ValTypedLiteralSeq(_, _, t, _, _, exprs, _) => LiteralSeq(convert(t), exprs.map(convert(_)).getOrElse(Nil)) case ValTypedLiteralSet(_, _, t, _, _, exprs, _) => LiteralSet(convert(t), exprs.map(convert(_)).getOrElse(Nil)) + case ValTypedLiteralVector(_, _, t, _, _, exprs, _) => LiteralVector(convert(t), exprs.map(convert(_)).getOrElse(Nil)) case ValSetComprehension(_, _, t, _, _, value, _, selectors, _, something, _) => ??(e) case ValTypedLiteralBag(_, _, t, _, _, exprs, _) => LiteralBag(convert(t), exprs.map(convert(_)).getOrElse(Nil)) case ValTypedLiteralMap(_, _, key, _, value, _, _, pairs, _) => LiteralMap(convert(key), convert(value), pairs.map(convert(_)).getOrElse(Nil)) diff --git a/src/rewrite/vct/rewrite/Disambiguate.scala b/src/rewrite/vct/rewrite/Disambiguate.scala index b3e9b57b0f..292675f767 100644 --- a/src/rewrite/vct/rewrite/Disambiguate.scala +++ b/src/rewrite/vct/rewrite/Disambiguate.scala @@ -105,6 +105,7 @@ case class Disambiguate[Pre <: Generation]() extends Rewriter[Pre] { else if(op.isMapOp) MapGet(dispatch(collection), dispatch(index))(op.blame) else if(op.isArrayOp) ArraySubscript(dispatch(collection), dispatch(index))(op.blame) else if(op.isSeqOp) SeqSubscript(dispatch(collection), dispatch(index))(op.blame) + else if(op.isVectorOp) VectorSubscript(dispatch(collection), dispatch(index))(op.blame) else throw Unreachable("AmbiguousSubscript must subscript a pointer, map, array, or seq because of the type check.") case op @ AmbiguousMember(x, xs) => if(op.isMapOp) MapMember(dispatch(x), dispatch(xs)) diff --git a/src/rewrite/vct/rewrite/ParBlockEncoder.scala b/src/rewrite/vct/rewrite/ParBlockEncoder.scala index 8154acb5bf..324dc96d91 100644 --- a/src/rewrite/vct/rewrite/ParBlockEncoder.scala +++ b/src/rewrite/vct/rewrite/ParBlockEncoder.scala @@ -223,6 +223,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] { case PointerSubscript(pointer, index) => combine(scanForAssignE(pointer), scanForAssignE(index)) case ArraySubscript(pointer, index) => combine(scanForAssignE(pointer), scanForAssignE(index)) case SeqSubscript(seq, index) => combine(scanForAssignE(seq), scanForAssignE(index)) + case VectorSubscript(vec, index) => combine(scanForAssignE(vec), scanForAssignE(index)) case _ => None } @@ -231,6 +232,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] { case ArraySubscript(arr, index) => combine(scanAssignTarget(arr), scanForAssignE(index)) case PointerSubscript(pointer, index) => combine(scanAssignTarget(pointer), scanForAssignE(index)) case SeqSubscript(seq, index) => combine(scanAssignTarget(seq), scanForAssignE(index)) + case VectorSubscript(vec, index) => combine(scanAssignTarget(vec), scanForAssignE(index)) case _ => None } diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 5519b00dde..ea2e01d414 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -32,6 +32,12 @@ case object ResolveExpressionSideEffects extends RewriterBuilder { ) ) + case class DisallowedAssignmentTarget(target: Expr[_]) extends UserError { + override def code: String = "disallowedAssignmentTarget" + override def text: String = + target.o.messageInContext("This target cannot be assigned to.") + } + case class DisallowedSideEffect(effector: Expr[_]) extends UserError { override def code: String = "sideEffect" override def text: String = @@ -409,6 +415,8 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr case ArraySubscript(arr, index) => ArraySubscript[Post](notInlined(arr), notInlined(index))(SubscriptAssignTarget)(target.o) case PointerSubscript(arr, index) => PointerSubscript[Post](notInlined(arr), notInlined(index))(SubscriptAssignTarget)(target.o) case deref @ DerefPointer(ptr) => DerefPointer[Post](notInlined(ptr))(deref.blame)(target.o) + case VectorSubscript(_, _) => throw DisallowedAssignmentTarget(target) + case SeqSubscript(_, _) => throw DisallowedAssignmentTarget(target) case other => ??? } flushExtractedExpressions() diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala index 933cd21810..1227b5863a 100644 --- a/src/rewrite/vct/rewrite/adt/ImportADT.scala +++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala @@ -46,6 +46,7 @@ case object ImportADT { case TEither(left, right) => "either$" + typeText(left) + "__" + typeText(right) + "$" case TSeq(element) => "seq_" + typeText(element) case TSet(element) => "set_" + typeText(element) + case TVector(element, size) => "vector" + size.toString + "_" + typeText(element) case TBag(element) => "bag_" + typeText(element) case TMatrix(element) => "mat_" + typeText(element) case TType(t) => "typ_" + typeText(t) diff --git a/src/rewrite/vct/rewrite/adt/ImportVector.scala b/src/rewrite/vct/rewrite/adt/ImportVector.scala new file mode 100644 index 0000000000..27abcd8de8 --- /dev/null +++ b/src/rewrite/vct/rewrite/adt/ImportVector.scala @@ -0,0 +1,135 @@ +package vct.col.rewrite.adt + +import vct.col.ast._ +import vct.col.origin._ +import vct.col.ref.Ref +import vct.col.rewrite._ +import vct.col.util.AstBuildHelpers._ + +import scala.collection.mutable + +case object ImportVector extends ImportADTBuilder("vector") { + case class VectorBoundsPreconditionFailed(inner: Blame[VectorBoundFailure], subscript: VectorSubscript[_]) extends Blame[PreconditionFailed] { + override def blame(error: PreconditionFailed): Unit = error.path match { + case FailLeft +: _ => inner.blame(VectorBoundNegative(subscript)) + case FailRight +: _ => inner.blame(VectorBoundExceedsLength(subscript)) + case _ => ??? + } + } +} + +case class ImportVector[Pre <: Generation](importer: ImportADTImporter) extends ImportADT[Pre](importer) { + import ImportVector._ + private lazy val vectorFile = parse("vector") + private lazy val vectorAdt = find[AxiomaticDataType[Post]](vectorFile, "vector") + private lazy val vector_loc = find[ADTFunction[Post]](vectorAdt, "vector_loc") + + val makeVectorMethods: mutable.Map[BigInt, Function[Post]] = mutable.Map() + val vLocMethods: mutable.Map[BigInt, Function[Post]] = mutable.Map() + + def vlocMake(size: BigInt): Function[Post] = { + implicit val o: Origin = Origin(Seq(LabelContext("vector access method"))) + /* for instance for size 4: + decreases; + requires 0 <= i; + requires i < 4; + pure T v4loc(`vector` a, int i) = `vector`.vector_loc(a, i); + */ + globalDeclarations.declare(withResult((result: Result[Post]) => { + val elementTypeVar = new Variable[Post](TType(TAnyValue()))(o.where(name= "T")) + val elementType = TVar[Post](elementTypeVar.ref) + val tVec = TAxiomatic[Post](vectorAdt.ref, Seq(elementType)) + + val a = new Variable[Post](tVec)(o.where(name= "a")) + val i = new Variable[Post](TInt())(o.where(name= "i")) + + val requires: Seq[Expr[Post]] = Seq(const[Post](0) <= i.get, i.get < const[Post](size)) + val body = ADTFunctionInvocation[Post](Some((vectorAdt.ref, Seq(elementType))), vector_loc.ref, Seq(a.get, i.get)) + + function( + blame = AbstractApplicable, + contractBlame = TrueSatisfiable, + typeArgs = Seq(elementTypeVar), + body = Some(body), + returnType = elementType, + args = Seq(a, i), + requires = SplitAccountedPredicate(UnitAccountedPredicate(requires(0)), UnitAccountedPredicate(requires(1))), + ensures = UnitAccountedPredicate(tt) + )(o.where(name= "v" + size.toString + "loc")) + })) + } + + def makeVectorCreation(size: BigInt): Function[Post] = { + implicit val o: Origin = Origin(Seq(LabelContext("vector creation method"))) + /* for instance for size 4: + decreases; + ensures vloc(\result, 0) == x0; + ensures vloc(\result, 1) == x1; + ensures vloc(\result, 2) == x2; + ensures vloc(\result, 3) == x3; + pure `vector` make_v4(T x0, T x1, T x2, T x3); + */ + globalDeclarations.declare(withResult((result: Result[Post]) => { + val elementTypeVar = new Variable[Post](TType(TAnyValue()))(o.where(name= "T")) + val elementType = TVar[Post](elementTypeVar.ref) + + val xs = Seq.tabulate(size.toInt)(x => new Variable[Post](elementType)(o.where(name= f"x$x"))) + val ensures: Seq[Expr[Post]] = xs.zipWithIndex.map({case (x, i) => Eq( + makeSubScript(result, const[Post](i), elementType, size, PanicBlame("Cannot Fail"), o), x.get)}) + + function( + blame = AbstractApplicable, + contractBlame = TrueSatisfiable, + typeArgs = Seq(elementTypeVar), + returnType = TAxiomatic[Post](vectorAdt.ref, Seq(elementType)), + args = xs, + requires = UnitAccountedPredicate(tt), + ensures = UnitAccountedPredicate(foldAnd(ensures)) + )(o.where(name= "make_v" + size.toString)) + })) + } + + override def postCoerce(t: Type[Pre]): Type[Post] = t match { + case TVector(inner, size) => TAxiomatic[Post](vectorAdt.ref, Seq(dispatch(inner)))(t.o) + case other => other.rewriteDefault() + } + + def typeArgs(xs: Expr[Pre]): Option[(Ref[Post, AxiomaticDataType[Post]], Seq[Type[Post]])] = + typeArgs(xs.t.asVector.get.element) + + def typeArgs(t: Type[Pre]): Option[(Ref[Post, AxiomaticDataType[Post]], Seq[Type[Post]])] = + Some((vectorAdt.ref, Seq(dispatch(t)))) + + def makeSubScript(vec: Expr[Post], index: Expr[Post], elementType: Type[Post], size: BigInt, blame: Blame[InvocationFailure], o: Origin) = { + val vloc = vLocMethods.getOrElseUpdate(size, vlocMake(size)) + + FunctionInvocation[Post]( + typeArgs = Seq(elementType), + ref = vloc.ref, + args = Seq(vec, index), + givenMap = Nil, + yields = Nil)(blame)(o) + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = e match { + case LiteralVector(element, xs) => + val makeVector = makeVectorMethods.getOrElseUpdate(xs.size, makeVectorCreation(xs.size)) + + FunctionInvocation[Post]( + typeArgs = Seq(dispatch(element)), + ref = makeVector.ref, + args = xs.map[Expr[Post]](dispatch), + givenMap = Nil, + yields = Nil + )(PanicBlame("No requires"))(e.o) + case sub@VectorSubscript(vec, index) => + val (elementT, size) = vec.t match { + case TVector(inner, size) => (inner, size) + case _ => ??? + } + makeSubScript(dispatch(vec), dispatch(index), dispatch(elementT), size, + NoContext(VectorBoundsPreconditionFailed(sub.blame, sub)), e.o) + + case other => other.rewriteDefault() + } +}