Display failing branches

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,19 +297,19 @@ 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())
       }
     }
 
     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)
       }
     }
   }

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 {
 

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
     }
   })
 

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)

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"
 }

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)

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)
 
 /**

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
 }

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` ---