Biabduction lsp with inference mode

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

@@ -13,12 +13,14 @@ import net.liftweb.json.JsonAST.JObject
 import viper.server.core.ViperCache.logger
 import viper.server.vsi._
 import viper.silver.{ast => vpr}
-import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, Sub, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
+import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, FilePosition, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, IdentifierPosition, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LineColumnPosition, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, SourcePosition, Sub, TranslatedPosition, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
 import viper.silver.utility.CacheHelper
 import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellformed, FoldFailed, HeuristicsFailed, IfFailed, InhaleFailed, Internal, LetWandFailed, UnfoldFailed, _}
-import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors}
+import viper.silver.verifier.{AbstractVerificationError, FailureContext, VerificationError, errors}
 import net.liftweb.json.Serialization.{read, write}
 import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints}
+import viper.silicon.interfaces.SiliconAbductionFailureContext
+import viper.silver.ast.utility.lsp.RangePosition
 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
@@ -83,7 +85,11 @@ object ViperCache extends Cache {
           val content = read[ViperCacheContent](ce.content.asInstanceOf[SerializedViperCacheContent].content)
           logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName")
           // set cached flag:
-          val cachedErrors = content.errors.map(setCached)
+          val cachedErrors = content.errors.map(e => {
+            val ce = setCached(e._1)
+            ce.failureContexts = e._2
+            ce
+          })
           CacheResult(concerning_method, cachedErrors)
         } catch {
           case e: Throwable =>
@@ -307,7 +313,7 @@ object ViperCache extends Cache {
     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.map(e => (e, e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext]))))))
   }
 }
 
@@ -521,7 +527,9 @@ object ViperCacheHelper {
     classOf[InternalReason], classOf[FeatureUnsupported], classOf[UnexpectedNode], classOf[AssertionFalse], classOf[EpsilonAsParam],
     classOf[ReceiverNull], classOf[DivisionByZero], classOf[NegativePermission], classOf[InsufficientPermission], classOf[InvalidPermMultiplication],
     classOf[MagicWandChunkNotFound], classOf[QPAssertionNotInjective], classOf[LabelledStateNotReached], classOf[SeqIndexNegative],
-    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained]
+    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained], classOf[SiliconAbductionFailureContext], classOf[LineColumnPosition],
+    classOf[FilePosition], classOf[RangePosition], classOf[IdentifierPosition], classOf[SourcePosition], classOf[TranslatedPosition],
+    classOf[IdentifierPosition]
   )) {
 
     override def serialize: PartialFunction[Any, JObject] = {
@@ -556,7 +564,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, Seq[FailureContext])])
 
 /** An access path holds a List of Numbers
   *

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

@@ -209,6 +209,14 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     }
   }
 
+  def sendInferenceResults(irs: InferenceResultParams): Unit = {
+    try{
+      client.get.notifyInferenceResults(irs)
+    } catch {
+      case e: Throwable => logger.debug(s"Error while sending inference results: $e")
+    }
+  }
+
   def refreshEndings(): Future[Array[String]] = {
     client.map{_.requestVprFileEndings().asScala.map(response => {
       _vprFileEndings = Some(response.fileEndings)

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

@@ -32,6 +32,7 @@ object S2C_Commands {
   final val Log = "Log"
   final val Hint = "Hint"
   final val VerificationNotStarted = "VerificationNotStarted"
+  final val InferenceResults = "InferenceResults"
   // final val StopDebugging = "StopDebugging"
   // final val StepsAsDecorationOptions = "StepsAsDecorationOptions"
   // final val HeapGraph = "HeapGraph"

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

@@ -178,6 +178,17 @@ case class StateChangeParams(
               stage: String = null,
               error: String = null)
 
+case class InferenceResultParams(
+              inferenceResults: Array[InferenceResult])
+
+case class InferenceResult(
+              start_line: Int,
+              start_col: Int,
+              end_line: Int,
+              end_col: Int,
+              edit: String,
+              file_uri: String)
+
 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.InferenceResults)
+  def notifyInferenceResults(irs: InferenceResultParams): Unit
 }

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

@@ -312,8 +312,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 ctxt = params.getContext
+    var diags = Seq.empty[Diagnostic]
+    ctxt.getDiagnostics.asScala.foreach(diag => diags = diags :+ diag)
+    coordinator.getRoot(uri).getCodeAction(uri, diags).map(cacts => cacts.map(cact => Either.forRight[Command, CodeAction](cact)).asJava).asJava.toCompletableFuture
   }
 
   override def formatting(params: DocumentFormattingParams) = {

src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala

@@ -13,8 +13,12 @@ trait HasCodeLens {
 case class CodeLens(
     /** The range in which this code lens is valid. Should only span a single line. */
     range: RangePosition,
+    /** The text this code lens displays. */
+    title: String,
     /** The command this code lens represents. */
