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)
  }
 }