From 44a3944e5f0b6e9c0bcc4182d70c2cf30a5b9283 Mon Sep 17 00:00:00 2001 From: Lars Date: Fri, 24 Nov 2023 00:02:40 +0100 Subject: [PATCH] Changes to loop contracts init values for structs --- src/col/vct/col/ast/Node.scala | 2 +- src/col/vct/col/resolve/lang/C.scala | 6 ++-- .../rewrite/CollectLocalDeclarations.scala | 7 ----- .../rewrite/IterationContractToParBlock.scala | 8 +++++- src/rewrite/vct/rewrite/PrettifyBlocks.scala | 4 +-- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 10 +++++-- .../vct/rewrite/lang/LangTypesToCol.scala | 8 ------ .../vct/test/integration/examples/CSpec.scala | 28 ++++++++++++++++++- 8 files changed, 47 insertions(+), 26 deletions(-) diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 8af0e75965..157037e2cb 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -906,7 +906,7 @@ final case class CSpecificationType[G](t: Type[G])(implicit val o: Origin) exten final case class CStructDeclaration[G](name: Option[String], decl: Seq[CStructMemberDeclarator[G]])(implicit val o: Origin) extends CTypeSpecifier[G] with CStructDeclarationImpl[G] final case class CStructSpecifier[G](name: String)(implicit val o: Origin) extends CTypeSpecifier[G] with CStructSpecifierImpl[G] { - var ref: Option[CStructTarget[G]] = None + var ref: Option[RefCStruct[G]] = None } final case class CStructMemberDeclarator[G](specs: Seq[CDeclarationSpecifier[G]], decls: Seq[CDeclarator[G]])(implicit val o: Origin) extends Declaration[G] with CStructMemberDeclaratorImpl[G] diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 40acd07423..d77b89e0ea 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/src/col/vct/col/resolve/lang/C.scala @@ -75,7 +75,7 @@ case object C { case Seq(CBool()) => TBool() case Seq(defn @ CTypedefName(_)) => Types.notAValue(defn.ref.get) case Seq(CSpecificationType(typ)) => typ - case Seq(defn @ CStructSpecifier(_)) => Types.notAValue(defn.ref.get) + case Seq(defn @ CStructSpecifier(_)) => CTStruct(defn.ref.get.decl.ref) case spec +: _ => throw CTypeNotSupported(context.orElse(Some(spec))) case _ => throw CTypeNotSupported(context) } @@ -94,9 +94,9 @@ case object C { case target: CTypeNameTarget[G] if target.name == name => target } - def findCStruct[G](name: String, ctx: TypeResolutionContext[G]): Option[CStructTarget[G]] = + def findCStruct[G](name: String, ctx: TypeResolutionContext[G]): Option[RefCStruct[G]] = ctx.stack.flatten.collectFirst { - case target: CStructTarget[G] if target.name == name => target + case target: RefCStruct[G] if target.name == name => target } def findCName[G](name: String, ctx: ReferenceResolutionContext[G]): Option[CNameTarget[G]] = diff --git a/src/rewrite/vct/rewrite/CollectLocalDeclarations.scala b/src/rewrite/vct/rewrite/CollectLocalDeclarations.scala index 686d67331f..bcb7c83abe 100644 --- a/src/rewrite/vct/rewrite/CollectLocalDeclarations.scala +++ b/src/rewrite/vct/rewrite/CollectLocalDeclarations.scala @@ -27,13 +27,6 @@ case class CollectLocalDeclarations[Pre <: Generation]() extends Rewriter[Pre] { dispatch(impl) } Scope[Post](newVars, newImpl)(stat.o) - case Loop(_, _, _, _, _: Scope[Pre]) => rewriteDefault(stat) - case loop@Loop(_, _, _, _, body) => - val (newVars, newBody) = variables.collect { - dispatch(body) - } - val bodyScope = Scope[Post](newVars, newBody)(body.o) - loop.rewrite(body = bodyScope) case other => rewriteDefault(other) } } \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/IterationContractToParBlock.scala b/src/rewrite/vct/rewrite/IterationContractToParBlock.scala index 5840999497..d93c77d59e 100644 --- a/src/rewrite/vct/rewrite/IterationContractToParBlock.scala +++ b/src/rewrite/vct/rewrite/IterationContractToParBlock.scala @@ -50,6 +50,11 @@ case class IterationContractToParBlock[Pre <: Generation]() extends Rewriter[Pre implicit val o: Origin = loop.o currentIterationVariables.having(v) { + val (newVars, newBody) = variables.collect { + dispatch(body) + } + val bodyScope = Scope[Post](newVars, newBody)(body.o) + sendDecls.scope { ParStatement( ParBlock( @@ -58,7 +63,8 @@ case class IterationContractToParBlock[Pre <: Generation]() extends Rewriter[Pre requires = dispatch(requires), ensures = dispatch(ensures), context_everywhere = dispatch(context_everywhere), - content = dispatch(body), + content = + bodyScope, )(contract.blame) ) } diff --git a/src/rewrite/vct/rewrite/PrettifyBlocks.scala b/src/rewrite/vct/rewrite/PrettifyBlocks.scala index 211eb200d5..aa600c4192 100644 --- a/src/rewrite/vct/rewrite/PrettifyBlocks.scala +++ b/src/rewrite/vct/rewrite/PrettifyBlocks.scala @@ -39,8 +39,8 @@ case class PrettifyBlocks[Pre <: Generation]() extends Rewriter[Pre] { collectVariables(body, extra = locals) } - case loop: Loop[Pre] => - loop.rewrite(body = collectVariables(loop.body)) + case loop @ Loop(_, _, _, _: IterationContract[Pre], body) => + loop.rewrite(body = collectVariables(body)) case vec: VecBlock[Pre] => vec.rewrite(content = collectVariables(vec.content)) diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 4307ee51f0..477be31563 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -788,16 +788,20 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz case _ => throw WrongStructType(decl) } - val target = ref.decl implicit val o: Origin = init.o - val targetClass: Class[Post] = cStructSuccessor(target) + val targetClass: Class[Post] = cStructSuccessor(ref.decl) val t = TClass[Post](targetClass.ref) val v = new Variable[Post](t)(o.sourceName(info.name)) cNameSuccessor(RefCLocalDeclaration(decl, 0)) = v - Block(Seq(LocalDecl(v), assignLocal(v.get, NewObject[Post](targetClass.ref)))) + val copy = init.init.map( v => + Eval(createStructCopy(rw.dispatch(v), ref.decl, (f: InstanceField[_]) => PanicBlame("Cannot fail due to insufficient perm"))) + ) + val stats = Seq(LocalDecl(v), assignLocal(v.get, NewObject[Post](targetClass.ref))) ++ + copy.toSeq + Block(stats) } def rewriteLocal(decl: CLocalDeclaration[Pre]): Statement[Post] = { diff --git a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala index 53c3915546..9b9743e6b7 100644 --- a/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangTypesToCol.scala @@ -75,15 +75,7 @@ case class LangTypesToCol[Pre <: Generation]() extends Rewriter[Pre] { case t @ SilverPartialTAxiomatic(Ref(adt), partialTypeArgs) => if(partialTypeArgs.map(_._1.decl).toSet != adt.typeArgs.toSet) throw IncompleteTypeArgs(t) - TAxiomatic(succ(adt), adt.typeArgs.map(arg => dispatch(t.partialTypeArgs.find(_._1.decl == arg).get._2))) - case TNotAValue(decl) => - decl match { - case RefCStruct(decl) => - CTStruct(succ(decl)) - case RefAxiomaticDataType(decl) => TAxiomatic[Post](succ(decl), Nil) - case _ => rewriteDefault(t) - } case other => rewriteDefault(other) } } diff --git a/test/main/vct/test/integration/examples/CSpec.scala b/test/main/vct/test/integration/examples/CSpec.scala index ec027f25c6..87aa7f6ea7 100644 --- a/test/main/vct/test/integration/examples/CSpec.scala +++ b/test/main/vct/test/integration/examples/CSpec.scala @@ -273,7 +273,7 @@ class CSpec extends VercorsSpec { } """ - vercors should error withCode "type" in "struct type is no value" c + vercors should error withCode "typeUsedAsValue" in "struct type is no value" c """ struct d { int x; @@ -343,4 +343,30 @@ class CSpec extends VercorsSpec { s = t; } """ + + vercors should verify using silicon in "Parallel omp loop with declarations inside" c + """ + #include + #include + + int main(){ + int sum[3] = {0, 0, 0}; + + #pragma omp parallel for + for(int i=0;i<3;i++) + /*@ + context 0 <= i && i <3; + context Perm(&sum[i], write); + requires sum[i] == 0; + ensures sum[i] == i; + @*/ + { + int xs[1] = {i}; + sum[i] += xs[0]; + } + assert(sum[0] == 0); + assert(sum[1] == 1); + assert(sum[2] == 2); + } + """ } \ No newline at end of file