From 64d54ad97a07643d4b63458634faf341762c6499 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 18 Feb 2023 21:30:25 +0100 Subject: [PATCH 1/9] First attempt to get annotations --- src/main/scala/viper/silver/ast/Ast.scala | 5 + .../viper/silver/parser/FastParser.scala | 18 +- .../scala/viper/silver/parser/ParseAst.scala | 9 + .../scala/viper/silver/parser/Resolver.scala | 5 + .../viper/silver/parser/Translator.scala | 274 ++++++++++-------- .../PredicateInstancePlugin.scala | 2 +- .../all/annotation/expAnnotation.vpr | 20 ++ 7 files changed, 204 insertions(+), 129 deletions(-) create mode 100644 src/test/resources/all/annotation/expAnnotation.vpr diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala index e39b43fb3..13909ca1d 100644 --- a/src/main/scala/viper/silver/ast/Ast.scala +++ b/src/main/scala/viper/silver/ast/Ast.scala @@ -371,6 +371,11 @@ case object NoInfo extends Info { override val isCached = false } +case class AnnotationInfo(values: Map[String, String]) extends Info { + override val isCached = false + override val comment = Nil +} + /** A simple `Info` that contains a list of comments. */ case class SimpleInfo(comment: Seq[String]) extends Info { override val isCached = false diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 60e8b4322..041b2e259 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -794,7 +794,8 @@ class FastParser { // Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former // and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut) - def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | integer | booltrue | boolfalse | nul | old + def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | annotatedAtom + | integer | booltrue | boolfalse | nul | old | result | unExp | typedFapp | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying | setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty @@ -802,6 +803,14 @@ class FastParser { | mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange | fapp | idnuse | ParserExtension.newExpAtEnd(ctx)) + def stringLiteral[_: P]: P[String] = P("\"" ~ CharsWhile(_ != '\"').! ~ "\"") + + def annotation[_: P]: P[(String, String)] = P("@" ~~ ident ~ stringLiteral) + + def annotatedAtom[_: P]: P[PExp] = FP(annotation ~ atom).map{ + case (pos, (key, value, exp)) => PAnnotatedExp(exp, (key, value))(pos) + } + def result[_: P]: P[PResultLit] = FP(keyword("result")).map { case (pos, _) => PResultLit()(pos) } def unExp[_: P]: P[PUnExp] = FP(CharIn("\\-\\!").! ~ suffixExpr).map { case (pos, (a, b)) => PUnExp(a, b)(pos) } @@ -1094,11 +1103,16 @@ class FastParser { case (pos, (func, args, typeGiven)) => PCall(func, args, Some(typeGiven))(pos) } - def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | macroassign | fieldassign | localassign | fold | unfold | exhale | assertP | + def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | annotatedStmt | + macroassign | fieldassign | localassign | fold | unfold | exhale | assertP | inhale | assume | ifthnels | whle | varDecl | defineDecl | newstmt | methodCall | goto | lbl | packageWand | applyWand | macroref | block | quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx)) + def annotatedStmt(implicit ctx : P[_]): P[PStmt] = (FP(annotation ~ stmt).map{ + case (pos, (key, value, pStmt)) => PAnnotatedStmt(pStmt, (key, value))(pos) + }) + def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fieldassign | localassign | fold | unfold | exhale | assertP | inhale | assume | ifthnels | whle | varDecl | newstmt | methodCall | goto | lbl | packageWand | applyWand | macroref | block | diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 2f9ff1555..2a54d12e0 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -357,6 +357,11 @@ trait PExp extends PNode { def forceSubstitution(ts: PTypeSubstitution): Unit } +case class PAnnotatedExp(e: PExp, annotation: (String, String))(val pos: (Position, Position)) extends PExp { + override def typeSubstitutions: collection.Seq[PTypeSubstitution] = e.typeSubstitutions + override def forceSubstitution(ts: PTypeSubstitution): Unit = e.forceSubstitution(ts) +} + case class PMagicWandExp(override val left: PExp, override val right: PExp)(val posi: (Position, Position)) extends PBinExp(left, MagicWandOp.op, right)(posi) with PResourceAccess class PTypeSubstitution(val m:Map[String,PType]) //extends Map[String,PType]() @@ -1050,6 +1055,8 @@ trait PStmt extends PNode { } } } + +case class PAnnotatedStmt(stmt: PStmt, annotation: (String, String))(val pos: (Position, Position)) extends PStmt case class PSeqn(ss: Seq[PStmt])(val pos: (Position, Position)) extends PStmt with PScope case class PFold(e: PExp)(val pos: (Position, Position)) extends PStmt case class PUnfold(e: PExp)(val pos: (Position, Position)) extends PStmt @@ -1330,6 +1337,8 @@ object Nodes { case PDefine(idndef, optArgs, body) => Seq(idndef) ++ optArgs.getOrElse(Nil) ++ Seq(body) case PQuasihavoc(lhs, e) => lhs.toSeq :+ e case PQuasihavocall(vars, lhs, e) => vars ++ lhs.toSeq :+ e + case PAnnotatedExp(e, _) => Seq(e) + case PAnnotatedStmt(s, _) => Seq(s) case t : PExtender => t.getSubnodes() case _: PSkip => Nil case _: PUnnamedFormalArgDecl => Nil diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index 69ad103b8..a50d06811 100644 --- a/src/main/scala/viper/silver/parser/Resolver.scala +++ b/src/main/scala/viper/silver/parser/Resolver.scala @@ -169,6 +169,8 @@ case class TypeChecker(names: NameAnalyser) { def check(stmt: PStmt): Unit = { stmt match { + case PAnnotatedStmt(s, _) => + check(s) case PMacroRef(id) => messages ++= FastMessaging.message(stmt, "unknown macro used: " + id.name ) case s@PSeqn(ss) => @@ -600,6 +602,9 @@ case class TypeChecker(names: NameAnalyser) { case t: PExtender => t.typecheck(this, names).getOrElse(Nil) foreach(message => messages ++= FastMessaging.message(t, message)) + case PAnnotatedExp(e, _) => + checkInternal(e) + setType(e.typ) case psl:PSimpleLiteral=> psl match { case r@PResultLit() => diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 019b59404..f68f18a26 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -176,21 +176,24 @@ case class Translator(program: PProgram) { private def findMethod(id: PIdentifier) = members(id.name).asInstanceOf[Method] /** Takes a `PStmt` and turns it into a `Stmt`. */ - def stmt(s: PStmt): Stmt = { - val pos = s + def stmt(pStmt: PStmt): Stmt = { + val pos = pStmt + val (s, annotations) = extractAnnotationFromStmt(pStmt) + val info = if (annotations.isEmpty) NoInfo else AnnotationInfo(annotations) s match { case p@PVarAssign(idnuse, PCall(func, args, _)) if members(func.name).isInstanceOf[Method] => /* This is a method call that got parsed in a slightly confusing way. * TODO: Get rid of this case! There is a matching case in the resolver. */ val call = PMethodCall(Seq(idnuse), func, args)(p.pos) - stmt(call) + val res = stmt(call) + res.withMeta(res.pos, info, res.errT) case PVarAssign(idnuse, rhs) => - LocalVarAssign(LocalVar(idnuse.name, ttyp(idnuse.typ))(pos), exp(rhs))(pos) + LocalVarAssign(LocalVar(idnuse.name, ttyp(idnuse.typ))(pos, info), exp(rhs))(pos, info) case PFieldAssign(field, rhs) => - FieldAssign(FieldAccess(exp(field.rcv), findField(field.idnuse))(field), exp(rhs))(pos) + FieldAssign(FieldAccess(exp(field.rcv), findField(field.idnuse))(field), exp(rhs))(pos, info) case PLocalVarDecl(idndef, t, Some(init)) => - LocalVarAssign(LocalVar(idndef.name, ttyp(t))(pos), exp(init))(pos) + LocalVarAssign(LocalVar(idndef.name, ttyp(t))(pos, info), exp(init))(pos, info) case PLocalVarDecl(_, _, None) => // there are no declarations in the Viper AST; rather they are part of the scope signature Statements.EmptyStmt @@ -202,24 +205,24 @@ case class Translator(program: PProgram) { val locals = plocals.flatten.map { case p@PLocalVarDecl(idndef, t, _) => LocalVarDecl(idndef.name, ttyp(t))(p) } - Seqn(ss filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos) + Seqn(ss filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info) case PFold(e) => - Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos) + Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info) case PUnfold(e) => - Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos) + Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info) case PPackageWand(e, proofScript) => val wand = exp(e).asInstanceOf[MagicWand] - Package(wand, stmt(proofScript).asInstanceOf[Seqn])(pos) + Package(wand, stmt(proofScript).asInstanceOf[Seqn])(pos, info) case PApplyWand(e) => - Apply(exp(e).asInstanceOf[MagicWand])(pos) + Apply(exp(e).asInstanceOf[MagicWand])(pos, info) case PInhale(e) => - Inhale(exp(e))(pos) + Inhale(exp(e))(pos, info) case PAssume(e) => - Assume(exp(e))(pos) + Assume(exp(e))(pos, info) case PExhale(e) => - Exhale(exp(e))(pos) + Exhale(exp(e))(pos, info) case PAssert(e) => - Assert(exp(e))(pos) + Assert(exp(e))(pos, info) case PNewStmt(target, fieldsOpt) => val fields = fieldsOpt match { case None => program.fields map translate @@ -228,25 +231,25 @@ case class Translator(program: PProgram) { */ case Some(pfields) => pfields map findField } - NewStmt(exp(target).asInstanceOf[LocalVar], fields)(pos) + NewStmt(exp(target).asInstanceOf[LocalVar], fields)(pos, info) case PMethodCall(targets, method, args) => val ts = (targets map exp).asInstanceOf[Seq[LocalVar]] - MethodCall(findMethod(method), args map exp, ts)(pos) + MethodCall(findMethod(method), args map exp, ts)(pos, info) case PLabel(name, invs) => - Label(name.name, invs map exp)(pos) + Label(name.name, invs map exp)(pos, info) case PGoto(label) => - Goto(label.name)(pos) + Goto(label.name)(pos, info) case PIf(cond, thn, els) => - If(exp(cond), stmt(thn).asInstanceOf[Seqn], stmt(els).asInstanceOf[Seqn])(pos) + If(exp(cond), stmt(thn).asInstanceOf[Seqn], stmt(els).asInstanceOf[Seqn])(pos, info) case PWhile(cond, invs, body) => - While(exp(cond), invs map exp, stmt(body).asInstanceOf[Seqn])(pos) + While(exp(cond), invs map exp, stmt(body).asInstanceOf[Seqn])(pos, info) case PQuasihavoc(lhs, e) => val (newLhs, newE) = havocStmtHelper(lhs, e) - Quasihavoc(newLhs, newE)(pos) + Quasihavoc(newLhs, newE)(pos, info) case PQuasihavocall(vars, lhs, e) => val newVars = vars map liftVarDecl val (newLhs, newE) = havocStmtHelper(lhs, e) - Quasihavocall(newVars, newLhs, newE)(pos) + Quasihavocall(newVars, newLhs, newE)(pos, info) case t: PExtender => t.translateStmt(this) case _: PDefine | _: PSkip => sys.error(s"Found unexpected intermediate statement $s (${s.getClass.getName}})") @@ -269,18 +272,37 @@ case class Translator(program: PProgram) { } } - /** Takes a `PExp` and turns it into an `Exp`. */ - def exp(pexp: PExp): Exp = { - val pos = pexp + def extractAnnotation(pexp: PExp): (PExp, Map[String, String]) = { pexp match { + case PAnnotatedExp(e, (key, value)) => + val (resPexp, innerMap) = extractAnnotation(e) + (resPexp, innerMap.updated(key, value)) + case _ => (pexp, Map()) + } + } + + def extractAnnotationFromStmt(pStmt: PStmt): (PStmt, Map[String, String]) = { + pStmt match { + case PAnnotatedStmt(s, (key, value)) => + val (resPStmt, innerMap) = extractAnnotationFromStmt(s) + (resPStmt, innerMap.updated(key, value)) + case _ => (pStmt, Map()) + } + } + /** Takes a `PExp` and turns it into an `Exp`. */ + def exp(parseExp: PExp): Exp = { + val pos = parseExp + val (pexp, annotationMap) = extractAnnotation(parseExp) + val info = if (annotationMap.isEmpty) NoInfo else AnnotationInfo(annotationMap) + pexp match { case piu @ PIdnUse(name) => piu.decl match { - case _: PLocalVarDecl | _: PFormalArgDecl => LocalVar(name, ttyp(pexp.typ))(pos) + case _: PLocalVarDecl | _: PFormalArgDecl => LocalVar(name, ttyp(pexp.typ))(pos, info) case pf: PField => /* A malformed AST where a field is dereferenced without a receiver */ Consistency.messages ++= FastMessaging.message(piu, s"expected expression but found field $name") - LocalVar(pf.idndef.name, ttyp(pf.typ))(pos) + LocalVar(pf.idndef.name, ttyp(pf.typ))(pos, info) case _ => sys.error("should not occur in type-checked program") } @@ -289,28 +311,28 @@ case class Translator(program: PProgram) { op match { case "+" => r.typ match { - case Int => Add(l, r)(pos) - case Perm => PermAdd(l, r)(pos) + case Int => Add(l, r)(pos, info) + case Perm => PermAdd(l, r)(pos, info) case _ => sys.error("should not occur in type-checked program") } case "-" => r.typ match { - case Int => Sub(l, r)(pos) - case Perm => PermSub(l, r)(pos) + case Int => Sub(l, r)(pos, info) + case Perm => PermSub(l, r)(pos, info) case _ => sys.error("should not occur in type-checked program") } case "*" => r.typ match { case Int => l.typ match { - case Int => Mul(l, r)(pos) - case Perm => IntPermMul(r, l)(pos) + case Int => Mul(l, r)(pos, info) + case Perm => IntPermMul(r, l)(pos, info) case _ => sys.error("should not occur in type-checked program") } case Perm => l.typ match { - case Int => IntPermMul(l, r)(pos) - case Perm => PermMul(l, r)(pos) + case Int => IntPermMul(l, r)(pos, info) + case Perm => PermMul(l, r)(pos, info) case _ => sys.error("should not occur in type-checked program") } case _ => sys.error("should not occur in type-checked program") @@ -318,63 +340,63 @@ case class Translator(program: PProgram) { case "/" => l.typ match { case Perm => r.typ match { - case Int => PermDiv(l, r)(pos) - case Perm => PermPermDiv(l, r)(pos) + case Int => PermDiv(l, r)(pos, info) + case Perm => PermPermDiv(l, r)(pos, info) } case Int => assert (r.typ==Int) if (ttyp(pbe.typ) == Int) - Div(l, r)(pos) + Div(l, r)(pos, info) else - FractionalPerm(l, r)(pos) + FractionalPerm(l, r)(pos, info) case _ => sys.error("should not occur in type-checked program") } - case "\\" => Div(l, r)(pos) - case "%" => Mod(l, r)(pos) + case "\\" => Div(l, r)(pos, info) + case "%" => Mod(l, r)(pos, info) case "<" => l.typ match { - case Int => LtCmp(l, r)(pos) - case Perm => PermLtCmp(l, r)(pos) + case Int => LtCmp(l, r)(pos, info) + case Perm => PermLtCmp(l, r)(pos, info) case _ => sys.error("unexpected type") } case "<=" => l.typ match { - case Int => LeCmp(l, r)(pos) - case Perm => PermLeCmp(l, r)(pos) + case Int => LeCmp(l, r)(pos, info) + case Perm => PermLeCmp(l, r)(pos, info) case _ => sys.error("unexpected type") } case ">" => l.typ match { - case Int => GtCmp(l, r)(pos) - case Perm => PermGtCmp(l, r)(pos) + case Int => GtCmp(l, r)(pos, info) + case Perm => PermGtCmp(l, r)(pos, info) case _ => sys.error("unexpected type") } case ">=" => l.typ match { - case Int => GeCmp(l, r)(pos) - case Perm => PermGeCmp(l, r)(pos) + case Int => GeCmp(l, r)(pos, info) + case Perm => PermGeCmp(l, r)(pos, info) case _ => sys.error("unexpected type") } - case "==" => EqCmp(l, r)(pos) - case "!=" => NeCmp(l, r)(pos) - case "==>" => Implies(l, r)(pos) - case "--*" => MagicWand(l, r)(pos) - case "<==>" => EqCmp(l, r)(pos) - case "&&" => And(l, r)(pos) - case "||" => Or(l, r)(pos) + case "==" => EqCmp(l, r)(pos, info) + case "!=" => NeCmp(l, r)(pos, info) + case "==>" => Implies(l, r)(pos, info) + case "--*" => MagicWand(l, r)(pos, info) + case "<==>" => EqCmp(l, r)(pos, info) + case "&&" => And(l, r)(pos, info) + case "||" => Or(l, r)(pos, info) case "in" => right.typ match { - case _: PSeqType => SeqContains(l, r)(pos) - case _: PMapType => MapContains(l, r)(pos) - case _: PSetType | _: PMultisetType => AnySetContains(l, r)(pos) + case _: PSeqType => SeqContains(l, r)(pos, info) + case _: PMapType => MapContains(l, r)(pos, info) + case _: PSetType | _: PMultisetType => AnySetContains(l, r)(pos, info) case t => sys.error(s"unexpected type $t") } - case "++" => SeqAppend(l, r)(pos) - case "subset" => AnySetSubset(l, r)(pos) - case "intersection" => AnySetIntersection(l, r)(pos) - case "union" => AnySetUnion(l, r)(pos) - case "setminus" => AnySetMinus(l, r)(pos) + case "++" => SeqAppend(l, r)(pos, info) + case "subset" => AnySetSubset(l, r)(pos, info) + case "intersection" => AnySetIntersection(l, r)(pos, info) + case "union" => AnySetUnion(l, r)(pos, info) + case "setminus" => AnySetMinus(l, r)(pos, info) case _ => sys.error(s"unexpected operator $op") } case PUnExp(op, pe) => @@ -382,16 +404,16 @@ case class Translator(program: PProgram) { op match { case "-" => e.typ match { - case Int => Minus(e)(pos) - case Perm => PermMinus(e)(pos) + case Int => Minus(e)(pos, info) + case Perm => PermMinus(e)(pos, info) case _ => sys.error("unexpected type") } - case "!" => Not(e)(pos) + case "!" => Not(e)(pos, info) } case PInhaleExhaleExp(in, ex) => - InhaleExhaleExp(exp(in), exp(ex))(pos) + InhaleExhaleExp(exp(in), exp(ex))(pos, info) case PIntLit(i) => - IntLit(i)(pos) + IntLit(i)(pos, info) case p@PResultLit() => // find function var par: PNode = p.parent.get @@ -399,19 +421,19 @@ case class Translator(program: PProgram) { if (par == null) sys.error("cannot use 'result' outside of function") par = par.parent.get } - Result(ttyp(par.asInstanceOf[PFunction].typ))(pos) + Result(ttyp(par.asInstanceOf[PFunction].typ))(pos, info) case PBoolLit(b) => - if (b) TrueLit()(pos) else FalseLit()(pos) + if (b) TrueLit()(pos, info) else FalseLit()(pos, info) case PNullLit() => - NullLit()(pos) + NullLit()(pos, info) case PFieldAccess(rcv, idn) => - FieldAccess(exp(rcv), findField(idn))(pos) + FieldAccess(exp(rcv), findField(idn))(pos, info) case PPredicateAccess(args, idn) => - PredicateAccess(args map exp, findPredicate(idn).name)(pos) - case PMagicWandExp(left, right) => MagicWand(exp(left), exp(right))(pos) + PredicateAccess(args map exp, findPredicate(idn).name)(pos, info) + case PMagicWandExp(left, right) => MagicWand(exp(left), exp(right))(pos, info) case pfa@PCall(func, args, _) => members(func.name) match { - case f: Function => FuncApp(f, args map exp)(pos) + case f: Function => FuncApp(f, args map exp)(pos, info) case f @ DomainFunc(_, _, _, _, _) => val actualArgs = args map exp /* TODO: Not used - problem?*/ @@ -427,23 +449,23 @@ case class Translator(program: PProgram) { val sp = s //completeWithDefault(d.typVars,s) assert(sp.keys.toSet == d.typVars.toSet) if (f.interpretation.isDefined) - BackendFuncApp(f, actualArgs)(pos) + BackendFuncApp(f, actualArgs)(pos, info) else - DomainFuncApp(f, actualArgs, sp)(pos) + DomainFuncApp(f, actualArgs, sp)(pos, info) case _ => sys.error("type unification error - should report and not crash") } case _: Predicate => - val inner = PredicateAccess(args map exp, findPredicate(func).name) (pos) - val fullPerm = FullPerm()(pos) - PredicateAccessPredicate(inner, fullPerm) (pos) + val inner = PredicateAccess(args map exp, findPredicate(func).name) (pos, info) + val fullPerm = FullPerm()(pos, info) + PredicateAccessPredicate(inner, fullPerm) (pos, info) case _ => sys.error("unexpected reference to non-function") } case PUnfolding(loc, e) => - Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos) + Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info) case PApplying(wand, e) => - Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos) + Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info) case PLet(exp1, PLetNestedScope(variable, body)) => - Let(liftVarDecl(variable), exp(exp1), exp(body))(pos) + Let(liftVarDecl(variable), exp(exp1), exp(body))(pos, info) case _: PLetNestedScope => sys.error("unexpected node PLetNestedScope, should only occur as a direct child of PLet nodes") case PExists(vars, triggers, e) => @@ -451,13 +473,13 @@ case class Translator(program: PProgram) { case PredicateAccessPredicate(inner, _) => inner case _ => e }))(t)) - Exists(vars map liftVarDecl, ts, exp(e))(pos) + Exists(vars map liftVarDecl, ts, exp(e))(pos, info) case PForall(vars, triggers, e) => val ts = triggers map (t => Trigger((t.exp map exp) map (e => e match { case PredicateAccessPredicate(inner, _) => inner case _ => e }))(t)) - val fa = Forall(vars map liftVarDecl, ts, exp(e))(pos) + val fa = Forall(vars map liftVarDecl, ts, exp(e))(pos, info) if (fa.isPure) { fa } else { @@ -468,98 +490,98 @@ case class Translator(program: PProgram) { case PForPerm(vars, res, e) => val varList = vars map liftVarDecl exp(res) match { - case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, exp(e))(pos) - case f : FieldAccess => ForPerm(varList, f, exp(e))(pos) - case p : PredicateAccess => ForPerm(varList, p, exp(e))(pos) - case w : MagicWand => ForPerm(varList, w, exp(e))(pos) + case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, exp(e))(pos, info) + case f : FieldAccess => ForPerm(varList, f, exp(e))(pos, info) + case p : PredicateAccess => ForPerm(varList, p, exp(e))(pos, info) + case w : MagicWand => ForPerm(varList, w, exp(e))(pos, info) case other => sys.error(s"Internal Error: Unexpectedly found $other in forperm") } case POld(e) => - Old(exp(e))(pos) + Old(exp(e))(pos, info) case PLabelledOld(lbl,e) => - LabelledOld(exp(e),lbl.name)(pos) + LabelledOld(exp(e),lbl.name)(pos, info) case PCondExp(cond, thn, els) => - CondExp(exp(cond), exp(thn), exp(els))(pos) + CondExp(exp(cond), exp(thn), exp(els))(pos, info) case PCurPerm(res) => exp(res) match { - case PredicateAccessPredicate(inner, _) => CurrentPerm(inner)(pos) - case x: FieldAccess => CurrentPerm(x)(pos) - case x: PredicateAccess => CurrentPerm(x)(pos) - case x: MagicWand => CurrentPerm(x)(pos) + case PredicateAccessPredicate(inner, _) => CurrentPerm(inner)(pos, info) + case x: FieldAccess => CurrentPerm(x)(pos, info) + case x: PredicateAccess => CurrentPerm(x)(pos, info) + case x: MagicWand => CurrentPerm(x)(pos, info) case other => sys.error(s"Unexpectedly found $other") } case PNoPerm() => - NoPerm()(pos) + NoPerm()(pos, info) case PFullPerm() => - FullPerm()(pos) + FullPerm()(pos, info) case PWildcard() => - WildcardPerm()(pos) + WildcardPerm()(pos, info) case PEpsilon() => - EpsilonPerm()(pos) + EpsilonPerm()(pos, info) case PAccPred(loc, perm) => val p = exp(perm) exp(loc) match { case loc@FieldAccess(_, _) => - FieldAccessPredicate(loc, p)(pos) + FieldAccessPredicate(loc, p)(pos, info) case loc@PredicateAccess(_, _) => - PredicateAccessPredicate(loc, p)(pos) - case PredicateAccessPredicate(inner, _) => PredicateAccessPredicate(inner, p)(pos) + PredicateAccessPredicate(loc, p)(pos, info) + case PredicateAccessPredicate(inner, _) => PredicateAccessPredicate(inner, p)(pos, info) case _ => sys.error("unexpected location") } case PEmptySeq(_) => - EmptySeq(ttyp(pexp.typ.asInstanceOf[PSeqType].elementType))(pos) + EmptySeq(ttyp(pexp.typ.asInstanceOf[PSeqType].elementType))(pos, info) case PExplicitSeq(elems) => - ExplicitSeq(elems map exp)(pos) + ExplicitSeq(elems map exp)(pos, info) case PRangeSeq(low, high) => - RangeSeq(exp(low), exp(high))(pos) + RangeSeq(exp(low), exp(high))(pos, info) case PLookup(base, index) => base.typ match { - case _: PSeqType => SeqIndex(exp(base), exp(index))(pos) - case _: PMapType => MapLookup(exp(base), exp(index))(pos) + case _: PSeqType => SeqIndex(exp(base), exp(index))(pos, info) + case _: PMapType => MapLookup(exp(base), exp(index))(pos, info) case t => sys.error(s"unexpected type $t") } case PSeqTake(seq, n) => - SeqTake(exp(seq), exp(n))(pos) + SeqTake(exp(seq), exp(n))(pos, info) case PSeqDrop(seq, n) => - SeqDrop(exp(seq), exp(n))(pos) + SeqDrop(exp(seq), exp(n))(pos, info) case PUpdate(base, key, value) => base.typ match { - case _: PSeqType => SeqUpdate(exp(base), exp(key), exp(value))(pos) - case _: PMapType => MapUpdate(exp(base), exp(key), exp(value))(pos) + case _: PSeqType => SeqUpdate(exp(base), exp(key), exp(value))(pos, info) + case _: PMapType => MapUpdate(exp(base), exp(key), exp(value))(pos, info) case t => sys.error(s"unexpected type $t") } case PSize(base) => base.typ match { - case _: PSeqType => SeqLength(exp(base))(pos) - case _: PMapType => MapCardinality(exp(base))(pos) - case _: PSetType | _: PMultisetType => AnySetCardinality(exp(base))(pos) + case _: PSeqType => SeqLength(exp(base))(pos, info) + case _: PMapType => MapCardinality(exp(base))(pos, info) + case _: PSetType | _: PMultisetType => AnySetCardinality(exp(base))(pos, info) case t => sys.error(s"unexpected type $t") } case PEmptySet(_) => - EmptySet(ttyp(pexp.typ.asInstanceOf[PSetType].elementType))(pos) + EmptySet(ttyp(pexp.typ.asInstanceOf[PSetType].elementType))(pos, info) case PExplicitSet(elems) => - ExplicitSet(elems map exp)(pos) + ExplicitSet(elems map exp)(pos, info) case PEmptyMultiset(_) => - EmptyMultiset(ttyp(pexp.typ.asInstanceOf[PMultisetType].elementType))(pos) + EmptyMultiset(ttyp(pexp.typ.asInstanceOf[PMultisetType].elementType))(pos, info) case PExplicitMultiset(elems) => - ExplicitMultiset(elems map exp)(pos) + ExplicitMultiset(elems map exp)(pos, info) case PEmptyMap(_, _) => EmptyMap( ttyp(pexp.typ.asInstanceOf[PMapType].keyType), ttyp(pexp.typ.asInstanceOf[PMapType].valueType) - )(pos) + )(pos, info) case PExplicitMap(elems) => - ExplicitMap(elems map exp)(pos) + ExplicitMap(elems map exp)(pos, info) case PMaplet(key, value) => - Maplet(exp(key), exp(value))(pos) + Maplet(exp(key), exp(value))(pos, info) case PMapDomain(base) => - MapDomain(exp(base))(pos) + MapDomain(exp(base))(pos, info) case PMapRange(base) => - MapRange(exp(base))(pos) + MapRange(exp(base))(pos, info) case t: PExtender => t.translateExp(this) } diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala index a8e8cc6ef..7c91b3fce 100644 --- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala @@ -30,7 +30,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter, /** * Syntactic marker for predicate instances */ - val PredicateInstanceMarker: String = "@" + val PredicateInstanceMarker: String = "#" val PredicateInstanceDomainName = "PredicateInstance" diff --git a/src/test/resources/all/annotation/expAnnotation.vpr b/src/test/resources/all/annotation/expAnnotation.vpr new file mode 100644 index 000000000..e7feca661 --- /dev/null +++ b/src/test/resources/all/annotation/expAnnotation.vpr @@ -0,0 +1,20 @@ +field f: Int + + +function fun01(x: Ref, y: Ref, b: Bool): Int + requires b ? acc(x.f) : acc(y.f) + +function fun02(x: Ref, y: Ref, b: Bool): Int + requires acc(x.f, b ? write : none) + requires acc(y.f, !b ? write : none) + + +method m(x: Ref, y: Ref) + requires acc(x.f) + requires acc(y.f) +{ + var tmp: Int + tmp := @asd "test 123" fun02(x, @lul "this is ugly" y, true) + y.f := 1 + assert tmp == fun02(x, y, true) +} \ No newline at end of file From 965e40f22435f0b855c3a2355cca6295e6155901 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 00:33:38 +0200 Subject: [PATCH 2/9] Annotations for members --- .../viper/silver/parser/FastParser.scala | 45 ++++++++++--------- .../scala/viper/silver/parser/ParseAst.scala | 33 ++++++++------ .../viper/silver/parser/Transformer.scala | 14 +++--- .../all/annotation/expAnnotation.vpr | 22 ++++++++- 4 files changed, 71 insertions(+), 43 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 041b2e259..9b768e464 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -510,7 +510,7 @@ class FastParser { } if (body != method.body) { - PMethod(method.idndef, method.formalArgs, method.formalReturns, method.pres, method.posts, body)(method.pos) + PMethod(method.idndef, method.formalArgs, method.formalReturns, method.pres, method.posts, body)(method.pos, method.annotations) } else { method } @@ -1224,7 +1224,8 @@ class FastParser { def applying[_: P]: P[PExp] = FP(keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PApplying(a, b)(pos) } - def programDecl(implicit ctx : P[_]) : P[PProgram] = P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map { + def programDecl(implicit ctx : P[_]) : P[PProgram] = + P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | fieldDecl | methodDecl | domainDecl | functionDecl | predicateDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map { case (pos, decls) => { PProgram( decls.collect { case i: PImport => i }, // Imports @@ -1249,24 +1250,24 @@ class FastParser { def anyString[_: P]: P[String] = P(CharIn("A-Z", "a-z", "0-9", "()._ ").rep(1).!) - def domainDecl[_: P]: P[PDomain] = FP("domain" ~/ idndef ~ ("[" ~ domainTypeVarDecl.rep(sep = ",") ~ "]").? ~ ("interpretation" ~ parens((ident ~ ":" ~ quoted(anyString.!)).rep(sep = ","))).? ~ "{" ~ (domainFunctionDecl | axiomDecl).rep ~ + def domainDecl[_: P]: P[PDomain] = FP(annotation.rep(0) ~ "domain" ~/ idndef ~ ("[" ~ domainTypeVarDecl.rep(sep = ",") ~ "]").? ~ ("interpretation" ~ parens((ident ~ ":" ~ quoted(anyString.!)).rep(sep = ","))).? ~ "{" ~ (domainFunctionDecl | axiomDecl).rep ~ "}").map { - case (pos, (name, typparams, interpretations, members)) => + case (pos, (anns, name, typparams, interpretations, members)) => val funcs = members collect { case m: PDomainFunction1 => m } val axioms = members collect { case m: PAxiom1 => m } PDomain( name, typparams.getOrElse(Nil), - funcs map (f => PDomainFunction(f.idndef, f.formalArgs, f.typ, f.unique, f.interpretation)(PIdnUse(name.name)(name.pos))(f.pos)), - axioms map (a => PAxiom(a.idndef, a.exp)(PIdnUse(name.name)(name.pos))(a.pos)), - interpretations.map(i => i.toMap))(pos) + funcs map (f => PDomainFunction(f.idndef, f.formalArgs, f.typ, f.unique, f.interpretation)(PIdnUse(name.name)(name.pos))(f.pos, f.annotations)), + axioms map (a => PAxiom(a.idndef, a.exp)(PIdnUse(name.name)(name.pos))(a.pos, a.annotations)), + interpretations.map(i => i.toMap))(pos, anns) } def domainTypeVarDecl[_: P]: P[PTypeVarDecl] = FP(idndef).map{ case (pos, i) => PTypeVarDecl(i)(pos) } - def domainFunctionDecl[_: P]: P[PDomainFunction1] = FP("unique".!.? ~ domainFunctionSignature ~ ("interpretation" ~ quoted(anyString.!)).? ~~~ ";".lw.?).map { - case (pos, (unique, fdecl, interpretation)) => fdecl match { - case (name, formalArgs, t) => PDomainFunction1(name, formalArgs, t, unique.isDefined, interpretation)(pos) + def domainFunctionDecl[_: P]: P[PDomainFunction1] = FP(annotation.rep(0) ~ "unique".!.? ~ domainFunctionSignature ~ ("interpretation" ~ quoted(anyString.!)).? ~~~ ";".lw.?).map { + case (pos, (anns, unique, fdecl, interpretation)) => fdecl match { + case (name, formalArgs, t) => PDomainFunction1(name, formalArgs, t, unique.isDefined, interpretation)(pos, anns) } } @@ -1280,15 +1281,15 @@ class FastParser { def formalArgList[_: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ",")) - def axiomDecl[_: P]: P[PAxiom1] = FP(keyword("axiom") ~ idndef.? ~ "{" ~ exp ~ "}" ~~~ ";".lw.?).map { case (pos, (a, b)) => PAxiom1(a, b)(pos) } + def axiomDecl[_: P]: P[PAxiom1] = FP(annotation.rep(0) ~ keyword("axiom") ~ idndef.? ~ "{" ~ exp ~ "}" ~~~ ";".lw.?).map { case (pos, (anns, a, b)) => PAxiom1(a, b)(pos, anns) } - def fieldDecl[_: P]: P[PField] = FP(keyword("field") ~/ idndef ~ ":" ~ typ ~~~ ";".lw.?).map { - case (pos, (a, b)) => PField(a, b)(pos) + def fieldDecl[_: P]: P[PField] = FP(annotation.rep(0) ~ keyword("field") ~/ idndef ~ ":" ~ typ ~~~ ";".lw.?).map { + case (pos, (anns, a, b)) => PField(a, b)(pos, anns) } - def functionDecl[_: P]: P[PFunction] = FP("function" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~ ":" ~ typ ~~~ pre.lw.rep ~~~ - post.lw.rep ~~~ ("{" ~ exp ~ "}").lw.?).map({ case (pos, (a, b, c, d, e, f)) => - PFunction(a, b, c, d, e, f)(pos) + def functionDecl[_: P]: P[PFunction] = FP(annotation.rep(0) ~ "function" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~ ":" ~ typ ~~~ pre.lw.rep ~~~ + post.lw.rep ~~~ ("{" ~ exp ~ "}").lw.?).map({ case (pos, (anns, a, b, c, d, e, f)) => + PFunction(a, b, c, d, e, f)(pos, anns) }) @@ -1298,14 +1299,14 @@ class FastParser { def decCl[_: P]: P[Seq[PExp]] = P(exp.rep(sep = ",")) - def predicateDecl[_: P]: P[PPredicate] = FP(keyword("predicate") ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("{" ~ exp ~ "}").lw.?).map { - case (pos, (a, b, c)) => - PPredicate(a, b, c)(pos) + def predicateDecl[_: P]: P[PPredicate] = FP(annotation.rep(0) ~ keyword("predicate") ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("{" ~ exp ~ "}").lw.?).map { + case (pos, (anns, a, b, c)) => + PPredicate(a, b, c)(pos, anns) } - def methodDecl[_: P]: P[PMethod] = FP(methodSignature ~~~/ pre.lw.rep ~~~ post.lw.rep ~~~ block.lw.?).map { - case (pos, (name, args, rets, pres, posts, body)) => - PMethod(name, args, rets.getOrElse(Nil), pres, posts, body)(pos) + def methodDecl[_: P]: P[PMethod] = FP(annotation.rep(0) ~ methodSignature ~~~/ pre.lw.rep ~~~ post.lw.rep ~~~ block.lw.?).map { + case (pos, (anns, (name, args, rets), pres, posts, body)) => + PMethod(name, args, rets.getOrElse(Nil), pres, posts, body)(pos, anns) } def methodSignature[_: P] = P("method" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("returns" ~ "(" ~ formalArgList ~ ")").lw.?) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 2a54d12e0..9338affdf 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -1149,7 +1149,9 @@ abstract class PErrorEntity extends PEntity { // a member (like method or axiom) that is its own name scope -trait PMember extends PDeclaration with PScope +trait PMember extends PDeclaration with PScope { + +} trait PAnyFunction extends PMember with PGlobalDeclaration with PTypedDeclaration{ def idndef: PIdnDef @@ -1161,39 +1163,44 @@ abstract class PImport() extends PNode case class PLocalImport(file: String)(val pos: (Position, Position)) extends PImport() case class PStandardImport(file: String)(val pos: (Position, Position)) extends PImport() -case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalArgDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt])(val pos: (Position, Position)) extends PMember with PGlobalDeclaration { +case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalArgDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt]) + (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PGlobalDeclaration { def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, formalReturns: Seq[PFormalArgDecl] = this.formalReturns, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PStmt] = this.body): PMethod = { StrategyBuilder.Slim[PNode]({ - case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos) + case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos, p.annotations) }).execute[PMethod](this) } def deepCopyWithNameSubstitution(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, formalReturns: Seq[PFormalArgDecl] = this.formalReturns, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PStmt] = this.body) (idn_generic_name: String, idn_substitution: String): PMethod = { StrategyBuilder.Slim[PNode]({ - case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos) + case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos, p.annotations) case p@PIdnDef(name) if name == idn_generic_name => PIdnDef(idn_substitution)(p.pos) case p@PIdnUse(name) if name == idn_generic_name => PIdnUse(idn_substitution)(p.pos) }).execute[PMethod](this) } } -case class PDomain(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], funcs: Seq[PDomainFunction], axioms: Seq[PAxiom], interpretations: Option[Map[String, String]])(val pos: (Position, Position)) extends PMember with PGlobalDeclaration -case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PType, pres: Seq[PExp], posts: Seq[PExp], body: Option[PExp])(val pos: (Position, Position)) extends PAnyFunction { +case class PDomain(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], funcs: Seq[PDomainFunction], axioms: Seq[PAxiom], interpretations: Option[Map[String, String]]) + (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PGlobalDeclaration +case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PType, pres: Seq[PExp], posts: Seq[PExp], body: Option[PExp]) + (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PAnyFunction { def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, typ: PType = this.typ, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PExp] = this.body): PFunction = { StrategyBuilder.Slim[PNode]({ - case p: PFunction => PFunction(idndef, formalArgs, typ, pres, posts, body)(p.pos) + case p: PFunction => PFunction(idndef, formalArgs, typ, pres, posts, body)(p.pos, p.annotations) }).execute[PFunction](this) } } -case class PDomainFunction(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val domainName:PIdnUse)(val pos: (Position, Position)) extends PAnyFunction -case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName:PIdnUse)(val pos: (Position, Position)) extends PScope -case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position)) extends PMember with PTypedDeclaration with PGlobalDeclaration -case class PPredicate(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], body: Option[PExp])(val pos: (Position, Position)) extends PMember with PTypedDeclaration with PGlobalDeclaration{ +case class PDomainFunction(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String]) + (val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PAnyFunction +case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PScope +case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PTypedDeclaration with PGlobalDeclaration +case class PPredicate(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], body: Option[PExp]) + (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PTypedDeclaration with PGlobalDeclaration{ val typ = PPredicateType()() } -case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position)) -case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position)) +case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position), val annotations: Seq[(String, String)]) +case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position), val annotations: Seq[(String, String)]) /** * A entity represented by names for whom we have seen more than one diff --git a/src/main/scala/viper/silver/parser/Transformer.scala b/src/main/scala/viper/silver/parser/Transformer.scala index 0e9a1f003..9001d5190 100644 --- a/src/main/scala/viper/silver/parser/Transformer.scala +++ b/src/main/scala/viper/silver/parser/Transformer.scala @@ -148,13 +148,13 @@ object Transformer { case p@PProgram(files, macros, domains, fields, functions, predicates, methods, extensions, errors) => PProgram(files, macros map go, domains map go, fields map go, functions map go, predicates map go, methods map go, extensions map go, errors)(p.pos) case p@PLocalImport(file) => PLocalImport(file)(p.pos) case p@PStandardImport(file) => PStandardImport(file)(p.pos) - case p@PMethod(idndef, formalArgs, formalReturns, pres, posts, body) => PMethod(go(idndef), formalArgs map go, formalReturns map go, pres map go, posts map go, body map go)(p.pos) - case p@PDomain(idndef, typVars, funcs, axioms, interp) => PDomain(go(idndef), typVars map go, funcs map go, axioms map go, interp)(p.pos) - case p@PField(idndef, typ) => PField(go(idndef), go(typ))(p.pos) - case p@PFunction(idndef, formalArgs, typ, pres, posts, body) => PFunction(go(idndef), formalArgs map go, go(typ), pres map go, posts map go, body map go)(p.pos) - case pdf@PDomainFunction(idndef, formalArgs, typ, unique, interp) => PDomainFunction(go(idndef), formalArgs map go, go(typ), unique, interp)(domainName = pdf.domainName)(pdf.pos) - case p@PPredicate(idndef, formalArgs, body) => PPredicate(go(idndef), formalArgs map go, body map go)(p.pos) - case pda@PAxiom(idndef, exp) => PAxiom(idndef map go, go(exp))(domainName = pda.domainName)(pda.pos) + case p@PMethod(idndef, formalArgs, formalReturns, pres, posts, body) => PMethod(go(idndef), formalArgs map go, formalReturns map go, pres map go, posts map go, body map go)(p.pos, p.annotations) + case p@PDomain(idndef, typVars, funcs, axioms, interp) => PDomain(go(idndef), typVars map go, funcs map go, axioms map go, interp)(p.pos, p.annotations) + case p@PField(idndef, typ) => PField(go(idndef), go(typ))(p.pos, p.annotations) + case p@PFunction(idndef, formalArgs, typ, pres, posts, body) => PFunction(go(idndef), formalArgs map go, go(typ), pres map go, posts map go, body map go)(p.pos, p.annotations) + case pdf@PDomainFunction(idndef, formalArgs, typ, unique, interp) => PDomainFunction(go(idndef), formalArgs map go, go(typ), unique, interp)(domainName = pdf.domainName)(pdf.pos, pdf.annotations) + case p@PPredicate(idndef, formalArgs, body) => PPredicate(go(idndef), formalArgs map go, body map go)(p.pos, p.annotations) + case pda@PAxiom(idndef, exp) => PAxiom(idndef map go, go(exp))(domainName = pda.domainName)(pda.pos, pda.annotations) case pe:PExtender => pe.transformExtension(this) } diff --git a/src/test/resources/all/annotation/expAnnotation.vpr b/src/test/resources/all/annotation/expAnnotation.vpr index e7feca661..fee4953c0 100644 --- a/src/test/resources/all/annotation/expAnnotation.vpr +++ b/src/test/resources/all/annotation/expAnnotation.vpr @@ -1,6 +1,7 @@ +@isghost "nope" field f: Int - +@inlining "never" function fun01(x: Ref, y: Ref, b: Bool): Int requires b ? acc(x.f) : acc(y.f) @@ -8,12 +9,31 @@ function fun02(x: Ref, y: Ref, b: Bool): Int requires acc(x.f, b ? write : none) requires acc(y.f, !b ? write : none) +@inline "never" +predicate P(x: Ref) + +@interp "some smtlib thingy" +domain MyType { + + @asd "test 123" + @asdd "test 123" + function id(MyType): MyType + + @asd "test 123" + axiom { + @asd "test 123" + true + } +} +@setting "donotverify" +@verifier "none" method m(x: Ref, y: Ref) requires acc(x.f) requires acc(y.f) { var tmp: Int + @annotatingastatement "the assignment" tmp := @asd "test 123" fun02(x, @lul "this is ugly" y, true) y.f := 1 assert tmp == fun02(x, y, true) From 8537f62a8f45bf01015a549d0cdb0dc15af77233 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 01:25:25 +0200 Subject: [PATCH 3/9] Fixed test code --- src/test/scala/ASTTransformationTests.scala | 12 ++++++------ src/test/scala/PluginTests.scala | 2 +- src/test/scala/SemanticAnalysisTests.scala | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/test/scala/ASTTransformationTests.scala b/src/test/scala/ASTTransformationTests.scala index 954853e05..bfe0c7cd7 100644 --- a/src/test/scala/ASTTransformationTests.scala +++ b/src/test/scala/ASTTransformationTests.scala @@ -83,11 +83,11 @@ class ASTTransformationTests extends AnyFunSuite { val p = (NoPosition, NoPosition) val binExp1 = PBinExp(PIntLit(1)(p), "==", PIntLit(1)(p))(p) - val method1 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PAssert(binExp1)(p)))(p)))(p) + val method1 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PAssert(binExp1)(p)))(p)))(p, Seq()) val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method1), Seq(), Seq())(p) val binExp2 = PBinExp(PIntLit(3)(p), "==", PIntLit(3)(p))(p) - val method2 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PAssert(binExp2)(p)))(p)))(p) + val method2 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PAssert(binExp2)(p)))(p)))(p, Seq()) val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method2), Seq(), Seq())(p) case class Context(increment: Int) @@ -119,13 +119,13 @@ class ASTTransformationTests extends AnyFunSuite { import viper.silver.parser._ val p = (NoPosition, NoPosition) - val function = PFunction(PIdnDef("f")(p), Seq(PFormalArgDecl(PIdnDef("x")(p), TypeHelper.Int)(p), PFormalArgDecl(PIdnDef("y")(p), TypeHelper.Int)(p)), TypeHelper.Int, Seq(), Seq(), None)(p) + val function = PFunction(PIdnDef("f")(p), Seq(PFormalArgDecl(PIdnDef("x")(p), TypeHelper.Int)(p), PFormalArgDecl(PIdnDef("y")(p), TypeHelper.Int)(p)), TypeHelper.Int, Seq(), Seq(), None)(p, Seq()) val assume1 = PAssume(PBinExp(PCall(PIdnUse("f")(p), Seq(PIntLit(1)(p), PIntLit(1)(p)))(p), "==", PCall(PIdnUse("f")(p), Seq(PIntLit(1)(p), PCall(PIdnUse("f")(p), Seq(PIntLit(1)(p), PCall(PIdnUse("f")(p), Seq(PIntLit(1)(p), PIntLit(1)(p)))(p)))(p)))(p))(p))(p) - val method1 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(assume1))(p)))(p) + val method1 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(assume1))(p)))(p, Seq()) val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method1), Seq(), Seq())(p) val assume2 = PAssume(PBinExp(PCall(PIdnUse("f")(p), Seq(PIntLit(2)(p), PIntLit(1)(p)))(p), "==", PCall(PIdnUse("f")(p), Seq(PIntLit(2)(p), PCall(PIdnUse("f")(p), Seq(PIntLit(3)(p), PCall(PIdnUse("f")(p), Seq(PIntLit(4)(p), PIntLit(1)(p)))(p)))(p)))(p))(p))(p) - val method2 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(assume2))(p)))(p) + val method2 = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(assume2))(p)))(p, Seq()) val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method2), Seq(), Seq())(p) case class Context(increment: Int) @@ -146,7 +146,7 @@ class ASTTransformationTests extends AnyFunSuite { val p = (NoPosition, NoPosition) val requires = PForall(Seq(PFormalArgDecl(PIdnDef("y")(p), TypeHelper.Int)(p)), Seq(), PBinExp(PIdnUse("y")(p), "==", PIdnUse("y")(p))(p))(p) - val function = PFunction(PIdnDef("f")(p), Seq(PFormalArgDecl(PIdnDef("x")(p), TypeHelper.Ref)(p)), TypeHelper.Bool, Seq(requires), Seq(), None)(p) + val function = PFunction(PIdnDef("f")(p), Seq(PFormalArgDecl(PIdnDef("x")(p), TypeHelper.Ref)(p)), TypeHelper.Bool, Seq(requires), Seq(), None)(p, Seq()) val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(), Seq(), Seq())(p) case class Context() diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala index ec953e27f..e6b0b6ab3 100644 --- a/src/test/scala/PluginTests.scala +++ b/src/test/scala/PluginTests.scala @@ -124,7 +124,7 @@ class TestPluginAddPredicate extends SilverPlugin { input.domains, input.fields, input.functions, - input.predicates :+ PPredicate(PIdnDef("testPredicate")(p), Seq(), None)(p), + input.predicates :+ PPredicate(PIdnDef("testPredicate")(p), Seq(), None)(p, Seq()), input.methods, input.extensions, input.errors diff --git a/src/test/scala/SemanticAnalysisTests.scala b/src/test/scala/SemanticAnalysisTests.scala index bb1381f7a..fda4fb733 100644 --- a/src/test/scala/SemanticAnalysisTests.scala +++ b/src/test/scala/SemanticAnalysisTests.scala @@ -29,7 +29,7 @@ class SemanticAnalysisTests extends AnyFunSuite { val p = (NoPosition, NoPosition) val binExp1 = PBinExp(PIntLit(1)(p), "==", PIntLit(1)(p))(p) val binExp2 = PBinExp(PIntLit(1)(p), "==", PIntLit(1)(p))(p) - val method = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PSeqn(Seq(PAssert(binExp1)(p), PSeqn(Seq(PAssert(binExp2)(p)))(p)))(p)))(p)))(p) + val method = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PSeqn(Seq(PAssert(binExp1)(p), PSeqn(Seq(PAssert(binExp2)(p)))(p)))(p)))(p)))(p, Seq()) val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq(), Seq())(p) assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program)) } @@ -37,7 +37,7 @@ class SemanticAnalysisTests extends AnyFunSuite { test("Semantic analysis in AST with shared nodes") { val p = (NoPosition, NoPosition) val binExp = PBinExp(PIntLit(1)(p), "==", PIntLit(1)(p))(p) - val method = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PSeqn(Seq(PAssert(binExp)(p), PSeqn(Seq(PAssert(binExp)(p)))(p)))(p)))(p)))(p) + val method = PMethod(PIdnDef("m")(p), Seq(), Seq(), Seq(), Seq(), Some(PSeqn(Seq(PSeqn(Seq(PAssert(binExp)(p), PSeqn(Seq(PAssert(binExp)(p)))(p)))(p)))(p)))(p, Seq()) val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq(), Seq())(p) assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program)) } From 0b93bdf916e4bc7da4097ef862a21b7987d2e3a8 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 13:15:00 +0200 Subject: [PATCH 4/9] Fixed rewriting of PMethods --- .../scala/viper/silver/ast/utility/rewriter/Rewritable.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala index b2ec5c4ea..c62e5159d 100644 --- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala +++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala @@ -6,7 +6,7 @@ package viper.silver.ast.utility.rewriter -import viper.silver.parser.{PDomain, PDomainFunction} +import viper.silver.parser.{PDomain, PDomainFunction, PMethod} import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position} @@ -53,6 +53,7 @@ trait Rewritable extends Product { case pm: PMagicWandExp => firstArgList = Seq(children.head) ++ children.drop(2) ++ Seq(pos.getOrElse(pm.pos)) case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos), pd.annotations) case pd: PDomain => secondArgList = Seq(pos.getOrElse(pd.pos), pd.annotations) + case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations) case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos)) case _ => } From 585a87d11bdccf08e4e6eda76d30dd8940eecea8 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 13:50:39 +0200 Subject: [PATCH 5/9] Changed syntax, allowing multiple values per key, checking for duplicate keys --- src/main/scala/viper/silver/ast/Ast.scala | 2 +- .../ast/utility/rewriter/Rewritable.scala | 4 +- .../viper/silver/parser/FastParser.scala | 2 +- .../scala/viper/silver/parser/ParseAst.scala | 22 +++++----- .../viper/silver/parser/Translator.scala | 40 +++++++++++++------ .../all/annotation/annotationFail.vpr | 30 ++++++++++++++ ...xpAnnotation.vpr => annotationSuccess.vpr} | 25 ++++++------ 7 files changed, 86 insertions(+), 39 deletions(-) create mode 100644 src/test/resources/all/annotation/annotationFail.vpr rename src/test/resources/all/annotation/{expAnnotation.vpr => annotationSuccess.vpr} (55%) diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala index 13909ca1d..5478d261e 100644 --- a/src/main/scala/viper/silver/ast/Ast.scala +++ b/src/main/scala/viper/silver/ast/Ast.scala @@ -371,7 +371,7 @@ case object NoInfo extends Info { override val isCached = false } -case class AnnotationInfo(values: Map[String, String]) extends Info { +case class AnnotationInfo(values: Map[String, Seq[String]]) extends Info { override val isCached = false override val comment = Nil } diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala index c62e5159d..c5217da02 100644 --- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala +++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala @@ -6,7 +6,7 @@ package viper.silver.ast.utility.rewriter -import viper.silver.parser.{PDomain, PDomainFunction, PMethod} +import viper.silver.parser.{PDomain, PDomainFunction, PFunction, PMethod, PPredicate} import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position} @@ -54,6 +54,8 @@ trait Rewritable extends Product { case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos), pd.annotations) case pd: PDomain => secondArgList = Seq(pos.getOrElse(pd.pos), pd.annotations) case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations) + case pp: PPredicate => secondArgList = Seq(pos.getOrElse(pp.pos), pp.annotations) + case pf: PFunction => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations) case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos)) case _ => } diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 531f2a6b1..02d96ab30 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -805,7 +805,7 @@ class FastParser { def stringLiteral[_: P]: P[String] = P("\"" ~ CharsWhile(_ != '\"').! ~ "\"") - def annotation[_: P]: P[(String, String)] = P("@" ~~ ident ~ stringLiteral) + def annotation[_: P]: P[(String, Seq[String])] = P("@" ~~ ident ~ parens(stringLiteral.rep(sep = ","))) def annotatedAtom[_: P]: P[PExp] = FP(annotation ~ atom).map{ case (pos, (key, value, exp)) => PAnnotatedExp(exp, (key, value))(pos) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 65b6b045d..22ee2d4d3 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -357,7 +357,7 @@ trait PExp extends PNode { def forceSubstitution(ts: PTypeSubstitution): Unit } -case class PAnnotatedExp(e: PExp, annotation: (String, String))(val pos: (Position, Position)) extends PExp { +case class PAnnotatedExp(e: PExp, annotation: (String, Seq[String]))(val pos: (Position, Position)) extends PExp { override def typeSubstitutions: collection.Seq[PTypeSubstitution] = e.typeSubstitutions override def forceSubstitution(ts: PTypeSubstitution): Unit = e.forceSubstitution(ts) } @@ -1056,7 +1056,7 @@ trait PStmt extends PNode { } } -case class PAnnotatedStmt(stmt: PStmt, annotation: (String, String))(val pos: (Position, Position)) extends PStmt +case class PAnnotatedStmt(stmt: PStmt, annotation: (String, Seq[String]))(val pos: (Position, Position)) extends PStmt case class PSeqn(ss: Seq[PStmt])(val pos: (Position, Position)) extends PStmt with PScope case class PFold(e: PExp)(val pos: (Position, Position)) extends PStmt case class PUnfold(e: PExp)(val pos: (Position, Position)) extends PStmt @@ -1164,7 +1164,7 @@ case class PLocalImport(file: String)(val pos: (Position, Position)) extends PIm case class PStandardImport(file: String)(val pos: (Position, Position)) extends PImport() case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalArgDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt]) - (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PGlobalDeclaration { + (val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PGlobalDeclaration { def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, formalReturns: Seq[PFormalArgDecl] = this.formalReturns, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PStmt] = this.body): PMethod = { StrategyBuilder.Slim[PNode]({ case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos, p.annotations) @@ -1180,9 +1180,9 @@ case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalRetur } } case class PDomain(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], funcs: Seq[PDomainFunction], axioms: Seq[PAxiom], interpretations: Option[Map[String, String]]) - (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PGlobalDeclaration + (val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PGlobalDeclaration case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PType, pres: Seq[PExp], posts: Seq[PExp], body: Option[PExp]) - (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PAnyFunction { + (val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PAnyFunction { def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, typ: PType = this.typ, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PExp] = this.body): PFunction = { StrategyBuilder.Slim[PNode]({ case p: PFunction => PFunction(idndef, formalArgs, typ, pres, posts, body)(p.pos, p.annotations) @@ -1191,16 +1191,16 @@ case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PTyp } case class PDomainFunction(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String]) - (val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PAnyFunction -case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PScope -case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PTypedDeclaration with PGlobalDeclaration + (val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PAnyFunction +case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PScope +case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PTypedDeclaration with PGlobalDeclaration case class PPredicate(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], body: Option[PExp]) - (val pos: (Position, Position), val annotations: Seq[(String, String)]) extends PMember with PTypedDeclaration with PGlobalDeclaration{ + (val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PTypedDeclaration with PGlobalDeclaration{ val typ = PPredicateType()() } -case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position), val annotations: Seq[(String, String)]) -case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position), val annotations: Seq[(String, String)]) +case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) +case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) /** * A entity represented by names for whom we have seen more than one diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 3b7476266..9c598f7fd 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -105,9 +105,9 @@ case class Translator(program: PProgram) { private def translate(a: PAxiom): DomainAxiom = a match { case pa@PAxiom(Some(name), e) => - NamedDomainAxiom(name.name, exp(e))(a, toInfo(pa.annotations), domainName = pa.domainName.name) + NamedDomainAxiom(name.name, exp(e))(a, toInfo(pa.annotations, pa), domainName = pa.domainName.name) case pa@PAxiom(None, e) => - AnonymousDomainAxiom(exp(e))(a, toInfo(pa.annotations), domainName = pa.domainName.name) + AnonymousDomainAxiom(exp(e))(a, toInfo(pa.annotations, pa), domainName = pa.domainName.name) } private def translate(f: PFunction): Function = f match { @@ -144,26 +144,34 @@ case class Translator(program: PProgram) { val name = p.idndef.name val t = p match { case pf@PField(_, typ) => - Field(name, ttyp(typ))(pos, toInfo(pf.annotations)) + Field(name, ttyp(typ))(pos, toInfo(pf.annotations, pf)) case pf@PFunction(_, formalArgs, typ, _, _, _) => - Function(name, formalArgs map liftVarDecl, ttyp(typ), null, null, null)(pos, toInfo(pf.annotations)) + Function(name, formalArgs map liftVarDecl, ttyp(typ), null, null, null)(pos, toInfo(pf.annotations, pf)) case pdf@ PDomainFunction(_, args, typ, unique, interp) => - DomainFunc(name, args map liftAnyVarDecl, ttyp(typ), unique, interp)(pos,toInfo(pdf.annotations),pdf.domainName.name) + DomainFunc(name, args map liftAnyVarDecl, ttyp(typ), unique, interp)(pos,toInfo(pdf.annotations, pdf),pdf.domainName.name) case pd@PDomain(_, typVars, _, _, interp) => - Domain(name, null, null, typVars map (t => TypeVar(t.idndef.name)), interp)(pos, toInfo(pd.annotations)) + Domain(name, null, null, typVars map (t => TypeVar(t.idndef.name)), interp)(pos, toInfo(pd.annotations, pd)) case pp@PPredicate(_, formalArgs, _) => - Predicate(name, formalArgs map liftVarDecl, null)(pos, toInfo(pp.annotations)) + Predicate(name, formalArgs map liftVarDecl, null)(pos, toInfo(pp.annotations, pp)) case pm@PMethod(_, formalArgs, formalReturns, _, _, _) => - Method(name, formalArgs map liftVarDecl, formalReturns map liftVarDecl, null, null, null)(pos, toInfo(pm.annotations)) + Method(name, formalArgs map liftVarDecl, formalReturns map liftVarDecl, null, null, null)(pos, toInfo(pm.annotations, pm)) } members.put(p.idndef.name, t) } - def toInfo(annotations: Seq[(String, String)]): Info = { - if (annotations.isEmpty) + def toInfo(annotations: Seq[(String, Seq[String])], node: PNode): Info = { + if (annotations.isEmpty) { NoInfo - else + } else { + val keys = annotations.map(_._1) + val duplicates = keys.diff(keys.distinct).distinct + if (duplicates.nonEmpty) { + for (dupKey <- duplicates) { + Consistency.messages ++= FastMessaging.message(node, s"duplicate annotation $dupKey") + } + } AnnotationInfo(annotations.toMap) + } } private def translateMemberSignature(p: PExtender): Unit ={ @@ -279,19 +287,25 @@ case class Translator(program: PProgram) { } } - def extractAnnotation(pexp: PExp): (PExp, Map[String, String]) = { + def extractAnnotation(pexp: PExp): (PExp, Map[String, Seq[String]]) = { pexp match { case PAnnotatedExp(e, (key, value)) => val (resPexp, innerMap) = extractAnnotation(e) + if (innerMap.contains(key)) { + Consistency.messages ++= FastMessaging.message(pexp, s"duplicate annotation $key") + } (resPexp, innerMap.updated(key, value)) case _ => (pexp, Map()) } } - def extractAnnotationFromStmt(pStmt: PStmt): (PStmt, Map[String, String]) = { + def extractAnnotationFromStmt(pStmt: PStmt): (PStmt, Map[String, Seq[String]]) = { pStmt match { case PAnnotatedStmt(s, (key, value)) => val (resPStmt, innerMap) = extractAnnotationFromStmt(s) + if (innerMap.contains(key)) { + Consistency.messages ++= FastMessaging.message(pStmt, s"duplicate annotation $key") + } (resPStmt, innerMap.updated(key, value)) case _ => (pStmt, Map()) } diff --git a/src/test/resources/all/annotation/annotationFail.vpr b/src/test/resources/all/annotation/annotationFail.vpr new file mode 100644 index 000000000..875fe85c2 --- /dev/null +++ b/src/test/resources/all/annotation/annotationFail.vpr @@ -0,0 +1,30 @@ +//:: ExpectedOutput(consistency.error) +@isghost("nope") +@isghost("yes") +field f: Int + +@setting("donotverify") +@verifier("none", "atall") +method m(x: Ref, y: Ref) + requires acc(x.f) + requires acc(y.f) +{ + var tmp: Ref + //:: ExpectedOutput(consistency.error) + @annotatingastatement("the assignment") + @annotatingastatement("double") + tmp := x + y.f := 1 +} + +@setting("donotverify") +@verifier("none", "atall") +method m2(x: Ref, y: Ref) + requires acc(x.f) + requires acc(y.f) +{ + var tmp: Ref + //:: ExpectedOutput(consistency.error) + tmp := @asd("test 123") @asd("test 1234") x + y.f := 1 +} \ No newline at end of file diff --git a/src/test/resources/all/annotation/expAnnotation.vpr b/src/test/resources/all/annotation/annotationSuccess.vpr similarity index 55% rename from src/test/resources/all/annotation/expAnnotation.vpr rename to src/test/resources/all/annotation/annotationSuccess.vpr index fee4953c0..9bd18549f 100644 --- a/src/test/resources/all/annotation/expAnnotation.vpr +++ b/src/test/resources/all/annotation/annotationSuccess.vpr @@ -1,7 +1,7 @@ -@isghost "nope" +@isghost("nope") field f: Int -@inlining "never" +@inlining("never", "inmylife") function fun01(x: Ref, y: Ref, b: Bool): Int requires b ? acc(x.f) : acc(y.f) @@ -9,32 +9,33 @@ function fun02(x: Ref, y: Ref, b: Bool): Int requires acc(x.f, b ? write : none) requires acc(y.f, !b ? write : none) -@inline "never" +@inline("never", "ever") predicate P(x: Ref) -@interp "some smtlib thingy" +@interp("some smtlib thingy") domain MyType { - @asd "test 123" - @asdd "test 123" + @asd("test 123") + @asdd("test 123") function id(MyType): MyType - @asd "test 123" + @asd("test 123") axiom { - @asd "test 123" + @asd("test 123", "huh") + @asdasd() true } } -@setting "donotverify" -@verifier "none" +@setting("donotverify") +@verifier("none", "atall") method m(x: Ref, y: Ref) requires acc(x.f) requires acc(y.f) { var tmp: Int - @annotatingastatement "the assignment" - tmp := @asd "test 123" fun02(x, @lul "this is ugly" y, true) + @annotatingastatement("the assignment") + tmp := @asd("test 123") fun02(x, @lul("this is ugly") y, true) y.f := 1 assert tmp == fun02(x, y, true) } \ No newline at end of file From 3320fef0398d20c2374f1fcc34a6da880d30c9a1 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 14:58:26 +0200 Subject: [PATCH 6/9] Fixed field rewriting --- .../scala/viper/silver/ast/utility/rewriter/Rewritable.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala index c5217da02..97ff78f3d 100644 --- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala +++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala @@ -6,7 +6,7 @@ package viper.silver.ast.utility.rewriter -import viper.silver.parser.{PDomain, PDomainFunction, PFunction, PMethod, PPredicate} +import viper.silver.parser.{PDomain, PDomainFunction, PField, PFunction, PMethod, PPredicate} import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position} @@ -56,6 +56,7 @@ trait Rewritable extends Product { case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations) case pp: PPredicate => secondArgList = Seq(pos.getOrElse(pp.pos), pp.annotations) case pf: PFunction => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations) + case pf: PField => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations) case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos)) case _ => } From bcb209b7912606499f9ca56321db8a2b63588774 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 15:36:12 +0200 Subject: [PATCH 7/9] Fixed test annotations --- src/test/resources/all/annotation/annotationFail.vpr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/resources/all/annotation/annotationFail.vpr b/src/test/resources/all/annotation/annotationFail.vpr index 875fe85c2..a16f1ea95 100644 --- a/src/test/resources/all/annotation/annotationFail.vpr +++ b/src/test/resources/all/annotation/annotationFail.vpr @@ -1,4 +1,4 @@ -//:: ExpectedOutput(consistency.error) +//:: ExpectedOutput(typechecker.error) @isghost("nope") @isghost("yes") field f: Int @@ -10,7 +10,7 @@ method m(x: Ref, y: Ref) requires acc(y.f) { var tmp: Ref - //:: ExpectedOutput(consistency.error) + //:: ExpectedOutput(typechecker.error) @annotatingastatement("the assignment") @annotatingastatement("double") tmp := x @@ -24,7 +24,7 @@ method m2(x: Ref, y: Ref) requires acc(y.f) { var tmp: Ref - //:: ExpectedOutput(consistency.error) + //:: ExpectedOutput(typechecker.error) tmp := @asd("test 123") @asd("test 1234") x y.f := 1 } \ No newline at end of file From d32493c23788237fd203f4815aa7d0f2facba82f Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 12 May 2023 17:26:16 +0200 Subject: [PATCH 8/9] Multiple annotations with same key are allowed, added test --- .../viper/silver/parser/Translator.scala | 25 ++-- .../all/annotation/annotationFail.vpr | 30 ----- .../all/annotation/annotationSuccess.vpr | 3 +- src/test/scala/AstAnnotationTests.scala | 120 ++++++++++++++++++ 4 files changed, 133 insertions(+), 45 deletions(-) delete mode 100644 src/test/resources/all/annotation/annotationFail.vpr create mode 100644 src/test/scala/AstAnnotationTests.scala diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 9c598f7fd..5f7ef90ed 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -163,14 +163,7 @@ case class Translator(program: PProgram) { if (annotations.isEmpty) { NoInfo } else { - val keys = annotations.map(_._1) - val duplicates = keys.diff(keys.distinct).distinct - if (duplicates.nonEmpty) { - for (dupKey <- duplicates) { - Consistency.messages ++= FastMessaging.message(node, s"duplicate annotation $dupKey") - } - } - AnnotationInfo(annotations.toMap) + AnnotationInfo(annotations.groupBy(_._1).map{ case (k, v) => k -> v.unzip._2.flatten}) } } @@ -291,10 +284,12 @@ case class Translator(program: PProgram) { pexp match { case PAnnotatedExp(e, (key, value)) => val (resPexp, innerMap) = extractAnnotation(e) - if (innerMap.contains(key)) { - Consistency.messages ++= FastMessaging.message(pexp, s"duplicate annotation $key") + val combinedValue = if (innerMap.contains(key)) { + value ++ innerMap(key) + } else { + value } - (resPexp, innerMap.updated(key, value)) + (resPexp, innerMap.updated(key, combinedValue)) case _ => (pexp, Map()) } } @@ -303,10 +298,12 @@ case class Translator(program: PProgram) { pStmt match { case PAnnotatedStmt(s, (key, value)) => val (resPStmt, innerMap) = extractAnnotationFromStmt(s) - if (innerMap.contains(key)) { - Consistency.messages ++= FastMessaging.message(pStmt, s"duplicate annotation $key") + val combinedValue = if (innerMap.contains(key)) { + value ++ innerMap(key) + } else { + value } - (resPStmt, innerMap.updated(key, value)) + (resPStmt, innerMap.updated(key, combinedValue)) case _ => (pStmt, Map()) } } diff --git a/src/test/resources/all/annotation/annotationFail.vpr b/src/test/resources/all/annotation/annotationFail.vpr deleted file mode 100644 index a16f1ea95..000000000 --- a/src/test/resources/all/annotation/annotationFail.vpr +++ /dev/null @@ -1,30 +0,0 @@ -//:: ExpectedOutput(typechecker.error) -@isghost("nope") -@isghost("yes") -field f: Int - -@setting("donotverify") -@verifier("none", "atall") -method m(x: Ref, y: Ref) - requires acc(x.f) - requires acc(y.f) -{ - var tmp: Ref - //:: ExpectedOutput(typechecker.error) - @annotatingastatement("the assignment") - @annotatingastatement("double") - tmp := x - y.f := 1 -} - -@setting("donotverify") -@verifier("none", "atall") -method m2(x: Ref, y: Ref) - requires acc(x.f) - requires acc(y.f) -{ - var tmp: Ref - //:: ExpectedOutput(typechecker.error) - tmp := @asd("test 123") @asd("test 1234") x - y.f := 1 -} \ No newline at end of file diff --git a/src/test/resources/all/annotation/annotationSuccess.vpr b/src/test/resources/all/annotation/annotationSuccess.vpr index 9bd18549f..aa3adbda4 100644 --- a/src/test/resources/all/annotation/annotationSuccess.vpr +++ b/src/test/resources/all/annotation/annotationSuccess.vpr @@ -10,6 +10,7 @@ function fun02(x: Ref, y: Ref, b: Bool): Int requires acc(y.f, !b ? write : none) @inline("never", "ever") +@inline("ever") predicate P(x: Ref) @interp("some smtlib thingy") @@ -35,7 +36,7 @@ method m(x: Ref, y: Ref) { var tmp: Int @annotatingastatement("the assignment") - tmp := @asd("test 123") fun02(x, @lul("this is ugly") y, true) + tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true) y.f := 1 assert tmp == fun02(x, y, true) } \ No newline at end of file diff --git a/src/test/scala/AstAnnotationTests.scala b/src/test/scala/AstAnnotationTests.scala new file mode 100644 index 000000000..dcb8a7136 --- /dev/null +++ b/src/test/scala/AstAnnotationTests.scala @@ -0,0 +1,120 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2020 ETH Zurich. + +import org.scalatest.funsuite.AnyFunSuite +import viper.silver.ast.Program +import viper.silver.frontend._ +import viper.silver.logger.ViperStdOutLogger +import viper.silver.reporter.StdIOReporter + +class AstAnnotationTests extends AnyFunSuite { + object AstProvider extends ViperAstProvider(StdIOReporter(), ViperStdOutLogger("AstAnnotationTestsLogger").get) { + def setCode(code: String): Unit = { + _input = Some(code) + } + + override def reset(input: java.nio.file.Path): Unit = { + if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.") + _state = DefaultStates.InputSet + _inputFile = Some(input) + /** must be set by [[setCode]] */ + // _input = None + _errors = Seq() + _parsingResult = None + _semanticAnalysisResult = None + _verificationResult = None + _program = None + resetMessages() + } + } + + def generateViperAst(code: String): Option[Program] = { + + val code_id = code.hashCode.asInstanceOf[Short].toString + AstProvider.setCode(code) + AstProvider.execute(Array("--ignoreFile", code_id)) + + if (AstProvider.errors.isEmpty) { + Some(AstProvider.translationResult) + } else { + AstProvider.logger.error(s"An error occurred while translating ${AstProvider.errors}") + None + } + } + + test("Correct annotations for AST nodes in a parsed program") { + import viper.silver.ast._ + + val code = + """@isghost("nope") + |field f: Int + | + |@inlining("never", "inmylife") + |function fun01(x: Ref, y: Ref, b: Bool): Int + | requires b ? acc(x.f) : acc(y.f) + | + |function fun02(x: Ref, y: Ref, b: Bool): Int + | requires acc(x.f, b ? write : none) + | requires acc(y.f, !b ? write : none) + | + |@inline("never", "ever") + |@inline("ever") + |predicate P(x: Ref) + | + |@interp("some smtlib thingy") + |domain MyType { + | + | @asd("test 123") + | @asdd("test 123", "test 125") + | function id(MyType): MyType + | + | @asd("test 123") + | axiom { + | @asd("test 123", "huh") + | @asdasd() + | true + | } + |} + | + |@setting("donotverify") + |@verifier("none", "atall") + |method m(x: Ref, y: Ref) + | requires acc(x.f) + | requires acc(y.f) + |{ + | var tmp: Int + | @annotatingastatement("the assignment", "12") + | @annotatingastatement("34") + | @suchannotations() + | tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true) + | y.f := 1 + | assert tmp == fun02(x, y, true) + |} + |""".stripMargin + + val res: Program = generateViperAst(code).get + + val fieldAnn = res.findField("f").info.getUniqueInfo[AnnotationInfo].get + assert(fieldAnn.values == Map("isghost" -> Seq("nope"))) + + val predAnn = res.findPredicate("P").info.getUniqueInfo[AnnotationInfo].get + assert(predAnn.values == Map("inline" -> Seq("never", "ever", "ever"))) + + val dFuncAnn = res.findDomainFunction("id").info.getUniqueInfo[AnnotationInfo].get + assert(dFuncAnn.values == Map("asd" -> Seq("test 123"), "asdd" -> Seq("test 123", "test 125"))) + + val assignment = res.methods.head.body.get.ss(1) + val assignmentAnn = assignment.info.getUniqueInfo[AnnotationInfo].get + assert(assignmentAnn.values == Map("annotatingastatement" -> Seq("the assignment", "12", "34"), "suchannotations" -> Seq())) + + val rhs = assignment.asInstanceOf[LocalVarAssign].rhs + val rhsAnn = rhs.info.getUniqueInfo[AnnotationInfo].get + assert(rhsAnn.values == Map("asd" -> Seq("test 123"))) + + val argAnn = rhs.asInstanceOf[FuncApp].args(1).info.getUniqueInfo[AnnotationInfo].get + assert(argAnn.values == Map("ann" -> Seq("this is ugly"))) + } +} From 8c6b733a871368c0e23fe2c586ee251c6b005fc4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 12 May 2023 17:38:41 +0200 Subject: [PATCH 9/9] Allowing . in annotation keys --- src/main/scala/viper/silver/parser/FastParser.scala | 4 +++- src/test/resources/all/annotation/annotationSuccess.vpr | 2 +- src/test/scala/AstAnnotationTests.scala | 4 ++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 1cec6bd53..5adab5194 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -805,7 +805,7 @@ class FastParser { def stringLiteral[$: P]: P[String] = P("\"" ~ CharsWhile(_ != '\"').! ~ "\"") - def annotation[$: P]: P[(String, Seq[String])] = P("@" ~~ ident ~ parens(stringLiteral.rep(sep = ","))) + def annotation[$: P]: P[(String, Seq[String])] = P("@" ~~ annotationIdentifier ~ parens(stringLiteral.rep(sep = ","))) def annotatedAtom[$: P]: P[PExp] = FP(annotation ~ atom).map{ case (pos, (key, value, exp)) => PAnnotatedExp(exp, (key, value))(pos) @@ -827,6 +827,8 @@ class FastParser { def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX + def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).! + def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("invalid identifier (could be a keyword)") def idnuse[$: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) } diff --git a/src/test/resources/all/annotation/annotationSuccess.vpr b/src/test/resources/all/annotation/annotationSuccess.vpr index aa3adbda4..d86418159 100644 --- a/src/test/resources/all/annotation/annotationSuccess.vpr +++ b/src/test/resources/all/annotation/annotationSuccess.vpr @@ -35,7 +35,7 @@ method m(x: Ref, y: Ref) requires acc(y.f) { var tmp: Int - @annotatingastatement("the assignment") + @annotating.a.statement("the assignment") tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true) y.f := 1 assert tmp == fun02(x, y, true) diff --git a/src/test/scala/AstAnnotationTests.scala b/src/test/scala/AstAnnotationTests.scala index dcb8a7136..f8f04954a 100644 --- a/src/test/scala/AstAnnotationTests.scala +++ b/src/test/scala/AstAnnotationTests.scala @@ -88,7 +88,7 @@ class AstAnnotationTests extends AnyFunSuite { | var tmp: Int | @annotatingastatement("the assignment", "12") | @annotatingastatement("34") - | @suchannotations() + | @such.annotations() | tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true) | y.f := 1 | assert tmp == fun02(x, y, true) @@ -108,7 +108,7 @@ class AstAnnotationTests extends AnyFunSuite { val assignment = res.methods.head.body.get.ss(1) val assignmentAnn = assignment.info.getUniqueInfo[AnnotationInfo].get - assert(assignmentAnn.values == Map("annotatingastatement" -> Seq("the assignment", "12", "34"), "suchannotations" -> Seq())) + assert(assignmentAnn.values == Map("annotatingastatement" -> Seq("the assignment", "12", "34"), "such.annotations" -> Seq())) val rhs = assignment.asInstanceOf[LocalVarAssign].rhs val rhsAnn = rhs.info.getUniqueInfo[AnnotationInfo].get