safety commit

src/main/antlr4/GobraLexer.g4

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

src/main/antlr4/GobraParser.g4

@@ -78,6 +78,7 @@ ghostPrimaryExpr: range
   | typeOf
   | typeExpr
   | isComparable
+  | low
   | old
   | before
   | sConversion
@@ -122,6 +123,8 @@ before: BEFORE L_PAREN expression R_PAREN;
 
 isComparable: IS_COMPARABLE L_PAREN expression R_PAREN;
 
+low: LOW L_PAREN expression R_PAREN;
+
 typeOf: TYPE_OF L_PAREN expression R_PAREN;
 
 access: ACCESS L_PAREN expression (COMMA expression)? R_PAREN;
@@ -433,13 +436,13 @@ implicitArray: L_BRACKET ELLIPSIS R_BRACKET elementType;
 // distinguish low,high cap
 slice_:
   L_BRACKET (
-    low? COLON high?
-    | low? COLON high COLON cap
+    lowSliceArgument? COLON highSliceArgument?
+    | lowSliceArgument? COLON highSliceArgument COLON capSliceArgument
   ) R_BRACKET;
 
-low : expression;
-high: expression;
-cap: expression;
+lowSliceArgument : expression;
+highSliceArgument: expression;
+capSliceArgument: expression;
 
 
 

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

@@ -1,3 +1,4 @@
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -255,6 +256,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitIsComparable(GobraParser.IsComparableContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitLow(GobraParser.LowContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -968,21 +976,21 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * <p>The default implementation returns the result of calling
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
-	@Override public T visitLow(GobraParser.LowContext ctx) { return visitChildren(ctx); }
+	@Override public T visitLowSliceArgument(GobraParser.LowSliceArgumentContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
 	 * <p>The default implementation returns the result of calling
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
-	@Override public T visitHigh(GobraParser.HighContext ctx) { return visitChildren(ctx); }
+	@Override public T visitHighSliceArgument(GobraParser.HighSliceArgumentContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
 	 * <p>The default implementation returns the result of calling
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
-	@Override public T visitCap(GobraParser.CapContext ctx) { return visitChildren(ctx); }
+	@Override public T visitCapSliceArgument(GobraParser.CapSliceArgumentContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -1529,4 +1537,4 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitEos(GobraParser.EosContext ctx) { return visitChildren(ctx); }
-}
+}

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

@@ -1,3 +1,4 @@
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.9.2
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -223,6 +224,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitIsComparable(GobraParser.IsComparableContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#low}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitLow(GobraParser.LowContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#typeOf}.
 	 * @param ctx the parse tree
@@ -863,23 +870,23 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 */
 	T visitSlice_(GobraParser.Slice_Context ctx);
 	/**
-	 * Visit a parse tree produced by {@link GobraParser#low}.
+	 * Visit a parse tree produced by {@link GobraParser#lowSliceArgument}.
 	 * @param ctx the parse tree
 	 * @return the visitor result
 	 */
-	T visitLow(GobraParser.LowContext ctx);
+	T visitLowSliceArgument(GobraParser.LowSliceArgumentContext ctx);
 	/**
-	 * Visit a parse tree produced by {@link GobraParser#high}.
+	 * Visit a parse tree produced by {@link GobraParser#highSliceArgument}.
 	 * @param ctx the parse tree
 	 * @return the visitor result
 	 */
-	T visitHigh(GobraParser.HighContext ctx);
+	T visitHighSliceArgument(GobraParser.HighSliceArgumentContext ctx);
 	/**
-	 * Visit a parse tree produced by {@link GobraParser#cap}.
+	 * Visit a parse tree produced by {@link GobraParser#capSliceArgument}.
 	 * @param ctx the parse tree
 	 * @return the visitor result
 	 */
-	T visitCap(GobraParser.CapContext ctx);
+	T visitCapSliceArgument(GobraParser.CapSliceArgumentContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#assign_op}.
 	 * @param ctx the parse tree
@@ -1348,4 +1355,4 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitEos(GobraParser.EosContext ctx);
-}
+}

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

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

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

@@ -516,6 +516,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
       case PTypeExpr(typ) => "type" <> brackets(showType(typ))
       case PIsComparable(exp) => "isComparable" <> parens(showExprOrType(exp))
 
+      case PLow(exp) => "low" <> parens(showExpr(exp))
+
       case POptionNone(t) => "none" <> brackets(showType(t))
       case POptionSome(e) => "some" <> parens(showExpr(e))
       case POptionGet(e) => "get" <> parens(showExpr(e))

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

@@ -562,6 +562,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case TupleTExpr(elem) => parens(showExprList(elem))
     case DefinedTExpr(name) => name
 
+    case Low(exp) => "low" <> parens(showExpr(exp))
+
     case DfltVal(typ) => "dflt" <> brackets(showType(typ))
     case Tuple(args) => parens(showExprList(args))
     case Deref(exp, _) => "*" <> showExpr(exp)

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

@@ -640,7 +640,11 @@ case class MathMapTExpr(keys: Expr, elems: Expr)(val info: Source.Parser.Info) e
 case class OptionTExpr(elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class TupleTExpr(elems: Vector[Expr])(val info: Source.Parser.Info) extends TypeExpr
 
+/* ** Information Flow  */
 
+case class Low(exp: Expr)(val info: Source.Parser.Info) extends Expr {
+  override val typ: Type = BoolT(Addressability.rValue)
+}
 
 /* ** Higher-order predicate expressions */
 

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

@@ -4265,6 +4265,8 @@ object Desugar {
           case t => Violation.violation(s"Expected interface or sort type, but got $t")
         }
 
+        case PLow(exp) => for { wExp <- go(exp) } yield in.Low(wExp)(src)
+
         case PIn(left, right) => for {
           dleft <- go(left)
           dright <- go(right)

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

@@ -110,7 +110,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
       case (GobraParser.DECLARE_ASSIGN, _ : TypeSpecContext) => GotAssignErrorType()
       // We expected more tokens inside a slice expression but got a closing bracket: One of the
       // limits must be missing.
-      case (GobraParser.R_BRACKET, expr : ExpressionContext) if expr.parent.isInstanceOf[CapContext] => SliceMissingIndex(3)
+      case (GobraParser.R_BRACKET, expr : ExpressionContext) if expr.parent.isInstanceOf[CapSliceArgumentContext] => SliceMissingIndex(3)
       case _ => DefaultExtraneous()
     }
   }
@@ -128,7 +128,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
       case (Token.EOF, _) => DefaultMismatch()
       // Again, we have an unexpected :=, so suggest using a =
       case (GobraParser.DECLARE_ASSIGN, _) => GotAssignErrorType()
-      case (GobraParser.R_BRACKET, e : ExpressionContext) if e.parent.isInstanceOf[CapContext] => SliceMissingIndex(3)
+      case (GobraParser.R_BRACKET, e : ExpressionContext) if e.parent.isInstanceOf[CapSliceArgumentContext] => SliceMissingIndex(3)
       case _ => DefaultMismatch()
     }
   }
@@ -156,7 +156,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
           case _ => DefaultNoViable(exception)
         }
       }
