Merge pull request #1221 from utwente-fmt/rasi_generator

Rasi generator

src/col/vct/col/ast/expr/apply/InstancePredicateApplyImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr.apply
 
-import vct.col.ast.InstancePredicateApply
+import vct.col.ast.{InstancePredicateApply, WritePerm}
 import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
 import vct.col.ast.ops.InstancePredicateApplyOps
 

src/col/vct/col/ast/expr/apply/PredicateApplyImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr.apply
 
-import vct.col.ast.PredicateApply
+import vct.col.ast.{PredicateApply, WritePerm}
 import vct.col.print.{Ctx, Doc, DocUtil, Empty, Group, Precedence, Text}
 import vct.col.ast.ops.PredicateApplyOps
 

src/main/vct/main/modes/VeSUV.scala

@@ -14,7 +14,9 @@ case object VeSUV extends LazyLogging {
     val stages = Stages
       .vesuvOfOptions(options, ConstantBlameProvider(collector))
     stages.run(options.inputs) match {
-      case Left(_: UserError) => EXIT_CODE_ERROR
+      case Left(err: UserError) =>
+        logger.error(err.text)
+        EXIT_CODE_ERROR
       case Left(err: SystemError) => throw err
       case Right(()) =>
         logger.info("Transformation complete")

src/main/vct/main/stages/Backend.scala

@@ -57,6 +57,7 @@ case object Backend {
               options.siliconPrintQuantifierStats.isDefined,
             reportOnNoProgress = options.devSiliconReportOnNoProgress,
             traceBranchConditions = options.devSiliconTraceBranchConditions,
+            optimizeUnsafe = options.devUnsafeOptimization,
             branchConditionReportInterval =
               options.devSiliconBranchConditionReportInterval,
             options = options.backendFlags,

src/main/vct/main/stages/GenerateRASI.scala

@@ -1,7 +1,24 @@
 package vct.main.stages
 
+import com.typesafe.scalalogging.LazyLogging
+import hre.io.LiteralReadable
 import hre.stages.Stage
-import vct.col.ast.{InstanceField, InstanceMethod, InstancePredicate, Node}
+import vct.col.ast.{
+  Declaration,
+  Deref,
+  Expr,
+  InstanceField,
+  InstanceMethod,
+  InstancePredicate,
+  Node,
+  Predicate,
+  Procedure,
+  Program,
+  Verification,
+  VerificationContext,
+}
+import vct.col.origin.{LabelContext, Origin, PreferredName}
+import vct.col.print.Ctx
 import vct.col.rewrite.Generation
 import vct.options.Options
 import vct.rewrite.rasi.{
@@ -12,16 +29,26 @@ import vct.rewrite.rasi.{
   SizeVariable,
 }
 
-import java.nio.file.Path
+import java.nio.charset.StandardCharsets
+import java.nio.file.{Files, Path}
 
 case object GenerateRASI {
   def ofOptions(options: Options): Stage[Node[_ <: Generation], Unit] = {
-    GenerateRASI(options.vesuvRasiVariables, options.vesuvOutput)
+    GenerateRASI(
+      options.vesuvRasiVariables,
+      options.vesuvRasiSplitVariables,
+      options.vesuvOutput,
+      test = options.vesuvRasiTest,
+    )
   }
 }
 
-case class GenerateRASI(vars: Option[Seq[String]], out: Path)
-    extends Stage[Node[_ <: Generation], Unit] {
+case class GenerateRASI(
+    vars: Option[Seq[String]],
+    split: Option[Seq[String]],
+    out: Path,
+    test: Boolean,
+) extends Stage[Node[_ <: Generation], Unit] with LazyLogging {
 
   override def friendlyName: String =
     "Generate reachable abstract states invariant"
@@ -31,16 +58,65 @@ case class GenerateRASI(vars: Option[Seq[String]], out: Path)
   override def run(in1: Node[_ <: Generation]): Unit = {
     val in = in1.asInstanceOf[Node[Generation]]
     val main_method =
-      in.collectFirst {
-        case m: InstanceMethod[_]
-            if m.o.getPreferredName.get.snake.equals("main") =>
-          m
-      }.get
+      in.collectFirst { case m: Procedure[_] if m.vesuv_entry => m }.get
     val variables: Set[ConcreteVariable[Generation]] =
       vars.getOrElse(Seq()).map(s => resolve_variable(in, s)).toSet
+    val split_on_variables: Option[Set[ConcreteVariable[Generation]]] = split
+      .map(seq => seq.map(s => resolve_variable(in, s)).toSet)
     val parameter_invariant: InstancePredicate[Generation] =
       get_parameter_invariant(in)
-    new RASIGenerator().test(main_method, variables, parameter_invariant, out)
+    if (test) {
+      new RASIGenerator().test(main_method, variables, parameter_invariant, out)
+    } else {
+      val rasis: Seq[(String, Expr[Generation])] = new RASIGenerator().execute(
+        main_method,
+        variables,
+        split_on_variables,
+        parameter_invariant,
+        in,
+      )
+      val predicates: Seq[Predicate[Generation]] = rasis
+        .map(t => rasi_predicate(t._1, t._2))
+      implicit val o: Origin = Origin(Seq(LabelContext("rasi-generation")))
+      val verification: Verification[Generation] = Verification(
+        Seq(VerificationContext(Program(predicates)(o))),
+        Seq(),
+      )
+
+      val name_map: Map[Declaration[_], String] = Map
+        .from(predicates.flatMap(p =>
+          p.collect {
+            case Deref(_, ref) =>
+              ref.decl -> ref.decl.o.getPreferredName.get.snake
+            case p: Predicate[_] => p -> p.o.getPreferredName.get.snake
+          }
+        ))
+      print(verification, name_map)
+    }
+  }
+
+  private def rasi_predicate(
+      name: String,
+      rasi: Expr[Generation],
+  ): Predicate[Generation] = {
+    implicit val o: Origin = Origin(Seq(LabelContext("rasi-generation")))
+      .withContent(PreferredName(Seq(name)))
+    new Predicate(Seq(), Some(rasi), threadLocal = false, inline = true)
+  }
+
+  private def print(
+      in: Verification[_ <: Generation],
+      name_map: Map[Declaration[_], String],
+  ): Unit = {
+    val ctx = Ctx(syntax = Ctx.PVL, names = name_map)
+
+    val buf = new StringBuffer()
+    in.write(buf)(ctx)
+    val path = s"invariant.pvl"
+    val txt = LiteralReadable(path, buf.toString)
+
+    logger.info(s"Writing ${txt.fileName} to $out")
+    Files.write(out, txt.data.getBytes(StandardCharsets.UTF_8))
   }
 
   private def resolve_variable(

src/main/vct/main/stages/Output.scala

@@ -2,9 +2,15 @@ package vct.main.stages
 
 import com.typesafe.scalalogging.LazyLogging
 import hre.io.{LiteralReadable, Readable}
-import hre.stages.{Stage, Stages}
-import vct.col.ast.{Declaration, Node, Program, Verification}
-import vct.col.origin.DiagnosticOrigin
+import hre.stages.{FunctionStage, Stage, Stages}
+import vct.col.ast.{
+  Declaration,
+  Node,
+  Program,
+  Verification,
+  VerificationContext,
+}
+import vct.col.origin.{DiagnosticOrigin, Origin}
 import vct.col.print.{Ctx, Namer}
 import vct.col.rewrite.{Generation, InitialGeneration}
 import vct.options.Options
@@ -22,9 +28,19 @@ case object Output {
   def vesuvOfOptions[G <: Generation](
       options: Options
   ): Stages[ParseResult[G], Unit] = {
-//    FunctionStage((pr: ParseResult[_ <: Generation]) => Program(pr.decls)(DiagnosticOrigin)(DiagnosticOrigin))
-//      .thenRun(??? /* Output(options.vesuvOutput, Ctx.PVL) */)
-    ???
+    implicit val o: Origin = DiagnosticOrigin
+    FunctionStage((pr: ParseResult[_ <: Generation]) =>
+      Verification(
+        Seq(VerificationContext(Program(pr.decls)(DiagnosticOrigin))),
+        Seq(),
+      )
+    ).thenRun(Output(
+      Some(options.vesuvOutput),
+      Ctx.PVL,
+      Files.isDirectory(options.vesuvOutput),
+    )).thenRun(FunctionStage((_: Seq[LiteralReadable]) =>
+        ()
+      )) // TODO: Not the prettiest, but I have no time for this. I blame Bob.
   }
 
   def veymontOfOptions(
@@ -63,9 +79,9 @@ case class Output(out: Option[Path], syntax: Ctx.Syntax, splitDecls: Boolean)
 
     val txts: Seq[LiteralReadable] =
       if (splitDecls) {
-        in.asInstanceOf[Program[_]].declarations.zipWithIndex.map {
+        in.tasks.map(t => t.program).flatMap(p => p.declarations).zipWithIndex.map {
           case (decl, i) =>
-            val name = names.getOrElse(decl.asInstanceOf, s"unknown$i")
+            val name = names.getOrElse(decl.asInstanceOf[Declaration[Generation]], s"unknown$i")
             val fileName = s"${name}.${extension(syntax)}"
             val buf = new StringBuffer()
             decl.write(buf)(ctx)

src/main/vct/main/stages/PrintCFG.scala

@@ -1,7 +1,7 @@
 package vct.main.stages
 
 import hre.stages.Stage
-import vct.col.ast.{InstanceMethod, Node}
+import vct.col.ast.{Node, Procedure}
 import vct.col.rewrite.Generation
 import vct.options.Options
 import vct.rewrite.cfg.CFGPrinter
@@ -21,11 +21,10 @@ case class PrintCFG(out: Path) extends Stage[Node[_ <: Generation], Unit] {
   override def progressWeight: Int = 0
 
   override def run(in1: Node[_ <: Generation]): Unit = {
-    // TODO: Is there a better way to find a "main" method?
     val main_method =
       in1.collectFirst {
-        case m: InstanceMethod[_]
-            if m.o.getPreferredName.get.snake.equals("main") =>
+        case m: Procedure[_]
+            if m.vesuv_entry =>
           m
       }.get
     CFGPrinter().print_ast_as_cfg(main_method, out)

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

@@ -148,6 +148,7 @@ object Transformation extends LazyLogging {
           bipResults = bipResults,
           splitVerificationByProcedure =
             options.devSplitVerificationByProcedure,
+          optimizeUnsafe = options.devUnsafeOptimization,
           veymontGeneratePermissions = options.veymontGeneratePermissions,
         )
     }
@@ -189,10 +190,14 @@ object Transformation extends LazyLogging {
   *   Execute a handler before/after a pass is executed.
   * @param passes
   *   The list of rewrite passes to execute.
+  * @param optimizeUnsafe
+  *   Flag indicating to not do typechecking in-between passes to save
+  *   performance
   */
 class Transformation(
     val onPassEvent: Seq[PassEventHandler],
     val passes: Seq[RewriterBuilder],
+    val optimizeUnsafe: Boolean = false,
 ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]]
     with LazyLogging {
   override def friendlyName: String = "Transformation"
@@ -236,11 +241,12 @@ class Transformation(
           action(passes, Transformation.after, pass.key, result)
         }
 
-        result.tasks.map(_.program)
-          .flatMap(program => program.check.map(program -> _)) match {
-          case Nil => // ok
-          case errors => throw TransformationCheckError(pass, errors)
-        }
+        if (!optimizeUnsafe)
+          result.tasks.map(_.program)
+            .flatMap(program => program.check.map(program -> _)) match {
+            case Nil => // ok
+            case errors => throw TransformationCheckError(pass, errors)
+          }
 
         result = PrettifyBlocks().dispatch(result)
       }
@@ -293,6 +299,7 @@ case class SilverTransformation(
     bipResults: BIP.VerificationResults,
     checkSat: Boolean = true,
     splitVerificationByProcedure: Boolean = false,
+    override val optimizeUnsafe: Boolean = false,
     veymontGeneratePermissions: Boolean = false,
 ) extends Transformation(
       onPassEvent,
@@ -433,6 +440,7 @@ case class SilverTransformation(
         PinSilverNodes,
         Explode.withArg(splitVerificationByProcedure),
       ),
+      optimizeUnsafe = optimizeUnsafe,
     )
 
 case class VeyMontImplementationGeneration(

src/main/vct/options/Options.scala

@@ -244,6 +244,9 @@ case object Options {
         "Indicate, in seconds, the timeout value for the backend verification. If the verification gets stuck " +
           "for longer than this timeout, the verification will timeout."
       ),
+      opt[Unit]("dev-unsafe-optimization").maybeHidden()
+        .action((_, c) => c.copy(devUnsafeOptimization = true))
+        .text("Optimizes runtime at the cost of progress logging and readability of error messages"),
       opt[Path]("dev-silicon-z3-log-file").maybeHidden()
         .action((p, c) => c.copy(devSiliconZ3LogFile = Some(p)))
         .text("Path for z3 to write smt2 log file to"),
@@ -326,11 +329,20 @@ case object Options {
           .action((_, c) => c.copy(vesuvGenerateRasi = true)).text(
             "Instead of transforming a SystemC design to PVL, generate a global invariant for a PVL program"
           ).children(
+            opt[Unit]("rasi-graph-output")
+              .action((_, c) => c.copy(vesuvRasiTest = true)).text(
+                "Output RASI graph to test the algorithm rather than outputting the invariant"
+              ),
             opt[Seq[String]]("rasi-vars").valueName("<var1>,...")
               .action((vars, c) => c.copy(vesuvRasiVariables = Some(vars)))
               .text(
                 "[WIP] Preliminary selection mechanism for RASI variables; might be replaced later"
-              )
+              ),
+            opt[Seq[String]]("split-rasi").valueName("<var1>,...")
+              .action((vars, c) => c.copy(vesuvRasiSplitVariables = Some(vars)))
+              .text(
+                "[WIP] Preliminary selection mechanism for localizing the RASI based on certain variables; might be changed later"
+              ),
           ),
       ),
       note(""),
@@ -433,6 +445,7 @@ case class Options(
     devSiliconTraceBranchConditions: Boolean = false,
     devCarbonBoogieLogFile: Option[Path] = None,
     devViperProverLogFile: Option[Path] = None,
+    devUnsafeOptimization: Boolean = false,
 
     // VeyMont options
     veymontOutput: Option[Path] = None,
@@ -444,7 +457,9 @@ case class Options(
     // VeSUV options
     vesuvOutput: Path = null,
     vesuvGenerateRasi: Boolean = false,
+    vesuvRasiTest: Boolean = false,
     vesuvRasiVariables: Option[Seq[String]] = None,
+    vesuvRasiSplitVariables: Option[Seq[String]] = None,
 
     // Control flow graph options
     cfgOutput: Path = null,