Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for backend annotations on functions and methods #749

Merged
merged 10 commits into from
Mar 25, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/main/antlr4/GobraLexer.g4
Original file line number Diff line number Diff line change
Expand Up @@ -90,4 +90,5 @@ GHOST_EQUALS : '===';
GHOST_NOT_EQUALS : '!==';
WITH : 'with';
OPAQUE : 'opaque' -> mode(NLSEMI);
REVEAL : 'reveal';
REVEAL : 'reveal';
BACKEND : '#backend';
10 changes: 8 additions & 2 deletions src/main/antlr4/GobraParser.g4
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ stmtOnly: statement EOF;

typeOnly: type_ EOF;


// Identifier lists with added addressability modifiers
maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressableIdentifier)*;

Expand Down Expand Up @@ -162,9 +161,16 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
// Specifications

specification returns[boolean trusted = false, boolean pure = false, boolean opaque = false;]:
((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
// Non-greedily match PURE to avoid missing eos errors.
((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
;

backendAnnotationEntry: ~('('|')'|',')+;
listOfValues: backendAnnotationEntry (COMMA backendAnnotationEntry)*;
singleBackendAnnotation: backendAnnotationEntry L_PAREN listOfValues? R_PAREN;
backendAnnotationList: singleBackendAnnotation (COMMA singleBackendAnnotation)*;
backendAnnotation: BACKEND L_BRACKET backendAnnotationList? R_BRACKET eos;

specStatement
: kind=PRE assertion
| kind=PRESERVES assertion
Expand Down
2,235 changes: 1,121 additions & 1,114 deletions src/main/java/viper/gobra/frontend/GobraLexer.java

Large diffs are not rendered by default.

5,550 changes: 2,955 additions & 2,595 deletions src/main/java/viper/gobra/frontend/GobraParser.java

Large diffs are not rendered by default.

37 changes: 36 additions & 1 deletion src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
package viper.gobra.frontend;
import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;

Expand Down Expand Up @@ -376,6 +376,41 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSpecification(GobraParser.SpecificationContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitBackendAnnotationEntry(GobraParser.BackendAnnotationEntryContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitListOfValues(GobraParser.ListOfValuesContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSingleBackendAnnotation(GobraParser.SingleBackendAnnotationContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitBackendAnnotationList(GobraParser.BackendAnnotationListContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitBackendAnnotation(GobraParser.BackendAnnotationContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
Expand Down
32 changes: 31 additions & 1 deletion src/main/java/viper/gobra/frontend/GobraParserVisitor.java
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
package viper.gobra.frontend;
import org.antlr.v4.runtime.tree.ParseTreeVisitor;

Expand Down Expand Up @@ -326,6 +326,36 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
* @return the visitor result
*/
T visitSpecification(GobraParser.SpecificationContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#backendAnnotationEntry}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitBackendAnnotationEntry(GobraParser.BackendAnnotationEntryContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#listOfValues}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitListOfValues(GobraParser.ListOfValuesContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#singleBackendAnnotation}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitSingleBackendAnnotation(GobraParser.SingleBackendAnnotationContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#backendAnnotationList}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitBackendAnnotationList(GobraParser.BackendAnnotationListContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#backendAnnotation}.
* @param ctx the parse tree
* @return the visitor result
*/
T visitBackendAnnotation(GobraParser.BackendAnnotationContext ctx);
/**
* Visit a parse tree produced by {@link GobraParser#specStatement}.
* @param ctx the parse tree
Expand Down
17 changes: 10 additions & 7 deletions src/main/scala/viper/gobra/ast/frontend/Ast.scala
Original file line number Diff line number Diff line change
Expand Up @@ -877,15 +877,18 @@ case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PEx
sealed trait PSpecification extends PGhostNode

case class PFunctionSpec(
pres: Vector[PExpression],
preserves: Vector[PExpression],
posts: Vector[PExpression],
terminationMeasures: Vector[PTerminationMeasure],
isPure: Boolean = false,
isTrusted: Boolean = false,
isOpaque: Boolean = false,
pres: Vector[PExpression],
preserves: Vector[PExpression],
posts: Vector[PExpression],
terminationMeasures: Vector[PTerminationMeasure],
backendAnnotations: Vector[PBackendAnnotation],
isPure: Boolean = false,
isTrusted: Boolean = false,
isOpaque: Boolean = false,
) extends PSpecification

case class PBackendAnnotation(key: String, values: Vector[String]) extends PGhostMisc

case class PBodyParameterInfo(
/**
* Stores parameters that have been declared as shared in the body of a function or method.
Expand Down
16 changes: 12 additions & 4 deletions src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -144,14 +144,15 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showSpec(spec: PSpecification): Doc = spec match {
case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted, isOpaque) =>
case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque) =>
(if (isPure) showPure else emptyDoc) <>
(if (isOpaque) showOpaque else emptyDoc) <>
(if (isTrusted) showTrusted else emptyDoc) <>
hcat(pres map (showPre(_) <> line)) <>
hcat(preserves map (showPreserves(_) <> line)) <>
hcat(posts map (showPost(_) <> line)) <>
hcat(measures map (showTerminationMeasure(_) <> line))
hcat(preserves map (showPreserves(_) <> line)) <>
hcat(posts map (showPost(_) <> line)) <>
hcat(measures map (showTerminationMeasure(_) <> line)) <>
showBackendAnnotations(backendAnnotations) <> line

case PLoopSpec(inv, measure) =>
hcat(inv map (showInv(_) <> line)) <> opt(measure)(showTerminationMeasure) <> line
Expand Down Expand Up @@ -691,6 +692,12 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter

def showLabel(id: PLabelNode): Doc = id.name

def showBackendAnnotation(annotation: PBackendAnnotation): Doc =
annotation.key <> parens(showList(annotation.values)(d => d))

def showBackendAnnotations(annotations: Vector[PBackendAnnotation]): Doc =
"#backend" <> brackets(showList(annotations)(showBackendAnnotation))

// misc

def showMisc(id: PMisc): Doc = id match {
Expand Down Expand Up @@ -729,6 +736,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
case expr: PMatchPattern => showMatchPattern(expr)
case c: PMatchExpDefault => showMatchExpClause(c)
case c: PMatchExpCase => showMatchExpClause(c)
case a: PBackendAnnotation => showBackendAnnotation(a)
}
}

Expand Down
67 changes: 41 additions & 26 deletions src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import org.bitbucket.inkytonik.kiama
import org.bitbucket.inkytonik.kiama.util.Trampolines.Done
import viper.gobra.ast.printing.PrettyPrinterCombinators
import viper.gobra.theory.Addressability
import viper.gobra.util.{Binary, Decimal, Hexadecimal, Octal}
import viper.gobra.util.{BackendAnnotation, Binary, Decimal, Hexadecimal, Octal}
import viper.silver.ast.{Position => GobraPosition}

import scala.collection.mutable
Expand Down Expand Up @@ -144,29 +144,29 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showFunction(f: Function): Doc = f match {
case Function(name, args, results, pres, posts, measures, body) =>
case Function(name, args, results, pres, posts, measures, backendAnnotations, body) =>
"func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block(showStmt(b)))
}

def showPureFunction(f: PureFunction): Doc = f match {
case PureFunction(name, args, results, pres, posts, measures, body, isOpaque) =>
case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque) =>
val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <> "pure func"
funcPrefix <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block("return" <+> showExpr(b)))
}

def showMethod(m: Method): Doc = m match {
case Method(receiver, name, args, results, pres, posts, measures, body) =>
case Method(receiver, name, args, results, pres, posts, measures, backendAnnotations, body) =>
"func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block(showStmt(b)))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block(showStmt(b)))
}

def showPureMethod(m: PureMethod): Doc = m match {
case PureMethod(receiver, name, args, results, pres, posts, measures, body, isOpaque) =>
case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque) =>
val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <> "pure func"
funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block("return" <+> showExpr(b)))
}

def showMethodSubtypeProof(m: MethodSubtypeProof): Doc = m match {
Expand Down Expand Up @@ -221,6 +221,12 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
case Field(name, typ, _) => "field" <> name <> ":" <+> showType(typ)
})

def showBackendAnnotations(annotations: Vector[BackendAnnotation]): Doc =
"#backend" <> brackets(showList(annotations)(showBackendAnnotation)) <> line

def showBackendAnnotation(annotation: BackendAnnotation): Doc =
annotation.key <> parens(showList(annotation.values)(d => d))

def showClosureSpec(spec: ClosureSpec): Doc =
showProxy(spec.func) <> braces(ssep(spec.params.map(p => p._1.toString <> colon <> showExpr(p._2)).toSeq, comma <> space))

Expand Down Expand Up @@ -351,9 +357,10 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
showVar(resTarget) <> "," <+> showVar(successTarget) <+> "=" <+> showExpr(mapLookup)
case PredExprFold(base, args, p) => "fold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
case PredExprUnfold(base, args, p) => "unfold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
case Outline(_, pres, posts, measures, body, trusted) =>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
"outline" <> (if (trusted) emptyDoc else parens(nest(line <> showStmt(body)) <> line))
case Outline(_, pres, posts, measures, backendAnnotations, body, trusted) =>
spec(showPreconditions(pres) <>
showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <>
"outline" <> (if (trusted) emptyDoc else parens(nest(line <> showStmt(body)) <> line))
case Continue(l, _) => "continue" <+> opt(l)(text)
case Break(l, _) => "break" <+> opt(l)(text)
})
Expand Down Expand Up @@ -607,14 +614,16 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
case BoolLit(b) => if (b) "true" else "false"
case NilLit(t) => parens("nil" <> ":" <> showType(t))

case FunctionLit(name, args, captured, results, pres, posts, measures, body) =>
case FunctionLit(name, args, captured, results, pres, posts, measures, backendAnnotations, body) =>
"func" <+> showProxy(name) <> showCaptured(captured) <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <>
showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <>
opt(body)(b => block(showStmt(b)))

case PureFunctionLit(name, args, captured, results, pres, posts, measures, body) =>
case PureFunctionLit(name, args, captured, results, pres, posts, measures, backendAnnotations, body) =>
"pure func" <+> showProxy(name) <> showCaptured(captured) <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <>
opt(body)(b => block("return" <+> showExpr(b)))

case ArrayLit(len, typ, elems) => {
val lenP = brackets(len.toString)
Expand Down Expand Up @@ -680,29 +689,33 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {


override def showFunction(f: Function): Doc = f match {
case Function(name, args, results, pres, posts, measures, _) =>
case Function(name, args, results, pres, posts, measures, backendAnnotations, _) =>
"func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
spec(showPreconditions(pres) <>
showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations))
}

override def showPureFunction(f: PureFunction): Doc = f match {
case PureFunction(name, args, results, pres, posts, measures, _, isOpaque) =>
case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque) =>
val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
funcPrefix <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
showBackendAnnotations(backendAnnotations))
}

override def showMethod(m: Method): Doc = m match {
case Method(receiver, name, args, results, pres, posts, measures, _) =>
case Method(receiver, name, args, results, pres, posts, measures, backendAnnotations, _) =>
"func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
showBackendAnnotations(backendAnnotations))
}

override def showPureMethod(m: PureMethod): Doc = m match {
case PureMethod(receiver, name, args, results, pres, posts, measures, _, isOpaque) =>
case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque) =>
val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
showBackendAnnotations(backendAnnotations))
}

override def showFPredicate(predicate: FPredicate): Doc = predicate match {
Expand Down Expand Up @@ -794,8 +807,10 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
case PredExprUnfold(base, args, p) => "unfold" <+> "acc" <> parens(showExpr(base) <> parens(showExprList(args)) <> "," <+> showExpr(p))
case Continue(l, _) => "continue" <+> opt(l)(text)
case Break(l, _) => "break" <+> opt(l)(text)
case Outline(_, pres, posts, measures, _, _) =>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <>
case Outline(_, pres, posts, measures, backendAnnotations, _, _) =>
spec(showPreconditions(pres) <>
showPostconditions(posts) <> showTerminationMeasures(measures)) <>
showBackendAnnotations(backendAnnotations) <>
"outline"
}
}
Loading
Loading