From c957125555dbec5c8fefca6b7ae0be7fba551718 Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 1 Jul 2024 12:03:32 +0200 Subject: [PATCH 01/12] Syntax and parsing of unique specifier --- examples/concepts/unique/arrays.c | 16 +++++++++++ src/col/vct/col/ast/Node.scala | 2 ++ src/col/vct/col/ast/lang/c/CUniqueImpl.scala | 9 +++++++ src/parsers/antlr4/SpecLexer.g4 | 1 + src/parsers/antlr4/SpecParser.g4 | 1 + .../vct/parsers/transform/CToCol.scala | 4 +++ src/parsers/vct/parsers/transform/ToCol.scala | 9 +++++++ src/rewrite/vct/rewrite/lang/LangCToCol.scala | 27 +++++++++++++++---- .../examples/UniqueFieldsSpec.scala | 9 +++++++ 9 files changed, 73 insertions(+), 5 deletions(-) create mode 100644 examples/concepts/unique/arrays.c create mode 100644 src/col/vct/col/ast/lang/c/CUniqueImpl.scala create mode 100644 test/main/vct/test/integration/examples/UniqueFieldsSpec.scala diff --git a/examples/concepts/unique/arrays.c b/examples/concepts/unique/arrays.c new file mode 100644 index 0000000000..7b63fcdace --- /dev/null +++ b/examples/concepts/unique/arrays.c @@ -0,0 +1,16 @@ + +/*@ + context_everywhere x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<1> @*/ /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){ + /*@ + loop_invariant 0 <= j && j <= n; + loop_invariant (\forall int i; 0<=i && i + override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Text("unique<") <> i.toString() <> ">") +} diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index c8a683e390..c96d691c95 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -58,6 +58,7 @@ VAL_STRING: 'string'; VAL_PURE: 'pure'; VAL_THREAD_LOCAL: 'thread_local'; VAL_BIP_ANNOTATION: 'bip_annotation'; +VAL_UNIQUE: 'unique'; VAL_WITH: 'with'; VAL_THEN: 'then'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index d7b73b3d24..b1351d8e48 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -417,6 +417,7 @@ valImpureDef valModifier : ('pure' | 'inline' | 'thread_local' | 'bip_annotation') | langStatic # valStatic + | 'unique' '<' langConstInt '>' # valUnique ; valArgList diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index 9e1a47ab97..1f1f16a891 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -168,10 +168,13 @@ case class CToCol[G]( else if (m.consume(m.inline)) CInline[G]() else + m.consume(m.unique).map(CUnique[G](_)).getOrElse( + fail( m.nodes.head, "This modifier cannot be attached to a declaration in C", ) + ) }, ) } @@ -1183,6 +1186,7 @@ case class CToCol[G]( case "thread_local" => collector.threadLocal += mod } case ValStatic(_) => collector.static += mod + case ValUnique(_, _, i, _) => collector.unique += ((mod, convert(i))) } def convertEmbedWith( diff --git a/src/parsers/vct/parsers/transform/ToCol.scala b/src/parsers/vct/parsers/transform/ToCol.scala index e2861443a7..e9a6a45653 100644 --- a/src/parsers/vct/parsers/transform/ToCol.scala +++ b/src/parsers/vct/parsers/transform/ToCol.scala @@ -130,6 +130,8 @@ abstract class ToCol[G]( val static: mutable.ArrayBuffer[ParserRuleContext] = mutable.ArrayBuffer() val bipAnnotation: mutable.ArrayBuffer[ParserRuleContext] = mutable .ArrayBuffer() + val unique: mutable.ArrayBuffer[(ParserRuleContext, BigInt)] = mutable + .ArrayBuffer() def consume(buffer: mutable.ArrayBuffer[ParserRuleContext]): Boolean = { val result = buffer.nonEmpty @@ -137,6 +139,13 @@ abstract class ToCol[G]( result } + def consume(buffer: mutable.ArrayBuffer[(ParserRuleContext, BigInt)]): Option[BigInt] = { + buffer match { + case mutable.ArrayBuffer() => None + case (_, i) +: _ => buffer.clear(); Some(i) + } + } + def nodes: Seq[ParserRuleContext] = Seq(pure, inline, threadLocal, static, bipAnnotation).flatten } diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index b187e5f7f4..c911e27612 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -30,6 +30,12 @@ case object LangCToCol { example.o.messageInContext("Global variables in C are not supported.") } + case class CDeclarationSpecifierNotSupported(spec: CDeclarationSpecifier[_]) extends UserError { + override def code: String = "notSupportedTypeDecl" + override def text: String = + spec.o.messageInContext("This decleration specifier is not supported.") + } + case class MultipleSharedMemoryDeclaration(decl: Node[_]) extends UserError { override def code: String = "multipleSharedMemoryDeclaration" override def text: String = @@ -860,14 +866,21 @@ 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 unique: Option[BigInt] = None + var static = false specs.foreach { case GPULocal() => shared = true case GPUGlobal() => global = true - case CSpecificationType(CTPointer(t)) => + case CSpecificationType(t@CTPointer(it)) => arrayOrPointer = true - innerType = Some(t) + innerType = Some(it) + mainType = Some(t) case CSpecificationType(ctarr @ CTArray(size, t)) => arraySize = size innerType = Some(t) @@ -875,7 +888,14 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) ctarr.blame ) // we set the blame here, together with the size arrayOrPointer = true + mainType = Some(t) + case CSpecificationType(t) => + mainType = Some(t) case CExtern() => extern = true + case CUnique(i) => unique = Some(i) + case CPure() => pure = true + case CInline() => inline = true + case CStatic() => static = true case _ => } @@ -894,7 +914,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } def addStaticShared( - decl: CDeclarator[Pre], cRef: CNameTarget[Pre], t: Type[Pre], o: Origin, @@ -942,7 +961,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) !prop.extern ) { addStaticShared( - init.decl, cRef, prop.innerType.get, varO, @@ -958,7 +976,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) !prop.extern ) { addStaticShared( - init.decl, cRef, prop.innerType.get, varO, diff --git a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala new file mode 100644 index 0000000000..ec3d171d8a --- /dev/null +++ b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala @@ -0,0 +1,9 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +class UniqueFieldsSpec extends VercorsSpec { + vercors should verify using silicon example "concepts/unique/arrays.c" + + vercors should error withCode "???" in """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}""" +} From 020fb357a15deca7918c1ffc213dc37bc5c507f2 Mon Sep 17 00:00:00 2001 From: Lars Date: Tue, 2 Jul 2024 16:26:37 +0200 Subject: [PATCH 02/12] First version working for function parameters --- examples/concepts/unique/arrays.c | 2 +- src/col/vct/col/ast/Node.scala | 11 ++++-- .../vct/col/ast/type/PointerTypeImpl.scala | 9 +++++ .../vct/col/ast/type/TUniquePointerImpl.scala | 16 ++++++++ .../vct/col/ast/type/typeclass/TypeImpl.scala | 2 +- .../vct/col/typerules/CoercingRewriter.scala | 11 +----- src/col/vct/col/typerules/CoercionUtils.scala | 4 +- .../vct/rewrite/adt/ImportPointer.scala | 17 ++++++--- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 38 ++++++++++--------- .../examples/UniqueFieldsSpec.scala | 5 ++- 10 files changed, 76 insertions(+), 39 deletions(-) create mode 100644 src/col/vct/col/ast/type/PointerTypeImpl.scala create mode 100644 src/col/vct/col/ast/type/TUniquePointerImpl.scala diff --git a/examples/concepts/unique/arrays.c b/examples/concepts/unique/arrays.c index 7b63fcdace..d5cd108b26 100644 --- a/examples/concepts/unique/arrays.c +++ b/examples/concepts/unique/arrays.c @@ -5,7 +5,7 @@ context_everywhere x2 != NULL ** \pointer_length(x2) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<1> @*/ /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){ +int main(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){ /*@ loop_invariant 0 <= j && j <= n; loop_invariant (\forall int i; 0<=i && i + + val element: Type[G] +} 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/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 312647796a..dbc1bd349a 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -538,7 +538,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) @@ -2145,14 +2145,7 @@ 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 Assume(assn) => Assume(bool(assn)) case Block(statements) => Block(statements) case Branch(branches) => diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 47295af0af..f3e90b9042 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -122,6 +122,7 @@ case object CoercionUtils { case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target) case (TNull(), TAnyClass()) => CoerceNullAnyClass() case (TNull(), TPointer(target)) => CoerceNullPointer(target) + case (TNull(), TUniquePointer(target, id)) => CoerceNullPointer(target) case (TNull(), CTPointer(target)) => CoerceNullPointer(target) case (TNull(), TEnum(target)) => CoerceNullEnum(target) @@ -425,10 +426,11 @@ case object CoercionUtils { def getAnyPointerCoercion[G]( source: Type[G] - ): Option[(Coercion[G], TPointer[G])] = + ): Option[(Coercion[G], PointerType[G])] = source match { case t: CPrimitiveType[G] => chainCCoercion(t, getAnyPointerCoercion) case t: TPointer[G] => Some((CoerceIdentity(source), t)) + case t: TUniquePointer[G] => Some((CoerceIdentity(source), t)) case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType))) case t: CTArray[G] => 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/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index c911e27612..fe76585abd 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -30,12 +30,6 @@ case object LangCToCol { example.o.messageInContext("Global variables in C are not supported.") } - case class CDeclarationSpecifierNotSupported(spec: CDeclarationSpecifier[_]) extends UserError { - override def code: String = "notSupportedTypeDecl" - override def text: String = - spec.o.messageInContext("This decleration specifier is not supported.") - } - case class MultipleSharedMemoryDeclaration(decl: Node[_]) extends UserError { override def code: String = "multipleSharedMemoryDeclaration" override def text: String = @@ -60,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 @@ -445,7 +439,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() => @@ -486,10 +480,11 @@ 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 = if(prop.unique.isEmpty) + rw.dispatch(prop.mainType.get) else + TUniquePointer(rw.dispatch(prop.innerType.get), prop.unique.get)(cParam.o) cParam.drop() val v = @@ -635,6 +630,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) t match { case TArray(element) => element case TPointer(element) => element + case TUniquePointer(element, _) => element case _ => throw Unreachable("Already checked on pointer or array type") } @@ -857,8 +853,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 @@ -892,15 +887,22 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case CSpecificationType(t) => mainType = Some(t) case CExtern() => extern = true + case CUnique(i) if unique.isDefined => throw WrongCType(decl) case CUnique(i) => unique = Some(i) case CPure() => pure = true case CInline() => inline = true case CStatic() => static = true - case _ => + // We want to make sure we process everything + case _ => ??? } def isShared: Boolean = shared && !global def isGlobal: Boolean = !shared && global + def validNonGpu: Boolean = !global && !shared && + (unique.isEmpty || (unique.isDefined && arrayOrPointer)) && mainType.isDefined + def validReturn: Boolean = validNonGpu && !static + def validCParam: Boolean = !pure && !inline && validNonGpu && !static + def validCLocal = validCParam } def addDynamicShared( @@ -940,7 +942,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 @@ -1266,9 +1268,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def isPointer(t: Type[Pre]): Boolean = getPointer(t).isDefined - def getPointer(t: Type[Pre]): Option[TPointer[Pre]] = + def getPointer(t: Type[Pre]): Option[Type[Pre]] = getBaseType(t) match { case t @ TPointer(_) => Some(t) + case t @ TUniquePointer(_, _) => Some(t) + case t @ CTPointer(_) => Some(t) case _ => None } diff --git a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala index ec3d171d8a..8fc4d821d0 100644 --- a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala +++ b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala @@ -5,5 +5,8 @@ import vct.test.integration.helper.VercorsSpec class UniqueFieldsSpec extends VercorsSpec { vercors should verify using silicon example "concepts/unique/arrays.c" - vercors should error withCode "???" in """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}""" + vercors should error withCode "wrongCType" in "multiple uniques" c """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}""" + vercors should error withCode "resolutionError:type" in "different uniques local" c """int main(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}""" + vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}""" + vercors should verify using silicon in "same uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}""" } From 8b43f3fe0088d5a4548607da708a5e4d4f15d20d Mon Sep 17 00:00:00 2001 From: Lars Date: Tue, 2 Jul 2024 17:30:11 +0200 Subject: [PATCH 03/12] Small fix for array types --- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index fe76585abd..d2aa6bfe68 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -876,11 +876,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) arrayOrPointer = true innerType = Some(it) mainType = Some(t) - case CSpecificationType(ctarr @ CTArray(size, t)) => + case CSpecificationType(t @ CTArray(size, it)) => arraySize = size - innerType = Some(t) + innerType = Some(it) sizeBlame = Some( - ctarr.blame + t.blame ) // we set the blame here, together with the size arrayOrPointer = true mainType = Some(t) From d4b7900a2c5214d968c40069996ba57b8017f534 Mon Sep 17 00:00:00 2001 From: Lars Date: Fri, 19 Jul 2024 18:42:50 +0200 Subject: [PATCH 04/12] Added qualifers (const, unique), const pointers, decrease fix --- examples/concepts/unique/arrays.c | 3 +- res/universal/res/adt/const_pointer.pvl | 27 +++ src/col/vct/col/ast/Node.scala | 59 +++++- .../heap/alloc/NewConstPointerArrayImpl.scala | 9 + .../expr/heap/alloc/NewPointerArrayImpl.scala | 9 +- .../ast/expr/heap/alloc/NewPointerImpl.scala | 16 ++ .../coercion/CoerceBetweenUniqueImpl.scala | 9 + .../CoerceDecreasePrecisionImpl.scala | 3 +- .../family/coercion/CoerceFromConstImpl.scala | 9 + .../coercion/CoerceFromUniqueImpl.scala | 9 + .../CoerceIncreasePrecisionImpl.scala | 3 +- .../coercion/CoerceNullPointerImpl.scala | 3 +- .../family/coercion/CoerceToConstImpl.scala | 9 + .../family/coercion/CoerceToUniqueImpl.scala | 9 + .../ast/family/coercion/CoercionImpl.scala | 5 + .../ast/lang/c/CPointerDeclaratorImpl.scala | 2 +- .../vct/col/ast/lang/c/CPointerTypeImpl.scala | 9 + .../ast/statement/terminal/AssignImpl.scala | 34 +-- .../terminal/AssignInitialImpl.scala | 9 + .../statement/terminal/AssignStmtImpl.scala | 41 ++++ src/col/vct/col/ast/type/TConstImpl.scala | 9 + .../vct/col/ast/type/TConstPointerImpl.scala | 11 + src/col/vct/col/ast/type/TUniqueImpl.scala | 9 + .../vct/col/ast/unsorted/ToUniqueImpl.scala | 10 + src/col/vct/col/check/Check.scala | 2 +- src/col/vct/col/feature/FeatureRainbow.scala | 4 +- src/col/vct/col/origin/Blame.scala | 24 ++- src/col/vct/col/resolve/lang/C.scala | 95 +++++---- .../vct/col/typerules/CoercingRewriter.scala | 12 +- src/col/vct/col/typerules/CoercionUtils.scala | 111 ++++++++-- src/col/vct/col/util/AstBuildHelpers.scala | 4 + src/main/vct/main/stages/Transformation.scala | 32 +-- src/parsers/antlr4/LangCParser.g4 | 1 + src/parsers/antlr4/SpecParser.g4 | 10 +- .../vct/parsers/transform/CToCol.scala | 20 +- src/parsers/vct/parsers/transform/ToCol.scala | 9 - .../vct/rewrite/EncodeArrayValues.scala | 56 +++-- .../ResolveExpressionSideEffects.scala | 2 + src/rewrite/vct/rewrite/TrivialAddrOf.scala | 2 +- .../vct/rewrite/TypeQualifierCoercion.scala | 97 +++++++++ src/rewrite/vct/rewrite/adt/ImportADT.scala | 2 + .../vct/rewrite/adt/ImportConstPointer.scala | 186 ++++++++++++++++ .../vct/rewrite/lang/LangCPPToCol.scala | 10 +- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 198 +++++++++--------- .../vct/rewrite/lang/LangSpecificToCol.scala | 1 + .../vct/rewrite/lang/LangTypesToCol.scala | 12 +- .../viper/api/backend/SilverBackend.scala | 27 ++- .../integration/examples/QualifierSpec.scala | 52 +++++ .../examples/UniqueFieldsSpec.scala | 12 -- 49 files changed, 988 insertions(+), 309 deletions(-) create mode 100644 res/universal/res/adt/const_pointer.pvl create mode 100644 src/col/vct/col/ast/expr/heap/alloc/NewConstPointerArrayImpl.scala create mode 100644 src/col/vct/col/ast/expr/heap/alloc/NewPointerImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceBetweenUniqueImpl.scala rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceDecreasePrecisionImpl.scala (73%) create mode 100644 src/col/vct/col/ast/family/coercion/CoerceFromConstImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceFromUniqueImpl.scala rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceIncreasePrecisionImpl.scala (73%) create mode 100644 src/col/vct/col/ast/family/coercion/CoerceToConstImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceToUniqueImpl.scala create mode 100644 src/col/vct/col/ast/lang/c/CPointerTypeImpl.scala create mode 100644 src/col/vct/col/ast/statement/terminal/AssignInitialImpl.scala create mode 100644 src/col/vct/col/ast/statement/terminal/AssignStmtImpl.scala create mode 100644 src/col/vct/col/ast/type/TConstImpl.scala create mode 100644 src/col/vct/col/ast/type/TConstPointerImpl.scala create mode 100644 src/col/vct/col/ast/type/TUniqueImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/ToUniqueImpl.scala create mode 100644 src/rewrite/vct/rewrite/TypeQualifierCoercion.scala create mode 100644 src/rewrite/vct/rewrite/adt/ImportConstPointer.scala create mode 100644 test/main/vct/test/integration/examples/QualifierSpec.scala delete mode 100644 test/main/vct/test/integration/examples/UniqueFieldsSpec.scala diff --git a/examples/concepts/unique/arrays.c b/examples/concepts/unique/arrays.c index d5cd108b26..0c684806c7 100644 --- a/examples/concepts/unique/arrays.c +++ b/examples/concepts/unique/arrays.c @@ -1,11 +1,10 @@ - /*@ context_everywhere x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<2> @*/ int* x2){ +int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1, /*@ unique<3> @*/ int* x2){ /*@ loop_invariant 0 <= j && j <= n; loop_invariant (\forall int i; 0<=i && i { + 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 7f6dc8d707..5d79517d4d 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -133,6 +133,12 @@ final case class TType[G](t: Type[G])(implicit val o: Origin = DiagnosticOrigin) 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] sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G] final case class TPointer[G](element: Type[G])( @@ -141,6 +147,9 @@ final case class TPointer[G](element: Type[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] @@ -329,10 +338,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) @@ -928,6 +943,24 @@ 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 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] @@ -974,7 +1007,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]])( @@ -1822,10 +1855,18 @@ 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 ToUnique[G](inner: Expr[G])(implicit val o: Origin) extends Expr[G] with ToUniqueImpl[G] + final case class FreePointer[G](pointer: Expr[G])( val blame: Blame[PointerFreeError] )(implicit val o: Origin) @@ -2494,8 +2535,6 @@ final case class CPure[G]()(implicit val o: Origin) extends CSpecificationModifier[G] with CPureImpl[G] final case class CInline[G]()(implicit val o: Origin) extends CSpecificationModifier[G] with CInlineImpl[G] -final case class CUnique[G](i: BigInt)(implicit val o: Origin) - extends CSpecificationModifier[G] with CUniqueImpl[G] sealed trait CStorageClassSpecifier[G] extends CDeclarationSpecifier[G] with CStorageClassSpecifierImpl[G] @@ -2575,6 +2614,8 @@ 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] sealed trait CFunctionSpecifier[G] extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G] @@ -2768,6 +2809,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)( @@ -2778,11 +2821,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/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/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/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/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/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/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/unsorted/ToUniqueImpl.scala b/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala new file mode 100644 index 0000000000..b0027cfc17 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.unsorted + +import vct.col.ast.{TAny, ToUnique} +import vct.col.ast.ops.ToUniqueOps +import vct.col.print._ + +trait ToUniqueImpl[G] extends ToUniqueOps[G] { this: ToUnique[G] => + // Solve typing immediately in TypeQualifiersCoercion pass + def t: vct.col.ast.Type[G] = TAny[G]() +} diff --git a/src/col/vct/col/check/Check.scala b/src/col/vct/col/check/Check.scala index 023d37aa63..5e76bdacb7 100644 --- a/src/col/vct/col/check/Check.scala +++ b/src/col/vct/col/check/Check.scala @@ -243,7 +243,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 d960b5a188..8a11320579 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 @@ -506,7 +509,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 0ba83a7534..9aa0e4f096 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -319,11 +319,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 with SeqCallableFailure + +case class DecreaseTerminationMeasureFailed( applicable: ContractApplicable[_], - apply: Invocation[_], + apply: InvokingNode[_], measure: DecreasesClause[_], -) extends ContractedFailure with SeqCallableFailure with VerificationFailure { +) extends TerminationMeasureFailed { override def code: String = "decreasesFailed" override def position: String = measure.o.shortPositionText override def desc: String = @@ -335,6 +338,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/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 720f63286e..709c4bf10d 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -1,5 +1,6 @@ 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} @@ -10,7 +11,7 @@ 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 +67,18 @@ 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 _ => 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 +87,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 +95,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,16 +128,6 @@ 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], context: Option[Node[G]] = None, @@ -142,17 +135,20 @@ case object C { 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) + info.typeOrReturnType(getPrimitiveType(specs, context)) } 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 +160,20 @@ 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, nonTypeSpecs) = specs.filter { + case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false + }.partition { case _: CTypeSpecifier[G] => true; case _ => false } + + var unique: Option[BigInt] = None + var constant: Boolean = false + nonTypeSpecs.foreach({ + case CTypeQualifierDeclarationSpecifier(CUnique(i)) if unique.isEmpty => unique = Some(i) + case CTypeQualifierDeclarationSpecifier(CConst()) => constant = true + case _ => throw CTypeNotSupported(context) + }) val t: Type[G] = - filteredSpecs match { + typeSpecs match { case Seq(CVoid()) => TVoid() case Seq(CChar()) => TChar() case CUnsigned() +: t if INTEGER_LIKE_TYPES.contains(t) => TCInt() @@ -189,10 +193,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) } + + nonTypeSpecs.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } + .foldLeft(res)(qualify[G]) } def nameFromDeclarator(declarator: CDeclarator[_]): String = @@ -263,30 +270,26 @@ 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) + } + def getCStructDeref[G]( decl: CGlobalDeclaration[G], name: String, diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index dbc1bd349a..aa8b141b44 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -263,6 +263,11 @@ 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 @@ -1564,8 +1569,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)) @@ -2146,6 +2153,7 @@ abstract class CoercingRewriter[Pre <: Generation]() stat match { case a @ Assert(assn) => Assert(res(assn))(a.blame) 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) => diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index f3e90b9042..fca0b8b7f0 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -25,7 +25,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(), @@ -121,9 +169,8 @@ case object CoercionUtils { CoerceNullClass(target, typeArgs) case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target) case (TNull(), TAnyClass()) => CoerceNullAnyClass() - case (TNull(), TPointer(target)) => CoerceNullPointer(target) - case (TNull(), TUniquePointer(target, id)) => 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 => @@ -215,7 +262,7 @@ 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) @@ -371,6 +418,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 } @@ -379,6 +428,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 } @@ -389,6 +440,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), @@ -407,6 +460,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 } @@ -417,6 +472,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)) @@ -428,16 +485,14 @@ case object CoercionUtils { source: Type[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: CPrimitiveType[G] => chainCCoercion(t, getAnyPointerCoercion) - case t: TPointer[G] => Some((CoerceIdentity(source), t)) - case t: TUniquePointer[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)) @@ -449,6 +504,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 } @@ -458,6 +515,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 } @@ -468,6 +527,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), @@ -492,6 +553,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 => @@ -520,6 +583,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 } @@ -528,6 +593,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 } @@ -538,6 +605,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 } @@ -548,6 +617,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 } @@ -558,6 +629,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 } @@ -568,6 +641,8 @@ 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: TUnion[G] => @@ -595,6 +670,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 } @@ -605,6 +682,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 } @@ -616,6 +695,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 } @@ -627,6 +708,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 } @@ -638,6 +721,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 24894abb69..6aadf8813a 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 a9d1230ccd..7ae9b723e2 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -18,39 +18,15 @@ 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 import vct.result.VerificationError.SystemError import vct.rewrite.adt.ImportSetCompat -import vct.rewrite.{ - EncodeAutoValue, - EncodeRange, - EncodeResourceValues, - ExplicitResourceValues, - HeapVariableToRef, - MonomorphizeClass, - SmtlibToProverTypes, -} +import vct.rewrite.{TypeQualifierCoercion, EncodeAutoValue, EncodeRange, EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef, MonomorphizeClass, SmtlibToProverTypes} import vct.rewrite.lang.ReplaceSYCLTypes -import vct.rewrite.veymont.{ - DeduplicateChorGuards, - DropChorExpr, - EncodeChannels, - EncodeChorBranchUnanimity, - EncodeChoreography, - EncodeEndpointInequalities, - StratifyUnpointedExpressions, - GenerateChoreographyPermissions, - GenerateImplementation, - InferEndpointContexts, - SpecializeEndpointClasses, - StratifyExpressions, -} +import vct.rewrite.veymont.{DeduplicateChorGuards, DropChorExpr, EncodeChannels, EncodeChorBranchUnanimity, EncodeChoreography, EncodeEndpointInequalities, GenerateChoreographyPermissions, GenerateImplementation, InferEndpointContexts, SpecializeEndpointClasses, StratifyExpressions, StratifyUnpointedExpressions} import java.nio.file.Path import java.nio.file.Files @@ -298,6 +274,7 @@ case class SilverTransformation( Seq( // Replace leftover SYCL types ReplaceSYCLTypes, + TypeQualifierCoercion, CFloatIntCoercion, ComputeBipGlue, InstantiateBipSynchronizations, @@ -394,6 +371,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/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/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index b1351d8e48..cadae5d5eb 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -417,9 +417,12 @@ valImpureDef valModifier : ('pure' | 'inline' | 'thread_local' | 'bip_annotation') | langStatic # valStatic - | 'unique' '<' langConstInt '>' # valUnique ; +valTypeQualifier + : 'unique' '<' langConstInt '>' # valUnique + ; + valArgList : valArg | valArg ',' valArgList @@ -462,3 +465,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 1f1f16a891..4947110468 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -168,13 +168,10 @@ case class CToCol[G]( else if (m.consume(m.inline)) CInline[G]() else - m.consume(m.unique).map(CUnique[G](_)).getOrElse( - fail( m.nodes.head, "This modifier cannot be attached to a declaration in C", ) - ) }, ) } @@ -293,6 +290,7 @@ case class CToCol[G]( case TypeQualifier1(_) => CRestrict() case TypeQualifier2(_) => CVolatile() case TypeQualifier3(_) => CAtomic() + case TypeQualifier4(spec) => convert(spec) } def convert( @@ -841,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] = @@ -1186,7 +1186,17 @@ case class CToCol[G]( case "thread_local" => collector.threadLocal += mod } case ValStatic(_) => collector.static += mod - case ValUnique(_, _, i, _) => collector.unique += ((mod, convert(i))) + } + + def convert(mod: ValEmbedTypeQualifierContext): CUnique[G] = + mod match { + case ValEmbedTypeQualifier0(_, mod, _) => convert(mod) + case ValEmbedTypeQualifier1(mod) => convert(mod) + } + + def convert(implicit mod: ValTypeQualifierContext): CUnique[G] = + mod match { + case ValUnique(_, _, uniqueId, _) => CUnique[G](convert(uniqueId)) } def convertEmbedWith( diff --git a/src/parsers/vct/parsers/transform/ToCol.scala b/src/parsers/vct/parsers/transform/ToCol.scala index e9a6a45653..e2861443a7 100644 --- a/src/parsers/vct/parsers/transform/ToCol.scala +++ b/src/parsers/vct/parsers/transform/ToCol.scala @@ -130,8 +130,6 @@ abstract class ToCol[G]( val static: mutable.ArrayBuffer[ParserRuleContext] = mutable.ArrayBuffer() val bipAnnotation: mutable.ArrayBuffer[ParserRuleContext] = mutable .ArrayBuffer() - val unique: mutable.ArrayBuffer[(ParserRuleContext, BigInt)] = mutable - .ArrayBuffer() def consume(buffer: mutable.ArrayBuffer[ParserRuleContext]): Boolean = { val result = buffer.nonEmpty @@ -139,13 +137,6 @@ abstract class ToCol[G]( result } - def consume(buffer: mutable.ArrayBuffer[(ParserRuleContext, BigInt)]): Option[BigInt] = { - buffer match { - case mutable.ArrayBuffer() => None - case (_, i) +: _ => buffer.clear(); Some(i) - } - } - def nodes: Seq[ParserRuleContext] = Seq(pure, inline, threadLocal, static, bipAnnotation).flatten } diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index dcb8e47ab8..721c13f814 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[ @@ -399,6 +402,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 +508,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 +537,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 +563,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 +609,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,6 +620,17 @@ 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 diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala index 584f634c15..9c3cc66690 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala @@ -542,6 +542,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..6ce0ed43f0 --- /dev/null +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -0,0 +1,97 @@ +package vct.rewrite + +import vct.col.ast.`type`.typeclass.TFloats +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, RewriterBuilder} +import vct.col.typerules.CoercingRewriter +import vct.result.VerificationError.UserError + +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 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] { + + 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 _ => + } + super.applyCoercion(e, coercion) + } + + 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) + } + + override def postCoerce(t: Type[Pre]): Type[Post] = + t match { + case TConst(t) => dispatch(t) + case TUnique(_, _) => throw DisallowedQualifiedType(t) + case TPointer(it) => makePointer(it) + case other => other.rewriteDefault() + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case npa @ NewPointerArray(t, size, _) => + val (info, newT) = getUnqualified(t) + if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) + else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case other => other.rewriteDefault() + } + } + + override def postCoerce(s: Statement[Pre]): Statement[Post] = + s match { + case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) + case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o) + case other => other.rewriteDefault() + } +} 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/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala index e66592de4b..b819092126 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) @@ -2733,11 +2733,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) @@ -2748,7 +2748,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 d2aa6bfe68..e74599d63e 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -391,17 +391,20 @@ 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 _ => 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 +416,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 +431,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) @@ -482,9 +489,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } val prop = new TypeProperties(cParam.specifiers, cParam) if(!prop.validCParam) throw WrongCType(cParam) - val specType = if(prop.unique.isEmpty) - rw.dispatch(prop.mainType.get) else - TUniquePointer(rw.dispatch(prop.innerType.get), prop.unique.get)(cParam.o) + val specType = rw.dispatch(prop.mainType.get) cParam.drop() val v = @@ -630,7 +635,6 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) t match { case TArray(element) => element case TPointer(element) => element - case TUniquePointer(element, _) => element case _ => throw Unreachable("Already checked on pointer or array type") } @@ -646,12 +650,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)) @@ -659,13 +662,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)) @@ -866,29 +868,21 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) var sizeBlame: Option[Blame[ArraySizeError]] = None var pure = false var inline = false - var unique: Option[BigInt] = None var static = false specs.foreach { case GPULocal() => shared = true case GPUGlobal() => global = true - case CSpecificationType(t@CTPointer(it)) => + case CSpecificationType(t) if isPointer(t) => + val (inner, size, blame) = getInnerPointerInfo(t).get arrayOrPointer = true - innerType = Some(it) + innerType = Some(inner) mainType = Some(t) - case CSpecificationType(t @ CTArray(size, it)) => + sizeBlame = blame arraySize = size - innerType = Some(it) - sizeBlame = Some( - t.blame - ) // we set the blame here, together with the size - arrayOrPointer = true - mainType = Some(t) case CSpecificationType(t) => mainType = Some(t) case CExtern() => extern = true - case CUnique(i) if unique.isDefined => throw WrongCType(decl) - case CUnique(i) => unique = Some(i) case CPure() => pure = true case CInline() => inline = true case CStatic() => static = true @@ -898,8 +892,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def isShared: Boolean = shared && !global def isGlobal: Boolean = !shared && global - def validNonGpu: Boolean = !global && !shared && - (unique.isEmpty || (unique.isDefined && arrayOrPointer)) && mainType.isDefined + def validNonGpu: Boolean = !global && !shared && mainType.isDefined def validReturn: Boolean = validNonGpu && !static def validCParam: Boolean = !pure && !inline && validNonGpu && !static def validCLocal = validCParam @@ -1092,12 +1085,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), + ) }) } @@ -1116,7 +1109,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), @@ -1131,43 +1124,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) } } @@ -1196,27 +1186,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) } @@ -1226,7 +1212,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)) } @@ -1266,16 +1252,39 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(KernelBarrierFailure(barrier)) } - def isPointer(t: Type[Pre]): Boolean = getPointer(t).isDefined - - def getPointer(t: Type[Pre]): Option[Type[Pre]] = + def getInnerPointerInfo(t: Type[Pre]) : Option[(Type[Pre], Option[Expr[Pre]], Option[Blame[ArraySizeError]])] = getBaseType(t) match { - case t @ TPointer(_) => Some(t) - case t @ TUniquePointer(_, _) => Some(t) - case t @ CTPointer(_) => Some(t) + 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 isArray(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t : CTArray[Pre] => true + case _ => false + } + + def isStruct(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t : CTStruct[Pre] => true + case _ => false + } + + def isPointer(t: Type[Pre]): Boolean = + getBaseType(t) match { + case t @ TPointer(_) => true + case t @ CTPointer(_) => true + case _ => false + } + def isNumeric(t: Type[Pre]): Boolean = getBaseType(t) match { case _: NumericType[Pre] => true @@ -1510,8 +1519,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, @@ -1655,7 +1664,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 @@ -1685,12 +1694,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], @@ -1728,7 +1731,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) } @@ -1957,7 +1960,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 _ => () } @@ -1993,8 +1996,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] = { diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 213997930e..5f34c6d49f 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -393,6 +393,7 @@ 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) diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index 6b7f9fe8eb..a6b6c290d0 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -115,12 +115,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) => diff --git a/src/viper/viper/api/backend/SilverBackend.scala b/src/viper/viper/api/backend/SilverBackend.scala index 2e1161e85e..31d757d5dc 100644 --- a/src/viper/viper/api/backend/SilverBackend.scala +++ b/src/viper/viper/api/backend/SilverBackend.scala @@ -285,18 +285,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 @@ -395,6 +387,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..8744be633f --- /dev/null +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -0,0 +1,52 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +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;}""" + vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}""" + + vercors should error withCode "resolutionError:type" 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 "resolutionError:type" 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 "resolutionError:type" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}""" + vercors should error withCode "resolutionError:type" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}""" + vercors should error withCode "resolutionError:type" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}""" + vercors should error withCode "resolutionError:type" 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 consts" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of consts" c """void f(){const int *x; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of consts" c """void f(const int *x){x[0] = 1;}""" + + vercors should 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;}""" +} + +class QualifierSpecWIP extends VercorsSpec { + vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}""" + +} \ No newline at end of file diff --git a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala b/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala deleted file mode 100644 index 8fc4d821d0..0000000000 --- a/test/main/vct/test/integration/examples/UniqueFieldsSpec.scala +++ /dev/null @@ -1,12 +0,0 @@ -package vct.test.integration.examples - -import vct.test.integration.helper.VercorsSpec - -class UniqueFieldsSpec extends VercorsSpec { - vercors should verify using silicon example "concepts/unique/arrays.c" - - vercors should error withCode "wrongCType" in "multiple uniques" c """int main(/*@ unique<1> @*/ /*@ unique<2> @*/ int* x0){}""" - vercors should error withCode "resolutionError:type" in "different uniques local" c """int main(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}""" - vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;}""" - vercors should verify using silicon in "same uniques parameter" c """int main(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){x1 = x0;}""" -} From 58533fa415dfd471161ac756bc16c796d7f0745b Mon Sep 17 00:00:00 2001 From: Lars Date: Tue, 23 Jul 2024 09:26:32 -0400 Subject: [PATCH 05/12] Fixes for tests --- examples/verifythis/2018/challenge2.pvl | 28 +++++++++---------- src/main/vct/main/stages/Transformation.scala | 2 +- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 10 ++++++- 3 files changed, 24 insertions(+), 16 deletions(-) diff --git a/examples/verifythis/2018/challenge2.pvl b/examples/verifythis/2018/challenge2.pvl index 163024b526..4a63c7c867 100644 --- a/examples/verifythis/2018/challenge2.pvl +++ b/examples/verifythis/2018/challenge2.pvl @@ -23,7 +23,7 @@ class ColoredTiles { || (i < n - 2 && s[i+1] && s[i+2]) ); - pure boolean unique(seq> 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/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index e4656e5dac..bd72d58daa 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -304,8 +304,8 @@ case class SilverTransformation( Seq( // Replace leftover SYCL types ReplaceSYCLTypes, - TypeQualifierCoercion, CFloatIntCoercion, + TypeQualifierCoercion, ComputeBipGlue, InstantiateBipSynchronizations, EncodeBipPermissions, diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index e74599d63e..05eeb06872 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -873,7 +873,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) specs.foreach { case GPULocal() => shared = true case GPUGlobal() => global = true - case CSpecificationType(t) if isPointer(t) => + case CSpecificationType(t) if isPointerOrArray(t) => val (inner, size, blame) = getInnerPointerInfo(t).get arrayOrPointer = true innerType = Some(inner) @@ -1285,6 +1285,14 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) 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 From b36382d8af6b312de6894e8be12fd940f97c218b Mon Sep 17 00:00:00 2001 From: Lars Date: Sat, 3 Aug 2024 20:32:09 -0400 Subject: [PATCH 06/12] Create abstract methods when coercing between unique pointers --- src/col/vct/col/ast/Node.scala | 12 +- .../CoerceBetweenUniquePointerImpl.scala | 9 + .../CoerceFromUniquePointerImpl.scala | 9 + .../unsorted/CoerceToUniquePointerImpl.scala | 10 + .../vct/col/ast/unsorted/ToUniqueImpl.scala | 10 - .../vct/col/typerules/CoercingRewriter.scala | 4 + src/col/vct/col/typerules/CoercionUtils.scala | 17 ++ .../vct/rewrite/TypeQualifierCoercion.scala | 179 +++++++++++++++++- .../integration/examples/QualifierSpec.scala | 51 ++++- 9 files changed, 285 insertions(+), 16 deletions(-) create mode 100644 src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala delete mode 100644 src/col/vct/col/ast/unsorted/ToUniqueImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index cfc96b90e5..acdfc9342a 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -954,6 +954,16 @@ 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](inner: Type[G], targetId: BigInt)( + implicit val o: Origin +) extends Coercion[G] with CoerceToUniquePointerImpl[G] +final case class CoerceFromUniquePointer[G](target: Type[G], sourceId: BigInt)( + implicit val o: Origin +) extends Coercion[G] with CoerceFromUniquePointerImpl[G] +final case class CoerceBetweenUniquePointer[G](target: Type[G], sourceId: BigInt, targetId: BigInt)( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G] + final case class CoerceToConst[G](source: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceToConstImpl[G] @@ -1868,8 +1878,6 @@ final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])( )(implicit val o: Origin) extends NewPointer[G] with NewConstPointerArrayImpl[G] -final case class ToUnique[G](inner: Expr[G])(implicit val o: Origin) extends Expr[G] with ToUniqueImpl[G] - final case class FreePointer[G](pointer: Expr[G])( val blame: Blame[PointerFreeError] )(implicit val o: Origin) diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala new file mode 100644 index 0000000000..a21660aa01 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceBetweenUniquePointer +import vct.col.ast.ops.CoerceBetweenUniquePointerOps +import vct.col.print._ + +trait CoerceBetweenUniquePointerImpl[G] extends CoerceBetweenUniquePointerOps[G] { this: CoerceBetweenUniquePointer[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala new file mode 100644 index 0000000000..4c6d12943f --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceFromUniquePointer +import vct.col.ast.ops.CoerceFromUniquePointerOps +import vct.col.print._ + +trait CoerceFromUniquePointerImpl[G] extends CoerceFromUniquePointerOps[G] { this: CoerceFromUniquePointer[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala new file mode 100644 index 0000000000..c7eac83f8d --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.unsorted + +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] => + // override def layout(implicit ctx: Ctx): Doc = ??? + override def target: Type[G] = TUniquePointer(inner, targetId) +} diff --git a/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala b/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala deleted file mode 100644 index b0027cfc17..0000000000 --- a/src/col/vct/col/ast/unsorted/ToUniqueImpl.scala +++ /dev/null @@ -1,10 +0,0 @@ -package vct.col.ast.unsorted - -import vct.col.ast.{TAny, ToUnique} -import vct.col.ast.ops.ToUniqueOps -import vct.col.print._ - -trait ToUniqueImpl[G] extends ToUniqueOps[G] { this: ToUnique[G] => - // Solve typing immediately in TypeQualifiersCoercion pass - def t: vct.col.ast.Type[G] = TAny[G]() -} diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index d90b8a3af8..f2e864e504 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -274,6 +274,10 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceJoinUnion(_, _, _) => e case CoerceSelectUnion(inner, _, _, _) => applyCoercion(e, inner) + case CoerceFromUniquePointer(_, _) => e + case CoerceToUniquePointer(_, _) => e + case CoerceBetweenUniquePointer(_, _, _) => e + case CoerceSupports(_, _) => e case CoerceClassAnyClass(_, _) => e case CoerceJavaSupports(_, _) => e diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index fca0b8b7f0..a41af10930 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -193,6 +193,21 @@ case object CoercionUtils { CTPointer(innerType), ) => // if element == innerType => getAnyCoercion(element, innerType).getOrElse(return None) + case ( + TPointer(innerType), + t@TPointer(TUnique(element, unique)), + ) if element == innerType => + ??? //CoerceToUnique() + case ( + TPointer(TUnique(element, unique)), + t@TPointer(innerType) + ) if element == innerType => + CoerceFromUniquePointer(t, unique) + case ( + TPointer(TUnique(elementS, uniqueS)), + t@TPointer(TUnique(elementT, uniqueT)) + ) if elementS == elementT => + CoerceBetweenUniquePointer(t, uniqueS, uniqueT) case (CTArray(_, innerType), CTPointer(element)) => if (element == innerType) { CoerceCArrayPointer(innerType) } else { @@ -487,6 +502,8 @@ case object CoercionUtils { 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: PointerType[G] => Some((CoerceIdentity(source), t)) case t: CTPointer[G] => Some((CoerceIdentity(source), TPointer(t.innerType))) diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index 6ce0ed43f0..9603afcc36 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -1,11 +1,12 @@ package vct.rewrite -import vct.col.ast.`type`.typeclass.TFloats -import vct.col.ast._ +import vct.col.ast.{Expr, _} import vct.col.origin.Origin import vct.col.rewrite.{Generation, 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" @@ -19,6 +20,12 @@ case class DisallowedQualifiedType(target: Node[_]) extends UserError { target.o.messageInContext("This qualified type is not allowed.") } +case class DisallowedQualifiedCoercion(calledOrigin: Origin) extends UserError { + override def code: String = "disallowedQualifiedCoercion" + override def text: String = + calledOrigin.messageInContext("The coercion of args with qualifiers for this method call is not allowed.") +} + case object TypeQualifierCoercion extends RewriterBuilder { override def key: String = "TypeQualifierCoercion" override def desc: String = @@ -27,6 +34,20 @@ case object TypeQualifierCoercion extends RewriterBuilder { case class TypeQualifierCoercion[Pre <: Generation]() extends CoercingRewriter[Pre] { + val methodCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() + val callee: ScopedStack[Declaration[Pre]] = ScopedStack() + val checkedCallees: mutable.Set[Declaration[Pre]] = mutable.Set() + + val abstractFunction: mutable.Map[(Function[Pre], Map[Type[Pre], Type[Post]]), Function[Post]] = mutable.Map() + val abstractProcedure: mutable.Map[(Procedure[Pre], Map[Type[Pre], Type[Post]]), Procedure[Post]] = mutable.Map() + + def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) + + def uniquePointerType(t: Type[Pre], unique: BigInt) = t match { + case TPointer(TUnique(it, _)) => TPointer(TUnique(it, unique)) + case TPointer(it) => TPointer(TUnique(it, unique)) + case _ => ??? + } override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin @@ -37,6 +58,8 @@ case class TypeQualifierCoercion[Pre <: Generation]() case CoerceToUnique(_, _) => case CoerceFromUnique(_, _) => case CoerceBetweenUnique(_, _, _) => + case CoerceFromUniquePointer(target, sourceId) => ??? + case CoerceBetweenUniquePointer(t, sourceId, targetId) => ??? case _ => } super.applyCoercion(e, coercion) @@ -67,13 +90,121 @@ case class TypeQualifierCoercion[Pre <: Generation]() else TPointer(resType) } - override def postCoerce(t: Type[Pre]): Type[Post] = + override def postCoerce(t: Type[Pre]): Type[Post] = getCopyType(t).getOrElse( t match { case TConst(t) => dispatch(t) case TUnique(_, _) => throw DisallowedQualifiedType(t) case TPointer(it) => makePointer(it) case other => other.rewriteDefault() + }) + + case 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 ApplyCoercion(e, CoerceFromUniquePointer(_, _)) => dispatch(e) + case e => dispatch(e) + }) + + def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] = + xs.zipWithIndex.collect { + case (ApplyCoercion(_, CoerceFromUniquePointer(target, sourceId)), i) => + val source = uniquePointerType(target, sourceId) + (UniqueCoercion(source, 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 DisallowedQualifiedCoercion(calledOrigin)) + } + + def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { + // Check if any non-coerced arguments contain a coerced type + args.zipWithIndex.foreach({ + case (a, i) => + if(!coercedArgs.contains(i) && + ( a.collectFirst { case ApplyCoercion(_, CoerceFromUniquePointer(_, _)) => () }.isDefined || + coercedTypes.contains(a.t) || a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined) + ) { + throw DisallowedQualifiedCoercion(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 DisallowedQualifiedCoercion(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 DisallowedQualifiedCoercion(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. + */ + def getCoercionMapAndCheck(allArgs: Seq[Args], returnType: Type[Pre], calledOrigin: Origin, + body: Option[Node[Pre]], original: Declaration[Pre] + ): Map[Type[Pre], Type[Post]] = { + val coercions: Seq[UniqueCoercion] = allArgs.flatMap(f => f.coercions.view.map(_._1)) + val coercionMap = getCoercionMap(coercions, calledOrigin) // Checks 1 + val coercedTypes = coercionMap.keySet + + allArgs.foreach({ args => + val coercedArgs = args.coercions.map(_._2).toSet + checkArgs(args.originalParams, coercedTypes, coercedArgs, calledOrigin) // Checks 2 + }) + // check return type (also 2) + returnType.collectFirst{ + case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedCoercion(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 createAbstractFunctionCopy(original: Function[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Function[Post] = { + methodCopyTypes.having(typeCoerced) { + globalDeclarations.declare({ + // Subtle, need to create variable scope, otherwise variables are already 'succeeded' in different copies. + variables.scope({ + original.rewrite(body = None) + }) + }) + } + } override def postCoerce(e: Expr[Pre]): Expr[Post] = { implicit val o: Origin = e.o @@ -84,10 +215,52 @@ case class TypeQualifierCoercion[Pre <: Generation]() val (info, newT) = getUnqualified(t) if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) => + val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args)) + if(argsNoCoercions(allArgs)) return inv.rewriteDefault() + if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o) + // Yields and givens are not supported + if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o) + + val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) + // Make sure we only create one copy per coercion mapping + val newFunc: Function[Post] = + abstractFunction.getOrElseUpdate((f.decl, map), createAbstractFunctionCopy(f.decl, map)) + val newArgs = removeCoercions(args) + inv.rewrite(ref = newFunc.ref, args=newArgs) + case inv@ProcedureInvocation(f, args, outArgs, typeArgs, givenMap, yields) => + val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args), + addArgs(f.decl.outArgs, outArgs)) + if(argsNoCoercions(allArgs)) return inv.rewriteDefault() + if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o) + // Yields and givens are not supported + if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o) + + val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) + val newProc: Procedure[Post] = + abstractProcedure.getOrElseUpdate((f.decl, map), createAbstractProcedureCopy(f.decl, map)) + val newArgs = removeCoercions(args) + val newOutArgs = removeCoercions(outArgs) + inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) + // TODO: consider doing exactly the same for any other abstractFunction/abstractMethod case other => other.rewriteDefault() } } + override def postCoerce(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()) + } + + + override def postCoerce(s: Statement[Pre]): Statement[Post] = s match { case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index 8744be633f..7d1f971b77 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -46,7 +46,56 @@ class QualifierSpec extends VercorsSpec { void f(int * const x){x[0] = 1;}""" } +class QualifierSpecWIP2 extends VercorsSpec { + 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){ + 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]; + }""" +} + class QualifierSpecWIP extends VercorsSpec { - vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}""" + 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){ + 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 "???" in "Recursive call wrong uniques" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) == 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, x1, x0); + } +}""" } \ No newline at end of file From db267fc31dda67a671c8dc5474abe021a3c44389 Mon Sep 17 00:00:00 2001 From: Lars Date: Sun, 4 Aug 2024 00:17:35 -0400 Subject: [PATCH 07/12] simpler pointer coercions --- src/col/vct/col/ast/Node.scala | 6 +-- .../CoerceBetweenUniquePointerImpl.scala | 2 +- .../CoerceFromUniquePointerImpl.scala | 2 +- .../unsorted/CoerceToUniquePointerImpl.scala | 3 +- .../vct/col/typerules/CoercingRewriter.scala | 2 +- src/col/vct/col/typerules/CoercionUtils.scala | 50 +++++++++---------- .../vct/rewrite/TypeQualifierCoercion.scala | 46 +++++++++-------- .../integration/examples/QualifierSpec.scala | 48 +++++++----------- 8 files changed, 72 insertions(+), 87 deletions(-) diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index acdfc9342a..b21b441ac4 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -954,13 +954,13 @@ 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](inner: Type[G], targetId: BigInt)( +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](target: Type[G], sourceId: BigInt)( +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](target: Type[G], sourceId: BigInt, targetId: BigInt)( +final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G] diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala index a21660aa01..60a1d0e566 100644 --- a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala @@ -5,5 +5,5 @@ import vct.col.ast.ops.CoerceBetweenUniquePointerOps import vct.col.print._ trait CoerceBetweenUniquePointerImpl[G] extends CoerceBetweenUniquePointerOps[G] { this: CoerceBetweenUniquePointer[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? + } diff --git a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala index 4c6d12943f..1f56025840 100644 --- a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala +++ b/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala @@ -5,5 +5,5 @@ import vct.col.ast.ops.CoerceFromUniquePointerOps import vct.col.print._ trait CoerceFromUniquePointerImpl[G] extends CoerceFromUniquePointerOps[G] { this: CoerceFromUniquePointer[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? + } diff --git a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala b/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala index c7eac83f8d..d354a2beb9 100644 --- a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala +++ b/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala @@ -5,6 +5,5 @@ import vct.col.ast.ops.CoerceToUniquePointerOps import vct.col.print._ trait CoerceToUniquePointerImpl[G] extends CoerceToUniquePointerOps[G] { this: CoerceToUniquePointer[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? - override def target: Type[G] = TUniquePointer(inner, targetId) + } diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index f2e864e504..fa894acf53 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -276,7 +276,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceFromUniquePointer(_, _) => e case CoerceToUniquePointer(_, _) => e - case CoerceBetweenUniquePointer(_, _, _) => e + case CoerceBetweenUniquePointer(_, _) => e case CoerceSupports(_, _) => e case CoerceClassAnyClass(_, _) => e diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index a41af10930..50053d222d 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -13,6 +13,19 @@ case object CoercionUtils { def getCoercion[G](source: Type[G], target: Type[G]): Option[Coercion[G]] = getAnyCoercion(source, target).filter(_.isCPromoting) + def getPointerCoercion[G](source: Type[G], target: Type[G], innerSource: Type[G], innerTarget: Type[G]) : Option[Coercion[G]] = { + Some((innerSource, innerTarget) match { + case (i,l) if i == l => CoerceIdentity(source) + case (TUnique(l, lId), TUnique(r, rId)) => + if(l == r) CoerceBetweenUniquePointer(source, target) else return None + case (TUnique(l, lId), r) => + if(l == r) CoerceFromUniquePointer(source, target) else return None + case (TUnique(l, lId), r) => + if(l == r) CoerceToUniquePointer(source, target) else return None + case _ => return None + }) + } + def getAnyCoercion[G]( source: Type[G], target: Type[G], @@ -183,37 +196,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 ( - TPointer(innerType), - t@TPointer(TUnique(element, unique)), - ) if element == innerType => - ??? //CoerceToUnique() - case ( - TPointer(TUnique(element, unique)), - t@TPointer(innerType) - ) if element == innerType => - CoerceFromUniquePointer(t, unique) - case ( - TPointer(TUnique(elementS, uniqueS)), - t@TPointer(TUnique(elementT, uniqueT)) - ) if elementS == elementT => - CoerceBetweenUniquePointer(t, uniqueS, uniqueT) - 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() diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index 9603afcc36..de91fb7676 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -20,12 +20,18 @@ case class DisallowedQualifiedType(target: Node[_]) extends UserError { target.o.messageInContext("This qualified type is not allowed.") } -case class DisallowedQualifiedCoercion(calledOrigin: Origin) extends UserError { - override def code: String = "disallowedQualifiedCoercion" +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 = @@ -43,12 +49,6 @@ case class TypeQualifierCoercion[Pre <: Generation]() def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) - def uniquePointerType(t: Type[Pre], unique: BigInt) = t match { - case TPointer(TUnique(it, _)) => TPointer(TUnique(it, unique)) - case TPointer(it) => TPointer(TUnique(it, unique)) - case _ => ??? - } - override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin ): Expr[Post] = { @@ -58,8 +58,9 @@ case class TypeQualifierCoercion[Pre <: Generation]() case CoerceToUnique(_, _) => case CoerceFromUnique(_, _) => case CoerceBetweenUnique(_, _, _) => - case CoerceFromUniquePointer(target, sourceId) => ??? - case CoerceBetweenUniquePointer(t, sourceId, targetId) => ??? + case CoerceToUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) + case CoerceFromUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) + case CoerceBetweenUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) case _ => } super.applyCoercion(e, coercion) @@ -114,8 +115,11 @@ case class TypeQualifierCoercion[Pre <: Generation]() def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] = xs.zipWithIndex.collect { - case (ApplyCoercion(_, CoerceFromUniquePointer(target, sourceId)), i) => - val source = uniquePointerType(target, sourceId) + case (ApplyCoercion(_, CoerceFromUniquePointer(source, target)), i) => + (UniqueCoercion(source, target), i) + case (ApplyCoercion(_, CoerceBetweenUniquePointer(source, target)), i) => + (UniqueCoercion(source, target), i) + case (ApplyCoercion(_, CoerceToUniquePointer(source, target)), i) => (UniqueCoercion(source, target), i) } @@ -124,7 +128,7 @@ case class TypeQualifierCoercion[Pre <: Generation]() _.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 DisallowedQualifiedCoercion(calledOrigin)) + (l, r) => if(l == r) l else throw DisallowedQualifiedMethodCoercion(calledOrigin)) } def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { @@ -135,7 +139,7 @@ case class TypeQualifierCoercion[Pre <: Generation]() ( a.collectFirst { case ApplyCoercion(_, CoerceFromUniquePointer(_, _)) => () }.isDefined || coercedTypes.contains(a.t) || a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined) ) { - throw DisallowedQualifiedCoercion(calledOrigin) + throw DisallowedQualifiedMethodCoercion(calledOrigin) } }) } @@ -144,10 +148,10 @@ case class TypeQualifierCoercion[Pre <: Generation]() 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 DisallowedQualifiedCoercion(calledOrigin) + 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 DisallowedQualifiedCoercion(calledOrigin) + if(inv.ref.decl == callee) throw DisallowedQualifiedMethodCoercion(calledOrigin) inv.ref.decl.body.map(checkBody(_, callee, seenMethods.addOne(inv.ref.decl), calledOrigin)) } } @@ -173,7 +177,7 @@ case class TypeQualifierCoercion[Pre <: Generation]() }) // check return type (also 2) returnType.collectFirst{ - case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedCoercion(calledOrigin) } + case t: Type[Pre] if coercedTypes.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 @@ -218,9 +222,9 @@ case class TypeQualifierCoercion[Pre <: Generation]() case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) => val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args)) if(argsNoCoercions(allArgs)) return inv.rewriteDefault() - if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o) + if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o) // Yields and givens are not supported - if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o) + if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) // Make sure we only create one copy per coercion mapping @@ -232,9 +236,9 @@ case class TypeQualifierCoercion[Pre <: Generation]() val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args), addArgs(f.decl.outArgs, outArgs)) if(argsNoCoercions(allArgs)) return inv.rewriteDefault() - if(callee.top == inv.ref.decl) throw DisallowedQualifiedCoercion(inv.o) + if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o) // Yields and givens are not supported - if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedCoercion(inv.o) + if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) val newProc: Procedure[Post] = diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index 7d1f971b77..acfd3ce53a 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -14,19 +14,19 @@ class QualifierSpec extends VercorsSpec { void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = 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 "resolutionError:type" in "malloc different uniques" c + 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 "resolutionError:type" 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 "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 "resolutionError:type" in "different uniques param - 1" c """void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}""" - vercors should error withCode "resolutionError:type" in "different uniques param - 2" c """void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;}""" - vercors should error withCode "resolutionError:type" in "different uniques local" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<2> @*/ int* x1; x1 = x0;}""" - vercors should error withCode "resolutionError:type" in "multiple uniques parameter" c """void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = 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;}""" @@ -44,10 +44,8 @@ class QualifierSpec extends VercorsSpec { 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;}""" -} -class QualifierSpecWIP2 extends VercorsSpec { - vercors should verify using silicon in "Call non-unique function" c """/*@ + 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 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 "???" in "Recursive call wrong uniques" c """/*@ + 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 @*/ int* x0, /*@ unique<2> @*/ int* x1){ if(n == 1){ - return h(x0) + h(x1); + return x0[0] + x1[0]; } else { return f(n-1, x1, x0); } }""" +} + +class QualifierSpecWIP2 extends VercorsSpec { + +} + +class QualifierSpecWIP extends VercorsSpec { + } \ No newline at end of file From a084769ee9248069a21bef40773a65bf129c32e8 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 8 Aug 2024 14:24:19 +0200 Subject: [PATCH 08/12] Coerce return, support methods unique coercion, fix for void --- src/col/vct/col/ast/Node.scala | 4 + .../CoerceBetweenUniquePointerImpl.scala | 2 +- .../CoerceFromUniquePointerImpl.scala | 2 +- .../coercion}/CoerceToUniquePointerImpl.scala | 2 +- .../vct/col/typerules/CoercingRewriter.scala | 23 +- src/col/vct/col/typerules/CoercionUtils.scala | 22 +- src/main/vct/main/stages/Transformation.scala | 2 + .../vct/rewrite/EncodeArrayValues.scala | 15 +- .../vct/rewrite/TypeQualifierCoercion.scala | 231 ++++++++++----- src/rewrite/vct/rewrite/adt/ImportVoid.scala | 5 +- .../integration/examples/QualifierSpec.scala | 274 +++++++++++++++++- .../integration/meta/ExampleCoverage.scala | 1 + 12 files changed, 482 insertions(+), 101 deletions(-) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceBetweenUniquePointerImpl.scala (87%) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceFromUniquePointerImpl.scala (86%) rename src/col/vct/col/ast/{unsorted => family/coercion}/CoerceToUniquePointerImpl.scala (87%) diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index b21b441ac4..19bbbb6cdb 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1878,6 +1878,10 @@ final case class NewConstPointerArray[G](element: Type[G], size: Expr[G])( )(implicit val o: Origin) extends NewPointer[G] with NewConstPointerArrayImpl[G] +final case class UniquePointerCoercion[G](e: Expr[G], t: Type[G])( + implicit val o: Origin +) extends Expr[G] with UniquePointerCoercionImpl[G] + final case class FreePointer[G](pointer: Expr[G])( val blame: Blame[PointerFreeError] )(implicit val o: Origin) diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala similarity index 87% rename from src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala index 60a1d0e566..6c5b0e4631 100644 --- a/src/col/vct/col/ast/unsorted/CoerceBetweenUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceBetweenUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceBetweenUniquePointer import vct.col.ast.ops.CoerceBetweenUniquePointerOps diff --git a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala similarity index 86% rename from src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala index 1f56025840..9f35fd55c0 100644 --- a/src/col/vct/col/ast/unsorted/CoerceFromUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceFromUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.CoerceFromUniquePointer import vct.col.ast.ops.CoerceFromUniquePointerOps diff --git a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala similarity index 87% rename from src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala rename to src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala index d354a2beb9..1ef12bbd9f 100644 --- a/src/col/vct/col/ast/unsorted/CoerceToUniquePointerImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoerceToUniquePointerImpl.scala @@ -1,4 +1,4 @@ -package vct.col.ast.unsorted +package vct.col.ast.family.coercion import vct.col.ast.{CoerceToUniquePointer, TUniquePointer, Type} import vct.col.ast.ops.CoerceToUniquePointerOps diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index fa894acf53..b65b5161b0 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -1,7 +1,7 @@ package vct.col.typerules import com.typesafe.scalalogging.LazyLogging -import hre.util.FuncTools +import hre.util.{FuncTools, ScopedStack} import vct.col.ast._ import vct.col.ast.rewrite.BaseCoercingRewriter import vct.col.ast.`type`.typeclass.TFloats @@ -53,6 +53,7 @@ abstract class CoercingRewriter[Pre <: Generation]() import CoercingRewriter._ type Post = Rewritten[Pre] + val resultType: ScopedStack[Type[Pre]] = ScopedStack() val coercedDeclaration: SuccessionMap[Declaration[Pre], Declaration[Pre]] = SuccessionMap() @@ -375,9 +376,16 @@ abstract class CoercingRewriter[Pre <: Generation]() def postCoerce(decl: Declaration[Pre]): Unit = allScopes.anySucceed(decl, decl.rewriteDefault()) override final def dispatch(decl: Declaration[Pre]): Unit = { - val coercedDecl = coerce(preCoerce(decl)) - coercedDeclaration(decl) = coercedDecl - postCoerce(coercedDecl) + def rewrite() : Unit = { + val coercedDecl = coerce(preCoerce(decl)) + coercedDeclaration(decl) = coercedDecl + postCoerce(coercedDecl) + } + decl match { + case m: AbstractMethod[Pre] => + resultType.having(m.returnType)({rewrite()}) + case _ => rewrite() + } } def coerce(node: Coercion[Pre]): Coercion[Pre] = { @@ -1981,6 +1989,7 @@ abstract class CoercingRewriter[Pre <: Generation]() UMinus(float(arg)), UMinus(rat(arg)), ) + case u: UniquePointerCoercion[Pre] => u case u @ Unfolding(pred, body) => Unfolding(pred, body)(u.blame) case UntypedLiteralBag(values) => val sharedType = Types.leastCommonSuperType(values.map(_.t)) @@ -2251,7 +2260,11 @@ abstract class CoercingRewriter[Pre <: Generation]() case Recv(ref) => Recv(ref) case r @ Refute(assn) => Refute(res(assn))(r.blame) case Return(result) => - Return(result) // TODO coerce return, make AmbiguousReturn? + if(resultType.nonEmpty){ + Return(coerce(result, resultType.top)) // TODO coerce return, make AmbiguousReturn? + } else { + Return(result) + } case Scope(locals, body) => Scope(locals, body) case send @ Send(decl, offset, resource) => Send(decl, offset, res(resource))(send.blame) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 50053d222d..6a63887c4d 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -13,14 +13,28 @@ case object CoercionUtils { def getCoercion[G](source: Type[G], target: Type[G]): Option[Coercion[G]] = getAnyCoercion(source, target).filter(_.isCPromoting) + // We don't want pointers to coerce just between anything, just some things we allow def getPointerCoercion[G](source: Type[G], target: Type[G], innerSource: Type[G], innerTarget: Type[G]) : Option[Coercion[G]] = { Some((innerSource, innerTarget) match { - case (i,l) if i == l => CoerceIdentity(source) - case (TUnique(l, lId), TUnique(r, rId)) => + case (l,r) if l == r => CoerceIdentity(source) + case (TCInt(), TInt()) => CoerceIdentity(source) + case (CPrimitiveType(specs), r) => + specs.collectFirst { case spec: CSpecificationType[G] => spec } match { + case Some(CSpecificationType(t)) => + return getPointerCoercion(source, target, t, r) + case None => return None + } + case (l, CPrimitiveType(specs)) => + specs.collectFirst { case spec: CSpecificationType[G] => spec } match { + case Some(CSpecificationType(t)) => + return getPointerCoercion(source, target, l, t) + case None => return None + } + case (TUnique(l, _), TUnique(r, _)) => if(l == r) CoerceBetweenUniquePointer(source, target) else return None - case (TUnique(l, lId), r) => + case (TUnique(l, _), r) => if(l == r) CoerceFromUniquePointer(source, target) else return None - case (TUnique(l, lId), r) => + case (l, TUnique(r, _)) => if(l == r) CoerceToUniquePointer(source, target) else return None case _ => return None }) diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index bd72d58daa..691825e2c7 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -35,6 +35,7 @@ import vct.rewrite.{ MonomorphizeClass, SmtlibToProverTypes, TypeQualifierCoercion, + MakeUniqueMethodCopies, } import vct.rewrite.lang.ReplaceSYCLTypes import vct.rewrite.veymont._ @@ -306,6 +307,7 @@ case class SilverTransformation( ReplaceSYCLTypes, CFloatIntCoercion, TypeQualifierCoercion, + MakeUniqueMethodCopies, ComputeBipGlue, InstantiateBipSynchronizations, EncodeBipPermissions, diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index 721c13f814..089f8ad471 100644 --- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala +++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala @@ -120,10 +120,14 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { ): (Procedure[Post], FreePointer[Pre] => PointerFreeFailed[Pre]) = { implicit val o: Origin = freeFuncOrigin var errors: Seq[Expr[Pre] => PointerFreeError] = Seq() + val innerT = t match { + case TPointer(it) => it + case TUniquePointer(it, _) => it + } val proc = globalDeclarations.declare({ val (vars, ptr) = variables.collect { - val a_var = new Variable[Post](TPointer(t))(o.where(name = "p")) + val a_var = new Variable[Post](t)(o.where(name = "p")) variables.declare(a_var) Local[Post](a_var.ref) } @@ -179,7 +183,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { IteratedPtrInjective, ) requiresT = - if (!typeIsRef(t)) + if (!typeIsRef(innerT)) requiresT else { // I think this error actually can never happen, since we require full write permission already @@ -192,7 +196,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { // If structure contains structs, the permission for those fields need to be released as well val permFields = t match { - case t: TClass[Post] => unwrapStructPerm(access, t, o, makeStruct) + case innerT: TClass[Post] => unwrapStructPerm(access, innerT, o, makeStruct) case _ => Seq() } requiresT = @@ -213,7 +217,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { body = None, requires = requiresPred, decreases = Some(DecreasesClauseNoRecursion[Post]()), - )(o.where("free_" + t.toString)) + )(o.where("free_" + innerT.toString)) }) (proc, (node: FreePointer[Pre]) => PointerFreeFailed(node, errors)) } @@ -633,8 +637,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { )(PointerArrayCreationFailed(ncpa)) case free @ FreePointer(xs) => val newXs = dispatch(xs) - val TPointer(t) = newXs.t - val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate(t, makeFree(t)) + val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate(newXs.t, makeFree(newXs.t)) ProcedureInvocation[Post](freeFunc.ref, Seq(newXs), Nil, Nil, Nil, Nil)( freeBlame(free) )(free.o) diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index de91fb7676..af97a4dd6a 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -2,10 +2,11 @@ package vct.rewrite import vct.col.ast.{Expr, _} import vct.col.origin.Origin -import vct.col.rewrite.{Generation, RewriterBuilder} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.typerules.CoercingRewriter import vct.result.VerificationError.UserError import hre.util.ScopedStack + import scala.collection.mutable case class DisallowedConstAssignment(target: Node[_]) extends UserError { @@ -39,15 +40,7 @@ case object TypeQualifierCoercion extends RewriterBuilder { } case class TypeQualifierCoercion[Pre <: Generation]() - extends CoercingRewriter[Pre] { - val methodCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() - val callee: ScopedStack[Declaration[Pre]] = ScopedStack() - val checkedCallees: mutable.Set[Declaration[Pre]] = mutable.Set() - - val abstractFunction: mutable.Map[(Function[Pre], Map[Type[Pre], Type[Post]]), Function[Post]] = mutable.Map() - val abstractProcedure: mutable.Map[(Procedure[Pre], Map[Type[Pre], Type[Post]]), Procedure[Post]] = mutable.Map() - - def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) + extends CoercingRewriter[Pre] { override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin @@ -58,14 +51,42 @@ case class TypeQualifierCoercion[Pre <: Generation]() case CoerceToUnique(_, _) => case CoerceFromUnique(_, _) => case CoerceBetweenUnique(_, _, _) => - case CoerceToUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) - case CoerceFromUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) - case CoerceBetweenUniquePointer(s, t) => throw DisallowedQualifiedCoercion(e.o, s, t) + case CoerceToUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) + case CoerceFromUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) + case CoerceBetweenUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) case _ => } - super.applyCoercion(e, coercion) + e } + override def postCoerce(t: Type[Pre]): Type[Post] = + t match { + case TConst(t) => dispatch(t) + case TUnique(_, _) => throw DisallowedQualifiedType(t) + case TPointer(it) => makePointer(it) + case other => other.rewriteDefault() + } + + override def postCoerce(e: Expr[Pre]): Expr[Post] = { + implicit val o: Origin = e.o + e match { + case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) + case npa @ NewPointerArray(t, size, _) => + val (info, newT) = getUnqualified(t) + if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) + else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case other => other.rewriteDefault() + } + } + + override def postCoerce(s: Statement[Pre]): Statement[Post] = + s match { + case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) + case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o) + case other => other.rewriteDefault() + } + case class InnerInfo(){ var unique: Option[BigInt] = None var const: Boolean = false @@ -90,14 +111,25 @@ case class TypeQualifierCoercion[Pre <: Generation]() else if (info.unique.isDefined) TUniquePointer(resType, info.unique.get) else TPointer(resType) } +} - override def postCoerce(t: Type[Pre]): Type[Post] = getCopyType(t).getOrElse( - t match { - case TConst(t) => dispatch(t) - case TUnique(_, _) => throw DisallowedQualifiedType(t) - case TPointer(it) => makePointer(it) - case other => other.rewriteDefault() - }) +case object MakeUniqueMethodCopies extends RewriterBuilder { + override def key: String = "MakeUniqueMethodCopies" + override def desc: String = + "Makes copies of called function that are specialized for unique pointers." +} + +case class MakeUniqueMethodCopies[Pre <: Generation]() + extends Rewriter[Pre] { + val methodCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() + val callee: ScopedStack[Declaration[Pre]] = ScopedStack() + val checkedCallees: mutable.Set[Declaration[Pre]] = mutable.Set() + + val abstractFunction: mutable.Map[(Function[Pre], Map[Type[Pre], Type[Post]]), Function[Post]] = mutable.Map() + val abstractProcedure: mutable.Map[(Procedure[Pre], Map[Type[Pre], Type[Post]]), Procedure[Post]] = mutable.Map() + def getCopyType(t: Type[Pre]): Option[Type[Post]] = methodCopyTypes.topOption.flatMap(m => m.get(t)) + + override def dispatch(t: Type[Pre]): Type[Post] = getCopyType(t).getOrElse(t.rewriteDefault()) case class UniqueCoercion(givenArgT: Type[Pre], originalParamT: Type[Pre]) case class Args(originalParams: Seq[Variable[Pre]], coercions: Seq[(UniqueCoercion, BigInt)]) @@ -109,18 +141,13 @@ case class TypeQualifierCoercion[Pre <: Generation]() def argsNoCoercions(args: Seq[Args]) : Boolean = args.forall(_.coercions.isEmpty) def removeCoercions(args: Seq[Expr[Pre]]): Seq[Expr[Post]] = args.map({ - case ApplyCoercion(e, CoerceFromUniquePointer(_, _)) => dispatch(e) + case UniquePointerCoercion(e, t) => dispatch(e) case e => dispatch(e) }) def containsUniqueCoerce(xs: Seq[Expr[Pre]]) : Seq[(UniqueCoercion, BigInt)] = xs.zipWithIndex.collect { - case (ApplyCoercion(_, CoerceFromUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) - case (ApplyCoercion(_, CoerceBetweenUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) - case (ApplyCoercion(_, CoerceToUniquePointer(source, target)), i) => - (UniqueCoercion(source, target), i) + case (UniquePointerCoercion(e, target), i) => (UniqueCoercion(e.t, target), i) } def getCoercionMap(coercions: Seq[UniqueCoercion], calledOrigin: Origin): Map[Type[Pre], Type[Post]] = { @@ -131,20 +158,26 @@ case class TypeQualifierCoercion[Pre <: Generation]() (l, r) => if(l == r) l else throw DisallowedQualifiedMethodCoercion(calledOrigin)) } - def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { + def checkArgs(args: Seq[Variable[Pre]], coercedTypes: Set[Type[Pre]], coercedResults: Set[Type[Post]], + coercedArgs: Set[BigInt], calledOrigin: Origin): Unit = { // Check if any non-coerced arguments contain a coerced type args.zipWithIndex.foreach({ case (a, i) => - if(!coercedArgs.contains(i) && - ( a.collectFirst { case ApplyCoercion(_, CoerceFromUniquePointer(_, _)) => () }.isDefined || - coercedTypes.contains(a.t) || a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined) - ) { - throw DisallowedQualifiedMethodCoercion(calledOrigin) + // Look at non-coerced args + if(!coercedArgs.contains(i)) { + // An argument cannot contain coercions themselves + if(a.collectFirst { case _: UniquePointerCoercion[Pre] => () }.isDefined || + // The (sub)type cannot be coerced in another argument + a.t.collectFirst { case t: Type[Pre] if coercedTypes.contains(t) => () }.isDefined || + // The (sub)type cannot be the same as a resulting coercion + dispatch(a.t).collectFirst { case t: Type[Post] if coercedResults.contains(t) => () }.isDefined + ){ + throw DisallowedQualifiedMethodCoercion(calledOrigin) + } } }) } - // def checkBody(body: Node[Pre], callee: Declaration[Pre], seenMethods: mutable.Set[Declaration[Pre]], calledOrigin: Origin): Unit = { body.collect { case inv: AnyMethodInvocation[Pre] if !seenMethods.contains(inv.ref.decl) => @@ -163,21 +196,40 @@ case class TypeQualifierCoercion[Pre <: Generation]() * This rules out coercing pointer of pointers, but I see no easy around this at the time 3. If the call is recursive, we do not allow this. * Also if there is a recursive call, further down the call tree, it is not allowed. + 4. The output types need to be unique + 5. We cannot coerce towards a type, for which this type was already present and not coerced */ - def getCoercionMapAndCheck(allArgs: Seq[Args], returnType: Type[Pre], calledOrigin: Origin, + def getCoercionMapAndCheck(allArgs: Seq[Args], returnType: Type[Pre], returnCoercion: Option[UniqueCoercion], + anyReturnCoercion: Boolean, + calledOrigin: Origin, body: Option[Node[Pre]], original: Declaration[Pre] ): Map[Type[Pre], Type[Post]] = { - val coercions: Seq[UniqueCoercion] = allArgs.flatMap(f => f.coercions.view.map(_._1)) + val coercions: Seq[UniqueCoercion] = allArgs.flatMap(f => f.coercions.view.map(_._1)) :++ returnCoercion val coercionMap = getCoercionMap(coercions, calledOrigin) // Checks 1 val coercedTypes = coercionMap.keySet + val coercedResults = coercionMap.values.toSet + // Checks 4 + if(coercedResults.size != coercedTypes.size){ + throw DisallowedQualifiedMethodCoercion(calledOrigin) + } allArgs.foreach({ args => val coercedArgs = args.coercions.map(_._2).toSet - checkArgs(args.originalParams, coercedTypes, coercedArgs, calledOrigin) // Checks 2 + checkArgs(args.originalParams, coercedTypes, coercedResults, coercedArgs, calledOrigin) // Checks 2 }) - // check return type (also 2) - returnType.collectFirst{ - case t: Type[Pre] if coercedTypes.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) } + // check return type if it not coerced (also 2) + // But not 1: if we have an explicit coercion (which is checked) + if(returnCoercion.isEmpty) { + // anyReturnCoercion means we are fine with a coerced return type. But no coerced subtype can be present though + val checkedSet = if(anyReturnCoercion) coercedTypes - returnType else coercedTypes + returnType.collectFirst { + case t: Type[Pre] if checkedSet.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) + } + // If the returnType is not coerced, it cannot be contained in any coerced Results + dispatch(returnType).collectFirst { + case t: Type[Post] if coercedResults.contains(t) => throw DisallowedQualifiedMethodCoercion(calledOrigin) + } + } if(!checkedCallees.contains(original)) { // If the body of this functions calls the callee, we end up with recursion we do not want body.foreach(b => checkBody(b, callee.top, mutable.Set(original), calledOrigin)) // Checks 3 @@ -210,15 +262,48 @@ case class TypeQualifierCoercion[Pre <: Generation]() } } - override def postCoerce(e: Expr[Pre]): Expr[Post] = { + def rewriteProcedureInvocation(inv: ProcedureInvocation[Pre], returnCoercion: Option[UniqueCoercion], anyReturnPointer: Boolean = false): ProcedureInvocation[Post] = { + val f = inv.ref.decl + val allArgs: Seq[Args] = Seq(addArgs(f.args, inv.args), + addArgs(f.outArgs, inv.outArgs)) + if(argsNoCoercions(allArgs) && returnCoercion.isEmpty) return inv.rewriteDefault() + if(callee.top == f) throw DisallowedQualifiedMethodCoercion(inv.o) + // Yields and givens are not supported for now (is possible) + if(inv.givenMap.nonEmpty || inv.yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) + + val map = getCoercionMapAndCheck(allArgs, f.returnType, returnCoercion, anyReturnPointer, inv.o, f.body, f) + val newProc: Procedure[Post] = + abstractProcedure.getOrElseUpdate((f, map), createAbstractProcedureCopy(f, map)) + val newArgs = removeCoercions(inv.args) + val newOutArgs = removeCoercions(inv.outArgs) + inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) + } + + // For AmbiguousSubscript / DerefPointer we do not care about how the return type is coerced + // so if we encounter invocations we communicate that. + def rewriteAnyPointerReturn(e: Expr[Pre]): Expr[Post] = e match { + case inv: ProcedureInvocation[Pre] => + rewriteProcedureInvocation(inv, None, anyReturnPointer=true) +// case inv: FunctionInvocation[Pre] => +// rewriteFunctionInvocation(inv, None, anyReturnPointer=true) + case e => dispatch(e) + } + + // If the coerce contains an invocation, maybe it is valid, otherwise not + def rewriteCoerce(e: Expr[Pre], target: Type[Pre]): Expr[Post] = e match { + case inv: ProcedureInvocation[Pre] => + val returnCoercion = Some(UniqueCoercion(target, inv.t)) + rewriteProcedureInvocation(inv, returnCoercion) +// case inv: FunctionInvocation[Pre] => + // rewriteFunctionInvocation(inv, None, anyReturnPointer=true) + case am@AmbiguousMinus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target)) + case am@AmbiguousPlus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target)) + case e => throw DisallowedQualifiedCoercion(e.o, e.t, target) + } + + override def dispatch(e: Expr[Pre]): Expr[Post] = { implicit val o: Origin = e.o e match { - case PreAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) - case PostAssignExpression(target, _) if target.t.isInstanceOf[TConst[Pre]] => throw DisallowedConstAssignment(target) - case npa @ NewPointerArray(t, size, _) => - val (info, newT) = getUnqualified(t) - if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) - else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) => val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args)) if(argsNoCoercions(allArgs)) return inv.rewriteDefault() @@ -226,32 +311,41 @@ case class TypeQualifierCoercion[Pre <: Generation]() // Yields and givens are not supported if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) - val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) + val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, ???, ???, inv.o, f.decl.body, f.decl) // Make sure we only create one copy per coercion mapping val newFunc: Function[Post] = abstractFunction.getOrElseUpdate((f.decl, map), createAbstractFunctionCopy(f.decl, map)) val newArgs = removeCoercions(args) inv.rewrite(ref = newFunc.ref, args=newArgs) - case inv@ProcedureInvocation(f, args, outArgs, typeArgs, givenMap, yields) => - val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args), - addArgs(f.decl.outArgs, outArgs)) - if(argsNoCoercions(allArgs)) return inv.rewriteDefault() - if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o) - // Yields and givens are not supported - if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) - - val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, inv.o, f.decl.body, f.decl) - val newProc: Procedure[Post] = - abstractProcedure.getOrElseUpdate((f.decl, map), createAbstractProcedureCopy(f.decl, map)) - val newArgs = removeCoercions(args) - val newOutArgs = removeCoercions(outArgs) - inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) + case inv: ProcedureInvocation[Pre] => + rewriteProcedureInvocation(inv, None) + // So this is awkward, but... + // A lot of times we just coerced to 'pointer', as with subscripting. In this case we don't care if the return gets + // coerced. + case e@AmbiguousSubscript(p, _) => e.rewrite(collection=rewriteAnyPointerReturn(p)) + case e@DerefPointer(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@FreePointer(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerBlockLength(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerLength(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@PointerBlockOffset(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + case e@SharedMemSize(p) => e.rewrite(pointer=rewriteAnyPointerReturn(p)) + // We store the coercion for the return type + case u: UniquePointerCoercion[Pre] => rewriteCoerce(u.e, u.t) // TODO: consider doing exactly the same for any other abstractFunction/abstractMethod case other => other.rewriteDefault() } } - override def postCoerce(d: Declaration[Pre]): Unit = d match { + override def dispatch(s: Statement[Pre]): Statement[Post] = { + implicit val o: Origin = s.o + s match { + case ev@Eval(e) => + ev.rewrite(rewriteAnyPointerReturn(e)) + case other => other.rewriteDefault() + } + } + + override def dispatch(d: Declaration[Pre]): Unit = d match { case f: AbstractFunction[Pre] => callee.having(f){ checkedCallees.clear() allScopes.anySucceed(f, f.rewriteDefault()) @@ -262,13 +356,4 @@ case class TypeQualifierCoercion[Pre <: Generation]() } case other => allScopes.anySucceed(other, other.rewriteDefault()) } - - - - override def postCoerce(s: Statement[Pre]): Statement[Post] = - s match { - case Assign(target, _) if getUnqualified(target.t)._1.const => throw DisallowedConstAssignment(target) - case a@AssignInitial(target, value) => Assign(dispatch(target), dispatch(value))(a.blame)(a.o) - case other => other.rewriteDefault() - } } diff --git a/src/rewrite/vct/rewrite/adt/ImportVoid.scala b/src/rewrite/vct/rewrite/adt/ImportVoid.scala index 414bdfed90..66b3b496d3 100644 --- a/src/rewrite/vct/rewrite/adt/ImportVoid.scala +++ b/src/rewrite/vct/rewrite/adt/ImportVoid.scala @@ -38,7 +38,10 @@ case class ImportVoid[Pre <: Generation](importer: ImportADTImporter) override def postCoerce(stat: Statement[Pre]): Statement[Post] = stat match { - case ret @ Return(v @ Void()) => ret.rewrite(result = Void()(v.o)) + case ret @ Return(v @ Void()) => + ret.rewrite(result = Void()(v.o)) + case ret @ Return(ApplyCoercion(v @ Void(), CoerceIdentity(_))) => + ret.rewrite(result = Void()(v.o)) case other => rewriteDefault(other) } } diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index acfd3ce53a..e6ac89de1b 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -11,7 +11,7 @@ class QualifierSpec extends VercorsSpec { vercors should verify using silicon in "same uniques local with inits" c """void f(){/*@ unique<1> @*/ int x0[2] = {1,2}; /*@ unique<1> @*/ int* x1; x1 = x0;}""" vercors should verify using silicon in "malloc uniques" c """#include - void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0;}""" + void f(){/*@ unique<1> @*/ int* x0 = (/*@ unique<1> @*/ int*) malloc(sizeof(int)*2); /*@ unique<1> @*/ int* x1; x1 = x0; free(x0);}""" vercors should verify using silicon in "uniques pointer of unique pointer" c """void f(){/*@ unique<1> @*/ int * /*@ unique<2> @*/ * x0;}""" vercors should error withCode "disallowedQualifiedCoercion" in "malloc different uniques" c @@ -33,9 +33,9 @@ class QualifierSpec extends VercorsSpec { vercors should error withCode "disallowedConstAssignment" in "Assign to param const" c """void f(const int x){x = 0;}""" vercors should verify using silicon in "Assign to init const array" c """void f(){const int x[2] = {0, 2}; /*@ assert x[1] == 2; @*/}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to local array of consts" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of consts" c """void f(){const int *x; x[0] = 1;}""" - vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of consts" c """void f(const int *x){x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local array of const" c """void f(){const int x[2] = {0, 2}; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to local pointer of const" c """void f(){const int *x; x[0] = 1;}""" + vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of const" c """void f(const int *x){x[0] = 1;}""" vercors should verify using silicon in "Assign const array to const pointer" c """void f(const int* y){const int x[2] = {0, 2}; y = x;}""" vercors should error withCode "resolutionError:type" in "Assign const array to non-const pointer" c """void f(int* y){const int x[2] = {0, 2}; x = y;}""" @@ -65,8 +65,8 @@ class QualifierSpec extends VercorsSpec { vercors should error withCode "disallowedQualifiedMethodCoercion" in "Recursive procedure call wrong uniques" c """/*@ context n > 0; - context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ if(n == 1){ @@ -76,12 +76,268 @@ int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){ return f(n-1, x1, x0); } }""" + + vercors should verify using silicon in "Recursive procedure call with uniques" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return x0[0] + x1[0]; + } + else { + return f(n-1, x0, x1); + } +}""" + + vercors should verify using silicon in "Recursive procedure call with uniques and coercion" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return f(n-1, x0, x1); + } } -class QualifierSpecWIP2 extends VercorsSpec { +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} +""" + vercors should verify using silicon in "Call procedure with multiple consistent coercions" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + return h(x0, x0) + h(x1, x1); } -class QualifierSpecWIP extends VercorsSpec { - +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4); + ensures \result == x[0] + y[0]; +@*/ +int h(int* x, int* y){ + return x[0] + y[0]; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Call procedure with multiple inconsistent coercions" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + return h(x0, x1); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4); + ensures \result == x[0] + y[0]; +@*/ +int h(int* x, int* y){ + return x[0] + y[0]; +}""" + + vercors should error withCode "resolutionError:type" in "Cannot coerce pointers of pointers" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0){ + /*@ unique<1> @*/ int y[1] = {1}; + /*@ unique<1> @*/ int* yy[1] = {y}; + return h(x0, yy); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context yy != NULL ** \pointer_length(yy) > 0 ** Perm(&yy[0], 1\4); + context yy[0] != NULL ** \pointer_length(yy[0]) > 0 ** Perm(&yy[0][0], 1\4); + ensures \result == x[0] + yy[0][0]; +@*/ +int h(int* x, int** yy){ + return x[0] + yy[0][0]; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Disallow coercion of types which are subtypes of other types" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0){ + int y[1] = {1}; + int* yy[1] = {y}; + return h(x0, yy); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + context yy != NULL ** \pointer_length(yy) > 0 ** Perm(&yy[0], 1\4); + context yy[0] != NULL ** \pointer_length(yy[0]) > 0 ** Perm(&yy[0][0], 1\4); + ensures \result == x[0] + yy[0][0]; +@*/ +int h(int* x, int** yy){ + return x[0] + yy[0][0]; +}""" + + vercors should verify using silicon in "Indirect recursive procedure call with uniques and coercion" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return g(n-1, x0, x1); + } +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} + +/*@ + context n > 0; + context x != NULL ** \pointer_length(x) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x, /*@ unique<2> @*/ int* y){ + return f(n, x, y); +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Indirect recursive procedure call with uniques and coercion" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + if(n == 1){ + return h(x0) + h(x1); + } + else { + return g(n-1, x1, x0); + } +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; +@*/ +int h(int* x){ + return x[0]; +} + +/*@ + context n > 0; + context x != NULL ** \pointer_length(x) >= n ** (\forall* int i; 0<=i && i= n ** (\forall* int i; 0<=i && i @*/ int* x, /*@ unique<2> @*/ int* y){ + return f(n, x, y); +}""" + + vercors should verify using silicon in "Call procedure which already has unique type" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, int* x1){ + return h(x0) + h(x1); +} + +/*@ + context x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + ensures \result == x[0]; +@*/ +int h(/*@ unique<2> @*/ int* x){ + return x[0]; +}""" + + vercors should verify using silicon in "Call procedure which returns pointer" c """/*@ +context n > 0; +context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, int* x1){ + int y = h(x0)[0]; + /*@ unique<1> @*/ int* yy = h(x0); + return h(x0)[0] + h(x1)[0]; +} + +/*@ + ensures \result == \old(x); +@*/ +int* h(int* x){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Call procedure with unsupported return type" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0){ + /*@ unique<2> @*/ int* yy = h(x0); +} + +/*@ + ensures \result == \old(x); +@*/ +int* h(int* x){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedCoercion" in "Returns non-unique when should" c """ +int* h(int /*@ unique<1> @*/ * x, int /*@ unique<2> @*/ * y){ + return x; +} +""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Arguments are same but should be unique" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0, int* x1){ + h(x0, x0); +} + +/*@ unique<1> @*/ int* h(int /*@ unique<1> @*/ * x, int /*@ unique<2> @*/ * y){ + return x; +}""" + + vercors should error withCode "disallowedQualifiedMethodCoercion" in "Return type cannot be same as coerced argument type" c """/*@ +context n > 1; +context x0 != NULL ** \pointer_length(x0) == n; +@*/ +int f(int n, /*@ unique<1> @*/ int* x0, int* x1){ + h(x0); +} + +/*@ unique<1> @*/ int* h(int /*@ unique<2> @*/ * y){ + return NULL; +}""" } \ No newline at end of file diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala index e5918fb39d..82cf5b39ed 100644 --- a/test/main/vct/test/integration/meta/ExampleCoverage.scala +++ b/test/main/vct/test/integration/meta/ExampleCoverage.scala @@ -36,6 +36,7 @@ class ExampleCoverage extends AnyFlatSpec { new PointerSpec(), new PredicatesSpec(), new PublicationsSpec(), + new QualifierSpec(), new RefuteSpec(), new SequencesSpec(), new SetsSpec(), From 2d925c68723d8765a40d3a7240d321996806d147 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 8 Aug 2024 15:25:03 +0200 Subject: [PATCH 09/12] Fix free function defect --- src/rewrite/vct/rewrite/EncodeArrayValues.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rewrite/vct/rewrite/EncodeArrayValues.scala b/src/rewrite/vct/rewrite/EncodeArrayValues.scala index 089f8ad471..ec058d9cda 100644 --- a/src/rewrite/vct/rewrite/EncodeArrayValues.scala +++ b/src/rewrite/vct/rewrite/EncodeArrayValues.scala @@ -195,7 +195,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] { } // If structure contains structs, the permission for those fields need to be released as well val permFields = - t match { + innerT match { case innerT: TClass[Post] => unwrapStructPerm(access, innerT, o, makeStruct) case _ => Seq() } From 529f4b4609f0f84007e9ae5fe40e4281bdc4aad8 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 8 Aug 2024 17:15:05 +0200 Subject: [PATCH 10/12] Support for qualified functions --- .../expr/misc/UniquePointerCoercionImpl.scala | 9 +++ src/parsers/antlr4/CParser.g4 | 4 +- .../vct/parsers/transform/CToCol.scala | 6 +- .../vct/rewrite/TypeQualifierCoercion.scala | 62 +++++++++++++------ .../integration/examples/QualifierSpec.scala | 46 ++++++++++++++ 5 files changed, 104 insertions(+), 23 deletions(-) create mode 100644 src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala diff --git a/src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala b/src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala new file mode 100644 index 0000000000..edaef3834a --- /dev/null +++ b/src/col/vct/col/ast/expr/misc/UniquePointerCoercionImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.expr.misc + +import vct.col.ast.UniquePointerCoercion +import vct.col.ast.ops.UniquePointerCoercionOps +import vct.col.print._ + +trait UniquePointerCoercionImpl[G] extends UniquePointerCoercionOps[G] { this: UniquePointerCoercion[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/parsers/antlr4/CParser.g4 b/src/parsers/antlr4/CParser.g4 index ad2e6b3e60..6a59d3f4b9 100644 --- a/src/parsers/antlr4/CParser.g4 +++ b/src/parsers/antlr4/CParser.g4 @@ -20,4 +20,6 @@ specFalse: 'false'; startSpec: LineStartSpec {specLevel++;} | BlockStartSpec {specLevel++;} | BlockStartSpecImmediate {specLevel++;}; endSpec: EndSpec {specLevel--;}; -typeSpecifierWithPointerOrArray : typeSpecifier | typeSpecifier '[' ']' | typeSpecifier '*'; \ No newline at end of file +typeSpecifierWithPointerOrArray : specifierQualifierList + | specifierQualifierList '[' ']' + | specifierQualifierList '*'; \ No newline at end of file diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index d9969964c0..ca5a375b16 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -1005,11 +1005,11 @@ case class CToCol[G]( def convert(t: TypeSpecifierWithPointerOrArrayContext): Type[G] = t match { case TypeSpecifierWithPointerOrArray0(typeSpec) => - CPrimitiveType(Seq(convert(typeSpec))) + CPrimitiveType(convert(typeSpec)) case TypeSpecifierWithPointerOrArray1(typeSpec, _, _) => - CTArray(None, CPrimitiveType(Seq(convert(typeSpec))))(blame(t)) + CTArray(None, CPrimitiveType(convert(typeSpec)))(blame(t)) case TypeSpecifierWithPointerOrArray2(typeSpec, _) => - CTPointer(CPrimitiveType(Seq(convert(typeSpec)))) + CTPointer(CPrimitiveType(convert(typeSpec))) } def convert(id: LangIdContext): String = diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index af97a4dd6a..e0a04cea23 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -251,12 +251,13 @@ case class MakeUniqueMethodCopies[Pre <: Generation]() } // Same for functions - def createAbstractFunctionCopy(original: Function[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Function[Post] = { + def createFunctionCopy(original: Function[Pre], typeCoerced: Map[Type[Pre], Type[Post]]): Function[Post] = { methodCopyTypes.having(typeCoerced) { globalDeclarations.declare({ // Subtle, need to create variable scope, otherwise variables are already 'succeeded' in different copies. variables.scope({ - original.rewrite(body = None) + // We do copy body, otherwise functions could be different. + original.rewrite() }) }) } @@ -279,13 +280,46 @@ case class MakeUniqueMethodCopies[Pre <: Generation]() inv.rewrite(ref = newProc.ref, args=newArgs, outArgs=newOutArgs) } + def rewriteFunctionInvocation(inv: FunctionInvocation[Pre], returnCoercion: Option[UniqueCoercion], anyReturnPointer: Boolean = false): FunctionInvocation[Post] = { + val f = inv.ref.decl + val allArgs: Seq[Args] = Seq(addArgs(f.args, inv.args)) + if(argsNoCoercions(allArgs) && returnCoercion.isEmpty){ + if(methodCopyTypes.nonEmpty){ + val map = methodCopyTypes.top + // So we are already coercing. Let's see if we need to change anything. + if(f.args.exists(v => map.contains(v.t)) || map.contains(f.returnType) ) { + // So yes, we just use the same map we were already using + val newFunc: Function[Post] = + abstractFunction.getOrElseUpdate((f, map), createFunctionCopy(f, map)) + val newArgs = removeCoercions(inv.args) + return inv.rewrite(ref = newFunc.ref, args=newArgs) + } + } + + return inv.rewriteDefault() + } + // Coercing a function call, whilst we are already coercing seems quite complicated. + // So let's not do that for now. + if(methodCopyTypes.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) + + if(callee.top == f) throw DisallowedQualifiedMethodCoercion(inv.o) + // Yields and givens are not supported for now (is possible) + if(inv.givenMap.nonEmpty || inv.yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) + + val map = getCoercionMapAndCheck(allArgs, f.returnType, returnCoercion, anyReturnPointer, inv.o, f.body, f) + val newFunc: Function[Post] = + abstractFunction.getOrElseUpdate((f, map), createFunctionCopy(f, map)) + val newArgs = removeCoercions(inv.args) + inv.rewrite(ref = newFunc.ref, args=newArgs) + } + // For AmbiguousSubscript / DerefPointer we do not care about how the return type is coerced // so if we encounter invocations we communicate that. def rewriteAnyPointerReturn(e: Expr[Pre]): Expr[Post] = e match { case inv: ProcedureInvocation[Pre] => rewriteProcedureInvocation(inv, None, anyReturnPointer=true) -// case inv: FunctionInvocation[Pre] => -// rewriteFunctionInvocation(inv, None, anyReturnPointer=true) + case inv: FunctionInvocation[Pre] => + rewriteFunctionInvocation(inv, None, anyReturnPointer=true) case e => dispatch(e) } @@ -294,8 +328,9 @@ case class MakeUniqueMethodCopies[Pre <: Generation]() case inv: ProcedureInvocation[Pre] => val returnCoercion = Some(UniqueCoercion(target, inv.t)) rewriteProcedureInvocation(inv, returnCoercion) -// case inv: FunctionInvocation[Pre] => - // rewriteFunctionInvocation(inv, None, anyReturnPointer=true) + case inv: FunctionInvocation[Pre] => + val returnCoercion = Some(UniqueCoercion(target, inv.t)) + rewriteFunctionInvocation(inv, returnCoercion) case am@AmbiguousMinus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target)) case am@AmbiguousPlus(pointer, _) => am.rewrite(left=rewriteCoerce(pointer, target)) case e => throw DisallowedQualifiedCoercion(e.o, e.t, target) @@ -304,19 +339,8 @@ case class MakeUniqueMethodCopies[Pre <: Generation]() override def dispatch(e: Expr[Pre]): Expr[Post] = { implicit val o: Origin = e.o e match { - case inv@FunctionInvocation(f, args, typeArgs, givenMap, yields) => - val allArgs: Seq[Args] = Seq(addArgs(f.decl.args, args)) - if(argsNoCoercions(allArgs)) return inv.rewriteDefault() - if(callee.top == inv.ref.decl) throw DisallowedQualifiedMethodCoercion(inv.o) - // Yields and givens are not supported - if(givenMap.nonEmpty || yields.nonEmpty) throw DisallowedQualifiedMethodCoercion(inv.o) - - val map = getCoercionMapAndCheck(allArgs, f.decl.returnType, ???, ???, inv.o, f.decl.body, f.decl) - // Make sure we only create one copy per coercion mapping - val newFunc: Function[Post] = - abstractFunction.getOrElseUpdate((f.decl, map), createAbstractFunctionCopy(f.decl, map)) - val newArgs = removeCoercions(args) - inv.rewrite(ref = newFunc.ref, args=newArgs) + case inv: FunctionInvocation[Pre] => + rewriteFunctionInvocation(inv, None) case inv: ProcedureInvocation[Pre] => rewriteProcedureInvocation(inv, None) // So this is awkward, but... diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index e6ac89de1b..ceec1aaf0a 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -340,4 +340,50 @@ int f(int n, /*@ unique<1> @*/ int* x0, int* x1){ /*@ unique<1> @*/ int* h(int /*@ unique<2> @*/ * y){ return NULL; }""" + + vercors should verify using silicon in "Call function in contract, which needs coercion" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + //@ assert h(x0, x1) == x0[0] + x1[0]; + //@ assert g(x0, x1) == x0[0] + x1[0]; + return 0; + } + + /*@ + context x0 != NULL ** \pointer_length(x0) > 0 ** Perm(&x0[0], 1\4); + context x1 != NULL ** \pointer_length(x1) > 0 ** Perm(&x1[0], 1\4); + ensures \result == h(x0, x1); + @*/ + int g(int* x0, /*@ unique<2> @*/ int* x1){ + return x0[0] + x1[0]; + } + + + /*@ + requires x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\4); + requires y != NULL ** \pointer_length(y) > 0 ** Perm(&y[0], 1\4); + ensures \result == x[0]+y[0]; + pure int h(int* x, unique<2>int * y) = x[0]+y[0]; + @*/ +""" + + vercors should verify using silicon in "Call non-unique function" c """/*@ + context n > 0; + context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i @*/ int* x0, /*@ unique<2> @*/ int* x1){ + //@ assert h(x0) + h(x1) == x0[0] + x1[0]; + return 0; + } + + /*@ + requires x != NULL ** \pointer_length(x) > 0 ** Perm(&x[0], 1\2); + ensures \result == x[0]; + pure int h(int* x) = x[0]; + @*/ + """ } \ No newline at end of file From 839a13c0d9422ab3e3fd80a7d57823234b83d91f Mon Sep 17 00:00:00 2001 From: Lars Date: Fri, 9 Aug 2024 15:47:22 +0200 Subject: [PATCH 11/12] Typedef struct works properly now --- src/col/vct/col/resolve/lang/C.scala | 12 +++++++++--- src/rewrite/vct/rewrite/lang/LangTypesToCol.scala | 11 +++++++++++ 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 709c4bf10d..9d2a45eb7d 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -129,9 +129,10 @@ case object C extends LazyLogging { } 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 @@ -141,7 +142,12 @@ case object C extends LazyLogging { // 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) - info.typeOrReturnType(getPrimitiveType(specs, context)) + val t = specs match { + case CStructDeclaration(_, _) +: Seq() => CTStruct[G](gdecl.ref) + case _ => getPrimitiveType(specs, context) + } + + info.typeOrReturnType(t) } def getPrimitiveType[G]( @@ -185,7 +191,7 @@ case object C extends LazyLogging { 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 diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index a6b6c290d0..4d61cc7c86 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -204,6 +204,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 From 3335ff9e19467e21c7d6ca1453e753f483b9ae11 Mon Sep 17 00:00:00 2001 From: Lars Date: Thu, 3 Oct 2024 16:20:45 +0200 Subject: [PATCH 12/12] WIP unique fields --- src/col/vct/col/ast/Node.scala | 19 ++++++ .../col/ast/expr/heap/read/DerefImpl.scala | 21 +++++- .../col/ast/unsorted/CTStructUniqueImpl.scala | 9 +++ .../unsorted/CUniquePointerFieldImpl.scala | 9 +++ .../CoerceBetweenUniqueClassImpl.scala | 9 +++ .../CoerceBetweenUniqueStructImpl.scala | 9 +++ .../col/ast/unsorted/TClassUniqueImpl.scala | 9 +++ src/col/vct/col/resolve/ResolutionError.scala | 7 ++ src/col/vct/col/resolve/Resolve.scala | 37 +++++------ src/col/vct/col/resolve/lang/C.scala | 42 ++++++++---- .../vct/col/typerules/CoercingRewriter.scala | 2 + src/col/vct/col/typerules/CoercionUtils.scala | 14 +++- src/parsers/antlr4/SpecLexer.g4 | 1 + src/parsers/antlr4/SpecParser.g4 | 1 + .../vct/parsers/transform/CToCol.scala | 5 +- .../vct/rewrite/TypeQualifierCoercion.scala | 58 +++++++++++++++++ src/rewrite/vct/rewrite/lang/LangCToCol.scala | 35 +++++++--- .../vct/rewrite/lang/LangSpecificToCol.scala | 7 +- .../vct/rewrite/lang/LangTypesToCol.scala | 15 ++++- .../integration/examples/QualifierSpec.scala | 64 +++++++++++++++++++ 20 files changed, 323 insertions(+), 50 deletions(-) create mode 100644 src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 19bbbb6cdb..0582e07886 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -140,6 +140,13 @@ final case class TConst[G](inner: Type[G])( final case class TUnique[G](inner: Type[G], unique: BigInt)( implicit val o: Origin = DiagnosticOrigin ) extends Type[G] with TUniqueImpl[G] +final case class CTStructUnique[G](inner: Type[G], fieldRef: Ref[G, CStructMemberDeclarator[G]], unique: BigInt)( + implicit val o: Origin = DiagnosticOrigin +) extends CType[G] with CTStructUniqueImpl[G] +final case class TClassUnique[G](inner: Type[G], fieldRef: Ref[G, InstanceField[G]], unique: BigInt)( + implicit val o: Origin = DiagnosticOrigin +) extends Type[G] with TClassUniqueImpl[G] + sealed trait PointerType[G] extends Type[G] with PointerTypeImpl[G] final case class TPointer[G](element: Type[G])( @@ -964,6 +971,14 @@ final case class CoerceBetweenUniquePointer[G](source: Type[G], target: Type[G]) implicit val o: Origin ) extends Coercion[G] with CoerceBetweenUniquePointerImpl[G] +final case class CoerceBetweenUniqueClass[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniqueClassImpl[G] +final case class CoerceBetweenUniqueStruct[G](source: Type[G], target: Type[G])( + implicit val o: Origin +) extends Coercion[G] with CoerceBetweenUniqueStructImpl[G] + + final case class CoerceToConst[G](source: Type[G])( implicit val o: Origin ) extends Coercion[G] with CoerceToConstImpl[G] @@ -2631,6 +2646,10 @@ final case class CAtomic[G]()(implicit val o: Origin) extends CTypeQualifier[G] with CAtomicImpl[G] final case class CUnique[G](i: BigInt)(implicit val o: Origin) extends CTypeQualifier[G] with CUniqueImpl[G] +final case class CUniquePointerField[G](name: String, i: BigInt)(implicit val o: Origin) + extends CTypeQualifier[G] with CUniquePointerFieldImpl[G] { + var ref: Option[RefCStructField[G]] = None +} sealed trait CFunctionSpecifier[G] extends CDeclarationSpecifier[G] with CFunctionSpecifierImpl[G] diff --git a/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala b/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala index 84ef4f7d4f..66b719507d 100644 --- a/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala +++ b/src/col/vct/col/ast/expr/heap/read/DerefImpl.scala @@ -7,6 +7,9 @@ import vct.col.ast.{ Expr, FieldLocation, TClass, + TClassUnique, + TPointer, + TUnique, Type, Value, } @@ -17,8 +20,22 @@ import vct.col.ast.ops.DerefOps trait DerefImpl[G] extends ExprImpl[G] with DerefOps[G] { this: Deref[G] => - override def t: Type[G] = - obj.t.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t) + override def t: Type[G] = obj.t match { + case TClassUnique(inner, fieldRef, unique) if fieldRef.decl == ref.decl => + addUniquePointer(inner, unique) + case t => getT(t) + } + + def getT(classT: Type[G]): Type[G] = { + classT.asClass.map(_.instantiate(ref.decl.t)).getOrElse(ref.decl.t) + } + + def addUniquePointer(inner: Type[G], unique: BigInt): Type[G] = { + getT(inner) match { + case TPointer(inner) => TPointer(TUnique(inner, unique)) + case _ => ??? + } + } override def check(context: CheckContext[G]): Seq[CheckError] = Check.inOrder( diff --git a/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala b/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala new file mode 100644 index 0000000000..a7731315e9 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CTStructUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CTStructUnique +import vct.col.ast.ops.CTStructUniqueOps +import vct.col.print._ + +trait CTStructUniqueImpl[G] extends CTStructUniqueOps[G] { this: CTStructUnique[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala b/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala new file mode 100644 index 0000000000..30f0308eb0 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CUniquePointerFieldImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CUniquePointerField +import vct.col.ast.ops.CUniquePointerFieldOps +import vct.col.print._ + +trait CUniquePointerFieldImpl[G] extends CUniquePointerFieldOps[G] { this: CUniquePointerField[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala new file mode 100644 index 0000000000..6a3aaecce9 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueClassImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceBetweenUniqueClass +import vct.col.ast.ops.CoerceBetweenUniqueClassOps +import vct.col.print._ + +trait CoerceBetweenUniqueClassImpl[G] extends CoerceBetweenUniqueClassOps[G] { this: CoerceBetweenUniqueClass[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala new file mode 100644 index 0000000000..fa95827757 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/CoerceBetweenUniqueStructImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.CoerceBetweenUniqueStruct +import vct.col.ast.ops.CoerceBetweenUniqueStructOps +import vct.col.print._ + +trait CoerceBetweenUniqueStructImpl[G] extends CoerceBetweenUniqueStructOps[G] { this: CoerceBetweenUniqueStruct[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala b/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala new file mode 100644 index 0000000000..8060f44485 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/TClassUniqueImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.unsorted + +import vct.col.ast.TClassUnique +import vct.col.ast.ops.TClassUniqueOps +import vct.col.print._ + +trait TClassUniqueImpl[G] extends TClassUniqueOps[G] { this: TClassUnique[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/resolve/ResolutionError.scala b/src/col/vct/col/resolve/ResolutionError.scala index 61bef3850e..1d43854286 100644 --- a/src/col/vct/col/resolve/ResolutionError.scala +++ b/src/col/vct/col/resolve/ResolutionError.scala @@ -17,6 +17,13 @@ case class MultipleForwardDeclarationContractError( ) } +case class NotSupportedStructUniqueField(use: Node[_]) + extends ResolutionError { + override def text: String = + use.o.messageInContext(s"This use of unique_pointer_field is not supported") + override def code: String = "notSupportedStructUniqueField" +} + case class NoSuchNameError(kind: String, name: String, use: Node[_]) extends ResolutionError { override def text: String = diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 9b4753bb3e..da49ae3c6f 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -3,7 +3,7 @@ package vct.col.resolve import com.typesafe.scalalogging.LazyLogging import hre.data.BitString import hre.util.FuncTools -import vct.col.ast._ +import vct.col.ast.{CUniquePointerField, _} import vct.col.ast.util.Declarator import vct.col.check.CheckError import vct.col.origin._ @@ -11,23 +11,8 @@ import vct.col.resolve.ResolveReferences.scanScope import vct.col.ref.Ref import vct.col.resolve.ctx._ import vct.col.resolve.lang.{C, CPP, Java, LLVM, PVL, Spec} -import vct.col.resolve.Resolve.{ - MalformedBipAnnotation, - SpecContractParser, - SpecExprParser, - getLit, - isBip, -} -import vct.col.resolve.lang.JavaAnnotationData.{ - BipComponent, - BipData, - BipGuard, - BipInvariant, - BipPort, - BipPure, - BipStatePredicate, - BipTransition, -} +import vct.col.resolve.Resolve.{MalformedBipAnnotation, SpecContractParser, SpecExprParser, getLit, isBip} +import vct.col.resolve.lang.JavaAnnotationData.{BipComponent, BipData, BipGuard, BipInvariant, BipPort, BipPure, BipStatePredicate, BipTransition} import vct.col.rewrite.InitialGeneration import vct.result.VerificationError.{Unreachable, UserError} @@ -188,6 +173,16 @@ case object ResolveTypes { case _ => ctx } + def addUniquePointerFieldRef[G](specifiers: Seq[CDeclarationSpecifier[G]], ctx: TypeResolutionContext[G], blameNode: Node[G]): Unit = { + val pf: Seq[CUniquePointerField[G]] = specifiers.collect + { case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) => s} + pf.foreach(f => + f.ref = Some(C.getUniquePointerStructFieldRef(specifiers, ctx).getOrElse( + throw NotSupportedStructUniqueField(blameNode) + )) + ) + } + def resolveOne[G](node: Node[G], ctx: TypeResolutionContext[G]): Unit = node match { case javaClass @ JavaNamedType(genericNames) => @@ -206,6 +201,12 @@ case object ResolveTypes { C.findCStruct(name, ctx) .getOrElse(throw NoSuchNameError("struct", name, t)) ) + case d: CParam[G] => addUniquePointerFieldRef(d.specifiers, ctx, d) + case d: CStructMemberDeclarator[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case d: CDeclaration[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case d: CFunctionDefinition[G] => addUniquePointerFieldRef(d.specs, ctx, d) + case t: CPrimitiveType[G] => addUniquePointerFieldRef(t.specifiers, ctx, t) + case t @ CPPTypedefName(nestedName, _) => t.ref = Some(CPP.findCPPTypeName(nestedName, ctx).getOrElse( throw NoSuchNameError("class, struct, or namespace", nestedName, t) diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 9d2a45eb7d..e9346e070f 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -6,6 +6,7 @@ import vct.col.ast._ import vct.col.ast.`type`.typeclass.TFloats.{C_ieee754_32bit, C_ieee754_64bit} import vct.col.ast.util.ExpressionEqualityCheck.isConstantInt import vct.col.origin._ +import vct.col.ref.Ref import vct.col.resolve._ import vct.col.resolve.ctx._ import vct.col.typerules.Types @@ -71,6 +72,10 @@ case object C extends LazyLogging { q match { case CConst() => TConst(t)(q.o) case CUnique(i) => TUnique(t, i)(q.o) + case pf@CUniquePointerField(_, i) => + val field: CStructMemberDeclarator[G] = pf.ref.get.decls + val fieldRef: Ref[G, CStructMemberDeclarator[G]] = field.ref + CTStructUnique(t, fieldRef, i)(q.o) case _ => throw CTypeNotSupported(Some(q)) } } @@ -166,18 +171,10 @@ case object C extends LazyLogging { case _ => throw CTypeNotSupported(context) } - val (typeSpecs, nonTypeSpecs) = specs.filter { + val (typeSpecs, qualifiers) = specs.filter { case _: CTypeSpecifier[G] | _: CTypeQualifierDeclarationSpecifier[G] => true ; case _ => false }.partition { case _: CTypeSpecifier[G] => true; case _ => false } - var unique: Option[BigInt] = None - var constant: Boolean = false - nonTypeSpecs.foreach({ - case CTypeQualifierDeclarationSpecifier(CUnique(i)) if unique.isEmpty => unique = Some(i) - case CTypeQualifierDeclarationSpecifier(CConst()) => constant = true - case _ => throw CTypeNotSupported(context) - }) - val t: Type[G] = typeSpecs match { case Seq(CVoid()) => TVoid() @@ -204,7 +201,7 @@ case object C extends LazyLogging { case Some(size) => CTVector(size, t) } - nonTypeSpecs.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } + qualifiers.collect{ case CTypeQualifierDeclarationSpecifier(q) => q } .foldLeft(res)(qualify[G]) } @@ -294,12 +291,13 @@ case object C extends LazyLogging { case _ => None } case struct: CTStruct[G] => getCStructDeref(struct.ref.decl, name) + case struct: CTStructUnique[G] => findStruct(struct.inner, name) } def getCStructDeref[G]( decl: CGlobalDeclaration[G], name: String, - ): Option[CDerefTarget[G]] = + ): Option[RefCStructField[G]] = decl.decl match { case CDeclaration(_, _, Seq(CStructDeclaration(_, decls)), Seq()) => decls.flatMap(Referrable.from).collectFirst { @@ -308,6 +306,28 @@ case object C extends LazyLogging { case _ => None } + def getUniquePointerStructFieldRef[G]( + specs: Seq[CDeclarationSpecifier[G]], + ctx: TypeResolutionContext[G] + ): Option[RefCStructField[G]] = { + var pf: Option[CUniquePointerField[G]] = None + var struct: Option[CStructSpecifier[G]] = None + specs foreach { + case CTypeQualifierDeclarationSpecifier(s: CUniquePointerField[G]) => + if(pf.isDefined) return None + pf = Some(s) + case s: CStructSpecifier[G] => + if(struct.isDefined) return None + struct = Some(s) + case _ => + } + if(pf.isEmpty || struct.isEmpty) return None + + val structRef: RefCStruct[G] = C.findCStruct(struct.get.name, ctx) + .getOrElse(return None) + C.getCStructDeref(structRef.decl, pf.get.name) + } + def openCLVectorAccessString[G]( access: String, typeSize: BigInt, diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index b65b5161b0..05a79b9e70 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -278,6 +278,8 @@ abstract class CoercingRewriter[Pre <: Generation]() case CoerceFromUniquePointer(_, _) => e case CoerceToUniquePointer(_, _) => e case CoerceBetweenUniquePointer(_, _) => e + case CoerceBetweenUniqueStruct(_, _) => e + case CoerceBetweenUniqueClass(_, _) => e case CoerceSupports(_, _) => e case CoerceClassAnyClass(_, _) => e diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 6a63887c4d..99934ff6ef 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -194,6 +194,8 @@ case object CoercionUtils { case (TNull(), TArray(target)) => CoerceNullArray(target) case (TNull(), TClass(target, typeArgs)) => CoerceNullClass(target, typeArgs) + case (TNull(), TClassUnique(TClass(target, typeArgs), _, _)) => + CoerceNullClass(target, typeArgs) case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target) case (TNull(), TAnyClass()) => CoerceNullAnyClass() case (TNull(), target: PointerType[G]) => CoerceNullPointer(target) @@ -291,10 +293,19 @@ case object CoercionUtils { supp.cls.decl == targetClass.decl } => CoerceSupports(sourceClass, targetClass) - + case (source @ TClass(_, _), target@TClassUnique(innerT @ TClass(_, _), _, _)) if innerT == source => + CoerceBetweenUniqueClass(source, target) + case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@ TClass(_, _)) if innerS == target => + CoerceBetweenUniqueClass(source, target) + case (source@TClassUnique(innerS @ TClass(_, _), _, _), target@TClassUnique(innerT @ TClass(_, _), _, _)) + if innerT == innerS => + CoerceBetweenUniqueClass(source, target) case (source @ TClass(sourceClass, typeArgs), TAnyClass()) => CoerceClassAnyClass(sourceClass, typeArgs) + case (source @ TClassUnique(TClass(sourceClass, typeArgs), _ ,_), TAnyClass()) => + CoerceClassAnyClass(sourceClass, typeArgs) + case ( source @ JavaTClass(sourceClass, Nil), target @ JavaTClass(targetClass, Nil), @@ -671,6 +682,7 @@ case object CoercionUtils { case t: TConst[G] => getAnyClassCoercion(t.inner).map{ case (c, res) => (CoercionSequence(Seq(CoerceFromConst(t.inner), c)), res)} case t: TClass[G] => Some((CoerceIdentity(source), t)) + case t: TClassUnique[G] => getAnyClassCoercion(t.inner) case t: TUnion[G] => val superType = Types.leastCommonSuperType(t.types) diff --git a/src/parsers/antlr4/SpecLexer.g4 b/src/parsers/antlr4/SpecLexer.g4 index c96d691c95..3842ef56ff 100644 --- a/src/parsers/antlr4/SpecLexer.g4 +++ b/src/parsers/antlr4/SpecLexer.g4 @@ -59,6 +59,7 @@ VAL_PURE: 'pure'; VAL_THREAD_LOCAL: 'thread_local'; VAL_BIP_ANNOTATION: 'bip_annotation'; VAL_UNIQUE: 'unique'; +VAL_UNIQUE_POINTER_FIELD: 'unique_pointer_field'; VAL_WITH: 'with'; VAL_THEN: 'then'; diff --git a/src/parsers/antlr4/SpecParser.g4 b/src/parsers/antlr4/SpecParser.g4 index cadae5d5eb..cd560cb6c3 100644 --- a/src/parsers/antlr4/SpecParser.g4 +++ b/src/parsers/antlr4/SpecParser.g4 @@ -421,6 +421,7 @@ valModifier valTypeQualifier : 'unique' '<' langConstInt '>' # valUnique + | 'unique_pointer_field' '<' langId ',' langConstInt '>' # valUniquePointerField ; valArgList diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index ca5a375b16..1112b0dd5b 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -1188,15 +1188,16 @@ case class CToCol[G]( case ValStatic(_) => collector.static += mod } - def convert(mod: ValEmbedTypeQualifierContext): CUnique[G] = + def convert(mod: ValEmbedTypeQualifierContext): CTypeQualifier[G] = mod match { case ValEmbedTypeQualifier0(_, mod, _) => convert(mod) case ValEmbedTypeQualifier1(mod) => convert(mod) } - def convert(implicit mod: ValTypeQualifierContext): CUnique[G] = + def convert(implicit mod: ValTypeQualifierContext): CTypeQualifier[G] = mod match { case ValUnique(_, _, uniqueId, _) => CUnique[G](convert(uniqueId)) + case ValUniquePointerField(_, _, name, _, uniqueId, _) => CUniquePointerField[G](convert(name), convert(uniqueId)) } def convertEmbedWith( diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala index e0a04cea23..22f7073ba1 100644 --- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala +++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala @@ -42,6 +42,46 @@ case object TypeQualifierCoercion extends RewriterBuilder { case class TypeQualifierCoercion[Pre <: Generation]() extends CoercingRewriter[Pre] { + val uniqueClasses: mutable.Map[(Class[Pre], Map[InstanceField[Pre], BigInt]), Class[Post]] = mutable.Map() + val uniqueField: mutable.Map[(InstanceField[Pre], Map[InstanceField[Pre], BigInt]), InstanceField[Post]] = mutable.Map() +// val classCopyTypes: ScopedStack[Map[Type[Pre], Type[Post]]] = ScopedStack() + + def createUniqueClassCopy(original: Class[Pre], pointerInstanceFields: Map[InstanceField[Pre], BigInt]): Class[Post] = { + globalDeclarations.declare({ + classDeclarations.scope({ + val decls = classDeclarations.collect { original.decls.foreach { d => + classDeclarations.declare[InstanceField[Post]] { d match { + case field: InstanceField[Pre] if pointerInstanceFields.contains(field) => + val unique = pointerInstanceFields(field) + val it = field.t match { + case TPointer(it) => it + case _ => ??? // Not allowed + } + val (info, innerResType) = getUnqualified(it) + if (info.const) ??? // Not allowed + val resType = TUniquePointer(innerResType, unique) + val resField = field.rewrite(t = resType) + uniqueField((field, pointerInstanceFields)) = resField + resField + case field: InstanceField[Pre] => + val resField = field.rewrite() + uniqueField((field, pointerInstanceFields)) = resField + resField + case _ => ??? // Not allowed + }} + }}._1 + original.rewrite(decls=decls) + }) + }) + } + + def getUniqueMap(t: TClassUnique[Pre]): (Map[InstanceField[Pre], BigInt], TClass[Pre]) = t.inner match { + case it: TClassUnique[Pre] => val (res, classT) = getUniqueMap(it) + if(res.contains(t.fieldRef.decl)) ??? // Not allowed + (res + (t.fieldRef.decl -> t.unique), classT) + case classT: TClass[Pre] => (Map(t.fieldRef.decl -> t.unique), classT) + } + override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])( implicit o: Origin ): Expr[Post] = { @@ -54,6 +94,7 @@ case class TypeQualifierCoercion[Pre <: Generation]() case CoerceToUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) case CoerceFromUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) case CoerceBetweenUniquePointer(s, t) => return UniquePointerCoercion(e, dispatch(t)) + case CoerceBetweenUniqueClass(_, t) => return UniquePointerCoercion(e, dispatch(t)) case _ => } e @@ -64,6 +105,11 @@ case class TypeQualifierCoercion[Pre <: Generation]() case TConst(t) => dispatch(t) case TUnique(_, _) => throw DisallowedQualifiedType(t) case TPointer(it) => makePointer(it) + case tu: TClassUnique[Pre] => + val (map, classT) = getUniqueMap(tu) + val c = classT.cls.decl + val uniqueClass = uniqueClasses.getOrElseUpdate((c,map), createUniqueClassCopy(c, map)) + classT.rewrite(cls = uniqueClass.ref) case other => other.rewriteDefault() } @@ -76,6 +122,18 @@ case class TypeQualifierCoercion[Pre <: Generation]() val (info, newT) = getUnqualified(t) if(info.const) NewConstPointerArray(newT, dispatch(size))(npa.blame) else NewPointerArray(newT, dispatch(size), info.unique)(npa.blame) + case d@Deref(obj, ref) => + obj match { + // Always has an CoerceClassAnyClassCoercion + case ApplyCoercion(e, _) if e.t.isInstanceOf[TClassUnique[Pre]] => + val source = e.t.asInstanceOf[TClassUnique[Pre]] + d.rewriteDefault() + val (map, classT) = getUniqueMap(source) + if (!uniqueField.contains(ref.decl, map)) createUniqueClassCopy(classT.cls.decl, map) + d.rewrite(ref = uniqueField(ref.decl, map).ref) + case _ => d.rewriteDefault() + } + case other => other.rewriteDefault() } } diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 05eeb06872..1a0abcfa31 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -394,6 +394,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case CPrimitiveType(specs) => getBaseType(C.getPrimitiveType(specs, Some(t))) case TUnique(it, _) => getBaseType(it) case TConst(it) => getBaseType(it) + case TClassUnique(it, _, _) => getBaseType(it) + case CTStructUnique(it, _, _) => getBaseType(it) case _ => t } @@ -1272,10 +1274,12 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => false } - def isStruct(t: Type[Pre]): Boolean = + def isStruct(t: Type[Pre]): Boolean = getStruct(t).isDefined + + def getStruct(t: Type[Pre]): Option[CTStruct[Pre]] = getBaseType(t) match { - case t : CTStruct[Pre] => true - case _ => false + case t : CTStruct[Pre] => Some(t) + case _ => None } def isPointer(t: Type[Pre]): Boolean = @@ -1448,6 +1452,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) val structRef = getBaseType(deref.struct.t) match { case CTPointer(CTStruct(struct)) => struct + case CTPointer(CTStructUnique(CTStruct(struct), fieldRef, unique)) => struct case t => throw WrongStructType(t) } Deref[Post]( @@ -1483,7 +1488,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(blame) )(struct.blame) member.specs.collectFirst { - case CSpecificationType(newStruct: CTStruct[Pre]) => + case CSpecificationType(specT) if isStruct(specT) => + val newStruct = getStruct(specT).get // We recurse, since a field is another struct Perm(loc, newPerm) &* unwrapStructPerm( loc, @@ -2028,9 +2034,18 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) TPointer(rw.dispatch(t.innerType)) } - def structType(t: CTStruct[Pre]): Type[Post] = { - val targetClass = - new LazyRef[Post, Class[Post]](cStructSuccessor(t.ref.decl)) - TClass[Post](targetClass, Seq())(t.o) - } -} + def structType(t: CType[Pre]): Type[Post] = t match { + case ts @ CTStruct(ref) => + val targetClass = + new LazyRef[Post, Class[Post]](cStructSuccessor(ref.decl)) + TClass[Post](targetClass, Seq())(t.o) + case CTStructUnique(CTStruct(ref), fieldRef, unique) => + val targetClass = + new LazyRef[Post, Class[Post]](cStructSuccessor(ref.decl)) + val targetField = + new LazyRef[Post, InstanceField[Post]](cStructFieldsSuccessor((ref.decl, fieldRef.decl))) + val tInner = TClass[Post](targetClass, Seq())(t.o) + TClassUnique[Post](tInner, targetField, unique)(t.o) + case _ => ??? + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 87ff3e3678..bafcccd2cd 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -324,7 +324,7 @@ case class LangSpecificToCol[Pre <: Generation]( case sizeof: SizeOf[Pre] => throw LangCToCol.UnsupportedSizeof(sizeof) case Perm(a @ AmbiguousLocation(expr), perm) - if c.getBaseType(expr.t).isInstanceOf[CTStruct[Pre]] => + if c.isStruct(expr.t) => c.getBaseType(expr.t) match { case structType: CTStruct[Pre] => c.unwrapStructPerm( @@ -366,9 +366,7 @@ case class LangSpecificToCol[Pre <: Generation]( case _ => } assign.target.t match { - case CPrimitiveType(specs) if specs.collectFirst { - case CSpecificationType(_: CTStruct[Pre]) => () - }.isDefined => + case t if c.isStruct(t) => c.assignStruct(assign) case CPPPrimitiveType(_) => cpp.preAssignExpr(assign) case _ => rewriteDefault(assign) @@ -396,6 +394,7 @@ case class LangSpecificToCol[Pre <: Generation]( case t: TOpenCLVector[Pre] => c.vectorType(t) case t: CTArray[Pre] => c.arrayType(t) case t: CTStruct[Pre] => c.structType(t) + case t: CTStructUnique[Pre] => c.structType(t) case t: CPPTArray[Pre] => cpp.arrayType(t) case other => rewriteDefault(other) } diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index 4d61cc7c86..c6826135eb 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -7,6 +7,7 @@ import vct.col.ref.{Ref, UnresolvedRef} import vct.col.resolve.ctx._ import vct.col.resolve.lang.{C, CPP} import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} +import vct.col.util.SuccessionMap import vct.result.VerificationError.UserError import vct.rewrite.lang.LangTypesToCol.{EmptyInlineDecl, IncompleteTypeArgs} @@ -35,6 +36,12 @@ case object LangTypesToCol extends RewriterBuilder { } case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { + + val cStructFieldsSuccessor: SuccessionMap[ + (CStructMemberDeclarator[Pre]), + CStructMemberDeclarator[Post], + ] = SuccessionMap() + override def porcelainRefSucc[RefDecl <: Declaration[Rewritten[Pre]]]( ref: Ref[Pre, _] )(implicit tag: ClassTag[RefDecl]): Option[Ref[Rewritten[Pre], RefDecl]] = @@ -94,6 +101,9 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { dispatch(C.getPrimitiveType(specs, context = Some(t))) case t @ CPPPrimitiveType(specs) => dispatch(CPP.getBaseTypeFromSpecs(specs, context = Some(t))) + case t @ CTStructUnique(inner, fieldRef, unique) => + val fieldSucc: Ref[Post, CStructMemberDeclarator[Post]] = cStructFieldsSuccessor(fieldRef.decl).ref + t.rewrite(fieldRef = fieldSucc) case t @ SilverPartialTAxiomatic(Ref(adt), partialTypeArgs) => if (partialTypeArgs.map(_._1.decl).toSet != adt.typeArgs.toSet) throw IncompleteTypeArgs(t) @@ -239,8 +249,9 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { decl, context = Some(declaration), ) - cStructMemberDeclarators - .declare(declaration.rewrite(specs = specs, decls = Seq(newDecl))) + val newMember = declaration.rewrite(specs = specs, decls = Seq(newDecl)) + cStructFieldsSuccessor(declaration) = newMember + cStructMemberDeclarators.declare(newMember) }) case declaration: CFunctionDefinition[Pre] => implicit val o: Origin = declaration.o diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala index ceec1aaf0a..dad6a34f8f 100644 --- a/test/main/vct/test/integration/examples/QualifierSpec.scala +++ b/test/main/vct/test/integration/examples/QualifierSpec.scala @@ -2,6 +2,69 @@ package vct.test.integration.examples import vct.test.integration.helper.VercorsSpec +class QualifierSpecWIP extends VercorsSpec { + vercors should verify using silicon in "Unique pointer field of struct containing unique struct" c """ + struct vec2 { + int* xxs; + }; + + struct vec { + int* xs; + /*@unique_pointer_field@*/ struct vec2 v; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs, /*@unique_pointer_field@*/ struct vec2 v){ + x1->xs = xs; + x1->v = v; + //@ assert xs != NULL; + return 0; + } + """ +} + +class StructQualifierSpec extends VercorsSpec { + vercors should verify using silicon in "Unique pointer field of struct" c """ + struct vec { + int* xs; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs){ + x1->xs = xs; + //@ assert xs != NULL; + return 0; + } + """ + + vercors should verify using silicon in "Unique pointer field of struct containing struct" c """ + struct vec2 { + int* xxs; + }; + + struct vec { + int* xs; + struct vec2 v; + }; + + /*@ + context xs != NULL; + context x1 != NULL ** \pointer_length(x1)==1 ** Perm(x1, write) ** Perm(*x1, write); + @*/ + int f(/*@unique_pointer_field@*/ struct vec* x1, /*@ unique<2> @*/ int* xs){ + x1->xs = xs; + //@ assert xs != NULL; + return 0; + } + """ +} + class QualifierSpec extends VercorsSpec { vercors should verify using silicon example "concepts/unique/arrays.c" @@ -123,6 +186,7 @@ ensures \result == 2*x0[0] + 2*x1[0]; @*/ int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){ return h(x0, x0) + h(x1, x1); + h(x0, x1); } /*@