Private Specification, Partial Struct Encoding, and Constructor

src/main/antlr4/GobraLexer.g4

@@ -2,7 +2,7 @@
 // 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.
+// Copyright (c) 2011-2023 ETH Zurich.
 
 lexer grammar GobraLexer;
 import GoLexer;
@@ -78,6 +78,7 @@ DOT_DOT     : '..';
 SHARED      : 'shared';
 EXCLUSIVE   : 'exclusive';
 PREDICATE   : 'predicate';
+PRIVATE     : 'private';
 WRITEPERM   : 'writePerm' -> mode(NLSEMI);
 NOPERM      : 'noPerm' -> mode(NLSEMI);
 TRUSTED     : 'trusted' -> mode(NLSEMI);
@@ -88,3 +89,6 @@ PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
+CONSTRUCT   : 'construct';
+DEREF       : 'deref';
+ASSIGN_STRUCT : 'assign';

src/main/antlr4/GobraParser.g4

@@ -2,7 +2,7 @@
 // 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.
+// Copyright (c) 2011-2023 ETH Zurich.
 
 parser grammar GobraParser;
 import GoParser;
@@ -164,13 +164,20 @@ specStatement
   | kind=PRESERVES assertion
   | kind=POST assertion
   | kind=DEC terminationMeasure
+  | kind=PRIVATE privateSpec
   ;
+
 terminationMeasure: expressionList? (IF expression)?;
 
 assertion:
   | expression
   ;
 
+// Private specification
+privateSpec: L_CURLY ((specStatement eos)*? privateEntailmentProof?)? R_CURLY;
+
+privateEntailmentProof: PROOF block eos;
+
 matchStmt: MATCH expression L_CURLY matchStmtClause* R_CURLY;
 matchStmtClause: matchCase COLON statementList?;
 
@@ -220,7 +227,13 @@ new_: NEW L_PAREN type_ R_PAREN;
 
 // Added specifications and parameter info
 
-specMember: specification (functionDecl[$specification.trusted, $specification.pure] | methodDecl[$specification.trusted, $specification.pure]);
+specMember: specification (
+  functionDecl[$specification.trusted, $specification.pure] 
+  | methodDecl[$specification.trusted, $specification.pure] 
+  | constructDecl
+  | derefDecl[$specification.pure]
+  | assignDecl
+  );
 
 functionDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
 
@@ -236,6 +249,14 @@ predicateBody: L_CURLY expression eos R_CURLY;
 
 mpredicateDecl: PRED receiver IDENTIFIER parameters predicateBody?;
 
