safety commit

build.sbt

@@ -34,7 +34,7 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
-    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0",
+    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0",
     libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT
 
     scalacOptions ++= Seq(

src/main/antlr4/GobraLexer.g4

@@ -74,6 +74,7 @@ PRED        : 'pred';
 TYPE_OF      : 'typeOf'-> mode(NLSEMI);
 IS_COMPARABLE: 'isComparable'-> mode(NLSEMI);
 LOW         : 'low'-> mode(NLSEMI);
+LOWC        : 'lowContext'-> mode(NLSEMI);
 SHARE       : 'share';
 ADDR_MOD    : '@'-> mode(NLSEMI);
 DOT_DOT     : '..';

src/main/antlr4/GobraParser.g4

@@ -83,6 +83,7 @@ ghostPrimaryExpr: range
   | typeExpr
   | isComparable
   | low
+  | lowc
   | old
   | before
   | sConversion
@@ -129,6 +130,8 @@ isComparable: IS_COMPARABLE L_PAREN expression R_PAREN;
 
 low: LOW L_PAREN expression R_PAREN;
 
+lowc: LOWC L_PAREN R_PAREN;
+
 typeOf: TYPE_OF L_PAREN expression R_PAREN;
 
 access: ACCESS L_PAREN expression (COMMA expression)? R_PAREN;

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

@@ -271,6 +271,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitLow(GobraParser.LowContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitLowc(GobraParser.LowcContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

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

@@ -236,6 +236,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitLow(GobraParser.LowContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#lowc}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitLowc(GobraParser.LowcContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#typeOf}.
 	 * @param ctx the parse tree

src/main/resources/stubs/sync/mutex.gobra

@@ -22,10 +22,12 @@ ensures m.LockP() && m.LockInv() == inv
 decreases
 func (m *Mutex) SetInv(ghost inv pred())
 
+requires lowContext()
 requires acc(m.LockP(), _)
 ensures m.LockP() && m.UnlockP() && m.LockInv()()
 func (m *Mutex) Lock()
 
+requires lowContext()
 requires acc(m.LockP(), _) && m.UnlockP() && m.LockInv()()
 ensures m.LockP()
 decreases

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

@@ -1043,6 +1043,8 @@ case class PIsComparable(exp: PExpressionOrType) extends PGhostExpression
 
 case class PLow(exp: PExpression) extends PGhostExpression
 
+case class PLowContext() extends PGhostExpression
+
 case class PMagicWand(left: PExpression, right: PExpression) extends PGhostExpression
 
 /* ** Option types */

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

@@ -528,6 +528,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PIsComparable(exp) => "isComparable" <> parens(showExprOrType(exp))
 
       case PLow(exp) => "low" <> parens(showExpr(exp))
+      case _: PLowContext => "low_context"
 
       case POptionNone(t) => "none" <> brackets(showType(t))
       case POptionSome(e) => "some" <> parens(showExpr(e))

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

@@ -563,6 +563,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case DefinedTExpr(name) => name
 
     case Low(exp) => "low" <> parens(showExpr(exp))
+    case LowContext() => "low_context"
 
     case DfltVal(typ) => "dflt" <> brackets(showType(typ))
     case Tuple(args) => parens(showExprList(args))

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -646,6 +646,10 @@ case class Low(exp: Expr)(val info: Source.Parser.Info) extends Expr {
   override val typ: Type = BoolT(Addressability.rValue)
 }
 
+case class LowContext()(val info: Source.Parser.Info) extends Expr {
+  override val typ: Type = BoolT(Addressability.rValue)
+}
+
 /* ** Higher-order predicate expressions */
 
 case class PredicateConstructor(proxy: PredicateProxy, proxyT: PredT, args: Vector[Option[Expr]])(val info: Source.Parser.Info) extends Expr {

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

@@ -4299,6 +4299,7 @@ object Desugar extends LazyLogging {
         }
 
         case PLow(exp) => for { wExp <- go(exp) } yield in.Low(wExp)(src)
+        case PLowContext() => unit(in.LowContext()(src))
 
         case PIn(left, right) => for {
           dleft <- go(left)

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

@@ -1391,6 +1391,12 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     case Vector("low", "(", expr: PExpression, ")") => PLow(expr)
   }
 
+  /**
+    */
+  override def visitLowc(ctx: LowcContext): AnyRef = super.visitLowc(ctx) match {
+    case Vector("lowContext",  "(", ")") => PLowContext()
+  }
+
 
   /**
     * Visits the rule

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

@@ -102,7 +102,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
       case _: PConditional | _: PImplication | _: PForall | _: PExists => AddrMod.rValue
       case _: PAccess | _: PPredicateAccess | _: PMagicWand => AddrMod.rValue
       case _: PClosureImplements => AddrMod.rValue
-      case _: PTypeOf | _: PIsComparable | _: PLow => AddrMod.rValue
+      case _: PTypeOf | _: PIsComparable | _: PLow | _: PLowContext => AddrMod.rValue
       case _: PIn | _: PMultiplicity | _: PSequenceAppend |
            _: PGhostCollectionExp | _: PRangeSequence | _: PUnion | _: PIntersection |
            _: PSetMinus | _: PSubset | _: PMapKeys | _: PMapValues => AddrMod.rValue

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -146,7 +146,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
         case Some(p: ap.AdtClause) =>
           val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ))
-          AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, this)
+          AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, p.symb.context)
         case Some(p: ap.AdtField) =>
           p.symb match {
             case AdtDestructor(decl, _, context) => context.symbType(decl.typ)

src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala

@@ -158,7 +158,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
       // ADT clause is special since it is a type with a name that is not a named type
       case a: AdtClause =>
         val fields = a.fields.map(f => f.id.name -> a.context.symbType(f.typ))
-        AdtClauseT(fields.toMap, fields.map(_._1), a.decl, a.adtDecl, this)
+        AdtClauseT(fields.toMap, fields.map(_._1), a.decl, a.adtDecl, a.context)
 
       case BuiltInType(tag, _, _) => tag.typ
       case _ => violation(s"expected type, but got $id")

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -108,6 +108,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     }
 
     case PLow(e) => isExpr(e).out
+    case _: PLowContext => noMessages
 
     case n: PGhostEquals =>
       val lType = typ(n.left)
@@ -251,7 +252,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PTypeExpr => SortT
     case _: PIsComparable => BooleanT
 
-    case _: PLow => BooleanT
+    case _: PLow | _: PLowContext => BooleanT
     case _: PGhostEquals | _: PGhostUnequals => BooleanT
 
     case POptionNone(t) => OptionT(typeSymbType(t))
@@ -453,6 +454,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case n: PIsComparable => asExpr(n.exp).forall(go)
 
       case n: PLow => go(n.exp)
+      case _: PLowContext => true
 
       case PCompositeLit(typ, _) => typ match {
         case _: PArrayType | _: PImplicitSizeArrayType => !strong

src/main/scala/viper/gobra/translator/Translator.scala

@@ -40,7 +40,7 @@ object Translator {
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
       new TerminationTransformer,
-      // new SIFTransformer
+      new SIFTransformer
     )
 
     val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {

src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala

@@ -10,7 +10,7 @@ import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.translator.encodings.combinators.Encoding
 import viper.gobra.translator.context.Context
-import viper.gobra.translator.transformers.hyper.SIFLowExp
+import viper.gobra.translator.transformers.hyper.{SIFLowExp, SIFLowEventExp}
 import viper.gobra.translator.util.ViperWriter.CodeWriter
 import viper.gobra.util.Violation
 import viper.gobra.translator.util.{ViperUtil => vu}
@@ -64,6 +64,7 @@ class AssertionEncoding extends Encoding {
       } yield withSrc(vpr.Let(l, r, exp), let)
 
     case n@ in.Low(e) => for {arg <- ctx.expression(e) } yield withSrc(SIFLowExp(arg), n)
+    case n: in.LowContext => unit(withSrc(SIFLowEventExp(), n))
   }
 
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {