Add support for backend annotations on functions and methods (#749)

* extend the syntax of Gobra * goifying printer * bureaucracy * Add encoding and tests * fix test * add an extra annotation * Fix unit tests * fix tests * implement feedback from Felix * improve a few things here and there
viperproject · Mar 25, 2024 · 09b191b · 09b191b
1 parent a2afc5b
commit 09b191b
Show file tree

Hide file tree

Showing 35 changed files with 4,470 additions and 3,820 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -90,4 +90,5 @@ GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
 OPAQUE      : 'opaque' -> mode(NLSEMI);
-REVEAL      : 'reveal';
+REVEAL      : 'reveal';
+BACKEND     : '#backend';
diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -25,7 +25,6 @@ stmtOnly: statement EOF;
 
 typeOnly: type_ EOF;
 
-
 // Identifier lists with added addressability modifiers
 maybeAddressableIdentifierList: maybeAddressableIdentifier (COMMA maybeAddressableIdentifier)*;
 
@@ -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

diff --git a/src/main/java/viper/gobra/frontend/GobraLexer.java b/src/main/java/viper/gobra/frontend/GobraLexer.java
diff --git a/src/main/java/viper/gobra/frontend/GobraParser.java b/src/main/java/viper/gobra/frontend/GobraParser.java
diff --git a/src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java b/src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java
@@ -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;
 
@@ -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}
 	 *

diff --git a/src/main/java/viper/gobra/frontend/GobraParserVisitor.java b/src/main/java/viper/gobra/frontend/GobraParserVisitor.java
@@ -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;
 
@@ -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

diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala
@@ -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.

diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
@@ -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
@@ -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 {
@@ -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)
     }
   }
 

diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
@@ -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
@@ -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 {
@@ -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))
 
@@ -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)
   })
@@ -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)
@@ -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 {
@@ -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"
   }
 }