path: root/Chalice/src/Ast.scala

//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
import scala.util.parsing.input.Position
import scala.util.parsing.input.NoPosition
import scala.util.parsing.input.Positional

trait ASTNode extends Positional

// classes and types

case class TopLevelDecl(id: String) extends ASTNode

// this is in fact root of type hierarchy (confusingly, called "class")
sealed case class Class(classId: String, parameters: List[Class], module: String, members: List[Member]) extends TopLevelDecl(classId) {
  var mm = Map[String,Member]()
  def LookupMember(id: String): Option[Member] = {
    if (mm.keys exists { i => i.equals(id)})
      Some(mm(id))
    else if (IsRef && (RootClass.mm contains id)) {
      val m = RootClass.mm(id)
      if (m.Hidden) None else Some(m)
    } else
      None
  }
  def IsInt: Boolean = false
  def IsBool: Boolean = false
  def IsRef: Boolean = true
  def IsNull: Boolean = false
  def IsMu: Boolean = false
  def IsSeq: Boolean = false
  def IsToken: Boolean = false
  def IsChannel: Boolean = false
  def IsState: Boolean = false
  def IsNormalClass = true;
  var IsExternal = false;  // says whether or not to compile the class (compilation ignores external classes)

  def Fields: List[Field] = {
    members flatMap (m => m match { case f:Field => List(f) case _ => List() })
  }
  def Invariants: List[MonitorInvariant] = {
    (members :\ List[MonitorInvariant]()) { (m,list) => m match {
      case m:MonitorInvariant => m :: list
      case _ => list }}
  }
  def FullName: String = if(parameters.isEmpty) id else id + "<" + parameters.tail.foldLeft(parameters.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
}

sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId)

case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) {
  override def IsRef = false;
  override def IsSeq = true;
  override def IsNormalClass = false;
}
object IntClass extends Class("int", Nil, "default", Nil) {
  override def IsRef = false
  override def IsInt = true
  override def IsNormalClass = false;
}
object BoolClass extends Class("bool", Nil, "default", Nil) {
  override def IsRef = false
  override def IsBool = true
  override def IsNormalClass = false;
}
object NullClass extends Class("null", Nil, "default", Nil) {
  override def IsNull = true
  override def IsNormalClass = false;
}
object MuClass extends Class("$Mu", Nil, "default", Nil) {
  override def IsRef = false
  override def IsMu = true
  override def IsNormalClass = false;
}
case class TokenClass(c: Type, m: String) extends Class("token", Nil, "default", List( 
  new SpecialField("joinable", new Type(BoolClass))
))
{
  var method = null: Method;
  override def IsRef = true;
  override def IsToken = true;
  override def IsNormalClass = false;
  override def FullName: String = "token<" + c.FullName + "." + m + ">"
  mm = mm.+(("joinable", Fields(0)));
}
case class ChannelClass(ch: Channel) extends Class(ch.id, Nil, "default", Nil) {
  override def IsRef = true;
  override def IsChannel = true;
  override def IsNormalClass = false;
}

object RootClass extends Class("$root", Nil, "default", List(
  new SpecialField("mu", new Type(MuClass)),
  new SpecialField("held", new Type(BoolClass)){ override val Hidden = true },
  new SpecialField("rdheld", new Type(BoolClass)){ override val Hidden = true }
  ))  // joinable and held are bool in Chalice, but translated into an int in Boogie
{
  def MentionableFields = Fields filter {fld => fld.id != "held" && fld.id != "rdheld"}
}

sealed case class Type(id: String, params: List[Type]) extends ASTNode {  // denotes the use of a type
  var typ: Class = null
  def this(id: String) = { this(id, Nil); }
  def this(cl: Class) = { this(cl.id); typ = cl }
  def FullName: String = if(params.isEmpty) id else id + "<" + params.tail.foldLeft(params.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
}

sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) {  // denotes the use of a type
  typ = TokenClass(C, m);
  var method = null : Method;

  override def FullName: String = "token<" + C.FullName + "." + m + ">"
}

// members

