Skip to content

Commit 1df0f34

Browse files
committed
Added several changes to allow for FastParse 2.2.2.
1 parent 3766bf6 commit 1df0f34

35 files changed

Lines changed: 156 additions & 167 deletions

src/main/scala/viper/silver/ast/Ast.scala

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ Some design choices:
4848
* Note that all but Program are transitive subtypes of `Node` via `Hashable`. The reason is
4949
* that AST node hashes may depend on the entire program, not just their sub-AST.
5050
*/
51-
trait Node extends Traversable[Node] with Rewritable {
51+
trait Node extends Iterable[Node] with Rewritable {
5252

5353
/** @see [[Nodes.subnodes()]] */
5454
def subnodes = Nodes.subnodes(this)
@@ -61,36 +61,54 @@ trait Node extends Traversable[Node] with Rewritable {
6161
Visitor.reduceWithContext(this, Nodes.subnodes)(context, enter, combine)
6262
}
6363

64+
override def iterator: Iterator[Node] = {
65+
val iterator = new Iterator[Node] {
66+
var remaining = Seq[Node]().empty
67+
68+
override def hasNext: Boolean = remaining.nonEmpty
69+
70+
override def next(): Node = {
71+
val result = remaining.head
72+
remaining = remaining.tail
73+
result
74+
}
75+
}
76+
77+
Visitor.visit(this, Nodes.subnodes) { case n: Node => iterator.remaining ++= Seq(n) }
78+
79+
iterator
80+
}
81+
6482
/** Applies the function `f` to the AST node, then visits all subnodes. */
65-
def foreach[A](f: Node => A) = Visitor.visit(this, Nodes.subnodes) { case a: Node => f(a) }
83+
//? override def foreach[A](f: Node => A) = Visitor.visit(this, Nodes.subnodes) { case a: Node => f(a) }
6684

6785
/** @see [[Visitor.visit()]] */
68-
def visit[A](f: PartialFunction[Node, A]) {
86+
def visit[A](f: PartialFunction[Node, A]): Unit = {
6987
Visitor.visit(this, Nodes.subnodes)(f)
7088
}
7189

7290
/** @see [[Visitor.visitWithContext()]] */
73-
def visitWithContext[C](c: C)(f: C => PartialFunction[Node, C]) {
91+
def visitWithContext[C](c: C)(f: C => PartialFunction[Node, C]): Unit = {
7492
Visitor.visitWithContext(this, Nodes.subnodes, c)(f)
7593
}
7694

7795
/** @see [[Visitor.visitWithContextManually()]] */
78-
def visitWithContextManually[C, A](c: C)(f: C => PartialFunction[Node, A]) {
96+
def visitWithContextManually[C, A](c: C)(f: C => PartialFunction[Node, A]): Unit = {
7997
Visitor.visitWithContextManually(this, Nodes.subnodes, c)(f)
8098
}
8199

82100
/** @see [[Visitor.visit()]] */
83-
def visit[A](f1: PartialFunction[Node, A], f2: PartialFunction[Node, A]) {
101+
def visit[A](f1: PartialFunction[Node, A], f2: PartialFunction[Node, A]): Unit = {
84102
Visitor.visit(this, Nodes.subnodes, f1, f2)
85103
}
86104

87105
/** @see [[Visitor.visitOpt()]] */
88-
def visitOpt(f: Node => Boolean) {
106+
def visitOpt(f: Node => Boolean): Unit = {
89107
Visitor.visitOpt(this, Nodes.subnodes)(f)
90108
}
91109

92110
/** @see [[Visitor.visitOpt()]] */
93-
def visitOpt[A](f1: Node => Boolean, f2: Node => A) {
111+
def visitOpt[A](f1: Node => Boolean, f2: Node => A): Unit = {
94112
Visitor.visitOpt(this, Nodes.subnodes, f1, f2)
95113
}
96114

src/main/scala/viper/silver/ast/utility/Consistency.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,17 @@ import viper.silver.{FastMessage, FastMessaging}
1515
/** An utility object for consistency checking. */
1616
object Consistency {
1717
var messages: FastMessaging.Messages = Nil
18-
def recordIfNot(suspect: Positioned, property: Boolean, message: String) {
18+
def recordIfNot(suspect: Positioned, property: Boolean, message: String): Unit = {
1919
if (!property) {
2020
val pos = suspect.pos
2121

2222
this.messages ++= FastMessaging.aMessage(FastMessage(message,pos)) // this is the way to construct a message directly with a position (only).
2323
}
2424
}
2525

26-
def resetMessages() { this.messages = Nil }
26+
def resetMessages(): Unit = { this.messages = Nil }
2727
@inline
28-
def recordIf(suspect: Positioned, property: Boolean, message: String) =
28+
def recordIf(suspect: Positioned, property: Boolean, message: String): Unit =
2929
recordIfNot(suspect, !property, message)
3030

3131
/** Names that are not allowed for use in programs. */

src/main/scala/viper/silver/ast/utility/Functions.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ object Functions {
3535
graph.addVertex(f)
3636
}
3737

38-
def process(f: Function, e: Exp) {
38+
def process(f: Function, e: Exp): Unit = {
3939
e visit {
4040
case FuncApp(f2name, _) =>
4141
graph.addEdge(f, program.findFunction(f2name))
@@ -156,7 +156,7 @@ object Functions {
156156
def recursiveCallsAndSurroundingUnfoldings(f : Function) : Seq[(FuncApp,Seq[Unfolding])] = {
157157
var result: Seq[(FuncApp, Seq[Unfolding])] = Seq()
158158

159-
def recordCallsAndUnfoldings(e: Node, ufs: Seq[Unfolding]) {
159+
def recordCallsAndUnfoldings(e: Node, ufs: Seq[Unfolding]): Unit = {
160160
e.shallowCollect {
161161
case Let(v, e, bod) => recordCallsAndUnfoldings(e.replace(e, bod), ufs)
162162
case uf@Unfolding (acc, body) =>

src/main/scala/viper/silver/ast/utility/GenericAxiomRewriter.scala

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,13 +59,10 @@ abstract class GenericAxiomRewriter[Type <: AnyRef,
5959

6060
protected def fresh(name: String, typ: Type): Var
6161

62-
@scala.annotation.elidable(level = scala.annotation.elidable.ASSERTION)
6362
protected def log(message: String): Unit
6463

65-
@scala.annotation.elidable(level = scala.annotation.elidable.ASSERTION)
6664
protected def log(key: String, item: Any): Unit
6765

68-
@scala.annotation.elidable(level = scala.annotation.elidable.ASSERTION)
6966
protected def log(key: String, items: Iterable[Any]): Unit
7067

7168
/*

src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ object QuantifiedPermissions {
100100
private def quantifiedFields(toVisit: mutable.Queue[Member],
101101
collected: mutable.LinkedHashSet[Field],
102102
visited: mutable.Set[Member],
103-
program: Program) {
103+
program: Program): Unit = {
104104

105105
while (toVisit.nonEmpty) {
106106
val root = toVisit.dequeue()
@@ -121,7 +121,7 @@ object QuantifiedPermissions {
121121
private def quantifiedPredicates(toVisit: mutable.Queue[Member],
122122
collected: mutable.LinkedHashSet[Predicate],
123123
visited: mutable.Set[Member],
124-
program: Program) {
124+
program: Program): Unit = {
125125

126126
while (toVisit.nonEmpty) {
127127
val root = toVisit.dequeue()

src/main/scala/viper/silver/ast/utility/Triggers.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -107,9 +107,9 @@ object Triggers {
107107
LocalVar(s"__rw_$name$nextUniqueId", typ)()
108108
}
109109

110-
protected def log(message: String) {}
111-
protected def log(key: String, item: Any) {}
112-
protected def log(key: String, items: Iterable[Any]) {}
110+
protected def log(message: String): Unit = {}
111+
protected def log(key: String, item: Any): Unit = {}
112+
protected def log(key: String, items: Iterable[Any]): Unit = {}
113113
}
114114

115115
object SimpleArithmeticSolver extends GenericArithmeticSolver[Type, Exp, LocalVar, Add, Sub] {

src/main/scala/viper/silver/cfg/CfgTest.scala

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,10 @@ import viper.silver.parser.{FastParser, PProgram, Resolver, Translator}
1313
import viper.silver.verifier.ParseWarning
1414

1515
import scala.io.Source
16+
import fastparse._
1617

1718
object CfgTest {
18-
def main(args: Array[String]): Unit = {
19+
def main[_: P](args: Array[String]): Unit = {
1920
if (args.isEmpty) throw new RuntimeException("No input file specified")
2021
val path = args(0)
2122

@@ -35,7 +36,7 @@ object CfgTest {
3536
}
3637
}
3738

38-
private def parse(input: String, file: Path): Option[PProgram] = {
39+
private def parse[_: P](input: String, file: Path): Option[PProgram] = {
3940
val result = FastParser.parse(input, file)
4041
result match {
4142
case Success(program@PProgram(_, _, _, _, _, _, _,_, errors), _) =>

src/main/scala/viper/silver/components/Components.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ package viper.silver.components
1515
* expected sequence of events (start, stop).
1616
*/
1717
trait LifetimeComponent {
18-
def start()
19-
def stop()
18+
def start(): Unit
19+
def stop(): Unit
2020
}
2121

2222
/** Describes a component that potentially has state which must be taken care
@@ -29,5 +29,5 @@ trait LifetimeComponent {
2929
* expected sequence of events (start, reset, stop).
3030
*/
3131
trait StatefulComponent extends LifetimeComponent {
32-
def reset()
32+
def reset(): Unit
3333
}

src/main/scala/viper/silver/frontend/Frontend.scala

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -25,18 +25,18 @@ import viper.silver.verifier._
2525
trait Frontend {
2626

2727
/** Initialize this translator with a given verifier. Only meant to be called once. */
28-
protected def init(verifier: Verifier)
28+
protected def init(verifier: Verifier): Unit
2929

3030
/**
3131
* Reset the translator, and set the input program. Can be called many times to verify multiple programs
3232
* using the same verifier.
3333
*/
34-
def reset(input: Seq[Path])
34+
def reset(input: Seq[Path]): Unit
3535

3636
/**
3737
* Reset any messages recorded internally (errors from previous program translations, etc.)
3838
*/
39-
def resetMessages()
39+
def resetMessages(): Unit
4040

4141
/**
4242
* Reporter is the message interface which enables (potentially dynamic) feedback from the backend.
@@ -116,25 +116,25 @@ trait DefaultPhases extends Frontend {
116116
val phases = Seq(Parsing, SemanticAnalysis, Translation, ConsistencyCheck, Verification)
117117

118118
/** Parse the program. */
119-
def parsing()
119+
def parsing(): Unit
120120

121121
/** Perform semantic analysis in the program, such as type, names and scope checking. */
122-
def semanticAnalysis()
122+
def semanticAnalysis(): Unit
123123

124124
/** Translate the program to Viper. */
125-
def translation()
125+
def translation(): Unit
126126

127127
/** Perform a consistency check in Viper AST. */
128-
def consistencyCheck()
128+
def consistencyCheck(): Unit
129129

130130
/** Verify the Viper program using a verifier. */
131-
def verification()
131+
def verification(): Unit
132132
}
133133

134134
trait SingleFileFrontend {
135-
def reset(file: Path)
135+
def reset(file: Path): Unit
136136

137-
def reset(files: Seq[Path]) {
137+
def reset(files: Seq[Path]): Unit = {
138138
files match {
139139
case f :: Nil => reset(f)
140140
case _ => sys.error("This frontend can only handle single files.")
@@ -185,12 +185,12 @@ trait DefaultFrontend extends Frontend with DefaultPhases with SingleFileFronten
185185

186186
def getVerificationResult: Option[VerificationResult] = _verificationResult
187187

188-
override def init(verifier: Verifier) {
188+
override def init(verifier: Verifier): Unit = {
189189
_state = DefaultStates.Initialized
190190
_verifier = Some(verifier)
191191
}
192192

193-
override def reset(input: Path) {
193+
override def reset(input: Path): Unit = {
194194
if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.")
195195
_state = DefaultStates.InputSet
196196
_inputFile = Some(input)

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
106106
)
107107

108108
validateOpt(file, ignoreFile) {
109-
case (_, Some(true)) => Right(Unit)
109+
case (_, Some(true)) => Right(())
110110
case (Some(filepath), _) => validateFileOpt(file.name, filepath)
111111
case (optFile, optIgnoreFile) =>
112112
/* Since the file is a trailing argument and thus mandatory, this case
@@ -121,12 +121,12 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
121121
val file = new java.io.File(filepath)
122122
if (!file.isFile) Left(s"Cannot find file '$filepath' from '$optionName' argument")
123123
else if (!file.canRead) Left(s"Cannot read from file '$filepath' from '$optionName' argument'")
124-
else Right(Unit)
124+
else Right(())
125125
}
126126

127127
protected def validateFileOpt(option: ScallopOption[String]): Unit = {
128128
validateOpt(option) {
129-
case None => Right(Unit)
129+
case None => Right(())
130130
case Some(filepath) => validateFileOpt(option.name, filepath)
131131
}
132132
}

0 commit comments

Comments
 (0)