Skip to content

Commit

Permalink
Fix PrettyPrint + Default/Call encoding errors
Browse files Browse the repository at this point in the history
  • Loading branch information
@dnezam
dnezam committed Feb 2, 2024
1 parent dc28aca commit 6f8f3f3
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 36 deletions.
8 changes: 6 additions & 2 deletions src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showPure: Doc = "pure" <> line
def showOpaque: Doc = "opaque" <> line
def showTrusted: Doc = "trusted" <> line
def showPre(pre: PExpression): Doc = "requires" <+> showExpr(pre)
def showPreserves(preserves: PExpression): Doc = "preserves" <+> showExpr(preserves)
Expand All @@ -143,8 +144,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showSpec(spec: PSpecification): Doc = spec match {
case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) =>
case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted, isOpaque) =>
(if (isPure) showPure else emptyDoc) <>
(if (isOpaque) showOpaque else emptyDoc) <>
(if (isTrusted) showTrusted else emptyDoc) <>
hcat(pres map (showPre(_) <> line)) <>
hcat(preserves map (showPreserves(_) <> line)) <>
Expand Down Expand Up @@ -453,7 +455,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
case PStringLit(lit) => "\"" <> lit <> "\""
case PCompositeLit(typ, lit) => showLiteralType(typ) <+> showLiteralValue(lit)
case lit: PFunctionLit => showFunctionLit(lit)
case PInvoke(base, args, spec) => showExprOrType(base) <> parens(showExprList(args)) <> opt(spec)(s => emptyDoc <+> "as" <+> showMisc(s))
case PInvoke(base, args, spec, reveal) =>
val revealDoc: Doc = if (reveal) "reveal" else emptyDoc
revealDoc <+> showExprOrType(base) <> parens(showExprList(args)) <> opt(spec)(s => emptyDoc <+> "as" <+> showMisc(s))
case PIndexedExp(base, index) => showExpr(base) <> brackets(showExpr(index))

case PSliceExp(base, low, high, cap) => {
Expand Down
28 changes: 18 additions & 10 deletions src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,8 +151,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showPureFunction(f: PureFunction): Doc = f match {
case PureFunction(name, args, results, pres, posts, measures, body) =>
"pure func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
case PureFunction(name, args, results, pres, posts, measures, body, 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)) <> opt(body)(b => block("return" <+> showExpr(b)))
}

Expand All @@ -163,8 +164,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
}

def showPureMethod(m: PureMethod): Doc = m match {
case PureMethod(receiver, name, args, results, pres, posts, measures, body) =>
"pure func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
case PureMethod(receiver, name, args, results, pres, posts, measures, body, isOpaque) =>
val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures)) <> opt(body)(b => block("return" <+> showExpr(b)))
}

Expand Down Expand Up @@ -488,9 +490,13 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
case c: CurrentPerm => "perm" <> parens(showAcc(c.acc))
case PermMinus(exp) => "-" <> showExpr(exp)

case PureFunctionCall(func, args, _) => func.name <> parens(showExprList(args))
case PureFunctionCall(func, args, _, reveal) =>
val revealDoc: Doc = if (reveal) "reveal" else emptyDoc
revealDoc <+> func.name <> parens(showExprList(args))

case PureMethodCall(recv, meth, args, _) => showExpr(recv) <> dot <> meth.name <> parens(showExprList(args))
case PureMethodCall(recv, meth, args, _, reveal) =>
val revealDoc: Doc = if (reveal) "reveal" else emptyDoc
revealDoc <+> showExpr(recv) <> dot <> meth.name <> parens(showExprList(args))

case PureClosureCall(closure, args, spec, _) => showExpr(closure) <> parens(showExprList(args)) <+> "as" <+> showClosureSpec(spec)

Expand Down Expand Up @@ -681,8 +687,9 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
}

override def showPureFunction(f: PureFunction): Doc = f match {
case PureFunction(name, args, results, pres, posts, measures, _) =>
"pure func" <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
case PureFunction(name, args, results, pres, posts, measures, _, 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))
}

Expand All @@ -693,8 +700,9 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
}

