From 389ab536cec67a3cb9182f71ed404885343ee98c Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 30 Sep 2022 15:09:38 +0200 Subject: [PATCH 1/3] added not nil to interface predicate instances --- .../encodings/closures/MethodObjectEncoder.scala | 4 ++-- .../encodings/interfaces/InterfaceEncoding.scala | 16 ++++++++++------ .../encodings/interfaces/InterfaceUtils.scala | 3 ++- 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala index d5d368920..dd352cc62 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala +++ b/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) diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala index 1f70d737f..e6afed921 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/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 => @@ -264,14 +264,18 @@ class InterfaceEncoding extends LeafTypeEncoding { for { instance <- mpredicateInstance(recv, p, args)(n)(ctx) perm <- goE(perm) - } yield vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT): vpr.Exp + predAccessPredicate = vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT) + notNil = utils.receiverNotNil(instance.args.head)(ctx) + } yield vpr.And(predAccessPredicate, notNil)(pos, info, errT) case n@ in.Access(in.Accessible.Predicate(in.FPredicateAccess(p, args)), perm) if hasFamily(p)(ctx) => val (pos, info, errT) = n.vprMeta for { instance <- fpredicateInstance(p, args)(n)(ctx) perm <- goE(perm) - } yield vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT): vpr.Exp + predAccessPredicate = vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT) + notNil = utils.receiverNotNil(instance.args.head)(ctx) + } yield vpr.And(predAccessPredicate, notNil)(pos, info, errT) } } @@ -681,7 +685,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 +725,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) diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceUtils.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceUtils.scala index 3421a5556..d1bb9b2ae 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceUtils.scala +++ b/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) } From a2c4d88171f375e2cae85c71bc0e7e308b68d37b Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 30 Sep 2022 15:56:47 +0200 Subject: [PATCH 2/3] added case for predicate with interface receiver but no family --- .../interfaces/InterfaceEncoding.scala | 27 ++++++++++++------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala index e6afed921..839115a92 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala @@ -258,24 +258,33 @@ class InterfaceEncoding extends LeafTypeEncoding { 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 n@in.Access(in.Accessible.Predicate(in.MPredicateAccess(recv, p, args)), perm) if hasFamily(p)(ctx) => for { instance <- mpredicateInstance(recv, p, args)(n)(ctx) perm <- goE(perm) - predAccessPredicate = vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT) - notNil = utils.receiverNotNil(instance.args.head)(ctx) - } yield vpr.And(predAccessPredicate, notNil)(pos, info, errT) + } yield wrap(instance, perm) + + case n@in.Access(in.Accessible.Predicate(in.MPredicateAccess(recv:: ctx.Interface(_), p, args)), perm) => + for { + recv <- goE(recv) + args <- sequence(args map goE) + instance = withSrc(vpr.PredicateAccess(recv +: args, p.uniqueName), n) + perm <- goE(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 for { instance <- fpredicateInstance(p, args)(n)(ctx) perm <- goE(perm) - predAccessPredicate = vpr.PredicateAccessPredicate(instance, perm)(pos, info, errT) - notNil = utils.receiverNotNil(instance.args.head)(ctx) - } yield vpr.And(predAccessPredicate, notNil)(pos, info, errT) + } yield wrap(instance, perm) } } From a2e75f0aa9b2d63b50544a6dc7034f732461864d Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 30 Sep 2022 20:08:14 +0200 Subject: [PATCH 3/3] special cased predicate instance encoding --- .../gobra/translator/context/Context.scala | 4 +++ .../encodings/PermissionEncoding.scala | 6 ++-- .../combinators/FinalTypeEncoding.scala | 1 + .../encodings/combinators/TypeEncoding.scala | 18 +++++++++-- .../combinators/TypeEncodingCombiner.scala | 1 + .../defaults/DefaultPredicateEncoding.scala | 31 +++++++------------ .../interfaces/InterfaceEncoding.scala | 30 ++++++------------ .../encodings/preds/PredEncoding.scala | 16 ++++------ .../typeless/AssertionEncoding.scala | 7 +---- .../typeless/TerminationEncoding.scala | 5 ++- 10 files changed, 54 insertions(+), 65 deletions(-) diff --git a/src/main/scala/viper/gobra/translator/context/Context.scala b/src/main/scala/viper/gobra/translator/context/Context.scala index 8486924e3..f8eacd122 100644 --- a/src/main/scala/viper/gobra/translator/context/Context.scala +++ b/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) diff --git a/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala index a0d436c86..18e47edfb 100644 --- a/src/main/scala/viper/gobra/translator/encodings/PermissionEncoding.scala +++ b/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) diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala index 3b7a49e89..4ab55eff6 100644 --- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala +++ b/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") diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala index ede5d7669..3fa7a3285 100644 --- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala +++ b/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 => diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala index 81b646efd..9d86d9bde 100644 --- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala +++ b/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)) diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPredicateEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPredicateEncoding.scala index 29470efe4..ab112832f 100644 --- a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPredicateEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPredicateEncoding.scala @@ -83,44 +83,37 @@ 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) } @@ -128,9 +121,9 @@ class DefaultPredicateEncoding extends Encoding { 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) } } diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala index 839115a92..02e36dfbd 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala @@ -249,14 +249,8 @@ 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 @@ -266,29 +260,25 @@ class InterfaceEncoding extends LeafTypeEncoding { } default(super.assertion(ctx)) { - case n@in.Access(in.Accessible.Predicate(in.MPredicateAccess(recv, p, args)), perm) if hasFamily(p)(ctx) => - for { - instance <- mpredicateInstance(recv, p, args)(n)(ctx) - perm <- goE(perm) - } yield wrap(instance, perm) - case n@in.Access(in.Accessible.Predicate(in.MPredicateAccess(recv:: ctx.Interface(_), p, args)), perm) => + case in.Access(in.Accessible.Predicate(pacc@ in.MPredicateAccess(_:: ctx.Interface(_), _, _)), perm) => for { - recv <- goE(recv) - args <- sequence(args map goE) - instance = withSrc(vpr.PredicateAccess(recv +: args, p.uniqueName), n) - perm <- goE(perm) + 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) => + 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) + 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. diff --git a/src/main/scala/viper/gobra/translator/encodings/preds/PredEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/preds/PredEncoding.scala index ade5f9d8a..058270ad1 100644 --- a/src/main/scala/viper/gobra/translator/encodings/preds/PredEncoding.scala +++ b/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]) } } diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala index 448dc0fbc..8f09e573e 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala +++ b/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) } diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala index 9254170b7..70c62a738 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/TerminationEncoding.scala +++ b/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) } }