Merge pull request #249 from LaurenzV/format-rnode

Add reformatter capabilities

Author: rayman2000

README.md

@@ -37,6 +37,7 @@ For more details about using Viper, please visit: http://viper.ethz.ch/downloads
 ### Running Tests ###
 
 * Set the environment variable ```Z3_EXE``` to an executable of a recent version of [Z3](https://github.com/Z3Prover/z3).
+* Set the environment variable ```BOOGIE_EXE``` to an executable of a recent version of [Boogie](https://github.com/viperproject/boogie-builder)
 
 * Run the following command: ```sbt test```.
 

src/main/scala/viper/server/core/AstWorker.scala

@@ -8,7 +8,7 @@ package viper.server.core
 
 import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
-import viper.server.utility.AstGenerator
+import viper.server.utility.ViperAstGenerator
 import viper.server.vsi.AstConstructionException
 import viper.silver.ast.Program
 import viper.silver.ast.utility.FileLoader
@@ -35,7 +35,7 @@ class AstWorker(val file: String,
   private def constructAst(args: Seq[String]): Option[Program] = {
 
     val reporter = new ActorReporter("AstGenerationReporter")
-    val astGen = new AstGenerator(logger, reporter, args, disablePlugins = config.disablePlugins())
+    val astGen = new ViperAstGenerator(logger, reporter, args, disablePlugins = config.disablePlugins())
 
     val ast_option: Option[Program] = try {
       astGen.generateViperAst(file, loader)
@@ -50,7 +50,7 @@ class AstWorker(val file: String,
         throw AstConstructionInterrupted
       case e: Throwable =>
         reporter report ExceptionReport(e)
-        logger.error(s"Creation/Execution of an AstGenerator instance ($file) resulted in $e.")
+        logger.error(s"Creation/Execution of a ViperAstGenerator instance ($file) resulted in $e.")
         registerTaskEnd(false)
         throw ServerCrashException(e)
     }

src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala

@@ -150,7 +150,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     Future.sequence(tasks).map(_ => {
       logger.debug("all running verifications have been stopped")
     })
-  }
+}
 
   /** returns true if verification was started */
   def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Future[Boolean] = {

src/main/scala/viper/server/frontends/lsp/DataProtocol.scala

@@ -87,6 +87,8 @@ case class VerifyParams (
               backend: String,
               customArgs: String)            // contains the path of the file that should be verified
 
+case class ReformatParams (uri: String)
+
 case class SettingsError (errorType: SettingsErrorType, msg: String)
 
 case class Stage(

src/main/scala/viper/server/frontends/lsp/Receiver.scala

@@ -23,6 +23,7 @@ import scala.language.postfixOps
 
 trait StandardReceiver {
   val coordinator: ClientCoordinator
+
   implicit def executor: VerificationExecutionContext
 }
 
@@ -41,11 +42,11 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     // Find References:
     capabilities.setReferencesProvider(true)
     // Prepare Call Hierarchy:  [N/A]
-      // Incoming Calls:        [N/A]
-      // Outgoing Calls:        [N/A]
+    // Incoming Calls:        [N/A]
+    // Outgoing Calls:        [N/A]
     // Prepare Type Hierarchy:  [N/A]
-      // Super Types:           [N/A]
-      // Sub Types:             [N/A]
+    // Super Types:           [N/A]
+    // Sub Types:             [N/A]
     // Document Highlight:
     capabilities.setDocumentHighlightProvider(true)
     // Document Link (disabled Resolve):
@@ -57,21 +58,21 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     // Folding Range:
     capabilities.setFoldingRangeProvider(true)
     // Selection Range:         [N/A]
-        // could try extracting from document symbols,
-        // but this req doesn't seem to ever be sent
+    // could try extracting from document symbols,
+    // but this req doesn't seem to ever be sent
     // Document Symbols:
     capabilities.setDocumentSymbolProvider(true)
     // Semantic Tokens:
     val legend = new SemanticTokensLegend(
       Seq(SemanticTokenTypes.Namespace, SemanticTokenTypes.Type, SemanticTokenTypes.Class, SemanticTokenTypes.Enum,
-          SemanticTokenTypes.Interface, SemanticTokenTypes.Struct, SemanticTokenTypes.TypeParameter, SemanticTokenTypes.Parameter,
-          SemanticTokenTypes.Variable, SemanticTokenTypes.Property, SemanticTokenTypes.EnumMember, SemanticTokenTypes.Event,
-          SemanticTokenTypes.Function, SemanticTokenTypes.Method, SemanticTokenTypes.Macro, SemanticTokenTypes.Keyword,
-          SemanticTokenTypes.Modifier, SemanticTokenTypes.Comment, SemanticTokenTypes.String, SemanticTokenTypes.Number,
-          SemanticTokenTypes.Regexp, SemanticTokenTypes.Operator, SemanticTokenTypes.Decorator, "constant").asJava,
+        SemanticTokenTypes.Interface, SemanticTokenTypes.Struct, SemanticTokenTypes.TypeParameter, SemanticTokenTypes.Parameter,
+        SemanticTokenTypes.Variable, SemanticTokenTypes.Property, SemanticTokenTypes.EnumMember, SemanticTokenTypes.Event,
+        SemanticTokenTypes.Function, SemanticTokenTypes.Method, SemanticTokenTypes.Macro, SemanticTokenTypes.Keyword,
+        SemanticTokenTypes.Modifier, SemanticTokenTypes.Comment, SemanticTokenTypes.String, SemanticTokenTypes.Number,
+        SemanticTokenTypes.Regexp, SemanticTokenTypes.Operator, SemanticTokenTypes.Decorator, "constant").asJava,
       Seq(SemanticTokenModifiers.Declaration, SemanticTokenModifiers.Definition, SemanticTokenModifiers.Readonly, SemanticTokenModifiers.Static,
-          SemanticTokenModifiers.Deprecated, SemanticTokenModifiers.Abstract, SemanticTokenModifiers.Async, SemanticTokenModifiers.Modification,
-          SemanticTokenModifiers.Documentation, SemanticTokenModifiers.DefaultLibrary, "controlFlow").asJava
+        SemanticTokenModifiers.Deprecated, SemanticTokenModifiers.Abstract, SemanticTokenModifiers.Async, SemanticTokenModifiers.Modification,
+        SemanticTokenModifiers.Documentation, SemanticTokenModifiers.DefaultLibrary, "controlFlow").asJava
     )
     capabilities.setSemanticTokensProvider(new SemanticTokensWithRegistrationOptions(legend, true))
     // Inline Value:            [N/A]
@@ -83,7 +84,7 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     // Pull Diagnostics:        DISABLED (we use `publishDiagnostics` instead)
     // capabilities.setDiagnosticProvider(new DiagnosticRegistrationOptions(true, false))
     // Signature Help:
-        // Allow a `,` to try and restart the signature help even after it has ended
+    // Allow a `,` to try and restart the signature help even after it has ended
     capabilities.setSignatureHelpProvider(new SignatureHelpOptions(Seq("(", ",").asJava, Seq().asJava))
     // Code Action:
     capabilities.setCodeActionProvider(true)
@@ -102,6 +103,8 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     // automatically cause all references to be renamed. This would probably be too annoying.
     capabilities.setLinkedEditingRangeProvider(false)
 
+    capabilities.setDocumentFormattingProvider(true)
+
     CompletableFuture.completedFuture(new InitializeResult(capabilities))
   }
 
@@ -191,7 +194,7 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService {
     val uri = params.getTextDocument.getUri
     val pos = params.getPosition
     coordinator.getRoot(uri).getGotoDefinitions(uri, pos).map(defns => {
-        Either.forRight[java.util.List[_ <: Location], java.util.List[_ <: LocationLink]](defns.asJava)
+      Either.forRight[java.util.List[_ <: Location], java.util.List[_ <: LocationLink]](defns.asJava)
     }).asJava.toCompletableFuture
   }
 
@@ -315,6 +318,18 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService {
     CompletableFuture.completedFuture(Nil.asJava)
   }
 
+  override def formatting(params: DocumentFormattingParams) = {
+    coordinator.logger.trace(s"[Req: textDocument/formatting] ${params.toString}")
+    val uri = params.getTextDocument.getUri
+    val result = coordinator.getRoot(uri).reformatFile() match {
+      case None => Seq()
+      case Some(e) =>
+        val range = new Range(new Position(0, 0), new Position(Int.MaxValue, Int.MaxValue))
+        Seq(new TextEdit(range, e))
+    }
+    CompletableFuture.completedFuture(result.asJava)
+  }
+
   // --- DISABLED, see comment in `initialize` ---
   override def diagnostic(params: DocumentDiagnosticParams) = {
     coordinator.logger.trace(s"[Req: textDocument/diagnostic] ${params.toString()}")
@@ -351,9 +366,10 @@ trait WorkspaceReceiver extends StandardReceiver with WorkspaceService {
 }
 
 class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl: String)(implicit _executor: VerificationExecutionContext)
-    extends LanguageClientAware with LanguageReceiver with WorkspaceReceiver with TextDocumentReceiver {
+  extends LanguageClientAware with LanguageReceiver with WorkspaceReceiver with TextDocumentReceiver {
 
   override val coordinator = new ClientCoordinator(server)
+
   override def executor: VerificationExecutionContext = _executor
 
   override def getTextDocumentService(): TextDocumentService = this
@@ -405,16 +421,22 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
           if (verificationStarted) {
             coordinator.logger.info("Verification Started")
           } else {
-            coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
+            coordinator.client.map {
+              _.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+            }
           }
         })
       }).recover(e => {
         coordinator.logger.debug(s"Error handling verify request: $e")
-        coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
+        coordinator.client.map {
+          _.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+        }
       })
     } else {
       coordinator.logger.info("The verification cannot be started.")
-      coordinator.client.map{_.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))}
+      coordinator.client.map {
+        _.notifyVerificationNotStarted(VerificationNotStartedParams(data.uri))
+      }
     }
   }
 

