Veymont gen par

examples/technical/veymont-seq-progs/veymont-swap.pvl

@@ -22,13 +22,13 @@ seq_program SeqProgram(int x, int y) {
    thread s1 = Storage(x);
    thread s2 = Storage(y);
 
-  int num() {}
+  //int num() {}
 
   void foo() {
-     s1.temp = 5;
+     s1.temp = 7;
   }
 
-  void bar(int a) {}
+  //void bar(int a) {}
 
   run {
     if(s1.v == 5 && s2.v == 6) {

res/universal/res/include/IntegerChannel.java

@@ -1,16 +1,14 @@
-package include;
-
-public final class IntegerChannel {
+public final class Channel {
 
     private boolean transfering;
 
-    private int exchangeValue;
+    private MessageType exchangeValue;
 
-    public IntegerChannel() {
+    public Channel() {
         transfering = true;
     }
 
-    public synchronized void writeValue(int v) {
+    public synchronized void writeValue(MessageType v) {
         while (!transfering) {
             try {
                 wait();
@@ -23,7 +21,7 @@ public synchronized void writeValue(int v) {
         notify();
     }
 
-    public synchronized int readValue() {
+    public synchronized MessageType readValue() {
         while (transfering) {
             try {
                 wait();

src/col/vct/col/ast/Node.scala

@@ -135,6 +135,7 @@ final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) exten
 final case class TAxiomatic[G](adt: Ref[G, AxiomaticDataType[G]], args: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAxiomaticImpl[G]
 final case class TEnum[G](enum: Ref[G, Enum[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G]
 final case class TProverType[G](ref: Ref[G, ProverType[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TProverTypeImpl[G]
+final case class TVeyMontChannel[G](channelType: String)(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TVeyMontChannelImpl[G]
 
 sealed trait ParRegion[G] extends NodeFamily[G] with ParRegionImpl[G]
 final case class ParParallel[G](regions: Seq[ParRegion[G]])(val blame: Blame[ParPreconditionFailed])(implicit val o: Origin) extends ParRegion[G] with ParParallelImpl[G]
@@ -672,7 +673,7 @@ final case class SuperType[G](left: Expr[G], right: Expr[G])(implicit val o: Ori
 final case class IndeterminateInteger[G](min: Expr[G], max: Expr[G])(implicit val o: Origin) extends Expr[G] with IndeterminateIntegerImpl[G]
 
 sealed trait AssignExpression[G] extends Expr[G] with AssignExpressionImpl[G]
-final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
+final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], chanType: Type[G], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
 final case class VeyMontAssignExpression[G](thread : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontAssignExpressionImpl[G]
 final case class PreAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PreAssignExpressionImpl[G]
 final case class PostAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PostAssignExpressionImpl[G]
@@ -1061,7 +1062,7 @@ sealed trait JavaClassDeclaration[G] extends ClassDeclaration[G] with JavaClassD
 final class JavaSharedInitialization[G](val isStatic: Boolean, val initialization: Statement[G])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaSharedInitializationImpl[G]
 final class JavaFields[G](val modifiers: Seq[JavaModifier[G]], val t: Type[G], val decls: Seq[JavaVariableDeclaration[G]])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaFieldsImpl[G]
 final class JavaConstructor[G](val modifiers: Seq[JavaModifier[G]], val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Statement[G], val contract: ApplicableContract[G])(val blame: Blame[ConstructorFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaConstructorImpl[G]
-final class JavaParam[G](val modifiers: Seq[JavaModifier[G]], val name: String, val t: Type[G])(implicit val o: Origin) extends Declaration[G]
+final class JavaParam[G](val modifiers: Seq[JavaModifier[G]], val name: String, val t: Type[G])(implicit val o: Origin) extends Declaration[G] with JavaParamImpl[G]
 
 final class JavaMethod[G](val modifiers: Seq[JavaModifier[G]], val returnType: Type[G], val dims: Int, val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Option[Statement[G]], val contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaMethodImpl[G]
 final class JavaAnnotationMethod[G](val returnType: Type[G], val name: String, val default: Option[Expr[G]])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaAnnotationMethodImpl[G]

src/col/vct/col/ast/lang/JavaFieldsImpl.scala

@@ -7,5 +7,5 @@ trait JavaFieldsImpl[G] { this: JavaFields[G] =>
   override def isStatic = modifiers.contains(JavaStatic[G]())
 
   override def layout(implicit ctx: Ctx): Doc =
-    Doc.lspread(modifiers) <> t <+> Doc.spread(decls) <> ";"
+    Doc.rspread(modifiers) <> t <+> Doc.spread(decls) <> ";"
 }

src/col/vct/col/ast/lang/JavaLocalDeclarationImpl.scala

@@ -5,5 +5,5 @@ import vct.col.print.{Ctx, Doc, Group}
 
 trait JavaLocalDeclarationImpl[G] { this: JavaLocalDeclaration[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Doc.lspread(modifiers) <> t <+> Doc.args(decls))
+    Group(Doc.rspread(modifiers) <> t <+> Doc.args(decls))
 }

src/col/vct/col/ast/lang/JavaMethodImpl.scala

@@ -12,7 +12,7 @@ trait JavaMethodImpl[G] extends Declarator[G] { this: JavaMethod[G] =>
     Doc.stack(Seq(
       contract,
       Group(Group(Group(
-        Doc.lspread(modifiers) <>
+        Doc.rspread(modifiers) <>
         (if(typeParameters.isEmpty) Empty else Text("<") <> Doc.args(typeParameters) <> ">" <+> Empty) <>
         returnType <+> name <> "[]".repeat(dims)) <> "(" <> Doc.args(parameters) <> ")") <>
         (if(signals.isEmpty) Empty else Empty <>> Group(Text("throws") <+> Doc.args(signals)))

src/col/vct/col/ast/lang/JavaParamImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.JavaParam
+import vct.col.print.{Ctx, Doc, Text}
+
+trait JavaParamImpl[G] { this: JavaParam[G] =>
+  override def layout(implicit ctx: Ctx): Doc = t.show <+> name
+
+}

src/col/vct/col/ast/type/TUnionImpl.scala

@@ -1,7 +1,9 @@
 package vct.col.ast.`type`
 
 import vct.col.ast.TUnion
+import vct.col.print.{Ctx, Doc}
 
 trait TUnionImpl[G] { this: TUnion[G] =>
+  override def layout(implicit ctx: Ctx): Doc =  Doc.fold(types)(_ <+> "|" <+> _)
 
 }

src/col/vct/col/ast/type/TVeyMontChannelImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TVeyMontChannel
+import vct.col.print.{Ctx, Doc, Text}
+
+trait TVeyMontChannelImpl[G] { this: TVeyMontChannel[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Text(this.channelType)
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1625,7 +1625,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case w @ WandApply(assn) => WandApply(res(assn))(w.blame)
       case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
       case VeyMontAssignExpression(t,a) => VeyMontAssignExpression(t,a)
-      case VeyMontCommExpression(r,s,a) => VeyMontCommExpression(r,s,a)
+      case VeyMontCommExpression(r,s,t,a) => VeyMontCommExpression(r,s,t,a)
     }
   }
 

src/main/vct/importer/Util.scala

@@ -1,11 +1,11 @@
 package vct.importer
 
 import hre.io.Readable
-import vct.col.ast.Program
+import vct.col.ast.{JavaClass, JavaNamespace, Program}
 import vct.col.origin.{Blame, VerificationFailure}
 import vct.col.rewrite.Disambiguate
 import vct.main.stages.Resolution
-import vct.parsers.ColPVLParser
+import vct.parsers.{ColJavaParser, ColPVLParser}
 import vct.parsers.transform.{ConstantBlameProvider, ReadableOriginProvider}
 import vct.result.VerificationError.UserError
 
@@ -27,4 +27,19 @@ case object Util {
     val unambiguousProgram: Program[_] = Disambiguate().dispatch(context.tasks.head.program)
     unambiguousProgram.asInstanceOf[Program[G]]
   }
+
+  case class JavaLoadError(error: String) extends UserError {
+    override def code: String = "JavaClassLoadError"
+
+    override def text: String = error
+  }
+
+  def loadJavaClass[G](readable: Readable): JavaClass[G] =
+    ColJavaParser(ReadableOriginProvider(readable), ConstantBlameProvider(LibraryFileBlame)).parse(readable).decls match {
+      case Seq(javaNamespace: JavaNamespace[G]) => javaNamespace.declarations match {
+        case Seq(javaClass: JavaClass[G]) => javaClass
+        case seq => throw JavaLoadError("Expected to load exactly one Java class but found " + seq.size)
+      }
+      case seq => throw JavaLoadError("Expected to load exactly one Java name space but found " + seq.size)
+    }
 }

src/main/vct/main/modes/VeyMont.scala

@@ -14,7 +14,7 @@ object VeyMont extends LazyLogging {
 
   def verifyWithOptions(options: Options, inputs: Seq[PathOrStd]) = {
     val collector = BlameCollector()
-    val stages = Stages.veymontOfOptions(options, ConstantBlameProvider(collector))
+    val stages = Stages.veymontTransformationOfOptions(options, ConstantBlameProvider(collector))
     logger.debug("Stages: " ++ stages.flatNames.map(_._1).mkString(", "))
     stages.run(inputs) match {
       case Left(value) => logger.error(value.text)

src/main/vct/main/stages/CodeGeneration.scala

@@ -0,0 +1,67 @@
+package vct.main.stages
+
+import hre.progress.Progress
+import hre.stages.Stage
+import vct.col.ast.{JavaClass, Node, Verification}
+import vct.col.print.Ctx
+import vct.col.rewrite.{Generation, PrettifyBlocks, RewriterBuilder}
+import vct.importer.Util
+import vct.main.stages.Transformation.writeOutFunctions
+import vct.options.Options
+import vct.options.types.{Backend, PathOrStd}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads
+
+object CodeGeneration {
+
+  private def writeOutFunctions(m: Map[String, PathOrStd]): Seq[(String, Verification[_ <: Generation] => Unit)] =
+    m.toSeq.map {
+      case (key, out) => (key, (program: Verification[_ <: Generation]) => out.write { writer =>
+        program.write(writer)(Ctx().namesIn(program))
+      })
+    }
+
+  def veymontGenerationOfOptions(options: Options): VeyMontGeneration =
+    options.backend match {
+      case Backend.Silicon | Backend.Carbon =>
+        VeyMontGeneration(
+          onBeforePassKey = writeOutFunctions(options.outputBeforePass),
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass),
+          channelClass = Util.loadJavaClass(options.veymontChannel),
+        )
+    }
+}
+
+class CodeGeneration(val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val passes: Seq[RewriterBuilder]
+                       ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]] {
+  override def friendlyName: String = "Generating VeyMont output"
+
+  override def progressWeight: Int = 1
+
+  override def run(input: Verification[_ <: Generation]): Verification[_ <: Generation] = {
+    var result: Verification[_ <: Generation] = input
+    Progress.foreach(passes, (pass: RewriterBuilder) => pass.key) { pass =>
+      onBeforePassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = pass().dispatch(result)
+
+      onAfterPassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = PrettifyBlocks().dispatch(result)
+    }
+    result
+  }
+
+}
+
+case class VeyMontGeneration(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             channelClass: JavaClass[_])
+  extends CodeGeneration(onBeforePassKey, onAfterPassKey, Seq(
+    ParalleliseVeyMontThreads.withArg(channelClass),
+  ))

src/main/vct/main/stages/Stages.scala

@@ -58,10 +58,11 @@ case object Stages {
       .thenRun(ExpectedErrors.ofOptions(options))
   }
 
-  def veymontOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
+  def veymontTransformationOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
     Parsing.ofOptions(options, blameProvider)
       .thenRun(Resolution.ofOptions(options, blameProvider))
-      .thenRun(Transformation.veymontOfOptions(options))
+      .thenRun(Transformation.veymontTransformationOfOptions(options))
+      .thenRun(CodeGeneration.veymontGenerationOfOptions(options))
       .thenRun(Output.veymontOfOptions(options))
   }
 

src/main/vct/main/stages/Transformation.scala

@@ -66,12 +66,12 @@ object Transformation {
         )
     }
 
-  def veymontOfOptions(options: Options): Transformation =
+  def veymontTransformationOfOptions(options: Options): Transformation =
     options.backend match {
       case Backend.Silicon | Backend.Carbon =>
         VeyMontTransformation(
           onBeforePassKey = writeOutFunctions(options.outputBeforePass),
-          onAfterPassKey = writeOutFunctions(options.outputAfterPass)
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass),
         )
     }
 }
@@ -296,6 +296,8 @@ case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Veri
   extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
-    StructureCheck
+    StructureCheck,
   ))
 
+
+

src/main/vct/options/Options.scala

@@ -6,6 +6,7 @@ import vct.main.BuildInfo
 import vct.main.stages.Parsing.Language
 import vct.options.types._
 import vct.resources.Resources
+import vct.resources.Resources.getVeymontChannel
 
 import java.nio.file.{Path, Paths}
 import scala.collection.mutable
@@ -387,6 +388,7 @@ case class Options
 
   // VeyMont options
   veymontOutput: Path = null, // required
+  veymontChannel: PathOrStd = PathOrStd.Path(getVeymontChannel),
 
   // VeSUV options
   vesuvOutput: Path = null,

src/main/vct/resources/Resources.scala

@@ -15,4 +15,5 @@ case object Resources {
   def getCcPath: Path = Paths.get("clang")
   def getCPPcPath: Path = Paths.get("clang++")
   def getSystemCConfig: Path = getResource("/systemc/config")
+  def getVeymontChannel: Path = getResource("/include/IntegerChannel.java")
 }

src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala

@@ -92,8 +92,16 @@ case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre]
     if (derefs.isEmpty)
       new VeyMontAssignExpression[Post](succ(receiver), rewriteDefault(a))(a.o)
     else if (derefs.size == 1) {
-      val sender = getAssignmentSender(derefs.head)
-      new VeyMontCommExpression[Post](succ(receiver), succ(sender), rewriteDefault(a))(a.o)
+      val thread = derefs.head.obj match {
+        case t: DerefVeyMontThread[Pre] => t
+        case _ => throw AddVeyMontAssignmentError(a.value, "The value of this assignment is expected to be a Deref of a thread!")
+      }
+      if(thread.ref.decl == receiver)
+        new VeyMontAssignExpression[Post](succ(receiver),rewriteDefault(a))(a.o)
+      else {
+        val sender = getAssignmentSender(derefs.head)
+        new VeyMontCommExpression[Post](succ(receiver), succ(sender), dispatch(derefs.head.ref.decl.t), rewriteDefault(a))(a.o)
+      }
     } else throw AddVeyMontAssignmentError(a.value, "The value of this assignment is not allowed to refer to multiple threads!")
   }
 

src/rewrite/vct/rewrite/veymont/ChannelInfo.scala

@@ -0,0 +1,8 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.{Type, VeyMontCommExpression}
+import vct.col.rewrite.Generation
+
+class ChannelInfo[Pre <: Generation](val comExpr: VeyMontCommExpression[Pre], val channelType: Type[Pre], val channelName: String) {
+
+}

src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala

@@ -0,0 +1,9 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.{Assign, Deref, InstanceField, JavaClass}
+import vct.col.rewrite.{Generation, Rewritten}
+
+class ParallelCommExprBuildingBlocks[Pre <: Generation](val channelField: InstanceField[Rewritten[Pre]], val channelClass: JavaClass[Rewritten[Pre]],
+                                                         val thisChanField: Deref[Rewritten[Pre]], val assign: Assign[Pre] ) {
+
+}