Hyper Gobra

src/main/antlr4/GobraLexer.g4

@@ -75,6 +75,8 @@ NONE        : 'none' -> mode(NLSEMI);
 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

@@ -81,6 +81,8 @@ ghostPrimaryExpr: range
   | typeOf
   | typeExpr
   | isComparable
+  | low
+  | lowc
   | old
   | before
   | sConversion
@@ -125,6 +127,10 @@ before: BEFORE L_PAREN expression R_PAREN;
 
 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;
@@ -455,13 +461,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,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -264,6 +264,20 @@ 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}
+	 *
+	 * <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}
 	 *
@@ -1040,21 +1054,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}
 	 *

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

@@ -1,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -230,6 +230,18 @@ 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#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
@@ -925,23 +937,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

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

@@ -23,10 +23,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/Gobra.scala

@@ -24,7 +24,7 @@ import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraC
 import viper.gobra.reporting._
 import viper.gobra.translator.Translator
 import viper.gobra.util.Violation.{KnownZ3BugException, LogicException, UglyErrorMessage}
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
+import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext, Sound}
 import viper.silicon.BuildInfo
 import viper.silver.{ast => vpr}
 
@@ -96,13 +96,17 @@ trait GoVerifier extends StrictLogging {
           warnings.foreach(w => logger.debug(w))
 
           result match {
-            case VerifierResult.Success => logger.info(s"$name found no errors")
+            case VerifierResult.Success =>
+              logger.info(s"$name found no errors")
+              Sound.playSuccess()
+
             case VerifierResult.Failure(errors) =>
               logger.error(s"$name has found ${errors.length} error(s) in package $pkgId")
               if (config.noStreamErrors) {
                 errors.foreach(err => logger.error(s"\t${err.formattedMessage}"))
               }
               allVerifierErrors = allVerifierErrors ++ errors
+              Sound.playFailure()
           }
         })(executor)
       try {

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

@@ -1059,6 +1059,10 @@ case class PTypeExpr(typ: PType) extends PGhostExpression
 
 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

@@ -533,6 +533,9 @@ 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 _: PLowContext => "low_context"
+
       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

@@ -580,6 +580,9 @@ 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 LowContext() => "low_context"
+
     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

@@ -656,7 +656,15 @@ 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)
+}
+
+case class LowContext()(val info: Source.Parser.Info) extends Expr {
+  override val typ: Type = BoolT(Addressability.rValue)
+}
 
 /* ** Higher-order predicate expressions */
 

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

@@ -68,7 +68,8 @@ object ConfigDefaults {
   val DefaultZ3APIMode: Boolean = false
   val DefaultDisableNL: Boolean = false
   val DefaultMCEMode: MCE.Mode = MCE.Enabled
-  val DefaultEnableLazyImports: Boolean = false
+  val DefaultHyperMode: Hyper.Mode = Hyper.Enabled
+  lazy val DefaultEnableLazyImports: Boolean = false
   val DefaultNoVerify: Boolean = false
   val DefaultNoStreamErrors: Boolean = false
   val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
@@ -93,24 +94,36 @@ object MCE {
   object Enabled extends Mode
 }
 
+object Hyper {
+  sealed trait Mode
+  /** uses more complete encoding that does not enforce low guards for control flow */
+  object EnabledExtended extends Mode
+  object Enabled extends Mode
+  object Disabled extends Mode
+  object NoMajor extends Mode
+}
+
 object MoreJoins {
   sealed trait Mode {
     // Option number used by Viper, as described in
     // https://github.com/viperproject/silicon/pull/823
     def viperValue: Int
   }
+
   object Disabled extends Mode {
     override val viperValue = 0
   }
+
   object Impure extends Mode {
     override val viperValue = 1
   }
+
   object All extends Mode {
     override val viperValue = 2
   }
 
   def merge(m1: Mode, m2: Mode): Mode = {
-    (m1, m2) match  {
+    (m1, m2) match {
       case (All, _) | (_, All) => All
       case (Impure, _) | (_, Impure) => Impure
       case _ => Disabled
@@ -167,6 +180,8 @@ case class Config(
                    z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                    disableNL: Boolean = ConfigDefaults.DefaultDisableNL,
                    mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
+                   // `None` indicates that no mode has been specified and instructs Gobra to use the default hyper mode
+                   hyperMode: Option[Hyper.Mode] = None,
                    enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                    noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
@@ -228,6 +243,12 @@ case class Config(
       z3APIMode = z3APIMode || other.z3APIMode,
       disableNL = disableNL || other.disableNL,
       mceMode = mceMode,
+      hyperMode = (hyperMode, other.hyperMode) match {
+        case (l, None) => l
+        case (None, r) => r
+        case (l, r) if l == r => l
+        case (Some(l), Some(r)) => Violation.violation(s"Unable to merge differing hyper modes from in-file configuration options, got $l and $r")
+      },
       enableLazyImports = enableLazyImports || other.enableLazyImports,
       noVerify = noVerify || other.noVerify,
       noStreamErrors = noStreamErrors || other.noStreamErrors,
@@ -249,6 +270,7 @@ case class Config(
     }
 
   val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend)
+  val hyperModeOrDefault: Hyper.Mode = hyperMode.getOrElse(ConfigDefaults.DefaultHyperMode)
 }
 
 object Config {
@@ -289,6 +311,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                       disableNL: Boolean = ConfigDefaults.DefaultDisableNL,
                       mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
+                      hyperMode: Option[Hyper.Mode] = None,
                       enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
@@ -352,6 +375,7 @@ trait RawConfig {
     z3APIMode = baseConfig.z3APIMode,
     disableNL = baseConfig.disableNL,
     mceMode = baseConfig.mceMode,
+    hyperMode = baseConfig.hyperMode,
     enableLazyImports = baseConfig.enableLazyImports,
     noVerify = baseConfig.noVerify,
     noStreamErrors = baseConfig.noStreamErrors,
@@ -809,6 +833,19 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true,
   )
 
+  val hyperMode: ScallopOption[Hyper.Mode] = choice(
+    name = "hyperMode",
+    choices = Seq("on", "extended", "off", "noMajor"),
+    descr = "Specifies whether hyper properties should be verified while enforcing low control flow (on), with support for non-low control flow (extended), not verified (off), or whether the major checks should be skipped (noMajor).",
+    default = None,
+    noshort = true
+  ).map {
+    case "on" => Hyper.Enabled
+    case "extended" => Hyper.EnabledExtended
+    case "off" => Hyper.Disabled
+    case "noMajor" => Hyper.NoMajor
+  }
+
   val enableLazyImports: ScallopOption[Boolean] = opt[Boolean](
     name = Config.enableLazyImportOptionName,
     descr = s"Enforces that ${GoVerifier.name} parses depending packages only when necessary. Note that this disables certain language features such as global variables.",
@@ -945,7 +982,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
       Right(())
     }
   }
-  
+
   // `disableSetAxiomatization` can only be provided when using a silicon-based backend
   // since, at the time of writing, we rely on Silicon's setAxiomatizationFile for the
   // implementation
@@ -960,7 +997,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
 
   addValidation {
     if (!disableNL.toOption.contains(true) || isSiliconBasedBackend) {
-      Right(())      
+      Right(())
     } else {
       Left("--disableNL is not compatible with Carbon")
     }
@@ -1055,6 +1092,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     z3APIMode = z3APIMode(),
     disableNL = disableNL(),
     mceMode = mceMode(),
+    hyperMode = hyperMode.toOption,
     enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),
     noStreamErrors = noStreamErrors(),