diff --git a/silver b/silver index 399835d1b..9f67812b8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 399835d1b2b4dadf2331493f2d74729c0708f3f9 +Subproject commit 9f67812b81fe8680531000956ed99c2a454b369e diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index fd19cafcc..3e141c46c 100644 --- a/src/main/scala/extensions/TryBlockParserPlugin.scala +++ b/src/main/scala/extensions/TryBlockParserPlugin.scala @@ -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 diff --git a/src/main/scala/extensions/TryBlockStmt.scala b/src/main/scala/extensions/TryBlockStmt.scala index 917330736..12680ca08 100644 --- a/src/main/scala/extensions/TryBlockStmt.scala +++ b/src/main/scala/extensions/TryBlockStmt.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)) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index c5e85cc60..8a31e545f 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.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)) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 0db992bea..c0c39435d 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.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) diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index 4fee83ac9..95e2b26a5 100644 --- a/src/test/scala/CounterexampleTests.scala +++ b/src/test/scala/CounterexampleTests.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 }) }