Merge pull request #804 from viperproject/sem-highlight

Add information required for LSP features to Parse AST

Author: marcoeilers

silver

@@ -11,16 +11,13 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 
 class TryBlockParserPlugin(fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
   import fastparse._
-  import viper.silver.parser.FastParserCompanion.whitespace
-  import fp.{FP, block, ParserExtension}
+  import viper.silver.parser.FastParserCompanion.{PositionParsing, reservedKw, whitespace}
+  import fp.{ParserExtension, lineCol, _file, stmtBlock}
 
-
-  private val tryKeyword = "try"
-
-  def tryBlock[_:P]: P[PTryBlock] =FP("try" ~/ block) map { case (pos, s) => PTryBlock(s)(pos) }
+  def tryBlock[$: P]: P[PTryBlock] = P((P(PTryKeyword) ~ stmtBlock()) map (PTryBlock.apply _).tupled).pos
 
   override def beforeParse(input: String, isImported: Boolean): String = {
-    ParserExtension.addNewKeywords(Set(tryKeyword))
+    ParserExtension.addNewKeywords(Set(PTryKeyword))
     ParserExtension.addNewStmtAtEnd(tryBlock(_))
 
     input

src/main/scala/extensions/TryBlockParserPlugin.scala

@@ -8,10 +8,12 @@ package viper.silicon.extensions
 
 import viper.silver.ast._
 import viper.silver.ast.pretty.PrettyPrintPrimitives
-import viper.silver.parser.{NameAnalyser, PExtender, PNode, PStmt, Translator, TypeChecker}
+import viper.silver.parser.{NameAnalyser, PExtender, PStmt, Translator, TypeChecker, PKw, PKeywordStmt, PReserved}
 
-final case class PTryBlock(body: PStmt)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PStmt {
-  override val getSubnodes: Seq[PNode] = Seq(body)
+/** Keyword used to define `try` statement. */
+case object PTryKeyword extends PKw("try") with PKeywordStmt
+
+final case class PTryBlock(kw: PReserved[PTryKeyword.type], body: PStmt)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PStmt {
 
   override def translateStmt(translator: Translator): Stmt = {
     TryBlock(translator.stmt(body))(translator.liftPos(this))

src/main/scala/extensions/TryBlockStmt.scala

@@ -678,8 +678,21 @@ object evaluator extends EvaluationRules {
 
         val body = eQuant.exp
         // Remove whitespace in identifiers to avoid parsing problems for the axiom profiler.
-        val posString = viper.silicon.utils.ast.sourceLine(sourceQuant).replaceAll(" ", "")
-        val name = s"prog.l$posString"
+        // TODO: add flag to enable old behavior for AxiomProfiler
+        val fallbackName = "l" + viper.silicon.utils.ast.sourceLine(sourceQuant).replaceAll(" ", "")
+        val posString = if (!sourceQuant.pos.isInstanceOf[ast.AbstractSourcePosition]) {
+          fallbackName
+        } else {
+          val pos = sourceQuant.pos.asInstanceOf[ast.AbstractSourcePosition]
+          if (pos.end.isEmpty) {
+            fallbackName
+          } else {
+            val file = pos.file.toString()
+            val end = pos.end.get
+            s"$file@${pos.start.line}@${pos.start.column}@${end.line}@${end.column}"
+          }
+        }
+        val name = s"prog.$posString"
         evalQuantified(s, qantOp, eQuant.variables, Nil, Seq(body), Some(eTriggers), name, pve, v){
           case (s1, tVars, _, Seq(tBody), tTriggers, (tAuxGlobal, tAux), v1) =>
             val tAuxHeapIndep = tAux.flatMap(v.quantifierSupporter.makeTriggersHeapIndependent(_, v1.decider.fresh))

src/main/scala/rules/Evaluator.scala

@@ -172,13 +172,13 @@ class DefaultMainVerifier(config: Config,
           val res = viper.silicon.utils.ast.autoTrigger(forall, forall.autoTrigger)
           if (res.triggers.isEmpty)
             reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos))))
-          reporter report QuantifierChosenTriggersMessage(res, res.triggers)
+          reporter report QuantifierChosenTriggersMessage(res, res.triggers, forall.triggers)
           res
         case exists: ast.Exists =>
           val res = viper.silicon.utils.ast.autoTrigger(exists, exists.autoTrigger)
           if (res.triggers.isEmpty)
             reporter.report(WarningsDuringVerification(Seq(VerifierWarning("No triggers provided or inferred for quantifier.", res.pos))))
-          reporter report QuantifierChosenTriggersMessage(res, res.triggers)
+          reporter report QuantifierChosenTriggersMessage(res, res.triggers, exists.triggers)
           res
       }, Traverse.BottomUp)
 

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -13,7 +13,7 @@ import viper.silicon.interfaces.SiliconMappedCounterexample
 import viper.silicon.reporting.{ExtractedModel, ExtractedModelEntry, LitIntEntry, LitPermEntry, NullRefEntry, RecursiveRefEntry, RefEntry, SeqEntry}
 import viper.silicon.state.terms.Rational
 import viper.silver.parser.FastParserCompanion.whitespace
-import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIntLit, PLookup, PUnExp}
+import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIntLit, PLookup, PUnExp, PSymOp}
 import viper.silver.verifier.{FailureContext, VerificationError}
 
 import java.nio.file.Path
