atomic methods and invariants

src/main/antlr4/GobraLexer.g4

@@ -99,7 +99,10 @@ GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
 OPAQUE      : 'opaque' -> mode(NLSEMI);
 MAYINIT     : 'mayInit' -> mode(NLSEMI);
+ATOMIC      : 'atomic' -> mode(NLSEMI);
 REVEAL      : 'reveal';
 BACKEND     : '#backend';
+CRITICAL    : 'critical';
+OPENSINV    : 'opensInvariants' -> mode(NLSEMI);
 FRIENDPKG   : 'friendPkg';
 // NOTE: if you append a new token, do not forget to update InformativeErrorListener.LAST_GOBRA_TOKEN

src/main/antlr4/GobraParser.g4

@@ -180,9 +180,9 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 
 // Specifications
 
-specification returns[boolean trusted = false, boolean pure = false, boolean mayInit = false, boolean opaque = false;]:
+specification returns[boolean trusted = false, boolean pure = false, boolean mayInit = false, boolean opensInv = false, boolean atomic = false, boolean opaque = false;]:
   // Non-greedily match PURE to avoid missing eos errors.
-  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | MAYINIT {$mayInit = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
+  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | OPENSINV {$opensInv = true;} |  MAYINIT {$mayInit = true;} | ATOMIC {$atomic = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? (ATOMIC {$atomic = true;})? backendAnnotation?
   ;
 
 backendAnnotationEntry: ~('('|')'|',')+;
@@ -364,8 +364,11 @@ statement:
   | selectStmt
   | specForStmt
   | deferStmt
+  | criticalStmt
   | closureImplProofStmt;
 
+criticalStmt: CRITICAL expression L_PAREN statementList? R_PAREN;
+
 applyStmt: APPLY expression;
 
 packageStmt: PACKAGE expression block?;

src/main/resources/builtin/builtin.gobra

@@ -40,3 +40,9 @@ type error interface {
 // a correct program must never call it.
 requires false
 func panic(v interface{})
+
+ghost
+requires p()
+ensures  Invariant(p)
+decreases
+func EstablishInvariant(p pred())

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

@@ -325,6 +325,8 @@ case class PBlock(stmts: Vector[PStatement]) extends PActualStatement with PScop
   }
 }
 
+case class PCritical(expr: PExpression, stmts: Vector[PStatement]) extends PActualStatement with PGhostifiableStatement
+
 case class PSeq(stmts: Vector[PStatement]) extends PActualStatement with PGhostifiableStatement {
   def nonEmptyStmts: Vector[PStatement] = stmts.filterNot {
     case _: PEmptyStmt => true
@@ -894,6 +896,8 @@ case class PFunctionSpec(
                           isPure: Boolean = false,
                           isTrusted: Boolean = false,
                           isOpaque: Boolean = false,
+                          isAtomic: Boolean = false,
+                          opensInvs: Boolean = false,
                           mayBeUsedInInit: Boolean = false,
                       ) extends PSpecification
 

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

@@ -148,6 +148,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
 
   def showPure: Doc = "pure" <> line
   def showOpaque: Doc = "opaque" <> line
+  def showOpensInvs: Doc = "opensInvariants" <> line
+  def showAtomic: Doc = "atomic" <> line
   def showTrusted: Doc = "trusted" <> line
   def showMayInit: Doc = "mayInit" <> line
   def showPre(pre: PExpression): Doc = "requires" <+> showExpr(pre)
@@ -164,11 +166,13 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showSpec(spec: PSpecification): Doc = spec match {
-    case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, mayInit) =>
+    case PFunctionSpec(pres, preserves, posts, measures, backendAnnotations, isPure, isTrusted, isOpaque, isAtomic, opensInvs, mayInit) =>
       (if (isPure) showPure else emptyDoc) <>
       (if (isOpaque) showOpaque else emptyDoc) <>
+      (if (opensInvs) showOpensInvs else emptyDoc) <>
       (if (isTrusted) showTrusted else emptyDoc) <>
       (if (mayInit) showMayInit else emptyDoc) <>
+      (if (isAtomic) showAtomic else emptyDoc) <>
       hcat(pres map (showPre(_) <> line)) <>
       hcat(preserves map (showPreserves(_) <> line)) <>
       hcat(posts map (showPost(_) <> line)) <>
@@ -300,6 +304,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PBlock(stmts) => block(showStmtList(stmts))
       case PSeq(stmts) => showStmtList(stmts)
       case POutline(body, spec) => showSpec(spec) <> "outline" <> parens(nest(line <> showStmt(body)) <> line)
+      case PCritical(expr, stmts) =>
+        "critical" <> showExpr(expr) <> parens(nest(line <> showStmtList(stmts)) <> line)
       case PClosureImplProof(impl, PBlock(stmts)) => "proof" <+> showExpr(impl) <> block(showStmtList(stmts))
     }
     case statement: PGhostStatement => statement match {

src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala

@@ -9,7 +9,7 @@ package viper.gobra.ast.internal.transform
 import viper.gobra.ast.internal._
 import viper.gobra.reporting.Source
 import viper.gobra.reporting.Source.OverflowCheckAnnotation
-import viper.gobra.reporting.Source.Parser.Single
+import viper.gobra.reporting.Source.Parser.{Internal, Single}
 import viper.gobra.util.TypeBounds.BoundedIntegerKind
 import viper.gobra.util.Violation.violation
 
@@ -192,6 +192,8 @@ object OverflowChecksTransform extends InternalTransform {
   private def createAnnotatedInfo(info: Source.Parser.Info): Source.Parser.Info =
     info match {
       case s: Single => s.createAnnotatedInfo(OverflowCheckAnnotation)
+      // the following is temporary hack that will be discarded when we merge the new support for overflow checking
+      case i@ Internal => i
       case i => violation(s"l.op.info ($i) is expected to be a Single")
     }
 }

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -7,7 +7,7 @@
 package viper.gobra.frontend
 
 import com.typesafe.scalalogging.LazyLogging
-import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _}
+import viper.gobra.ast.frontend.{AstPattern => ap, _}
 import viper.gobra.ast.{internal => in}
 import viper.gobra.frontend.PackageResolver.RegularImport
 import viper.gobra.frontend.Source.TransformableSource
@@ -16,7 +16,7 @@ import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.base.{BuiltInMemberTag, Type, SymbolTable => st}
 import viper.gobra.frontend.info.implementation.resolution.MemberPath
 import viper.gobra.frontend.info.{ExternalTypeInfo, TypeInfo}
-import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstablished, MainPreNotEstablished}
+import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstablished, InvariantMightBeOpenAnnotation, InvariantNotRestoredAnnotation, IsInvariantAnnotation, MainPreNotEstablished}
 import viper.gobra.reporting.{DesugaredMessage, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
@@ -526,6 +526,13 @@ object Desugar extends LazyLogging {
       in.GlobalVarProxy(v.id.name, name)(meta(v.decl, v.context.getTypeInfo))
     }
 
+    def openInvsVar : in.LocalVar =
+      in.LocalVar(
+        "openInvariants",
+        in.SetT(
+          in.PredT(Vector.empty, Addressability.exclusiveVariable),
+          Addressability.exclusiveVariable))(Source.Parser.Internal)
+
     def constDeclD(block: PConstDecl): Vector[in.GlobalConstDecl] = block.specs.flatMap(constSpecD)
 
     def constSpecD(decl: PConstSpec): Vector[in.GlobalConstDecl] = decl.left.flatMap(l => info.regular(l) match {
@@ -692,7 +699,7 @@ object Desugar extends LazyLogging {
       val capturedWithAliases = (captured.map { v => in.Ref(localVarD(outerCtx, info)(v))(meta(v, info)) } zip capturedPar)
 
       val bodyOpt = decl.body.map{ case (_, s) =>
-        val vars = argSubs.flatten ++ capturedSubs ++ returnSubs.flatten
+        val vars = argSubs.flatten ++ capturedSubs ++ returnSubs.flatten ++ Vector(openInvsVar)
         val varsInit = vars map (v => in.Initialization(v)(v.info))
         val body = varsInit ++ argInits ++ capturedInits ++ Vector(blockD(ctx, info)(s))
         in.MethodBody(vars, in.MethodBodySeqn(body)(fsrc), resultAssignments)(fsrc)
@@ -890,7 +897,7 @@ object Desugar extends LazyLogging {
 
 
       val bodyOpt = decl.body.map{ case (_, s) =>
-        val vars = recvSub.toVector ++ argSubs.flatten ++ returnSubs.flatten
+        val vars = recvSub.toVector ++ argSubs.flatten ++ returnSubs.flatten ++ Vector(openInvsVar)
         val varsInit = vars map (v => in.Initialization(v)(v.info))
         val body = varsInit ++ recvInits ++ argInits ++ Vector(blockD(ctx, info)(s))
         in.MethodBody(vars, in.MethodBodySeqn(body)(fsrc), resultAssignments)(fsrc)
@@ -1587,6 +1594,19 @@ object Desugar extends LazyLogging {
           case n@PForStmt(pre, cond, post, spec, body) =>
             unit(block( // is a block because 'pre' might define new variables
               for {
+                oldOpenInvs <- freshDeclaredExclusiveVar(
+                  in.SetT(in.PredT(Vector.empty, Addressability.Exclusive), Addressability.Exclusive), n, info
+                )(src)
+                initOldOpenInvs = in.SingleAss(in.Assignee.Var(oldOpenInvs), openInvsVar)(src)
+                // This invariant allows for loops that open critical regions without havocking the value
+                // of openInvs, which would prevent opening invariants in the body of the loop or after the loop.
+                // This invariant does not impose any restrictions on the user, given that the syntax of critical
+                // regions guarantees that no invariant may be open for longer than one loop iteration.
+                // TODO: do the same for range loops
+                openInvsDoesNotChange: in.Assertion = in.ExprAssertion(
+                  in.EqCmp(oldOpenInvs, openInvsVar)(src)
+                )(src)
+
                 dPre <- maybeStmtD(ctx)(pre)(src)
                 (dCondPre, dCond) <- prelude(exprD(ctx, info)(cond))
                 (dInvPre, dInv) <- prelude(sequence(spec.invariants map assertionD(ctx, info)))
@@ -1605,8 +1625,8 @@ object Desugar extends LazyLogging {
                 dPost <- maybeStmtD(ctx)(post)(src)
 
                 wh = in.Seqn(
-                  Vector(dPre) ++ dCondPre ++ dInvPre ++ dTerPre ++ Vector(
-                    in.While(dCond, dInv, dTer, in.Block(Vector(continueLoopLabelProxy),
+                  Vector(initOldOpenInvs, dPre) ++ dCondPre ++ dInvPre ++ dTerPre ++ Vector(
+                    in.While(dCond, openInvsDoesNotChange +: dInv, dTer, in.Block(Vector(continueLoopLabelProxy),
                       Vector(dBody, continueLoopLabel, dPost) ++ dCondPre ++ dInvPre ++ dTerPre
                     )(src))(src), breakLoopLabel
                   )
@@ -1903,6 +1923,91 @@ object Desugar extends LazyLogging {
               } yield in.Outline(name, pres, posts, terminationMeasures, annotations, dummyBody, trusted = true)(src)
             }
 
+          case n@PCritical(expr, stmts) =>
+            val exprSrc: Meta = meta(expr, info)
+            val exprSrcIsInv = meta(expr, info).createAnnotatedInfo(IsInvariantAnnotation())
+            val exprSrcIsOpen = meta(expr, info).createAnnotatedInfo(InvariantMightBeOpenAnnotation())
+            val exprSrcNotRestored = meta(expr, info).createAnnotatedInfo(InvariantNotRestoredAnnotation())
+
+            for {
+              e <- goE(expr)
+
+              // check if the invariant is an invariant
+              isInv = in.Assert(
+                in.ExprAssertion(
+                  in.PureFunctionCall(
+                    functionProxy(InvariantFunctionTag, Vector(e.typ))(exprSrcIsInv),
+                    Vector(e),
+                    in.BoolT(Addressability.Exclusive),
+                    false
+                  )(exprSrcIsInv)
+                )(exprSrcIsInv)
+              )(exprSrcIsInv)
+              _ <- write(isInv)
+
+              // check the invariant is not open yet
+              checkIsOpen = in.Assert(
+                in.ExprAssertion(
+                  in.Negation(
+                    in.Contains(
+                      e,
+                      openInvsVar
+                    )(exprSrcIsOpen)
+                  )(exprSrcIsOpen)
+                )(exprSrcIsOpen)
+              )(exprSrcIsOpen)
+              _ <- write(checkIsOpen)
+
+              // mark invariant as open
+              markOpen = in.SingleAss(
+                in.Assignee.Var(openInvsVar),
+                in.Union(
+                  openInvsVar,
+                  in.SetLit(
+                    in.PredT(Vector.empty, Addressability.Exclusive),
+                    Vector(e)
+                  )(exprSrc),
+                  in.PredT(Vector.empty, Addressability.Exclusive)
+                )(exprSrc)
+              )(exprSrc)
+              _ <- write(markOpen)
+
+              // inhale the invariant
+              inhaleInv = in.Inhale(
+                in.Access(
+                  in.Accessible.PredExpr(in.PredExprInstance(e, Vector.empty)(exprSrc)),
+                  in.FullPerm(exprSrc)
+                )(exprSrc)
+              )(exprSrc)
+              _ <- write(inhaleInv)
+
+              // stmts
+              stmtsD <- sequence(stmts.map(goS))
+              _ <- write(stmtsD : _*)
+
+              // exhale the invariant
+              exhaleInv = in.Exhale(
+                in.Access(
+                  in.Accessible.PredExpr(in.PredExprInstance(e, Vector.empty)(exprSrcNotRestored)),
+                  in.FullPerm(exprSrcNotRestored)
+                )(exprSrcNotRestored)
+              )(exprSrcNotRestored)
+
+              // mark invariant as closed
+              markClosed = in.SingleAss(
+                in.Assignee.Var(openInvsVar),
+                in.SetMinus(
+                  openInvsVar,
+                  in.SetLit(
+                    in.PredT(Vector.empty, Addressability.Exclusive),
+                    Vector(e)
+                  )(exprSrc),
+                  in.PredT(Vector.empty, Addressability.Exclusive)
+                )(exprSrc)
+              )(exprSrc)
+              _ <- write(markClosed)
+
+            } yield exhaleInv
 
           case n@PContinue(label) => unit(in.Continue(label.map(x => x.name), nm.fetchContinueLabel(n, info))(src))
 
@@ -3704,7 +3809,7 @@ object Desugar extends LazyLogging {
         backendAnnotations = Vector.empty,
         body = Some(
           in.MethodBody(
-            decls = Vector(),
+            decls = Vector(openInvsVar),
             postprocessing = Vector(),
             seqn = in.MethodBodySeqn{
               // Init all global variables declared in the file (not all declarations in the package!).
@@ -4823,7 +4928,7 @@ object Desugar extends LazyLogging {
           unit(in.MPredicateAccess(implicitThisD(recvType)(src), proxy, convertArgs(dArgs))(src))
 
         case b: ap.BuiltInPredicate =>
-          val fproxy = fpredicateProxy(b.id, info)
+          val fproxy = fpredicateProxy(b.symb.tag, convertArgs(dArgs).map(_.typ))(src)
           unit(in.FPredicateAccess(fproxy, convertArgs(dArgs))(src))
 
         case b: ap.BuiltInReceivedPredicate =>

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -926,6 +926,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       isPure = ctx.pure,
       isTrusted = ctx.trusted,
       isOpaque = ctx.opaque,
+      isAtomic = ctx.atomic,
+      opensInvs = ctx.opensInv,
       mayBeUsedInInit = ctx.mayInit,
     )
   }
@@ -2184,6 +2186,11 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     */
   override def visitGotoStmt(ctx: GotoStmtContext): PGoto = PGoto(visitLabelUse(ctx.IDENTIFIER())).at(ctx)
 
+  override def visitCriticalStmt(ctx: CriticalStmtContext): PCritical = {
+    val e = visit(ctx.expression()).asInstanceOf[PExpression]
+    val l = visitStatementList(ctx.statementList())
+    PCritical(e, l).at(ctx)
+  }
 
   /**
     * Fallthrough

src/main/scala/viper/gobra/frontend/info/base/BuiltInMemberTag.scala

@@ -214,6 +214,13 @@ object BuiltInMemberTag {
     override def isPure: Boolean = false
   }
 
+  case object InvariantFunctionTag extends BuiltInFunctionTag {
+    override def identifier: String = "Invariant"
+    override def name: String = "InvariantTag"
+    override def ghost: Boolean = true
+    override def isPure: Boolean = true
+  }
+
   /** Built-in FPredicate Tags */
 
   case object PredTrueFPredTag extends BuiltInFPredicateTag {
@@ -222,7 +229,6 @@ object BuiltInMemberTag {
     override def isAbstract: Boolean = false
   }
 
-
   /** Built-in Method Tags */
   case object BufferSizeMethodTag extends BuiltInMethodTag with GhostBuiltInMember {
     override def identifier: String = "BufferSize"
@@ -347,6 +353,7 @@ object BuiltInMemberTag {
     CopyFunctionTag,
     // fpredicates
     PredTrueFPredTag,
+    InvariantFunctionTag,
     // methods
     BufferSizeMethodTag,
     SendGivenPermMethodTag,

src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala

@@ -182,21 +182,25 @@ object SymbolTable extends Environments[Entity] {
 
   sealed trait Method extends MethodLike with ActualTypeMember with WithResult {
     def isPure: Boolean
+    def isAtomic: Boolean
   }
 
   case class MethodImpl(decl: PMethodDecl, ghost: Boolean, context: ExternalTypeInfo) extends Method {
     override def rep: PNode = decl
     override def isPure: Boolean = decl.spec.isPure
     override val args: Vector[PParameter] = decl.args
     override val result: PResult = decl.result
+    override val isAtomic: Boolean = decl.spec.isAtomic
     def isOpaque: Boolean = decl.spec.isOpaque
+
   }
 
   case class MethodSpec(spec: PMethodSig, itfDef: PInterfaceType, ghost: Boolean, context: ExternalTypeInfo) extends Method {
     override def rep: PNode = spec
     override def isPure: Boolean = spec.spec.isPure
     override val args: Vector[PParameter] = spec.args
     override def result: PResult = spec.result
+    override val isAtomic: Boolean = spec.spec.isAtomic
     val itfType: Type.InterfaceT = Type.InterfaceT(itfDef, context)
   }
 

src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala

@@ -77,6 +77,13 @@ trait Implements { this: TypeInfoImpl =>
                     }
                   }) {
                     Vector(s"For member $name, the 'pure' annotation for implementation and interface does not match")
+                  } else if ({
+                    (implMember, itfMember) match {
+                      case (implMember: Method, itfMember: Method) => itfMember.isAtomic && !implMember.isAtomic
+                      case _ => false
+                    }
+                  }){
+                    Vector(s"The implementation of atomic method $name is not marked as atomic")
                   } else {
                     Vector.empty
                   }