RASI Generator

build.sc

@@ -402,7 +402,8 @@ object vercors extends Module {
       )
     }
     def deps = Agg(
-      ivy"org.antlr:antlr4-runtime:4.8"
+      ivy"org.antlr:antlr4-runtime:4.8",
+      ivy"org.apache.logging.log4j:log4j-to-slf4j:2.23.1",
     )
     override def moduleDeps = Seq(hre, col, serialize)
     override def bareResourcePaths = T { Seq(vcllvm.compile().path / os.up) }

src/col/vct/col/ast/declaration/cls/InstancePredicateImpl.scala

@@ -15,6 +15,6 @@ trait InstancePredicateImpl[G] extends ClassDeclarationImpl[G] with AbstractPred
 
   override def layout(implicit ctx: Ctx): Doc = Group(
     Doc.rspread(layoutModifiers) <> "resource" <+> ctx.name(this) <> "(" <> Doc.args(args) <> ")" <>
-      body.map(Text(" =") <>> _).getOrElse(Text(";"))
+      body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";"))
   )
 }

src/col/vct/col/ast/declaration/cls/VeSUVMainMethodImpl.scala

@@ -0,0 +1,12 @@
+package vct.col.ast.declaration.cls
+
+import vct.col.ast.VeSUVMainMethod
+import vct.col.print.{Ctx, Doc, Empty, Text}
+import vct.col.ast.ops.VeSUVMainMethodOps
+
+trait VeSUVMainMethodImpl[G] extends VeSUVMainMethodOps[G] { this: VeSUVMainMethod[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      Text("vesuv_entry") <> body.map(Empty <+> _.layoutAsBlock).getOrElse(Text(";")),
+    ))
+}

src/col/vct/col/ast/declaration/global/ClassImpl.scala