@@ -112,7 +112,7 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path,
   def meetsExpectations(model1: ExpectedCounterexample, model2: ExtractedModel): Boolean = {
     model1.exprs.forall {
       case accPred: PAccPred => containsAccessPredicate(accPred, model2)
-      case PBinExp(lhs, "==", rhs) => containsEquality(lhs, rhs, model2)
+      case PBinExp(lhs, r, rhs) if r.rs == PSymOp.EqEq => containsEquality(lhs, rhs, model2)
     }
   }
 
@@ -130,13 +130,13 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path,
   /** resolves `expr` to a model entry in the given model. In case it's a field access, the corresponding permissions are returned as well */
   def resolve(expr: PExp, model: ExtractedModel): Option[(ExtractedModelEntry, Option[Rational])] = expr match {
     case PIntLit(value) => Some(LitIntEntry(value), None)
-    case PUnExp("-", PIntLit(value)) => Some(LitIntEntry(-value), None)
-    case PBinExp(PIntLit(n), "/", PIntLit(d)) => Some(LitPermEntry(Rational(n, d)), None)
-    case PIdnUse(name) => model.entries.get(name).map((_, None))
-    case PFieldAccess(rcv, idnuse) => resolveWoPerm(rcv, model).flatMap {
+    case PUnExp(r, PIntLit(value)) if r.rs == PSymOp.Neg => Some(LitIntEntry(-value), None)
+    case PBinExp(PIntLit(n), r, PIntLit(d)) if r.rs == PSymOp.Div => Some(LitPermEntry(Rational(n, d)), None)
+    case idnuse: PIdnUse => model.entries.get(idnuse.name).map((_, None))
+    case PFieldAccess(rcv, _, idnuse) => resolveWoPerm(rcv, model).flatMap {
       case RefEntry(_, fields) => fields.get(idnuse.name)
     }
-    case PLookup(base, idx) => resolveWoPerm(Vector(base, idx), model).flatMap {
+    case PLookup(base, _, idx, _) => resolveWoPerm(Vector(base, idx), model).flatMap {
       case Vector(SeqEntry(_, values), LitIntEntry(evaluatedIdx)) if values.size > evaluatedIdx => Some(values(evaluatedIdx.toInt), None)
     }
   }
@@ -184,7 +184,7 @@ class CounterexampleParser(fp: FastParser) {
 case class ExpectedCounterexample(exprs: Seq[PExp]) {
   assert(exprs.forall {
     case _: PAccPred => true
-    case PBinExp(_, "==", _) => true
+    case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true
     case _ => false
   })
 }