From fae262bfe39f1cf75b84b7f0f01c10650ee6af5c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 18:03:43 +0200 Subject: [PATCH 1/6] Correct parsing and pretty printing of internal scopes --- .../silver/ast/pretty/PrettyPrinter.scala | 42 +++++--- .../viper/silver/parser/FastParser.scala | 13 ++- .../scala/viper/silver/parser/ParseAst.scala | 8 ++ src/test/resources/all/issues/silver/0697.vpr | 31 ++++++ src/test/scala/PrettyPrinterTest.scala | 96 +++++++++++++++++++ 5 files changed, 172 insertions(+), 18 deletions(-) create mode 100644 src/test/resources/all/issues/silver/0697.vpr diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index c879e3bbc..feaef4e0f 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/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, stmts) <> + 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) => diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index d1326b8db..09f73bbda 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -495,17 +495,17 @@ 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 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 +678,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) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 0b7b194e1..d0fcbd3ab 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/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 diff --git a/src/test/resources/all/issues/silver/0697.vpr b/src/test/resources/all/issues/silver/0697.vpr new file mode 100644 index 000000000..bab274abf --- /dev/null +++ b/src/test/resources/all/issues/silver/0697.vpr @@ -0,0 +1,31 @@ +// 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) { + var x: Int + x := 45 + assert x > 34 + } + //:: ExpectedOutput(typechecker.error) + var x: Int + x := 45 + assert x > 34 + +} \ No newline at end of file diff --git a/src/test/scala/PrettyPrinterTest.scala b/src/test/scala/PrettyPrinterTest.scala index 0a6b282f8..243ba29ab 100644 --- a/src/test/scala/PrettyPrinterTest.scala +++ b/src/test/scala/PrettyPrinterTest.scala @@ -8,6 +8,9 @@ import org.scalatest.funsuite.AnyFunSuite import org.scalatest.matchers.should.Matchers import viper.silver.ast._ import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.frontend.{DefaultStates, ViperAstProvider} +import viper.silver.logger.ViperStdOutLogger +import viper.silver.reporter.StdIOReporter class PrettyPrinterTest extends AnyFunSuite with Matchers { test("The comment of nested Seqn-s is printed correctly") { @@ -21,4 +24,97 @@ class PrettyPrinterTest extends AnyFunSuite with Matchers { // In particular, we don't want `printed` to end with a newline. assert(printed == "// " + comment) } + + object AstProvider extends ViperAstProvider(StdIOReporter(), ViperStdOutLogger("AstAnnotationTestsLogger").get) { + def setCode(code: String): Unit = { + _input = Some(code) + } + + override def reset(input: java.nio.file.Path): Unit = { + if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.") + _state = DefaultStates.InputSet + _inputFile = Some(input) + + /** must be set by [[setCode]] */ + // _input = None + _errors = Seq() + _parsingResult = None + _semanticAnalysisResult = None + _verificationResult = None + _program = None + resetMessages() + } + } + + def generateViperAst(code: String): Option[Program] = { + + val code_id = code.hashCode.asInstanceOf[Short].toString + AstProvider.setCode(code) + AstProvider.execute(Array("--ignoreFile", code_id)) + + if (AstProvider.errors.isEmpty) { + Some(AstProvider.translationResult) + } else { + AstProvider.logger.error(s"An error occurred while translating ${AstProvider.errors}") + None + } + } + + test("Pretty printer and parser roundtrip yields same result") { + import viper.silver.ast._ + + val code = + """ + |domain Measures { // used for issue 154 test, see below + | function Measure$contains(Ref, Int): Bool + | function Measure$value(slf: Ref, k: Int): Int + |} + | + |function issue154(self: Ref, key: Int, value: Int): Bool + | ensures result == (Measure$contains(self, key) ==> (Measure$value(self, key) > value)) + | + |function concatFirst(xs: Seq[Int], ys: Seq[Int]): Int { + | (xs ++ ys)[0] // issue #496 + |} + | + |method bodyless() // bodyless method, issue #223 + | + |// scopes, issue #697 + |method test() { + | { + | var index: Int + | index := index + 1 + | index := index + 2 + | var p: Int + | p := 1 / 2 // integer division + | } + | { + | var index: Int + | if (index > 5) { + | index := 56 + | } elseif (index < -56) { + | var index2: Ref + | index := 77 + | } else { + | index := 45 + | while (index != 0) + | invariant index > 23 + | { + | var index2: Ref + | index2 := null + | var m: Map[Bool, Bool] + | m := Map(true := false, false := true) // maps, issue #619 + | } + | } + | } + |} + |""".stripMargin + + val origProgram: Program = generateViperAst(code).get + // Pretty print and reparse + val res = generateViperAst(origProgram.toString()).get + assert(origProgram == res) + } + + } From 7e49e434d6f01d7bfc083ca6557aa6a12303930a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 19:00:19 +0200 Subject: [PATCH 2/6] Adapted tests --- .../silver/ast/pretty/PrettyPrinter.scala | 2 +- .../Macros/Hygienic/collision2Ref.vpr | 17 +++---- .../Macros/Hygienic/collisionRef.vpr | 17 +++---- .../Macros/Hygienic/loopConstructionRef.vpr | 51 +++++++++---------- .../Macros/Hygienic/nestedRef.vpr | 21 +++----- .../Macros/Hygienic/simpleRef.vpr | 13 ++--- src/test/scala/PrettyPrinterTest.scala | 4 +- 7 files changed, 55 insertions(+), 70 deletions(-) diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index feaef4e0f..cb2896faa 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala @@ -639,7 +639,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case _ => true } braces(nest(defaultIndent, - lineIfSomeNonEmpty(scopedDecls, stmts) <> + lineIfSomeNonEmpty(scopedDecls, nonEmptyStmts) <> ssep((locals map (text("var") <+> showVar(_))) ++ (nonEmptyStmts map show), line)) <> line) case s => braces(nest(defaultIndent, diff --git a/src/test/resources/transformations/Macros/Hygienic/collision2Ref.vpr b/src/test/resources/transformations/Macros/Hygienic/collision2Ref.vpr index 8ac8bba4b..2c5b25241 100644 --- a/src/test/resources/transformations/Macros/Hygienic/collision2Ref.vpr +++ b/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) } \ No newline at end of file diff --git a/src/test/resources/transformations/Macros/Hygienic/collisionRef.vpr b/src/test/resources/transformations/Macros/Hygienic/collisionRef.vpr index 4961e7df5..bd0e477c4 100644 --- a/src/test/resources/transformations/Macros/Hygienic/collisionRef.vpr +++ b/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) } \ No newline at end of file diff --git a/src/test/resources/transformations/Macros/Hygienic/loopConstructionRef.vpr b/src/test/resources/transformations/Macros/Hygienic/loopConstructionRef.vpr index 885f730bc..003e3f0e9 100644 --- a/src/test/resources/transformations/Macros/Hygienic/loopConstructionRef.vpr +++ b/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) } \ No newline at end of file diff --git a/src/test/resources/transformations/Macros/Hygienic/nestedRef.vpr b/src/test/resources/transformations/Macros/Hygienic/nestedRef.vpr index 59f8088c5..673e1c141 100644 --- a/src/test/resources/transformations/Macros/Hygienic/nestedRef.vpr +++ b/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) } \ No newline at end of file diff --git a/src/test/resources/transformations/Macros/Hygienic/simpleRef.vpr b/src/test/resources/transformations/Macros/Hygienic/simpleRef.vpr index 0b5d62aba..ed23b0d3f 100644 --- a/src/test/resources/transformations/Macros/Hygienic/simpleRef.vpr +++ b/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) } \ No newline at end of file diff --git a/src/test/scala/PrettyPrinterTest.scala b/src/test/scala/PrettyPrinterTest.scala index 243ba29ab..df8510e2b 100644 --- a/src/test/scala/PrettyPrinterTest.scala +++ b/src/test/scala/PrettyPrinterTest.scala @@ -113,7 +113,9 @@ class PrettyPrinterTest extends AnyFunSuite with Matchers { val origProgram: Program = generateViperAst(code).get // Pretty print and reparse val res = generateViperAst(origProgram.toString()).get - assert(origProgram == res) + val origString = origProgram.toString() + val resString = res.toString() + assert(origString == resString) } From ccef9f15689bee60f7624e01474b86edad273a3a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 19:43:15 +0200 Subject: [PATCH 3/6] Transforming nested Seqns --- src/main/scala/viper/silver/parser/FastParser.scala | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 09f73bbda..7008a93d6 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -499,6 +499,9 @@ class FastParser { var stmts = Seq.empty[PStmt] ss.foreach { case s: PMacroSeqn => stmts = stmts ++ linearizeSeqOfNestedStmt(s.ss) + case s@PSeqn(ss) => stmts :+ PSeqn(linearizeSeqOfNestedStmt(ss))(s.pos) + case i@PIf(cond, t@PSeqn(thn), e@PSeqn(els)) => stmts :+ PIf(cond, PSeqn(linearizeSeqOfNestedStmt(thn))(t.pos), PSeqn(linearizeSeqOfNestedStmt(els))(e.pos))(i.pos) + case w@PWhile(cond, invs, b@PSeqn(body)) => stmts :+ PWhile(cond, invs, PSeqn(linearizeSeqOfNestedStmt(body))(b.pos))(w.pos) case v => stmts = stmts :+ v } stmts From 4ab85692f588fabdfff29e72b705138a3a2718de Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 20:13:53 +0200 Subject: [PATCH 4/6] Fixing nested transformation --- src/main/scala/viper/silver/parser/FastParser.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index 7008a93d6..e185c2b5d 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -499,9 +499,9 @@ class FastParser { var stmts = Seq.empty[PStmt] ss.foreach { case s: PMacroSeqn => stmts = stmts ++ linearizeSeqOfNestedStmt(s.ss) - case s@PSeqn(ss) => stmts :+ PSeqn(linearizeSeqOfNestedStmt(ss))(s.pos) - case i@PIf(cond, t@PSeqn(thn), e@PSeqn(els)) => stmts :+ PIf(cond, PSeqn(linearizeSeqOfNestedStmt(thn))(t.pos), PSeqn(linearizeSeqOfNestedStmt(els))(e.pos))(i.pos) - case w@PWhile(cond, invs, b@PSeqn(body)) => stmts :+ PWhile(cond, invs, PSeqn(linearizeSeqOfNestedStmt(body))(b.pos))(w.pos) + 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 From adc2855cea4b0d016df5b7a7b651587c07517683 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 20:50:08 +0200 Subject: [PATCH 5/6] Fixed test annotation --- src/test/resources/all/issues/silver/0697.vpr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/resources/all/issues/silver/0697.vpr b/src/test/resources/all/issues/silver/0697.vpr index bab274abf..04877fb46 100644 --- a/src/test/resources/all/issues/silver/0697.vpr +++ b/src/test/resources/all/issues/silver/0697.vpr @@ -23,7 +23,7 @@ method main2(b: Bool) x := 45 assert x > 34 } - //:: ExpectedOutput(typechecker.error) + //:: ExpectedOutput(consistency.error) var x: Int x := 45 assert x > 34 From 8490c55045363aa038e4b48c2b2d5fce2ab991bd Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 21 May 2023 21:10:43 +0200 Subject: [PATCH 6/6] Fixed test annotation --- src/test/resources/all/issues/silver/0697.vpr | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/test/resources/all/issues/silver/0697.vpr b/src/test/resources/all/issues/silver/0697.vpr index 04877fb46..a1db01682 100644 --- a/src/test/resources/all/issues/silver/0697.vpr +++ b/src/test/resources/all/issues/silver/0697.vpr @@ -19,11 +19,12 @@ method main1(b: Bool) method main2(b: Bool) { if (b) { + //:: ExpectedOutput(consistency.error) var x: Int x := 45 assert x > 34 } - //:: ExpectedOutput(consistency.error) + var x: Int x := 45 assert x > 34