src/main/scala/viper/server/frontends/lsp/ViperServerService.scala

@@ -13,9 +13,12 @@ import akka.util.Timeout
 import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
 import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, ViperCoreServer}
+import viper.server.utility.ReformatterAstGenerator
+import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile}
 import viper.server.utility.Helpers.validateViperFile
 import viper.server.vsi.VerificationProtocol.{StopAstConstruction, StopVerification}
 import viper.server.vsi.{AstJobId, DefaultVerificationServerStart, VerHandle, VerJobId}
+import viper.silver.parser.ReformatPrettyPrinter
 import viper.silver.ast.utility.FileLoader
 
 import scala.concurrent.Future
@@ -52,6 +55,21 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve
     ver_id
   }
 
+  def reformatFile(file: String, localLogger: Option[Logger] = None): Option[String] = {
+    val logger = combineLoggers(localLogger)
+    logger.debug("Requesting ViperServer to create a reformatted file.");
+
+    val ast_generator = new ReformatterAstGenerator(logger);
+    val parse_ast = ast_generator.generateViperParseAst(file);
+    parse_ast match {
+      case Some(p) => Some(ReformatPrettyPrinter.showProgram(p))
+      case _ => {
+        logger.error("Failed to generate parse AST for reformatting the program.")
+        None
+      }
+    }
+  }
+
   def startStreaming(jid: VerJobId, relayActor_props: Props, localLogger: Option[Logger] = None): Option[Future[Unit]] = {
     val logger = combineLoggers(localLogger)
     logger.debug("Sending verification request to ViperServer...")

src/main/scala/viper/server/frontends/lsp/file/Verification.scala

@@ -204,6 +204,11 @@ trait VerificationManager extends ManagesLeaf {
     }
   }
 
