Improve language flexibility

Author: JonasAlaif

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

@@ -16,6 +16,7 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
   lazy val isPure = Expressions.isPure(this)
+  lazy val noAccessPredicates = Expressions.noAccessPredicates(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
   def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
 
@@ -446,6 +447,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 */
@@ -533,6 +536,14 @@ case class Let(variable: LocalVarDecl, exp: Exp, body: Exp)(val pos: Position =
   val scopedDecls: Seq[Declaration] = Seq(variable)
 }
 
+/** An expression that creates a new object. */
+case class NewExp(fields: Seq[Field])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check : Seq[ConsistencyError] =
+    (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq())
+
+  override def typ: Type = Ref
+}
+
 // --- Quantifications
 
 /** A common trait for quantified expressions. */
@@ -1257,7 +1268,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

@@ -37,49 +37,16 @@ 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 {
+/** 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()) ++
-    (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{
-  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) ++
+    Consistency.checkCanAssignFrom(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 +59,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

@@ -644,10 +644,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
   /** Show a statement. */
   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))
+      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)
@@ -748,6 +745,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     case Let(v, exp, body) =>
       parens(text("let") <+> text(v.name) <+> "==" <> nest(defaultIndent, line <> parens(show(exp))) <+>
         "in" <> nest(defaultIndent, line <> show(body)))
+    case NewExp(fields) =>
+      text("new") <> parens(ssep(fields map (f => value(f.name)), char(',') <> space))
     case CondExp(cond, thn, els) =>
       group(parens(show(cond) <+> "?" <> nest(defaultIndent, line <> show(thn) <+> ":" <@> show(els))))
     case Exists(v, triggers, exp) =>

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, access predicates or `new` operations.
    */
   def checkPure(e: Exp): Seq[ConsistencyError] = {
     if(!e.isPure){
@@ -137,6 +137,17 @@ object Consistency {
     }
   }
 
+  /**
+   * Checks that this expression can be used to assign to a variable i.e. it contains no magic wands or access predicates.
+   */
+  def checkCanAssignFrom(e: Exp): Seq[ConsistencyError] = {
+    if(!e.noAccessPredicates){
+      Seq(ConsistencyError( s"$e is non pure and appears where only pure expressions are allowed.", e.pos))
+    }else{
+      Seq()
+    }
+  }
+
   /** Checks that no perm or forperm expression occurs in a node, except inside inhale/exhale statements */
   def checkNoPermForpermExceptInhaleExhale(e: Exp) : Seq[ConsistencyError] = {
     val permsAndForperms: Seq[Node] = e.deepCollect({case p: CurrentPerm => p; case fp: ForPerm => fp})
@@ -165,15 +176,12 @@ 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)){
-      s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
-    }
     s
   }
   /** Check all properties required for a precondition. */
@@ -387,13 +395,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: NewExp =>
+        Some(ConsistencyError("New expressions 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/Expressions.scala

@@ -14,35 +14,9 @@ import viper.silver.utility.Sanitizer
 
 /** Utility methods for expressions. */
 object Expressions {
-  def isPure(e: Exp): Boolean = e match {
-    case   _: AccessPredicate
-         | _: MagicWand
-         => false
-
-    case UnExp(e0) => isPure(e0)
-    case InhaleExhaleExp(in, ex) => isPure(in) && isPure(ex)
-    case BinExp(e0, e1) => isPure(e0) && isPure(e1)
-    case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
-    case unf: Unfolding => isPure(unf.body)
-    case app: Applying => isPure(app.body)
-    case QuantifiedExp(_, e0) => isPure(e0)
-    case Let(_, _, body) => isPure(body)
-    case e: ExtensionExp => e.extensionIsPure
-
-    case   _: Literal
-         | _: PermExp
-         | _: FuncApp
-         | _: DomainFuncApp
-         | _: BackendFuncApp
-         | _: LocationAccess
-         | _: AbstractLocalVar
-         | _: SeqExp
-         | _: SetExp
-         | _: MultisetExp
-         | _: MapExp
-         | _: ForPerm
-      => true
-  }
+  def isPure(e: Exp): Boolean = noAccessPredicates(e) && !e.contains[NewExp]
+  // This includes `acc(..)`, `Pred(..)` and `.. --* ...`
+  def noAccessPredicates(e: Exp): Boolean = !e.contains[AccessPredicate]
 
   def isTopLevelHeapDependent(e: Exp, p:Program) : Boolean = e match {
     case   _: AccessPredicate

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

@@ -48,9 +48,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)
@@ -85,6 +83,7 @@ object Nodes {
           case Applying(wand, body) => Seq(wand, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
+          case NewExp(fields) => fields
           case Let(v, exp, body) => Seq(v, exp, body)
           case Exists(v, triggers, exp) => v ++ triggers ++ Seq(exp)
           case Forall(v, triggers, exp) => v ++ triggers ++ Seq(exp)

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

@@ -79,9 +79,8 @@ 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 While(_, _, body) => writtenTo = writtenTo ++ (writtenVars(body) intersect s.undeclLocalVars)
     }
 

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

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