Improve language flexibility

Author: JonasAlaif

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

@@ -446,6 +446,8 @@ case class FieldAccess(rcv: Exp, field: Field)
   def getArgs: Seq[Exp] = Seq(rcv)
   def withArgs(args: Seq[Exp]): FieldAccess = copy(rcv = args.head, field)(pos, info, errT)
 //  def asManifestation: Exp = this
+
+  override def name: String = field.name
 }
 
 /** A predicate access expression. See also companion object below for an alternative creation signature */
@@ -1257,7 +1259,9 @@ sealed abstract class DomainUnExp(val funct: UnOp) extends PrettyUnaryExpression
 }
 
 /** Expressions which can appear on the left hand side of an assignment */
-sealed trait Lhs extends Exp
+sealed trait Lhs extends Exp {
+  def name: String
+}
 
 /** Generic Expression to use to extend the AST.
   * New expression-typed AST nodes can be defined by creating new case classes extending this trait.

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

@@ -38,48 +38,22 @@ sealed trait Stmt extends Hashable with Infoed with Positioned with Transformabl
 }
 
 /** A statement that creates a new object and assigns it to a local variable. */
-case class NewStmt(lhs: LocalVar, fields: Seq[Field])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt {
+case class NewStmt[T <: Lhs](lhs: T, fields: Seq[Field])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt {
   override lazy val check : Seq[ConsistencyError] =
     (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq()) ++
     (if(!(Ref isSubtype lhs)) Seq(ConsistencyError(s"Left-hand side of New statement must be Ref type, but found ${lhs.typ}", lhs.pos)) else Seq())
-
-}
-
-/** An assignment to a field or a local variable */
-sealed trait AbstractAssign extends Stmt {
-
-  def lhs: Lhs
-
-  def rhs: Exp
-}
-
-object AbstractAssign {
-  def apply(lhs: Lhs, rhs: Exp)(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) = lhs match {
-    case l: LocalVar => LocalVarAssign(l, rhs)(pos, info, errT)
-    case l: FieldAccess => FieldAssign(l, rhs)(pos, info, errT)
-  }
-
-  def unapply(a: AbstractAssign) = Some((a.lhs, a.rhs))
-}
-
-/** An assignment to a local variable. */
-case class LocalVarAssign(lhs: LocalVar, rhs: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AbstractAssign{
-  override lazy val check : Seq[ConsistencyError] =
-    (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq()) ++
-    Consistency.checkPure(rhs) ++
-    (if(!Consistency.isAssignable(rhs, lhs)) Seq(ConsistencyError(s"Right-hand side $rhs is not assignable to left-hand side $lhs.", lhs.pos)) else Seq())
 }
 
-/** An assignment to a field variable. */
-case class FieldAssign(lhs: FieldAccess, rhs: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AbstractAssign{
+/** An assignment to a field or a local variable. */
+case class Assign[T <: Lhs](lhs: T, rhs: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt {
   override lazy val check : Seq[ConsistencyError] =
     (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq()) ++
     Consistency.checkPure(rhs) ++
     (if(!Consistency.isAssignable(rhs, lhs)) Seq(ConsistencyError(s"Right-hand side $rhs is not assignable to left-hand side $lhs.", lhs.pos)) else Seq())
 }
 
 /** A method call. */
-case class MethodCall(methodName: String, args: Seq[Exp], targets: Seq[LocalVar])(val pos: Position, val info: Info, val errT: ErrorTrafo) extends Stmt {
+case class MethodCall(methodName: String, args: Seq[Exp], targets: Seq[Lhs])(val pos: Position, val info: Info, val errT: ErrorTrafo) extends Stmt {
   override lazy val check : Seq[ConsistencyError] = {
     var s = Seq.empty[ConsistencyError]
     if(!Consistency.noResult(this))
@@ -92,7 +66,7 @@ case class MethodCall(methodName: String, args: Seq[Exp], targets: Seq[LocalVar]
 }
 
 object MethodCall {
-  def apply(method: Method, args: Seq[Exp], targets: Seq[LocalVar])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): MethodCall = {
+  def apply(method: Method, args: Seq[Exp], targets: Seq[Lhs])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): MethodCall = {
     MethodCall(method.name, args, targets)(pos, info, errT)
   }
 }

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

@@ -645,9 +645,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
   def showStmt(stmt: Stmt): Cont = {
     val stmtDoc = stmt match {
       case NewStmt(target, fields) =>
-        show(target) <+> ":=" <+> "new(" <> ssep(fields map (f => value(f.name)), char(',') <> space) <> ")"
-      case LocalVarAssign(lhs, rhs) => show(lhs) <+> ":=" <+> nest(defaultIndent, show(rhs))
-      case FieldAssign(lhs, rhs) => show(lhs) <+> ":=" <+> nest(defaultIndent, show(rhs))
+        show(target) <+> ":=" <+> text("new") <> parens(ssep(fields map (f => value(f.name)), char(',') <> space))
+      case Assign(lhs, rhs) => show(lhs) <+> ":=" <+> nest(defaultIndent, show(rhs))
       case Fold(e) => text("fold") <+> nest(defaultIndent, show(e))
       case Unfold(e) => text("unfold") <+> nest(defaultIndent, show(e))
       case Package(e, proofScript) => text("package") <+> show(e) <+> showBlock(proofScript)

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

@@ -127,7 +127,7 @@ object Consistency {
   def nullValue[T](a: T, b: T) = if (a != null) a else b
 
   /**
-   * Checks that this boolean expression is pure i.e. it contains no magic wands, access predicates or ghost operations.
+   * Checks that this boolean expression is pure i.e. it contains no magic wands or access predicates.
    */
   def checkPure(e: Exp): Seq[ConsistencyError] = {
     if(!e.isPure){
@@ -165,13 +165,13 @@ object Consistency {
     val argVars = args.map(_.localVar).toSet
     var s = Seq.empty[ConsistencyError]
 
-    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l)) {
+    for (a@Assign(l: LocalVar, _) <- b if argVars.contains(l)) {
       s :+= ConsistencyError(s"$a is a reassignment of formal argument $l.", a.pos)
     }
-    for (c@MethodCall(_, _, targets) <- b; t <- targets if argVars.contains(t)) {
+    for (c@MethodCall(_, _, targets) <- b; t@LocalVar(_, _) <- targets if argVars.contains(t)) {
       s :+= ConsistencyError(s"$c is a reassignment of formal argument $t.", c.pos)
     }
-    for (n@NewStmt(l, _) <- b if argVars.contains(l)){
+    for (n@NewStmt(l: LocalVar, _) <- b if argVars.contains(l)){
       s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
     }
     s
@@ -387,13 +387,13 @@ object Consistency {
 
   private def checkMagicWandProofScript(script: Stmt, locals: Seq[LocalVarDecl]): Seq[ConsistencyError] =
     script.shallowCollect({
-      case fa: FieldAssign =>
+      case Assign(fa: FieldAccess, _) =>
         Some(ConsistencyError("Field assignments are not allowed in magic wand proof scripts.", fa.pos))
-      case ne: NewStmt =>
-        Some(ConsistencyError("New statements statements are not allowed in magic wand proof scripts.", ne.pos))
+      case ne: NewStmt[_] =>
+        Some(ConsistencyError("New statements are not allowed in magic wand proof scripts.", ne.pos))
       case wh: While =>
         Some(ConsistencyError("While statements are not allowed in magic wand proof scripts.", wh.pos))
-      case loc @ LocalVarAssign(LocalVar(varName, _), _) if !locals.exists(_.name == varName) =>
+      case loc @ Assign(LocalVar(varName, _), _) if !locals.exists(_.name == varName) =>
         Some(ConsistencyError("Can only assign to local variables that were declared inside the proof script.", loc.pos))
       case _: Package => None
     }).flatten

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

@@ -49,8 +49,7 @@ object Nodes {
       case s: Stmt =>
         s match {
           case NewStmt(target, fields) => Seq(target) ++ fields
-          case LocalVarAssign(lhs, rhs) => Seq(lhs, rhs)
-          case FieldAssign(lhs, rhs) => Seq(lhs, rhs)
+          case Assign(lhs, rhs) => Seq(lhs, rhs)
           case Fold(e) => Seq(e)
           case Unfold(e) => Seq(e)
           case Package(e, proofScript) => Seq(e, proofScript)

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

@@ -79,9 +79,9 @@ object Statements {
     var writtenTo = Seq[LocalVar]()
 
     s visit {
-      case LocalVarAssign(lhs, _) => writtenTo = lhs +: writtenTo
-      case MethodCall(_, _, targets) => writtenTo = writtenTo ++ targets
-      case NewStmt(target, _) => writtenTo = target +: writtenTo
+      case Assign(lhs: LocalVar, _) => writtenTo = lhs +: writtenTo
+      case MethodCall(_, _, targets) => writtenTo = writtenTo ++ targets collect { case t: LocalVar => t }
+      case NewStmt(target: LocalVar, _) => writtenTo = target +: writtenTo
       case While(_, _, body) => writtenTo = writtenTo ++ (writtenVars(body) intersect s.undeclLocalVars)
     }
 

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

@@ -215,16 +215,15 @@ object CfgGenerator {
         val label = TmpLabel(name)
         addLabel(label)
         addStatement(WrappedStmt(stmt))
-      case _: LocalVarAssign |
-           _: FieldAssign |
+      case _: Assign[_] |
            _: Inhale |
            _: Exhale |
            _: Fold |
            _: Unfold |
            _: Package |
            _: Apply |
            _: MethodCall |
-           _: NewStmt |
+           _: NewStmt[_] |
            _: Assert |
            _: LocalVarDeclStmt |
            _: Assume |

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

@@ -750,20 +750,23 @@ class FastParser {
     val expander = StrategyBuilder.Ancestor[PNode] {
 
       // Handles macros on the left hand-side of assignments
-      case (PMacroAssign(call, exp), ctx) =>
-        if (!isMacro(call.opName))
-          throw ParseException("The only calls that can be on the left-hand side of an assignment statement are calls to macros", call.pos._1)
-
-        val body = ExpandMacroIfValid(call, ctx)
-
-        // Check if macro's body can be the left-hand side of an assignment and,
-        // if that's the case, add it in a corresponding assignment statement
-        body match {
-          case fa: PFieldAccess =>
-            val node = PFieldAssign(fa, exp)(fa.pos)
-            (node, ctx)
-          case _ => throw ParseException("The body of this macro is not a suitable left-hand side for an assignment statement", call.pos._1)
+      case (assign@PAssign(targets, rhs), ctx) =>
+        val expandedTargets = targets map {
+          case call: PCall => {
+            if (!isMacro(call.opName))
+              throw ParseException("The only calls that can be on the left-hand side of an assignment statement are calls to macros", call.pos._1)
+            val body = ExpandMacroIfValid(call, ctx)
+
+            // Check if macro's body can be the left-hand side of an assignment and,
+            // if that's the case, add it in a corresponding assignment statement
+            body match {
+              case target: PAssignTarget => target
+              case _ => throw ParseException("The body of this macro is not a suitable left-hand side for an assignment statement", call.pos._1)
+            }
+          }
+          case target => target
         }
+        (PAssign(expandedTargets, rhs)(assign.pos), ctx)
 
       // Handles all other calls to macros
       case (node, ctx) => (ExpandMacroIfValid(node, ctx), ctx)
@@ -800,7 +803,7 @@ class FastParser {
     | setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty
     | size | explicitSeqNonEmpty | seqRange
     | mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange
-    | fapp | idnuse | ParserExtension.newExpAtEnd(ctx))
+    | newExp | fapp | idnuse | ParserExtension.newExpAtEnd(ctx))
 
   def result[$: P]: P[PResultLit] = FP(keyword("result")).map { case (pos, _) => PResultLit()(pos) }
 
@@ -1085,6 +1088,10 @@ class FastParser {
     case (pos, e) => PMapRange(e)(pos)
   })
 
+  def newExp[$: P]: P[PNewExp] = FP("new" ~ "(" ~ newExpFields ~ ")").map { case (pos, fields) => PNewExp(fields)(pos) }
+
+  def newExpFields[$: P]: P[Option[Seq[PIdnUse]]] = P(idnuse.rep(sep = ",")).map(Some(_)) | P("*").map(_ => None)
+
   def fapp[$: P]: P[PCall] = FP(idnuse ~ parens(actualArgList)).map {
     case (pos, (func, args)) =>
       PCall(func, args, None)(pos)
@@ -1094,23 +1101,21 @@ class FastParser {
     case (pos, (func, args, typeGiven)) => PCall(func, args, Some(typeGiven))(pos)
   }
 
-  def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | macroassign | fieldassign | localassign | fold | unfold | exhale | assertP |
-    inhale | assume | ifthnels | whle | varDecl | defineDecl | newstmt | 
-    methodCall | goto | lbl | packageWand | applyWand | macroref | block |
+  def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fold | unfold | exhale | assertP |
+    inhale | assume | ifthnels | whle | varDecl | defineDecl | 
+    goto | lbl | packageWand | applyWand | assign | macroref | block |
     quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
 
-  def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fieldassign | localassign | fold | unfold | exhale | assertP |
-    inhale | assume | ifthnels | whle | varDecl | newstmt |
-    methodCall | goto | lbl | packageWand | applyWand | macroref | block |
+  def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fold | unfold | exhale | assertP |
+    inhale | assume | ifthnels | whle | varDecl |
+    goto | lbl | packageWand | applyWand | assign | macroref | block |
     quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
 
   def macroref[$: P]: P[PMacroRef] = FP(idnuse).map { case (pos, a) => PMacroRef(a)(pos) }
 
-  def fieldassign[$: P]: P[PFieldAssign] = FP(fieldAcc ~ ":=" ~ exp).map { case (pos, (a, b)) => PFieldAssign(a, b)(pos) }
-
-  def macroassign[$: P]: P[PMacroAssign] = FP(NoCut(fapp) ~ ":=" ~ exp).map { case (pos, (call, exp)) => PMacroAssign(call, exp)(pos) }
+  def assignTarget[$: P]: P[PAssignTarget] = fieldAcc | NoCut(fapp) | idnuse
 
-  def localassign[$: P]: P[PVarAssign] = FP(idnuse ~ ":=" ~ exp).map { case (pos, (a, b)) => PVarAssign(a, b)(pos) }
+  def assign[$: P]: P[PAssign] = FP((assignTarget.rep(min = 1, sep = ",") ~ ":=").? ~ exp).map { case (pos, (targets, rhs)) => PAssign(targets.getOrElse(Seq()), rhs)(pos) }
 
   def fold[$: P]: P[PFold] = FP("fold" ~ predicateAccessPred).map{ case (pos, e) => PFold(e)(pos)}
 
@@ -1170,7 +1175,9 @@ class FastParser {
 
   def inv(implicit ctx : P[_]) : P[PExp] = P((keyword("invariant") ~ exp ~~~ ";".lw.?) | ParserExtension.invSpecification(ctx))
 
-  def varDecl[$: P]: P[PLocalVarDecl] = FP(keyword("var") ~/ idndef ~ ":" ~ typ ~~~ (":=" ~ exp).lw.?).map { case (pos, (a, b, c)) => PLocalVarDecl(a, b, c)(pos) }
+  def varDecl[$: P]: P[PLocalVarDecl] = FP(keyword("var") ~/ nonEmptyFormalArgList ~~~ (":=" ~ exp).lw.?).map {
+    case (pos, (a, b)) => PLocalVarDecl(a, b.map(i => PAssign(a.map(v => PIdnUse(v.idndef.name)(v.idndef.pos)), i)(pos)))(pos)
+  }
 
   def defineDecl[$: P]: P[PDefine] = FP(keyword("define") ~/ idndef ~ ("(" ~ idndef.rep(sep = ",") ~ ")").? ~ (exp | "{" ~ (nodefinestmt ~ ";".?).rep ~ "}")).map {
     case (pos, (a, b, c)) => c match {
@@ -1179,19 +1186,6 @@ class FastParser {
     }
   }
 
-  def newstmt[$: P]: P[PNewStmt] = starredNewstmt | regularNewstmt
-
-  def regularNewstmt[$: P]: P[PRegularNewStmt] = FP(idnuse ~ ":=" ~ "new" ~ "(" ~ idnuse.rep(sep = ",") ~ ")").map { case (pos, (a, b)) => PRegularNewStmt(a, b)(pos) }
-
-  def starredNewstmt[$: P]: P[PStarredNewStmt] = FP(idnuse ~ ":=" ~ "new" ~ "(" ~ "*" ~ ")").map{ case (pos, e) => PStarredNewStmt(e)(pos) }
-
-  def methodCall[$: P]: P[PMethodCall] = FP((idnuse.rep(sep = ",") ~ ":=").? ~ idnuse ~ parens(exp.rep(sep = ","))).map {
-    case (pos, (None, method, args)) =>
-      PMethodCall(Nil, method, args)(pos)
-    case (pos, (Some(targets), method, args)) =>
-      PMethodCall(targets, method, args)(pos)
-  }
-
   def goto[$: P]: P[PGoto] = FP("goto" ~/ idnuse).map{ case (pos, e) => PGoto(e)(pos) }
 
   def lbl[$: P]: P[PLabel] = FP(keyword("label") ~/ idndef ~~~ (keyword("invariant") ~/ exp).lw.rep).map {
@@ -1264,8 +1258,6 @@ class FastParser {
 
   def unnamedFormalArg[$: P] = FP(typ).map{ case (pos, t) => PUnnamedFormalArgDecl(t)(pos) }
 
-  def functionSignature[$: P] = P("function" ~ idndef ~ "(" ~ formalArgList ~ ")" ~ ":" ~ typ)
-
   def formalArgList[$: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ","))
 
   def axiomDecl[$: P]: P[PAxiom1] = FP(keyword("axiom") ~ idndef.? ~ "{" ~ exp ~ "}" ~~~ ";".lw.?).map { case (pos, (a, b)) => PAxiom1(a, b)(pos) }