+  def reformatFile(): Option[String] = {
+    coordinator.logger.info(s"reformatting the file $filename")
+    coordinator.server.reformatFile(path.toString, Some(coordinator.localLogger))
+  }
+
   /** Do full parsing, type checking and verification */
   def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = {
     lastBackendClassName = Some(backendClassName)

src/main/scala/viper/server/utility/AstGenerator.scala renamed to src/main/scala/viper/server/utility/AstGeneratorBase.scala

@@ -2,43 +2,44 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 //
-// Copyright (c) 2011-2020 ETH Zurich.
+// Copyright (c) 2011-2025 ETH Zurich.
 
 package viper.server.utility
 
 import ch.qos.logback.classic.Logger
 
 import java.nio.file.NoSuchFileException
 import viper.server.utility.Helpers.validateViperFile
-import viper.silver.ast.Program
 import viper.silver.ast.utility.FileLoader
-import viper.silver.frontend.{SilFrontend, ViperAstProvider}
+import viper.silver.frontend.SilFrontend
 import viper.silver.reporter.{NoopReporter, Reporter, PProgramReport}
 
-class AstGenerator(private val _logger: Logger,
-                   private val _reporter: Reporter = NoopReporter,
-                   private val argList: Seq[String] = Seq(),
-                   private val disablePlugins: Boolean = false) extends ProgramDefinitionsProvider {
+/** Base class for AST generators. The parameter T determines the type of AST returned, currently either PProgram or Program
+ */
+abstract class AstGeneratorBase[T](private val _logger: Logger,
+                                   private val _reporter: Reporter = NoopReporter,
+                                   private val argList: Seq[String] = Seq(),
+                                   private val disablePlugins: Boolean = false) extends ProgramDefinitionsProvider {
 
+  /** Creates a backend that reads and parses the file
+   */
+  protected val _frontend: SilFrontend
 
+  /** Extracts the result of type T from the frontend
+   */
+  protected def getResult: T
 
-  /** Creates a backend that reads and parses the file
-    */
-  protected override val _frontend: SilFrontend = {
-    _logger.info(s"Creating new AstGenerator instance.")
-    new ViperAstProvider(_reporter, disablePlugins = disablePlugins)
-  }
-  /** Parses and translates a Viper file into a Viper AST.
-    *
-    * Throws an exception when passed an non-existent file!
-    */
-  def generateViperAst(vpr_file_path: String, loader: Option[FileLoader] = None): Option[Program] = {
+  /** Parses and translates a Viper file into the appropriate AST type.
+   *
+   * Throws an exception when passed a non-existent file!
+   */
+  def generateViperAstImpl(vpr_file_path: String, loader: Option[FileLoader] = None): Option[T] = {
 
     if (!validateViperFile(vpr_file_path)) {
       _logger.error(s"No such file: `$vpr_file_path`")
       throw new NoSuchFileException(vpr_file_path)
     }
-    
+
     _logger.info(s"Parsing `$vpr_file_path` ...")
 
     // We need to pass all arguments relevant to AST creation to the frontend (e.g. everything plugin-related), but we
@@ -52,7 +53,7 @@ class AstGenerator(private val _logger: Logger,
         // argument is the next item in the argList
         filteredArgs = argList.slice(optionArgIndex, optionArgIndex + 2) ++ filteredArgs
       } else {
-        argList.find(_.startsWith(s"${option}=")) match {
+        argList.find(_.startsWith(s"$option=")) match {
           case Some(arg) =>
             filteredArgs = Seq(arg) ++ filteredArgs
           case _ =>
@@ -74,7 +75,7 @@ class AstGenerator(private val _logger: Logger,
       reportProgramStats()
     }
     if (_frontend.errors.isEmpty) {
-      Some(_frontend.translationResult)
+      Some(getResult)
     } else {
       _logger.info(s"Errors occurred while translating `$vpr_file_path`: ${_frontend.errors}")
       None
@@ -85,4 +86,4 @@ class AstGenerator(private val _logger: Logger,
   val flagWhiteList: Seq[String] = Seq("--disableDefaultPlugins", "--disableAdtPlugin", "--disableTerminationPlugin")
   // Parameters that are relevant for AST creation and are passed additional values
   val optionWhiteList: Seq[String] = Seq("--plugin")
-}
+}

src/main/scala/viper/server/utility/ReformatterAstGenerator.scala

@@ -0,0 +1,36 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
+package viper.server.utility
+
+import ch.qos.logback.classic.Logger
+import viper.silver.ast.utility.FileLoader
+import viper.silver.frontend.{SilFrontend, ReformatterAstProvider}
+import viper.silver.parser.PProgram
+import viper.silver.reporter.{NoopReporter, Reporter}
+
+class ReformatterAstGenerator(private val _logger: Logger,
+                              private val _reporter: Reporter = NoopReporter,
+                              private val argList: Seq[String] = Seq(),
+                              private val disablePlugins: Boolean = false) extends AstGeneratorBase[PProgram](_logger, _reporter, argList, disablePlugins) {
+
+  protected override val _frontend: SilFrontend = {
+    _logger.info(s"Creating new ReformatterAstGenerator instance.")
+    new ReformatterAstProvider(_reporter)
+  }
+
+  /** Extracts the parse AST (PProgram) from the frontend
+   */
+  protected override def getResult: PProgram = _frontend.parsingResult
+
+  /** Parses a Viper file into a parse AST (PProgram) without macro expansion.
+   *
+   * Throws an exception when passed a non-existent file!
+   */
+  def generateViperParseAst(vpr_file_path: String, loader: Option[FileLoader] = None): Option[PProgram] = {
+    generateViperAstImpl(vpr_file_path, loader)
+  }
+}