Introduce Hyper Functions / Fix issue 846

src/main/antlr4/GobraLexer.g4

@@ -102,5 +102,6 @@ OPAQUE      : 'opaque' -> mode(NLSEMI);
 MAYINIT     : 'mayInit' -> mode(NLSEMI);
 REVEAL      : 'reveal';
 BACKEND     : '#backend';
+HYPER       : 'hyper' -> 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

@@ -182,9 +182,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 hyper, boolean mayInit = 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;} | HYPER {$hyper = true;} | MAYINIT {$mayInit = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
   ;
 
 backendAnnotationEntry: ~('('|')'|',')+;

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

@@ -898,6 +898,7 @@ case class PFunctionSpec(
                           isPure: Boolean = false,
                           isTrusted: Boolean = false,
                           isOpaque: Boolean = false,
+                          isHyperFunc: Boolean = false,
                           mayBeUsedInInit: Boolean = false,
                       ) extends PSpecification
 

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

@@ -150,6 +150,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
 
   def showPure: Doc = "pure" <> line
   def showOpaque: Doc = "opaque" <> line
+  def showHyperFunc: Doc = "hyper" <> line
   def showTrusted: Doc = "trusted" <> line
   def showMayInit: Doc = "mayInit" <> line
   def showPre(pre: PExpression): Doc = "requires" <+> showExpr(pre)
@@ -166,9 +167,10 @@ 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, isHyperFunc, mayInit) =>
       (if (isPure) showPure else emptyDoc) <>
       (if (isOpaque) showOpaque else emptyDoc) <>
+      (if (isHyperFunc) showHyperFunc else emptyDoc) <>
       (if (isTrusted) showTrusted else emptyDoc) <>
       (if (mayInit) showMayInit else emptyDoc) <>
       hcat(pres map (showPre(_) <> line)) <>

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

@@ -150,8 +150,10 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showPureFunction(f: PureFunction): Doc = f match {
-    case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque) =>
-      val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <> "pure func"
+    case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque, isHyper) =>
+      val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <>
+        (if (isHyper) text("hyper ") else emptyDoc) <>
+        "pure func"
       funcPrefix <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
         spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block("return" <+> showExpr(b)))
   }
@@ -163,8 +165,10 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   }
 
   def showPureMethod(m: PureMethod): Doc = m match {
-    case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque) =>
-      val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <> "pure func"
+    case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, body, isOpaque, isHyper) =>
+      val funcPrefix = (if (isOpaque) text("opaque ") else emptyDoc) <>
+        (if (isHyper) text("hyper ") else emptyDoc) <>
+        "pure func"
       funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
         spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <> showBackendAnnotations(backendAnnotations)) <> opt(body)(b => block("return" <+> showExpr(b)))
   }
@@ -701,11 +705,15 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
   }
 
   override def showPureFunction(f: PureFunction): Doc = f match {
-    case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque) =>
-    val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
-      funcPrefix <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
-        spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
-        showBackendAnnotations(backendAnnotations))
+    case PureFunction(name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque, isHyper) =>
+    val funcPrefix = {
+      val opaque: Doc = if (isOpaque) "opaque" else emptyDoc
+      val hyper: Doc = if (isHyper) "hyper" else emptyDoc
+      opaque <+> hyper <+> "pure func"
+    }
+    funcPrefix <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
+      spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
+      showBackendAnnotations(backendAnnotations))
   }
 
   override def showMethod(m: Method): Doc = m match {
@@ -716,8 +724,12 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
   }
 
   override def showPureMethod(m: PureMethod): Doc = m match {
-    case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque) =>
-      val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
+    case PureMethod(receiver, name, args, results, pres, posts, measures, backendAnnotations, _, isOpaque, isHyper) =>
+      val funcPrefix = {
+        val opaque: Doc = if (isOpaque) "opaque" else emptyDoc
+        val hyper: Doc = if (isHyper) "hyper" else emptyDoc
+        opaque <+> hyper <+> "pure func"
+      }
       funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
         spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures) <>
           showBackendAnnotations(backendAnnotations))

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

@@ -201,7 +201,8 @@ case class PureMethod(
                        override val terminationMeasures: Vector[TerminationMeasure],
                        override val backendAnnotations: Vector[BackendAnnotation],
                        body: Option[Expr],
-                       isOpaque: Boolean
+                       isOpaque: Boolean,
+                       isHyper: Boolean
                      )(val info: Source.Parser.Info) extends Member with MethodMember {
   require(results.size <= 1)
 }
@@ -259,7 +260,8 @@ case class PureFunction(
                          override val terminationMeasures: Vector[TerminationMeasure],
                          override val backendAnnotations: Vector[BackendAnnotation],
                          body: Option[Expr],
-                         isOpaque: Boolean
+                         isOpaque: Boolean,
+                         isHyper: Boolean
                        )(val info: Source.Parser.Info) extends Member with FunctionMember {
   require(results.size <= 1)
 }
