From 590da0cc8acddbb4d232204d016959bd780a1f46 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sat, 19 Oct 2024 17:41:26 +0200 Subject: [PATCH 01/44] No braces --- .../viper/server/frontends/lsp/file/QuantifierInlayHints.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/QuantifierInlayHints.scala b/src/main/scala/viper/server/frontends/lsp/file/QuantifierInlayHints.scala index 78d17cd9..a47d066a 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/QuantifierInlayHints.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/QuantifierInlayHints.scala @@ -13,7 +13,7 @@ import viper.silver.ast.{AbstractSourcePosition, QuantifiedExp, Trigger} trait QuantifierInlayHints extends ProjectAware { def handleQuantifierChosenTriggers(quantifier: QuantifiedExp, triggers: Seq[Trigger], oldTriggers: Seq[Trigger]): Unit = { if (!quantifier.exp.pos.isInstanceOf[AbstractSourcePosition]) { - coordinator.logger.error(s"Got chosen triggers, but quantifier has no position: ${quantifier.toString()}") + coordinator.logger.error(s"Got chosen triggers, but quantifier has no position: ${quantifier.toString}") return } val pos = RangePosition(quantifier.exp.pos.asInstanceOf[AbstractSourcePosition]) From a94d9ec2d7f2d9275ad343603ccd35aab93493c9 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 22 Oct 2024 17:07:05 +0200 Subject: [PATCH 02/44] Make verification work --- .../scala/viper/server/frontends/lsp/ClientCoordinator.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index c6ffcf29..195702f2 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -208,7 +208,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif // we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent val fm = _files.computeIfAbsent(uri, createFMFunc) // Override the content if we are given one and the file manager was not just created - if (!createdNew && content.isDefined) fm.content.set(content.get) + if (!createdNew && content.isDefined && content.get != null) fm.content.set(content.get) fm } def ensureFmExists(uri: String, content: String): FileManager = { From 27271f71bfb727f39709f2fda030447cc524e31a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 26 Dec 2024 19:44:38 +0100 Subject: [PATCH 03/44] Macros: Signature help + fix hover --- .../frontends/lsp/ClientCoordinator.scala | 2 +- .../frontends/lsp/ast/ParseAstLsp.scala | 67 +++++++++++++------ .../frontends/lsp/file/FileContent.scala | 1 + 3 files changed, 50 insertions(+), 20 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index 195702f2..c6ffcf29 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -208,7 +208,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif // we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent val fm = _files.computeIfAbsent(uri, createFMFunc) // Override the content if we are given one and the file manager was not just created - if (!createdNew && content.isDefined && content.get != null) fm.content.set(content.get) + if (!createdNew && content.isDefined) fm.content.set(content.get) fm } def ensureFmExists(uri: String, content: String): FileManager = { diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index e33c58d5..3ad34d04 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -30,12 +30,21 @@ object HasDocumentSymbol { } object HasHoverHints { - def apply(p: PProgram): Seq[HoverHint] = p.deepCollect({ - case n: PIdnUse => PLspIdnUse.getHoverHints(n) - case n: PExp => PLspExp.getHoverHints(n) - case n: PDeclaration => PLspDeclaration.getHoverHints(n) - case n: PReserved[_] => PLspReserved.getHoverHints(n) - }).flatten + def apply(p: PProgram): Seq[HoverHint] = { + p.deepCollectOpt({ + case _: PDefine | _: PAnnotatedExp | _: PAnnotatedStmt => false + case _ => true + }, { + case n: PIdnUse => PLspIdnUse.getHoverHints(n) + case n: PDeclaration => PLspDeclaration.getHoverHints(n) + case n: PReserved[_] => PLspReserved.getHoverHints(n) + case n: PAnnotatedStmt if n.annotation.key.str.equals("expandedMacro") => + RangePosition(n).toSeq.map(rp => HoverHint(n.stmt.pretty, None, Option(rp), SelectionBoundScope(rp))) + case n: PAnnotatedExp if n.annotation.key.str.equals("expandedMacro") => + RangePosition(n).toSeq.map(rp => HoverHint(n.e.pretty, None, Option(rp), SelectionBoundScope(rp))) + case n: PExp => PLspExp.getHoverHints(n) + }).flatten + } } object HasGotoDefinitions { @@ -81,21 +90,41 @@ object HasSemanticHighlights { } object HasSignatureHelps { - def apply(p: PProgram): Seq[SignatureHelp] = p.deepCollect({ - case n: PCallable => { - val bound = SelectionBoundKeyword(n.idndef.name) - // Start - val start = SignatureHelpPart(false, s"${n.keyword.pretty}${n.idndef.pretty}${n.args.l.pretty}", None) - // Args - def faToSigHelpPart(fa: PAnyFormalArgDecl): SignatureHelpPart = SignatureHelpPart(true, fa.pretty, None) - val args = n.args.inner.first.map(faToSigHelpPart).toSeq ++ n.args.inner.inner.flatMap { - case (c, fa) => Seq(SignatureHelpPart(false, c.pretty, None), faToSigHelpPart(fa)) + def apply(p: PProgram): Seq[SignatureHelp] = { + def argsToSigHelpPart[T <: PNode](args: PDelimited.Comma[PSym.Paren, T]) : Seq[SignatureHelpPart] = { + def getSigHelpPart[T <: PNode](arg: T): SignatureHelpPart = SignatureHelpPart(true, arg.pretty, None) + args.inner.first.map(getSigHelpPart).toSeq ++ args.inner.inner.flatMap { + case (c, arg) => Seq(SignatureHelpPart(false, c.pretty, None), getSigHelpPart(arg)) + } } - // Tail - val tail = SignatureHelpPart(false, s"${n.args.r.pretty}${n.returnNodes.map(_.pretty).mkString}", None) - Seq(SignatureHelp(start +: args :+ tail, PLspDeclaration.documentation(n), bound)) + p.deepCollect({ + case n: PCallable => { + val bound = SelectionBoundKeyword(n.idndef.name) + // Start + val start = SignatureHelpPart(false, s"${n.keyword.pretty}${n.idndef.pretty}${n.args.l.pretty}", None) + // Args + val args = argsToSigHelpPart[PAnyFormalArgDecl](n.args) + // Tail + val tail = SignatureHelpPart(false, s"${n.args.r.pretty}${n.returnNodes.map(_.pretty).mkString}", None) + Seq(SignatureHelp(start +: args :+ tail, PLspDeclaration.documentation(n), bound)) + } + case n: PDefine => { + val bound = SelectionBoundKeyword(n.idndef.name) + // Start + val start = SignatureHelpPart(false, s"define ${n.idndef.pretty}", None) + // Args + var mappedParams = Seq[SignatureHelpPart]() + if (n.parameters.isDefined) { + val params = n.parameters.get + mappedParams = argsToSigHelpPart[PDefineParam](n.parameters.get) + mappedParams = SignatureHelpPart(false, s"${params.l.pretty}", None) +: mappedParams :+ SignatureHelpPart(false, s"${params.r.pretty}", None) + } + // Tail + val tail = SignatureHelpPart(false, s" ${n.body.pretty}", None) + Seq(SignatureHelp(start +: mappedParams :+ tail, PLspDeclaration.documentation(n), bound)) + } + }).flatten } - }).flatten } object HasSuggestionScopeRanges { diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 15630135..844e1af9 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -29,6 +29,7 @@ case class FileContent(path: Path) extends DiskLoader { val fileContent = new ArrayBuffer[String] def set(newContent: String): Unit = { + if (newContent == null) return fileContent.clear() fileContent.addAll(newContent.split("\n", -1)) } From 4f5e4f638589b8e0b625d3766ecd0d2a1de13619 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 16 Jan 2025 17:44:51 +0100 Subject: [PATCH 04/44] Display Failing Branches --- .../scala/viper/server/frontends/lsp/file/RelayActor.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 916d639e..3fc1cdf0 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -173,6 +173,10 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntityFailureMessage") markErrorsAsReported(res.errors) task.processErrors(backendClassName, res.errors) + case BranchFailureMessage(_, _, res, _) => + coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] BranchFailureMessage") + markErrorsAsReported(res.errors) + task.processErrors(backendClassName, res.errors) case OverallSuccessMessage(_, verificationTime) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallSuccessMessage") task.state = VerificationReporting From 18d6020b2125d5b957fd97ce7c4219171bb0b900 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 29 Jan 2025 14:53:30 +0100 Subject: [PATCH 05/44] Store trees --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 759f3c1e..bd351141 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 759f3c1e80724d5ab6c53fc9cfb989ccc4be1fc6 +Subproject commit bd35114106d3f18d7fc37d2ca4128288ed137ae7 diff --git a/silicon b/silicon index 46a35ffb..b7a0a6f6 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 46a35ffb154afc8962a9e3646673bd62ccff33c4 +Subproject commit b7a0a6f6e98bd371b41fe56094736af5a1800e08 From 20e5ad5a31bbbfd1f51caf468849714474ecfb6d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 30 Jan 2025 15:45:30 +0100 Subject: [PATCH 06/44] Move class --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index b7a0a6f6..9aea9452 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit b7a0a6f6e98bd371b41fe56094736af5a1800e08 +Subproject commit 9aea94525afae76f4b17b8e0133f9643bcb87e68 From b23b86ce3648b48a092f7a56f4857a8460f1282d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 2 Feb 2025 19:04:58 +0100 Subject: [PATCH 07/44] Refactoring + fixes + red beams support --- carbon | 2 +- silicon | 2 +- .../server/frontends/lsp/DataProtocol.scala | 5 +- .../server/frontends/lsp/file/Branches.scala | 52 +++++++++++++++++++ .../frontends/lsp/file/FileContent.scala | 15 ++++-- .../frontends/lsp/file/RelayActor.scala | 6 --- .../frontends/lsp/file/Verification.scala | 39 +++++++++----- 7 files changed, 94 insertions(+), 27 deletions(-) create mode 100644 src/main/scala/viper/server/frontends/lsp/file/Branches.scala diff --git a/carbon b/carbon index bd351141..6c7762c7 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit bd35114106d3f18d7fc37d2ca4128288ed137ae7 +Subproject commit 6c7762c78140718297779900ce4e7336d742a062 diff --git a/silicon b/silicon index 9aea9452..921d12e9 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 9aea94525afae76f4b17b8e0133f9643bcb87e68 +Subproject commit 921d12e93adfc150b2fa125135bd2124831a9b62 diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index 100eb08a..3b41099c 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -62,6 +62,8 @@ object BackendOutputType { case class ProgressParams(data: Progress, logLevel: Int) +case class BranchFailureDetails(errorMessage: String, /*tree string*/ range: Range) + case class Progress ( domain: String, current: Double, @@ -174,7 +176,8 @@ case class StateChangeParams( verificationNeeded: Double = -1, uri: String = null, stage: String = null, - error: String = null) + error: String = null, + branchFailureDetails: Array[BranchFailureDetails] = null) case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala new file mode 100644 index 00000000..2dfd73f3 --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala @@ -0,0 +1,52 @@ +// 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-2024 ETH Zurich. + +package viper.server.frontends.lsp.file + +import org.eclipse.lsp4j + +trait Branches extends ProjectAware { + def getBranchRange(uri: String, pos: lsp4j.Position, leftIsFatal: Boolean, rightIsFatal: Boolean): lsp4j.Range = { + var start = new lsp4j.Position(pos.getLine, 0) + var end = new lsp4j.Position(pos.getLine, 0) + val m = getInProject(uri) + var currPos = m.content.iterForward(start).drop(1).find { case (c, _) => c == '{' } + if (!currPos.isDefined) return new lsp4j.Range(start, end) + var openBraceCount = 0 + var movedStart = false + do { + val (c, p) = currPos.get + c match { + case '}' => + openBraceCount -= 1 + if (openBraceCount == 0) { + end = new lsp4j.Position(p.getLine, 0) + if (leftIsFatal && !movedStart) { + val nextBracePos = m.content.iterForward(p).drop(1).find { case (c, _) => c == '{' } + if (nextBracePos.isDefined) { + currPos = nextBracePos + } + // move start + if (!rightIsFatal) { + if (nextBracePos.isDefined) { // no else clause + start = new lsp4j.Position(currPos.get._2.getLine, 0) + } else if (p.getLine + 1 < m.content.fileContent.length) { // else clause + start = new lsp4j.Position(p.getLine + 1, 0) + } + } + openBraceCount = 1 + movedStart = true + } + } + case '{' => + openBraceCount += 1 + case _ => + } + currPos = m.content.iterForward(currPos.get._2).drop(1).find { case (c, _) => c == '{' || c == '}' } + } while (currPos.isDefined && openBraceCount > 0) + new lsp4j.Range(start, end) + } +} diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 844e1af9..26db27c3 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -61,14 +61,19 @@ case class FileContent(path: Path) extends DiskLoader { } None } else if (pos.getCharacter > fileContent(pos.getLine).length) { - val newPos = new Position(pos.getLine + 1, pos.getCharacter - fileContent(pos.getLine).length - 1) - while (newPos.getLine < fileContent.length && newPos.getCharacter <= fileContent(newPos.getLine).length) { - newPos.setCharacter(newPos.getCharacter - fileContent(newPos.getLine).length - 1) + var prevLineLength = fileContent(pos.getLine).length + val newPos = new Position(pos.getLine + 1, pos.getCharacter) + while (newPos.getLine < fileContent.length) { + newPos.setCharacter(newPos.getCharacter - prevLineLength - 1) + if (newPos.getCharacter <= fileContent(newPos.getLine).length) { + return Some(newPos) + } + prevLineLength = fileContent(pos.getLine).length newPos.setLine(newPos.getLine + 1) } - if (newPos.getLine < fileContent.length) Some(newPos) else None + None } else { - return Some(new Position(pos.getLine, pos.getCharacter)) + Some(new Position(pos.getLine, pos.getCharacter)) } } def getCharAt(pos: Position): Char = { diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 3fc1cdf0..76e56133 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -13,8 +13,6 @@ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} - -import viper.server.frontends.lsp.file.ProgressCoordinator import viper.silver.parser._ trait MessageHandler extends ProjectManager with VerificationManager with QuantifierCodeLens with QuantifierInlayHints with SignatureHelp { @@ -173,10 +171,6 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntityFailureMessage") markErrorsAsReported(res.errors) task.processErrors(backendClassName, res.errors) - case BranchFailureMessage(_, _, res, _) => - coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] BranchFailureMessage") - markErrorsAsReported(res.errors) - task.processErrors(backendClassName, res.errors) case OverallSuccessMessage(_, verificationTime) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallSuccessMessage") task.state = VerificationReporting diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index e5230808..bfbba532 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -7,24 +7,25 @@ package viper.server.frontends.lsp.file import viper.server.frontends.lsp + import scala.concurrent.Future import viper.server.vsi.AstJobId import viper.server.vsi.VerJobId + import scala.concurrent.ExecutionContext import akka.actor.Props - import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ import akka.actor.ActorRef - import viper.silver.verifier.AbstractError -import scala.collection.mutable.HashSet import viper.silver.ast.AbstractSourcePosition import org.eclipse.lsp4j.Range import org.eclipse.lsp4j +import viper.server.frontends.lsp.BranchFailureDetails import viper.silver.ast.utility.lsp.RangePosition import viper.silver.ast.HasLineColumn import viper.silver.ast.LineColumnPosition +import viper.silver.verifier.errors.PostconditionViolatedBranch import java.nio.file.Path case class VerificationHandler(server: lsp.ViperServerService) { @@ -70,7 +71,7 @@ object VerificationPhase { } } -trait VerificationManager extends Manager { +trait VerificationManager extends Manager with Branches{ implicit def ec: ExecutionContext def file_uri: String = file.file_uri def filename: String = file.filename @@ -237,7 +238,13 @@ trait VerificationManager extends Manager { def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") - val files = HashSet[String]() + val toRangePosition = (err: AbstractError) => { + err.pos match { + case sp: AbstractSourcePosition => RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) + case pos: HasLineColumn => RangePosition(path, pos, pos) + case _ => RangePosition(path, LineColumnPosition(1, 1), LineColumnPosition(1, 1)) + } + } val diags = errors.map(err => { coordinator.logger.info(s"Handling error ${err.toString()}") @@ -267,17 +274,11 @@ trait VerificationManager extends Manager { val range = err.pos match { case sp: AbstractSourcePosition => lsp.Common.toRange(sp) - case pos => { + case pos => val start = lsp.Common.toPosition(pos) new Range(start, start) - } - } - val rp = err.pos match { - case sp: AbstractSourcePosition => RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) - case pos: HasLineColumn => RangePosition(path, pos, pos) - case _ => RangePosition(path, LineColumnPosition(1, 1), LineColumnPosition(1, 1)) } - files.add(rp.file.toUri().toString()) + val rp = toRangePosition(err) val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" @@ -293,5 +294,17 @@ trait VerificationManager extends Manager { diags.groupBy(d => d._1).foreach { case (phase, diags) => addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2)) } + + val branchFailureDetails = errors.collect({case err: PostconditionViolatedBranch => + BranchFailureDetails(err.readableMessage, getBranchRange(this.file_uri, lsp.Common.toPosition(err.pos), err.leftIsFatal, err.rightIsFatal)) + }) + if (branchFailureDetails.length > 0) { + val params = lsp.StateChangeParams( + VerificationRunning.id, + uri=this.file_uri, + branchFailureDetails = branchFailureDetails.toArray + ) + coordinator.sendStateChangeNotification(params, Some(this)) + } } } From b91d6b7471479e7a0490fa2a9fbd32162aeaacbe Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 3 Feb 2025 20:43:58 +0100 Subject: [PATCH 08/44] Fix macro hover --- carbon | 2 +- silicon | 2 +- .../viper/server/frontends/lsp/ast/ParseAstLsp.scala | 9 ++++----- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/carbon b/carbon index 6c7762c7..27f3f1f1 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 6c7762c78140718297779900ce4e7336d742a062 +Subproject commit 27f3f1f13a84c2345564d79a615081b3600195a3 diff --git a/silicon b/silicon index 921d12e9..ec2474e9 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 921d12e93adfc150b2fa125135bd2124831a9b62 +Subproject commit ec2474e961016f3dbe083c418d365441c5691a37 diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 3ad34d04..bb06c9eb 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -32,16 +32,15 @@ object HasDocumentSymbol { object HasHoverHints { def apply(p: PProgram): Seq[HoverHint] = { p.deepCollectOpt({ - case _: PDefine | _: PAnnotatedExp | _: PAnnotatedStmt => false + case _: PDefine | _: PExpandedMacro => false case _ => true }, { + case n: PExpandedMacro => { + RangePosition(n).toSeq.map(rp => HoverHint(n.pretty, None, Option(rp), SelectionBoundScope(rp))) + } case n: PIdnUse => PLspIdnUse.getHoverHints(n) case n: PDeclaration => PLspDeclaration.getHoverHints(n) case n: PReserved[_] => PLspReserved.getHoverHints(n) - case n: PAnnotatedStmt if n.annotation.key.str.equals("expandedMacro") => - RangePosition(n).toSeq.map(rp => HoverHint(n.stmt.pretty, None, Option(rp), SelectionBoundScope(rp))) - case n: PAnnotatedExp if n.annotation.key.str.equals("expandedMacro") => - RangePosition(n).toSeq.map(rp => HoverHint(n.e.pretty, None, Option(rp), SelectionBoundScope(rp))) case n: PExp => PLspExp.getHoverHints(n) }).flatten } From 08a0d93b0608a378d435a9c187c6370375965cf9 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 5 Feb 2025 16:24:58 +0100 Subject: [PATCH 09/44] Redo change for macro hover --- .../scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index bb06c9eb..9bcb9ad9 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -35,12 +35,11 @@ object HasHoverHints { case _: PDefine | _: PExpandedMacro => false case _ => true }, { - case n: PExpandedMacro => { - RangePosition(n).toSeq.map(rp => HoverHint(n.pretty, None, Option(rp), SelectionBoundScope(rp))) - } case n: PIdnUse => PLspIdnUse.getHoverHints(n) case n: PDeclaration => PLspDeclaration.getHoverHints(n) case n: PReserved[_] => PLspReserved.getHoverHints(n) + case n: PExpandedMacro => + RangePosition(n).toSeq.map(rp => HoverHint(n.pretty, None, Option(rp), SelectionBoundScope(rp))) case n: PExp => PLspExp.getHoverHints(n) }).flatten } From b68a4d65ae78e111f87f27d869a577aedd8be321 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Feb 2025 12:39:38 +0100 Subject: [PATCH 10/44] Implementing a code action --- .../viper/server/frontends/lsp/Receiver.scala | 8 +- .../frontends/lsp/ast/ParseAstLsp.scala | 90 ++++++++++++++++++- .../lsp/ast/utility/CodeAction.scala | 21 +++++ .../frontends/lsp/file/FileManager.scala | 2 + .../server/frontends/lsp/file/Manager.scala | 7 ++ .../frontends/lsp/file/ProjectManager.scala | 7 ++ .../frontends/lsp/file/RelayActor.scala | 1 + .../lsp/file/utility/Conversions.scala | 15 ++++ 8 files changed, 148 insertions(+), 3 deletions(-) create mode 100644 src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index cc485217..5c1634a7 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala @@ -311,8 +311,12 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService { } override def codeAction(params: CodeActionParams) = { - // TODO - CompletableFuture.completedFuture(Nil.asJava) + coordinator.logger.trace(s"[Req: textDocument/codeAction] ${params.toString()}") + val uri = params.getTextDocument.getUri + val range = params.getRange + val actions = coordinator.getRoot(uri).getCodeActions(uri, range.getStart) + val jActions = actions.map(_.asJava.asInstanceOf[java.util.List[Either[Command, CodeAction]]]) + jActions.asJava.toCompletableFuture } // --- DISABLED, see comment in `initialize` --- diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 9bcb9ad9..125d4c8f 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -6,10 +6,11 @@ package viper.silver.parser +import viper.server.frontends.lsp.Common import viper.silver.ast.utility.lsp._ import viper.silver.ast.LineColumnPosition -import viper.silver.parser.PStringLiteral import viper.silver.plugin.standard.adt._ +import viper.silver.plugin.standard.termination.PDecreasesKeyword object HasCodeLens { def apply(p: PProgram): Seq[CodeLens] = p.deepCollect(PartialFunction.empty).flatten @@ -146,6 +147,93 @@ object HasCompletionProposals { }).flatten } +object HasCodeActions { + private def isIncreasingSelfAssignment(e: PBinExp): Boolean = { + e.op.rs match { + case PSymOp.Plus | PSymOp.Mul | PKwOp.Union => true + case _ => false + } + } + private def oppositeOp(e: PBinExp): PBinaryOp = { // TODO Does this belong somewhere else? + e.op.rs match { + case PSymOp.Plus => PSymOp.Minus + case PSymOp.Minus => PSymOp.Plus + case PSymOp.Mul => PSymOp.Div + case PSymOp.ArithDiv => PSymOp.Mul // ? + case PSymOp.Div => PSymOp.Mul + case PKwOp.Intersection => PKwOp.Union + case PKwOp.Union => PKwOp.Intersection + //case PKwOp.Setminus => PKwOp.Union + //case PKwOp. => PKwOp.Union + // TODO Stephanie Mod / Subset ... (?) + case _ => e.op.rs + } + } + private def containsSetOp(e: PExp) = e.find({case n: PKwOp => n}).nonEmpty // Correct? + private def getIdentifierNames(e: PExp) : Set[String] = e.deepCollect({case n: PIdnUseExp => n.name}).toSet + private def findSelfAssignment(stmts : PSeqn, idns: Set[String]) : Option[(String, PExp)] = { + stmts.find({case p: PAssign if p.rhs.isInstanceOf[PBinExp]=> ( + idns.intersect( + (p.targets.first ++ p.targets.inner.map(_._1)).map(_.deepCollect({case n: PIdnUseExp => n.name})) + .flatten.toSet.intersect(getIdentifierNames(p.rhs))).headOption, p.rhs)}) + .find(t => t._1.isDefined)}.map(t => (t._1.get, t._2)) + private def findLiteralAssignment(p: PProgram, idn: String): Option[PExp] = { + p.find({case n: PAssign if (n.targets.first ++ n.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]] // TODO Stephanie + .map(getIdentifierNames(_)).flatten.toSet + .contains(idn) && n.rhs.find({case _ : PSimpleLiteral => n}).isDefined => n.rhs}) // TODO Before + } + private def updateExp(e: PExp, j: Int): PExp = { + val newExp = e match { + case PIntLit(i) => PIntLit(i + j)(e.pos) + case _ => PBinExp(e, PReserved(if (j > 0) PSymOp.Plus else PSymOp.Minus)(e.pos), PIntLit(-j)(e.pos))(e.pos) + } + newExp + } + private def getCodeAction(p: PProgram, w: PWhile) : CodeAction = { + val cond = w.cond.inner.asInstanceOf[PBinExp] + val condOp = cond.op.rs + var condBound = cond.right + var selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.left)) + if (!selfAssignment.isDefined) { + selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.right)) + condBound = cond.left + } + selfAssignment match { + case Some(ass) => + val idn = ass._1 + val rhs = ass._2.asInstanceOf[PBinExp] + + val editRp = RangePosition(w.body.ss.l).get + val editRange = Common.toRange(editRp) + editRange.setEnd(editRange.getStart) + val rp = RangePosition(w).get // TODO Stephanie + val decrIndent = " "*(rp.start.column+1) // TODO obtain indentation differently + val braceIndent = " "*(rp.start.column-1) + + val literalAssign = findLiteralAssignment(p, idn) + val bound = if (literalAssign.isDefined) literalAssign.get.pretty + else if (containsSetOp(cond)) "Set[Int]()" // If contains div rational? + else "0" // TODO Stephanie + + val isIncrSelfAssign = isIncreasingSelfAssignment(rhs) + val updatedCondBound = if (condOp == PSymOp.Le || condOp == PSymOp.Ge) + updateExp(condBound, if (isIncrSelfAssign) 1 else -1) else condBound + val lowerBound = if (isIncrSelfAssign) bound else updatedCondBound.pretty + val upperBound = if (isIncrSelfAssign) updatedCondBound.pretty else bound + val decreasesExp = if (isIncrSelfAssign) upperBound + " " + oppositeOp(rhs).token + " " + idn else idn + + val invariant = "\n"+decrIndent + PKw.Invariant.keyword +" "+ lowerBound + " " + PSymOp.Le.symbol + " " + idn + " " + PSymOp.Le.symbol + " " + upperBound + "\n" + val decreases = decrIndent + PDecreasesKeyword.keyword +" "+ decreasesExp + "\n" + braceIndent + + CodeAction(invariant + decreases, editRange, SelectionBoundScope(rp)) + } + } + + def apply(p: PProgram): Seq[CodeAction] = { + p.deepCollect({ + case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => getCodeAction(p,w)}) + } +} //// // Identifiers (uses and definitions) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala new file mode 100644 index 00000000..2712846d --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -0,0 +1,21 @@ +// 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-2024 ETH Zurich. + +package viper.silver.ast.utility.lsp + +import org.eclipse.lsp4j + +trait HasCodeActions { + def getCodeActions: Seq[CodeAction] +} + +case class CodeAction( + edit: String, /* Workspace edit */ + editRange: lsp4j.Range, + bound: SelectionBoundScopeTrait, +) extends SelectableInBound with HasRangePositions { + override def rangePositions: Seq[RangePosition] = bound.rangePositions +} diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala index c63d120d..9732fcc4 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala @@ -57,6 +57,8 @@ case class FileManager(file: PathInfo, coordinator: lsp.ClientCoordinator, conte getInFuture(getInProject(uri).getFoldingRange()) def getCompletionProposal(uri: String, pos: lsp4j.Position, char: Option[String]): Future[Seq[lsp4j.CompletionItem]] = getInFuture(getCompletionProposal(uri, pos, char, ())) + def getCodeActions(uri: String, pos: lsp4j.Position): Future[Seq[lsp4j.CodeAction]] = + Future.successful(getCodeActionsProject(uri, pos)) } object FileManager { diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala index b40bd619..8b91d8db 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala @@ -178,6 +178,13 @@ trait StandardManager extends Manager { containers.addOne(completionProposalContainer) def getCompletionProposal(scope: lsp.SuggestionScope, pos: Option[lsp4j.Position], char: Char) = completionProposalContainer.get((scope, pos, char)) def addCompletionProposal(first: Boolean)(vs: Seq[lsp.CompletionProposal]): Unit = add(completionProposalContainer, first, vs) + + // CodeAction + type CodeActionContainer = utility.StageRangeContainer.RangeContainer[lsp.CodeAction, lsp4j.CodeAction] + val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator) + containers.addOne(codeActionContainer) + def getCodeAction(pos: Option[lsp4j.Position]) = codeActionContainer.get((pos,None,true)) + def addCodeAction(first: Boolean)(vs: Seq[lsp.CodeAction]): Unit = add(codeActionContainer, first, vs) } trait FullManager extends StandardManager with FindReferencesManager diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala index 9d353a72..989d8546 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala @@ -154,6 +154,13 @@ trait ProjectManager extends FullManager with ProjectAware { else super.getCompletionProposal(scope, None, char) ++ getInProject(uri).getCompletionProposal(scope, Some(pos), char) } + override def addCodeAction(first: Boolean)(vs: Seq[lsp.CodeAction]): Unit = + addSib(uri => if (uri == file.file_uri) super.addCodeAction(first) else getInProject(uri).addCodeAction(first), vs) + def getCodeActionsProject(uri: String, pos: lsp4j.Position): Seq[lsp4j.CodeAction] = { + if (uri == file.file_uri) super.getCodeAction(Some(pos)) + else super.getCodeAction(None) ++ getInProject(uri).getCodeAction(Some(pos)) + } + def getIdentAtPos(uri: String, pos: lsp4j.Position): Option[(String, Range)] = getInProject(uri).content.getIdentAtPos(pos) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 76e56133..97f63205 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -139,6 +139,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.addSignatureHelp(true)(HasSignatureHelps(pProgram)) task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram)) task.addCompletionProposal(true)(HasCompletionProposals(pProgram)) + task.addCodeAction(true)(HasCodeActions(pProgram)) } case StatisticsReport(m, f, p, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index 2f714527..b116c458 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -210,3 +210,18 @@ case object SuggestionScopeRangeTranslator extends Translates[lsp.SuggestionScop Seq(min) } } + +case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAction, (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)] { + override def translate(ca: lsp.CodeAction)(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)): lsp4j.CodeAction = ??? + override def translate(cas: Seq[lsp.CodeAction])(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean))(implicit log: Logger): Seq[lsp4j.CodeAction] = { + cas.map(ca => { + val codeAction = new lsp4j.CodeAction("Add invariant") + val textEdits = Seq(new lsp4j.TextEdit(ca.editRange, ca.edit)).asJava + val uri = ca.bound.scope.file.toUri().toString() + val edits = Map(uri -> textEdits).asJava + val workspaceEdit = new lsp4j.WorkspaceEdit(edits) + codeAction.setEdit(workspaceEdit) + codeAction + }) + } +} \ No newline at end of file From 6a12366fd02659750309d9b8a692e32e9c811d3d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Feb 2025 18:12:42 +0100 Subject: [PATCH 11/44] Implementing a code action --- .../frontends/lsp/ast/ParseAstLsp.scala | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 125d4c8f..ca847d84 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -8,7 +8,7 @@ package viper.silver.parser import viper.server.frontends.lsp.Common import viper.silver.ast.utility.lsp._ -import viper.silver.ast.LineColumnPosition +import viper.silver.ast.{AnySetCardinality, LineColumnPosition} import viper.silver.plugin.standard.adt._ import viper.silver.plugin.standard.termination.PDecreasesKeyword @@ -169,7 +169,7 @@ object HasCodeActions { case _ => e.op.rs } } - private def containsSetOp(e: PExp) = e.find({case n: PKwOp => n}).nonEmpty // Correct? + private def containsSetOp(e: PExp) = e.find({case PReserved(n) if n.isInstanceOf[PSetToSetOp] => n}).nonEmpty // Correct? private def getIdentifierNames(e: PExp) : Set[String] = e.deepCollect({case n: PIdnUseExp => n.name}).toSet private def findSelfAssignment(stmts : PSeqn, idns: Set[String]) : Option[(String, PExp)] = { stmts.find({case p: PAssign if p.rhs.isInstanceOf[PBinExp]=> ( @@ -192,27 +192,31 @@ object HasCodeActions { private def getCodeAction(p: PProgram, w: PWhile) : CodeAction = { val cond = w.cond.inner.asInstanceOf[PBinExp] val condOp = cond.op.rs + val containsSetOpCond = containsSetOp(cond) var condBound = cond.right + var middle = cond.left var selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.left)) if (!selfAssignment.isDefined) { selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.right)) condBound = cond.left + middle = cond.right } selfAssignment match { case Some(ass) => val idn = ass._1 val rhs = ass._2.asInstanceOf[PBinExp] + val containsSetOpRhs = containsSetOp(rhs) val editRp = RangePosition(w.body.ss.l).get val editRange = Common.toRange(editRp) editRange.setEnd(editRange.getStart) val rp = RangePosition(w).get // TODO Stephanie - val decrIndent = " "*(rp.start.column+1) // TODO obtain indentation differently + val decrIndent = " "*rp.start.column // TODO obtain indentation differently val braceIndent = " "*(rp.start.column-1) val literalAssign = findLiteralAssignment(p, idn) val bound = if (literalAssign.isDefined) literalAssign.get.pretty - else if (containsSetOp(cond)) "Set[Int]()" // If contains div rational? + else if (containsSetOpCond && containsSetOpRhs) "Set[Int]()" // If contains div rational? else "0" // TODO Stephanie val isIncrSelfAssign = isIncreasingSelfAssignment(rhs) @@ -220,10 +224,11 @@ object HasCodeActions { updateExp(condBound, if (isIncrSelfAssign) 1 else -1) else condBound val lowerBound = if (isIncrSelfAssign) bound else updatedCondBound.pretty val upperBound = if (isIncrSelfAssign) updatedCondBound.pretty else bound - val decreasesExp = if (isIncrSelfAssign) upperBound + " " + oppositeOp(rhs).token + " " + idn else idn + val decreasesOp = if (!containsSetOpCond && containsSetOpRhs) PSymOp.Minus.token else oppositeOp(rhs).token + val decreasesExp = if (isIncrSelfAssign) s"$upperBound $decreasesOp ${middle.pretty}" else middle.pretty - val invariant = "\n"+decrIndent + PKw.Invariant.keyword +" "+ lowerBound + " " + PSymOp.Le.symbol + " " + idn + " " + PSymOp.Le.symbol + " " + upperBound + "\n" - val decreases = decrIndent + PDecreasesKeyword.keyword +" "+ decreasesExp + "\n" + braceIndent + val invariant = s"\n$decrIndent ${PKw.Invariant.keyword} $lowerBound ${PSymOp.Le.symbol} ${middle.pretty} ${PSymOp.Le.symbol} $upperBound\n" + val decreases = s"$decrIndent ${PDecreasesKeyword.keyword} $decreasesExp\n$braceIndent" CodeAction(invariant + decreases, editRange, SelectionBoundScope(rp)) } From 1f21000008eb0ccce056846b22f75616123340e9 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Feb 2025 18:17:12 +0100 Subject: [PATCH 12/44] Remove unused import --- src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index ca847d84..3a1ab99a 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -8,7 +8,7 @@ package viper.silver.parser import viper.server.frontends.lsp.Common import viper.silver.ast.utility.lsp._ -import viper.silver.ast.{AnySetCardinality, LineColumnPosition} +import viper.silver.ast.{LineColumnPosition} import viper.silver.plugin.standard.adt._ import viper.silver.plugin.standard.termination.PDecreasesKeyword From 05f8b6ee5f831cc40f68364be623f6fc38d173b4 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 16 Feb 2025 20:37:19 +0100 Subject: [PATCH 13/44] Add code actions + cleanup --- .../frontends/lsp/ast/ParseAstLsp.scala | 97 ++++++------ .../lsp/ast/utility/CodeAction.scala | 9 +- .../server/frontends/lsp/file/Manager.scala | 17 +- .../frontends/lsp/file/ProjectManager.scala | 4 +- .../frontends/lsp/file/RelayActor.scala | 3 + .../frontends/lsp/file/Verification.scala | 145 +++++++++++++++--- .../lsp/file/utility/Conversions.scala | 8 +- 7 files changed, 194 insertions(+), 89 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 3a1ab99a..f236eef6 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -6,9 +6,10 @@ package viper.silver.parser +import org.eclipse.lsp4j.{CodeActionKind, Range} import viper.server.frontends.lsp.Common import viper.silver.ast.utility.lsp._ -import viper.silver.ast.{LineColumnPosition} +import viper.silver.ast.LineColumnPosition import viper.silver.plugin.standard.adt._ import viper.silver.plugin.standard.termination.PDecreasesKeyword @@ -154,22 +155,6 @@ object HasCodeActions { case _ => false } } - private def oppositeOp(e: PBinExp): PBinaryOp = { // TODO Does this belong somewhere else? - e.op.rs match { - case PSymOp.Plus => PSymOp.Minus - case PSymOp.Minus => PSymOp.Plus - case PSymOp.Mul => PSymOp.Div - case PSymOp.ArithDiv => PSymOp.Mul // ? - case PSymOp.Div => PSymOp.Mul - case PKwOp.Intersection => PKwOp.Union - case PKwOp.Union => PKwOp.Intersection - //case PKwOp.Setminus => PKwOp.Union - //case PKwOp. => PKwOp.Union - // TODO Stephanie Mod / Subset ... (?) - case _ => e.op.rs - } - } - private def containsSetOp(e: PExp) = e.find({case PReserved(n) if n.isInstanceOf[PSetToSetOp] => n}).nonEmpty // Correct? private def getIdentifierNames(e: PExp) : Set[String] = e.deepCollect({case n: PIdnUseExp => n.name}).toSet private def findSelfAssignment(stmts : PSeqn, idns: Set[String]) : Option[(String, PExp)] = { stmts.find({case p: PAssign if p.rhs.isInstanceOf[PBinExp]=> ( @@ -177,10 +162,28 @@ object HasCodeActions { (p.targets.first ++ p.targets.inner.map(_._1)).map(_.deepCollect({case n: PIdnUseExp => n.name})) .flatten.toSet.intersect(getIdentifierNames(p.rhs))).headOption, p.rhs)}) .find(t => t._1.isDefined)}.map(t => (t._1.get, t._2)) - private def findLiteralAssignment(p: PProgram, idn: String): Option[PExp] = { - p.find({case n: PAssign if (n.targets.first ++ n.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]] // TODO Stephanie + private def containsIdn(ass: PAssign, idn: String): Boolean = { + (ass.targets.first ++ ass.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]] .map(getIdentifierNames(_)).flatten.toSet - .contains(idn) && n.rhs.find({case _ : PSimpleLiteral => n}).isDefined => n.rhs}) // TODO Before + .contains(idn) && ass.rhs.find({case _ : PSimpleLiteral => ass}).isDefined + } + private def findClosestLiteralAssignment(n: PNode, idn: String): Option[PExp] = { + var curr: Option[PNode] = Some(n) + var result: Option[PExp] = None + while (curr.isDefined && !result.isDefined) { + curr.get match { + case pa : PAssign if containsIdn(pa, idn) => result = Some(pa.rhs) + case _ => + } + curr = curr.get.prev + } + if (result.isDefined) { + result + } else if (n.getParent.isDefined && !n.getParent.get.isInstanceOf[PMethod]){ + findClosestLiteralAssignment(n.getParent.get, idn) + } else { + None + } } private def updateExp(e: PExp, j: Int): PExp = { val newExp = e match { @@ -189,10 +192,11 @@ object HasCodeActions { } newExp } - private def getCodeAction(p: PProgram, w: PWhile) : CodeAction = { + private def getEditRange(n: PNode): Option[Range] = RangePosition(n) + .map(Common.toRange(_)).map(r => {r.setEnd(r.getStart); r}) + .headOption + private def getCodeActionAddingInvariant(w: PWhile) : CodeAction = { val cond = w.cond.inner.asInstanceOf[PBinExp] - val condOp = cond.op.rs - val containsSetOpCond = containsSetOp(cond) var condBound = cond.right var middle = cond.left var selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.left)) @@ -201,43 +205,34 @@ object HasCodeActions { condBound = cond.left middle = cond.right } - selfAssignment match { - case Some(ass) => - val idn = ass._1 - val rhs = ass._2.asInstanceOf[PBinExp] - val containsSetOpRhs = containsSetOp(rhs) - - val editRp = RangePosition(w.body.ss.l).get - val editRange = Common.toRange(editRp) - editRange.setEnd(editRange.getStart) - val rp = RangePosition(w).get // TODO Stephanie - val decrIndent = " "*rp.start.column // TODO obtain indentation differently - val braceIndent = " "*(rp.start.column-1) - - val literalAssign = findLiteralAssignment(p, idn) - val bound = if (literalAssign.isDefined) literalAssign.get.pretty - else if (containsSetOpCond && containsSetOpRhs) "Set[Int]()" // If contains div rational? - else "0" // TODO Stephanie - - val isIncrSelfAssign = isIncreasingSelfAssignment(rhs) - val updatedCondBound = if (condOp == PSymOp.Le || condOp == PSymOp.Ge) + val rp = RangePosition(w) + val editRange = getEditRange(w.body.ss.l) + (rp, editRange, selfAssignment) match { + case (Some(rp), Some(er), Some(sa)) => + val (idn, saRhs) = sa + val la = findClosestLiteralAssignment(w, idn) + + val bound = if (la.isDefined) la.get.pretty else "0" + val isIncrSelfAssign = isIncreasingSelfAssignment(saRhs.asInstanceOf[PBinExp]) + val updatedCondBound = if (cond.op.rs == PSymOp.Le || cond.op.rs == PSymOp.Ge) updateExp(condBound, if (isIncrSelfAssign) 1 else -1) else condBound val lowerBound = if (isIncrSelfAssign) bound else updatedCondBound.pretty val upperBound = if (isIncrSelfAssign) updatedCondBound.pretty else bound - val decreasesOp = if (!containsSetOpCond && containsSetOpRhs) PSymOp.Minus.token else oppositeOp(rhs).token - val decreasesExp = if (isIncrSelfAssign) s"$upperBound $decreasesOp ${middle.pretty}" else middle.pretty + val decreasesExp = if (isIncrSelfAssign) s"$upperBound ${PSymOp.Minus.token} ${middle.pretty}" else middle.pretty - val invariant = s"\n$decrIndent ${PKw.Invariant.keyword} $lowerBound ${PSymOp.Le.symbol} ${middle.pretty} ${PSymOp.Le.symbol} $upperBound\n" - val decreases = s"$decrIndent ${PDecreasesKeyword.keyword} $decreasesExp\n$braceIndent" + val indent = " "*(rp.start.column-1) + val beforeInvKeyword = if (rp.start.line == er.getStart.getLine) "" else s"\n$indent" + val invariant = s"$beforeInvKeyword ${PKw.Invariant.keyword} $lowerBound ${PSymOp.Le.symbol} ${middle.pretty} ${PSymOp.Le.symbol} $upperBound\n" + val decreases = s"$indent ${PDecreasesKeyword.keyword} $decreasesExp\n$indent" - CodeAction(invariant + decreases, editRange, SelectionBoundScope(rp)) + CodeAction("Add loop invariant", invariant + decreases, er, SelectionBoundScope(rp), CodeActionKind.Empty, Seq.empty) } } def apply(p: PProgram): Seq[CodeAction] = { - p.deepCollect({ - case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => getCodeAction(p,w)}) - } + p.deepCollect({ case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => w}) + .collect(getCodeActionAddingInvariant(_)) + } } //// diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 2712846d..930a7210 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -13,9 +13,12 @@ trait HasCodeActions { } case class CodeAction( - edit: String, /* Workspace edit */ - editRange: lsp4j.Range, - bound: SelectionBoundScopeTrait, + title: String, + edit: String, /* Workspace edit */ + editRange: lsp4j.Range, + bound: SelectionBoundScopeTrait, + kind: String, + resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty ) extends SelectableInBound with HasRangePositions { override def rangePositions: Seq[RangePosition] = bound.rangePositions } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala index 8b91d8db..18e008c2 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala @@ -12,15 +12,15 @@ import viper.server.frontends.lsp.ClientCoordinator import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer -import viper.server.frontends.lsp.file.FileContent import viper.server.frontends.lsp.Lsp4jSemanticHighlight import VerificationPhase._ - import org.eclipse.lsp4j import viper.silver.ast.utility.lsp import viper.server.frontends.lsp.Common +import viper.silver.ast.utility.lsp.{SelectableInBound, SelectionBoundScope, SelectionBoundTrait} -case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile { +case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends SelectableInBound with lsp.HasRangePositions with lsp.BelongsToFile { + override val bound: SelectionBoundTrait = SelectionBoundScope(position) override def rangePositions: Seq[lsp.RangePosition] = Seq(position) override def file: Path = position.file } @@ -39,6 +39,7 @@ trait Manager { def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit def getDiagnostic(): Seq[lsp4j.Diagnostic] + def getDiagnosticBy(pos: Option[lsp4j.Position], keyword: Option[(String, lsp4j.Range)]) : Seq[lsp4j.Diagnostic] def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit def resetDiagnostics(first: Boolean): Unit @@ -70,6 +71,9 @@ trait Manager { def getCompletionProposal(scope: lsp.SuggestionScope, pos: Option[lsp4j.Position], char: Char): Seq[lsp4j.CompletionItem] def addCompletionProposal(first: Boolean)(vs: Seq[lsp.CompletionProposal]): Unit + + def getCodeAction(pos: Option[lsp4j.Position], keyword: Option[(String, lsp4j.Range)]): Seq[lsp4j.CodeAction] + def addCodeAction(first: Boolean)(vs: Seq[lsp.CodeAction]): Unit } trait StandardManager extends Manager { @@ -98,14 +102,15 @@ trait StandardManager extends Manager { def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit = add(codeLensContainer, first, vs) // Diagnostic - type DiagnosticContainer = utility.StageArrayContainer.ArrayContainer[Diagnostic, lsp4j.Diagnostic] + type DiagnosticContainer = utility.StageRangeContainer.RangeContainer[Diagnostic, lsp4j.Diagnostic] val diagnosticContainer: DiagnosticContainer = utility.LspContainer(utility.DiagnosticTranslator, publishDiags) private def publishDiags(): Unit = { val diagnosticParams = new PublishDiagnosticsParams(file.file_uri, getDiagnostic().asJava) coordinator.client.publishDiagnostics(diagnosticParams) } // containers.addOne(diagnosticContainer) - def getDiagnostic() = diagnosticContainer.get(()) + def getDiagnostic() = diagnosticContainer.all(_=>true).map(d => utility.DiagnosticTranslator.translate(d)(None,None,true)) + def getDiagnosticBy(pos: Option[lsp4j.Position], keyword: Option[(String, lsp4j.Range)]) = diagnosticContainer.get((pos,keyword,true)) def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit = add(diagnosticContainer, first, vs) def removeDiagnostics() = diagnosticContainer.resetAll() def resetDiagnostics(first: Boolean): Unit = diagnosticContainer.reset(first) @@ -183,7 +188,7 @@ trait StandardManager extends Manager { type CodeActionContainer = utility.StageRangeContainer.RangeContainer[lsp.CodeAction, lsp4j.CodeAction] val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator) containers.addOne(codeActionContainer) - def getCodeAction(pos: Option[lsp4j.Position]) = codeActionContainer.get((pos,None,true)) + def getCodeAction(pos: Option[lsp4j.Position], keyword: Option[(String, lsp4j.Range)]) = codeActionContainer.get((pos,None,true)) def addCodeAction(first: Boolean)(vs: Seq[lsp.CodeAction]): Unit = add(codeActionContainer, first, vs) } diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala index 989d8546..fa0b9d48 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala @@ -157,8 +157,8 @@ trait ProjectManager extends FullManager with ProjectAware { override def addCodeAction(first: Boolean)(vs: Seq[lsp.CodeAction]): Unit = addSib(uri => if (uri == file.file_uri) super.addCodeAction(first) else getInProject(uri).addCodeAction(first), vs) def getCodeActionsProject(uri: String, pos: lsp4j.Position): Seq[lsp4j.CodeAction] = { - if (uri == file.file_uri) super.getCodeAction(Some(pos)) - else super.getCodeAction(None) ++ getInProject(uri).getCodeAction(Some(pos)) + if (uri == file.file_uri) super.getCodeAction(Some(pos),None) + else getInProject(uri).getCodeAction(Some(pos),None) } def getIdentAtPos(uri: String, pos: lsp4j.Position): Option[(String, Range)] = diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 97f63205..219e9c69 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -117,6 +117,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case PProgramReport(typeckSuccess, pProgram) => // New project + println("TEST TEST TEST TEST TEST pProgram") + println(pProgram) coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] got new pProgram for ${task.filename}") val files = pProgram.imports.flatMap(_.resolved).map(_.toUri().toString()).toSet task.setupProject(files) @@ -139,6 +141,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.addSignatureHelp(true)(HasSignatureHelps(pProgram)) task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram)) task.addCompletionProposal(true)(HasCompletionProposals(pProgram)) + // Only for code actions not associated to a diagnostic, others are added in processErrors task.addCodeAction(true)(HasCodeActions(pProgram)) } case StatisticsReport(m, f, p, _, _) => diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index bfbba532..23e983d2 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -17,15 +17,15 @@ import akka.actor.Props import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ import akka.actor.ActorRef -import viper.silver.verifier.AbstractError -import viper.silver.ast.AbstractSourcePosition -import org.eclipse.lsp4j.Range +import viper.silver.verifier.{AbstractError, TypecheckerError, VerificationError} +import viper.silver.parser.{PFieldAccess, PKw} +import viper.silver.ast.{AbstractSourcePosition, FieldAccess, HasLineColumn, Label, LineColumnPosition, MemberWithSpec, Method, Position, Seqn, While} import org.eclipse.lsp4j -import viper.server.frontends.lsp.BranchFailureDetails -import viper.silver.ast.utility.lsp.RangePosition -import viper.silver.ast.HasLineColumn -import viper.silver.ast.LineColumnPosition +import viper.server.frontends.lsp.{BranchFailureDetails, Common} +import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} import viper.silver.verifier.errors.PostconditionViolatedBranch +import viper.silver.verifier.reasons.InsufficientPermission + import java.nio.file.Path case class VerificationHandler(server: lsp.ViperServerService) { @@ -71,7 +71,7 @@ object VerificationPhase { } } -trait VerificationManager extends Manager with Branches{ +trait VerificationManager extends Manager with Branches { implicit def ec: ExecutionContext def file_uri: String = file.file_uri def filename: String = file.filename @@ -236,16 +236,114 @@ trait VerificationManager extends Manager with Branches{ def props(backendClassName: Option[String]): Props - def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { - val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") - val toRangePosition = (err: AbstractError) => { - err.pos match { - case sp: AbstractSourcePosition => RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) - case pos: HasLineColumn => RangePosition(path, pos, pos) - case _ => RangePosition(path, LineColumnPosition(1, 1), LineColumnPosition(1, 1)) - } + private def toRange(pos : Position) : lsp4j.Range = { + pos match { + case sp: AbstractSourcePosition => lsp.Common.toRange(sp) + case pos => + val start = lsp.Common.toPosition(pos) + new lsp4j.Range(start, start) } + } + + private def toRangePosition(pos: Position) : RangePosition = { + pos match { + case sp: AbstractSourcePosition => RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) + case pos: HasLineColumn => RangePosition(path, pos, pos) + case _ => RangePosition(path, LineColumnPosition(1, 1), LineColumnPosition(1, 1)) + } + } + + private case object CodeActionType { + val undeclaredField : Int = 0 + val fieldPermError : Int = 1 + } + + private val startOfFileRange = new lsp4j.Range(new lsp4j.Position(0, 0), new lsp4j.Position(0, 0)) + private def getCodeActionsForUndeclaredFields(errors: Seq[TypecheckerError]) : Seq[CodeAction] = { + errors.groupBy(_.node.get) + .flatMap(fa => { + val (faNode, faErrors) = fa + val fieldAccess = faNode.asInstanceOf[PFieldAccess] + val faDiags = faErrors.flatMap(e => { + val pos = Common.toPosition(e.pos) + getDiagnosticBy(Some(pos), None) + }) + faErrors.map(err => { + CodeAction("Add field declaration", s"field ${fieldAccess.idnref.pretty} : [your type]\n", + startOfFileRange, + SelectionBoundScope(toRangePosition(err.pos)), + lsp4j.CodeActionKind.QuickFix, + faDiags) + }) + }).toSeq + } + private def getCodeActionsForFieldPermissionError(errors: Seq[VerificationError]) : Seq[CodeAction] = { + errors.groupBy(_.reason.offendingNode.toString()).flatMap(fa => { + val (faStr, faErrors) = fa + val faDiags = faErrors.flatMap(err => { + val pos = Common.toPosition(err.pos) + getDiagnosticBy(Some(pos), None) + }) + faErrors.flatMap(err => { + val f = err.reason.offendingNode + val seqn = f.getAncestor[Seqn] // TODO Stephanie check + var parentWithSpec : Option[MemberWithSpec] = None + if (seqn.isDefined) { + parentWithSpec = seqn.get.getAncestor[MemberWithSpec] + } + parentWithSpec.collect({ + case l : Label => (l,PKw.Invariant.keyword) + case w : While => (w,PKw.Invariant.keyword) + case m : Method => (m,PKw.Requires.keyword) + }).map( t => { + val (parent, keyword) = t + val parentPosFile = Common.toPosition(parent.pos) + val m = getInProject(this.file_uri).content + val closingBracketPos = m.iterForward(parentPosFile) + .find { case (c, _) => c == '{'} + .map(t => {val p = t._2; p.setCharacter(p.getCharacter-1); p}) + val closingBracketInSameLine = closingBracketPos + .map(p => p.getLine == parentPosFile.getLine) + .getOrElse(false) + val editPos = if (closingBracketInSameLine) closingBracketPos.get else + {val p = Common.toPosition(parent.pos);p.setLine(p.getLine+1);p} + val parentRangePosition = toRangePosition(parent.pos) + val indent = " "*(parentRangePosition.start.column-1) + val beforeKeyword = if (closingBracketInSameLine) s"\n$indent " else " " + CodeAction("Add access precondition", s"$beforeKeyword$keyword acc($faStr)\n$indent", + new lsp4j.Range(editPos, editPos), + SelectionBoundScope(toRangePosition(err.pos)), + lsp4j.CodeActionKind.QuickFix, + faDiags) + }).toSeq + }) + }).toSeq + } + private def addCodeActions(errors : Seq[AbstractError]) = { + errors.groupBy({ + case e: TypecheckerError if e.node.isDefined + && e.node.get.isInstanceOf[PFieldAccess] => CodeActionType.undeclaredField + case e : VerificationError if e.reason.isInstanceOf[InsufficientPermission] + && e.reason.offendingNode.isInstanceOf[FieldAccess] => CodeActionType.fieldPermError + case _ => -1 + }).filter(t => t._1 >= 0) + .map(e => { + val (caType, filteredErrors) = e + caType match { + case CodeActionType.undeclaredField => + val filteredErrors_ = filteredErrors.asInstanceOf[Seq[TypecheckerError]] + this.addCodeAction(first = true)(getCodeActionsForUndeclaredFields(filteredErrors_)) + case CodeActionType.fieldPermError => + val filteredErrors_ = filteredErrors.asInstanceOf[Seq[VerificationError]] + this.addCodeAction(first = false)(getCodeActionsForFieldPermissionError(filteredErrors_)) + } + }) + } + + def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { + // Add diagnostics + val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") val diags = errors.map(err => { coordinator.logger.info(s"Handling error ${err.toString()}") var errorType: String = "" @@ -272,13 +370,8 @@ trait VerificationManager extends Manager with Branches{ errorType = "Verification error" } - val range = err.pos match { - case sp: AbstractSourcePosition => lsp.Common.toRange(sp) - case pos => - val start = lsp.Common.toPosition(pos) - new Range(start, start) - } - val rp = toRangePosition(err) + val range = toRange(err.pos) + val rp = toRangePosition(err.pos) val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" @@ -295,10 +388,14 @@ trait VerificationManager extends Manager with Branches{ addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2)) } + // Add code actions + addCodeActions(errors) + + // Support for red beams indicating branch failure val branchFailureDetails = errors.collect({case err: PostconditionViolatedBranch => BranchFailureDetails(err.readableMessage, getBranchRange(this.file_uri, lsp.Common.toPosition(err.pos), err.leftIsFatal, err.rightIsFatal)) }) - if (branchFailureDetails.length > 0) { + if (branchFailureDetails.nonEmpty) { val params = lsp.StateChangeParams( VerificationRunning.id, uri=this.file_uri, diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index b116c458..4597e4fb 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -29,8 +29,8 @@ case object CodeLensTranslator extends Translates[lsp.CodeLens, lsp4j.CodeLens, } } -case object DiagnosticTranslator extends Translates[Diagnostic, lsp4j.Diagnostic, Unit] { - override def translate(diag: Diagnostic)(i: Unit): lsp4j.Diagnostic = { +case object DiagnosticTranslator extends Translates[Diagnostic, lsp4j.Diagnostic, (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)] { + override def translate(diag: Diagnostic)(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)): lsp4j.Diagnostic = { val range = Common.toRange(diag.position) new lsp4j.Diagnostic(range, diag.message, diag.severity, "viper") } @@ -215,12 +215,14 @@ case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAc override def translate(ca: lsp.CodeAction)(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)): lsp4j.CodeAction = ??? override def translate(cas: Seq[lsp.CodeAction])(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean))(implicit log: Logger): Seq[lsp4j.CodeAction] = { cas.map(ca => { - val codeAction = new lsp4j.CodeAction("Add invariant") + val codeAction = new lsp4j.CodeAction(ca.title) val textEdits = Seq(new lsp4j.TextEdit(ca.editRange, ca.edit)).asJava val uri = ca.bound.scope.file.toUri().toString() val edits = Map(uri -> textEdits).asJava val workspaceEdit = new lsp4j.WorkspaceEdit(edits) codeAction.setEdit(workspaceEdit) + codeAction.setDiagnostics(ca.resolvedDiags.asJava) + codeAction.setKind(ca.kind) codeAction }) } From b4bd4879728be937fdbb6683767bd1d4c2369936 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 17 Feb 2025 16:28:44 +0100 Subject: [PATCH 14/44] Remove print statement --- src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 219e9c69..16963da8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -117,8 +117,6 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case PProgramReport(typeckSuccess, pProgram) => // New project - println("TEST TEST TEST TEST TEST pProgram") - println(pProgram) coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] got new pProgram for ${task.filename}") val files = pProgram.imports.flatMap(_.resolved).map(_.toUri().toString()).toSet task.setupProject(files) From a31986a029351b76dfcfd92d690c508ad300189c Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 19 Feb 2025 21:35:47 +0100 Subject: [PATCH 15/44] Red squiggly line on method name --- .../frontends/lsp/file/Verification.scala | 39 ++++++++++++++++--- 1 file changed, 34 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 23e983d2..573d7062 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -286,7 +286,7 @@ trait VerificationManager extends Manager with Branches { }) faErrors.flatMap(err => { val f = err.reason.offendingNode - val seqn = f.getAncestor[Seqn] // TODO Stephanie check + val seqn = f.getAncestor[Seqn] var parentWithSpec : Option[MemberWithSpec] = None if (seqn.isDefined) { parentWithSpec = seqn.get.getAncestor[MemberWithSpec] @@ -341,6 +341,32 @@ trait VerificationManager extends Manager with Branches { }) } + def getMethodIdentifier(error: PostconditionViolatedBranch): Option[(String, lsp4j.Range)] = { + val content = getInProject(this.file_uri).content + error.offendingNode.getAncestor[Method].map(m => + content.iterForward(Common.toPosition(m.pos)) + .dropWhile(c => c._1.isLetter) + .find({ case (c, _) => Common.isIdentChar(c) }) + .map(t => content.getIdentAtPos(t._2)) + .getOrElse(None) + ).getOrElse(None) + } + + private def getErrorRangeAndPos(error: AbstractError) : (lsp4j.Range, RangePosition) = { + val range = toRange(error.pos) + val rp = toRangePosition(error.pos) + error match { + case e : PostconditionViolatedBranch => + getMethodIdentifier(e).map(i => { + val (_, identRange) = i + (identRange, new RangePosition(path, + LineColumnPosition(identRange.getStart.getLine+1, identRange.getStart.getCharacter+1), + LineColumnPosition(identRange.getEnd.getLine+1, identRange.getEnd.getCharacter+1))) + }).getOrElse((range,rp)) + case _ => (range,rp) + } + } + def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { // Add diagnostics val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") @@ -370,8 +396,7 @@ trait VerificationManager extends Manager with Branches { errorType = "Verification error" } - val range = toRange(err.pos) - val rp = toRangePosition(err.pos) + val (range,rp) = getErrorRangeAndPos(err) val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" @@ -393,8 +418,12 @@ trait VerificationManager extends Manager with Branches { // Support for red beams indicating branch failure val branchFailureDetails = errors.collect({case err: PostconditionViolatedBranch => - BranchFailureDetails(err.readableMessage, getBranchRange(this.file_uri, lsp.Common.toPosition(err.pos), err.leftIsFatal, err.rightIsFatal)) - }) + BranchFailureDetails(err.readableMessage, + getBranchRange(this.file_uri, + lsp.Common.toPosition(err.pos), + err.leftIsFatal, + err.rightIsFatal) + )}) if (branchFailureDetails.nonEmpty) { val params = lsp.StateChangeParams( VerificationRunning.id, From b38e7c061b290db5c6b7c2d974416d5aee1f7f62 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 19 Feb 2025 22:15:46 +0100 Subject: [PATCH 16/44] Refactoring --- .../frontends/lsp/file/Verification.scala | 67 +++++++++---------- 1 file changed, 32 insertions(+), 35 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 573d7062..43061d73 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -253,9 +253,10 @@ trait VerificationManager extends Manager with Branches { } } - private case object CodeActionType { - val undeclaredField : Int = 0 - val fieldPermError : Int = 1 + private case object ErrorType { + val branchFailureInfo : Int = 0 + val undeclaredField : Int = 1 + val fieldPermError : Int = 2 } private val startOfFileRange = new lsp4j.Range(new lsp4j.Position(0, 0), new lsp4j.Position(0, 0)) @@ -320,24 +321,37 @@ trait VerificationManager extends Manager with Branches { }).toSeq } - private def addCodeActions(errors : Seq[AbstractError]) = { + private def processByType(errors : Seq[AbstractError]) = { errors.groupBy({ + case _: PostconditionViolatedBranch => ErrorType.branchFailureInfo case e: TypecheckerError if e.node.isDefined - && e.node.get.isInstanceOf[PFieldAccess] => CodeActionType.undeclaredField + && e.node.get.isInstanceOf[PFieldAccess] => ErrorType.undeclaredField case e : VerificationError if e.reason.isInstanceOf[InsufficientPermission] - && e.reason.offendingNode.isInstanceOf[FieldAccess] => CodeActionType.fieldPermError + && e.reason.offendingNode.isInstanceOf[FieldAccess] => ErrorType.fieldPermError case _ => -1 }).filter(t => t._1 >= 0) - .map(e => { - val (caType, filteredErrors) = e - caType match { - case CodeActionType.undeclaredField => - val filteredErrors_ = filteredErrors.asInstanceOf[Seq[TypecheckerError]] - this.addCodeAction(first = true)(getCodeActionsForUndeclaredFields(filteredErrors_)) - case CodeActionType.fieldPermError => - val filteredErrors_ = filteredErrors.asInstanceOf[Seq[VerificationError]] - this.addCodeAction(first = false)(getCodeActionsForFieldPermissionError(filteredErrors_)) - } + .map(_ match { + // Support for red beams indicating branch failure + case (ErrorType.branchFailureInfo, errs : Seq[PostconditionViolatedBranch]) => + val branchFailureDetails = errs.map(err => BranchFailureDetails(err.readableMessage, + getBranchRange(this.file_uri, + lsp.Common.toPosition(err.pos), + err.leftIsFatal, + err.rightIsFatal) + )) + if (branchFailureDetails.nonEmpty) { + val params = lsp.StateChangeParams( + VerificationRunning.id, + uri=this.file_uri, + branchFailureDetails = branchFailureDetails.toArray + ) + coordinator.sendStateChangeNotification(params, Some(this)) + } + // Code actions + case (ErrorType.undeclaredField, errs : Seq[TypecheckerError]) => + this.addCodeAction(first = true)(getCodeActionsForUndeclaredFields(errs)) + case (ErrorType.fieldPermError, errs : Seq[VerificationError]) => + this.addCodeAction(first = false)(getCodeActionsForFieldPermissionError(errs)) }) } @@ -413,24 +427,7 @@ trait VerificationManager extends Manager with Branches { addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2)) } - // Add code actions - addCodeActions(errors) - - // Support for red beams indicating branch failure - val branchFailureDetails = errors.collect({case err: PostconditionViolatedBranch => - BranchFailureDetails(err.readableMessage, - getBranchRange(this.file_uri, - lsp.Common.toPosition(err.pos), - err.leftIsFatal, - err.rightIsFatal) - )}) - if (branchFailureDetails.nonEmpty) { - val params = lsp.StateChangeParams( - VerificationRunning.id, - uri=this.file_uri, - branchFailureDetails = branchFailureDetails.toArray - ) - coordinator.sendStateChangeNotification(params, Some(this)) - } + // Right now: Add red beams and code actions + processByType(errors) } } From 20d74e15364c9396c6aeb40dbb0acb9f0bb06a44 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 19 Feb 2025 22:28:10 +0100 Subject: [PATCH 17/44] Refactoring --- .../scala/viper/server/frontends/lsp/file/Verification.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 43061d73..227be364 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -333,7 +333,8 @@ trait VerificationManager extends Manager with Branches { .map(_ match { // Support for red beams indicating branch failure case (ErrorType.branchFailureInfo, errs : Seq[PostconditionViolatedBranch]) => - val branchFailureDetails = errs.map(err => BranchFailureDetails(err.readableMessage, + val branchFailureDetails = errs.map(err => + BranchFailureDetails(err.readableMessage, getBranchRange(this.file_uri, lsp.Common.toPosition(err.pos), err.leftIsFatal, From a2b809952f960b4ff6f49168bc576c182f35fa1d Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 20 Feb 2025 23:33:44 +0100 Subject: [PATCH 18/44] Fix while loop invariant code action --- .../frontends/lsp/ast/ParseAstLsp.scala | 84 +++++++++++-------- 1 file changed, 48 insertions(+), 36 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index f236eef6..cbe7bdc4 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -151,17 +151,26 @@ object HasCompletionProposals { object HasCodeActions { private def isIncreasingSelfAssignment(e: PBinExp): Boolean = { e.op.rs match { - case PSymOp.Plus | PSymOp.Mul | PKwOp.Union => true + case PSymOp.Plus | PSymOp.Mul | PKwOp.Union | PSymOp.Append => true case _ => false } } - private def getIdentifierNames(e: PExp) : Set[String] = e.deepCollect({case n: PIdnUseExp => n.name}).toSet + private def getIdentifierNames(e: PExp) : Set[String] = e.deepCollect( + { case n: PLookup => getIdentifierNames(n.base) + case n: PIdnUseExp => Set(n.name)} + ).reduceOption((s,e) => s union e) + .getOrElse(Set.empty) private def findSelfAssignment(stmts : PSeqn, idns: Set[String]) : Option[(String, PExp)] = { - stmts.find({case p: PAssign if p.rhs.isInstanceOf[PBinExp]=> ( - idns.intersect( - (p.targets.first ++ p.targets.inner.map(_._1)).map(_.deepCollect({case n: PIdnUseExp => n.name})) - .flatten.toSet.intersect(getIdentifierNames(p.rhs))).headOption, p.rhs)}) - .find(t => t._1.isDefined)}.map(t => (t._1.get, t._2)) + stmts.deepCollect({case p: PAssign if p.rhs.isInstanceOf[PBinExp]=> ( + idns.intersect((p.targets.first ++ p.targets.inner.map(_._1)) + .collect({ + case i: PLookup => getIdentifierNames(i) + case i: PIdnUseExp => Set(i.name)} + ).reduceOption((s,e) => s union e) + .getOrElse(Set.empty) + .intersect(getIdentifierNames(p.rhs))).headOption, p.rhs)}) + .find(t => t._1.isDefined)} + .map(t => (t._1.get, t._2)) private def containsIdn(ass: PAssign, idn: String): Boolean = { (ass.targets.first ++ ass.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]] .map(getIdentifierNames(_)).flatten.toSet @@ -185,17 +194,14 @@ object HasCodeActions { None } } - private def updateExp(e: PExp, j: Int): PExp = { - val newExp = e match { - case PIntLit(i) => PIntLit(i + j)(e.pos) - case _ => PBinExp(e, PReserved(if (j > 0) PSymOp.Plus else PSymOp.Minus)(e.pos), PIntLit(-j)(e.pos))(e.pos) - } - newExp + private def updateExp(e: PExp, j: Int): PExp = e match { + case PIntLit(i) => PIntLit(i + j)(e.pos) + case _ => PBinExp(e, PReserved(if (j > 0) PSymOp.Plus else PSymOp.Minus)(e.pos), PIntLit(-j)(e.pos))(e.pos) } private def getEditRange(n: PNode): Option[Range] = RangePosition(n) .map(Common.toRange(_)).map(r => {r.setEnd(r.getStart); r}) .headOption - private def getCodeActionAddingInvariant(w: PWhile) : CodeAction = { + private def getCodeActionsLoopInvariants(w: PWhile) : Seq[CodeAction] = { val cond = w.cond.inner.asInstanceOf[PBinExp] var condBound = cond.right var middle = cond.left @@ -205,33 +211,39 @@ object HasCodeActions { condBound = cond.left middle = cond.right } - val rp = RangePosition(w) + val whileRp = RangePosition(w) val editRange = getEditRange(w.body.ss.l) - (rp, editRange, selfAssignment) match { - case (Some(rp), Some(er), Some(sa)) => - val (idn, saRhs) = sa - val la = findClosestLiteralAssignment(w, idn) - - val bound = if (la.isDefined) la.get.pretty else "0" - val isIncrSelfAssign = isIncreasingSelfAssignment(saRhs.asInstanceOf[PBinExp]) - val updatedCondBound = if (cond.op.rs == PSymOp.Le || cond.op.rs == PSymOp.Ge) - updateExp(condBound, if (isIncrSelfAssign) 1 else -1) else condBound - val lowerBound = if (isIncrSelfAssign) bound else updatedCondBound.pretty - val upperBound = if (isIncrSelfAssign) updatedCondBound.pretty else bound - val decreasesExp = if (isIncrSelfAssign) s"$upperBound ${PSymOp.Minus.token} ${middle.pretty}" else middle.pretty - - val indent = " "*(rp.start.column-1) - val beforeInvKeyword = if (rp.start.line == er.getStart.getLine) "" else s"\n$indent" - val invariant = s"$beforeInvKeyword ${PKw.Invariant.keyword} $lowerBound ${PSymOp.Le.symbol} ${middle.pretty} ${PSymOp.Le.symbol} $upperBound\n" - val decreases = s"$indent ${PDecreasesKeyword.keyword} $decreasesExp\n$indent" - - CodeAction("Add loop invariant", invariant + decreases, er, SelectionBoundScope(rp), CodeActionKind.Empty, Seq.empty) - } + Seq((whileRp, selfAssignment, editRange)).collect({ + case (Some(wRp), Some(sa), Some(er)) => + val (idn, saRhs) = sa + val la = findClosestLiteralAssignment(w, idn) + + val bound = if (la.isDefined) la.get.pretty else "0" + val isIncrSelfAssign = isIncreasingSelfAssignment(saRhs.asInstanceOf[PBinExp]) + val updatedCondBound = if (cond.op.rs == PSymOp.Le || cond.op.rs == PSymOp.Ge) + updateExp(condBound, if (isIncrSelfAssign) 1 else -1) else condBound + val lowerBound = if (isIncrSelfAssign) bound else updatedCondBound.pretty + val upperBound = if (isIncrSelfAssign) updatedCondBound.pretty else bound + val decreasesExp = if (isIncrSelfAssign) s"$upperBound ${PSymOp.Minus.token} ${middle.pretty}" else middle.pretty + + val indent = " "*(wRp.start.column-1) + val invs = w.invs.first ++ w.invs.inner.map(_._2) + val prevLinePos = if (invs.nonEmpty) RangePosition(invs.last).getOrElse(wRp) else wRp + val optNewLine = if (prevLinePos.line == er.getStart.getLine+1) s"\n$indent" else "" + val invariant = s"$optNewLine ${PKw.Invariant.keyword} $lowerBound ${PSymOp.Le.symbol} ${middle.pretty} ${PSymOp.Le.symbol} $upperBound\n$indent" + val decreases = s"$optNewLine ${PDecreasesKeyword.keyword} $decreasesExp\n$indent" + + Seq( + CodeAction("Add invariant", invariant , er, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), + CodeAction("Add decreases", decreases, er, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) + ) + }).flatten } def apply(p: PProgram): Seq[CodeAction] = { p.deepCollect({ case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => w}) - .collect(getCodeActionAddingInvariant(_)) + .collect(getCodeActionsLoopInvariants(_)) + .flatten } } From 1d722dac6c028aebdee176dcdba2fde954c25ea1 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 21 Feb 2025 15:01:50 +0100 Subject: [PATCH 19/44] Support code action with client field declaration command --- .../frontends/lsp/ast/ParseAstLsp.scala | 4 ++-- .../lsp/ast/utility/CodeAction.scala | 7 +++++-- .../frontends/lsp/file/Verification.scala | 21 ++++++++----------- .../lsp/file/utility/Conversions.scala | 18 +++++++++++----- 4 files changed, 29 insertions(+), 21 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index cbe7bdc4..01bdf3bf 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -234,8 +234,8 @@ object HasCodeActions { val decreases = s"$optNewLine ${PDecreasesKeyword.keyword} $decreasesExp\n$indent" Seq( - CodeAction("Add invariant", invariant , er, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), - CodeAction("Add decreases", decreases, er, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) + CodeAction("Add invariant", CaEdit(invariant , er), SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), + CodeAction("Add decreases", CaEdit(decreases, er), SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) ) }).flatten } diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 930a7210..7ee85fc3 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -12,10 +12,13 @@ trait HasCodeActions { def getCodeActions: Seq[CodeAction] } +trait CaAction +case class CaEdit(edit : String, range : lsp4j.Range) extends CaAction +case class CaCommand(cmd : String, args : Seq[AnyRef]) extends CaAction + case class CodeAction( title: String, - edit: String, /* Workspace edit */ - editRange: lsp4j.Range, + action: CaAction, bound: SelectionBoundScopeTrait, kind: String, resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 227be364..e191adda 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -22,7 +22,7 @@ import viper.silver.parser.{PFieldAccess, PKw} import viper.silver.ast.{AbstractSourcePosition, FieldAccess, HasLineColumn, Label, LineColumnPosition, MemberWithSpec, Method, Position, Seqn, While} import org.eclipse.lsp4j import viper.server.frontends.lsp.{BranchFailureDetails, Common} -import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} +import viper.silver.ast.utility.lsp.{CaCommand, CaEdit, CodeAction, RangePosition, SelectionBoundScope} import viper.silver.verifier.errors.PostconditionViolatedBranch import viper.silver.verifier.reasons.InsufficientPermission @@ -253,13 +253,10 @@ trait VerificationManager extends Manager with Branches { } } - private case object ErrorType { - val branchFailureInfo : Int = 0 - val undeclaredField : Int = 1 - val fieldPermError : Int = 2 + private object ErrorType extends Enumeration(1) { + val branchFailureInfo, undeclaredField, fieldPermError = Value } - private val startOfFileRange = new lsp4j.Range(new lsp4j.Position(0, 0), new lsp4j.Position(0, 0)) private def getCodeActionsForUndeclaredFields(errors: Seq[TypecheckerError]) : Seq[CodeAction] = { errors.groupBy(_.node.get) .flatMap(fa => { @@ -270,8 +267,8 @@ trait VerificationManager extends Manager with Branches { getDiagnosticBy(Some(pos), None) }) faErrors.map(err => { - CodeAction("Add field declaration", s"field ${fieldAccess.idnref.pretty} : [your type]\n", - startOfFileRange, + CodeAction("Add field declaration", + CaCommand("viper.addFieldDeclaration", Seq(fieldAccess.idnref.pretty)), SelectionBoundScope(toRangePosition(err.pos)), lsp4j.CodeActionKind.QuickFix, faDiags) @@ -311,8 +308,8 @@ trait VerificationManager extends Manager with Branches { val parentRangePosition = toRangePosition(parent.pos) val indent = " "*(parentRangePosition.start.column-1) val beforeKeyword = if (closingBracketInSameLine) s"\n$indent " else " " - CodeAction("Add access precondition", s"$beforeKeyword$keyword acc($faStr)\n$indent", - new lsp4j.Range(editPos, editPos), + CodeAction("Add access precondition", + CaEdit(s"$beforeKeyword$keyword acc($faStr)\n$indent", new lsp4j.Range(editPos, editPos)), SelectionBoundScope(toRangePosition(err.pos)), lsp4j.CodeActionKind.QuickFix, faDiags) @@ -329,8 +326,7 @@ trait VerificationManager extends Manager with Branches { case e : VerificationError if e.reason.isInstanceOf[InsufficientPermission] && e.reason.offendingNode.isInstanceOf[FieldAccess] => ErrorType.fieldPermError case _ => -1 - }).filter(t => t._1 >= 0) - .map(_ match { + }).map(_ match { // Support for red beams indicating branch failure case (ErrorType.branchFailureInfo, errs : Seq[PostconditionViolatedBranch]) => val branchFailureDetails = errs.map(err => @@ -353,6 +349,7 @@ trait VerificationManager extends Manager with Branches { this.addCodeAction(first = true)(getCodeActionsForUndeclaredFields(errs)) case (ErrorType.fieldPermError, errs : Seq[VerificationError]) => this.addCodeAction(first = false)(getCodeActionsForFieldPermissionError(errs)) + case _ => }) } diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index 4597e4fb..d54fc51f 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -12,6 +12,8 @@ import viper.silver.ast.utility.lsp import viper.server.frontends.lsp.{Common, Lsp4jSemanticHighlight} import viper.server.frontends.lsp.file.{Diagnostic, FindReferences} import ch.qos.logback.classic.Logger +import org.eclipse.lsp4j.Command +import viper.silver.ast.utility.lsp.{CaCommand, CaEdit} import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer @@ -216,11 +218,17 @@ case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAc override def translate(cas: Seq[lsp.CodeAction])(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean))(implicit log: Logger): Seq[lsp4j.CodeAction] = { cas.map(ca => { val codeAction = new lsp4j.CodeAction(ca.title) - val textEdits = Seq(new lsp4j.TextEdit(ca.editRange, ca.edit)).asJava - val uri = ca.bound.scope.file.toUri().toString() - val edits = Map(uri -> textEdits).asJava - val workspaceEdit = new lsp4j.WorkspaceEdit(edits) - codeAction.setEdit(workspaceEdit) + ca.action match { + case CaCommand(cmd, args) => + codeAction.setCommand(new Command(ca.title, cmd, args.asJava)) + case CaEdit(edit, range) => + val textEdits = Seq(new lsp4j.TextEdit(range, edit)).asJava + val uri = ca.bound.scope.file.toUri().toString() + val edits = Map(uri -> textEdits).asJava + val workspaceEdit = new lsp4j.WorkspaceEdit(edits) + codeAction.setEdit(workspaceEdit) + case _=> + } codeAction.setDiagnostics(ca.resolvedDiags.asJava) codeAction.setKind(ca.kind) codeAction From 8f359f9862b417d8239c1c88ff752a30f74c856e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 21 Feb 2025 15:13:26 +0100 Subject: [PATCH 20/44] Shorten name of code action --- .../scala/viper/server/frontends/lsp/file/Verification.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index e191adda..f874bd65 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -267,7 +267,7 @@ trait VerificationManager extends Manager with Branches { getDiagnosticBy(Some(pos), None) }) faErrors.map(err => { - CodeAction("Add field declaration", + CodeAction("Declare field", CaCommand("viper.addFieldDeclaration", Seq(fieldAccess.idnref.pretty)), SelectionBoundScope(toRangePosition(err.pos)), lsp4j.CodeActionKind.QuickFix, From 63ee57c33d9945ffd443af23857b1b5f9aba5101 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 21 Feb 2025 15:14:02 +0100 Subject: [PATCH 21/44] Shorten name of code action --- .../scala/viper/server/frontends/lsp/file/Verification.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index f874bd65..a074ad51 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -268,7 +268,7 @@ trait VerificationManager extends Manager with Branches { }) faErrors.map(err => { CodeAction("Declare field", - CaCommand("viper.addFieldDeclaration", Seq(fieldAccess.idnref.pretty)), + CaCommand("viper.declareField", Seq(fieldAccess.idnref.pretty)), SelectionBoundScope(toRangePosition(err.pos)), lsp4j.CodeActionKind.QuickFix, faDiags) From 6d2b0422d96bcd96e58d0d12e0a72fd17e1bb0a4 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 26 Feb 2025 14:18:00 +0100 Subject: [PATCH 22/44] Alternate fix --- .../scala/viper/server/frontends/lsp/ClientCoordinator.scala | 4 ++-- .../scala/viper/server/frontends/lsp/file/FileContent.scala | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index c6ffcf29..fc6ad1a7 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -79,7 +79,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif if (server.isRunning) { logger.trace("server is running") // This should only be necessary if one wants to verify a closed file for some reason - val fm = getFileManager(uri, Some(content)) + val fm = getFileManager(uri, Option(content)) // This will be the new project root makeEmptyRoot(fm) true @@ -212,7 +212,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif fm } def ensureFmExists(uri: String, content: String): FileManager = { - getFileManager(uri, Some(content)) + getFileManager(uri, Option(content)) } def getRoot(uri: String): FileManager = { val fm = getFileManager(uri) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 26db27c3..095c669f 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -29,7 +29,6 @@ case class FileContent(path: Path) extends DiskLoader { val fileContent = new ArrayBuffer[String] def set(newContent: String): Unit = { - if (newContent == null) return fileContent.clear() fileContent.addAll(newContent.split("\n", -1)) } From 74e4203b18bbb52e477e30e017cb288b59408448 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 27 Feb 2025 14:20:18 +0100 Subject: [PATCH 23/44] Do not hardcode keyword --- src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 01bdf3bf..c68e0172 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -111,7 +111,7 @@ object HasSignatureHelps { case n: PDefine => { val bound = SelectionBoundKeyword(n.idndef.name) // Start - val start = SignatureHelpPart(false, s"define ${n.idndef.pretty}", None) + val start = SignatureHelpPart(false, s"${n.define.pretty} ${n.idndef.pretty}", None) // Args var mappedParams = Seq[SignatureHelpPart]() if (n.parameters.isDefined) { From c624ff9e867006abf1f6a36d67b16b6dcce2e7ce Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 27 Feb 2025 14:36:51 +0100 Subject: [PATCH 24/44] refactoring signature help --- .../server/frontends/lsp/ast/ParseAstLsp.scala | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index c68e0172..94d2be4b 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -93,19 +93,20 @@ object HasSignatureHelps { def apply(p: PProgram): Seq[SignatureHelp] = { def argsToSigHelpPart[T <: PNode](args: PDelimited.Comma[PSym.Paren, T]) : Seq[SignatureHelpPart] = { def getSigHelpPart[T <: PNode](arg: T): SignatureHelpPart = SignatureHelpPart(true, arg.pretty, None) - args.inner.first.map(getSigHelpPart).toSeq ++ args.inner.inner.flatMap { + SignatureHelpPart(false, s"${args.l.pretty}", None) +: + (args.inner.first.map(getSigHelpPart).toSeq ++ args.inner.inner.flatMap { case (c, arg) => Seq(SignatureHelpPart(false, c.pretty, None), getSigHelpPart(arg)) - } + }) :+ SignatureHelpPart(false, s"${args.r.pretty}", None) } p.deepCollect({ case n: PCallable => { val bound = SelectionBoundKeyword(n.idndef.name) // Start - val start = SignatureHelpPart(false, s"${n.keyword.pretty}${n.idndef.pretty}${n.args.l.pretty}", None) + val start = SignatureHelpPart(false, s"${n.keyword.pretty}${n.idndef.pretty}", None) // Args val args = argsToSigHelpPart[PAnyFormalArgDecl](n.args) // Tail - val tail = SignatureHelpPart(false, s"${n.args.r.pretty}${n.returnNodes.map(_.pretty).mkString}", None) + val tail = SignatureHelpPart(false, s"${n.returnNodes.map(_.pretty).mkString}", None) Seq(SignatureHelp(start +: args :+ tail, PLspDeclaration.documentation(n), bound)) } case n: PDefine => { @@ -113,11 +114,9 @@ object HasSignatureHelps { // Start val start = SignatureHelpPart(false, s"${n.define.pretty} ${n.idndef.pretty}", None) // Args - var mappedParams = Seq[SignatureHelpPart]() - if (n.parameters.isDefined) { - val params = n.parameters.get - mappedParams = argsToSigHelpPart[PDefineParam](n.parameters.get) - mappedParams = SignatureHelpPart(false, s"${params.l.pretty}", None) +: mappedParams :+ SignatureHelpPart(false, s"${params.r.pretty}", None) + val mappedParams = n.parameters match { + case Some(params) => argsToSigHelpPart[PDefineParam](params) + case _ => Seq.empty } // Tail val tail = SignatureHelpPart(false, s" ${n.body.pretty}", None) From fcf92b2938e261ecb701a7baa1a1fd3b36e8fac3 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 3 Mar 2025 22:53:20 +0100 Subject: [PATCH 25/44] Clean up --- carbon | 2 +- silicon | 2 +- src/main/scala/viper/server/ViperConfig.scala | 2 +- .../frontends/lsp/ClientCoordinator.scala | 9 ++ .../frontends/lsp/CommandProtocol.scala | 1 + .../viper/server/frontends/lsp/Common.scala | 12 +- .../server/frontends/lsp/DataProtocol.scala | 7 +- .../frontends/lsp/IdeLanguageClient.scala | 3 + .../frontends/lsp/ast/ParseAstLsp.scala | 47 +++++- .../frontends/lsp/file/FileContent.scala | 19 +++ .../frontends/lsp/file/RelayActor.scala | 25 ++- .../frontends/lsp/file/Verification.scala | 150 +----------------- .../viper/server/core/CoreServerSpec.scala | 3 +- 13 files changed, 121 insertions(+), 161 deletions(-) diff --git a/carbon b/carbon index 27f3f1f1..8db5b30c 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 27f3f1f13a84c2345564d79a615081b3600195a3 +Subproject commit 8db5b30c679cdc57316c8d9dd1c278089bea6ea1 diff --git a/silicon b/silicon index ec2474e9..5f699cc7 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit ec2474e961016f3dbe083c418d365441c5691a37 +Subproject commit 5f699cc7ba7af07b660f2d57912d3d3e04553903 diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala index 53ea337a..255eca32 100644 --- a/src/main/scala/viper/server/ViperConfig.scala +++ b/src/main/scala/viper/server/ViperConfig.scala @@ -89,7 +89,7 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) { } isLSP } else true, - default = Some(false), + default = Some(true), noshort = true ) diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index fc6ad1a7..17457848 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -173,6 +173,15 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif } } + /** Notifies the client about details of branch failure for displaying red beams */ + def sendBranchFailureDetails(details: BranchFailureDetails): Unit = { + try { + client.sendBranchFailureDetails(details) + } catch { + case e: Throwable => logger.debug(s"Error while sending branch failure details: $e") + } + } + def refreshEndings(): Future[Array[String]] = { client.requestVprFileEndings().asScala.map(response => { _vprFileEndings = Some(response.fileEndings) diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala index e67e5a37..0578b3b6 100644 --- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala @@ -36,4 +36,5 @@ object S2C_Commands { // final val StepsAsDecorationOptions = "StepsAsDecorationOptions" // final val HeapGraph = "HeapGraph" final val UnhandledViperServerMessageType = "UnhandledViperServerMessageType" + final val BranchFailureDetails = "BranchFailureDetails" } diff --git a/src/main/scala/viper/server/frontends/lsp/Common.scala b/src/main/scala/viper/server/frontends/lsp/Common.scala index ef671e4d..5de811e6 100644 --- a/src/main/scala/viper/server/frontends/lsp/Common.scala +++ b/src/main/scala/viper/server/frontends/lsp/Common.scala @@ -9,10 +9,10 @@ package viper.server.frontends.lsp import java.net.URI import java.nio.file.{Path, Paths} -import org.eclipse.lsp4j.{Position, Range} +import org.eclipse.lsp4j.{Position, Range, Location} import scala.collection.mutable.ArrayBuffer import viper.silver.ast -import org.eclipse.lsp4j.Location +import viper.silver.ast.utility.lsp object Common { @@ -28,6 +28,14 @@ object Common { Paths.get(uri).getFileName.toString } + def toRangePosition(path: Path, pos: ast.Position) : lsp.RangePosition = { + pos match { + case sp: ast.AbstractSourcePosition => lsp.RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) + case pos: ast.HasLineColumn => lsp.RangePosition(path, pos, pos) + case _ => lsp.RangePosition(path, ast.LineColumnPosition(1, 1), ast.LineColumnPosition(1, 1)) + } + } + def toPosition(pos: ast.Position): Position = pos match { case lc: ast.HasLineColumn => new Position(lc.line - 1, lc.column - 1) case ast.NoPosition => new Position(0, 0) diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index 3b41099c..5c2dea13 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -62,8 +62,6 @@ object BackendOutputType { case class ProgressParams(data: Progress, logLevel: Int) -case class BranchFailureDetails(errorMessage: String, /*tree string*/ range: Range) - case class Progress ( domain: String, current: Double, @@ -176,8 +174,9 @@ case class StateChangeParams( verificationNeeded: Double = -1, uri: String = null, stage: String = null, - error: String = null, - branchFailureDetails: Array[BranchFailureDetails] = null) + error: String = null) + +case class BranchFailureDetails(uri: String, /*errorMessage: String, tree string*/ ranges: Array[Range]) case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int) diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala index 0b614f3b..ebccd700 100644 --- a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala +++ b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala @@ -41,4 +41,7 @@ trait IdeLanguageClient extends LanguageClient { @JsonNotification(S2C_Commands.StateChange) def notifyStateChanged(params: StateChangeParams): Unit + + @JsonNotification(S2C_Commands.BranchFailureDetails) + def sendBranchFailureDetails(params: BranchFailureDetails): Unit } diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 94d2be4b..064c2922 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -6,7 +6,7 @@ package viper.silver.parser -import org.eclipse.lsp4j.{CodeActionKind, Range} +import org.eclipse.lsp4j.{CodeActionKind, Diagnostic, Position, Range} import viper.server.frontends.lsp.Common import viper.silver.ast.utility.lsp._ import viper.silver.ast.LineColumnPosition @@ -239,9 +239,48 @@ object HasCodeActions { }).flatten } - def apply(p: PProgram): Seq[CodeAction] = { - p.deepCollect({ case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => w}) - .collect(getCodeActionsLoopInvariants(_)) + private def getCodeActionsForUndeclaredFields(fas: Seq[PFieldAccess], getDiagnostic : Function[Position, Seq[Diagnostic]]) : Seq[CodeAction] = { + fas.map(f => (f,RangePosition(f))).collect { + case (f, Some(fRp)) => + CodeAction("Declare field", + CaCommand("viper.declareField", Seq(f.idnref.pretty)), + SelectionBoundScope(fRp), + CodeActionKind.QuickFix, + getDiagnostic(Common.toPosition(f.pos._1))) + } + } + + private def getCodeActionsFieldAccess(fas : Seq[PFieldAccess], getDiagnostic : Function[Position, Seq[Diagnostic]]): Seq[CodeAction] = { + fas.flatMap(f => { + val seqn = f.getAncestor[PSeqn] + var parentWithSpec : Option[PMemberWithSpec] = None + if (seqn.isDefined) { + parentWithSpec = seqn.get.getAncestor[PMemberWithSpec] + } + parentWithSpec.collect({ + case w : PWhile => (RangePosition(f), RangePosition(w),PKw.Invariant.keyword,RangePosition(w.body.ss.l)) + case m : PMethod => (RangePosition(f), RangePosition(m),PKw.Requires.keyword,RangePosition(m.body.get.ss.l)) + }).collect( { + case (Some(fRp), Some(parentRp), keyword, Some(openingBracketRp)) => + val openingBracketInSameLine = openingBracketRp.line == parentRp.line + val editPos = if (openingBracketInSameLine) Common.toPosition(openingBracketRp.start) else + {val p = Common.toPosition(parentRp.start);p.setLine(p.getLine+1);p} + val indent = " "*(parentRp.start.column-1) + val beforeKeyword = if (openingBracketInSameLine) s"\n$indent " else " " + CodeAction("Add access precondition", + CaEdit(s"$beforeKeyword$keyword acc(${f.pretty})\n$indent", new Range(editPos, editPos)), + SelectionBoundScope(fRp), + CodeActionKind.QuickFix, + getDiagnostic(Common.toPosition(f.pos._1))) + }).toSeq + }) + } + + def apply(p: PProgram, getDiagnostic : Function[Position, Seq[Diagnostic]]): Seq[CodeAction] = { + p.deepCollect({ + case w: PWhile if w.cond.inner.isInstanceOf[PBinExp] => getCodeActionsLoopInvariants(w) + case f: PFieldAccess => getCodeActionsForUndeclaredFields(Seq(f),getDiagnostic) ++ getCodeActionsFieldAccess(Seq(f),getDiagnostic) + }) .flatten } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 095c669f..21a4f552 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -6,13 +6,18 @@ package viper.server.frontends.lsp.file +import org.eclipse.lsp4j + import scala.util.{Success, Try} import scala.collection.mutable.ArrayBuffer import org.eclipse.lsp4j.Range import viper.silver.ast.utility.DiskLoader + import java.nio.file.Path import org.eclipse.lsp4j.Position import viper.server.frontends.lsp.Common +import viper.silver.ast.utility.lsp.RangePosition +import viper.silver.ast.{LineColumnPosition, Method} case class FileContent(path: Path) extends DiskLoader { case class FileContentIter(fc: FileContent, delta: Int, var currPos: Option[Position]) extends Iterator[(Char, Position)] { @@ -93,6 +98,20 @@ case class FileContent(path: Path) extends DiskLoader { } }) } + def getMethodIdentifierRangePosition(method: Method) : RangePosition = { + val methodIdentifier = iterForward(Common.toPosition(method.pos)) + .dropWhile(c => c._1.isLetter) + .find({ case (c, _) => Common.isIdentChar(c) }) + .map(t => getIdentAtPos(t._2)) + .getOrElse(None) + + methodIdentifier.map(i => { + val (_, identRange) = i + new RangePosition(path, + LineColumnPosition(identRange.getStart.getLine+1, identRange.getStart.getCharacter+1), + LineColumnPosition(identRange.getEnd.getLine+1, identRange.getEnd.getCharacter+1)) + }).getOrElse(Common.toRangePosition(path, method.pos)) + } def inComment(pos: Position): Boolean = { normalize(pos).map(nPos => { var isComment = false diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 16963da8..81552b8a 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,7 +7,10 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} +import org.eclipse.lsp4j +import org.eclipse.lsp4j.Position import viper.server.frontends.lsp +import viper.server.frontends.lsp.{BranchFailureDetails, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast @@ -139,8 +142,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.addSignatureHelp(true)(HasSignatureHelps(pProgram)) task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram)) task.addCompletionProposal(true)(HasCompletionProposals(pProgram)) - // Only for code actions not associated to a diagnostic, others are added in processErrors - task.addCodeAction(true)(HasCodeActions(pProgram)) + task.addCodeAction(true)(HasCodeActions(pProgram,(pos:Position)=>task.getDiagnosticBy(Some(pos),None))) } case StatisticsReport(m, f, p, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") @@ -158,6 +160,25 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] InvalidArgumentsReport") markErrorsAsReported(errors) task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) + case BranchTreeReport(method,tree,beams) => + task.addDiagnostic(false)( + Seq(Diagnostic( + backendClassName=backendClassName, + position=task.content.getMethodIdentifierRangePosition(method), + message=tree, + severity=lsp4j.DiagnosticSeverity.Error, + cached = false, + errorMsgPrefix=None + ))) + val details = beams.map(b => + task.getBranchRange(task.file_uri, + Common.toPosition(b.e.pos), + b.isLeftFatal, + b.isRightFatal) + ).toArray + if (details.nonEmpty) coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri,details) + ) case EntitySuccessMessage(_, concerning, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntitySuccessMessage") if (task.progress == null) { diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index a074ad51..803b0b20 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -17,14 +17,10 @@ import akka.actor.Props import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ import akka.actor.ActorRef -import viper.silver.verifier.{AbstractError, TypecheckerError, VerificationError} -import viper.silver.parser.{PFieldAccess, PKw} -import viper.silver.ast.{AbstractSourcePosition, FieldAccess, HasLineColumn, Label, LineColumnPosition, MemberWithSpec, Method, Position, Seqn, While} +import viper.silver.verifier.AbstractError +import viper.silver.ast.{AbstractSourcePosition, Position} import org.eclipse.lsp4j -import viper.server.frontends.lsp.{BranchFailureDetails, Common} -import viper.silver.ast.utility.lsp.{CaCommand, CaEdit, CodeAction, RangePosition, SelectionBoundScope} -import viper.silver.verifier.errors.PostconditionViolatedBranch -import viper.silver.verifier.reasons.InsufficientPermission +import viper.server.frontends.lsp.Common import java.nio.file.Path @@ -245,140 +241,6 @@ trait VerificationManager extends Manager with Branches { } } - private def toRangePosition(pos: Position) : RangePosition = { - pos match { - case sp: AbstractSourcePosition => RangePosition(sp.file, sp.start, sp.end.getOrElse(sp.start)) - case pos: HasLineColumn => RangePosition(path, pos, pos) - case _ => RangePosition(path, LineColumnPosition(1, 1), LineColumnPosition(1, 1)) - } - } - - private object ErrorType extends Enumeration(1) { - val branchFailureInfo, undeclaredField, fieldPermError = Value - } - - private def getCodeActionsForUndeclaredFields(errors: Seq[TypecheckerError]) : Seq[CodeAction] = { - errors.groupBy(_.node.get) - .flatMap(fa => { - val (faNode, faErrors) = fa - val fieldAccess = faNode.asInstanceOf[PFieldAccess] - val faDiags = faErrors.flatMap(e => { - val pos = Common.toPosition(e.pos) - getDiagnosticBy(Some(pos), None) - }) - faErrors.map(err => { - CodeAction("Declare field", - CaCommand("viper.declareField", Seq(fieldAccess.idnref.pretty)), - SelectionBoundScope(toRangePosition(err.pos)), - lsp4j.CodeActionKind.QuickFix, - faDiags) - }) - }).toSeq - } - private def getCodeActionsForFieldPermissionError(errors: Seq[VerificationError]) : Seq[CodeAction] = { - errors.groupBy(_.reason.offendingNode.toString()).flatMap(fa => { - val (faStr, faErrors) = fa - val faDiags = faErrors.flatMap(err => { - val pos = Common.toPosition(err.pos) - getDiagnosticBy(Some(pos), None) - }) - faErrors.flatMap(err => { - val f = err.reason.offendingNode - val seqn = f.getAncestor[Seqn] - var parentWithSpec : Option[MemberWithSpec] = None - if (seqn.isDefined) { - parentWithSpec = seqn.get.getAncestor[MemberWithSpec] - } - parentWithSpec.collect({ - case l : Label => (l,PKw.Invariant.keyword) - case w : While => (w,PKw.Invariant.keyword) - case m : Method => (m,PKw.Requires.keyword) - }).map( t => { - val (parent, keyword) = t - val parentPosFile = Common.toPosition(parent.pos) - val m = getInProject(this.file_uri).content - val closingBracketPos = m.iterForward(parentPosFile) - .find { case (c, _) => c == '{'} - .map(t => {val p = t._2; p.setCharacter(p.getCharacter-1); p}) - val closingBracketInSameLine = closingBracketPos - .map(p => p.getLine == parentPosFile.getLine) - .getOrElse(false) - val editPos = if (closingBracketInSameLine) closingBracketPos.get else - {val p = Common.toPosition(parent.pos);p.setLine(p.getLine+1);p} - val parentRangePosition = toRangePosition(parent.pos) - val indent = " "*(parentRangePosition.start.column-1) - val beforeKeyword = if (closingBracketInSameLine) s"\n$indent " else " " - CodeAction("Add access precondition", - CaEdit(s"$beforeKeyword$keyword acc($faStr)\n$indent", new lsp4j.Range(editPos, editPos)), - SelectionBoundScope(toRangePosition(err.pos)), - lsp4j.CodeActionKind.QuickFix, - faDiags) - }).toSeq - }) - }).toSeq - } - - private def processByType(errors : Seq[AbstractError]) = { - errors.groupBy({ - case _: PostconditionViolatedBranch => ErrorType.branchFailureInfo - case e: TypecheckerError if e.node.isDefined - && e.node.get.isInstanceOf[PFieldAccess] => ErrorType.undeclaredField - case e : VerificationError if e.reason.isInstanceOf[InsufficientPermission] - && e.reason.offendingNode.isInstanceOf[FieldAccess] => ErrorType.fieldPermError - case _ => -1 - }).map(_ match { - // Support for red beams indicating branch failure - case (ErrorType.branchFailureInfo, errs : Seq[PostconditionViolatedBranch]) => - val branchFailureDetails = errs.map(err => - BranchFailureDetails(err.readableMessage, - getBranchRange(this.file_uri, - lsp.Common.toPosition(err.pos), - err.leftIsFatal, - err.rightIsFatal) - )) - if (branchFailureDetails.nonEmpty) { - val params = lsp.StateChangeParams( - VerificationRunning.id, - uri=this.file_uri, - branchFailureDetails = branchFailureDetails.toArray - ) - coordinator.sendStateChangeNotification(params, Some(this)) - } - // Code actions - case (ErrorType.undeclaredField, errs : Seq[TypecheckerError]) => - this.addCodeAction(first = true)(getCodeActionsForUndeclaredFields(errs)) - case (ErrorType.fieldPermError, errs : Seq[VerificationError]) => - this.addCodeAction(first = false)(getCodeActionsForFieldPermissionError(errs)) - case _ => - }) - } - - def getMethodIdentifier(error: PostconditionViolatedBranch): Option[(String, lsp4j.Range)] = { - val content = getInProject(this.file_uri).content - error.offendingNode.getAncestor[Method].map(m => - content.iterForward(Common.toPosition(m.pos)) - .dropWhile(c => c._1.isLetter) - .find({ case (c, _) => Common.isIdentChar(c) }) - .map(t => content.getIdentAtPos(t._2)) - .getOrElse(None) - ).getOrElse(None) - } - - private def getErrorRangeAndPos(error: AbstractError) : (lsp4j.Range, RangePosition) = { - val range = toRange(error.pos) - val rp = toRangePosition(error.pos) - error match { - case e : PostconditionViolatedBranch => - getMethodIdentifier(e).map(i => { - val (_, identRange) = i - (identRange, new RangePosition(path, - LineColumnPosition(identRange.getStart.getLine+1, identRange.getStart.getCharacter+1), - LineColumnPosition(identRange.getEnd.getLine+1, identRange.getEnd.getCharacter+1))) - }).getOrElse((range,rp)) - case _ => (range,rp) - } - } - def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { // Add diagnostics val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") @@ -408,7 +270,8 @@ trait VerificationManager extends Manager with Branches { errorType = "Verification error" } - val (range,rp) = getErrorRangeAndPos(err) + val range = toRange(err.pos) + val rp = Common.toRangePosition(path,err.pos) val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" @@ -424,8 +287,5 @@ trait VerificationManager extends Manager with Branches { diags.groupBy(d => d._1).foreach { case (phase, diags) => addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2)) } - - // Right now: Add red beams and code actions - processByType(errors) } } diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index b723514e..9c083318 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -16,7 +16,7 @@ import org.scalatest.matchers.should.Matchers import org.scalatest.{Assertion, Outcome, Succeeded} import org.scalatest.wordspec.AnyWordSpec import viper.server.ViperConfig -import viper.server.frontends.lsp.{ClientCoordinator, GetIdentifierResponse, GetRangeResponse, GetViperFileEndingsResponse, HintMessage, IdeLanguageClient, LogParams, SetupProjectParams, StateChangeParams, UnhandledViperServerMessageTypeParams, VerificationNotStartedParams, ViperServerService} +import viper.server.frontends.lsp.{BranchFailureDetails, ClientCoordinator, GetIdentifierResponse, GetRangeResponse, GetViperFileEndingsResponse, HintMessage, IdeLanguageClient, LogParams, SetupProjectParams, StateChangeParams, UnhandledViperServerMessageTypeParams, VerificationNotStartedParams, ViperServerService} import viper.server.frontends.lsp.file.FileManager import viper.server.utility.AstGenerator import viper.server.vsi.{DefaultVerificationServerStart, JobNotFoundException, VerJobId} @@ -431,6 +431,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { override def notifyUnhandledViperServerMessage(params: UnhandledViperServerMessageTypeParams): Unit = {} override def notifyVerificationNotStarted(params: VerificationNotStartedParams): Unit = {} override def notifyStateChanged(params: StateChangeParams): Unit = {} + override def sendBranchFailureDetails(params: BranchFailureDetails): Unit = {} override def telemetryEvent(`object`: Any): Unit = {} override def publishDiagnostics(diagnostics: PublishDiagnosticsParams): Unit = {} override def showMessage(messageParams: MessageParams): Unit = {} From e45372389ba3230ef60d23f4bbb2672fd403f710 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 3 Mar 2025 22:59:15 +0100 Subject: [PATCH 26/44] Change back default --- src/main/scala/viper/server/ViperConfig.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala index 255eca32..53ea337a 100644 --- a/src/main/scala/viper/server/ViperConfig.scala +++ b/src/main/scala/viper/server/ViperConfig.scala @@ -89,7 +89,7 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) { } isLSP } else true, - default = Some(true), + default = Some(false), noshort = true ) From 8507c942bb9113837fca95e248ae0c578881b889 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 13:11:14 +0100 Subject: [PATCH 27/44] Code Action for displaying DOT representation of explored branches --- carbon | 2 +- silicon | 2 +- .../frontends/lsp/ast/utility/CodeAction.scala | 3 ++- .../server/frontends/lsp/file/RelayActor.scala | 15 ++++++++++++--- .../frontends/lsp/file/utility/Conversions.scala | 1 + 5 files changed, 17 insertions(+), 6 deletions(-) diff --git a/carbon b/carbon index 8db5b30c..ba34f1c5 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 8db5b30c679cdc57316c8d9dd1c278089bea6ea1 +Subproject commit ba34f1c54e9e094dec044c8cf2dcf605f33d10be diff --git a/silicon b/silicon index 5f699cc7..5046b6b5 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 5f699cc7ba7af07b660f2d57912d3d3e04553903 +Subproject commit 5046b6b56b3c34ef8909ca7fbcd678d40132d030 diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 7ee85fc3..5c989ca1 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -21,7 +21,8 @@ case class CodeAction( action: CaAction, bound: SelectionBoundScopeTrait, kind: String, - resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty + resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty, + branchTree : Option[viper.silver.reporter.BranchTree] = None ) extends SelectableInBound with HasRangePositions { override def rangePositions: Seq[RangePosition] = bound.rangePositions } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 81552b8a..6e815aad 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -8,12 +8,13 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} import org.eclipse.lsp4j -import org.eclipse.lsp4j.Position +import org.eclipse.lsp4j.{CodeActionKind, Position} import viper.server.frontends.lsp import viper.server.frontends.lsp.{BranchFailureDetails, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast +import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} import viper.silver.parser._ @@ -161,15 +162,23 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends markErrorsAsReported(errors) task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) case BranchTreeReport(method,tree,beams) => + val mRp = task.content.getMethodIdentifierRangePosition(method) task.addDiagnostic(false)( Seq(Diagnostic( backendClassName=backendClassName, - position=task.content.getMethodIdentifierRangePosition(method), - message=tree, + position=mRp, + message=s"BranchFails.\n${tree.prettyPrint()}", severity=lsp4j.DiagnosticSeverity.Error, cached = false, errorMsgPrefix=None ))) + task.addCodeAction(false)(Seq( + CodeAction("Display explored branches", + CaCommand("viper.displayExploredBranches", Seq("/home/stephanie/viperserver/tmp/BranchTree.dot")), + SelectionBoundScope(mRp), + CodeActionKind.QuickFix, + branchTree=Some(tree)) + )) val details = beams.map(b => task.getBranchRange(task.file_uri, Common.toPosition(b.e.pos), diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index d54fc51f..a0d7b254 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -217,6 +217,7 @@ case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAc override def translate(ca: lsp.CodeAction)(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)): lsp4j.CodeAction = ??? override def translate(cas: Seq[lsp.CodeAction])(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean))(implicit log: Logger): Seq[lsp4j.CodeAction] = { cas.map(ca => { + if (ca.branchTree.isDefined) ca.branchTree.get.toDotFile() // TODO val codeAction = new lsp4j.CodeAction(ca.title) ca.action match { case CaCommand(cmd, args) => From 9f6b54a0e2b105bc918e7b5f65d0b2e676cb82f9 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 21:40:26 +0100 Subject: [PATCH 28/44] Add space --- src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 6e815aad..25f0f08b 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -167,7 +167,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends Seq(Diagnostic( backendClassName=backendClassName, position=mRp, - message=s"BranchFails.\n${tree.prettyPrint()}", + message=s"Branch fails.\n${tree.prettyPrint()}", severity=lsp4j.DiagnosticSeverity.Error, cached = false, errorMsgPrefix=None From 2d686116ae5bd49d308d31c7c997977f2121117a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 21:53:32 +0100 Subject: [PATCH 29/44] Renaming --- .../scala/viper/server/frontends/lsp/file/FileContent.scala | 4 +--- .../scala/viper/server/frontends/lsp/file/RelayActor.scala | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index 21a4f552..214e75b8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -6,8 +6,6 @@ package viper.server.frontends.lsp.file -import org.eclipse.lsp4j - import scala.util.{Success, Try} import scala.collection.mutable.ArrayBuffer import org.eclipse.lsp4j.Range @@ -98,7 +96,7 @@ case class FileContent(path: Path) extends DiskLoader { } }) } - def getMethodIdentifierRangePosition(method: Method) : RangePosition = { + def methodIdentToRangePosition(method: Method) : RangePosition = { val methodIdentifier = iterForward(Common.toPosition(method.pos)) .dropWhile(c => c._1.isLetter) .find({ case (c, _) => Common.isIdentChar(c) }) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 25f0f08b..0912c9b8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -162,7 +162,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends markErrorsAsReported(errors) task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) case BranchTreeReport(method,tree,beams) => - val mRp = task.content.getMethodIdentifierRangePosition(method) + val mRp = task.content.methodIdentToRangePosition(method) task.addDiagnostic(false)( Seq(Diagnostic( backendClassName=backendClassName, From b5ebe1cd0e57d544c83192b0e44a2e11bcdbf13a Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 4 Mar 2025 23:53:47 +0100 Subject: [PATCH 30/44] Add method name for tab title (displaying dot) --- .../scala/viper/server/frontends/lsp/file/RelayActor.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 0912c9b8..885d228e 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -13,6 +13,7 @@ import viper.server.frontends.lsp import viper.server.frontends.lsp.{BranchFailureDetails, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ +import viper.silicon.state.Tree import viper.silver.ast import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} import viper.silver.reporter._ @@ -174,7 +175,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends ))) task.addCodeAction(false)(Seq( CodeAction("Display explored branches", - CaCommand("viper.displayExploredBranches", Seq("/home/stephanie/viperserver/tmp/BranchTree.dot")), + CaCommand("viper.displayExploredBranches", Seq(method.name, Tree.DotFilePath)), SelectionBoundScope(mRp), CodeActionKind.QuickFix, branchTree=Some(tree)) From c7003165f00d2ad0506e123e1eba4f8630c5d67e Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 7 Mar 2025 22:55:18 +0100 Subject: [PATCH 31/44] Switch back from reporting to errors --- .../lsp/ast/utility/CodeAction.scala | 3 +- .../frontends/lsp/file/RelayActor.scala | 33 +------------------ .../frontends/lsp/file/Verification.scala | 31 +++++++++++++++-- 3 files changed, 32 insertions(+), 35 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 5c989ca1..515c4eb8 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -7,6 +7,7 @@ package viper.silver.ast.utility.lsp import org.eclipse.lsp4j +import viper.silver.verifier.errors.BranchTree trait HasCodeActions { def getCodeActions: Seq[CodeAction] @@ -22,7 +23,7 @@ case class CodeAction( bound: SelectionBoundScopeTrait, kind: String, resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty, - branchTree : Option[viper.silver.reporter.BranchTree] = None + branchTree : Option[BranchTree] = None ) extends SelectableInBound with HasRangePositions { override def rangePositions: Seq[RangePosition] = bound.rangePositions } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 885d228e..89a0009b 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,15 +7,11 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} -import org.eclipse.lsp4j -import org.eclipse.lsp4j.{CodeActionKind, Position} +import org.eclipse.lsp4j.Position import viper.server.frontends.lsp -import viper.server.frontends.lsp.{BranchFailureDetails, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ -import viper.silicon.state.Tree import viper.silver.ast -import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} import viper.silver.parser._ @@ -162,33 +158,6 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] InvalidArgumentsReport") markErrorsAsReported(errors) task.processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:")) - case BranchTreeReport(method,tree,beams) => - val mRp = task.content.methodIdentToRangePosition(method) - task.addDiagnostic(false)( - Seq(Diagnostic( - backendClassName=backendClassName, - position=mRp, - message=s"Branch fails.\n${tree.prettyPrint()}", - severity=lsp4j.DiagnosticSeverity.Error, - cached = false, - errorMsgPrefix=None - ))) - task.addCodeAction(false)(Seq( - CodeAction("Display explored branches", - CaCommand("viper.displayExploredBranches", Seq(method.name, Tree.DotFilePath)), - SelectionBoundScope(mRp), - CodeActionKind.QuickFix, - branchTree=Some(tree)) - )) - val details = beams.map(b => - task.getBranchRange(task.file_uri, - Common.toPosition(b.e.pos), - b.isLeftFatal, - b.isRightFatal) - ).toArray - if (details.nonEmpty) coordinator.sendBranchFailureDetails( - BranchFailureDetails(task.file_uri,details) - ) case EntitySuccessMessage(_, concerning, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] EntitySuccessMessage") if (task.progress == null) { diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 803b0b20..fb101d37 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -20,7 +20,12 @@ import akka.actor.ActorRef import viper.silver.verifier.AbstractError import viper.silver.ast.{AbstractSourcePosition, Position} import org.eclipse.lsp4j -import viper.server.frontends.lsp.Common +import org.eclipse.lsp4j.CodeActionKind +import viper.server.frontends.lsp.{BranchFailureDetails, Common} +import viper.silicon.state.Tree +import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} +import viper.silver.verifier.errors.BranchFailed +import viper.silver.verifier.reasons.BranchFails import java.nio.file.Path @@ -271,7 +276,29 @@ trait VerificationManager extends Manager with Branches { } val range = toRange(err.pos) - val rp = Common.toRangePosition(path,err.pos) + var rp = Common.toRangePosition(path,err.pos) + + err match { + case BranchFailed(_, BranchFails(method, tree, beamInfos), _) => + rp = content.methodIdentToRangePosition(method) + addCodeAction(false)(Seq( + CodeAction("Display explored branches", + CaCommand("viper.displayExploredBranches", Seq(method.name, Tree.DotFilePath)), + SelectionBoundScope(rp), + CodeActionKind.QuickFix, + branchTree=Some(tree)) + )) + val details = beamInfos.map(b => + getBranchRange(this.file_uri, + Common.toPosition(b.e.pos), + b.isLeftFatal, + b.isRightFatal) + ).toArray + if (details.nonEmpty) coordinator.sendBranchFailureDetails( + BranchFailureDetails(this.file_uri,details) + ) + case _ => + } val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" From 16ec135385f48dc9591585b8eac19cc314b4ead6 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sun, 9 Mar 2025 12:18:08 +0100 Subject: [PATCH 32/44] Refactoring --- .../frontends/lsp/ast/ParseAstLsp.scala | 37 ++++++++++--------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 064c2922..0226c371 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -13,6 +13,8 @@ import viper.silver.ast.LineColumnPosition import viper.silver.plugin.standard.adt._ import viper.silver.plugin.standard.termination.PDecreasesKeyword +import scala.annotation.tailrec + object HasCodeLens { def apply(p: PProgram): Seq[CodeLens] = p.deepCollect(PartialFunction.empty).flatten } @@ -92,36 +94,34 @@ object HasSemanticHighlights { object HasSignatureHelps { def apply(p: PProgram): Seq[SignatureHelp] = { def argsToSigHelpPart[T <: PNode](args: PDelimited.Comma[PSym.Paren, T]) : Seq[SignatureHelpPart] = { - def getSigHelpPart[T <: PNode](arg: T): SignatureHelpPart = SignatureHelpPart(true, arg.pretty, None) - SignatureHelpPart(false, s"${args.l.pretty}", None) +: + def getSigHelpPart[T <: PNode](arg: T): SignatureHelpPart = SignatureHelpPart(isArgument = true, arg.pretty, None) + SignatureHelpPart(isArgument = false, s"${args.l.pretty}", None) +: (args.inner.first.map(getSigHelpPart).toSeq ++ args.inner.inner.flatMap { - case (c, arg) => Seq(SignatureHelpPart(false, c.pretty, None), getSigHelpPart(arg)) - }) :+ SignatureHelpPart(false, s"${args.r.pretty}", None) + case (c, arg) => Seq(SignatureHelpPart(isArgument = false, c.pretty, None), getSigHelpPart(arg)) + }) :+ SignatureHelpPart(isArgument = false, s"${args.r.pretty}", None) } p.deepCollect({ - case n: PCallable => { + case n: PCallable => val bound = SelectionBoundKeyword(n.idndef.name) // Start - val start = SignatureHelpPart(false, s"${n.keyword.pretty}${n.idndef.pretty}", None) + val start = SignatureHelpPart(isArgument = false, s"${n.keyword.pretty}${n.idndef.pretty}", None) // Args val args = argsToSigHelpPart[PAnyFormalArgDecl](n.args) // Tail - val tail = SignatureHelpPart(false, s"${n.returnNodes.map(_.pretty).mkString}", None) + val tail = SignatureHelpPart(isArgument = false, s"${n.returnNodes.map(_.pretty).mkString}", None) Seq(SignatureHelp(start +: args :+ tail, PLspDeclaration.documentation(n), bound)) - } - case n: PDefine => { + case n: PDefine => val bound = SelectionBoundKeyword(n.idndef.name) // Start - val start = SignatureHelpPart(false, s"${n.define.pretty} ${n.idndef.pretty}", None) + val start = SignatureHelpPart(isArgument = false, s"${n.define.pretty} ${n.idndef.pretty}", None) // Args val mappedParams = n.parameters match { case Some(params) => argsToSigHelpPart[PDefineParam](params) case _ => Seq.empty } // Tail - val tail = SignatureHelpPart(false, s" ${n.body.pretty}", None) + val tail = SignatureHelpPart(isArgument = false, s" ${n.body.pretty}", None) Seq(SignatureHelp(start +: mappedParams :+ tail, PLspDeclaration.documentation(n), bound)) - } }).flatten } } @@ -171,14 +171,14 @@ object HasCodeActions { .find(t => t._1.isDefined)} .map(t => (t._1.get, t._2)) private def containsIdn(ass: PAssign, idn: String): Boolean = { - (ass.targets.first ++ ass.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]] - .map(getIdentifierNames(_)).flatten.toSet + (ass.targets.first ++ ass.targets.inner.map(_._1)).asInstanceOf[Seq[PExp]].flatMap(getIdentifierNames).toSet .contains(idn) && ass.rhs.find({case _ : PSimpleLiteral => ass}).isDefined } + @tailrec private def findClosestLiteralAssignment(n: PNode, idn: String): Option[PExp] = { var curr: Option[PNode] = Some(n) var result: Option[PExp] = None - while (curr.isDefined && !result.isDefined) { + while (curr.isDefined && result.isEmpty) { curr.get match { case pa : PAssign if containsIdn(pa, idn) => result = Some(pa.rhs) case _ => @@ -198,14 +198,15 @@ object HasCodeActions { case _ => PBinExp(e, PReserved(if (j > 0) PSymOp.Plus else PSymOp.Minus)(e.pos), PIntLit(-j)(e.pos))(e.pos) } private def getEditRange(n: PNode): Option[Range] = RangePosition(n) - .map(Common.toRange(_)).map(r => {r.setEnd(r.getStart); r}) - .headOption + .map(Common.toRange(_)).map(r => { + r.setEnd(r.getStart); r + }) private def getCodeActionsLoopInvariants(w: PWhile) : Seq[CodeAction] = { val cond = w.cond.inner.asInstanceOf[PBinExp] var condBound = cond.right var middle = cond.left var selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.left)) - if (!selfAssignment.isDefined) { + if (selfAssignment.isEmpty) { selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.right)) condBound = cond.left middle = cond.right From ef4cfdce2dafd2d9fcd4bd633ea75d8ec6e18ffb Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 00:21:54 +0100 Subject: [PATCH 33/44] Refactoring --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index ba34f1c5..03a361ec 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit ba34f1c54e9e094dec044c8cf2dcf605f33d10be +Subproject commit 03a361ec39d15362f4af10c8e0661ff8adfc7d7d diff --git a/silicon b/silicon index 5046b6b5..3fd047bd 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 5046b6b56b3c34ef8909ca7fbcd678d40132d030 +Subproject commit 3fd047bd8a04cb52b056d15ef7c0748cfc27a70c From 6527ea5437fc261ec6cfe72f33528f183ee31c06 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 00:59:27 +0100 Subject: [PATCH 34/44] Missing import --- .../scala/viper/server/frontends/lsp/file/Verification.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index fb101d37..731ba0fa 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -22,7 +22,7 @@ import viper.silver.ast.{AbstractSourcePosition, Position} import org.eclipse.lsp4j import org.eclipse.lsp4j.CodeActionKind import viper.server.frontends.lsp.{BranchFailureDetails, Common} -import viper.silicon.state.Tree +import viper.silicon.state.branchTree.BranchTree import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} import viper.silver.verifier.errors.BranchFailed import viper.silver.verifier.reasons.BranchFails @@ -283,7 +283,7 @@ trait VerificationManager extends Manager with Branches { rp = content.methodIdentToRangePosition(method) addCodeAction(false)(Seq( CodeAction("Display explored branches", - CaCommand("viper.displayExploredBranches", Seq(method.name, Tree.DotFilePath)), + CaCommand("viper.displayExploredBranches", Seq(method.name, BranchTree.DotFilePath)), SelectionBoundScope(rp), CodeActionKind.QuickFix, branchTree=Some(tree)) From d63423131b502be0be63101ff06b63f76141c211 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 01:10:44 +0100 Subject: [PATCH 35/44] Refactoring --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index 3fd047bd..b2229f78 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 3fd047bd8a04cb52b056d15ef7c0748cfc27a70c +Subproject commit b2229f785c671e74157d58b1ffe3c7bbb88afaa6 From f226f7bbc07896d76e53e43c59aee597e04c39bf Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 10 Mar 2025 10:48:23 +0100 Subject: [PATCH 36/44] Switch back to reporting --- carbon | 2 +- silicon | 2 +- .../server/core/VerificationWorker.scala | 29 +++++++------ .../scala/viper/server/core/ViperCache.scala | 18 +++++--- .../http/jsonWriters/ViperIDEProtocol.scala | 2 +- .../lsp/ast/utility/CodeAction.scala | 2 +- .../frontends/lsp/file/RelayActor.scala | 43 ++++++++++++++++++- .../frontends/lsp/file/Verification.scala | 31 +------------ 8 files changed, 75 insertions(+), 54 deletions(-) diff --git a/carbon b/carbon index 03a361ec..19a2880d 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 03a361ec39d15362f4af10c8e0661ff8adfc7d7d +Subproject commit 19a2880db774ed6229fb0a100c17d9ce6d8b82a4 diff --git a/silicon b/silicon index b2229f78..ed4693e4 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit b2229f785c671e74157d58b1ffe3c7bbb88afaa6 +Subproject commit ed4693e4c62fca1655f6d1a74d5ddf639da136d7 diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index 1b6b0bfa..f5d807c4 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -15,6 +15,7 @@ import viper.silver.ast._ import viper.silver.frontend.SilFrontend import viper.silver.reporter.{Reporter, _} import viper.silver.utility.ViperProgramSubmitter +import viper.silver.reporter.BranchTree import viper.silver.verifier.{AbstractVerificationError, VerificationResult, _} import scala.collection.mutable.ListBuffer @@ -207,12 +208,12 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } } - case class CachingResult(transformedProgram: Program, cachedErrors: Seq[VerificationError]) + case class CachingResult(transformedProgram: Program, cachedErrors: Seq[VerificationError], branchTree: Option[BranchTree]) private def caching(input: Program): CachingResult = { if (_frontend.config.disableCaching()) { // NOP - return CachingResult(input, Seq.empty) + return CachingResult(input, Seq.empty, None) } val (transformed_prog, cached_results) = ViperCache.applyCache(backendName, programId, input) @@ -227,7 +228,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } else { all_cached_errors ++= cached_errors _frontend.reporter report - CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(cached_errors)) + CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(cached_errors, result.branchTree)) } }) @@ -239,7 +240,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, s" methodsToVerify: ${methodsToVerify.map(_.name)}.") _frontend.logger.trace(s"The cached program is equivalent to: \n${transformed_prog.toString()}") - CachingResult(transformed_prog, all_cached_errors.toSeq) + CachingResult(transformed_prog, all_cached_errors.toSeq, None) } private def beforeVerify(input: Program): Either[Seq[AbstractError], Program] = { @@ -271,11 +272,13 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, val astAfterApplyingCache = cachingResult.transformedProgram val methodsToVerify: Seq[Method] = astAfterApplyingCache.methods.filter(_.body.isDefined) - val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]])] = methodsToVerify.map((m: Method) => { + val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]],Option[BranchTree])] = methodsToVerify.map((m: Method) => { // Results come back irrespective of program Member. + var branchTree : Option[BranchTree] = None val cacheable_errors: Option[List[AbstractVerificationError]] = for { cache_errs <- verificationResult match { - case Failure(errs) => + case Failure(errs,bt) => + branchTree = if (bt.nonEmpty) bt else branchTree val r = getMethodSpecificErrors(m, errs) _frontend.logger.debug(s"getMethodSpecificErrors returned $r") r @@ -284,7 +287,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } } yield cache_errs - (m, cacheable_errors) + (m, cacheable_errors, branchTree) }) // Check that the mapping from errors to methods is not messed up @@ -294,7 +297,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, verificationResult match { case Success => all_errors_in_file.isEmpty - case Failure(errors) => + case Failure(errors,_) => // FIXME find a better sorting criterion errors.sortBy(ae => ae.hashCode()) == all_errors_in_file.sortBy(ae => ae.hashCode()) } @@ -302,11 +305,11 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, if (update_cache_criterion) { // update cache - meth_to_err_map.foreach { case (m: Method, cacheable_errors: Option[List[AbstractVerificationError]]) => + meth_to_err_map.foreach { case (m: Method, cacheable_errors: Option[List[AbstractVerificationError]],branchTree:Option[BranchTree]) => _frontend.logger.debug(s"Obtained cacheable errors: $cacheable_errors") if (cacheable_errors.isDefined) { - ViperCache.update(backendName, programId, m, astAfterApplyingCache, cacheable_errors.get) match { + ViperCache.update(backendName, programId, m, astAfterApplyingCache, cacheable_errors.get, branchTree) match { case e :: es => _frontend.logger.trace(s"Storing new entry in cache for method '${m.name}' and backend '$backendName': $e. Other entries for this method: ($es)") case Nil => @@ -326,10 +329,10 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, verificationResult // verificationResult remains unchanged as the cached errors (which are none) do not change the outcome } else { verificationResult match { - case Failure(errorList) => - Failure(errorList ++ cachingResult.cachedErrors) + case Failure(errorList,branchTree) => + Failure(errorList ++ cachingResult.cachedErrors, branchTree) case Success => - Failure(cachingResult.cachedErrors) + Failure(cachingResult.cachedErrors, None) } } } diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala index 4679f420..49dc4184 100644 --- a/src/main/scala/viper/server/core/ViperCache.scala +++ b/src/main/scala/viper/server/core/ViperCache.scala @@ -19,6 +19,7 @@ import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellfor import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors} import net.liftweb.json.Serialization.{read, write} import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints} +import viper.silver.reporter.BranchTree import viper.silver.verifier.reasons.{AssertionFalse, DivisionByZero, EpsilonAsParam, FeatureUnsupported, InsufficientPermission, InternalReason, InvalidPermMultiplication, LabelledStateNotReached, MagicWandChunkNotFound, MapKeyNotContained, NegativePermission, QPAssertionNotInjective, ReceiverNull, SeqIndexExceedsLength, SeqIndexNegative, UnexpectedNode} import java.nio.charset.StandardCharsets @@ -84,7 +85,8 @@ object ViperCache extends Cache { logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName") // set cached flag: val cachedErrors = content.errors.map(setCached) - CacheResult(concerning_method, cachedErrors) + content.branchTree.foreach(bt => bt.cached=true) + CacheResult(concerning_method, cachedErrors, content.branchTree) } catch { case e: Throwable => // In case parsing of the cache entry fails, abort caching & evict cache entries for this file, since hey might come from an unsupported version @@ -262,11 +264,12 @@ object ViperCache extends Cache { file: String, method: Method, program: Program, - errors: List[AbstractVerificationError]): List[CacheEntry] = { + errors: List[AbstractVerificationError], + branchTree: Option[BranchTree]): List[CacheEntry] = { val viperMethod = ViperMethod(method) val deps: List[Member] = viperMethod.getDependencies(ViperAst(program)) - val content = createCacheContent(backendName, file, program, errors) + val content = createCacheContent(backendName, file, program, errors, branchTree) val file_key = getKey(file = file, backendName = backendName) super.update(file_key, ViperMethod(method), deps, content) } @@ -302,12 +305,13 @@ object ViperCache extends Cache { def createCacheContent( backendName: String, file: String, p: Program, - errors: List[AbstractVerificationError]): SerializedViperCacheContent = { + errors: List[AbstractVerificationError], + branchTree: Option[BranchTree]): SerializedViperCacheContent = { val key: String = getKey(file = file, backendName = backendName) implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key)) - SerializedViperCacheContent(write(ViperCacheContent(errors))) + SerializedViperCacheContent(write(ViperCacheContent(errors,branchTree))) } } @@ -556,7 +560,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent /** Class containing the verification results of a viper verification run * */ -case class ViperCacheContent(errors: List[AbstractVerificationError]) +case class ViperCacheContent(errors: List[AbstractVerificationError], branchTree: Option[BranchTree]) /** An access path holds a List of Numbers * @@ -589,7 +593,7 @@ case class ViperAst(p: Program) extends Ast { } } -case class CacheResult(method: Method, verification_errors: List[VerificationError]) +case class CacheResult(method: Method, verification_errors: List[VerificationError], branchTree: Option[BranchTree]) case class ViperMember(h: Hashable) extends Member { diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala index 74b7791a..4d2f73b3 100644 --- a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala +++ b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala @@ -254,7 +254,7 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs implicit val verificationResult_writer: RootJsonFormat[VerificationResult] = lift(new RootJsonWriter[VerificationResult] { override def write(obj: VerificationResult): JsValue = obj match { case Success => JsObject("type" -> JsString("success")) - case f@ Failure(_) => f.toJson + case f@ Failure(_,_) => f.toJson } }) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 515c4eb8..5a5685df 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -7,7 +7,7 @@ package viper.silver.ast.utility.lsp import org.eclipse.lsp4j -import viper.silver.verifier.errors.BranchTree +import viper.silver.reporter.BranchTree trait HasCodeActions { def getCodeActions: Seq[CodeAction] diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 89a0009b..3e1f2152 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,11 +7,13 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} -import org.eclipse.lsp4j.Position +import org.eclipse.lsp4j.{CodeActionKind, DiagnosticSeverity, Position} import viper.server.frontends.lsp +import viper.server.frontends.lsp.{BranchFailureDetails, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast +import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, RangePosition, SelectionBoundScope} import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} import viper.silver.parser._ @@ -99,6 +101,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends * at different position just get dropped. */ var reportedErrors: Set[(AbstractError, Option[ast.Position])] = Set.empty + var reportedBranchTrees: Set[RangePosition] = Set.empty /** helper function to add an error to `reportedErrors` */ private def markErrorAsReported(err: AbstractError): Unit = err match { case err: ErrorMessage => reportedErrors = reportedErrors + ((err, Some(err.offendingNode.pos))) @@ -112,6 +115,41 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case _ => reportedErrors.contains((err, None)) } + private def handleBranchTree(tree: BranchTree): Unit = { + val method = tree.getMethod() + val beams = tree.getBeams() + val mRp = task.content.methodIdentToRangePosition(method) + if (!reportedBranchTrees.contains(mRp)){ + val cacheFlag = if (tree.cached) "(cached)" else "" + task.addDiagnostic(false)( + Seq(Diagnostic( + backendClassName=backendClassName, + position=mRp, + message=s"Branch fails. ${{cacheFlag}} \n${tree.prettyPrint()}", + severity=DiagnosticSeverity.Error, + cached = false, + errorMsgPrefix=None + ))) + task.addCodeAction(false)(Seq( + CodeAction("Display explored branches", + CaCommand("viper.displayExploredBranches", Seq(method.name, tree.DotFilePath)), + SelectionBoundScope(mRp), + CodeActionKind.QuickFix, + branchTree=Some(tree)) + )) + val details = beams.map(b => + task.getBranchRange(task.file_uri, + Common.toPosition(b.e.pos), + b.isLeftFatal, + b.isRightFatal) + ).toArray + if (details.nonEmpty) coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri,details) + ) + reportedBranchTrees += mRp + } + } + override def receive: PartialFunction[Any, Unit] = { case m if task.is_aborting => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] ignoring message because we are aborting: $m") @@ -178,6 +216,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.state = VerificationReporting task.timeMs = verificationTime // the completion handler is not yet invoked (but as part of Status.Success) + case BranchTreeReport(tree) => + handleBranchTree(tree) case OverallFailureMessage(_, verificationTime, failure) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallFailureMessage") task.state = VerificationReporting @@ -188,6 +228,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends // ViperServer produces EntitySuccessMessage and EntityFailureMessages) val newErrors = failure.errors.filterNot(hasAlreadyBeenReported) markErrorsAsReported(newErrors) + if (failure.branchTree.nonEmpty) handleBranchTree(failure.branchTree.get) task.processErrors(backendClassName, newErrors) case WarningsDuringParsing(warnings) => markErrorsAsReported(warnings) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 731ba0fa..7492d269 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -20,12 +20,7 @@ import akka.actor.ActorRef import viper.silver.verifier.AbstractError import viper.silver.ast.{AbstractSourcePosition, Position} import org.eclipse.lsp4j -import org.eclipse.lsp4j.CodeActionKind -import viper.server.frontends.lsp.{BranchFailureDetails, Common} -import viper.silicon.state.branchTree.BranchTree -import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, SelectionBoundScope} -import viper.silver.verifier.errors.BranchFailed -import viper.silver.verifier.reasons.BranchFails +import viper.server.frontends.lsp.{Common} import java.nio.file.Path @@ -276,29 +271,7 @@ trait VerificationManager extends Manager with Branches { } val range = toRange(err.pos) - var rp = Common.toRangePosition(path,err.pos) - - err match { - case BranchFailed(_, BranchFails(method, tree, beamInfos), _) => - rp = content.methodIdentToRangePosition(method) - addCodeAction(false)(Seq( - CodeAction("Display explored branches", - CaCommand("viper.displayExploredBranches", Seq(method.name, BranchTree.DotFilePath)), - SelectionBoundScope(rp), - CodeActionKind.QuickFix, - branchTree=Some(tree)) - )) - val details = beamInfos.map(b => - getBranchRange(this.file_uri, - Common.toPosition(b.e.pos), - b.isLeftFatal, - b.isRightFatal) - ).toArray - if (details.nonEmpty) coordinator.sendBranchFailureDetails( - BranchFailureDetails(this.file_uri,details) - ) - case _ => - } + val rp = Common.toRangePosition(path,err.pos) val errFullId = if(err.fullId != null) s"[${err.fullId}] " else "" val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else "" From c7c90dd377fa07d8449936f4e00bdc75a96bf6ae Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Fri, 14 Mar 2025 16:39:41 +0100 Subject: [PATCH 37/44] Generate ASCII / DOT client side --- carbon | 2 +- silicon | 2 +- .../server/core/VerificationWorker.scala | 28 ++++--- .../scala/viper/server/core/ViperCache.scala | 18 ++-- .../frontends/lsp/ClientCoordinator.scala | 2 +- .../server/frontends/lsp/DataProtocol.scala | 10 ++- .../frontends/lsp/IdeLanguageClient.scala | 2 +- .../frontends/lsp/ast/ParseAstLsp.scala | 10 ++- .../lsp/ast/utility/CodeAction.scala | 13 +-- .../server/frontends/lsp/file/Branches.scala | 47 +++++------ .../frontends/lsp/file/RelayActor.scala | 84 ++++++++++--------- .../lsp/file/utility/Conversions.scala | 25 +++--- .../viper/server/core/CoreServerSpec.scala | 2 +- 13 files changed, 127 insertions(+), 118 deletions(-) diff --git a/carbon b/carbon index 19a2880d..5d09b506 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 19a2880db774ed6229fb0a100c17d9ce6d8b82a4 +Subproject commit 5d09b5069c8fee032fcacca91ddf26c3cc27f499 diff --git a/silicon b/silicon index ed4693e4..4403e454 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit ed4693e4c62fca1655f6d1a74d5ddf639da136d7 +Subproject commit 4403e45469d460fdf2aaba4bd8ccd6c7909fdffd diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index f5d807c4..fc893848 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -15,7 +15,7 @@ import viper.silver.ast._ import viper.silver.frontend.SilFrontend import viper.silver.reporter.{Reporter, _} import viper.silver.utility.ViperProgramSubmitter -import viper.silver.reporter.BranchTree +import viper.silver.reporter.ExploredBranches import viper.silver.verifier.{AbstractVerificationError, VerificationResult, _} import scala.collection.mutable.ListBuffer @@ -208,7 +208,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } } - case class CachingResult(transformedProgram: Program, cachedErrors: Seq[VerificationError], branchTree: Option[BranchTree]) + case class CachingResult(transformedProgram: Program, cachedErrors: Seq[VerificationError], exploredBranches: Option[ExploredBranches]) private def caching(input: Program): CachingResult = { if (_frontend.config.disableCaching()) { @@ -228,7 +228,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } else { all_cached_errors ++= cached_errors _frontend.reporter report - CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(cached_errors, result.branchTree)) + CachedEntityMessage(_frontend.getVerifierName, result.method, Failure(cached_errors, result.exploredBranches)) } }) @@ -272,13 +272,13 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, val astAfterApplyingCache = cachingResult.transformedProgram val methodsToVerify: Seq[Method] = astAfterApplyingCache.methods.filter(_.body.isDefined) - val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]],Option[BranchTree])] = methodsToVerify.map((m: Method) => { + val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]],Option[ExploredBranches])] = methodsToVerify.map((m: Method) => { // Results come back irrespective of program Member. - var branchTree : Option[BranchTree] = None + var exploredBranches : Option[ExploredBranches] = None val cacheable_errors: Option[List[AbstractVerificationError]] = for { cache_errs <- verificationResult match { - case Failure(errs,bt) => - branchTree = if (bt.nonEmpty) bt else branchTree + case Failure(errs,eb) => + exploredBranches = if (eb.nonEmpty) eb else exploredBranches val r = getMethodSpecificErrors(m, errs) _frontend.logger.debug(s"getMethodSpecificErrors returned $r") r @@ -287,7 +287,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, } } yield cache_errs - (m, cacheable_errors, branchTree) + (m, cacheable_errors, exploredBranches) }) // Check that the mapping from errors to methods is not messed up @@ -305,11 +305,11 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, if (update_cache_criterion) { // update cache - meth_to_err_map.foreach { case (m: Method, cacheable_errors: Option[List[AbstractVerificationError]],branchTree:Option[BranchTree]) => + meth_to_err_map.foreach { case (m: Method, cacheable_errors: Option[List[AbstractVerificationError]],exploredBranches:Option[ExploredBranches]) => _frontend.logger.debug(s"Obtained cacheable errors: $cacheable_errors") if (cacheable_errors.isDefined) { - ViperCache.update(backendName, programId, m, astAfterApplyingCache, cacheable_errors.get, branchTree) match { + ViperCache.update(backendName, programId, m, astAfterApplyingCache, cacheable_errors.get, exploredBranches) match { case e :: es => _frontend.logger.trace(s"Storing new entry in cache for method '${m.name}' and backend '$backendName': $e. Other entries for this method: ($es)") case Nil => @@ -329,8 +329,12 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, verificationResult // verificationResult remains unchanged as the cached errors (which are none) do not change the outcome } else { verificationResult match { - case Failure(errorList,branchTree) => - Failure(errorList ++ cachingResult.cachedErrors, branchTree) + case Failure(errorList,exploredBranches) => + val combinedExploredBranches = (exploredBranches, cachingResult.exploredBranches) match { + case (Some(eb),Some(ebC)) => Some(ExploredBranches(eb.method, ebC.paths ++ eb.paths, ebC.cached)) + case _=> exploredBranches + } + Failure(errorList ++ cachingResult.cachedErrors, combinedExploredBranches) case Success => Failure(cachingResult.cachedErrors, None) } diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala index 49dc4184..a970cc24 100644 --- a/src/main/scala/viper/server/core/ViperCache.scala +++ b/src/main/scala/viper/server/core/ViperCache.scala @@ -19,7 +19,7 @@ import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellfor import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors} import net.liftweb.json.Serialization.{read, write} import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints} -import viper.silver.reporter.BranchTree +import viper.silver.reporter.ExploredBranches import viper.silver.verifier.reasons.{AssertionFalse, DivisionByZero, EpsilonAsParam, FeatureUnsupported, InsufficientPermission, InternalReason, InvalidPermMultiplication, LabelledStateNotReached, MagicWandChunkNotFound, MapKeyNotContained, NegativePermission, QPAssertionNotInjective, ReceiverNull, SeqIndexExceedsLength, SeqIndexNegative, UnexpectedNode} import java.nio.charset.StandardCharsets @@ -85,8 +85,8 @@ object ViperCache extends Cache { logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName") // set cached flag: val cachedErrors = content.errors.map(setCached) - content.branchTree.foreach(bt => bt.cached=true) - CacheResult(concerning_method, cachedErrors, content.branchTree) + content.exploredBranches.foreach(eb => eb.cached=true) + CacheResult(concerning_method, cachedErrors, content.exploredBranches) } catch { case e: Throwable => // In case parsing of the cache entry fails, abort caching & evict cache entries for this file, since hey might come from an unsupported version @@ -265,11 +265,11 @@ object ViperCache extends Cache { method: Method, program: Program, errors: List[AbstractVerificationError], - branchTree: Option[BranchTree]): List[CacheEntry] = { + exploredBranches: Option[ExploredBranches]): List[CacheEntry] = { val viperMethod = ViperMethod(method) val deps: List[Member] = viperMethod.getDependencies(ViperAst(program)) - val content = createCacheContent(backendName, file, program, errors, branchTree) + val content = createCacheContent(backendName, file, program, errors, exploredBranches) val file_key = getKey(file = file, backendName = backendName) super.update(file_key, ViperMethod(method), deps, content) } @@ -306,12 +306,12 @@ object ViperCache extends Cache { backendName: String, file: String, p: Program, errors: List[AbstractVerificationError], - branchTree: Option[BranchTree]): SerializedViperCacheContent = { + exploredBranches: Option[ExploredBranches]): SerializedViperCacheContent = { val key: String = getKey(file = file, backendName = backendName) implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key)) - SerializedViperCacheContent(write(ViperCacheContent(errors,branchTree))) + SerializedViperCacheContent(write(ViperCacheContent(errors,exploredBranches))) } } @@ -560,7 +560,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent /** Class containing the verification results of a viper verification run * */ -case class ViperCacheContent(errors: List[AbstractVerificationError], branchTree: Option[BranchTree]) +case class ViperCacheContent(errors: List[AbstractVerificationError], exploredBranches: Option[ExploredBranches]) /** An access path holds a List of Numbers * @@ -593,7 +593,7 @@ case class ViperAst(p: Program) extends Ast { } } -case class CacheResult(method: Method, verification_errors: List[VerificationError], branchTree: Option[BranchTree]) +case class CacheResult(method: Method, verification_errors: List[VerificationError], exploredBranches: Option[ExploredBranches]) case class ViperMember(h: Hashable) extends Member { diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index 17457848..8cf8ca5c 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -176,7 +176,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif /** Notifies the client about details of branch failure for displaying red beams */ def sendBranchFailureDetails(details: BranchFailureDetails): Unit = { try { - client.sendBranchFailureDetails(details) + client.sendBranchFailureInfo(details) } catch { case e: Throwable => logger.debug(s"Error while sending branch failure details: $e") } diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index 5c2dea13..4959c9ba 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -176,7 +176,15 @@ case class StateChangeParams( stage: String = null, error: String = null) -case class BranchFailureDetails(uri: String, /*errorMessage: String, tree string*/ ranges: Array[Range]) +case class BranchCondition(condition: String, negated: Boolean) +case class BranchFailurePath(conditions: Array[BranchCondition], isResultFatal: Boolean) +case class BranchClauseRange(ifLine: Int, elseLine: Int, methodEndLine: Int) +case class BranchFailureDetails(uri: String, + methodName : String, + methodIdentifierRange : Range, + paths: Array[BranchFailurePath], + clauseRange: BranchClauseRange, + cached : Boolean) case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int) diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala index ebccd700..3eff256e 100644 --- a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala +++ b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala @@ -43,5 +43,5 @@ trait IdeLanguageClient extends LanguageClient { def notifyStateChanged(params: StateChangeParams): Unit @JsonNotification(S2C_Commands.BranchFailureDetails) - def sendBranchFailureDetails(params: BranchFailureDetails): Unit + def sendBranchFailureInfo(params: BranchFailureDetails): Unit } diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala index 0226c371..a05e45c7 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala @@ -234,8 +234,8 @@ object HasCodeActions { val decreases = s"$optNewLine ${PDecreasesKeyword.keyword} $decreasesExp\n$indent" Seq( - CodeAction("Add invariant", CaEdit(invariant , er), SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), - CodeAction("Add decreases", CaEdit(decreases, er), SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) + CodeAction("Add invariant", Some((invariant , er)), None, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), + CodeAction("Add decreases", Some((decreases, er)), None, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) ) }).flatten } @@ -244,7 +244,8 @@ object HasCodeActions { fas.map(f => (f,RangePosition(f))).collect { case (f, Some(fRp)) => CodeAction("Declare field", - CaCommand("viper.declareField", Seq(f.idnref.pretty)), + None, + Some(("viper.declareField", Seq(f.idnref.pretty))), SelectionBoundScope(fRp), CodeActionKind.QuickFix, getDiagnostic(Common.toPosition(f.pos._1))) @@ -269,7 +270,8 @@ object HasCodeActions { val indent = " "*(parentRp.start.column-1) val beforeKeyword = if (openingBracketInSameLine) s"\n$indent " else " " CodeAction("Add access precondition", - CaEdit(s"$beforeKeyword$keyword acc(${f.pretty})\n$indent", new Range(editPos, editPos)), + Some((s"$beforeKeyword$keyword acc(${f.pretty})\n$indent", new Range(editPos, editPos))), + None, SelectionBoundScope(fRp), CodeActionKind.QuickFix, getDiagnostic(Common.toPosition(f.pos._1))) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 5a5685df..2d66237b 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -7,23 +7,18 @@ package viper.silver.ast.utility.lsp import org.eclipse.lsp4j -import viper.silver.reporter.BranchTree trait HasCodeActions { def getCodeActions: Seq[CodeAction] } -trait CaAction -case class CaEdit(edit : String, range : lsp4j.Range) extends CaAction -case class CaCommand(cmd : String, args : Seq[AnyRef]) extends CaAction - case class CodeAction( title: String, - action: CaAction, + edit: Option[(String, lsp4j.Range)], + cmd: Option[(String, Seq[AnyRef])], bound: SelectionBoundScopeTrait, kind: String, - resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty, - branchTree : Option[BranchTree] = None -) extends SelectableInBound with HasRangePositions { + resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty + ) extends SelectableInBound with HasRangePositions { override def rangePositions: Seq[RangePosition] = bound.rangePositions } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala index 2dfd73f3..59493f43 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala @@ -6,39 +6,36 @@ package viper.server.frontends.lsp.file -import org.eclipse.lsp4j +import viper.server.frontends.lsp.Common +import viper.silver.ast.Method +import viper.silver.parser.PKw trait Branches extends ProjectAware { - def getBranchRange(uri: String, pos: lsp4j.Position, leftIsFatal: Boolean, rightIsFatal: Boolean): lsp4j.Range = { - var start = new lsp4j.Position(pos.getLine, 0) - var end = new lsp4j.Position(pos.getLine, 0) + def getFirstBranchClauseLines(uri: String, method: Method): (Int,Int,Int) = { + var start = Common.toPosition(method.pos) val m = getInProject(uri) - var currPos = m.content.iterForward(start).drop(1).find { case (c, _) => c == '{' } - if (!currPos.isDefined) return new lsp4j.Range(start, end) + var currPos = m.content.iterForward(start) + .drop(1).find { case (c, _) => c == '{' } + if (currPos.isDefined) start = currPos.get._2 + currPos = m.content.iterForward(currPos.get._2) + .drop(1).find { case (c, _) => c == '{' } + if (currPos.isDefined) start = currPos.get._2 + var middleLn = start.getLine + var endLn = start.getLine var openBraceCount = 0 - var movedStart = false do { - val (c, p) = currPos.get + val (c,p) = currPos.get c match { case '}' => openBraceCount -= 1 if (openBraceCount == 0) { - end = new lsp4j.Position(p.getLine, 0) - if (leftIsFatal && !movedStart) { - val nextBracePos = m.content.iterForward(p).drop(1).find { case (c, _) => c == '{' } - if (nextBracePos.isDefined) { - currPos = nextBracePos - } - // move start - if (!rightIsFatal) { - if (nextBracePos.isDefined) { // no else clause - start = new lsp4j.Position(currPos.get._2.getLine, 0) - } else if (p.getLine + 1 < m.content.fileContent.length) { // else clause - start = new lsp4j.Position(p.getLine + 1, 0) - } - } - openBraceCount = 1 - movedStart = true + val ln = if (!m.content.fileContent(p.getLine).contains(PKw.Else.keyword)) p.getLine+1 + else p.getLine + if (start.getLine == middleLn) { + middleLn = ln + openBraceCount += 1 + } else { + endLn = ln } } case '{' => @@ -47,6 +44,6 @@ trait Branches extends ProjectAware { } currPos = m.content.iterForward(currPos.get._2).drop(1).find { case (c, _) => c == '{' || c == '}' } } while (currPos.isDefined && openBraceCount > 0) - new lsp4j.Range(start, end) + (start.getLine, middleLn, endLn) } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 3e1f2152..b9cec819 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,13 +7,13 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} -import org.eclipse.lsp4j.{CodeActionKind, DiagnosticSeverity, Position} +import org.eclipse.lsp4j.{CodeActionKind, Position} import viper.server.frontends.lsp -import viper.server.frontends.lsp.{BranchFailureDetails, Common} +import viper.server.frontends.lsp.{BranchClauseRange, BranchCondition, BranchFailureDetails, BranchFailurePath, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ import viper.silver.ast -import viper.silver.ast.utility.lsp.{CaCommand, CodeAction, RangePosition, SelectionBoundScope} +import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} import viper.silver.reporter._ import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} import viper.silver.parser._ @@ -101,7 +101,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends * at different position just get dropped. */ var reportedErrors: Set[(AbstractError, Option[ast.Position])] = Set.empty - var reportedBranchTrees: Set[RangePosition] = Set.empty + var reportedExploredBranches: Set[RangePosition] = Set.empty /** helper function to add an error to `reportedErrors` */ private def markErrorAsReported(err: AbstractError): Unit = err match { case err: ErrorMessage => reportedErrors = reportedErrors + ((err, Some(err.offendingNode.pos))) @@ -115,39 +115,43 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case _ => reportedErrors.contains((err, None)) } - private def handleBranchTree(tree: BranchTree): Unit = { - val method = tree.getMethod() - val beams = tree.getBeams() - val mRp = task.content.methodIdentToRangePosition(method) - if (!reportedBranchTrees.contains(mRp)){ - val cacheFlag = if (tree.cached) "(cached)" else "" - task.addDiagnostic(false)( - Seq(Diagnostic( - backendClassName=backendClassName, - position=mRp, - message=s"Branch fails. ${{cacheFlag}} \n${tree.prettyPrint()}", - severity=DiagnosticSeverity.Error, - cached = false, - errorMsgPrefix=None - ))) - task.addCodeAction(false)(Seq( - CodeAction("Display explored branches", - CaCommand("viper.displayExploredBranches", Seq(method.name, tree.DotFilePath)), - SelectionBoundScope(mRp), - CodeActionKind.QuickFix, - branchTree=Some(tree)) - )) - val details = beams.map(b => - task.getBranchRange(task.file_uri, - Common.toPosition(b.e.pos), - b.isLeftFatal, - b.isRightFatal) - ).toArray - if (details.nonEmpty) coordinator.sendBranchFailureDetails( - BranchFailureDetails(task.file_uri,details) - ) - reportedBranchTrees += mRp - } + private def handleExploredBranches(eb: ExploredBranches): Unit = { + if (eb.paths.nonEmpty) { + val mRp = task.content.methodIdentToRangePosition(eb.method) + if (!reportedExploredBranches.contains(mRp)) { + task.addCodeAction(false)(Seq( + CodeAction("Display explored branches", + None, + Some("viper.displayExploredBranches", Seq(task.file_uri, eb.method.name)), + SelectionBoundScope(mRp), + CodeActionKind.QuickFix, + ))) + + val paths = eb.paths.map(e => { + val (conds, isResultFatal) = e + val transformedConds = conds.map(c => { + val (cond, negated) = c + BranchCondition(cond, negated) + }).toArray + BranchFailurePath(transformedConds, isResultFatal) + }).toArray + + reportedExploredBranches += mRp + + val idnRange = Common.toRange(mRp) + val (ifLn, elseLn, methodEndLn) = task.getFirstBranchClauseLines(task.file_uri, eb.method) + coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri, + eb.method.name, + idnRange, + paths, + BranchClauseRange(ifLn, + elseLn, + methodEndLn), + eb.cached) + ) + } + } } override def receive: PartialFunction[Any, Unit] = { @@ -216,8 +220,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.state = VerificationReporting task.timeMs = verificationTime // the completion handler is not yet invoked (but as part of Status.Success) - case BranchTreeReport(tree) => - handleBranchTree(tree) + case ExploredBranchesReport(exploredBranches) => + handleExploredBranches(exploredBranches) case OverallFailureMessage(_, verificationTime, failure) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallFailureMessage") task.state = VerificationReporting @@ -228,7 +232,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends // ViperServer produces EntitySuccessMessage and EntityFailureMessages) val newErrors = failure.errors.filterNot(hasAlreadyBeenReported) markErrorsAsReported(newErrors) - if (failure.branchTree.nonEmpty) handleBranchTree(failure.branchTree.get) + if (failure.exploredBranches.nonEmpty) handleExploredBranches(failure.exploredBranches.get) task.processErrors(backendClassName, newErrors) case WarningsDuringParsing(warnings) => markErrorsAsReported(warnings) diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index a0d7b254..bb700f5e 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -13,7 +13,6 @@ import viper.server.frontends.lsp.{Common, Lsp4jSemanticHighlight} import viper.server.frontends.lsp.file.{Diagnostic, FindReferences} import ch.qos.logback.classic.Logger import org.eclipse.lsp4j.Command -import viper.silver.ast.utility.lsp.{CaCommand, CaEdit} import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer @@ -217,19 +216,19 @@ case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAc override def translate(ca: lsp.CodeAction)(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean)): lsp4j.CodeAction = ??? override def translate(cas: Seq[lsp.CodeAction])(i: (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean))(implicit log: Logger): Seq[lsp4j.CodeAction] = { cas.map(ca => { - if (ca.branchTree.isDefined) ca.branchTree.get.toDotFile() // TODO val codeAction = new lsp4j.CodeAction(ca.title) - ca.action match { - case CaCommand(cmd, args) => - codeAction.setCommand(new Command(ca.title, cmd, args.asJava)) - case CaEdit(edit, range) => - val textEdits = Seq(new lsp4j.TextEdit(range, edit)).asJava - val uri = ca.bound.scope.file.toUri().toString() - val edits = Map(uri -> textEdits).asJava - val workspaceEdit = new lsp4j.WorkspaceEdit(edits) - codeAction.setEdit(workspaceEdit) - case _=> - } + ca.cmd.map(c => { + val (cmd,args) = c + codeAction.setCommand(new Command(ca.title, cmd, args.asJava)) + }) + ca.edit.map(e => { + val (edit, range) = e + val textEdits = Seq(new lsp4j.TextEdit(range, edit)).asJava + val uri = ca.bound.scope.file.toUri().toString() + val edits = Map(uri -> textEdits).asJava + val workspaceEdit = new lsp4j.WorkspaceEdit(edits) + codeAction.setEdit(workspaceEdit) + }) codeAction.setDiagnostics(ca.resolvedDiags.asJava) codeAction.setKind(ca.kind) codeAction diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index 9c083318..6e42b658 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -431,7 +431,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { override def notifyUnhandledViperServerMessage(params: UnhandledViperServerMessageTypeParams): Unit = {} override def notifyVerificationNotStarted(params: VerificationNotStartedParams): Unit = {} override def notifyStateChanged(params: StateChangeParams): Unit = {} - override def sendBranchFailureDetails(params: BranchFailureDetails): Unit = {} + override def sendBranchFailureInfo(params: BranchFailureDetails): Unit = {} override def telemetryEvent(`object`: Any): Unit = {} override def publishDiagnostics(diagnostics: PublishDiagnosticsParams): Unit = {} override def showMessage(messageParams: MessageParams): Unit = {} From c96a1f31818a0a0ce22f7168810ab35ffcf50e99 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 24 Mar 2025 19:37:33 +0100 Subject: [PATCH 38/44] Move tree generation --- .../server/frontends/lsp/DataProtocol.scala | 11 +- .../lsp/ast/utility/CodeAction.scala | 4 +- .../frontends/lsp/file/BranchTree.scala | 285 ++++++++++++++++++ .../frontends/lsp/file/RelayActor.scala | 49 +-- .../lsp/file/utility/Conversions.scala | 1 + .../viper/branch-tree/allPathsCorrect.vpr | 10 + .../default/allPathsCorrect_expected | 1 + .../default/firstPathFails_expected | 10 + .../default/lastPathFails_expected | 10 + .../default/multipleMethods_expected | 20 ++ .../branch-tree/default/noBranches_expected | 1 + .../viper/branch-tree/default/onlyIf_expected | 6 + .../viper/branch-tree/default/while_expected | 6 + .../viper/branch-tree/firstPathFails.vpr | 19 ++ .../viper/branch-tree/lastPathFails.vpr | 19 ++ .../viper/branch-tree/multipleMethods.vpr | 37 +++ .../viper/branch-tree/noBranches.vpr | 6 + .../resources/viper/branch-tree/onlyIf.vpr | 14 + .../reportAllErrors/allPathsCorrect_expected | 1 + .../reportAllErrors/firstPathFails_expected | 9 + .../reportAllErrors/lastPathFails_expected | 10 + .../reportAllErrors/noBranches_expected | 1 + .../reportAllErrors/onlyIf_expected | 5 + .../reportAllErrors/while_expected | 6 + .../reportTwoErrors/firstPathFails_expected | 9 + .../reportTwoErrors/lastPathFails_expected | 10 + .../resources/viper/branch-tree/while.vpr | 13 + .../viper/server/core/BranchTreeTests.scala | 131 ++++++++ .../viper/server/core/CoreServerSpec.scala | 36 +-- .../scala/viper/server/core/MockClient.scala | 24 ++ 30 files changed, 702 insertions(+), 62 deletions(-) create mode 100644 src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala create mode 100644 src/test/resources/viper/branch-tree/allPathsCorrect.vpr create mode 100644 src/test/resources/viper/branch-tree/default/allPathsCorrect_expected create mode 100644 src/test/resources/viper/branch-tree/default/firstPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/default/lastPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/default/multipleMethods_expected create mode 100644 src/test/resources/viper/branch-tree/default/noBranches_expected create mode 100644 src/test/resources/viper/branch-tree/default/onlyIf_expected create mode 100644 src/test/resources/viper/branch-tree/default/while_expected create mode 100644 src/test/resources/viper/branch-tree/firstPathFails.vpr create mode 100644 src/test/resources/viper/branch-tree/lastPathFails.vpr create mode 100644 src/test/resources/viper/branch-tree/multipleMethods.vpr create mode 100644 src/test/resources/viper/branch-tree/noBranches.vpr create mode 100644 src/test/resources/viper/branch-tree/onlyIf.vpr create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/allPathsCorrect_expected create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/firstPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/lastPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/noBranches_expected create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/onlyIf_expected create mode 100644 src/test/resources/viper/branch-tree/reportAllErrors/while_expected create mode 100644 src/test/resources/viper/branch-tree/reportTwoErrors/firstPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/reportTwoErrors/lastPathFails_expected create mode 100644 src/test/resources/viper/branch-tree/while.vpr create mode 100644 src/test/scala/viper/server/core/BranchTreeTests.scala create mode 100644 src/test/scala/viper/server/core/MockClient.scala diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index 4959c9ba..f4a2c147 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -176,15 +176,8 @@ case class StateChangeParams( stage: String = null, error: String = null) -case class BranchCondition(condition: String, negated: Boolean) -case class BranchFailurePath(conditions: Array[BranchCondition], isResultFatal: Boolean) -case class BranchClauseRange(ifLine: Int, elseLine: Int, methodEndLine: Int) -case class BranchFailureDetails(uri: String, - methodName : String, - methodIdentifierRange : Range, - paths: Array[BranchFailurePath], - clauseRange: BranchClauseRange, - cached : Boolean) + +case class BranchFailureDetails(uri: String, ranges: Array[Range]) case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int) diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala index 2d66237b..ce9636c6 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -7,6 +7,7 @@ package viper.silver.ast.utility.lsp import org.eclipse.lsp4j +import viper.server.frontends.lsp.file.branchTree.BranchTree trait HasCodeActions { def getCodeActions: Seq[CodeAction] @@ -18,7 +19,8 @@ case class CodeAction( cmd: Option[(String, Seq[AnyRef])], bound: SelectionBoundScopeTrait, kind: String, - resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty + resolvedDiags: Seq[lsp4j.Diagnostic] = Seq.empty, + branchTree : Option[BranchTree] = None ) extends SelectableInBound with HasRangePositions { override def rangePositions: Seq[RangePosition] = bound.rangePositions } diff --git a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala new file mode 100644 index 00000000..2eee8ae6 --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala @@ -0,0 +1,285 @@ +package viper.server.frontends.lsp.file.branchTree + +import viper.silver.utility.Common.PrintWriter + +import scala.annotation.tailrec + +class BranchTree { + private def incrementIfFatal(currBranchResultFatal: Int, isResultFatal: Boolean) : Int = + if (isResultFatal) Math.max(currBranchResultFatal,0)+1 else currBranchResultFatal + + protected[branchTree] def extend(branchConditions : Vector[(String, Boolean)], isResultFatal: Boolean) : Unit = { + (this, branchConditions) match { + case (b:Branch, bcs) if bcs.nonEmpty => + var currBranch = b + var negated = branchConditions.head._2 + var tail = branchConditions.tail + var next = true + while (tail.nonEmpty && next) { + next = false + val headExp = tail.head._1 + (currBranch.left, currBranch.right) match { + case (lb@Branch(exp,_,_,_,_),_) if headExp == exp && negated => + currBranch.leftResFatalCount = incrementIfFatal(currBranch.leftResFatalCount,isResultFatal) + currBranch = lb + next = true + case (_,rb@Branch(exp,_,_,_,_)) if headExp == exp && !negated => + currBranch.rightResFatalCount = incrementIfFatal(currBranch.rightResFatalCount,isResultFatal) + currBranch = rb + next = true + case _ => + } + if (next) { + negated = tail.head._2 + tail = tail.tail + } + } + val errorCount = if (isResultFatal) 1 else -1 + val subTree = BranchTree.generate(Vector((tail, isResultFatal)))// -1 for successful result + if (negated) { + currBranch.left = subTree.get + currBranch.leftResFatalCount = errorCount + } else { + currBranch.right = subTree.get + currBranch.rightResFatalCount = errorCount + } + case _=> + } + } + + + private def even(n: Int) = (n & 1) == 0 + private def buildTreeStrRec(fatalCount: Int) : (Vector[String], Int, Int) = { + this match { + case Leaf if fatalCount == -1 => (Vector("✔"), 0, 0) + case Leaf if fatalCount > 0 => (Vector("Error"), 2, 2) // ✘ + case _ : Branch => this.buildTreeStr() + case _ => (Vector("?"), 0, 0) + } + } + private def buildTreeStr() : (Vector[String], Int, Int) = { + this match { + case Branch(exp, left, right, leftErrCount, rightErrCount) => + val expStrLen = exp.length + + var boxMiddle = "│ " + exp + (if (even(exp.length)) " " else "") + " │" + val boxLen = boxMiddle.length + val halfBoxLen = boxLen / 2 + + var (leftStrVec, _, prevLeftRightBoxLen) = left.buildTreeStrRec(leftErrCount) + var (rightStrVec, prevRightLeftBoxLen, _) = right.buildTreeStrRec(rightErrCount) + + val halfExpStrLen = expStrLen / 2 + val leftBoxLen = leftStrVec.head.length + val rightBoxLen = rightStrVec.head.length + + var leftFiller = halfBoxLen - leftBoxLen + if (leftFiller > 0) { + leftStrVec = leftStrVec.map(str => " " * leftFiller + str) + leftFiller = 0 + } else { + leftFiller = -leftFiller + } + + var rightFiller = halfBoxLen - rightBoxLen + if (rightFiller > 0) { + rightStrVec = rightStrVec.map(str => str + " " * rightFiller) + rightFiller = 0 + } else { + rightFiller = -rightFiller + } + + val boxTop = " " * leftFiller + "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + "─┐" + " " * rightFiller + boxMiddle = " " * leftFiller + boxMiddle + " " * rightFiller + val boxBottom = " " * leftFiller + "└─" + "─" * halfExpStrLen + "┬" + "─" * halfExpStrLen + "─┘" + " " * rightFiller + + leftStrVec = leftStrVec.map(str => str + " ") + leftStrVec +:= " " * (leftFiller+halfExpStrLen-prevLeftRightBoxLen) + "F┌" + "─" * prevLeftRightBoxLen + "┴" + rightStrVec +:= "─" * prevRightLeftBoxLen + "┐T" + " " * (rightFiller+halfExpStrLen-prevRightLeftBoxLen) + + if (leftStrVec.length > rightStrVec.length){ + for(_ <- 0 to leftStrVec.length - rightStrVec.length) + { + rightStrVec :+= " "*rightStrVec.head.length + } + } else { + for(_ <- 0 to rightStrVec.length - leftStrVec.length) + { + leftStrVec :+= " "*leftStrVec.head.length + } + } + (boxTop +: boxMiddle +: boxBottom +: (leftStrVec zip rightStrVec).map(t => t._1 + t._2), leftFiller + halfBoxLen, rightFiller + halfBoxLen) + case _ => (Vector.empty, -1, -1) // Should not happen + } + } + + + private def fill(vec : Vector[String], filler :Int): Vector[String] = { + vec.grouped(4) + .flatMap(elems => { + Vector( + " "*filler + elems(0) + " "*filler, + " "*filler + elems(1) + "─"*filler, + " "*filler + elems(2) + " "*filler, + " "*filler + elems(3) + " "*filler + ) + }).toVector + } + private def buildPathStr() : String = { + var currTree : BranchTree = this + var maxBoxLen = 5 // for 'Error' + var path = Vector[String]() + var side = Vector[String]() + while (currTree != Leaf) { + currTree match { + case b@Branch(e, l, r, lc, rc) => + val expStr = e.toString + val halfExpStrLen = expStr.length / 2 + val (pathTaken, pathNotTaken) = if (b.isRightFatal) ("T", "F") else ("F","T") + + val boxTop = "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + s"─┐ $pathNotTaken " + val boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " ├──" + val boxBottom = "└─" + "─" * halfExpStrLen + "┬" + "─" * halfExpStrLen + "─┘ " + val conDown = " " * (halfExpStrLen+2) + s"│$pathTaken " + " " * halfExpStrLen + var box = Vector(boxTop, boxMiddle, boxBottom, conDown) + + val boxLen = boxMiddle.length-2 + val filler = Math.abs(maxBoxLen - boxLen) / 2 + if (maxBoxLen > boxLen) box = fill(box, filler) else path = fill(path, filler) + maxBoxLen = Math.max(maxBoxLen, boxLen) + + (if(b.isRightFatal) lc else rc) match { + case -1 => side ++= Vector("\n"," ✔\n","\n","\n") + case 0 => side ++= Vector("\n"," ?\n","\n","\n") + case _ => side ++= Vector("\n"," Error\n","\n","\n") + } + + path ++= box + currTree = if (b.isRightFatal) r else l // influenced by order of verification results (true branch results before left) + case _ => currTree = Leaf + } + } + val filler = maxBoxLen/2 + val combined = path.zip(side).map(t => t._1+t._2) + ((" "*filler + "│" + " "*filler + "\n") +: combined :+ (" "*(filler-2)+"Error\n")) + .reduce((str, s) => str + s) + } + + def getErrorCount: Int = { + this match { + case Branch(_,_,_,lf,rf) => Math.max(lf,0) + Math.max(rf,0) + case _ => 0 + } + } + + def prettyPrint() : String = { + if (this.getErrorCount == 1) { + this.buildPathStr() + } else { + this.buildTreeStr()._1.reduce((str, s) => str + "\n" + s) + "\n" + } + } + + private def leafToDotNodeContent(fatalCount : Int): String = { + fatalCount match { + case -1 => "label=\"✔\",shape=\"octagon\",style=\"filled\", fillcolor=\"palegreen\"" + case 1 => "label=\"Error\",shape=\"octagon\",style=\"filled\", fillcolor=\"lightsalmon\"" + case _ => "label=\"?\",shape=\"octagon\",style=\"filled\", fillcolor=\"lightgoldenrodyellow\"" + } + } + private def writeDotFileRec(writer: java.io.PrintWriter, visitedCount : Int = 0) : Int = { + this match { + case Branch(exp,left,right,leftResFatalCount,rightResFatalCount) => + val parentIdn = s"B$visitedCount" + writer.write(s" $parentIdn[shape=\"square\",label=\"${exp.toString}\"];\n") + val newVisitedCountLeft = visitedCount + 1 + val visitedCountLeft = left match { + case _ : Branch => + val leftBranchIdn = s"B$newVisitedCountLeft" + val visitedCountLeft_ = left.writeDotFileRec(writer, newVisitedCountLeft) + writer.write(s" $parentIdn -> $leftBranchIdn[label=\"F\"];\n") + visitedCountLeft_ + case Leaf => + val leftLeafIdn = s"B$newVisitedCountLeft" + writer.write(s" $leftLeafIdn[${leafToDotNodeContent(leftResFatalCount)}];\n") + writer.write(s" $parentIdn -> $leftLeafIdn [label=\"F\"];\n") + newVisitedCountLeft + } + val newVisitedCountRight = visitedCountLeft + 1 + val visitedCountRight = right match { + case _ : Branch => + val rightBranchIdn = s"B$newVisitedCountRight" + val visitedCountRight_ = right.writeDotFileRec(writer, newVisitedCountRight) + writer.write(s" $parentIdn -> $rightBranchIdn[label=\"T\"];\n") + visitedCountRight_ + case Leaf => + val rightLeafIdn = s"B$newVisitedCountRight" + writer.write(s" $rightLeafIdn[${leafToDotNodeContent(rightResFatalCount)}];\n") + writer.write(s" $parentIdn -> $rightLeafIdn [label=\"T\"];\n") + newVisitedCountRight + } + visitedCountRight + case _ => 0 + } + } + + def toDotFile(): Unit = { + val writer = PrintWriter(new java.io.File(BranchTree.DotFilePath),append=true) + writer.write("digraph {\n") + this.writeDotFileRec(writer) + writer.write("}\n") + writer.close() + } +} + +object BranchTree { + val DotFilePath = s"${java.nio.file.Paths.get(System.getProperty("java.io.tmpdir"), ".vscode")}/BranchTree.dot" + + @tailrec + private def generatePathRec(expressions: Vector[(String, Boolean)], + errorCount: Int, + result: BranchTree): BranchTree = { + expressions.length match { + case 0 => result + case _ => + val (lastExp, negated) = expressions.last + negated match { + case true => + generatePathRec(expressions.init, errorCount, Branch(lastExp, result, Leaf, errorCount, 0)) + case _ => + generatePathRec(expressions.init, errorCount, Branch(lastExp, Leaf, result, 0, errorCount)) + } + } + } + + @tailrec + private def generateRec(exploredPaths: Vector[(Vector[(String, Boolean)],Boolean)], result: BranchTree): BranchTree = { // result.instanceOf[Branch] must hold + exploredPaths.length match { + case 0 => result + case _ => + val (expressions, isResultFatal) = exploredPaths.head + result.extend(expressions, isResultFatal) + generateRec(exploredPaths.tail, result) + } + } + + def generate(exploredPaths: Vector[(Vector[(String, Boolean)],Boolean)]): Option[BranchTree] = { + exploredPaths.length match { + case 0 => None + case _ => + val (expressions, isResultFatal) = exploredPaths.head + val path = generatePathRec(expressions, if (isResultFatal) 1 else -1, Leaf) // -1 or distinguishing successful from no result at leaves + Some(generateRec(exploredPaths.tail, path)) + } + } +} + +object Leaf extends BranchTree +case class Branch(var exp : String, + var left: BranchTree, + var right: BranchTree, + protected[branchTree] var leftResFatalCount: Int, + protected[branchTree] var rightResFatalCount: Int) extends BranchTree { + def isLeftFatal : Boolean = leftResFatalCount > 0 + def isRightFatal : Boolean = rightResFatalCount > 0 +} \ No newline at end of file diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index b9cec819..d5bab387 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,11 +7,11 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} -import org.eclipse.lsp4j.{CodeActionKind, Position} +import org.eclipse.lsp4j.{CodeActionKind, DiagnosticSeverity, Position} import viper.server.frontends.lsp -import viper.server.frontends.lsp.{BranchClauseRange, BranchCondition, BranchFailureDetails, BranchFailurePath, Common} import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ +import viper.server.frontends.lsp.file.branchTree.BranchTree import viper.silver.ast import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} import viper.silver.reporter._ @@ -117,39 +117,40 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends private def handleExploredBranches(eb: ExploredBranches): Unit = { if (eb.paths.nonEmpty) { + val branchTree = BranchTree.generate(eb.paths) + val mRp = task.content.methodIdentToRangePosition(eb.method) if (!reportedExploredBranches.contains(mRp)) { + + val cacheFlag = if (eb.cached) "(cached)" else "" + branchTree.map(tree => { + task.addDiagnostic(false)( + Seq(Diagnostic( + backendClassName = backendClassName, + position = mRp, + message = s"Branch fails. ${cacheFlag} \n${tree.prettyPrint()}", + severity = DiagnosticSeverity.Error, + cached = eb.cached, + errorMsgPrefix = None + ))) + + //val idnRange = Common.toRange(mRp) + //val (ifLn, elseLn, methodEndLn) = task.getBranchRange(task.file_uri, eb.method, tree.) + /*if (details.nonEmpty) coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri,Array()) + )*/ + }) + task.addCodeAction(false)(Seq( CodeAction("Display explored branches", None, Some("viper.displayExploredBranches", Seq(task.file_uri, eb.method.name)), SelectionBoundScope(mRp), CodeActionKind.QuickFix, + branchTree=branchTree ))) - val paths = eb.paths.map(e => { - val (conds, isResultFatal) = e - val transformedConds = conds.map(c => { - val (cond, negated) = c - BranchCondition(cond, negated) - }).toArray - BranchFailurePath(transformedConds, isResultFatal) - }).toArray - reportedExploredBranches += mRp - - val idnRange = Common.toRange(mRp) - val (ifLn, elseLn, methodEndLn) = task.getFirstBranchClauseLines(task.file_uri, eb.method) - coordinator.sendBranchFailureDetails( - BranchFailureDetails(task.file_uri, - eb.method.name, - idnRange, - paths, - BranchClauseRange(ifLn, - elseLn, - methodEndLn), - eb.cached) - ) } } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index bb700f5e..833f18dc 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -229,6 +229,7 @@ case object CodeActionTranslator extends Translates[lsp.CodeAction, lsp4j.CodeAc val workspaceEdit = new lsp4j.WorkspaceEdit(edits) codeAction.setEdit(workspaceEdit) }) + ca.branchTree.foreach(bt => bt.toDotFile()) codeAction.setDiagnostics(ca.resolvedDiags.asJava) codeAction.setKind(ca.kind) codeAction diff --git a/src/test/resources/viper/branch-tree/allPathsCorrect.vpr b/src/test/resources/viper/branch-tree/allPathsCorrect.vpr new file mode 100644 index 00000000..f00c6ff1 --- /dev/null +++ b/src/test/resources/viper/branch-tree/allPathsCorrect.vpr @@ -0,0 +1,10 @@ +define P(z) z == true + +method foo(b: Bool) returns (z: Bool) +ensures P(z) { + if (b) { + z := true + } else { + z := true + } +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/default/allPathsCorrect_expected b/src/test/resources/viper/branch-tree/default/allPathsCorrect_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/allPathsCorrect_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/default/firstPathFails_expected b/src/test/resources/viper/branch-tree/default/firstPathFails_expected new file mode 100644 index 00000000..118145ee --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/firstPathFails_expected @@ -0,0 +1,10 @@ + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error diff --git a/src/test/resources/viper/branch-tree/default/lastPathFails_expected b/src/test/resources/viper/branch-tree/default/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/default/multipleMethods_expected b/src/test/resources/viper/branch-tree/default/multipleMethods_expected new file mode 100644 index 00000000..864299d3 --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/multipleMethods_expected @@ -0,0 +1,20 @@ + │ + ┌─┴─┐ F + │ a ├──── ? + └─┬─┘ + │T +┌───┴───┐ F +│ bcde ├── ? +└───┬───┘ + │T + Error + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/default/noBranches_expected b/src/test/resources/viper/branch-tree/default/noBranches_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/noBranches_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/default/onlyIf_expected b/src/test/resources/viper/branch-tree/default/onlyIf_expected new file mode 100644 index 00000000..2035a798 --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/onlyIf_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ F +│ d ├── ? +└─┬─┘ + │T +Error diff --git a/src/test/resources/viper/branch-tree/default/while_expected b/src/test/resources/viper/branch-tree/default/while_expected new file mode 100644 index 00000000..3b4a031d --- /dev/null +++ b/src/test/resources/viper/branch-tree/default/while_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/firstPathFails.vpr b/src/test/resources/viper/branch-tree/firstPathFails.vpr new file mode 100644 index 00000000..e896a90f --- /dev/null +++ b/src/test/resources/viper/branch-tree/firstPathFails.vpr @@ -0,0 +1,19 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := !(bcde && a) // failure + } else { + z := (bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) + } + } +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/lastPathFails.vpr b/src/test/resources/viper/branch-tree/lastPathFails.vpr new file mode 100644 index 00000000..a1618e5d --- /dev/null +++ b/src/test/resources/viper/branch-tree/lastPathFails.vpr @@ -0,0 +1,19 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := (bcde && a) + } else { + z := !(bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) // failure + } + } +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/multipleMethods.vpr b/src/test/resources/viper/branch-tree/multipleMethods.vpr new file mode 100644 index 00000000..f527fed0 --- /dev/null +++ b/src/test/resources/viper/branch-tree/multipleMethods.vpr @@ -0,0 +1,37 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := !(bcde && a) // failure + } else { + z := (bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) + } + } +} + +method bar(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + if (a) { + if (bcde) { + z := (bcde && a) + } else { + z := !(bcde && !a) + } + } else { + if (c) { + z := !(c && a) + } else { + z := !(!c && !a) // failure + } + } +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/noBranches.vpr b/src/test/resources/viper/branch-tree/noBranches.vpr new file mode 100644 index 00000000..7ae9e52e --- /dev/null +++ b/src/test/resources/viper/branch-tree/noBranches.vpr @@ -0,0 +1,6 @@ +define P(z) z == true + +method foo(b: Bool) returns (z: Bool) +ensures P(z) { + z := true +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/onlyIf.vpr b/src/test/resources/viper/branch-tree/onlyIf.vpr new file mode 100644 index 00000000..6f8c13eb --- /dev/null +++ b/src/test/resources/viper/branch-tree/onlyIf.vpr @@ -0,0 +1,14 @@ +define P(z) z == true + +method foo(a: Int, b: Int, d: Bool) returns (z: Bool) +ensures P(z) { + var a_ : Int := a + var b_ : Int := b + if (d) { + a_ := 3 + b_ := 3 + } + var c: Int + c := a_ / b_ + z := c > 1 +} \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/allPathsCorrect_expected b/src/test/resources/viper/branch-tree/reportAllErrors/allPathsCorrect_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/allPathsCorrect_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/firstPathFails_expected b/src/test/resources/viper/branch-tree/reportAllErrors/firstPathFails_expected new file mode 100644 index 00000000..ef79e48e --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/firstPathFails_expected @@ -0,0 +1,9 @@ + ┌─┴─┐ + │ a │ + └─┬─┘ + F┌──┴─────┐T + ┌─┴─┐ ┌───┴───┐ + │ c │ │ bcde │ + └─┬─┘ └───┬───┘ + F┌──┴┐T F┌──┴──┐T +Error ✔ Error Error diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/lastPathFails_expected b/src/test/resources/viper/branch-tree/reportAllErrors/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/noBranches_expected b/src/test/resources/viper/branch-tree/reportAllErrors/noBranches_expected new file mode 100644 index 00000000..49263a9e --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/noBranches_expected @@ -0,0 +1 @@ +Verification successful. \ No newline at end of file diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/onlyIf_expected b/src/test/resources/viper/branch-tree/reportAllErrors/onlyIf_expected new file mode 100644 index 00000000..b43faf03 --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/onlyIf_expected @@ -0,0 +1,5 @@ + ┌─┴─┐ + │ d │ + └─┬─┘ + F┌──┴──┐T +Error Error diff --git a/src/test/resources/viper/branch-tree/reportAllErrors/while_expected b/src/test/resources/viper/branch-tree/reportAllErrors/while_expected new file mode 100644 index 00000000..3b4a031d --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportAllErrors/while_expected @@ -0,0 +1,6 @@ + │ +┌─┴─┐ T +│ a ├── ? +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/reportTwoErrors/firstPathFails_expected b/src/test/resources/viper/branch-tree/reportTwoErrors/firstPathFails_expected new file mode 100644 index 00000000..4e978087 --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportTwoErrors/firstPathFails_expected @@ -0,0 +1,9 @@ +┌─┴─┐ +│ a │ +└─┬─┘ +F┌┴─────┐T + ? ┌───┴───┐ + │ bcde │ + └───┬───┘ + F┌──┴──┐T + Error Error diff --git a/src/test/resources/viper/branch-tree/reportTwoErrors/lastPathFails_expected b/src/test/resources/viper/branch-tree/reportTwoErrors/lastPathFails_expected new file mode 100644 index 00000000..abf6886c --- /dev/null +++ b/src/test/resources/viper/branch-tree/reportTwoErrors/lastPathFails_expected @@ -0,0 +1,10 @@ + │ +┌─┴─┐ T +│ a ├── ✔ +└─┬─┘ + │F +┌─┴─┐ T +│ c ├── ✔ +└─┬─┘ + │F +Error diff --git a/src/test/resources/viper/branch-tree/while.vpr b/src/test/resources/viper/branch-tree/while.vpr new file mode 100644 index 00000000..307ed321 --- /dev/null +++ b/src/test/resources/viper/branch-tree/while.vpr @@ -0,0 +1,13 @@ +define P(z) z == true + +method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool) +requires a ==> c +ensures P(z) { + while (a) { + if (bcde) { + z := !(bcde && a) + } else { + z := !(bcde && !a) + } + } +} \ No newline at end of file diff --git a/src/test/scala/viper/server/core/BranchTreeTests.scala b/src/test/scala/viper/server/core/BranchTreeTests.scala new file mode 100644 index 00000000..ebd4b886 --- /dev/null +++ b/src/test/scala/viper/server/core/BranchTreeTests.scala @@ -0,0 +1,131 @@ +package viper.server.core + +// 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 distrcibuted with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2019 ETH Zurich. + +import org.scalatest.{Assertion, Succeeded} +import org.scalatest.funsuite.AnyFunSuite +import viper.server.ViperConfig +import viper.server.frontends.lsp.{ClientCoordinator, ViperServerService} +import viper.server.frontends.lsp.file.FileManager +import viper.server.utility.AstGenerator +import viper.server.vsi.JobNotFoundException +import viper.silver.ast.utility.DiskLoader +import viper.silver.logger.SilentLogger + +import java.nio.file.Paths +import scala.concurrent.duration.Duration +import scala.concurrent.{Await, Future} +import scala.util.{Failure, Success} + +class BranchTreeTests extends AnyFunSuite { + + val testDir = Paths.get("src", "test", "resources", "viper","branch-tree").toString + private val ast_gen = new AstGenerator(SilentLogger().get) + + def executeTestDefault(fileName: String) : Unit = executeTest(fileName, "default") + + test("FirstPathFailsPath") { + executeTestDefault("firstPathFails") + } + test("LastPathFailsPath") { + executeTestDefault("lastPathFails") + } + test("WhilePath") { + executeTestDefault("while") + } + test("OnlyIfPath") { + executeTestDefault("onlyIf") + } + test("AllPathsPath") { + executeTestDefault("allPathsCorrect") + } + test("NoBranchesPath") { + executeTestDefault("noBranches") + } + test("MultipleMethodsPath") { + executeTestDefault("multipleMethods") + } + + def executeTestReportAllErrors(fileName: String) : Unit = executeTest(fileName, "reportAllErrors", List("--numberOfErrorsToReport", "0")) + + test("FirstPathFailsTreeAll") { + executeTestReportAllErrors("firstPathFails") + } + test("LastPathFailsTreeAll") { + executeTestReportAllErrors("lastPathFails") + } + test("WhileTreeAll") { + executeTestReportAllErrors("while") + } + test("OnlyIfTreeAll") { + executeTestReportAllErrors("onlyIf") + } + test("AllPathsCorrectTreeAll") { + executeTestReportAllErrors("allPathsCorrect") + } + test("NoBranchesTreeAll") { + executeTestReportAllErrors("noBranches") + } + + def executeTestReportTwoErrors(fileName: String) : Unit = executeTest(fileName, "reportTwoErrors", List("--numberOfErrorsToReport", "2")) + + test("FirstPathFailsTreeTwo") { + executeTestReportTwoErrors("firstPathFails") + } + test("LastPathFailsTreeTwo") { + executeTestReportTwoErrors("lastPathFails") + } + + def getExpectedString(fileName: String, expectedFolder : String): String = { + val expectedFilePath = Paths.get(testDir,expectedFolder,fileName+"_expected") + DiskLoader.loadContent(expectedFilePath).get + } + + def executeTest(fileName: String, expectedFolder : String, args: List[String] = List.empty) + : Unit = { + val filePath = Paths.get(testDir,s"$fileName.vpr") + val expected = getExpectedString(fileName, expectedFolder) + + val viperConfig = new ViperConfig(Seq.empty) + val siliconConfig: SiliconConfig = SiliconConfig(args) + val ast = ast_gen.generateViperAst(filePath.toString).get + + val verificationContext = new DefaultVerificationExecutionContext() + val core = new ViperServerService(viperConfig)(verificationContext) + val started = core.start() + + // execute testCode + val testFuture = started.flatMap(_ => { + val coordinator = new ClientCoordinator(core)(verificationContext) + coordinator.setClient(new MockClient()) + val fileManager = FileManager(filePath.toAbsolutePath.toUri.toString, coordinator, None)(verificationContext) + val jid = core.verify("some-program-id", siliconConfig, ast) + val relayActorRef = verificationContext.actorSystem.actorOf(fileManager.props(Some("silicon"))) + core.streamMessages(jid, relayActorRef, true).getOrElse(Future.failed(JobNotFoundException)) + .map(_=>{ + val diags = fileManager.getDiagnostic() + val actual = if (diags.nonEmpty) diags.map(_.getMessage) + .filter(m => m.startsWith("Branch")) + .flatMap(m => m.split("\n").filterNot(l => l.startsWith(" (") + ||l.startsWith(" [") + ||l.startsWith("Branch")) + ).map(str => str+"\n").reduce((str,s)=>str+s) else "Verification successful." + assert(actual.contains(expected)) + })(verificationContext) + })(verificationContext) + val testWithShutdownFuture = testFuture.transformWith(testRes => { + val coreStopFuture = core.stop() + testRes match { + case Success(_) => coreStopFuture + case f: Failure[Assertion] => coreStopFuture.transform(_ => f)(verificationContext) + } + })(verificationContext) + Await.result(testWithShutdownFuture, Duration.Inf) + } +} + + diff --git a/src/test/scala/viper/server/core/CoreServerSpec.scala b/src/test/scala/viper/server/core/CoreServerSpec.scala index 6e42b658..171e3113 100644 --- a/src/test/scala/viper/server/core/CoreServerSpec.scala +++ b/src/test/scala/viper/server/core/CoreServerSpec.scala @@ -10,13 +10,12 @@ import java.nio.file.Paths import akka.actor.{Actor, Props, Status} import akka.pattern.ask import akka.util.Timeout -import org.eclipse.lsp4j.{MessageActionItem, MessageParams, Position, PublishDiagnosticsParams, Range, ShowMessageRequestParams} import org.scalatest.exceptions.TestFailedException import org.scalatest.matchers.should.Matchers import org.scalatest.{Assertion, Outcome, Succeeded} import org.scalatest.wordspec.AnyWordSpec import viper.server.ViperConfig -import viper.server.frontends.lsp.{BranchFailureDetails, ClientCoordinator, GetIdentifierResponse, GetRangeResponse, GetViperFileEndingsResponse, HintMessage, IdeLanguageClient, LogParams, SetupProjectParams, StateChangeParams, UnhandledViperServerMessageTypeParams, VerificationNotStartedParams, ViperServerService} +import viper.server.frontends.lsp.{ClientCoordinator, ViperServerService} import viper.server.frontends.lsp.file.FileManager import viper.server.utility.AstGenerator import viper.server.vsi.{DefaultVerificationServerStart, JobNotFoundException, VerJobId} @@ -26,7 +25,6 @@ import viper.silver.logger.SilentLogger import viper.silver.reporter.{EntityFailureMessage, EntitySuccessMessage, Message, OverallFailureMessage, OverallSuccessMessage} import viper.silver.verifier.{AbstractError, VerificationResult, Failure => VerifierFailure, Success => VerifierSuccess} -import java.util.concurrent.CompletableFuture import scala.concurrent.duration._ import scala.concurrent.{Await, Future, Promise} import scala.util.{Failure, Success} @@ -340,14 +338,14 @@ class CoreServerSpec extends AnyWordSpec with Matchers { implicit val ctx: VerificationExecutionContext = context val siliconJid = verifySiliconWithoutCaching(core, ver_error_file) val siliconVerification = ViperCoreServerUtils.getResultsFuture(core, siliconJid).map { - case VerifierFailure(Seq(err)) => assert(!err.cached, "first verification should not be cached") + case VerifierFailure(Seq(err),_) => assert(!err.cached, "first verification should not be cached") case res => fail(s"expected a single entity failure from Silicon but got $res") } siliconVerification .map(_ => verifyCarbonWithCaching(core, ver_error_file)) .flatMap(carbonJid => ViperCoreServerUtils.getResultsFuture(core, carbonJid)) .map { - case VerifierFailure(Seq(err)) => assert(!err.cached, "verification should not reuse cache from other backend") + case VerifierFailure(Seq(err),_) => assert(!err.cached, "verification should not reuse cache from other backend") case res => fail(s"expected a single entity failure from Carbon but got $res") } }) @@ -421,24 +419,6 @@ class CoreServerSpec extends AnyWordSpec with Matchers { }) })(viperServerServiceFactory) - class MockClient extends IdeLanguageClient { - override def requestIdentifier(pos: Position): CompletableFuture[GetIdentifierResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) - override def requestRange(range: Range): CompletableFuture[GetRangeResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) - override def requestVprFileEndings(): CompletableFuture[GetViperFileEndingsResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) - override def requestSetupProject(param: SetupProjectParams): CompletableFuture[Unit] = CompletableFuture.failedFuture(new UnsupportedOperationException()) - override def notifyLog(param: LogParams): Unit = {} - override def notifyHint(param: HintMessage): Unit = {} - override def notifyUnhandledViperServerMessage(params: UnhandledViperServerMessageTypeParams): Unit = {} - override def notifyVerificationNotStarted(params: VerificationNotStartedParams): Unit = {} - override def notifyStateChanged(params: StateChangeParams): Unit = {} - override def sendBranchFailureInfo(params: BranchFailureDetails): Unit = {} - override def telemetryEvent(`object`: Any): Unit = {} - override def publishDiagnostics(diagnostics: PublishDiagnosticsParams): Unit = {} - override def showMessage(messageParams: MessageParams): Unit = {} - override def showMessageRequest(requestParams: ShowMessageRequestParams): CompletableFuture[MessageActionItem] = CompletableFuture.failedFuture(new UnsupportedOperationException()) - override def logMessage(message: MessageParams): Unit = {} - } - s"verifyMultipleFiles behalves as expected" in withServer[ViperCoreServer]({ (core, context) => // this unit tests makes sure that verifying two identical files using `verifyMultipleFiles` actually // triggers the cache @@ -447,7 +427,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { val file2 = "src/test/resources/viper/identical-versions/version2.vpr" def handleResult(file: String, res: VerificationResult): Assertion = res match { - case VerifierFailure(errors) => + case VerifierFailure(errors,_) => assert(errors.size == 1) assert(errors.head.cached == (file == file2)) case _ => fail(s"unexpected verification result for file $file") @@ -462,7 +442,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { def handleResult(file: String, res: VerificationResult): Assertion = res match { case VerifierSuccess => assert(file == fileBeforeModification) - case VerifierFailure(errors) => + case VerifierFailure(errors,_) => assert(file == fileAfterModification) assert(errors.size == 1) } @@ -491,7 +471,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { val fileAfterReordering = "src/test/resources/viper/reordered-domains/version2.vpr" def handleResult(file: String, res: VerificationResult): Assertion = (res: @unchecked) match { - case VerifierFailure(errors) => + case VerifierFailure(errors,_) => assert(errors.size == 1) val err = errors.head if (err.cached) { @@ -510,7 +490,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { val fileAfterReorderingDomainAxioms = "src/test/resources/viper/reordered-axioms/version3.vpr" def handleResult(file: String, res: VerificationResult): Assertion = (res: @unchecked) match { - case VerifierFailure(errors) => + case VerifierFailure(errors,_) => assert(errors.size == 1) val err = errors.head if (err.cached) { @@ -684,7 +664,7 @@ class CoreServerSpec extends AnyWordSpec with Matchers { var errPosBeforeReordering: Option[ast.Position] = None var errPosAfterReordering: Option[ast.Position] = None def handleResult(file: String, res: VerificationResult): Assertion = (res: @unchecked) match { - case VerifierFailure(errors) => + case VerifierFailure(errors,_) => assert(errors.size == 1) val err = errors.head if (file == fileBeforeReordering) { diff --git a/src/test/scala/viper/server/core/MockClient.scala b/src/test/scala/viper/server/core/MockClient.scala new file mode 100644 index 00000000..7e13fb4a --- /dev/null +++ b/src/test/scala/viper/server/core/MockClient.scala @@ -0,0 +1,24 @@ +package viper.server.core + +import org.eclipse.lsp4j.{MessageActionItem, MessageParams, Position, PublishDiagnosticsParams, Range, ShowMessageRequestParams} +import viper.server.frontends.lsp.{BranchFailureDetails, GetIdentifierResponse, GetRangeResponse, GetViperFileEndingsResponse, HintMessage, IdeLanguageClient, LogParams, SetupProjectParams, StateChangeParams, UnhandledViperServerMessageTypeParams, VerificationNotStartedParams} + +import java.util.concurrent.CompletableFuture + +class MockClient extends IdeLanguageClient { + override def requestIdentifier(pos: Position): CompletableFuture[GetIdentifierResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) + override def requestRange(range: Range): CompletableFuture[GetRangeResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) + override def requestVprFileEndings(): CompletableFuture[GetViperFileEndingsResponse] = CompletableFuture.failedFuture(new UnsupportedOperationException()) + override def requestSetupProject(param: SetupProjectParams): CompletableFuture[Unit] = CompletableFuture.failedFuture(new UnsupportedOperationException()) + override def notifyLog(param: LogParams): Unit = {} + override def notifyHint(param: HintMessage): Unit = {} + override def notifyUnhandledViperServerMessage(params: UnhandledViperServerMessageTypeParams): Unit = {} + override def notifyVerificationNotStarted(params: VerificationNotStartedParams): Unit = {} + override def notifyStateChanged(params: StateChangeParams): Unit = {} + override def sendBranchFailureInfo(params: BranchFailureDetails): Unit = {} + override def telemetryEvent(`object`: Any): Unit = {} + override def publishDiagnostics(diagnostics: PublishDiagnosticsParams): Unit = {} + override def showMessage(messageParams: MessageParams): Unit = {} + override def showMessageRequest(requestParams: ShowMessageRequestParams): CompletableFuture[MessageActionItem] = CompletableFuture.failedFuture(new UnsupportedOperationException()) + override def logMessage(message: MessageParams): Unit = {} +} From 0cead860749d740daab424efc3c217a422ec3e69 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Mon, 24 Mar 2025 21:18:06 +0100 Subject: [PATCH 39/44] Update red beams --- .../server/frontends/lsp/file/BranchTree.scala | 5 ++--- .../server/frontends/lsp/file/Branches.scala | 13 ++++++++++--- .../server/frontends/lsp/file/RelayActor.scala | 17 ++++++++++------- 3 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala index 2eee8ae6..f6e7daed 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala @@ -133,12 +133,11 @@ class BranchTree { while (currTree != Leaf) { currTree match { case b@Branch(e, l, r, lc, rc) => - val expStr = e.toString - val halfExpStrLen = expStr.length / 2 + val halfExpStrLen = e.length / 2 val (pathTaken, pathNotTaken) = if (b.isRightFatal) ("T", "F") else ("F","T") val boxTop = "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + s"─┐ $pathNotTaken " - val boxMiddle = "│ " + expStr + (if (even(expStr.length)) " " else "") + " ├──" + val boxMiddle = "│ " + e + (if (even(e.length)) " " else "") + " ├──" val boxBottom = "└─" + "─" * halfExpStrLen + "┬" + "─" * halfExpStrLen + "─┘ " val conDown = " " * (halfExpStrLen+2) + s"│$pathTaken " + " " * halfExpStrLen var box = Vector(boxTop, boxMiddle, boxBottom, conDown) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala index 59493f43..83627f65 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala @@ -9,9 +9,11 @@ package viper.server.frontends.lsp.file import viper.server.frontends.lsp.Common import viper.silver.ast.Method import viper.silver.parser.PKw +import org.eclipse.lsp4j +import org.eclipse.lsp4j.Position trait Branches extends ProjectAware { - def getFirstBranchClauseLines(uri: String, method: Method): (Int,Int,Int) = { + def getBeamRange(uri: String, method: Method, failsInElse: Boolean): lsp4j.Range = { var start = Common.toPosition(method.pos) val m = getInProject(uri) var currPos = m.content.iterForward(start) @@ -29,7 +31,9 @@ trait Branches extends ProjectAware { case '}' => openBraceCount -= 1 if (openBraceCount == 0) { - val ln = if (!m.content.fileContent(p.getLine).contains(PKw.Else.keyword)) p.getLine+1 + val ln = if (!m.content.fileContent(p.getLine) + .contains(PKw.Else.keyword)) + p.getLine+1 else p.getLine if (start.getLine == middleLn) { middleLn = ln @@ -44,6 +48,9 @@ trait Branches extends ProjectAware { } currPos = m.content.iterForward(currPos.get._2).drop(1).find { case (c, _) => c == '{' || c == '}' } } while (currPos.isDefined && openBraceCount > 0) - (start.getLine, middleLn, endLn) + new lsp4j.Range( + new Position(if (failsInElse) middleLn else start.getLine,0), + new Position(endLn,0) + ) } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index d5bab387..8c0395f3 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -9,9 +9,10 @@ package viper.server.frontends.lsp.file import akka.actor.{Actor, Props, Status} import org.eclipse.lsp4j.{CodeActionKind, DiagnosticSeverity, Position} import viper.server.frontends.lsp +import viper.server.frontends.lsp.BranchFailureDetails import viper.server.frontends.lsp.VerificationState._ import viper.server.frontends.lsp.VerificationSuccess._ -import viper.server.frontends.lsp.file.branchTree.BranchTree +import viper.server.frontends.lsp.file.branchTree.{Branch, BranchTree} import viper.silver.ast import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} import viper.silver.reporter._ @@ -128,17 +129,19 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends Seq(Diagnostic( backendClassName = backendClassName, position = mRp, - message = s"Branch fails. ${cacheFlag} \n${tree.prettyPrint()}", + message = s"Branch fails. $cacheFlag \n${tree.prettyPrint()}", severity = DiagnosticSeverity.Error, cached = eb.cached, errorMsgPrefix = None ))) - //val idnRange = Common.toRange(mRp) - //val (ifLn, elseLn, methodEndLn) = task.getBranchRange(task.file_uri, eb.method, tree.) - /*if (details.nonEmpty) coordinator.sendBranchFailureDetails( - BranchFailureDetails(task.file_uri,Array()) - )*/ + val failsInElse = if (tree.isInstanceOf[Branch]) + tree.asInstanceOf[Branch].isLeftFatal + else false + val beamRange = task.getBeamRange(task.file_uri, eb.method, failsInElse) + coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri,Array(beamRange)) + ) }) task.addCodeAction(false)(Seq( From bb93a7b5af228bcff570f36bcd2f198ec2ed3e76 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 25 Mar 2025 21:23:36 +0100 Subject: [PATCH 40/44] Fix display DOT --- src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 8c0395f3..60f8a259 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -147,7 +147,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends task.addCodeAction(false)(Seq( CodeAction("Display explored branches", None, - Some("viper.displayExploredBranches", Seq(task.file_uri, eb.method.name)), + Some("viper.displayExploredBranches", Seq(eb.method.name, BranchTree.DotFilePath)), SelectionBoundScope(mRp), CodeActionKind.QuickFix, branchTree=branchTree From a6ed9789147fc2dbd4badb18d4b6b00cc29e4979 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Tue, 25 Mar 2025 22:17:26 +0100 Subject: [PATCH 41/44] Fix display DOT --- src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala index f6e7daed..5ba47c43 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala @@ -223,7 +223,7 @@ class BranchTree { } def toDotFile(): Unit = { - val writer = PrintWriter(new java.io.File(BranchTree.DotFilePath),append=true) + val writer = PrintWriter(new java.io.File(BranchTree.DotFilePath)) writer.write("digraph {\n") this.writeDotFileRec(writer) writer.write("}\n") From 25cea5267038aea4908e9d23d97ca9d349663ce7 Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Thu, 27 Mar 2025 10:36:40 +0100 Subject: [PATCH 42/44] Move Statement --- .../scala/viper/server/frontends/lsp/file/RelayActor.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 60f8a259..29d03698 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -118,10 +118,9 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends private def handleExploredBranches(eb: ExploredBranches): Unit = { if (eb.paths.nonEmpty) { - val branchTree = BranchTree.generate(eb.paths) - val mRp = task.content.methodIdentToRangePosition(eb.method) if (!reportedExploredBranches.contains(mRp)) { + val branchTree = BranchTree.generate(eb.paths) val cacheFlag = if (eb.cached) "(cached)" else "" branchTree.map(tree => { From 06f39a8b08fc52d622169d81d9bd989fae54908c Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Sat, 29 Mar 2025 20:57:14 +0100 Subject: [PATCH 43/44] Remove whitespace --- .../scala/viper/server/frontends/lsp/file/BranchTree.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala index 5ba47c43..cb117f09 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala @@ -201,7 +201,7 @@ class BranchTree { case Leaf => val leftLeafIdn = s"B$newVisitedCountLeft" writer.write(s" $leftLeafIdn[${leafToDotNodeContent(leftResFatalCount)}];\n") - writer.write(s" $parentIdn -> $leftLeafIdn [label=\"F\"];\n") + writer.write(s" $parentIdn -> $leftLeafIdn[label=\"F\"];\n") newVisitedCountLeft } val newVisitedCountRight = visitedCountLeft + 1 @@ -214,7 +214,7 @@ class BranchTree { case Leaf => val rightLeafIdn = s"B$newVisitedCountRight" writer.write(s" $rightLeafIdn[${leafToDotNodeContent(rightResFatalCount)}];\n") - writer.write(s" $parentIdn -> $rightLeafIdn [label=\"T\"];\n") + writer.write(s" $parentIdn -> $rightLeafIdn[label=\"T\"];\n") newVisitedCountRight } visitedCountRight @@ -267,7 +267,7 @@ object BranchTree { case 0 => None case _ => val (expressions, isResultFatal) = exploredPaths.head - val path = generatePathRec(expressions, if (isResultFatal) 1 else -1, Leaf) // -1 or distinguishing successful from no result at leaves + val path = generatePathRec(expressions, if (isResultFatal) 1 else -1, Leaf) // -1 for distinguishing successful from no result at leaves Some(generateRec(exploredPaths.tail, path)) } } From 796fa9a343422841a4ccefa341357e861189b07b Mon Sep 17 00:00:00 2001 From: 7i6ht Date: Wed, 9 Apr 2025 09:12:41 +0200 Subject: [PATCH 44/44] Fix beams error --- .../scala/viper/server/frontends/lsp/file/Branches.scala | 4 ++-- .../scala/viper/server/frontends/lsp/file/RelayActor.scala | 7 ++++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala index 83627f65..2440680c 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Branches.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala @@ -13,7 +13,7 @@ import org.eclipse.lsp4j import org.eclipse.lsp4j.Position trait Branches extends ProjectAware { - def getBeamRange(uri: String, method: Method, failsInElse: Boolean): lsp4j.Range = { + def getBeamRange(uri: String, method: Method, failsInElseOnly: Boolean): lsp4j.Range = { var start = Common.toPosition(method.pos) val m = getInProject(uri) var currPos = m.content.iterForward(start) @@ -49,7 +49,7 @@ trait Branches extends ProjectAware { currPos = m.content.iterForward(currPos.get._2).drop(1).find { case (c, _) => c == '{' || c == '}' } } while (currPos.isDefined && openBraceCount > 0) new lsp4j.Range( - new Position(if (failsInElse) middleLn else start.getLine,0), + new Position(if (failsInElseOnly) middleLn else start.getLine,0), new Position(endLn,0) ) } diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 29d03698..760ae05b 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -134,10 +134,11 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends errorMsgPrefix = None ))) - val failsInElse = if (tree.isInstanceOf[Branch]) - tree.asInstanceOf[Branch].isLeftFatal + val failsInElseOnly = if (tree.isInstanceOf[Branch]) + { val branch = tree.asInstanceOf[Branch] + !branch.isRightFatal && branch.isLeftFatal } else false - val beamRange = task.getBeamRange(task.file_uri, eb.method, failsInElse) + val beamRange = task.getBeamRange(task.file_uri, eb.method, failsInElseOnly) coordinator.sendBranchFailureDetails( BranchFailureDetails(task.file_uri,Array(beamRange)) )