Enable let expressions with weakly pure subexpressions (#678)

* enable non-pure lets

* fix tests

* addressability of let

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

@@ -428,6 +428,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   def showAss(a: Assertion): Doc = updatePositionStore(a) <> (a match {
     case SepAnd(left, right) => showAss(left) <+> "&&" <+> showAss(right)
     case ExprAssertion(exp) => showExpr(exp)
+    case Let(left, right, exp) =>
+      "let" <+> showVar(left) <+> "==" <+> parens(showExpr(right)) <+> "in" <+> showAss(exp)
     case MagicWand(left, right) => showAss(left) <+> "--*" <+> showAss(right)
     case Implication(left, right) => showExpr(left) <+> "==>" <+> showAss(right)
     case Access(e, FullPerm(_)) => "acc" <> parens(showAcc(e))
@@ -462,7 +464,8 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   def showExpr(e: Expr): Doc = updatePositionStore(e) <> (e match {
     case Unfolding(acc, exp) => "unfolding" <+> showAss(acc) <+> "in" <+> showExpr(exp)
 
-    case Let(left, right, exp) => "let" <+> showVar(left) <+> "==" <+> parens(showExpr(right)) <+> "in" <+> showExpr(exp)
+    case PureLet(left, right, exp) =>
+      "let" <+> showVar(left) <+> "==" <+> parens(showExpr(right)) <+> "in" <+> showExpr(exp)
 
     case Old(op, _) => "old" <> parens(showExpr(op))
 

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

@@ -543,10 +543,12 @@ case class Unfolding(acc: Access, in: Expr)(val info: Source.Parser.Info) extend
   require(typ.addressability == Addressability.unfolding(in.typ.addressability))
 }
 
-case class Let(left: LocalVar, right: Expr, in: Expr)(val info: Source.Parser.Info) extends Expr {
+case class PureLet(left: LocalVar, right: Expr, in: Expr)(val info: Source.Parser.Info) extends Expr {
   override def typ: Type = in.typ
 }
 
+case class Let(left: LocalVar, right: Expr, in: Assertion)(val info: Source.Parser.Info) extends Assertion
+
 case class Old(operand: Expr, typ: Type)(val info: Source.Parser.Info) extends Expr
 
 case class LabeledOld(label: LabelProxy, operand: Expr)(val info: Source.Parser.Info) extends Expr {

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

@@ -2446,7 +2446,6 @@ object Desugar extends LazyLogging {
       }
     }
 
-
     private def indexedExprD(base : PExpression, index : PExpression)(ctx : FunctionContext, info : TypeInfo)(src : Meta) : Writer[in.IndexedExp] = {
       for {
         dbase <- exprD(ctx, info)(base)
@@ -2660,14 +2659,6 @@ object Desugar extends LazyLogging {
             val dOp = pureExprD(ctx, info)(op)
             unit(in.Unfolding(dAcc, dOp)(src))
 
-          case PLet(ass, op) =>
-            val dOp = pureExprD(ctx, info)(op)
-            unit((ass.left zip ass.right).foldRight(dOp)((lr, letop) => {
-              val right = pureExprD(ctx, info)(lr._2)
-              val left = in.LocalVar(nm.variable(lr._1.name, info.scope(lr._1), info), right.typ.withAddressability(Addressability.exclusiveVariable))(src)
-              in.Let(left, right, letop)(src)
-            }))
-
           case n : PIndexedExp => indexedExprD(n)(ctx, info)
 
           case PSliceExp(base, low, high, cap) => for {
@@ -4277,6 +4268,17 @@ object Desugar extends LazyLogging {
           wels <- go(els)
         } yield in.Conditional(wcond, wthn, wels, typ)(src)
 
+        case PLet(ass, op) =>
+          val dOp = pureExprD(ctx, info)(op)
+          unit((ass.left zip ass.right).foldRight(dOp)((lr, letop) => {
+            val right = pureExprD(ctx, info)(lr._2)
+            val left = in.LocalVar(
+              nm.variable(lr._1.name, info.scope(lr._1), info),
+              right.typ.withAddressability(Addressability.exclusiveVariable)
+            )(src)
+            in.PureLet(left, right, letop)(src)
+          }))
+
         case PForall(vars, triggers, body) =>
           for { (newVars, newTriggers, newBody) <- quantifierD(ctx, info)(vars, triggers, body)(ctx => exprD(ctx, info)) }
             yield in.PureForall(newVars, newTriggers, newBody)(src)
@@ -4530,6 +4532,19 @@ object Desugar extends LazyLogging {
         case n: PAccess => for {e <- accessibleD(ctx, info)(n.exp); p <- permissionD(ctx, info)(n.perm)} yield in.Access(e, p)(src)
         case n: PPredicateAccess => predicateCallD(ctx, info)(n.pred, n.perm)
 
+        case PLet(ass, op) =>
+          for {
+            dOp <- assertionD(ctx, info)(op)
+            lets = (ass.left zip ass.right).foldRight(dOp)((lr, letop) => {
+              val right = pureExprD(ctx, info)(lr._2)
+              val left = in.LocalVar(
+                nm.variable(lr._1.name, info.scope(lr._1), info),
+                right.typ.withAddressability(Addressability.exclusiveVariable)
+              )(src)
+              in.Let(left, right, letop)(src)
+            })
+          } yield lets
+
         case n: PInvoke =>
           // a predicate invocation corresponds to a predicate access with full permissions
           // register the full permission AST node in the position manager such that its meta information

src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala

@@ -98,6 +98,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
       case _: PPermission => AddrMod.rValue
       case _: PPredConstructor => AddrMod.rValue
       case n: PUnfolding => AddrMod.unfolding(addressability(n.op))
+      case n: PLet => AddrMod.let(addressability(n.op))
       case _: POld | _: PLabeledOld | _: PBefore => AddrMod.old
       case _: PConditional | _: PImplication | _: PForall | _: PExists => AddrMod.rValue
       case _: PAccess | _: PPredicateAccess | _: PMagicWand => AddrMod.rValue

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -74,7 +74,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case n: PClosureImplements => isPureExpr(n.closure) ++ wellDefIfClosureMatchesSpec(n.closure, n.spec)
 
-    case n: PLet => isExpr(n.op).out ++ isPureExpr(n.op) ++
+    case n: PLet => isExpr(n.op).out ++ isWeaklyPureExpr(n.op) ++
       n.ass.right.foldLeft(noMessages)((a, b) => a ++ isPureExpr(b))
 
     case n: PAccess =>

src/main/scala/viper/gobra/theory/Addressability.scala

@@ -119,6 +119,7 @@ object Addressability {
   val mathDataStructureLookup: Addressability = mathDataStructureElement
 
   def unfolding(bodyAddressability: Addressability): Addressability = bodyAddressability
+  def let(bodyAddressability: Addressability): Addressability = bodyAddressability
   val old: Addressability = rValue
   val make: Addressability = Exclusive
   val exprInAcc: Addressability = Exclusive

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

@@ -55,7 +55,7 @@ class AssertionEncoding extends Encoding {
         case errors => Violation.violation(s"invalid trigger pattern (${errors.head.readableMessage})")
       }
 
-    case let: in.Let =>
+    case let: in.PureLet =>
       for {
         exp <- ctx.expression(let.in)
         l = ctx.variable(let.left)
@@ -66,6 +66,12 @@ class AssertionEncoding extends Encoding {
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
     case n@ in.SepAnd(l, r) => for {vl <- ctx.assertion(l); vr <- ctx.assertion(r)} yield withSrc(vpr.And(vl, vr), n)
     case in.ExprAssertion(e) => ctx.expression(e)
+    case n@ in.Let(left, right, op) =>
+      for {
+        exp <- ctx.assertion(op)
+        r <- ctx.expression(right)
+        l = ctx.variable(left)
+      } yield withSrc(vpr.Let(l, r, exp), n)
     case n@ in.MagicWand(l, r) => for {vl <- ctx.assertion(l); vr <- ctx.assertion(r)} yield withSrc(vpr.MagicWand(vl, vr), n)
     case n@ in.Implication(l, r) => for {vl <- ctx.expression(l); vr <- ctx.assertion(r)} yield withSrc(vpr.Implies(vl, vr), n)
 

src/test/resources/regressions/features/let/let_simple.gobra

@@ -32,3 +32,13 @@ func (a *A) g(x int) {
 	fold a.Mem()
 }
 
+pred Q(x int) {
+	true
+}
+
+requires acc(x)
+requires Q(y)
+func impureLets(x *int, y int) {
+	assert let z := y in Q(z)
+	assert let z := x in acc(z)
+}