sealed abstract class Member extends ASTNode {
  val Hidden: Boolean = false  // hidden means not mentionable in source
}
case class MonitorInvariant(e: Expression) extends Member
sealed abstract class NamedMember(id: String) extends Member {
  val Id = id
  var Parent: Class = null
  def FullName = Parent.id + "." + Id
}
case class Field(id: String, typ: Type, isGhost: Boolean) extends NamedMember(id)
case class SpecialField(name: String, tp: Type) extends Field(name, tp, false) {  // direct assignments are not allowed to a SpecialField
  override def FullName = id
}
case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], body: List[Statement]) extends NamedMember(id)
case class Predicate(id: String, definition: Expression) extends NamedMember(id)
case class Function(id: String, ins: List[Variable], out: Type, spec: List[Specification], definition: Option[Expression]) extends NamedMember(id) {
  def apply(rec: Expression, args: List[Expression]): FunctionApplication = {
    val result = FunctionApplication(rec, id, args);
    result.f = this;
    result
  }
  val isUnlimited = false;
  var isRecursive = false;
  var SCC: List[Function] = Nil;
}
case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)
class Variable(name: String, typ: Type) extends ASTNode {
  val id = name
  val t = typ
  val IsGhost: Boolean = false
  val IsImmutable: Boolean = false
  val UniqueName = {
    val n = Variable.VariableCount
    Variable.VariableCount = Variable.VariableCount + 1
    name + "#" + n
  }
}
object Variable { var VariableCount = 0 }
class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
  override val IsImmutable: Boolean = true
}
class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {
  override val UniqueName = name
}

sealed abstract class Specification extends ASTNode
case class Precondition(e: Expression) extends Specification
case class Postcondition(e: Expression) extends Specification
case class LockChange(ee: List[Expression]) extends Specification

// statements

sealed abstract class Statement extends ASTNode
case class Assert(e: Expression) extends Statement
case class Assume(e: Expression) extends Statement
case class BlockStmt(ss: List[Statement]) extends Statement
case class IfStmt(guard: Expression, thn: BlockStmt, els: Option[Statement]) extends Statement
case class WhileStmt(guard: Expression,
                     invs: List[Expression], lkch: List[Expression],
                     body: BlockStmt) extends Statement {
  var LoopTargets: Set[Variable] = null
  lazy val LoopTargetsList: List[Variable] = {  // to be called only after LoopTargets has been completely filled in
    var vv = List[Variable]()
    LoopTargets foreach (v => vv = v :: vv)
    vv
  }
}
case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement
case class FieldUpdate(lhs: MemberAccess, rhs: RValue) extends Statement
case class LocalVar(id: String, t: Type, const: Boolean, ghost: Boolean, rhs: Option[RValue]) extends Statement {
  val v =
    if (const)
      new ImmutableVariable(id, t){override val IsGhost = ghost}
    else
      new Variable(id, t){override val IsGhost = ghost}
}
case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
  var locals = List[Variable]()
  var m: Method = null
}
case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
case class Unshare(obj: Expression) extends Statement
case class Acquire(obj: Expression) extends Statement
case class Release(obj: Expression) extends Statement
case class RdAcquire(obj: Expression) extends Statement
case class RdRelease(obj: Expression) extends Statement
case class Downgrade(obj: Expression) extends Statement
case class Lock(obj: Expression, b: BlockStmt, rdLock: Boolean) extends Statement
case class Free(obj: Expression) extends Statement
case class CallAsync(declaresLocal: Boolean, lhs: VariableExpr, obj: Expression, id: String, args: List[Expression]) extends Statement {
  var local: Variable = null
  var m: Method = null
}
case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Statement {
  var m: Method = null
}
case class Wait(obj: Expression, id: String) extends Statement {
  var c: Condition = null
}
case class Signal(obj: Expression, id: String, all: Boolean) extends Statement {
  var c: Condition = null
}
case class Send(ch: Expression, args: List[Expression]) extends Statement {
}
case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {
  var locals = List[Variable]()
}
case class Fold(pred: Access) extends Statement
case class Unfold(pred: Access) extends Statement

// expressions

