Introduce support for closures (#479)

* Extend parser with closure literal * Temporary * Type checking for function literals * Internal Program object * Use correct substitutions within function literals * Within desugaring, replace captured variables with their reference * Fix Ghostless printer * Fix warnings, finish implementation of desugarer * Implement encoding of function literals, including encoding of closure domain, satisfies functions, default getter * Small refactorings * Implement parsing and type checking of closure spec instances and implements expressions * Implement desugaring and encoding of spec instance literals and implements assertion * Add support for treating method members as closures * Implement encoding of closure calls * Implement parsing and type checking of closure implementation proofs * Introduce desugaring and encoding of spec proof statements * In spec implementation proofs, introduce an alias for the closure to avoid access permissions problems * Fixes * Introduce closure objects, fix ghostness of function and method constants * Add ghost erasure tests * Try to support importing packages * Add fixes to support closures when importing packages * Extend type checking to make sure that closure names are not use improperly * Refactor name resolution * Fix ghostness checks for closure calls and spec implementation proofs * Fix warnings * Fix errors if spec name not found * Fix error, improve how the encoding deals with pure functions or literals * Fix bugs, add examples * add closure import tests * Fix bugs * Add comments * Fix bug * Add comments, fix parser * Rename some files/classes * Fix Goification, add copyright headers to all new files * Fix test * Fix custom error condition * Remove blank line * Fix bug causing violation * Encode function nil, fix error message for closure calls * Add test examples, fix bug causing crash while type checking * More test cases (including examples with call descriptions) * Fix encoding of captured variables as domain functions (allowing types different from Ref) * Remove changes made for debugging and left there by mistake * Make ClosureImplements a ghost expression (instead of an assertion), allow shareable closure arguments * Address some comments (mainly refactorings) * Remove PClosureNamedDecl * Address typing comments (name resolution in proofs, closure spec used as operand) * Delete PClosureSpecParameter, use PKeyedElement instead; regenerate ANTLR sources * Solve bug caused by merge * Remove PCallWithSpec and internal.CallWithSpec, use PInvoke and method, function calls instead * Change one of the test examples to make it shorter * Fix bug causing crash (wrong value passed to error message) * Introduce ClosureCall and PureClosureCall * Fix termination-related problems with proof and function/method objects * Fix bug * Improve documentation of the encoding * Change a word in a comment * Remove default value for info parameter in Desugar, other minor changes * Change proof loop so that it actually terminates * Simplify genConversion function in MethodObjectEncoder * Fix ambiguity resolution between ClosureCall and FunctionCall, remove termination measures when unnecessary * Turn closureImplements$... functions into domain functions * Simplify preconditions for closureCall$ of closure obtained from function literal * Refactor following advice in the comments, fix error message for closure calls * Implement suggestions * Add comment from suggestion Co-authored-by: Felix Wolf <[email protected]> * Add suggested `Experimental feature` warning Co-authored-by: Felix Wolf <[email protected]> * Ensure that the Closure domain is only generated if there are closures Co-authored-by: Stefano Milizia <[email protected]> Co-authored-by: Felix Wolf <[email protected]>
viperproject · Aug 2, 2022 · 7294137 · 7294137
1 parent 3619330
commit 7294137
Show file tree

Hide file tree

Showing 81 changed files with 7,475 additions and 3,390 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -30,6 +30,7 @@ INV         : 'invariant';
 DEC         : 'decreases' -> mode(NLSEMI);
 PURE        : 'pure' -> mode(NLSEMI);
 IMPL        : 'implements';
+AS          : 'as';
 OLD         : 'old'-> mode(NLSEMI);
 BEFORE      : 'before'-> mode(NLSEMI);
 LHS         : '#lhs';
@@ -78,4 +79,5 @@ PREDICATE   : 'predicate';
 WRITEPERM   : 'writePerm' -> mode(NLSEMI);
 NOPERM      : 'noPerm' -> mode(NLSEMI);
 TRUSTED     : 'trusted' -> mode(NLSEMI);
-OUTLINE     : 'outline';
+OUTLINE     : 'outline';
+PROOF       : 'proof';
diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -155,6 +155,15 @@ assertion:
 
 blockWithBodyParameterInfo: L_CURLY (SHARE identifierList eos)? statementList? R_CURLY;
 
+// Closures
+closureSpecInstance: (qualifiedIdent | IDENTIFIER) (L_CURLY (closureSpecParams COMMA?)? R_CURLY)?;
+
+closureSpecParams: closureSpecParam (COMMA closureSpecParam)*;
+
+closureSpecParam: (IDENTIFIER COLON)? expression;
+
+closureImplProofStmt: PROOF expression IMPL closureSpecInstance block;
+
 // Implementation proofs
 implementationProof: type_ IMPL type_ (L_CURLY (implementationProofPredicateAlias eos)* (methodImplementationProof eos)*  R_CURLY)?;
 
@@ -197,7 +206,6 @@ predicateBody: L_CURLY expression eos R_CURLY;
 
 mpredicateDecl: PRED receiver IDENTIFIER parameters predicateBody?;
 
-
 // Addressability
 
 varSpec:
@@ -260,6 +268,7 @@ expression:
     | GREATER
     | GREATER_OR_EQUALS
   ) expression #relExpr