+// Struct Constructor
+constructDecl: CONSTRUCT AMPERSAND? type_ (signature blockWithBodyParameterInfo?);
+// Struct Dereference
+derefDecl[boolean pure]: DEREF AMPERSAND? type_ (signature blockWithBodyParameterInfo?);
+// Struct Assignment
+assignDecl: ASSIGN_STRUCT AMPERSAND? type_ (signature blockWithBodyParameterInfo?);
+
+
 // Addressability
 
 varSpec:

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -382,6 +382,20 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitAssertion(GobraParser.AssertionContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitPrivateSpec(GobraParser.PrivateSpecContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitPrivateEntailmentProof(GobraParser.PrivateEntailmentProofContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -564,6 +578,27 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitMpredicateDecl(GobraParser.MpredicateDeclContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitConstructDecl(GobraParser.ConstructDeclContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitDerefDecl(GobraParser.DerefDeclContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitAssignDecl(GobraParser.AssignDeclContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -332,6 +332,18 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitAssertion(GobraParser.AssertionContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#privateSpec}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitPrivateSpec(GobraParser.PrivateSpecContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#privateEntailmentProof}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitPrivateEntailmentProof(GobraParser.PrivateEntailmentProofContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#matchStmt}.
 	 * @param ctx the parse tree
@@ -491,6 +503,24 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitMpredicateDecl(GobraParser.MpredicateDeclContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#constructDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitConstructDecl(GobraParser.ConstructDeclContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#derefDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitDerefDecl(GobraParser.DerefDeclContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#assignDecl}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitAssignDecl(GobraParser.AssignDeclContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#varSpec}.
 	 * @param ctx the parse tree

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -2,7 +2,7 @@
 // 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.
+// Copyright (c) 2011-2023 ETH Zurich.
 
 package viper.gobra.ast.frontend
 
@@ -70,6 +70,7 @@ class PositionManager(val positions: Positions) extends Messaging(positions) {
     messages.sorted map { m =>
       errorFactory(
         formatMessage(m),
+        if (positions.getStart(m.value).isEmpty) None else //TODO: position of private members in private specifications
         Some(translate(positions.getStart(m.value).get, positions.getFinish(m.value).get))
       )
     }
@@ -194,7 +195,39 @@ case class PTypeDef(right: PType, left: PIdnDef) extends PTypeDecl
 
 case class PTypeAlias(right: PType, left: PIdnDef) extends PTypeDecl
 
+sealed trait PConstructor extends PGhostMember with PScope {
+  def typ: PType
+  def spec: PConstructSpec
+}
+
+case class PConstructSpec(
+                      pres: Vector[PExpression],
+                      preserves: Vector[PExpression],
+                      posts: Vector[PExpression],
+                      isShared: Boolean
+                      ) extends PSpecification
 
+case class PConstructDecl(
+                          typ: PType, 
+                          args: Vector[PParameter], 
+                          spec: PConstructSpec,
+                          body: Option[(PBodyParameterInfo, PBlock)]
+                         ) extends PConstructor
+
+case class PDerefDecl(
+                      typ: PType, 
+                      args: Vector[PParameter],
+                      result: PResult, 
+                      spec: PConstructSpec,
+                      body: Option[(PBodyParameterInfo, PBlock)]
+                     ) extends PConstructor with PCodeRootWithResult
+
+case class PAssignDecl(
+                       typ: PType, 
+                       args: Vector[PParameter], 
+                       spec: PConstructSpec, 
+                       body: Option[(PBodyParameterInfo, PBlock)]
+                      ) extends PConstructor
 /**
   * Statements
   */
@@ -867,6 +900,7 @@ case class PFunctionSpec(
                       preserves: Vector[PExpression],
                       posts: Vector[PExpression],
                       terminationMeasures: Vector[PTerminationMeasure],
+                      privateSpec: Option[PPrivateSpec],
                       isPure: Boolean = false,
                       isTrusted: Boolean = false
                       ) extends PSpecification
@@ -887,6 +921,14 @@ case class PLoopSpec(
                     ) extends PSpecification
 
 
+case class PPrivateSpec(
+                       pres: Vector[PExpression],
+                       preserves: Vector[PExpression],
+                       posts: Vector[PExpression],
+                       terminationMeasures: Vector[PTerminationMeasure],
+                       proof: Option[PPrivateEntailmentProof]
+                       ) extends PSpecification
+
 /**
   * Ghost Member
   */
@@ -927,6 +969,8 @@ case class PMethodImplementationProof(
 
 case class PImplementationProofPredicateAlias(left: PIdnUse, right: PNameOrDot) extends PGhostMisc
 
+case class PPrivateEntailmentProof(block: PBlock) extends PGhostStatement with PScope
+
 sealed trait PNameOrDot extends PExpression
 
 /**

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -2,7 +2,7 @@
 // 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.
+// Copyright (c) 2011-2023 ETH Zurich.
 
 package viper.gobra.ast.frontend
 
@@ -113,6 +113,15 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
             if (ip.alias.isEmpty && ip.memberProofs.isEmpty) emptyDoc
             else block(ssep(ip.alias map showMisc, line) <> line <> ssep(ip.memberProofs map showMisc, line))
           )
+      case PConstructDecl(typ, args, spec, body) => 
+        showSpec(spec) <> "construct" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> 
+        parens(showParameterList(args)) <> opt(body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
+      case PDerefDecl(typ, args, _, spec, body) =>
+        showSpec(spec) <> "pure deref" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> 
+        parens(showParameterList(args)) <> opt(body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
+      case PAssignDecl(typ, args, spec, body) =>
+        showSpec(spec) <> "assign" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> 
+        parens(showParameterList(args)) <> opt(body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
     }
   }
 
@@ -132,16 +141,30 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showSpec(spec: PSpecification): Doc = spec match {
-    case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) =>
+    case PFunctionSpec(pres, preserves, posts, measures, privateSpec, isPure, isTrusted) => 
       (if (isPure) showPure 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(measures map (showTerminationMeasure(_) <> line)) <>
+        opt(privateSpec)(showSpec) 
 
     case PLoopSpec(inv, measure) =>
       hcat(inv map (showInv(_) <> line)) <> opt(measure)(showTerminationMeasure) <> line
+
+    case PPrivateSpec(pres, preserves, posts, measures, proof) =>
+      "private" <+> block(
+      hcat(pres map (showPre(_) <> line)) <>
+        hcat(preserves map (showPreserves(_) <> line)) <>
+        hcat(posts map (showPost(_) <> line)) <>
+        hcat(measures map (showTerminationMeasure(_) <> line)) <>
+        opt(proof)(showStmt)) <> line
+
+    case PConstructSpec(pres, preserves, posts, _) => 
+      hcat(pres map (showPre(_) <> line)) <>
+        hcat(preserves map (showPreserves(_) <> line)) <>
+        hcat(posts map (showPost(_) <> line))
   }
 
   def showBodyParameterInfoWithBlock(info: PBodyParameterInfo, block: PBlock): Doc = {
@@ -279,6 +302,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PMatchStatement(exp, clauses, _) => "match" <+>
         showExpr(exp) <+> block(ssep(clauses map showMatchClauseStatement, line))
       case PClosureImplProof(impl, PBlock(stmts)) => "proof" <+> showExpr(impl) <> block(showStmtList(stmts))
+      case PPrivateEntailmentProof(PBlock(stmts)) => "proof" <+> block(showStmtList(stmts))
     }
   }
 
@@ -508,6 +532,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
         case n: PExpression if perm == PFullPerm() => "acc" <> parens(showExpr(n))
         case n: PExpression => "acc" <> parens(showExpr(n) <> "," <+> showExpr(perm))
       }
+
       case PMagicWand(left, right) => showSubExpr(expr, left) <+> "--*" <+> showSubExpr(expr, right)
       case PClosureImplements(closure, spec) => showExpr(closure) <+> "implements" <+> showMisc(spec)
 
@@ -742,6 +767,12 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
         "pred" <+> showReceiver(recv) <+> showId(id) <> parens(showParameterList(args))
       case ip: PImplementationProof =>
         showType(ip.subT) <+> "implements" <+> showType(ip.superT)
+      case PConstructDecl(typ, args, spec, _) => 
+        showSpec(spec) <> "construct" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> parens(showParameterList(args))
+      case PDerefDecl(typ, args, _, spec, _) =>
+        showSpec(spec) <> "pure deref" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> parens(showParameterList(args))
+      case PAssignDecl(typ, args, spec, _) =>
+        showSpec(spec) <> "assign" <+> (if (spec.isShared) "&" else emptyDoc) <> showType(typ) <> parens(showParameterList(args))
     }
   }