From e92387832cdf58285686c89dae4eba0e47a9ee7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 15 May 2023 02:12:26 +0200 Subject: [PATCH 1/8] Update silver --- silver | 2 +- src/test/scala/CounterexampleTests.scala | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/silver b/silver index c2c1b1183..a57e30780 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d +Subproject commit a57e30780d56d3da3b5e70e298236140315e1aaa diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index 4fee83ac9..1af786ab1 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, POperator, PUnExp} 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, POperator("=="), rhs) => containsEquality(lhs, rhs, model2) } } @@ -130,8 +130,8 @@ 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 PUnExp(POperator("-"), PIntLit(value)) => Some(LitIntEntry(-value), None) + case PBinExp(PIntLit(n), POperator("/"), 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 RefEntry(_, fields) => fields.get(idnuse.name) @@ -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(_, POperator("=="), _) => true case _ => false }) } From e0c2984a66634650b42539cf6e326fad6d395ea2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Wed, 31 May 2023 15:35:35 +0200 Subject: [PATCH 2/8] Store more info in name of quantifier --- .../scala/extensions/TryBlockParserPlugin.scala | 4 ++-- src/main/scala/rules/Evaluator.scala | 17 +++++++++++++++-- .../scala/verifier/DefaultMainVerifier.scala | 4 ++-- 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index fd19cafcc..c69947911 100644 --- a/src/main/scala/extensions/TryBlockParserPlugin.scala +++ b/src/main/scala/extensions/TryBlockParserPlugin.scala @@ -12,12 +12,12 @@ 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 fp.{FP, stmtBlock, ParserExtension} private val tryKeyword = "try" - def tryBlock[_:P]: P[PTryBlock] =FP("try" ~/ block) map { case (pos, s) => PTryBlock(s)(pos) } + def tryBlock[_:P]: P[PTryBlock] =FP("try" ~/ stmtBlock) map { case (pos, s) => PTryBlock(s)(pos) } override def beforeParse(input: String, isImported: Boolean): String = { ParserExtension.addNewKeywords(Set(tryKeyword)) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 610cc514e..d48ff42bf 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -669,8 +669,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 4e3809788..8e3d1fe53 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -167,13 +167,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) From de1fc95e259d542bb41a6dcd28d77b699cab1914 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Fri, 9 Jun 2023 03:47:17 +0200 Subject: [PATCH 3/8] Update silver --- src/test/scala/CounterexampleTests.scala | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index 1af786ab1..b1e8625e4 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, POperator, PUnExp} +import viper.silver.parser.{FastParser, PAccPred, PBinExp, PExp, PFieldAccess, PIdnUse, PIntLit, PLookup, POperatorSymbol, PUnExp} 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, POperator("=="), rhs) => containsEquality(lhs, rhs, model2) + case PBinExp(lhs, POperatorSymbol("=="), rhs) => containsEquality(lhs, rhs, model2) } } @@ -130,8 +130,8 @@ 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(POperator("-"), PIntLit(value)) => Some(LitIntEntry(-value), None) - case PBinExp(PIntLit(n), POperator("/"), PIntLit(d)) => Some(LitPermEntry(Rational(n, d)), None) + case PUnExp(POperatorSymbol("-"), PIntLit(value)) => Some(LitIntEntry(-value), None) + case PBinExp(PIntLit(n), POperatorSymbol("/"), 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 RefEntry(_, fields) => fields.get(idnuse.name) @@ -184,7 +184,7 @@ class CounterexampleParser(fp: FastParser) { case class ExpectedCounterexample(exprs: Seq[PExp]) { assert(exprs.forall { case _: PAccPred => true - case PBinExp(_, POperator("=="), _) => true + case PBinExp(_, POperatorSymbol("=="), _) => true case _ => false }) } From 0713de14e54b7b503a0a5086aad8ec4166971bc0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 18 Jul 2023 17:38:42 +0200 Subject: [PATCH 4/8] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index a57e30780..00611a702 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit a57e30780d56d3da3b5e70e298236140315e1aaa +Subproject commit 00611a7026dcf8cd495647655e781fe74a0702da From 9f7f099b23ae779ae178da642a852e2065c6d99b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 16 Jan 2024 15:23:41 +0100 Subject: [PATCH 5/8] Fix update --- silver | 2 +- src/main/scala/extensions/TryBlockParserPlugin.scala | 11 ++++------- src/main/scala/extensions/TryBlockStmt.scala | 11 +++++++++-- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/silver b/silver index 00611a702..db6534214 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 00611a7026dcf8cd495647655e781fe74a0702da +Subproject commit db65342143fa51c4ca304b75f5377a7286ee0c81 diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index c69947911..33681fc22 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, stmtBlock, 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" ~/ stmtBlock) 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.keyword)) ParserExtension.addNewStmtAtEnd(tryBlock(_)) input diff --git a/src/main/scala/extensions/TryBlockStmt.scala b/src/main/scala/extensions/TryBlockStmt.scala index 917330736..0ffa67901 100644 --- a/src/main/scala/extensions/TryBlockStmt.scala +++ b/src/main/scala/extensions/TryBlockStmt.scala @@ -8,9 +8,16 @@ 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, PNode, PStmt, Translator, TypeChecker, PKw, PKeywordStmt, PReserved} +import viper.silver.ast.utility.lsp.BuiltinFeature -final case class PTryBlock(body: PStmt)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PStmt { +/** Keyword used to define `try` statement. */ +case object PTryKeyword extends PKw("try", TODOTryDoc) with PKeywordStmt +case object TODOTryDoc extends BuiltinFeature( + """TODO""".stripMargin.replaceAll("\n", " ") +) + +final case class PTryBlock(kw: PReserved[PTryKeyword.type], body: PStmt)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PExtender with PStmt { override val getSubnodes: Seq[PNode] = Seq(body) override def translateStmt(translator: Translator): Stmt = { From bf4b1fa64bae0c25e7201196b6d5b770f8146eae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 16 Jan 2024 20:56:08 +0100 Subject: [PATCH 6/8] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index db6534214..d565779b7 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit db65342143fa51c4ca304b75f5377a7286ee0c81 +Subproject commit d565779b7acbb8a728a1abb3a88a743c60cd3fcd From 18fd0d25ab475fedd00b0737c003d3530b0c1a92 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Fri, 9 Feb 2024 13:52:13 +0100 Subject: [PATCH 7/8] Fixes --- silver | 2 +- .../scala/extensions/TryBlockParserPlugin.scala | 2 +- src/main/scala/extensions/TryBlockStmt.scala | 9 ++------- src/test/scala/CounterexampleTests.scala | 16 ++++++++-------- 4 files changed, 12 insertions(+), 17 deletions(-) diff --git a/silver b/silver index d565779b7..f0ccd0c88 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d565779b7acbb8a728a1abb3a88a743c60cd3fcd +Subproject commit f0ccd0c88096717ca62579923ee6b817fd9029e6 diff --git a/src/main/scala/extensions/TryBlockParserPlugin.scala b/src/main/scala/extensions/TryBlockParserPlugin.scala index 33681fc22..3e141c46c 100644 --- a/src/main/scala/extensions/TryBlockParserPlugin.scala +++ b/src/main/scala/extensions/TryBlockParserPlugin.scala @@ -17,7 +17,7 @@ class TryBlockParserPlugin(fp: FastParser) extends SilverPlugin with ParserPlugi 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(PTryKeyword.keyword)) + 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 0ffa67901..12680ca08 100644 --- a/src/main/scala/extensions/TryBlockStmt.scala +++ b/src/main/scala/extensions/TryBlockStmt.scala @@ -8,17 +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, PKw, PKeywordStmt, PReserved} -import viper.silver.ast.utility.lsp.BuiltinFeature +import viper.silver.parser.{NameAnalyser, PExtender, PStmt, Translator, TypeChecker, PKw, PKeywordStmt, PReserved} /** Keyword used to define `try` statement. */ -case object PTryKeyword extends PKw("try", TODOTryDoc) with PKeywordStmt -case object TODOTryDoc extends BuiltinFeature( - """TODO""".stripMargin.replaceAll("\n", " ") -) +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 val getSubnodes: Seq[PNode] = Seq(body) override def translateStmt(translator: Translator): Stmt = { TryBlock(translator.stmt(body))(translator.liftPos(this)) diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/CounterexampleTests.scala index b1e8625e4..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, POperatorSymbol, 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, POperatorSymbol("=="), 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(POperatorSymbol("-"), PIntLit(value)) => Some(LitIntEntry(-value), None) - case PBinExp(PIntLit(n), POperatorSymbol("/"), 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(_, POperatorSymbol("=="), _) => true + case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true case _ => false }) } From 37f29197f7cf1ff46c3a2be835781b9cb1bc7df1 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 11 Feb 2024 12:03:37 +0100 Subject: [PATCH 8/8] Updating silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 09309050f..9f67812b8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 09309050f384edfa21cc29e8c09ffc6fa187a0ec +Subproject commit 9f67812b81fe8680531000956ed99c2a454b369e