Parser changes for documentation generator

silver.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+BASEDIR="$(realpath "$(dirname "$0")")"
+
+CP_FILE="$BASEDIR/silver_classpath.txt"
+
+if [ ! -f "$CP_FILE" ]; then
+    (cd "$BASEDIR"; sbt "export runtime:dependencyClasspath" | tail -n1 > "$CP_FILE")
+fi
+
+exec java -cp "$(cat "$CP_FILE")" viper.silver.SilverRunner "$@"

src/main/scala/viper/silver/SilverRunner.scala

@@ -0,0 +1,28 @@
+package viper.silver
+
+
+import scala.collection.immutable.ArraySeq
+import viper.silver.frontend.DefaultStates 
+import viper.silver.frontend.ViperAstProvider
+import viper.silver.logger.SilentLogger
+import viper.silver.reporter.NoopReporter
+
+
+object SilverRunner extends SilverRunnerInstance {
+  def main(args: Array[String]): Unit = {
+    runMain(args)
+  }
+}
+
+class SilverRunnerInstance extends ViperAstProvider(NoopReporter, SilentLogger().get) {
+  def runMain(args: Array[String]): Unit = {
+    var exitCode = 1 /* Only 0 indicates no error */
+
+    execute(ArraySeq.unsafeWrapArray(args))
+
+    if (state >= DefaultStates.Translation) {
+      exitCode = 0
+    }
+    sys.exit(exitCode)
+  }
+}

src/main/scala/viper/silver/parser/FastParser.scala

