-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1053 from utwente-fmt/veymont-gen-par
Veymont gen par
- Loading branch information
Showing
23 changed files
with
629 additions
and
27 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)(_ <+> "|" <+> _) | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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), | ||
)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) { | ||
|
||
} |
9 changes: 9 additions & 0 deletions
9
src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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] ) { | ||
|
||
} |
Oops, something went wrong.