-      case e: ExpressionContext if e.parent.isInstanceOf[CapContext] => SliceMissingIndex(3)
+      case e: ExpressionContext if e.parent.isInstanceOf[CapSliceArgumentContext] => SliceMissingIndex(3)
       case _ if new_reserved.contains(context.offendingSymbol.getType) => ReservedWord()
       case _ => DefaultNoViable(exception)
     }

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

@@ -1318,9 +1318,9 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     * @param ctx the parse tree
     */
   override def visitSlice_(ctx: Slice_Context): (Option[PExpression], Option[PExpression], Option[PExpression]) = {
-    val low = if (ctx.low() != null) Some(visitNode[PExpression](ctx.low().expression())).pos() else None
-    val high = if (ctx.high() != null) Some(visitNode[PExpression](ctx.high().expression())).pos() else None
-    val cap = if (ctx.cap() != null) Some(visitNode[PExpression](ctx.cap().expression())).pos() else None
+    val low = if (ctx.lowSliceArgument() != null) Some(visitNode[PExpression](ctx.lowSliceArgument().expression())).pos() else None
+    val high = if (ctx.highSliceArgument() != null) Some(visitNode[PExpression](ctx.highSliceArgument().expression())).pos() else None
+    val cap = if (ctx.capSliceArgument() != null) Some(visitNode[PExpression](ctx.capSliceArgument().expression())).pos() else None
     (low, high, cap)
   }
 
@@ -1383,6 +1383,14 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     case Vector("isComparable", "(", e : PExpression, ")") => PIsComparable(e)
   }
 
+  /**
+    * Visits the rule
+    * typeOf: LOW L_PAREN expression R_PAREN;
+    */
+  override def visitLow(ctx: LowContext): AnyRef = super.visitLow(ctx) match {
+    case Vector("low", "(", expr: PExpression, ")") => PLow(expr)
+  }
+
 
   /**
     * 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 => AddrMod.rValue
+      case _: PTypeOf | _: PIsComparable | _: PLow => 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/ghost/GhostExprTyping.scala

@@ -107,6 +107,8 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case t =>  error(n, s"expected interface or type, but got an expression of type $t")
     }
 
+    case PLow(e) => isExpr(e).out
+
     case n: PGhostEquals =>
       val lType = typ(n.left)
       val rType = typ(n.right)
@@ -248,6 +250,8 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case _: PTypeOf => SortT
     case _: PTypeExpr => SortT
     case _: PIsComparable => BooleanT
+
+    case _: PLow => BooleanT
     case _: PGhostEquals | _: PGhostUnequals => BooleanT
 
     case POptionNone(t) => OptionT(typeSymbType(t))
@@ -448,6 +452,8 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case _: PTypeExpr => true
       case n: PIsComparable => asExpr(n.exp).forall(go)
 
+      case n: PLow => go(n.exp)
+
       case PCompositeLit(typ, _) => typ match {
         case _: PArrayType | _: PImplicitSizeArrayType => !strong
         case _ => true

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

@@ -13,6 +13,7 @@ import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.GeneratedViperMessage
 import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
+import viper.gobra.translator.transformers.hyper.SIFTransformer
 import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
 import viper.silver.ast.pretty.FastPrettyPrinter
@@ -27,7 +28,8 @@ object Translator {
 
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
-      new TerminationTransformer
+      new TerminationTransformer,
+      // new SIFTransformer
     )
 
     val transformedTask = transformers.foldLeft(task) {

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

@@ -10,6 +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.util.ViperWriter.CodeWriter
 import viper.gobra.util.Violation
 import viper.gobra.translator.util.{ViperUtil => vu}
@@ -61,6 +62,8 @@ class AssertionEncoding extends Encoding {
         l = ctx.variable(let.left)
         r <- ctx.expression(let.right)
       } yield withSrc(vpr.Let(l, r, exp), let)
+
+    case n@ in.Low(e) => for {arg <- ctx.expression(e) } yield withSrc(SIFLowExp(arg), n)
   }
 
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {