Interface predicate instances imply that the interface argument is not nil

src/main/scala/viper/gobra/translator/context/Context.scala

@@ -87,6 +87,10 @@ trait Context {
 
   def assertion(x: in.Assertion): CodeWriter[vpr.Exp] = typeEncoding.finalAssertion(this)(x)
 
+  def predicateAccess(x: in.PredicateAccess): CodeWriter[vpr.PredicateAccess] = typeEncoding.predicateAccess(this)(x)
+
+  def predicateAccessPredicate(x: in.PredicateAccess, p: in.Expr)(src: in.Node): CodeWriter[vpr.PredicateAccessPredicate] = typeEncoding.predicateAccessPredicate(this)(x, p, src)
+
   def invariant(x: in.Assertion): (CodeWriter[Unit], vpr.Exp) = typeEncoding.invariant(this)(x)
 
   def precondition(x: in.Assertion): MemberWriter[vpr.Exp] = typeEncoding.precondition(this)(x)

src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala

@@ -53,10 +53,8 @@ class PermissionEncoding extends LeafTypeEncoding {
       case cp: in.CurrentPerm =>
         val (pos, info, errT) = cp.vprMeta
         for {
-          arg <- ctx.assertion(in.Access(in.Accessible.Predicate(cp.acc.op), in.FullPerm(cp.info))(cp.info))
-          pap = arg.asInstanceOf[vpr.PredicateAccessPredicate]
-          res = vpr.CurrentPerm(pap.loc)(pos, info, errT)
-        } yield res
+          pacc <- ctx.predicateAccess(cp.acc.op)
+        } yield vpr.CurrentPerm(pacc)(pos, info, errT)
       case pm@ in.PermMinus(exp) => for { e <- goE(exp) } yield withSrc(vpr.PermMinus(e), pm)
       case fp@ in.FractionalPerm(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.FractionalPerm(vl, vr), fp)
       case pa@ in.PermAdd(l, r) => for {vl <- goE(l); vr <- goE(r)} yield withSrc(vpr.PermAdd(vl, vr), pa)

src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala

@@ -64,7 +64,7 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) {
     */
   private def genConversion(recvType: in.Type, meth: in.MethodProxy)(ctx: Context): vpr.Function = {
     generatedConversions.getOrElse(meth, {
-      val (pos, info: Source.Verifier.Info, errT) = meth.vprMeta
+      val (pos, info, errT) = meth.vprMeta
 
       val proxy = getterFunctionProxy(meth)
       val receiver = in.Parameter.In("self", recvType)(meth.info)
@@ -73,7 +73,7 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) {
 
       val result = underlyingType(recvType)(ctx) match {
         case recvType: in.InterfaceT =>
-          val recvNotNil = interfaceUtils.receiverNotNil(vprReceiverVar)(pos, info, errT)(ctx)
+          val recvNotNil = interfaceUtils.receiverNotNil(vprReceiverVar)(ctx)
           val defTCall: in.Type => vpr.Exp = t => {
             val func = genConversion(t, defTMethodProxy(t, meth.name)(ctx))(ctx)
             vpr.FuncApp(func = func, args = Seq(poly.unbox(interfaces.polyValOf(vprReceiverVar)()(ctx), t)(pos, info, errT)(ctx)))(pos, info, errT)

src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala

@@ -47,6 +47,7 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")
+  override def predicateAccess(ctx: Context): in.PredicateAccess ==> CodeWriter[vpr.PredicateAccess] = te.predicateAccess(ctx) orElse expectedMatch("predicateAccess")
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = te.reference(ctx) orElse expectedMatch("reference")
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = te.addressFootprint(ctx) orElse expectedMatch("addressFootprint")
   override def isComparable(ctx: Context): Expr ==> Either[Boolean, CodeWriter[Exp]] = te.isComparable(ctx) orElse expectedMatch("isComparable")

src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala

@@ -206,12 +206,24 @@ trait TypeEncoding extends Generator {
 
   /**
     * Encodes assertions.
-    *
-    * Constraints:
-    * - in.Access with in.PredicateAccess has to encode to vpr.PredicateAccessPredicate.
     */
   def assertion(@unused ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = PartialFunction.empty
 
+  /**
+    * Encodes predicate accesses.
+    * Supported predicate accesses have a default encoding of access, fold, unfold, unfolding, trigger, perm, and termination measures.
+    */
+  def predicateAccess(@unused ctx: Context): in.PredicateAccess ==> CodeWriter[vpr.PredicateAccess] = PartialFunction.empty
+
+  final def predicateAccessPredicate(ctx: Context): (in.PredicateAccess, in.Expr, in.Node) ==> CodeWriter[vpr.PredicateAccessPredicate] = {
+    val pa = predicateAccess(ctx); { case (pa(w), perm, src) =>
+      for {
+        pacc <- w
+        perm <- ctx.expression(perm)
+      } yield withSrc(vpr.PredicateAccessPredicate(pacc, perm), src)
+    }
+  }
+
   final def invariant(ctx: Context): in.Assertion ==> (CodeWriter[Unit], vpr.Exp) = {
     def invErr(inv: vpr.Exp): ErrorTransformer = {
       case e@ vprerr.ContractNotWellformed(Source(info), reason, _) if e causedBy inv =>

src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala

@@ -50,6 +50,7 @@ abstract class TypeEncodingCombiner(encodings: Vector[TypeEncoding], defaults: V
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = combiner(_.goEqual(ctx))
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = combiner(_.expression(ctx))
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = combiner(_.assertion(ctx))
+  override def predicateAccess(ctx: Context): in.PredicateAccess ==> CodeWriter[vpr.PredicateAccess] = combiner(_.predicateAccess(ctx))
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = combiner(_.reference(ctx))
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = combiner(_.addressFootprint(ctx))
   override def isComparable(ctx: Context): in.Expr ==> Either[Boolean, CodeWriter[Exp]] = combiner(_.isComparable(ctx))

src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPredicateEncoding.scala

@@ -83,54 +83,47 @@ class DefaultPredicateEncoding extends Encoding {
   /**
     * Encodes assertions.
     *
-    * Constraints:
-    * - in.Access with in.PredicateAccess has to encode to vpr.PredicateAccessPredicate.
-    *
     * [acc(  p(as), perm] -> p(Argument[as], Permission[perm])
     * [acc(e.p(as), perm] -> p(Argument[e], Argument[as], Permission[perm])
     */
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
-    case acc@ in.Access(in.Accessible.Predicate(op: in.FPredicateAccess), perm) =>
-      val (pos, info, errT) = acc.vprMeta
+    case acc@ in.Access(in.Accessible.Predicate(op: in.PredicateAccess), perm) => ctx.predicateAccessPredicate(op, perm)(acc)
+  }
+
+  override def predicateAccess(ctx: Context): in.PredicateAccess ==> CodeWriter[vpr.PredicateAccess] = {
+    case op: in.FPredicateAccess =>
       for {
         vArgs <- cl.sequence(op.args map ctx.expression)
-        pacc = vpr.PredicateAccess(vArgs, op.pred.name)(pos, info, errT)
-        vPerm <- ctx.expression(perm)
-      } yield vpr.PredicateAccessPredicate(pacc, vPerm)(pos, info, errT)
+      } yield withSrc(vpr.PredicateAccess(vArgs, op.pred.name), op)
 
-    case acc@ in.Access(in.Accessible.Predicate(op: in.MPredicateAccess), perm) =>
-      val (pos, info, errT) = acc.vprMeta
+    case op: in.MPredicateAccess =>
       for {
         vRecv <- ctx.expression(op.recv)
         vArgs <- cl.sequence(op.args map ctx.expression)
-        pacc = vpr.PredicateAccess(vRecv +: vArgs, op.pred.uniqueName)(pos, info, errT)
-        vPerm <- ctx.expression(perm)
-      } yield vpr.PredicateAccessPredicate(pacc, vPerm)(pos, info, errT)
+      } yield withSrc(vpr.PredicateAccess(vRecv +: vArgs, op.pred.uniqueName), op)
   }
 
   override def statement(ctx: Context): in.Stmt ==> CodeWriter[vpr.Stmt] = {
     case fold: in.Fold =>
       val (pos, info, errT) = fold.vprMeta
       for {
-        a <- ctx.assertion(fold.acc)
-        pap = a.asInstanceOf[vpr.PredicateAccessPredicate]
+        pap <- ctx.predicateAccessPredicate(fold.op, fold.acc.p)(fold.acc)
       } yield vpr.Fold(pap)(pos, info, errT)
 
     case unfold: in.Unfold =>
       val (pos, info, errT) = unfold.vprMeta
       for {
-        a <- ctx.assertion(unfold.acc)
-        pap = a.asInstanceOf[vpr.PredicateAccessPredicate]
+        pap <- ctx.predicateAccessPredicate(unfold.op, unfold.acc.p)(unfold.acc)
       } yield vpr.Unfold(pap)(pos, info, errT)
   }
 
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     case unfold: in.Unfolding =>
       val (pos, info, errT) = unfold.vprMeta
       for {
-        a <- ctx.assertion(unfold.acc)
+        pap <- ctx.predicateAccessPredicate(unfold.op, unfold.acc.p)(unfold.acc)
         e <- cl.pure(ctx.expression(unfold.in))(ctx)
-      } yield vpr.Unfolding(a.asInstanceOf[vpr.PredicateAccessPredicate], e)(pos, info, errT)
+      } yield vpr.Unfolding(pap, e)(pos, info, errT)
   }
 
 }

src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala

@@ -94,11 +94,11 @@ class InterfaceEncoding extends LeafTypeEncoding {
   override def method(ctx: Context): in.Member ==> MemberWriter[vpr.Method] = {
     case p: in.Method if p.receiver.typ.isInstanceOf[in.InterfaceT] =>
       // adds the precondition that the receiver is not equal to the nil interface
-      val (pos, info: Source.Verifier.Info, errT) = p.vprMeta
+      val (pos, info, errT) = p.vprMeta
       for {
         m <- ctx.defaultEncoding.method(p)(ctx)
         recv = m.formalArgs.head.localVar // receiver is always the first parameter
-        mWithNotNilCheck = m.copy(pres = utils.receiverNotNil(recv)(pos, info, errT)(ctx) +: m.pres)(pos, info, errT)
+        mWithNotNilCheck = m.copy(pres = utils.receiverNotNil(recv)(ctx) +: m.pres)(pos, info, errT)
       } yield mWithNotNilCheck
 
     case p: in.MethodSubtypeProof =>
@@ -249,33 +249,36 @@ class InterfaceEncoding extends LeafTypeEncoding {
 
   /**
     * Encodes assertions.
-    *
-    * Constraints:
-    * - in.Access with in.PredicateAccess has to encode to vpr.PredicateAccessPredicate.
-    *
-    *
     */
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
-    def goE(x: in.Expr): CodeWriter[vpr.Exp] = ctx.expression(x)
+
+    def wrap(predicateAccess: vpr.PredicateAccess, perm: vpr.Exp): vpr.Exp = {
+      val (pos, info, errT) = predicateAccess.meta
+      val predicateAccessPredicate = vpr.PredicateAccessPredicate(predicateAccess, perm)(pos, info, errT)
+      val notNil = utils.receiverNotNil(predicateAccess.args.head)(ctx)
+      vpr.And(predicateAccessPredicate, notNil)(pos, info, errT)
+    }
 
     default(super.assertion(ctx)) {
-      case n@ in.Access(in.Accessible.Predicate(in.MPredicateAccess(recv, p, args)), perm) if hasFamily(p)(ctx) =>
-        val (pos, info, errT) = n.vprMeta
+
+      case in.Access(in.Accessible.Predicate(pacc@ in.MPredicateAccess(_:: ctx.Interface(_), _, _)), perm) =>
         for {
-          instance <- mpredicateInstance(recv, p, args)(n)(ctx)
-          perm <- goE(perm)
-        } yield vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT): vpr.Exp
+          instance <- ctx.predicateAccess(pacc)
+          perm <- ctx.expression(perm)
+        } yield wrap(instance, perm)
 
-      case n@ in.Access(in.Accessible.Predicate(in.FPredicateAccess(p, args)), perm) if hasFamily(p)(ctx) =>
-        val (pos, info, errT) = n.vprMeta
+      case in.Access(in.Accessible.Predicate(pacc: in.FPredicateAccess), perm) if hasFamily(pacc.pred)(ctx) =>
         for {
-          instance <- fpredicateInstance(p, args)(n)(ctx)
-          perm <- goE(perm)
-        } yield vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT): vpr.Exp
+          instance <- ctx.predicateAccess(pacc)
+          perm <- ctx.expression(perm)
+        } yield wrap(instance, perm)
     }
   }
 
-
+  override def predicateAccess(ctx: Context): in.PredicateAccess ==> CodeWriter[vpr.PredicateAccess] = {
+    case n@ in.MPredicateAccess(recv, p, args) if hasFamily(p)(ctx) => mpredicateInstance(recv ,p, args)(n)(ctx)
+    case n@ in.FPredicateAccess(p, args) if hasFamily(p)(ctx) => fpredicateInstance(p, args)(n)(ctx)
+  }
 
   /**
     * Encodes whether a value is comparable or not.
@@ -681,7 +684,7 @@ class InterfaceEncoding extends LeafTypeEncoding {
   private def function(p: in.PureMethod)(ctx: Context): MemberWriter[vpr.Function] = {
     Violation.violation(p.results.size == 1, s"expected a single result, but got ${p.results}")
 
-    val (pos, info: Source.Verifier.Info, errT) = p.vprMeta
+    val (pos, info, errT) = p.vprMeta
 
     val pProxy = Names.InterfaceMethod.origin(p.name)
 
@@ -721,7 +724,7 @@ class InterfaceEncoding extends LeafTypeEncoding {
         name = p.name.uniqueName,
         formalArgs = recvDecl +: argDecls,
         typ = resultType,
-        pres = utils.receiverNotNil(recv)(pos, info, errT)(ctx) +: (vPres ++ measures),
+        pres = utils.receiverNotNil(recv)(ctx) +: (vPres ++ measures),
         posts = (cases map { case (impl, implProxy) => clause(impl, implProxy) }) ++ posts,
         body = body
       )(pos, info, errT)

src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceUtils.scala

@@ -14,7 +14,8 @@ import viper.silver.{ast => vpr}
 class InterfaceUtils(interfaces: InterfaceComponent, types: TypeComponent, poly: PolymorphValueComponent) {
 
   /** Returns [x != nil: Interface{}] */
-  def receiverNotNil(recv: vpr.Exp)(pos: vpr.Position, info: Source.Verifier.Info, errT: vpr.ErrorTrafo)(ctx: Context): vpr.Exp = {
+  def receiverNotNil(recv: vpr.Exp)(ctx: Context): vpr.Exp = {
+    val (pos, info: Source.Verifier.Info, errT) = recv.meta
     // In Go, checking that an interface receiver is not nil never panics.
     vpr.Not(vpr.EqCmp(recv, nilInterface()(pos, info, errT)(ctx))(pos, info, errT))(pos, info.createAnnotatedInfo(Source.ReceiverNotNilCheckAnnotation), errT)
   }

src/main/scala/viper/gobra/translator/encodings/preds/PredEncoding.scala

@@ -68,9 +68,6 @@ class PredEncoding extends LeafTypeEncoding {
   /**
     * Encodes assertions.
     *
-    * Constraints:
-    * - in.Access with in.PredicateAccess has to encode to vpr.PredicateAccessPredicate.
-    *
     * [acc(p(e1, ..., en))] -> eval_S([p], [e1], ..., [en]) where p: pred(S)
     */
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
@@ -127,7 +124,7 @@ class PredEncoding extends LeafTypeEncoding {
             // a1, ..., ak
             qArgs = mergeArgs(ctrArgs, accArgs)
             // acc(Q(a1, ..., ak), [p])
-            qAcc <- proxyAccess(q, qArgs, perm)(n.info)(ctx)
+            qAcc <- proxyAccess(q, qArgs, perm)(n)(ctx)
             // fold acc(Q(a1, ..., ak), [p])
             fold = vpr.Fold(qAcc)(pos, info, errT)
             _ <- write(fold)
@@ -169,7 +166,7 @@ class PredEncoding extends LeafTypeEncoding {
                 UnfoldError(info) dueTo DefaultErrorBackTranslator.defaultTranslate(reason) // we might want to change the message
             }
             // acc(Q(a1, ..., ak), [p])
-            qAcc <- proxyAccess(q, qArgs, perm)(n.info)(ctx)
+            qAcc <- proxyAccess(q, qArgs, perm)(n)(ctx)
             // inhale acc(Q(a1, ..., ak), [p])
             _ <- write(vpr.Inhale(qAcc)(pos, info, errT))
             // unfold acc(Q(a1, ..., ak), [p])
@@ -179,11 +176,10 @@ class PredEncoding extends LeafTypeEncoding {
   }
 
   /** Returns proxy(args) */
-  def proxyAccess(proxy: in.PredicateProxy, args: Vector[in.Expr], perm: in.Expr)(src: Source.Parser.Info)(ctx: Context): CodeWriter[vpr.PredicateAccessPredicate] = {
-    val predicateInstance = proxy match {
-      case proxy: in.FPredicateProxy => in.Access(in.Accessible.Predicate(in.FPredicateAccess(proxy, args)(src)), perm)(src)
-      case proxy: in.MPredicateProxy => in.Access(in.Accessible.Predicate(in.MPredicateAccess(args.head, proxy, args.tail)(src)), perm)(src)
+  def proxyAccess(proxy: in.PredicateProxy, args: Vector[in.Expr], perm: in.Expr)(src: in.Node)(ctx: Context): CodeWriter[vpr.PredicateAccessPredicate] = {
+    proxy match {
+      case proxy: in.FPredicateProxy => ctx.predicateAccessPredicate(in.FPredicateAccess(proxy, args)(src.info), perm)(src)
+      case proxy: in.MPredicateProxy => ctx.predicateAccessPredicate(in.MPredicateAccess(args.head, proxy, args.tail)(src.info), perm)(src)
     }
-    ctx.assertion(predicateInstance).map(_.asInstanceOf[vpr.PredicateAccessPredicate])
   }
 }

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

@@ -104,12 +104,7 @@ class AssertionEncoding extends Encoding {
   }
 
   def triggerExpr(expr: in.TriggerExpr)(ctx: Context): CodeWriter[vpr.Exp] = expr match {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
-    case in.Accessible.Predicate(op) =>
-      for {
-        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
-        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-      } yield pap.loc
+    case in.Accessible.Predicate(op) => ctx.predicateAccess(op)
     case e: in.Expr => ctx.expression(e)
   }
 

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

@@ -42,8 +42,7 @@ class TerminationEncoding extends Encoding {
   def predicateInstance(x: in.PredicateAccess)(ctx: Context): CodeWriter[predicateinstance.PredicateInstance] = {
     val (pos, info, errT) = x.vprMeta
     for {
-      v <- ctx.assertion(in.Access(in.Accessible.Predicate(x), in.FullPerm(x.info))(x.info))
-      pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-    } yield predicateinstance.PredicateInstance(pap.loc.args, pap.loc.predicateName)(pos, info, errT)
+      pacc <- ctx.predicateAccess(x)
+    } yield predicateinstance.PredicateInstance(pacc.args, pacc.predicateName)(pos, info, errT)
   }
 }