-    command: String,
+    command: Option[String] = None,
+    /** The command this code lens represents. */
+    args: Option[Seq[AnyRef]] = None
 ) extends HasRangePositions with BelongsToFile {
   override def rangePositions: Seq[RangePosition] = Seq(range)
   override def file = range.file

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

@@ -40,6 +40,7 @@ trait ManagesLeaf {
   def resetDiagnostics(first: Boolean): Unit
   def resetContainers(first: Boolean): Unit
   def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
 
   def getInFuture[T](f: => T): Future[T]
 }

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

@@ -18,12 +18,27 @@ import viper.server.frontends.lsp.Lsp4jSemanticHighlight
 import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
+import viper.silicon.biabduction.ProgramEdit
 
 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 {
   override def rangePositions: Seq[lsp.RangePosition] = Seq(position)
   override def file: Path = position.file
 }
 
+case class CodeAction(backendClassName: Option[String],
+                      title: String,
+                      kind: String,
+                      diags: Seq[Diagnostic],
+                      command: Option[(String, String)],
+                      edit: Option[Seq[ProgramEdit]],
+                      diagkey: Option[lsp4j.Diagnostic],
+                      fileinfo: PathInfo
+                     ) extends lsp.HasRangePositions with lsp.BelongsToFile with utility.HasKey[lsp4j.Diagnostic] {
+  override def rangePositions: Seq[lsp.RangePosition] = diags.map(_.position)
+  override def file: Path = fileinfo.path
+  override val key: lsp4j.Diagnostic = diagkey.orNull
+}
+
 trait Manager {
   val file: PathInfo
   val content: FileContent
@@ -33,6 +48,9 @@ trait Manager {
   def addContainer(c: utility.LspContainer[_, _, _, _, _]): Unit
   def resetContainers(first: Boolean): Unit
 
+  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction]
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
+
   def getCodeLens(): Seq[lsp4j.CodeLens]
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit
 
@@ -71,6 +89,7 @@ trait Manager {
 }
 
 /** Stores and handles all aspects relating the the lsp features:
+ *  - CodeAction
  *  - CodeLens
  *  - Diagnostic
  *  - DocumentSymbol
@@ -103,6 +122,20 @@ trait StandardManager extends Manager {
   }
 
 
+  // CodeAction
+  type CodeActionContainer = utility.StageMapContainer.MapContainer[CodeAction, lsp4j.Diagnostic, lsp4j.CodeAction]
+  val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator, () => {})
+  private def initCodeActionKey(codeAction: CodeAction): Seq[CodeAction] = {
+    var cas: Seq[CodeAction] = Seq.empty
+    codeAction.diags.foreach(diag => {
+      cas = cas :+ new CodeAction(codeAction.backendClassName, codeAction.title, codeAction.kind, Seq(diag), codeAction.command, codeAction.edit, Some(diagnosticContainer.translator.translate(diag)()), codeAction.fileinfo)
+    })
+    cas
+  }
+  containers.addOne(codeActionContainer)
+  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag)
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten)
+
   // CodeLens
   type CodeLensContainer = utility.StageArrayContainer.ArrayContainer[lsp.CodeLens, lsp4j.CodeLens]
   val codeLensContainer: CodeLensContainer = utility.LspContainer(utility.CodeLensTranslator, if (coordinator.client.isDefined) coordinator.client.get.refreshCodeLenses else () => {})

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

@@ -141,6 +141,8 @@ trait ProjectManager extends ProjectAware {
     })
     grouped foreach (g => toC(g._1)(g._2))
   }
+  override def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit =
+    addBtf(uri => getInProject(uri).addCodeAction(first), vs)
 
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit =
     addBtf(uri => getInProject(uri).addCodeLens(first), vs)
@@ -236,6 +238,8 @@ trait ProjectManager extends ProjectAware {
     }
   }
 
+  def getCodeAction(uri: String, diags: Seq[lsp4j.Diagnostic]): Future[Seq[lsp4j.CodeAction]] =
+    Future.successful(diags.map(diag => getInProject(uri).getCodeAction(diag)).flatten)
   // Can force a refresh in the future if we get new ones, so return immediately
   def getCodeLens(uri: String): Future[Seq[lsp4j.CodeLens]] =
     Future.successful(getInProject(uri).getCodeLens())

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

@@ -8,23 +8,27 @@ package viper.server.frontends.lsp.file
 
 import ch.qos.logback.classic.Logger
 import viper.server.frontends.lsp
+
 import scala.concurrent.Future
 import viper.server.core.ViperBackendConfig
 import viper.server.vsi.{AstJobId, VerJobId}
+
 import scala.concurrent.ExecutionContext
 import akka.actor.Props
-
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.server.frontends.lsp.VerificationState._
-
 import viper.silver.verifier.AbstractError
+
 import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
+import viper.server.frontends.lsp.{InferenceResult, InferenceResultParams}
 import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
+import viper.silicon.interfaces._
+import viper.silver.verifier._
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
   private var waitingOn: Option[Either[AstJobId, VerJobId]] = None
@@ -123,6 +127,7 @@ trait VerificationManager extends ManagesLeaf {
   //other
   var lastSuccess: VerificationSuccess = NA
   var internalErrorMessage: String = ""
+  var inferenceMode: Boolean = false
 
   //state specific to one verification
   var is_aborting: Boolean = false
@@ -212,6 +217,7 @@ trait VerificationManager extends ManagesLeaf {
   def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = {
     lastBackendClassName = Some(backendClassName)
     lastCustomArgs = Some(customArgs)
+    inferenceMode = customArgs.contains("--inferenceMode=full")
     val backend = ViperBackendConfig(backendClassName, customArgs)
 
     coordinator.logger.info(s"verify $filename ($backendClassName $customArgs)")
@@ -279,6 +285,8 @@ trait VerificationManager extends ManagesLeaf {
   def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = {
     val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("")
     val files = HashSet[String]()
+    var cas: Seq[CodeAction] = Seq.empty
+    var lsp_irs: Array[InferenceResult] = Array.empty
 
     val diags = errors.map(err => {
       coordinator.logger.info(s"Handling error ${err.toString()}")
@@ -327,12 +335,49 @@ trait VerificationManager extends ManagesLeaf {
 
       val cachFlag: String = if(err.cached) " (cached)" else ""
       val message = s"$errMsgPrefixWithWhitespace${err.readableMessage}$cachFlag"
-      (phase, Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix))
+      val diagnostic = Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix)
+      //If error contains inference results and inference mode is on error, create code action for inference results
+      if (errorType == "Verification error"){
+        err match {
+          case g: VerificationError =>
+            g.failureContexts.foreach {
+              case h1: SiliconAbductionFailureContext =>
+                h1.fix match {
+                  case Some(irs) =>
+                    irs.foreach(ir =>
+                      lsp_irs = lsp_irs :+ InferenceResult(
+                        start_line = ir.start.line,
+                        start_col = ir.start.column,
+                        end_line = ir.end.line,
+                        end_col = ir.end.column,
+                        edit = ir.newText,
+                        file_uri = this.file.file_uri)
+                    )
+                    cas = cas :+ CodeAction(backendClassName, irs.map(ir =>
+                      if (ir.newText.equals(""))
+                        "remove: Line " + ir.start.line + ", Col " + ir.start.column + " to Line " + ir.end.line + ", Col " + ir.end.column
+                      else
+                        "insert: " + ir.newText).foldLeft("")((cur: String, next: String) => if (cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                  case None => ()
+                }
+              case _ => ()
+            }
+          case _ => ()
+        }
+      }
+      (phase, diagnostic)
     })
+
+    if(inferenceMode){
+      coordinator.sendInferenceResults(InferenceResultParams(inferenceResults = lsp_irs))
+      return
+    }
+
     diagnosticCount += errors.size
     errorCount += diags.count(_._2.severity == lsp4j.DiagnosticSeverity.Error)
     diags.groupBy(d => d._1).foreach { case (phase, diags) =>
       this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2))
     }
+    this.addCodeAction(true)(cas)
   }
 }

src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala

@@ -17,6 +17,10 @@ import viper.silver.ast.utility.lsp
 import viper.silver.ast.utility.lsp.SelectionBoundScopeTrait
 import viper.silver.ast.utility.lsp.SelectionBoundKeywordTrait
 
+trait HasKey[K] {
+  val key: K
+}
+
 trait StageContainer[K, V, I] {
   var resetCount: Int = 0
   def reset(): Unit = {
@@ -54,6 +58,33 @@ object StageArrayContainer {
   implicit def default[V]: () => StageArrayContainer[V] = () => StageArrayContainer()
 }
 
+case class StageMapContainer[K, V <: HasKey[K]]() extends StageContainer[K, V, K]{
+  private val map: HashMap[K, Seq[V]] = HashMap()
+
+  override protected def innerReset(): Unit = map.clear()
+  override protected def innerAdd(v: V): K = {
+    map.put(v.key, map.getOrElse(v.key, Seq.empty) :+ v)
+    v.key
+  }
+  override def get(k: K): Seq[V] = {
+    map.getOrElse(k, Seq.empty)
+  }
+  override protected def innerUpdate(i: K, f: V => V): Boolean = {
+    if (!map.contains(i)) {
+      false
+    } else {
+      map.put(i, map(i).map(v => f(v)))
+      true
+    }
+  }
+  override def all(): Iterator[V] = map.values.flatten.iterator
+  override def filterInPlace(p: V => Boolean): Unit = map.values.map(vs => vs.filter(p))
+}
+object StageMapContainer {
+  type MapContainer[V <: HasRangePositions with BelongsToFile with HasKey[K], K, U] = LspContainer[StageMapContainer[K, V], K, V, K, U]
+  implicit def default[K, V <: HasKey[K]]: () => StageMapContainer[K, V] = () => StageMapContainer()
+}
+
 case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[(Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int)] {
   // Has a `scope` bound
   val localKeyword: HashMap[String, ArrayBuffer[V]] = HashMap()