@@ -33,7 +33,7 @@ object FastParserCompanion {
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((("/*" ~ (!"*/" ~ AnyChar).rep ~ "*/") | ((("//" ~ !("/")) | "////") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
@@ -312,14 +312,7 @@ class FastParser {
   //////////////////////////
 
   import fastparse._
-  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym}
-
-
-  implicit val whitespace = {
-    import NoWhitespace._
-    implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-  }
+  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym, whitespace}
 
   implicit val lineCol: LineCol = new LineCol(this)
 
@@ -403,7 +396,11 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
-  def annotation[$: P]: P[PAnnotation] = P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
+  def docString[$: P]: P[PRawString] = P(CharsWhile(_ != '\n', 0).! map PRawString.apply).pos
+
+  def docAnnotation[$: P]: P[PAnnotation] = P(P(PSym.TripleSlash) ~~ docString).map{ case (s, d) => p => PDocAnnotation(s, d)(p) }.pos
+
+  def annotation[$: P]: P[PAnnotation] = P(P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAtAnnotation.apply _).tupled).pos | docAnnotation)
 
   def annotated[$: P, T](inner: => P[PAnnotationsPosition => T]): P[T] = P((annotation.rep(0) ~ inner).map {
     case (annotations, i) => pos: Pos => i(PAnnotationsPosition(annotations, pos))
@@ -486,7 +483,7 @@ class FastParser {
 
   def suffixExpr[$: P](bracketed: Boolean = false): P[PExp] = P((atomParen(bracketed) ~~~ suffix.lw.rep).map { case (fac, ss) => foldPExp(fac, ss) })
 
-  def termOp[$: P] = P(reservedSymMany(None, StringIn("*", "/", "\\", "%"), _ match {
+  def termOp[$: P] = P(reservedSymMany(None, !("///") ~ StringIn("*", "/", "\\", "%"), _ match {
     case "*" => PSymOp.Mul
     case "/" => PSymOp.Div
     case "\\" => PSymOp.ArithDiv
@@ -807,9 +804,15 @@ class FastParser {
     P((P(PKw.Else) ~ stmtBlock()) map (PElse.apply _).tupled).pos
 
   def whileStmt[$: P]: P[PKw.While => Pos => PWhile] =
-    P((parenthesizedExp ~~ semiSeparated(invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
+    P((parenthesizedExp ~~ semiSeparated(annotatedInvariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
 
-  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] = P((P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
+  def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: Pos =>
+            PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
+
+  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    P((P(PKw.Invariant) ~ exp).map{ case (kw, e) => p: Pos =>
+      PSpecification[PKw.InvSpec](kw, e)(p) }.pos | ParserExtension.invSpecification(ctx))
 
   def localVars[$: P]: P[PKw.Var => Pos => PVars] =
     P((nonEmptyIdnTypeList(PLocalVarDecl(_)) ~~~ (P(PSymOp.Assign) ~ exp).lw.?) map { case (a, i) => PVars(_, a, i) })
@@ -824,7 +827,7 @@ class FastParser {
   def goto[$: P]: P[PKw.Goto => Pos => PGoto] = P(idnref[$, PLabel] map { i => PGoto(_, i) _ })
 
   def label[$: P]: P[PKw.Label => Pos => PLabel] =
-    P((idndef ~~ semiSeparated(invariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
+    P((idndef ~~ semiSeparated(annotatedInvariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
 
   def packageWand[$: P]: P[PKw.Package => Pos => PPackageWand] =
     P((magicWandExp() ~~~ stmtBlock().lw.?) map { case (wand, proof) => PPackageWand(_, wand, proof) _ })
@@ -915,23 +918,34 @@ class FastParser {
   })
 
   def functionDecl[$: P]: P[PKw.Function => PAnnotationsPosition => PFunction] = P((idndef ~ argList(formalArg) ~ PSym.Colon ~ typ
-    ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ bracedExp.lw.?
+    ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ bracedExp.lw.?
   ) map { case (idn, args, c, typ, d, e, f) => k =>
       ap: PAnnotationsPosition => PFunction(ap.annotations, k, idn, args, c, typ, d, e, f)(ap.pos)
   })
 
+  def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: Pos =>
+            PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
+
+  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    P((P(PKw.Requires) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+        PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
 
-  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] = P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx))
+  def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: Pos =>
+      PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
 
-  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] = P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx))
+  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    P((P(PKw.Ensures) ~ exp).map{ case (kw, e) => p: Pos =>
+        PSpecification[PKw.PostSpec](kw, e)(p)}.pos | ParserExtension.postSpecification(ctx))
 
   def predicateDecl[$: P]: P[PKw.Predicate => PAnnotationsPosition => PPredicate] = P(idndef ~ argList(formalArg) ~~~ bracedExp.lw.?).map {
     case (idn, args, c) => k =>
       ap: PAnnotationsPosition => PPredicate(ap.annotations, k, idn, args, c)(ap.pos)
   }
 
   def methodDecl[$: P]: P[PKw.Method => PAnnotationsPosition => PMethod] =
-    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ stmtBlock().lw.?) map {
+    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ stmtBlock().lw.?) map {
         case (idn, args, rets, pres, posts, body) => k =>
           ap: PAnnotationsPosition => PMethod(ap.annotations, k, idn, args, rets, pres, posts, body)(ap.pos)
     })

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -1668,7 +1668,7 @@ case class PFields(annotations: Seq[PAnnotation], field: PKw.Field, fields: PDel
   override def declares: Seq[PGlobalDeclaration] = fields.toSeq
 }
 
-case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp)(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp, annotations: Seq[PAnnotation] = Seq())(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
   override def pretty: String = "\n  " + super.pretty
 }
 
@@ -1694,10 +1694,15 @@ case class PMethodReturns(k: PKw.Returns, formalReturns: PGrouped.Paren[PDelimit
   */
 case class PAnnotationsPosition(annotations: Seq[PAnnotation], pos: (FilePosition, FilePosition))
 
-case class PAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+sealed trait PAnnotation extends PNode with PPrettySubnodes {
+  def key: PRawString
   override def pretty: String = super.pretty + "\n"
 }
 
+case class PAtAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PAnnotation with PPrettySubnodes {}
+
+case class PDocAnnotation(tripleSlash: PSym.TripleSlash, docString: PRawString, key: PRawString = PRawString("doc")(NoPosition, NoPosition))(val pos: (Position, Position)) extends PAnnotation {}
+
 // Any unenclosed string (e.g. `hello`)
 case class PRawString(str: String)(val pos: (Position, Position)) extends PNode with PLeaf {
   override def display: String = str

src/main/scala/viper/silver/parser/ParseAstKeyword.scala

@@ -321,6 +321,9 @@ object PSym {
   // Used for annotations
   case object At extends PSym("@") with PSymbolLang
   type At = PReserved[At.type]
+  // Used for documentation
+  case object TripleSlash extends PSym("///") with PSymbolLang
+  type TripleSlash = PReserved[TripleSlash.type]
   // Used for `new(*)`
   case object Star extends PSym("*") with PSymbolLang
   type Star = PReserved[Star.type]

src/main/scala/viper/silver/parser/Translator.scala

@@ -81,7 +81,9 @@ case class Translator(program: PProgram) {
 
       val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn])
 
-      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT)
+      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               body = newBody)(m.pos, m.info, m.errT)
 
       members(m.name) = finalMethod
 
@@ -107,7 +109,9 @@ case class Translator(program: PProgram) {
   private def translate(f: PFunction): Function = f match {
     case PFunction(_, _, idndef, _, _, _, pres, posts, body) =>
       val f = findFunction(idndef)
-      val ff = f.copy( pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
+      val ff = f.copy( pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
       members(f.name) = ff
       ff
   }
@@ -232,7 +236,8 @@ case class Translator(program: PProgram) {
         }) getOrElse Statements.EmptyStmt)(pos, info)
       case PElse(_, els) => stmt(els)
       case PWhile(_, cond, invs, body) =>
-        While(exp(cond.inner), invs.toSeq map (inv => exp(inv.e)), stmt(body).asInstanceOf[Seqn])(pos, info)
+        While(exp(cond.inner), invs.toSeq map (inv => exp(wrapAnnotations(inv.annotations, inv.e)(inv.pos))),
+              stmt(body).asInstanceOf[Seqn])(pos, info)
       case PQuasihavoc(_, lhs, e) =>
         val (newLhs, newE) = havocStmtHelper(lhs, e)
         Quasihavoc(newLhs, newE)(pos, info)
@@ -313,16 +318,33 @@ case class Translator(program: PProgram) {
     }
   }
 
+  def wrapAnnotations(annotations: Seq[PAnnotation], pexp: PExp)(pos: (Position, Position)): PExp =
+    annotations.foldRight(pexp) { (ann, e) => new PAnnotatedExp(ann, e)(pos) }
+
   def extractAnnotation(pexp: PExp): (PExp, Map[String, Seq[String]]) = {
     pexp match {
       case PAnnotatedExp(ann, e) =>
         val (resPexp, innerMap) = extractAnnotation(e)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPexp, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPexp, innerMap.updated(key, combinedValue))
       case _ => (pexp, Map())
     }
   }
@@ -331,12 +353,26 @@ case class Translator(program: PProgram) {
     pStmt match {
       case PAnnotatedStmt(ann, s) =>
         val (resPStmt, innerMap) = extractAnnotationFromStmt(s)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPStmt, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPStmt, innerMap.updated(key, combinedValue))
       case _ => (pStmt, Map())
     }
   }
@@ -723,7 +759,9 @@ object Translator {
     if (annotations.isEmpty) {
       NoInfo
     } else {
-      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap(_.values.inner.toSeq.map(_.str)) })
+      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap{
+                         case a: PAtAnnotation => a.values.inner.toSeq.map(_.str)
+                         case a: PDocAnnotation => Seq(a.docString.str) }})
     }
   }
 }