+  | expression IMPL closureSpecInstance #closureImplSpecExpr
   | expression LOGICAL_AND expression #andExpr
   | expression LOGICAL_OR expression #orExpr
   |<assoc=right> expression IMPLIES expression #implication
@@ -289,7 +298,8 @@ statement:
   | switchStmt
   | selectStmt
   | specForStmt
-  | deferStmt;
+  | deferStmt
+  | closureImplProofStmt;
 
 applyStmt: APPLY expression;
 
@@ -328,6 +338,7 @@ primaryExpr:
   | primaryExpr seqUpdExp #seqUpdPrimaryExpr
   | primaryExpr typeAssertion #typeAssertionPrimaryExpr
   | primaryExpr arguments #invokePrimaryExpr
+  | primaryExpr arguments AS closureSpecInstance #invokePrimaryExprWithSpec
   | primaryExpr predConstructArgs #predConstrPrimaryExpr
   | call_op=(
   LEN
@@ -337,6 +348,10 @@ primaryExpr:
   ) L_PAREN expression R_PAREN #builtInCallExpr // Remove this alternative when predeclared functions are properly handled
   ;
 
+functionLit: specification closureDecl[$specification.trusted, $specification.pure];
+
+closureDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER? (signature blockWithBodyParameterInfo?);
+
 predConstructArgs: L_PRED expressionList? COMMA? R_PRED;
 
 // Added predicate spec and method specifications

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
@@ -326,6 +326,34 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitBlockWithBodyParameterInfo(GobraParser.BlockWithBodyParameterInfoContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureSpecInstance(GobraParser.ClosureSpecInstanceContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureSpecParams(GobraParser.ClosureSpecParamsContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureSpecParam(GobraParser.ClosureSpecParamContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureImplProofStmt(GobraParser.ClosureImplProofStmtContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -473,6 +501,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitParameterType(GobraParser.ParameterTypeContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureImplSpecExpr(GobraParser.ClosureImplSpecExprContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -634,6 +669,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitGhostPrimaryExpr_(GobraParser.GhostPrimaryExpr_Context ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitInvokePrimaryExprWithSpec(GobraParser.InvokePrimaryExprWithSpecContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -711,6 +753,20 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitSlicePrimaryExpr(GobraParser.SlicePrimaryExprContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitFunctionLit(GobraParser.FunctionLitContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitClosureDecl(GobraParser.ClosureDeclContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -1327,13 +1383,6 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitEmbeddedField(GobraParser.EmbeddedFieldContext ctx) { return visitChildren(ctx); }
-	/**
-	 * {@inheritDoc}
-	 *
-	 * <p>The default implementation returns the result of calling
-	 * {@link #visitChildren} on {@code ctx}.</p>
-	 */
-	@Override public T visitFunctionLit(GobraParser.FunctionLitContext 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
@@ -283,6 +283,30 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitBlockWithBodyParameterInfo(GobraParser.BlockWithBodyParameterInfoContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#closureSpecInstance}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureSpecInstance(GobraParser.ClosureSpecInstanceContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#closureSpecParams}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureSpecParams(GobraParser.ClosureSpecParamsContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#closureSpecParam}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureSpecParam(GobraParser.ClosureSpecParamContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#closureImplProofStmt}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureImplProofStmt(GobraParser.ClosureImplProofStmtContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#implementationProof}.
 	 * @param ctx the parse tree
@@ -409,6 +433,13 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitParameterType(GobraParser.ParameterTypeContext ctx);
+	/**
+	 * Visit a parse tree produced by the {@code closureImplSpecExpr}
+	 * labeled alternative in {@link GobraParser#expression}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureImplSpecExpr(GobraParser.ClosureImplSpecExprContext ctx);
 	/**
 	 * Visit a parse tree produced by the {@code primaryExpr_}
 	 * labeled alternative in {@link GobraParser#expression}.
@@ -563,6 +594,13 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitGhostPrimaryExpr_(GobraParser.GhostPrimaryExpr_Context ctx);
+	/**
+	 * Visit a parse tree produced by the {@code invokePrimaryExprWithSpec}
+	 * labeled alternative in {@link GobraParser#primaryExpr}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitInvokePrimaryExprWithSpec(GobraParser.InvokePrimaryExprWithSpecContext ctx);
 	/**
 	 * Visit a parse tree produced by the {@code indexPrimaryExpr}
 	 * labeled alternative in {@link GobraParser#primaryExpr}.
@@ -640,6 +678,18 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitSlicePrimaryExpr(GobraParser.SlicePrimaryExprContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#functionLit}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitFunctionLit(GobraParser.FunctionLitContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#closureDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitClosureDecl(GobraParser.ClosureDeclContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#predConstructArgs}.
 	 * @param ctx the parse tree
@@ -1168,12 +1218,6 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitEmbeddedField(GobraParser.EmbeddedFieldContext ctx);
-	/**
-	 * Visit a parse tree produced by {@link GobraParser#functionLit}.
-	 * @param ctx the parse tree
-	 * @return the visitor result
-	 */
-	T visitFunctionLit(GobraParser.FunctionLitContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#index}.
 	 * @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
@@ -150,13 +150,20 @@ case class PConstSpec(typ: Option[PType], right: Vector[PExpression], left: Vect
 
 case class PVarDecl(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId], addressable: Vector[Boolean]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration
 
+sealed trait PFunctionOrClosureDecl extends PScope {
+  def args: Vector[PParameter]
+  def result: PResult
+  def spec: PFunctionSpec
+  def body: Option[(PBodyParameterInfo, PBlock)]
+}
+
 case class PFunctionDecl(
                           id: PIdnDef,
                           args: Vector[PParameter],
                           result: PResult,
                           spec: PFunctionSpec,
                           body: Option[(PBodyParameterInfo, PBlock)]
-                        ) extends PActualMember with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember
+                        ) extends PFunctionOrClosureDecl with PActualMember with PCodeRootWithResult with PWithBody with PGhostifiableMember
 
 case class PMethodDecl(
                         id: PIdnDef,
@@ -416,9 +423,32 @@ case class PExpCompositeVal(exp: PExpression) extends PCompositeVal // exp is ne
 
 case class PLitCompositeVal(lit: PLiteralValue) extends PCompositeVal
 
-case class PFunctionLit(args: Vector[PParameter], result: PResult, body: PBlock) extends PLiteral with PCodeRootWithResult with PScope
+case class PFunctionLit(id: Option[PIdnDef], decl: PClosureDecl) extends PLiteral {
+  val args: Vector[PParameter] = decl.args
+  val result: PResult = decl.result
+  val spec: PFunctionSpec = decl.spec
+  val body: Option[(PBodyParameterInfo, PBlock)] = decl.body
+}
+
+case class PClosureDecl(args: Vector[PParameter],
+                  result: PResult,
+                  spec: PFunctionSpec,
+                  body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithResult with PActualMisc
 
-case class PInvoke(base: PExpressionOrType, args: Vector[PExpression]) extends PActualExpression
+case class PClosureSpecInstance(func: PNameOrDot, params: Vector[PKeyedElement]) extends PGhostMisc {
+  require(params.forall(p => p.exp.isInstanceOf[PExpCompositeVal]))
+  require(params.forall(p => p.key.isEmpty || p.key.get.isInstanceOf[PIdentifierKey]))
+  val paramKeys: Vector[String] = params.collect{ case PKeyedElement(Some(PIdentifierKey(id)), _) => id.name }
+  val paramExprs: Vector[PExpression] = params.collect{ case PKeyedElement(_, PExpCompositeVal(exp)) => exp }
+}
+
+case class PClosureImplements(closure: PExpression, spec: PClosureSpecInstance) extends PGhostExpression
+
+case class PClosureImplProof(impl: PClosureImplements, block: PBlock) extends PGhostStatement with PScope
+
+case class PInvoke(base: PExpressionOrType, args: Vector[PExpression], spec: Option[PClosureSpecInstance]) extends PActualExpression {
+  require(base.isInstanceOf[PExpression] || spec.isEmpty) // `base` is a type for conversions only, for which `spec` is empty
+}
 
 // TODO: Check Arguments in language specification, also allows preceding type
 

diff --git a/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala b/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala
@@ -32,7 +32,18 @@ object AstPattern {
   case class Deref(base: PExpression) extends Expr
   case class FieldSelection(base: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.StructMember) extends Expr with Symbolic
   case class Conversion(typ: PType, arg: PExpression) extends Expr
-  case class FunctionCall(callee: FunctionKind, args: Vector[PExpression]) extends Expr
+
+  sealed trait FunctionLikeCall extends Expr {
+    def args: Vector[PExpression]
+    def maybeSpec: Option[PClosureSpecInstance]
+  }
+  case class FunctionCall(callee: FunctionKind, args: Vector[PExpression]) extends FunctionLikeCall {
+    override def maybeSpec: Option[PClosureSpecInstance] = None
+  }
+  case class ClosureCall(callee: PExpression, args: Vector[PExpression], spec: PClosureSpecInstance) extends FunctionLikeCall {
+    override def maybeSpec: Option[PClosureSpecInstance] = Some(spec)
+  }
+
   case class IndexedExp(base : PExpression, index : PExpression) extends Expr
   case class BlankIdentifier(decl: PBlankIdentifier) extends Expr
 
@@ -41,6 +52,7 @@ object AstPattern {
   }
 
   case class Function(id: PIdnUse, symb: st.Function) extends FunctionKind with Symbolic
+  case class Closure(id: PIdnUse, symb: st.Closure) extends FunctionKind with Symbolic
   case class DomainFunction(id: PIdnUse, symb: st.DomainFunction) extends FunctionKind with Symbolic
   case class ReceivedMethod(recv: PExpression, id: PIdnUse, path: Vector[MemberPath], symb: st.Method) extends FunctionKind with Symbolic
   case class ImplicitlyReceivedInterfaceMethod(id: PIdnUse, symb: st.MethodSpec) extends FunctionKind with Symbolic // for method references withing an interface definition