override def showPureMethod(m: PureMethod): Doc = m match {
case PureMethod(receiver, name, args, results, pres, posts, measures, _) =>
"pure func" <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
case PureMethod(receiver, name, args, results, pres, posts, measures, _, isOpaque) =>
val funcPrefix = if (isOpaque) "pure opaque func" else "pure func"
funcPrefix <+> parens(showVarDecl(receiver)) <+> name.name <> parens(showFormalArgList(args)) <+> parens(showVarDeclList(results)) <>
spec(showPreconditions(pres) <> showPostconditions(posts) <> showTerminationMeasures(measures))
}

Expand Down
14 changes: 4 additions & 10 deletions src/main/scala/viper/gobra/translator/encodings/defaults/DefaultPureMethodEncoding.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,7 @@ class DefaultPureMethodEncoding extends Encoding {
require(meth.results.size == 1)

val (pos, info, errT) = meth.vprMeta

if (meth.isOpaque) {
info = VprInfo.attachOpaque(info)
}
val annotatedInfo = VprInfo.maybeAttachOpaque(info, meth.isOpaque)

val vRecv = ctx.variable(meth.receiver)
val vRecvPres = ctx.varPrecondition(meth.receiver).toVector
Expand Down Expand Up @@ -67,7 +64,7 @@ class DefaultPureMethodEncoding extends Encoding {
pres = pres ++ measures,
posts = posts,
body = body
)(pos, info, errT)
)(pos, annotatedInfo, errT)

} yield function
}
Expand All @@ -76,10 +73,7 @@ class DefaultPureMethodEncoding extends Encoding {
require(func.results.size == 1)

val (pos, info, errT) = func.vprMeta

if (func.isOpaque) {
info = VprInfo.attachOpaque(info)
}
val annotatedInfo = VprInfo.maybeAttachOpaque(info, func.isOpaque)

val vArgs = func.args.map(ctx.variable)
val vArgPres = func.args.flatMap(ctx.varPrecondition)
Expand Down Expand Up @@ -113,7 +107,7 @@ class DefaultPureMethodEncoding extends Encoding {
pres = pres ++ measures,
posts = posts,
body = body
)(pos, info, errT)
)(pos, annotatedInfo, errT)

} yield function
}
Expand Down
14 changes: 4 additions & 10 deletions src/main/scala/viper/gobra/translator/encodings/typeless/CallEncoding.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,31 +24,25 @@ class CallEncoding extends Encoding {
override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
case x@in.PureFunctionCall(func, args, typ, reveal) =>
val (pos, info, errT) = x.vprMeta

if (reveal) {
info = VprInfo.attachReveal(info)
}
val annotatedInfo = VprInfo.maybeAttachReveal(info, reveal)

val resultType = ctx.typ(typ)

for {
vArgs <- sequence(args map ctx.expression)
app = vpr.FuncApp(func.name, vArgs)(pos, info, resultType, errT)
app = vpr.FuncApp(func.name, vArgs)(pos, annotatedInfo, resultType, errT)
} yield app

case x@in.PureMethodCall(recv, meth, args, typ, reveal) =>
val (pos, info, errT) = x.vprMeta

if (reveal) {
info = VprInfo.attachReveal(info)
}
val annotatedInfo = VprInfo.maybeAttachReveal(info, reveal)

val resultType = ctx.typ(typ)

for {
vRecv <- ctx.expression(recv)
vArgs <- sequence(args map ctx.expression)
app = vpr.FuncApp(meth.uniqueName, vRecv +: vArgs)(pos, info, resultType, errT)
app = vpr.FuncApp(meth.uniqueName, vRecv +: vArgs)(pos, annotatedInfo, resultType, errT)
} yield app
}

Expand Down
16 changes: 12 additions & 4 deletions src/main/scala/viper/gobra/translator/util/VprInfo.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,20 @@ package viper.gobra.translator.util
import viper.silver.{ast => vpr}

object VprInfo {
def attachOpaque(info: vpr.Info): vpr.Info = {
attachAnnotation(info, "opaque")
def maybeAttachOpaque(info: vpr.Info, isOpaque: Boolean): vpr.Info = {
if (isOpaque) {
attachAnnotation(info, "opaque")
} else {
info
}
}

def attachReveal(info: vpr.Info): vpr.Info = {
attachAnnotation(info, "reveal")
def maybeAttachReveal(info: vpr.Info, reveal: Boolean): vpr.Info = {
if (reveal) {
attachAnnotation(info, "reveal")
} else {
info
}
}

private def attachAnnotation(info: vpr.Info, key: String, values: String*) : vpr.Info = {
Expand Down

0 comments on commit 6f8f3f3

Please sign in to comment.