Merge pull request #704 from viperproject/meilers_seqn_scopes

Fix scope (Seqn) handling in parser and pretty-printer

Author: marcoeilers

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -541,10 +541,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
             case None =>
               nil
             case Some(actualBody) =>
-              braces(nest(defaultIndent,
-                lineIfSomeNonEmpty(actualBody.children) <>
-                ssep(Seq(showStmt(actualBody)), line)
-              ) <> line)
+              showBlock(actualBody)
           })
       case Predicate(name, formalArgs, body) =>
         text("predicate") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <+> (body match {
@@ -634,11 +631,20 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
   }
 
   /** Show some node inside square braces (with nesting). */
-  def showBlock(stmt: Stmt): Cont = {
-    braces(nest(defaultIndent,
-      lineIfSomeNonEmpty(stmt match {case s: Seqn => s.scopedDecls; case _ => Seq()}, stmt.children) <>
-        showStmt(stmt)
-    ) <> line)
+  def showBlock(stmt: Stmt): Cont = stmt match {
+    case Seqn(stmts, scopedDecls) =>
+      val locals = scopedDecls.collect { case l: LocalVarDecl => l }
+      val nonEmptyStmts = stmts.filter {
+        case s@Seqn(ss, sd) => ss.nonEmpty || sd.nonEmpty || s.info.comment.nonEmpty
+        case _ => true
+      }
+      braces(nest(defaultIndent,
+        lineIfSomeNonEmpty(scopedDecls, nonEmptyStmts) <>
+          ssep((locals map (text("var") <+> showVar(_))) ++ (nonEmptyStmts map show), line)) <> line)
+    case s =>
+      braces(nest(defaultIndent,
+        line <> showStmt(s)
+      ))
   }
 
   /** Show a statement. */
@@ -662,6 +668,19 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
           case Nil => call
           case _ => ssep(targets map show, char(',') <> space) <+> ":=" <+> call
         }
+      case Seqn(stmts, scopedDecls) if scopedDecls.nonEmpty =>
+        val locals = scopedDecls.collect {case l: LocalVarDecl => l}
+        val nonEmptyStmts = stmts.filter{
+          case s@Seqn(ss, sd) => ss.nonEmpty || sd.nonEmpty || s.info.comment.nonEmpty
+          case _ => true
+        }
+        if (stmts.isEmpty && locals.isEmpty)
+          nil
+        else {
+          braces(nest(defaultIndent,
+            lineIfSomeNonEmpty(scopedDecls, stmts) <>
+            ssep((locals map (text("var") <+> showVar(_))) ++ (nonEmptyStmts map show), line)) <> line)
+        }
       case seqn@Seqn(stmts, scopedDecls) =>
         val locals = scopedDecls.collect {case l: LocalVarDecl => l}
         if (stmts.isEmpty && locals.isEmpty && seqn.info.comment.isEmpty)
@@ -677,10 +696,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
           nest(defaultIndent,
             showContracts("invariant", invs)
           ) <+> lineIfSomeNonEmpty(invs) <>
-          braces(nest(defaultIndent,
-            lineIfSomeNonEmpty(body.scopedDecls, body.children) <>
-              ssep(Seq(showStmt(body)), line)
-          ) <> line)
+          showBlock(body)
       case If(cond, thn, els) =>
         text("if") <+> parens(show(cond)) <+> showBlock(thn) <> showElse(els)
       case Label(name, invs) =>

src/main/scala/viper/silver/parser/FastParser.scala

@@ -495,17 +495,20 @@ class FastParser {
       })
 
     def linearizeMethod(method: PMethod): PMethod = {
-      def linearizeSeqOfNestedStmt(pseqn: PSeqn): Seq[PStmt] = {
+      def linearizeSeqOfNestedStmt(ss: Seq[PStmt]): Seq[PStmt] = {
         var stmts = Seq.empty[PStmt]
-        pseqn.ss.foreach {
-          case s: PSeqn => stmts = stmts ++ linearizeSeqOfNestedStmt(s)
+        ss.foreach {
+          case s: PMacroSeqn => stmts = stmts ++ linearizeSeqOfNestedStmt(s.ss)
+          case s@PSeqn(ss) => stmts = stmts :+ PSeqn(linearizeSeqOfNestedStmt(ss))(s.pos)
+          case i@PIf(cond, t@PSeqn(thn), e@PSeqn(els)) => stmts = stmts :+ PIf(cond, PSeqn(linearizeSeqOfNestedStmt(thn))(t.pos), PSeqn(linearizeSeqOfNestedStmt(els))(e.pos))(i.pos)
+          case w@PWhile(cond, invs, b@PSeqn(body)) => stmts = stmts :+ PWhile(cond, invs, PSeqn(linearizeSeqOfNestedStmt(body))(b.pos))(w.pos)
           case v => stmts = stmts :+ v
         }
         stmts
       }
 
       val body = method.body match {
-        case Some(s: PSeqn) => Some(PSeqn(linearizeSeqOfNestedStmt(s))(method.pos))
+        case Some(s: PSeqn) => Some(PSeqn(linearizeSeqOfNestedStmt(s.ss))(method.pos))
         case v => v
       }
 
@@ -678,7 +681,10 @@ class FastParser {
     def replacerOnBody(body: PNode, paramToArgMap: Map[String, PExp], pos: (Position, Position)): PNode = {
 
       // Duplicate the body of the macro to allow for differing type checks depending on the context
-      val replicatedBody = body.deepCopyAll
+      val replicatedBody = body.deepCopyAll match {
+        case s@PSeqn(ss) => PMacroSeqn(ss)(s.pos)
+        case b => b
+      }
 
       // Rename locally bound variables in macro's body
       var bodyWithRenamedVars = renamer.execute[PNode](replicatedBody)

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -1215,6 +1215,14 @@ case class PAnnotatedStmt(stmt: PStmt, annotation: (String, Seq[String]))(val po
 
 case class PSeqn(ss: Seq[PStmt])(val pos: (Position, Position)) extends PStmt with PScope
 
+/**
+  * PSeqn representing the expanded body of a statement macro.
+  * Unlike a normal PSeqn, it does not represent its own scope.
+  * Is created only temporarily during macro expansion and eliminated (i.e., expanded into the surrounding scope)
+  * before translation.
+  */
+case class PMacroSeqn(ss: Seq[PStmt])(val pos: (Position, Position)) extends PStmt
+
 case class PFold(e: PExp)(val pos: (Position, Position)) extends PStmt
 
 case class PUnfold(e: PExp)(val pos: (Position, Position)) extends PStmt

src/test/resources/all/issues/silver/0697.vpr

@@ -0,0 +1,32 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main1(b: Bool)
+{
+    if (b) {
+        var x: Int
+        x := 45
+        assert x > 34
+    }
+    {
+      var x: Int
+      x := 45
+      assert x > 34
+    }
+}
+
+method main2(b: Bool)
+{
+    if (b) {
+        //:: ExpectedOutput(consistency.error)
+        var x: Int
+        x := 45
+        assert x > 34
+    }
+
+      var x: Int
+      x := 45
+      assert x > 34
+
+}

src/test/resources/transformations/Macros/Hygienic/collision2Ref.vpr

@@ -12,14 +12,11 @@ define macro2(x, y) {
 
 method main()
 {
-    {
-        var x: Bool
-        x := true
-        assert((true && true) && x)
-    }
-    {
-        var x$0: Bool
-        x$0 := true
-        assert((true && true) && x$0)
-    }
+    var x: Bool
+    x := true
+    assert((true && true) && x)
+
+    var x$0: Bool
+    x$0 := true
+    assert((true && true) && x$0)
 }

src/test/resources/transformations/Macros/Hygienic/collisionRef.vpr

@@ -16,14 +16,11 @@ function x$3() : Bool {
 
 method main()
 {
-    {
-        var x: Bool
-        x := true
-        assert(x)
-    }
-    {
-        var x$2: Bool
-        x$2 := true
-        assert(x$2)
-    }
+    var x: Bool
+    x := true
+    assert(x)
+
+    var x$2: Bool
+    x$2 := true
+    assert(x$2)
 }

src/test/resources/transformations/Macros/Hygienic/loopConstructionRef.vpr

@@ -5,33 +5,32 @@ method main()
 {
     var value:Int
     value := 0
-    {
-        var oldX: Int
-        var ctr: Int
-        oldX := value
-        ctr := 0
-        label loop invariant ctr < 5 && value == oldX + ctr
-        value := value + 1
-        ctr := ctr + 1
-        if(ctr < 5) {
-            goto loop
-        }
-        assert(ctr == 5)
-        assert(oldX + 5 == value)
+
+    var oldX: Int
+    var ctr: Int
+    oldX := value
+    ctr := 0
+    label loop invariant ctr < 5 && value == oldX + ctr
+    value := value + 1
+    ctr := ctr + 1
+    if(ctr < 5) {
+        goto loop
     }
-    {
-        var oldX$0: Int
-        var ctr$0: Int
-        oldX$0 := value
-        ctr$0 := 0
-        label loop$0 invariant ctr$0 < 5 && value == oldX$0 + ctr$0
-        value := value + 1
-        ctr$0 := ctr$0 + 1
-        if(ctr$0 < 5) {
-            goto loop$0
-        }
-        assert(ctr$0 == 5)
-        assert(oldX$0 + 5 == value)
+    assert(ctr == 5)
+    assert(oldX + 5 == value)
+
+    var oldX$0: Int
+    var ctr$0: Int
+    oldX$0 := value
+    ctr$0 := 0
+    label loop$0 invariant ctr$0 < 5 && value == oldX$0 + ctr$0
+    value := value + 1
+    ctr$0 := ctr$0 + 1
+    if(ctr$0 < 5) {
+        goto loop$0
     }
+    assert(ctr$0 == 5)
+    assert(oldX$0 + 5 == value)
+
     assert(value == 10)
 }

src/test/resources/transformations/Macros/Hygienic/nestedRef.vpr

@@ -13,18 +13,11 @@ define macro2(y) {
 
 method main()
 {
-    {
-        var x: Bool := true
-        {
-            var x$0: Bool := false
-            assert(x || x$0)
-        }
-    }
-    {
-        var x$1: Bool := true
-        {
-            var x$2: Bool := false
-            assert(x$1 || x$2)
-        }
-    }
+    var x: Bool := true
+    var x$0: Bool := false
+    assert(x || x$0)
+
+    var x$1: Bool := true
+    var x$2: Bool := false
+    assert(x$1 || x$2)
 }

src/test/resources/transformations/Macros/Hygienic/simpleRef.vpr

@@ -8,12 +8,9 @@ define macro {
 
 method main()
 {
-    {
-        var x: Bool := true
-        assert(x)
-    }
-    {
-        var x$0: Bool := true
-        assert(x$0)
-    }
+    var x: Bool := true
+    assert(x)
+
+    var x$0: Bool := true
+    assert(x$0)
 }