diff --git a/carbon b/carbon index 759f3c1e..5d09b506 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 759f3c1e80724d5ab6c53fc9cfb989ccc4be1fc6 +Subproject commit 5d09b5069c8fee032fcacca91ddf26c3cc27f499 diff --git a/silicon b/silicon index 46a35ffb..4403e454 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 46a35ffb154afc8962a9e3646673bd62ccff33c4 +Subproject commit 4403e45469d460fdf2aaba4bd8ccd6c7909fdffd diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index 1b6b0bfa..fc893848 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.ExploredBranches 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], exploredBranches: Option[ExploredBranches]) 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.exploredBranches)) } }) @@ -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[ExploredBranches])] = methodsToVerify.map((m: Method) => { // Results come back irrespective of program Member. + var exploredBranches : Option[ExploredBranches] = None val cacheable_errors: Option[List[AbstractVerificationError]] = for { cache_errs <- verificationResult match { - case Failure(errs) => + case Failure(errs,eb) => + exploredBranches = if (eb.nonEmpty) eb else exploredBranches 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, exploredBranches) }) // 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]],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) 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 => @@ -326,10 +329,14 @@ 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,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) + 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..a970cc24 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.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 @@ -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.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 @@ -262,11 +264,12 @@ object ViperCache extends Cache { file: String, method: Method, program: Program, - errors: List[AbstractVerificationError]): List[CacheEntry] = { + errors: List[AbstractVerificationError], + exploredBranches: Option[ExploredBranches]): 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, exploredBranches) 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], + 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))) + SerializedViperCacheContent(write(ViperCacheContent(errors,exploredBranches))) } } @@ -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], exploredBranches: Option[ExploredBranches]) /** 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], exploredBranches: Option[ExploredBranches]) 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/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index c6ffcf29..8cf8ca5c 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 @@ -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.sendBranchFailureInfo(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) @@ -212,7 +221,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/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 100eb08a..f4a2c147 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -176,6 +176,9 @@ case class StateChangeParams( stage: String = null, error: String = null) + +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/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala index 0b614f3b..3eff256e 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 sendBranchFailureInfo(params: BranchFailureDetails): Unit } 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 e33c58d5..a05e45c7 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,14 @@ package viper.silver.parser +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 -import viper.silver.parser.PStringLiteral 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 @@ -30,12 +34,19 @@ 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 | _: PExpandedMacro => false + case _ => true + }, { + 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 + } } object HasGotoDefinitions { @@ -81,21 +92,38 @@ 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(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(isArgument = false, c.pretty, None), getSigHelpPart(arg)) + }) :+ SignatureHelpPart(isArgument = false, s"${args.r.pretty}", None) } - // 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(isArgument = false, s"${n.keyword.pretty}${n.idndef.pretty}", None) + // Args + val args = argsToSigHelpPart[PAnyFormalArgDecl](n.args) + // Tail + val tail = SignatureHelpPart(isArgument = false, s"${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(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(isArgument = false, s" ${n.body.pretty}", None) + Seq(SignatureHelp(start +: mappedParams :+ tail, PLspDeclaration.documentation(n), bound)) + }).flatten } - }).flatten } object HasSuggestionScopeRanges { @@ -119,6 +147,146 @@ object HasCompletionProposals { }).flatten } +object HasCodeActions { + private def isIncreasingSelfAssignment(e: PBinExp): Boolean = { + e.op.rs match { + case PSymOp.Plus | PSymOp.Mul | PKwOp.Union | PSymOp.Append => true + case _ => false + } + } + 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.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]].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.isEmpty) { + 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 = 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 + }) + 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.isEmpty) { + selfAssignment = findSelfAssignment(w.body, getIdentifierNames(cond.right)) + condBound = cond.left + middle = cond.right + } + val whileRp = RangePosition(w) + val editRange = getEditRange(w.body.ss.l) + 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", Some((invariant , er)), None, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty), + CodeAction("Add decreases", Some((decreases, er)), None, SelectionBoundScope(wRp), CodeActionKind.Empty, Seq.empty) + ) + }).flatten + } + + 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", + None, + Some(("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", + Some((s"$beforeKeyword$keyword acc(${f.pretty})\n$indent", new Range(editPos, editPos))), + None, + 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 + } +} //// // 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..ce9636c6 --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeAction.scala @@ -0,0 +1,26 @@ +// 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 +import viper.server.frontends.lsp.file.branchTree.BranchTree + +trait HasCodeActions { + def getCodeActions: Seq[CodeAction] +} + +case class CodeAction( + title: String, + 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 { + 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..cb117f09 --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/file/BranchTree.scala @@ -0,0 +1,284 @@ +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 halfExpStrLen = e.length / 2 + val (pathTaken, pathNotTaken) = if (b.isRightFatal) ("T", "F") else ("F","T") + + val boxTop = "┌─" + ("─" * halfExpStrLen) + "┴" + ("─" * halfExpStrLen) + s"─┐ $pathNotTaken " + 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) + + 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)) + 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 for 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/Branches.scala b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala new file mode 100644 index 00000000..2440680c --- /dev/null +++ b/src/main/scala/viper/server/frontends/lsp/file/Branches.scala @@ -0,0 +1,56 @@ +// 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 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 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) + .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 + do { + val (c,p) = currPos.get + c match { + case '}' => + openBraceCount -= 1 + if (openBraceCount == 0) { + 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 '{' => + 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( + new Position(if (failsInElseOnly) middleLn else start.getLine,0), + new Position(endLn,0) + ) + } +} 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..214e75b8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -10,9 +10,12 @@ 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)] { @@ -60,14 +63,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 = { @@ -88,6 +96,20 @@ case class FileContent(path: Path) extends DiskLoader { } }) } + def methodIdentToRangePosition(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/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..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) @@ -178,6 +183,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], keyword: Option[(String, lsp4j.Range)]) = 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..fa0b9d48 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),None) + else getInProject(uri).getCodeAction(Some(pos),None) + } + 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/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]) 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..760ae05b 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala @@ -7,14 +7,16 @@ 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.{Branch, BranchTree} import viper.silver.ast +import viper.silver.ast.utility.lsp.{CodeAction, RangePosition, SelectionBoundScope} 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 { @@ -100,6 +102,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 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))) @@ -113,6 +116,48 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends case _ => reportedErrors.contains((err, None)) } + private def handleExploredBranches(eb: ExploredBranches): Unit = { + if (eb.paths.nonEmpty) { + 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 => { + 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 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, failsInElseOnly) + coordinator.sendBranchFailureDetails( + BranchFailureDetails(task.file_uri,Array(beamRange)) + ) + }) + + task.addCodeAction(false)(Seq( + CodeAction("Display explored branches", + None, + Some("viper.displayExploredBranches", Seq(eb.method.name, BranchTree.DotFilePath)), + SelectionBoundScope(mRp), + CodeActionKind.QuickFix, + branchTree=branchTree + ))) + + reportedExploredBranches += 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") @@ -141,6 +186,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,(pos:Position)=>task.getDiagnosticBy(Some(pos),None))) } case StatisticsReport(m, f, p, _, _) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] StatisticsReport") @@ -178,6 +224,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 ExploredBranchesReport(exploredBranches) => + handleExploredBranches(exploredBranches) case OverallFailureMessage(_, verificationTime, failure) => coordinator.logger.debug(s"[receive@${task.filename}/${backendClassName.isDefined}] OverallFailureMessage") task.state = VerificationReporting @@ -188,6 +236,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends // ViperServer produces EntitySuccessMessage and EntityFailureMessages) val newErrors = failure.errors.filterNot(hasAlreadyBeenReported) markErrorsAsReported(newErrors) + 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/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index e5230808..7492d269 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,21 @@ 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 viper.silver.ast.{AbstractSourcePosition, Position} import org.eclipse.lsp4j -import viper.silver.ast.utility.lsp.RangePosition -import viper.silver.ast.HasLineColumn -import viper.silver.ast.LineColumnPosition +import viper.server.frontends.lsp.{Common} + import java.nio.file.Path case class VerificationHandler(server: lsp.ViperServerService) { @@ -70,7 +67,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 @@ -235,10 +232,18 @@ trait VerificationManager extends Manager { def props(backendClassName: Option[String]): Props + 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) + } + } + def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { + // Add diagnostics val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") - val files = HashSet[String]() - val diags = errors.map(err => { coordinator.logger.info(s"Handling error ${err.toString()}") var errorType: String = "" @@ -265,19 +270,8 @@ trait VerificationManager extends Manager { 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 = 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 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 "" 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..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 @@ -12,6 +12,7 @@ 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 scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer @@ -29,8 +30,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") } @@ -210,3 +211,28 @@ 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(ca.title) + 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) + }) + ca.branchTree.foreach(bt => bt.toDotFile()) + codeAction.setDiagnostics(ca.resolvedDiags.asJava) + codeAction.setKind(ca.kind) + codeAction + }) + } +} \ No newline at end of file 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 b723514e..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.{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,23 +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 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 @@ -446,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") @@ -461,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) } @@ -490,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) { @@ -509,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) { @@ -683,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 = {} +}