@@ -16,7 +16,7 @@ trait ClassImpl[G] extends Declarator[G] with ClassOps[G] { this: Class[G] =>
   def transSupportArrows: Seq[(Class[G], Class[G])] = transSupportArrows(Set.empty)
 
   def layoutLockInvariant(implicit ctx: Ctx): Doc =
-    Text("lock_invariant") <+> intrinsicLockInvariant <+/> Empty
+    Text("lock_invariant") <+> intrinsicLockInvariant <> ";" <+/> Empty
 
   override def layout(implicit ctx: Ctx): Doc =
     (if(intrinsicLockInvariant == tt[G]) Empty else Doc.spec(Show.lazily(layoutLockInvariant(_)))) <>

src/col/vct/col/ast/lang/silver/SilverFieldAssignImpl.scala

@@ -1,10 +1,12 @@
 package vct.col.ast.lang.silver
 
-import vct.col.ast.SilverFieldAssign
+import vct.col.ast.{Expr, SilverFieldAssign}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.SilverFieldAssignOps
 
 trait SilverFieldAssignImpl[G] extends SilverFieldAssignOps[G] { this: SilverFieldAssign[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     obj.bind(Precedence.POSTFIX) <> "." <> ctx.name(field) <+> ":=" <+> value
+
+  override def expr: Expr[G] = this.value
 }

src/col/vct/col/ast/lang/silver/SilverLocalAssignImpl.scala

@@ -1,10 +1,12 @@
 package vct.col.ast.lang.silver
 
-import vct.col.ast.SilverLocalAssign
+import vct.col.ast.{Expr, SilverLocalAssign}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.ast.ops.SilverLocalAssignOps
 
 trait SilverLocalAssignImpl[G] extends SilverLocalAssignOps[G] { this: SilverLocalAssign[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Text(ctx.name(v)) <+> ":=" <+> value
+
+  override def expr: Expr[G] = this.value
 }

src/col/vct/col/ast/statement/behavior/ExpressionContainerStatementImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.statement.behavior
+
+import vct.col.ast.{Expr, ExpressionContainerStatement}
+import vct.col.ast.statement.StatementImpl
+
+trait ExpressionContainerStatementImpl[G] extends StatementImpl[G] { this: ExpressionContainerStatement[G] =>
+  def expr: Expr[G]
+}

src/col/vct/col/ast/statement/exceptional/ReturnImpl.scala

@@ -18,4 +18,6 @@ trait ReturnImpl[G] extends ExceptionalStatementImpl[G] with ReturnOps[G] { this
 
   override def layout(implicit ctx: Ctx): Doc =
     Text("return") <> (if(result == Void[G]()) Text(";") else Empty <+> result <> ";")
+
+  override def expr: Expr[G] = this.result
 }

src/col/vct/col/ast/statement/exceptional/ThrowImpl.scala

@@ -1,10 +1,12 @@
 package vct.col.ast.statement.exceptional
 
-import vct.col.ast.Throw
+import vct.col.ast.{Expr, Throw}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.ast.ops.ThrowOps
 
 trait ThrowImpl[G] extends ThrowOps[G] { this: Throw[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Text("throw") <+> obj <> ";"
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/AssertImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Assert
+import vct.col.ast.{Assert, Expr}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.AssertOps
 
@@ -15,4 +15,6 @@ trait AssertImpl[G] extends AssertOps[G] { this: Assert[G] =>
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/AssumeImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Assume
+import vct.col.ast.{Assume, Expr}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.AssumeOps
 
@@ -15,4 +15,6 @@ trait AssumeImpl[G] extends AssumeOps[G] { this: Assume[G] =>
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.assn
 }

src/col/vct/col/ast/statement/terminal/CommitImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Commit
+import vct.col.ast.{Commit, Expr}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.CommitOps
 
@@ -9,4 +9,6 @@ trait CommitImpl[G] extends CommitOps[G] { this: Commit[G] =>
     Text("commit") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/ExhaleImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Exhale
+import vct.col.ast.{Exhale, Expr}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.ExhaleOps
 
@@ -15,4 +15,6 @@ trait ExhaleImpl[G] extends ExhaleOps[G] { this: Exhale[G] =>
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/FoldImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Fold
+import vct.col.ast.{Expr, Fold}
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.util.CheckFoldUnfoldTarget
 import vct.col.print.{Ctx, Doc, Show, Text}
@@ -17,4 +17,6 @@ trait FoldImpl[G] extends NodeFamilyImpl[G] with CheckFoldUnfoldTarget[G] with F
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/ForkImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Fork
+import vct.col.ast.{Expr, Fork}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.ForkOps
 
@@ -9,4 +9,6 @@ trait ForkImpl[G] extends ForkOps[G] { this: Fork[G] =>
     Text("fork") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/HavocImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Havoc
+import vct.col.ast.{Expr, Havoc}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.HavocOps
 
@@ -9,4 +9,6 @@ trait HavocImpl[G] extends HavocOps[G] { this: Havoc[G] =>
     Text("havoc") <+> loc <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.loc
 }

src/col/vct/col/ast/statement/terminal/InhaleImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Inhale
+import vct.col.ast.{Expr, Inhale}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.InhaleOps
 
@@ -15,4 +15,6 @@ trait InhaleImpl[G] extends InhaleOps[G] { this: Inhale[G] =>
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/JoinImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Join
+import vct.col.ast.{Expr, Join}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.JoinOps
 
@@ -9,4 +9,6 @@ trait JoinImpl[G] extends JoinOps[G] { this: Join[G] =>
     Text("join") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/LockImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Lock
+import vct.col.ast.{Expr, Lock}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.LockOps
 
@@ -9,4 +9,6 @@ trait LockImpl[G] extends LockOps[G] { this: Lock[G] =>
     Text("lock") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/NotifyImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Notify
+import vct.col.ast.{Expr, Notify}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.NotifyOps
 
@@ -9,4 +9,6 @@ trait NotifyImpl[G] extends NotifyOps[G] { this: Notify[G] =>
     Text("notify") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/RefuteImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Refute
+import vct.col.ast.{Expr, Refute}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.RefuteOps
 
@@ -15,4 +15,6 @@ trait RefuteImpl[G] extends RefuteOps[G] { this: Refute[G] =>
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.assn
 }

src/col/vct/col/ast/statement/terminal/SendImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Send
-import vct.col.print.{Ctx, Doc, Show, Text, Group}
+import vct.col.ast.{Expr, Send}
+import vct.col.print.{Ctx, Doc, Group, Show, Text}
 import vct.col.ast.ops.SendOps
 
 trait SendImpl[G] extends SendOps[G] { this: Send[G] =>
@@ -10,4 +10,6 @@ trait SendImpl[G] extends SendOps[G] { this: Send[G] =>
 
   override def layout(implicit ctx: Ctx): Doc =
     Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/UnfoldImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Unfold
+import vct.col.ast.{Expr, Unfold}
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.util.CheckFoldUnfoldTarget
 import vct.col.print.{Ctx, Doc, Show, Text}
@@ -17,4 +17,6 @@ trait UnfoldImpl[G] extends NodeFamilyImpl[G] with CheckFoldUnfoldTarget[G] with
     case Ctx.Silver => layoutSilver
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/terminal/UnlockImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Unlock
+import vct.col.ast.{Expr, Unlock}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.UnlockOps
 
@@ -9,4 +9,6 @@ trait UnlockImpl[G] extends UnlockOps[G] { this: Unlock[G] =>
     Text("unlock") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/WaitImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.Wait
+import vct.col.ast.{Expr, Wait}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.WaitOps
 
@@ -9,4 +9,6 @@ trait WaitImpl[G] extends WaitOps[G] { this: Wait[G] =>
     Text("wait") <+> obj <> ";"
 
   override def layout(implicit ctx: Ctx): Doc = Doc.inlineSpec(Show.lazily(layoutSpec(_)))
+
+  override def expr: Expr[G] = this.obj
 }

src/col/vct/col/ast/statement/terminal/WandApplyImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.statement.terminal
 
-import vct.col.ast.WandApply
+import vct.col.ast.{Expr, WandApply}
 import vct.col.print.{Ctx, Doc, Show, Text}
 import vct.col.ast.ops.WandApplyOps
 
@@ -12,4 +12,6 @@ trait WandApplyImpl[G] extends WandApplyOps[G] { this: WandApply[G] =>
     case Ctx.Silver => Text("apply") <+> res
     case _ => Doc.inlineSpec(Show.lazily(layoutSpec(_)))
   }
+
+  override def expr: Expr[G] = this.res
 }

src/col/vct/col/ast/statement/veymont/PVLSeqAssignImpl.scala

@@ -1,10 +1,12 @@
 package vct.col.ast.statement.veymont
 
-import vct.col.ast.PVLSeqAssign
+import vct.col.ast.{Expr, PVLSeqAssign}
 import vct.col.print.{Ctx, Doc, Group, Text}
 import vct.col.ast.ops.PVLSeqAssignOps
 
 trait  PVLSeqAssignImpl[G] extends PVLSeqAssignOps[G] { this: PVLSeqAssign[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     Group(Text(receiver.decl.name) <> "." <> ctx.name(field) <+> ":=" <+> value.show)
+
+  override def expr: Expr[G] = this.value
 }