From f36c2ba2d4ee979f98c7fd87326c99f95f6710f4 Mon Sep 17 00:00:00 2001 From: Petra van den Bos Date: Thu, 13 Jul 2023 17:26:15 +0200 Subject: [PATCH] VeyMont produces output --- src/main/vct/main/modes/VeyMont.scala | 2 +- src/main/vct/main/stages/CodeGeneration.scala | 67 +++++++++++++++++++ src/main/vct/main/stages/Stages.scala | 5 +- src/main/vct/main/stages/Transformation.scala | 9 ++- .../veymont/ParalleliseVeyMontThreads.scala | 2 +- 5 files changed, 76 insertions(+), 9 deletions(-) create mode 100644 src/main/vct/main/stages/CodeGeneration.scala diff --git a/src/main/vct/main/modes/VeyMont.scala b/src/main/vct/main/modes/VeyMont.scala index c9405ebe20..cb51f3a472 100644 --- a/src/main/vct/main/modes/VeyMont.scala +++ b/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) diff --git a/src/main/vct/main/stages/CodeGeneration.scala b/src/main/vct/main/stages/CodeGeneration.scala new file mode 100644 index 0000000000..0e350061f2 --- /dev/null +++ b/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), + )) diff --git a/src/main/vct/main/stages/Stages.scala b/src/main/vct/main/stages/Stages.scala index cc7155ebda..2be2b1151a 100644 --- a/src/main/vct/main/stages/Stages.scala +++ b/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)) } diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index ad04613619..11131f15ef 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -65,13 +65,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), - channelClass = Util.loadJavaClass(options.veymontChannel), ) } } @@ -289,12 +288,12 @@ case class SilverTransformation )) case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, - override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil, - val channelClass: JavaClass[_]) + override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil) extends Transformation(onBeforePassKey, onAfterPassKey, Seq( AddVeyMontAssignmentNodes, AddVeyMontConditionNodes, StructureCheck, - ParalleliseVeyMontThreads.withArg(channelClass), )) + + diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala index a109e8adec..99158fa3ec 100644 --- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala +++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala @@ -158,7 +158,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[ } override def dispatch(decl: Declaration[Pre]): Unit = decl match { - case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType))) //TODO: deze rewrite verwijderd de constructor.. + case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType))) case other => rewriteDefault(other) } }