sealed abstract class RValue extends ASTNode {
  var typ: Class = null
}
case class NewRhs(id: String, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression]) extends RValue
case class Init(id: String, e: Expression) extends ASTNode {
  var f: Field = null;
}
sealed abstract class Expression extends RValue {
  def transform(f: Expression => Option[Expression]) = AST.transform(this, f)
  def visit(f: RValue => Unit) = AST.visit(this, f);
}
sealed abstract class Literal extends Expression
case class IntLiteral(n: Int) extends Literal
case class BoolLiteral(b: Boolean) extends Literal
case class NullLiteral() extends Literal
case class MaxLockLiteral() extends Literal
case class LockBottomLiteral() extends Literal
case class VariableExpr(id: String) extends Expression {
  var v: Variable = null
  def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }
  def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ }
}
case class Result() extends Expression
sealed abstract class ThisExpr extends Expression {
  override def equals(other: Any): Boolean = {
    // needed in autoMagic, which checks for syntactic equality using equals
    other.isInstanceOf[ThisExpr]
  }
}
case class ExplicitThisExpr() extends ThisExpr
case class ImplicitThisExpr() extends ThisExpr
case class MemberAccess(e: Expression, id: String) extends Expression {
  var isPredicate: Boolean = false;
  var f: Field = null
  var predicate: Predicate = null
}
case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression

sealed abstract class Permission extends Expression
sealed abstract class Write extends Permission
object Full extends Write                // None
case class Frac(n: Expression) extends Write // Some(n)
sealed abstract class Read extends Permission
object Epsilon extends Read                      // None
object Star extends Read               // Some(None)
case class Epsilons(n: Expression) extends Read   // Some(Some(n))

sealed abstract class PermissionExpr(perm: Permission) extends Expression
sealed abstract class WildCardPermission(perm: Permission) extends PermissionExpr(perm)
case class Access(ma: MemberAccess, perm: Permission) extends PermissionExpr(perm) 
case class AccessAll(obj: Expression, perm: Permission) extends WildCardPermission(perm)
case class AccessSeq(s: Expression, f: Option[MemberAccess], perm: Permission) extends WildCardPermission(perm)

case class Credit(e: Expression, n: Option[Expression]) extends Expression {
  val N = n match { case None => IntLiteral(1) case Some(n) => n }
}

case class Holds(e: Expression) extends Expression
case class RdHolds(e: Expression) extends Expression
case class Assigned(id: String) extends Expression {
  var v: Variable = null
}
case class Old(e: Expression) extends Expression
case class Not(e: Expression) extends Expression
case class FunctionApplication(obj: Expression, id: String, args: List[Expression]) extends Expression {
  var f: Function = null
}
case class Unfolding(pred: Access, in: Expression) extends Expression
sealed abstract class BinaryExpr(e0: Expression, e1: Expression) extends Expression {
  val E0 = e0
  val E1 = e1
  val ExpectedLhsType: Class = BoolClass  // sometimes undefined
  val ExpectedRhsType: Class = BoolClass  // sometimes undefined
  val ResultType: Class = BoolClass
  val OpName: String
}
case class Iff(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val OpName = "<==>"
}
case class Implies(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val OpName = "==>"
}
case class And(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val OpName = "&&"
}
case class Or(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val OpName = "||"
}
sealed abstract class ArithmeticExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val ExpectedLhsType = IntClass
  override val ExpectedRhsType = IntClass
  override val ResultType = IntClass
}
case class Plus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
  override val OpName = "+"
}
case class Minus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
  override val OpName = "-"
}
case class Times(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
  override val OpName = "*"
}
case class Div(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
  override val OpName = "/"
}
case class Mod(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
  override val OpName = "%"
}
sealed abstract class CompareExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
  override val ExpectedLhsType = IntClass
  override val ExpectedRhsType = IntClass
}
sealed abstract class EqualityCompareExpr(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val ExpectedLhsType = null;
  override val ExpectedRhsType = null;
}
case class Eq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
  override val OpName = "=="
}
case class Neq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
  override val OpName = "!="
}
case class Less(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val OpName = "<"
}
case class AtMost(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val OpName = "<="
}
case class AtLeast(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val OpName = ">="
}
case class Greater(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val OpName = ">"
}
case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
  override val ExpectedLhsType = null;
  override val ExpectedRhsType = null;
  override val OpName = "<<"
}