@@ -766,6 +768,7 @@ case class IndexedExp(base : Expr, index : Expr, baseUnderlyingType: Type)(val i
     case t: SliceT => t.elems
     case t: MapT => t.values
     case t: MathMapT => t.values
+    case _: StringT => IntT(Addressability.Exclusive, TypeBounds.Byte)
     case t => Violation.violation(s"expected an array, map or sequence type, but got $t")
   }
 }

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

@@ -10,6 +10,7 @@ import viper.gobra.reporting.Source
 import viper.gobra.reporting.Source.InvalidImplTermMeasureAnnotation
 import viper.gobra.reporting.Source.Parser.Single
 import viper.gobra.translator.Names
+import viper.gobra.translator.util.VprInfo
 import viper.gobra.util.Violation
 
 /**
@@ -183,11 +184,13 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   Violation.violation(m.results.length == 1, "Expected one and only one out-parameter.")
                   // only performs transformation if method has termination measures
                   val src = m.info
+                  val (posMeta, infoMeta, errTMeta) = m.vprMeta
+                  val annotatedInfoMeta = VprInfo.maybeAttachHyperFunc(infoMeta, m.isHyper)
 
                   // the fallback function is called if no comparison succeeds
                   val fallbackProxy = Names.InterfaceMethod.copy(m.name, "fallback")
                   val fallbackTermMeasures = Vector(in.NonItfMethodWildcardMeasure(None)(src))
-                  val fallbackFunction = m.copy(name = fallbackProxy, terminationMeasures = fallbackTermMeasures, body = None)(src)
+                  val fallbackFunction = m.copy(name = fallbackProxy, terminationMeasures = fallbackTermMeasures, body = None)(src).withMeta(posMeta, annotatedInfoMeta, errTMeta)
 
                   // new body to check termination
                   val terminationCheckBody = {
@@ -224,7 +227,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
                     }
                     in.Conditional(in.BoolLit(b = true)(src), fallbackProxyCall, bodyFalseBranch, returnType)(src)
                   }
-                  val transformedM = m.copy(terminationMeasures = m.terminationMeasures, body = Some(terminationCheckBody))(src)
+                  val transformedM = m.copy(terminationMeasures = m.terminationMeasures, body = Some(terminationCheckBody))(src).withMeta(posMeta, annotatedInfoMeta, errTMeta)
 
                   methodsToRemove += m
                   methodsToAdd += transformedM

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

@@ -34,18 +34,18 @@ object OverflowChecksTransform extends InternalTransform {
 
     // Adds pre-conditions stating the bounds of each argument and a post-condition to check if the body expression
     // overflows
-    case f@PureFunction(name, args, results, pres, posts, terminationMeasure, annotations, body, isOpaque) => body match {
+    case f@PureFunction(name, args, results, pres, posts, terminationMeasure, annotations, body, isOpaque, isHyper) => body match {
       case Some(expr) =>
         val newPost = posts ++ getPureBlockPosts(expr, results)
-        PureFunction(name, args, results, pres, newPost, terminationMeasure, annotations, body, isOpaque)(f.info)
+        PureFunction(name, args, results, pres, newPost, terminationMeasure, annotations, body, isOpaque, isHyper)(f.info)
       case None => f
     }
 
     // Same as pure functions
-    case m@PureMethod(receiver, name, args, results, pres, posts, terminationMeasure, annotations, body, isOpaque) => body match {
+    case m@PureMethod(receiver, name, args, results, pres, posts, terminationMeasure, annotations, body, isOpaque, isHyper) => body match {
       case Some(expr) =>
         val newPost = posts ++ getPureBlockPosts(expr, results)
-        PureMethod(receiver, name, args, results, pres, newPost, terminationMeasure, annotations, body, isOpaque)(m.info)
+        PureMethod(receiver, name, args, results, pres, newPost, terminationMeasure, annotations, body, isOpaque, isHyper)(m.info)
       case None => m
     }
 

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

@@ -708,7 +708,8 @@ object Desugar extends LazyLogging {
       val funcInfo = pureFunctionMemberOrLitD(decl, fsrc, new FunctionContext(_ => _ => in.Seqn(Vector.empty)(fsrc)), info)
 
       in.PureFunction(name, funcInfo.args, funcInfo.results, funcInfo.pres,
-        funcInfo.posts, funcInfo.terminationMeasures, funcInfo.backendAnnotations, funcInfo.body, funcInfo.isOpaque)(fsrc)
+        funcInfo.posts, funcInfo.terminationMeasures, funcInfo.backendAnnotations, funcInfo.body, funcInfo.isOpaque,
+        funcInfo.isHyper)(fsrc)
     }
 
     private case class PureFunctionInfo(args: Vector[in.Parameter.In],
@@ -719,7 +720,9 @@ object Desugar extends LazyLogging {
                                         terminationMeasures: Vector[in.TerminationMeasure],
                                         backendAnnotations: Vector[BackendAnnotation],
                                         body: Option[in.Expr],
-                                        isOpaque: Boolean)
+                                        isOpaque: Boolean,
+                                        isHyper: Boolean
+                                       )
 
 
     private def pureFunctionMemberOrLitD(decl: PFunctionOrClosureDecl, fsrc: Meta, outerCtx: FunctionContext, info: TypeInfo): PureFunctionInfo = {
@@ -766,6 +769,7 @@ object Desugar extends LazyLogging {
       val terminationMeasure = sequence(decl.spec.terminationMeasures map terminationMeasureD(ctx, info, false)).res
 
       val isOpaque = decl.spec.isOpaque
+      val isHyper = decl.spec.isHyperFunc
 
       val capturedWithAliases = (captured.map { v => in.Ref(localVarD(outerCtx, info)(v))(meta(v, info)) } zip capturedPar)
 
@@ -779,7 +783,7 @@ object Desugar extends LazyLogging {
       }
       val annotations = desugarBackendAnnotations(decl.spec.backendAnnotations)
 
-      PureFunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasure, annotations, bodyOpt, isOpaque)
+      PureFunctionInfo(args, capturedWithAliases, returns, pres, posts, terminationMeasure, annotations, bodyOpt, isOpaque, isHyper)
     }
 
 
@@ -946,6 +950,7 @@ object Desugar extends LazyLogging {
       val terminationMeasure = sequence(decl.spec.terminationMeasures map terminationMeasureD(ctx, info, false)).res
 
       val isOpaque = decl.spec.isOpaque
+      val isHyper = decl.spec.isHyperFunc
 
       val bodyOpt = decl.body.map {
         case (_, b: PBlock) =>
@@ -956,7 +961,7 @@ object Desugar extends LazyLogging {
           implicitConversion(res.typ, returns.head.typ, res)
       }
       val annotations = desugarBackendAnnotations(decl.spec.backendAnnotations)
-      in.PureMethod(recv, name, args, returns, pres, posts, terminationMeasure, annotations, bodyOpt, isOpaque)(fsrc)
+      in.PureMethod(recv, name, args, returns, pres, posts, terminationMeasure, annotations, bodyOpt, isOpaque, isHyper)(fsrc)
     }
 
     def fpredicateD(decl: PFPredicateDecl): in.FPredicate = {
@@ -3295,9 +3300,10 @@ object Desugar extends LazyLogging {
             sequence(m.spec.terminationMeasures map terminationMeasureD(specCtx, info, true)).res
           val annotations = desugarBackendAnnotations(m.spec.backendAnnotations)
           val isOpaque = m.spec.isOpaque
+          val isHyper = m.spec.isHyperFunc
 
           val mem = if (m.spec.isPure) {
-            in.PureMethod(recv, proxy, args, returns, pres, posts, terminationMeasures, annotations, None, isOpaque)(src)
+            in.PureMethod(recv, proxy, args, returns, pres, posts, terminationMeasures, annotations, None, isOpaque, isHyper)(src)
           } else {
             in.Method(recv, proxy, args, returns, pres, posts, terminationMeasures, annotations, None)(src)
           }

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

@@ -926,6 +926,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       isPure = ctx.pure,
       isTrusted = ctx.trusted,
       isOpaque = ctx.opaque,
+      isHyperFunc = ctx.hyper,
       mayBeUsedInInit = ctx.mayInit,
     )
   }

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

@@ -73,6 +73,7 @@ object SymbolTable extends Environments[Entity] {
     override val result: PResult = decl.result
     def isPure: Boolean = decl.spec.isPure
     def isOpaque: Boolean = decl.spec.isOpaque
+    def isHyper: Boolean = decl.spec.isHyperFunc
   }
 
   case class Closure(lit: PFunctionLit, ghost: Boolean, context: ExternalTypeInfo) extends ActualDataEntity with WithArguments with WithResult {
@@ -182,11 +183,13 @@ object SymbolTable extends Environments[Entity] {
 
   sealed trait Method extends MethodLike with ActualTypeMember with WithResult {
     def isPure: Boolean
+    def isHyper: 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 def isHyper: Boolean = decl.spec.isHyperFunc
     override val args: Vector[PParameter] = decl.args
     override val result: PResult = decl.result
     def isOpaque: Boolean = decl.spec.isOpaque
@@ -195,6 +198,7 @@ object SymbolTable extends Environments[Entity] {
   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 def isHyper: Boolean = spec.spec.isHyperFunc
     override val args: Vector[PParameter] = spec.args
     override def result: PResult = spec.result
     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) => implMember.isHyper != itfMember.isHyper
+                      case _ => false
+                    }
+                  }) {
+                    Vector(s"For member $name, the 'hyper' annotation for implementation and interface does not match")
                   } else {
                     Vector.empty
                   }

src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala

@@ -92,6 +92,9 @@ trait Enclosing { this: TypeInfoImpl =>
   lazy val isEnclosingGhost: PNode => Boolean =
     down(false){ case _: PGhostifier[_] | _: PGhostNode => true }
 
+  lazy val isEnclosingLowAssertion: PNode => Boolean =
+    down(false) { case _: PLow => true }
+
   // Returns true iff n occurs in an init() function, or a function marked with
   // 'mayInit' or in the rhs of a global variable declaration.
   def isEnclosingMayInit(n: PNode): Boolean = {