// quantifiers
trait Quant
object Forall extends Quant
object Exists extends Quant

sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) extends Expression {
  val Q = q;
  val Is = is;
  val E = e;
  var variables = null: List[Variable]; // resolved by type checker
}
case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)
case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)

// sequences

case class EmptySeq(t: Type) extends Literal
case class ExplicitSeq(elems: List[Expression]) extends Expression
case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Expression
case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {
  override val OpName = "++"
}
sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1) {
  override val ExpectedLhsType = null
  override val ExpectedRhsType = null
  override val ResultType = null
}
case class Length(e: Expression) extends Expression
case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {
  override val OpName = ""
}
case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
  override val OpName = ""
}
case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {
  override val OpName = ""
}
case class Contains(n: Expression, s: Expression) extends SeqAccess(n, s) {
  override val OpName = "in"
}

// eval

case class Eval(h: EvalState, e: Expression) extends Expression
sealed abstract class EvalState {
  def target(): Expression;
}
case class AcquireState(obj: Expression) extends EvalState {
  def target() = obj
}
case class ReleaseState(obj: Expression) extends EvalState {
  def target() = obj
}
case class CallState(token: Expression, obj: Expression, id: String, args: List[Expression]) extends EvalState {
  var m = null: Method;
  def target() = token;
}

// visitors / operations

object AST {
  /**
   * Transforms an expression using f. f must produce expressions of the appropriate type (e.g. not replace int literal with a bool literal)
   * Ensures that mutable fields of expressions are carried over. f must make sure that mutable fields of its value are filled in.
   */
  def transform(expr: Expression, f: Expression => Option[Expression]):Expression = {
    val func = (e:Expression) => transform(e, f);
    val x = f(expr);
    // apply recursively
    val result = if (x isDefined) x.get else expr match {
      case _:Literal => expr
      case _:ThisExpr => expr
      case _:Result => expr
      case _:VariableExpr => expr
      case ma@MemberAccess(e, id) =>
        val g = MemberAccess(func(e), id);
        g.f = ma.f;
        g.predicate = ma.predicate;
        g.isPredicate = ma.isPredicate;
        g
      case Full | Epsilon | Star => expr
      case Frac(perm) => Frac(func(perm))
      case Epsilons(perm) => Epsilons(func(perm))
      case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], func(perm).asInstanceOf[Permission]);
      case AccessAll(obj, perm) => AccessAll(func(obj), func(perm).asInstanceOf[Permission]);
      case AccessSeq(s, None, perm) => AccessSeq(func(s), None, func(perm).asInstanceOf[Permission])
      case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), func(perm).asInstanceOf[Permission])
      case Credit(e, None) => Credit(func(e), None)
      case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
      case Holds(e) => Holds(func(e))
      case RdHolds(e) => RdHolds(func(e))
      case _: Assigned => expr
      case Old(e) => Old(func(e))
      case IfThenElse(con, then, els) => IfThenElse(func(con), func(then), func(els))
      case Not(e) => Not(func(e))
      case funapp@FunctionApplication(obj, id, args) =>
        val appl = FunctionApplication(func(obj), id, args map { arg => func(arg)});
        appl.f = funapp.f;
        appl
      case Unfolding(pred, e) =>
        Unfolding(func(pred).asInstanceOf[Access], func(e))
      case Iff(e0,e1) => Iff(func(e0), func(e1))
      case Implies(e0,e1) => Implies(func(e0), func(e1))
      case And(e0,e1) => And(func(e0), func(e1))
      case Or(e0,e1) => Or(func(e0), func(e1))
      case Eq(e0,e1) => Eq(func(e0), func(e1))
      case Neq(e0,e1) => Neq(func(e0), func(e1))
      case Less(e0,e1) => Less(func(e0), func(e1))
      case AtMost(e0,e1) => AtMost(func(e0), func(e1))
      case AtLeast(e0,e1) => AtLeast(func(e0), func(e1))
      case Greater(e0,e1) => Greater(func(e0), func(e1))
      case LockBelow(e0,e1) => LockBelow(func(e0), func(e1))
      case Plus(e0,e1) => Plus(func(e0), func(e1))
      case Minus(e0,e1) => Minus(func(e0), func(e1))
      case Times(e0,e1) => Times(func(e0), func(e1))
      case Div(e0,e1) => Div(func(e0), func(e1))
      case Mod(e0,e1) => Mod(func(e0), func(e1))
      case ExplicitSeq(es) => ExplicitSeq(es map { e => func(e) })
      case Range(min, max)=> Range(func(min), func(max))
      case Append(e0, e1) => Append(func(e0), func(e1))
      case At(e0, e1) => At(func(e0), func(e1))
      case Drop(e0, e1) => Drop(func(e0), func(e1))
      case Take(e0, e1) => Take(func(e0), func(e1))
      case Length(e) => Length(func(e))
      case Contains(e0, e1) => Contains(func(e0), func(e1))
      case qe @ SeqQuantification(q, is, seq, e) =>
        val result = SeqQuantification(q, is, func(seq), func(e));
        result.variables = qe.variables;
        result;
      case qe @ TypeQuantification(q, is, t, e) =>
        val result = TypeQuantification(q, is, t, func(e));
        result.variables = qe.variables;
        result;
      case Eval(h, e) =>
        Eval(h match {
          case AcquireState(obj) => AcquireState(func(obj))
          case ReleaseState(obj) => ReleaseState(func(obj))
          case cs @ CallState(token, obj, i, args) =>
            val result = CallState(func(token), func(obj), i, args map { a => func(a)});
            result.m = cs.m;
            result;
        }, func(e))
    };
    
    // preserve type
    if (result.typ == null) result.typ = expr.typ;
    // preserve position
    if (result.pos == NoPosition) result.pos = expr.pos
    result
  }

  // Applies recursively the function f first to the expression and then to its subexpressions (that is members of type RValue)  
  def visit(expr: RValue, f: RValue => Unit) {
    f(expr);
    expr match {
     case _:Literal => ;
     case _:ThisExpr => ;
     case _:Result => ;
     case _:VariableExpr => ;
     case MemberAccess(e, _) =>
       visit(e, f);

     case Frac(p) => visit(p, f);
     case Epsilons(p) => visit(p, f);
     case Full | Epsilon | Star =>;
     case Access(e, perm) =>
       visit(e, f); visit(perm, f);
     case AccessAll(obj, perm) =>
       visit(obj, f); visit(perm, f);
     case AccessSeq(s, _, perm) =>
       visit(s, f); visit(perm, f);

     case Credit(e, n) =>
       visit(e, f); n match { case Some(n) => visit(n, f); case _ => }
     case Holds(e) => visit(e, f);
     case RdHolds(e) => visit(e, f);

     case e: BinaryExpr =>
       visit(e.E0, f); visit(e.E1, f);
     case Range(min, max) =>
       visit(min, f); visit(max, f);
     case e: Assigned => e
     case Old(e) => visit(e, f);
     case IfThenElse(con, then, els) => visit(con, f); visit(then, f); visit(els, f);
     case Not(e) => visit(e, f);
     case funapp@FunctionApplication(obj, id, args) =>
       visit(obj, f); args foreach { arg => visit(arg, f) };
     case Unfolding(pred, e) =>
       visit(pred, f); visit(e, f);

     case SeqQuantification(_, _, seq, e) => visit(seq, f); visit(e, f);
     case TypeQuantification(_, _, _, e) => visit(e, f);

     case ExplicitSeq(es) =>
       es foreach { e => visit(e, f) }
     case Length(e) =>
       visit(e, f)
     case Eval(h, e) =>
       h match {
         case AcquireState(obj) => visit(obj, f);
         case ReleaseState(obj) => visit(obj, f);
         case CallState(token, obj, id, args) =>
           visit(token, f); visit(obj, f); args foreach {a : Expression => visit(a, f)};
       }
       visit(e, f);
     case NewRhs(_, init, lowerBounds, upperBounds) =>
       lowerBounds foreach { e => visit(e, f)};
       upperBounds foreach { e => visit(e, f)};
   }
 }
}