path: root/Chalice/src/main/scala/Resolver.scala

//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
package chalice;
import scala.util.parsing.input.Position
import scala.util.parsing.input.Positional
import collection.mutable.ListBuffer

object Resolver {
 sealed abstract class ResolverOutcome
 case class Success() extends ResolverOutcome
 case class Errors(ss: List[(Position,String)]) extends ResolverOutcome

 val runMethod = "run";

 sealed class ProgramContext(val decls: Map[String,TopLevelDecl], val currentClass: Class,
                      val currentMember: Member, val errors: ListBuffer[(Position,String)]) {
   final def AddVariable(v: Variable): ProgramContext = new LProgramContext(v, this);
   final def Error(pos: Position, msg: String) {errors += ((pos, msg))}
   final def SetClass(cl: Class): ProgramContext = new MProgramContext(cl, null, false, this)
   final def SetMember(m: Member): ProgramContext = {
     val static = m match {
       case f: Function => f.isStatic
       case _			=> false			
     }
     var ctx:ProgramContext = new MProgramContext(currentClass, m, static, this)
     m match {
       case m: Method =>
         assert(currentClass == m.Parent)
         for (v <- m.Ins ++ m.Outs) ctx = ctx.AddVariable(v)
       case f: Function =>
         assert(currentClass == f.Parent)
         for (v <- f.ins) ctx = ctx.AddVariable(v)
       case mt: MethodTransform =>
         assert(currentClass == mt.Parent)
         for (v <- mt.Ins ++ mt.Outs) ctx = ctx.AddVariable(v)
       case _ =>
     }
     ctx
   }
   final def AsNonStatic(): ProgramContext = new NSProgramContext(this) 

   def LookupVariable(id: String): Option[Variable] = None
   def IsVariablePresent(vr: Variable): Boolean = false
   def IsStatic: Boolean = false
   
   private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.decls, parent.currentClass, parent.currentMember, errors) {
     assert (v!=null)
     override def LookupVariable(id: String): Option[Variable] =
       if (id == v.id) Some(v) else parent.LookupVariable(id)
     override def IsVariablePresent(vr: Variable): Boolean =
       if (vr == v) true else parent.IsVariablePresent(vr)
     override def IsStatic = parent.IsStatic
   }
   private class MProgramContext(cl: Class, m: Member, static: Boolean, parent: ProgramContext) extends ProgramContext(parent.decls, cl, m, errors) {
     override def LookupVariable(id: String) = parent.LookupVariable(id)
     override def IsVariablePresent(vr: Variable) = parent.IsVariablePresent(vr)
     override def IsStatic: Boolean =
       if (static) true else parent.IsStatic
   }
   private class NSProgramContext(parent: ProgramContext) extends ProgramContext(parent.decls, parent.currentClass, parent.currentMember, errors) {
     override def LookupVariable(id: String) = parent.LookupVariable(id)
     override def IsVariablePresent(vr: Variable) = parent.IsVariablePresent(vr)
     override def IsStatic = false 
   }
 }

 def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = {
 
   // check for deprecates and/or unsupported constructs
   var refinements = false
   prog map (_ match {
     case c: Class => if (c.IsRefinement) refinements = true
     case _ => }
   )
   if (refinements) throw new NotSupportedException("stepwise refinements are currently not supported")
 
   // register the channels as well as the classes and their members
   var decls = Map[String,TopLevelDecl]()
   for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: StringClass :: MuClass :: prog) {
     if (decls contains decl.id) {
       return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id)))
     } else {
       decl match {
         case cl: Class =>
           val ids = scala.collection.mutable.Set.empty[String]
           for (m <- cl.members) m match {
             case _:MonitorInvariant =>
             case _:CouplingInvariant =>
             case m: NamedMember =>
               m.Parent = cl
               if (ids contains m.Id) {
                 return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id)))
               } else {
                 ids += m.Id
               }
           }
         case ch: Channel =>
       }
       decls = decls + (decl.id -> decl)
     }
   }

   // resolve refinements
   val refinesRel = new DiGraph[Class];
   for (decl <- prog) decl match {
     case cl: Class if cl.IsRefinement =>
       if (! (decls contains cl.refinesId)) {
         return Errors(List((cl.pos, "refined class " + cl.refinesId + " does not exist")))
       } else if (cl.refinesId == cl.id) {
         return Errors(List((cl.pos, "class cannot refine itself")))
       } else decls(cl.refinesId) match {
         case abs: Class =>
           cl.refines = abs;
           refinesRel.addNode(cl);
           refinesRel.addNode(cl.refines);
           refinesRel.addEdge(cl, cl.refines);
         case _ =>
           return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class")))
       }
     case _ =>
   }
   val (dag, refinesSCC) = refinesRel.computeSCC;
   refinesSCC.values foreach {l =>
     if (l.size > 1) {
       val msg = new StringBuilder("a refinement cycle detected ")
       return Errors(List((l(0).pos, l.map(cl => cl.id).addString(msg, "->").toString)))
     }
   }

   // resolve refinement members: set-up refinement between members and check for duplicates
   for (decl <- prog) decl match {
     case cl: Class =>
       if (! cl.IsRefinement) {
         // check has no refinement members
         if (cl.members.exists{
           case _: CouplingInvariant => true
           case _: MethodTransform => true
           case _ => false})
           return Errors(List((cl.pos, "non-refinement class cannot have refinement members")))
       } else for (member <- cl.members) member match {
         case r: MethodTransform =>
           r.refines = cl.refines.LookupMember(r.Id) match {
             case Some(m: Method) => m;
             case Some(mt: MethodTransform) => mt
             case None => return Errors(List((r.pos, "abstract class has no method with name " + r.Id))) 
             case _ => return Errors(List((r.pos, "method transform can only refine a method or a method transform")))
           }
         case m: NamedMember =>
           cl.refines.LookupMember(m.Id) match {
             case Some(x) => return Errors(List((m.pos, "member needs to be a refinement since abstract class has a member with the same name: " + x.pos)))
             case None =>
           }
         case _ =>
       }
     case _ =>
   }

   // collect errors
   val baseContext = new ProgramContext(decls, null, null, new ListBuffer[(Position,String)])

   // resolve types of members
   for (decl <- prog) decl match {
     case ch: Channel =>
       for (v <- ch.parameters) {
         ResolveType(v.t, baseContext)
        }
     case cl: Class =>
       for (m <- cl.members) m match {
         case _: MonitorInvariant =>
         case _: CouplingInvariant =>
         case Field(_, t, _) =>
           ResolveType(t, baseContext)
         case Method(id, ins, outs, _, _) =>
           val ids = scala.collection.mutable.Set.empty[String]
           for (v <- ins ++ outs) {
             ResolveType(v.t, baseContext)
             if (ids contains v.Id) {
               return Errors(List((m.pos, "duplicate parameter " + v.Id + " of method " + id + " in class " + cl.id)))
             } else {
               ids += v.Id
             }
           }
         case _: Condition =>
         case _: Predicate =>
         case Function(id, ins, out, specs, _) => 
           val ids = scala.collection.mutable.Set.empty[String]
           for (v <- ins) {
             ResolveType(v.t, baseContext)
             if (ids contains v.Id) {
               return Errors(List((m.pos, "duplicate parameter " + v.Id + " of function " + id + " in class " + cl.id)))
             } else {
               ids += v.Id
             }
           }
           ResolveType(out, baseContext)
         case mt: MethodTransform =>
           val ids = scala.collection.mutable.Set.empty[String]
           for (v <- mt.ins ++ mt.outs) {
             ResolveType(v.t, baseContext)
             if (ids contains v.Id) {
               return Errors(List((m.pos, "duplicate parameter " + v.Id + " of method transform " + mt.Id + " in class " + cl.id)))
             } else {
               ids += v.Id
             }
           }
       }
   }   

   // now, resolve and typecheck all
   //  * Field types and Method formal-parameter types
   //  * Assign, FieldUpdate, and Call statements
   //  * VariableExpr and FieldSelect expressions
   //  * Call graph for functions
   val calls = new DiGraph[Function];
   for (decl <- prog) decl match {
     case ch: Channel =>
       val context = baseContext.SetClass(ChannelClass(ch))
       var ctx = context
       for (v <- ch.parameters) {
         ctx = ctx.AddVariable(v)
       }
       ResolveExpr(ch.where, ctx, false, true)(false)
     case cl: Class =>
       for (m <- cl.members) {
         val context = baseContext.SetClass(cl).SetMember(m);
         m match {
           case MonitorInvariant(e) =>
             ResolveExpr(e, context, true, true)(true)
             if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")")
           case _:Field => // nothing more to do
           case m@Method(id, ins, outs, spec, body) =>
             spec foreach {
               case Precondition(e) => ResolveExpr(e, context, false, true)(false)
               case Postcondition(e) => ResolveExpr(e, context, true, true)(false)
               case lc@LockChange(ee) => 
               if (m.id == runMethod) context.Error(lc.pos, "lockchange not allowed on method run")
               ee foreach (e => ResolveExpr(e, context, true, false)(false))
             }
             ResolveStmt(BlockStmt(body), context)
           case Condition(id, None) =>
           case c@Condition(id, Some(e)) =>
             ResolveExpr(e, context, false, true)(false)
             if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")")
           case p@Predicate(id, e) =>
             var ctx = context;
             if (ContainsWaitlevel(e)) context.Error(e.pos, "predicate body is not allowed to mention 'waitlevel'")
             ResolveExpr(e, ctx, false, true)(true);
             if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")
           case f@Function(id, ins, out, spec, definition) =>
             def hasCredit(e: Expression) = {
               var b = false
               e transform {
                 case _:Credit => b = true; None
                 case _ => None
               }
               b
             }
             def hasAccessibilityPredicate(e: Expression) = {
               var b = false
               e visitOpt {
                 case _: PermissionExpr => b = true; false
                 case ma: MemberAccess => if (ma.isPredicate) { b = true; false } else { true }
                 case Unfolding(pred, e) => false
                 case _ => true
               }
               b
             }
             def hasUnfoldingExpression(e: Expression) = {
               var b = false
               e visit {
                 case Unfolding(pred, e) => b = true
                 case _ =>
               }
               b
             }
             spec foreach {
               case p@Precondition(e) =>
                 ResolveExpr(e, context, false, true)(false)
                 if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 
               case p@Postcondition(e) =>
                 ResolveExpr(e, context, false, true)(false)
                 if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 
                 if (hasAccessibilityPredicate(e)) context.Error(p.pos, "the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)") 
                 // The following check is necessary, because the postcondition axiom has the limited function as a trigger.  If we were to allow unfolding expressions, then this might introduce a matching loop.  Since we don't know of any cases where one would use an unfolding expression in the postcondition, we forbid it here.
                 if (hasUnfoldingExpression(e)) context.Error(p.pos, "the postcondition of functions cannot contain unfolding expressions at the moment") 
               case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function") 
             }

             definition match {
               case Some(e) =>
                 ResolveExpr(e, context, false, false)(false)
                 if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")")
                 // resolve function calls
                 calls addNode f;
                 e visit {
                   case app : FunctionApplication if app.f != null /* may not be resolved */ =>
                     calls addNode app.f;
                     calls.addEdge(f, app.f);
                     if (app.f == f) f.isRecursive = true; // self-recursion
                   case _ =>
                 }
               case None =>
             }
           case mt: MethodTransform => // need to resolve them in reverse refinement order
           case ci: CouplingInvariant => ResolveCouplingInvariant(ci, cl, baseContext)
         }
       }
   }

   // fill in SCC and height for recursive functions 
   val (callGraphCondensation, h) = calls.computeSCC;
   val callGraphTopoSort = callGraphCondensation.computeTopologicalSort.reverse
   h.keys foreach {f:Function =>
     f.SCC = h(f);
     f.height = callGraphTopoSort.indexOf(h(f))
     assert(f.height >= 0)
     assert(f.SCC contains f);
     if (h(f).size > 1)
       f.isRecursive = true;
   }

   // resolve refinement members (starting from abstract programs): assign types to expressions
   for (List(cl) <- dag.computeTopologicalSort.reverse) {
     for (m <- cl.members) m match {
       case mt: MethodTransform => ResolveTransform(mt, baseContext)
       case _ =>
     }
   }

   val errors = baseContext.errors.toList
   if (errors.length == 0) {
     Success()
   } else {
     Errors(errors)
   }
 }

 def ResolveType(t: Type, context: ProgramContext): Unit = {
     for(p <- t.params){
       ResolveType(p, context);
     }
     if(t.isInstanceOf[TokenType]){
       val tt = t.asInstanceOf[TokenType];
       ResolveType(tt.C, context);
       if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class.");
       tt.C.typ.LookupMember(tt.m) match {
         case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc;
         case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + ".");
       }
       return;
     }
     if (context.decls contains t.FullName) {
       context.decls(t.FullName) match {
         case cl: Class => t.typ = cl
         case ch: Channel => t.typ = ChannelClass(ch)
         case _ =>
           context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class")
           t.typ = IntClass
       }
     } else {
       if(t.id.equals("seq") && t.params.length == 1) {
         t.typ = new SeqClass(t.params(0).typ);
       } else {
         context.Error(t.pos, "undeclared type " + t.FullName)
         t.typ = IntClass
       }
     }
 }

 def ResolveStmt(s: Statement, context: ProgramContext):Unit = s match {
   case Assert(e) =>
     ResolveExpr(e, context, true, true)(false)
     if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")
   case Assume(e) =>
     ResolveExpr(e, context, true, true)(false)  
     if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")
   case RefinementBlock(ss, _) => throw new InternalErrorException("unexpected statement")
   case BlockStmt(ss) =>
     var ctx = context
     for (s <- ss) s match {
       case l @ LocalVar(v, rhs) =>
         if (ctx.LookupVariable(v.id).isDefined) {
           context.Error(l.pos, "local variable name "+v.id+" collides with parameter or other local variable")
         }
         ResolveType(v.t, ctx)
         val oldCtx = ctx
         ctx = ctx.AddVariable(v)
         rhs match {
           case None =>
           case Some(rhs) =>
             val lhs = VariableExpr(v.id)
             lhs.pos = l.pos;
             ResolveExpr(lhs, ctx, false, false)(false)
             ResolveAssign(lhs, rhs, oldCtx)
         }
       case c: CallAsync =>
         ResolveStmt(c, ctx)
         if (c.local != null) {
           ctx = ctx.AddVariable(c.local)
         }
       case c: Call =>
         ResolveStmt(c, ctx)
         for (v <- c.locals) { ctx = ctx.AddVariable(v) } 
       case r: Receive =>
         ResolveStmt(r, ctx)
         for (v <- r.locals) { ctx = ctx.AddVariable(v) }
       case s: SpecStmt =>
         for (v <- s.locals) { ResolveType(v.t, ctx); ctx = ctx.AddVariable(v) }
         for (v <- s.lhs) {
           ResolveExpr(v, ctx, true, true)(false)
           if (v.v != null && !s.locals.contains(v.v) && v.v.isImmutable)
             context.Error(s.pos, "Immutable variable cannot be updated by a spec statement: " + v.id);           
         }
         ResolveExpr(s.pre, ctx, false, true)(false)
         ResolveExpr(s.post, ctx, true, true)(false)
       case s =>
         ResolveStmt(s, ctx)
     }
   case IfStmt(guard, thn, els) =>
     ResolveExpr(guard, context, false, false)(false)
     if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")")
     CheckNoGhost(guard, context)
     ResolveStmt(thn, context)
     els match { case None => case Some(s) => ResolveStmt(s, context) }
   case w@ WhileStmt(guard, invs, ref, lkch, body) =>
     if (ref.size > 0) throw new InternalErrorException("unexpected statement")
     ResolveExpr(guard, context, false, false)(false)
     if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")
     CheckNoGhost(guard, context)
     for (inv <- invs) {
       ResolveExpr(inv, context, true, true)(false)
       if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")
     }
     for (l <- lkch) {
       ResolveExpr(l, context, true, false)(false)
       if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")")
     }
     ResolveStmt(body, context)
     w.LoopTargets = body.Targets.filter(context.IsVariablePresent).toList
   case Assign(lhs, rhs) =>
     ResolveExpr(lhs, context, false, false)(false)
     ResolveAssign(lhs, rhs, context)
     if (lhs.v != null && lhs.v.isImmutable) {
       if (lhs.v.isGhost)
         CheckNoGhost(rhs, context)
       else
         context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id)
     }
   case fu@FieldUpdate(lhs, rhs) =>
     ResolveExpr(lhs, context, false, false)(false)
     if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(lhs.e, context)
     if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)
     ResolveExpr(rhs, context, false, false)(false)
     if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
     if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(rhs, context)
   case _:LocalVar => throw new InternalErrorException("unexpected LocalVar; should have been handled in BlockStmt above")
   case _:SpecStmt => throw new InternalErrorException("should have been handled before")
   case c @ Call(declaresLocal, lhs, obj, id, args) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
     // lookup method
     var typ: Class = IntClass
     c.m = obj.typ.LookupMember(id) match {
       case None =>
         context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
         null
       case Some(m: Method) => m
       case Some(mt: MethodTransform) => mt
       case _ =>
         context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
         null
     }
     if (c.m != null) {
       if (args.size != c.m.Ins.size)
         context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
                       " (" + args.size + " instead of " + c.m.Ins.size + ")")
       else {
         for((actual, formal) <- args zip c.m.Ins){
           if(! canAssign(formal.t.typ, actual.typ))
             context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
         }
       }
       if (lhs.size != c.m.Outs.size)
         context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +
                       " (" + lhs.size + " instead of " + c.m.Outs.size + ")")
       else
         c.locals = ResolveLHS(declaresLocal, lhs, c.m.Outs, context)
     }
   case Install(obj, lowerBounds, upperBounds) =>
     ResolveExpr(obj, context, false, false)(false)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in reorder statement must be of a reference type (found " + obj.typ.FullName + ")")
     if (obj.typ.IsChannel) context.Error(obj.pos, "object in reorder statement must not be a channel (found " + obj.typ.FullName + ")")
     ResolveBounds(lowerBounds, upperBounds, context, "install")
   case Share(obj, lowerBounds, upperBounds) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")")
     if (obj.typ.IsChannel) context.Error(obj.pos, "object in share statement must not be a channel (found " + obj.typ.FullName + ")")
     ResolveBounds(lowerBounds, upperBounds, context, "share")
   case Unshare(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")")
     if (obj.typ.IsChannel) context.Error(obj.pos, "object in unshare statement must not be a channel (found " + obj.typ.FullName + ")")
   case Acquire(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
   case Release(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")")
   case RdAcquire(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")")
   case RdRelease(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")")
   case Lock(obj, b, rdLock) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) {
       val sname = if (rdLock) "rd lock" else "lock";
       context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")")
                                      
     }
     ResolveStmt(b, context)
   case Downgrade(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")")
   case Free(obj) =>
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")")
   case fld@Fold(e) =>
     ResolveExpr(e, context, false, true)(false);
     CheckNoGhost(e, context);
     if(!e.ma.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")
   case ufld@Unfold(e) =>
     ResolveExpr(e, context, false, true)(false);
     CheckNoGhost(e, context);
     if(!e.ma.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
   case c@CallAsync(declaresLocal, token, obj, id, args) =>
     // resolve receiver
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     // resolve arguments
     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
     // lookup method
     var typ: Class = IntClass
     obj.typ.LookupMember(id) match {
       case None =>
         context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
       case Some(m: Method) =>
         c.m = m
         if (args.length != m.ins.length)
           context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
                         " (" + args.length + " instead of " + m.ins.length + ")")
         else {
           for((actual, formal) <- args zip m.ins){
             if(! canAssign(formal.t.typ, actual.typ))
               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
           }
         }
       case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
     }
     // resolve the token
     if (declaresLocal) {
       c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))
       ResolveType(c.local.t, context)
       token.Resolve(c.local)
     } else if (token != null) {
       ResolveExpr(token, context, false, false)(false)
       if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))
         context.Error(token.pos, "wrong token type")
     }
   case jn@JoinAsync(lhs, token) =>
     // resolve the assignees
     var vars = Set[Variable]()
     for (v <- lhs) {
       ResolveExpr(v, context, false, false)(false)
       if (v.v != null) {
         if (v.v.isImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
         if (vars contains v.v) {
           context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
         } else {
           vars = vars + v.v
         }
       }
     }
     // resolve the token
     ResolveExpr(token, context, false, false)(false);
     if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null)
       context.Error(token.pos, "the first argument of a join async must be a token")
     else {
       val m = token.typ.asInstanceOf[TokenClass].method;
       jn.m = m
       if (lhs.length != m.outs.length)
         context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName +
                        " (" + lhs.length + " instead of " + m.outs.length + ")")
       else {
         for((out, l) <- m.outs zip lhs){
           if(! canAssign(l.typ, out.t.typ))
             context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")
         }
       }
     
     }
   case w@Wait(obj, id) =>
     // resolve receiver
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     // lookup condition
     obj.typ.LookupMember(id) match {
       case None =>
         context.Error(w.pos, "wait on undeclared member " + id + " in class " + obj.typ.FullName)
       case Some(c: Condition) => w.c = c
       case _ =>
         context.Error(w.pos, "wait expression does not denote a condition: " + obj.typ.FullName + "." + id)
     }
   case s@Signal(obj, id, all) =>
     // resolve receiver
     ResolveExpr(obj, context, false, false)(false)
     CheckNoGhost(obj, context)
     // lookup condition
     obj.typ.LookupMember(id) match {
       case None =>
         context.Error(s.pos, "signal on undeclared member " + id + " in class " + obj.typ.FullName)
       case Some(c: Condition) => s.c = c
       case _ =>
         context.Error(s.pos, "signal expression does not denote a condition: " + obj.typ.FullName + "." + id)
     }
   case s@Send(ch, args) =>
     ResolveExpr(ch, context, false, false)(false)
     CheckNoGhost(ch, context)
     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
     // match types of arguments
     ch.typ match {
       case ChannelClass(channel) =>
         if (args.length != channel.parameters.length)
           context.Error(s.pos, "wrong number of actual in-parameters in send for channel type " + ch.typ.FullName +
                         " (" + args.length + " instead of " + channel.parameters.length + ")")
         else {
           for ((actual, formal) <- args zip channel.parameters) {
             if (! canAssign(formal.t.typ, actual.typ))
               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
           }
         }
       case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel")
     }
   case r@Receive(declaresLocal, ch, outs) =>
     ResolveExpr(ch, context, false, false)(false)
     CheckNoGhost(ch, context)
     // match types of arguments
     ch.typ match {
       case ChannelClass(channel) =>
         if (outs.length != channel.parameters.length)
           context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName +
                         " (" + outs.length + " instead of " + channel.parameters.length + ")")
         else
           r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context)
       case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")
     }
 }

 def ResolveLHS(declaresLocal: List[Boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {
   var locals = List[Variable]()
   var vars = Set[Variable]()
   var ctx = context
   for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {
     if (declareLocal) {
       val local = new Variable(actual.id, new Type(formal.t.typ))
       locals = locals ::: List(local)
       ResolveType(local.t, ctx)
       actual.Resolve(local)
       vars = vars + actual.v
       ctx = ctx.AddVariable(local)
     } else {
       ResolveExpr(actual, ctx, false, false)(false)
       CheckNoGhost(actual, ctx)
       if (actual.v != null) {
         if (! canAssign(actual.typ, formal.t.typ))
           ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " +
                         formal.t.FullName + ", found: " + actual.typ.FullName + ")")
         if (vars contains actual.v)
           ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id)
         else if (actual.v.isImmutable)
           ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter")
         vars = vars + actual.v
       }
     }
   }
   locals
 }

 def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) =
   for (b <- lowerBounds ++ upperBounds) {
     ResolveExpr(b, context, true, false)(false)
     if (!b.typ.IsRef && !b.typ.IsMu)
       context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")")
   }

 def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = {
   rhs match {
     case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs
     case _ => ResolveExpr(rhs, context, false, false)(false)
   }
   if (! canAssign(lhs.typ, rhs.typ))
     context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
   if (lhs.v != null && !lhs.v.isGhost) CheckNoGhost(rhs, context)
 }
 
 // ResolvePermissionExpr resolves all parts of a permission expression, and replaces arithmetic operations
 // by the appropriate operation on permissions
 // Note that the parsing of permissions can be highly inaccurate. Besides historic reasons, we also need type information
 // to decide how rd(x) inside acc(o.f, ***) should be interpreted. If x is an integer expression, it stands for Epsilons(x),
 // but x could also be a channel, monitor or predicate.
 // For instance, acc(x,rd(n)) is parsed to
 //    Access(MemberAccess(ImplicitThisExpr(),x),Frac(Access(MemberAccess(ImplicitThisExpr(),n),Epsilon)))
 // These error during parsing are corrected here during the resolve process. In particular, the following corrections are done:
 // - Plus and Minus are replaced by the corresponding operation on permission (i.e. PermPlus and PermMinus)
 // - Integer expressions x are replaced by Frac(x)
 def ResolvePermissionExpr(e: Expression, context: ProgramContext, twoStateContext: Boolean,
                 specContext: Boolean, pos: Position)(implicit inPredicate: Boolean): Permission = e match {
   case ve @ VariableExpr(id) =>
     ResolvePermissionExpr(Frac(ve), context, twoStateContext, specContext, pos)(inPredicate);
   case f @ Frac(perm) =>
     ResolveExpr(perm, context, twoStateContext, false);
     if(perm.typ != IntClass)
       context.Error(pos, "fraction in permission must be of type integer")
     f
   case sel @ MemberAccess(e, id) =>
     ResolvePermissionExpr(Frac(sel), context, twoStateContext, specContext, pos)(inPredicate);
   case ep @ Epsilons(exp) => 
     ResolveExpr(exp, context, twoStateContext, false)
     var p: Permission = Epsilon
     exp.typ match {
       case BoolClass if exp.isInstanceOf[MemberAccess] && exp.asInstanceOf[MemberAccess].isPredicate =>
         p = PredicateEpsilon(Some(exp.asInstanceOf[MemberAccess]))
         p.pos = ep.pos
       case IntClass =>
         p = Epsilons(exp)
         p.pos = ep.pos
       case TokenClass(c, m) =>
         p = ForkEpsilon(exp)
         p.pos = ep.pos
       case c:Channel =>
         p = ChannelEpsilon(Some(exp))
         p.pos = ep.pos
       case c:Class if (c.IsNormalClass) =>
         p = MonitorEpsilon(Some(exp))
         p.pos = ep.pos
       case _ =>
         p = Star
         context.Error(ep.pos, "type " + exp.typ.FullName + " is not supported inside a rd expression.");
     }
     exp.pos = ep.pos
     p
   case f @ Full => f
   case f:PredicateEpsilon => f
   case f:ForkEpsilon => f
   case f:ChannelEpsilon => f
   case f:MonitorEpsilon => f
   case Epsilon => Epsilon
   case MethodEpsilon => MethodEpsilon
   case f @ Star => f
   case p @ Plus(ee0, ee1) =>
     if (ContainsStar(ee0) || ContainsStar(ee1))
       context.Error(p.pos, "rd* is not allowed inside permission expressions.")
     val e0 = ResolvePermissionExpr(ee0, context, twoStateContext, specContext, pos)(inPredicate);
     val e1 = ResolvePermissionExpr(ee1, context, twoStateContext, specContext, pos)(inPredicate);
     val pp = PermPlus(e0, e1)
     pp.pos = p.pos;
     pp
   case p @ Minus(ee0, ee1) =>
     if (ContainsStar(ee0) || ContainsStar(ee1))
       context.Error(p.pos, "rd* is not allowed inside permission expressions.")
     val e0 = ResolvePermissionExpr(ee0, context, twoStateContext, specContext, pos)(inPredicate);
     val e1 = ResolvePermissionExpr(ee1, context, twoStateContext, specContext, pos)(inPredicate);
     val pp = PermMinus(e0, e1)
     pp.pos = p.pos;
     pp
   case a @ Access(sel @ MemberAccess(e, id),Epsilon) =>
     var exp: Expression = sel
     var typ: Class = null
     if (e.getClass == classOf[ImplicitThisExpr]) { // id could be a local variable, if e == ImplicitThisExpr()
       val ve = VariableExpr(id)
       context.LookupVariable(id) match {
         case Some(v) => ve.Resolve(v); typ = ve.typ; exp = ve;
         case None =>
       }
     }
     if (typ == null) {
       ResolveExpr(e, context, twoStateContext, false)
       e.typ.LookupMember(id) match {
         case None =>
           context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)
         case Some(f: Field) => sel.f = f; typ = f.typ.typ
         case Some(pred@Predicate(id, body)) =>
           sel.predicate = pred;
           sel.isPredicate = true;
           typ = BoolClass
         case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
       }
       sel.typ = typ
       exp = sel
     }
     var p: Permission = Epsilon
     typ match {
       case BoolClass if sel.isPredicate =>
         p = PredicateEpsilon(Some(sel))
         p.pos = a.pos
       case IntClass =>
         p = Epsilons(exp)
         p.pos = a.pos
       case TokenClass(c, m) =>
         p = ForkEpsilon(exp)
         p.pos = a.pos
       case c:Channel =>
         p = ChannelEpsilon(Some(exp))
         p.pos = a.pos
       case c:Class if (c.IsNormalClass) =>
         p = MonitorEpsilon(Some(exp))
         p.pos = a.pos
       case null =>
         // ignore, found error earlier
         p = Star
       case _ =>
         context.Error(a.pos, "type " + typ.FullName + " of variable " + id + " is not supported inside a rd expression.")
         p = Star
     }
     exp.pos = a.pos
     p
   // multiplication is a bit tricky: we want to support integer multiplication i0*i1 (which will
   // correspond to a percentage i0*i1), but also the multiplication of an integer i0 with a permission
   // amount p1 (and vice versa): i0*p1 or p0*i1.
   // we first try to resolve both expressions as integer, and if not successful, try again as
   // permission amount
   case bin @ Times(e0, e1) =>
     var p0, p1: Permission = null
     var ee0 = e0
     var ee1 = e1
     var oldErrors = (new ListBuffer[(Position,String)]) ++= context.errors
     ResolveExpr(bin.E0, context, twoStateContext, false)
     if (context.errors.size > oldErrors.size) {
       context.errors.clear; context.errors ++= oldErrors // reset errors
       p0 = ResolvePermissionExpr(bin.E0, context, twoStateContext, specContext, pos)(inPredicate)
       ee0 = p0
     }
     
     oldErrors = (new ListBuffer[(Position,String)]) ++= context.errors
     ResolveExpr(bin.E1, context, twoStateContext, false)
     if (context.errors.size > oldErrors.size) {
       context.errors.clear; context.errors ++= oldErrors // reset errors
       p1 = ResolvePermissionExpr(bin.E1, context, twoStateContext, specContext, pos)(inPredicate)
       ee1 = p1
     }
     
     if (ee0.typ.IsInt && ee1.typ.IsInt) {
       bin.typ = IntClass
       val pp = Frac(bin)
       pp.pos = bin.pos
       pp
     } else if (ee0.typ.IsInt && ee1.typ.IsPermission) {
       val pp = IntPermTimes(ee0,p1)
       pp.pos = bin.pos
       pp
     } else if (ee0.typ.IsPermission && ee1.typ.IsInt) {
       val pp = IntPermTimes(ee1,p0)
       pp.pos = bin.pos
       pp
     } else {
       context.Error(pos, "multiplication of permission amounts not supported"); Star
     }
   case expr =>
     ResolveExpr(expr, context, twoStateContext, specContext)(inPredicate);
     if (expr.typ == IntClass) {
       val pp = Frac(expr)
       pp.pos = expr.pos;
       pp
     } else {
       context.Error(pos, "expression of type " + expr.typ.FullName + " invalid in permission"); Star
     }
 }
 
 // does e contain a Star (i.e., rd*)?
 def ContainsStar(expr: Expression): Boolean = {
   var x: Boolean = false
   AST.visit(expr,
     e => e match {
       case Star => x = true
       case _ =>
     }
   )
   x
 }
 
 // does e contain 'waitlevel'?
 def ContainsWaitlevel(expr: Expression): Boolean = {
   var x: Boolean = false
   AST.visit(expr,
     e => e match {
       case _:MaxLockLiteral => x = true
       case _ =>
     }
   )
   x
 }

 // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field
 def ResolveExpr(e: RValue, context: ProgramContext,
                 twoStateContext: Boolean, specContext: Boolean)(implicit inPredicate: Boolean): Unit = e match {
   case e @ NewRhs(id, initialization, lower, upper) =>
     if (context.decls contains id) {
       context.decls(id) match {
         case ch: Channel =>
           e.typ = ChannelClass(ch)
         case cl: Class =>
           e.typ = cl
           if (lower != Nil || upper != Nil)
             context.Error(e.pos, "A new object of a class type is not allowed to have a wait-order bounds clause (use the share statement instead)")
       }
       // initialize the fields
       var fieldNames = Set[String]()
       for(ini@Init(f, init) <- initialization) {
         if (fieldNames contains f) {
           context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.")
         } else {
           fieldNames = fieldNames + f
           e.typ.LookupMember(f) match {
             case Some(field@Field(name, tp, _)) =>
               if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");
               ResolveExpr(init, context, false, false);
               if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");
               ini.f = field;
             case _ => 
               context.Error(e.pos, "The type " + id + " does not declare a field " + f + ".");  
           }
         }
       }
       // resolve the bounds
       ResolveBounds(lower, upper, context, "new")
     } else {
       context.Error(e.pos, "undefined class or channel " + id + " used in new expression")
       e.typ = IntClass
     }
   case i:IntLiteral =>
     i.typ = IntClass
   case b:BoolLiteral =>
     b.typ = BoolClass
   case n:NullLiteral =>
     n.typ = NullClass
   case s:StringLiteral =>
     s.typ = StringClass
   case mx:MaxLockLiteral =>
     mx.typ = MuClass
   case mx:LockBottomLiteral =>
     mx.typ = MuClass
   case _:BoogieExpr =>
     throw new InternalErrorException("boogie expression unexpected here")
   case r:Result =>
     assert(context.currentMember!=null);
     r.typ = IntClass
     if(context.currentMember==null || ! context.currentMember.isInstanceOf[Function]){
       context.Error(r.pos, "The variable result can only be used in the postcondition of a function.");
     } else {
       r.typ = context.currentMember.asInstanceOf[Function].out.typ;
     }
   case ve @ VariableExpr(id) =>
     context.LookupVariable(id) match {
       case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass
       case Some(v) => ve.Resolve(v) }
   case v:ThisExpr => 
     v.typ = context.currentClass
     if (context.IsStatic) {
       context.Error(v.pos, "Accessing non-static member not allowed in static context.")
     }
   case sel @ MemberAccess(e, id) =>
     ResolveExpr(e, context, twoStateContext, false)
     var typ: Class = IntClass
     e.typ.LookupMember(id) match {
       case None =>
         context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)
       case Some(f: Field) => sel.f = f; typ = f.typ.typ
       case Some(pred@Predicate(id, body)) =>
         if(! specContext)
           context.Error(sel.pos, "predicate can only be used in positive predicate contexts")
         sel.predicate = pred;
         sel.isPredicate = true;
         typ = BoolClass
       case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);
     }
     sel.typ = typ
   case p: Permission => context.Error(p.pos, "permission not expected here.")
   case expr @ Access(e, perm) =>
     if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
     ResolveExpr(e, context, twoStateContext, true)
     val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
     expr.perm = p;
     expr.typ = BoolClass
   case expr @ AccessAll(obj, perm) =>
     if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
     ResolveExpr(obj, context, twoStateContext, false)
     if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")
     val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
     expr.perm = p;
     expr.typ = BoolClass
   case expr @ AccessSeq(s, f, perm) =>
     if (!specContext) context.Error(expr.pos, permExpressionName(perm) + " expression is allowed only in positive predicate contexts")
     ResolveExpr(s, context, twoStateContext, false)
     if(!s.typ.IsSeq) context.Error(expr.pos, "Target of [*] must be sequence.")
     val p = ResolvePermissionExpr(perm match { case Frac(f) => f; case o => o;}, context, twoStateContext, false, expr.pos);
     expr.perm = p;
     f match {
       case Some(x) =>
         ResolveExpr(x, context, twoStateContext, true);
       case _ => }
     expr.typ = BoolClass
   case expr@ Credit(e,n) =>
     if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts")
     ResolveExpr(e, context, twoStateContext, false)
     if(!e.typ.IsChannel) context.Error(expr.pos, "credit argument must denote a channel.")
     ResolveExpr(expr.N, context, twoStateContext, false)
     expr.typ = BoolClass
   case expr@ Holds(e) =>
     if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")
     ResolveExpr(e, context, twoStateContext, false)
     expr.typ = BoolClass
   case expr@ RdHolds(e) =>
     if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates")
     ResolveExpr(e, context, twoStateContext, false)
     expr.typ = BoolClass
   case expr@ Assigned(id) =>
     context.LookupVariable(id) match {
       case None => context.Error(expr.pos, "undefined local variable " + id)
       case Some(v) =>
         expr.v = v
         if (!(v.isImmutable && v.isGhost))
           context.Error(expr.pos, "assigned can only be used with ghost consts")
     }
     expr.typ = BoolClass
   case expr@ Old(e) =>
     if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") }
     ResolveExpr(e, context, twoStateContext, false)
     expr.typ = e.typ
   case ite@IfThenElse(con, then, els) => 
     ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext);
     if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean");
     if (!canAssign(then.typ, els.typ) && !canAssign(els.typ, then.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types");
     ite.typ = then.typ;
   case expr@ Not(e) =>
     ResolveExpr(e, context, twoStateContext, false)
     if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")
     expr.typ = BoolClass
   case appl@FunctionApplication(obj, id, args) =>
     // HACK: allow non-static access for receiver
     ResolveExpr(obj, context.AsNonStatic(), twoStateContext, false);
     args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};
     // lookup function
     appl.typ = IntClass
     obj.typ.LookupMember(id) match {
       case None =>
         context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName)
       case Some(func@Function(f, ins, out, specs, body)) =>
         appl.f = func
         appl.typ = func.out.typ;
         if (args.length != ins.length)
           context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id +
                         " (" + args.length + " instead of " + ins.length + ")")
         else {
           for((actual, formal) <- args zip func.ins){
             if(! canAssign(formal.t.typ, actual.typ))
               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
           }
         }
       case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function")
     }
   case uf@Unfolding(pred, e) =>
     ResolveExpr(pred, context, twoStateContext, true);
     ResolveExpr(e, context, twoStateContext, false);
     if(! pred.ma.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
     uf.typ = e.typ;
   case bin: EqualityCompareExpr =>
     ResolveExpr(bin.E0, context, twoStateContext, false)
     ResolveExpr(bin.E1, context, twoStateContext, false)
     if (bin.E0.typ == bin.E1.typ) { /* all is well */ }
     else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ }
     else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ }
     else
       context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName)
     bin.typ = BoolClass
   case bin: LockBelow =>
     ResolveExpr(bin.E0, context, twoStateContext, false)
     ResolveExpr(bin.E1, context, twoStateContext, false)
     if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu))
       context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")")
     if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu))
       context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")")
     bin.typ = BoolClass
   case app@Append(e0, e1) =>
     ResolveExpr(e0, context, twoStateContext, false);
     ResolveExpr(e1, context, twoStateContext, false);
     if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ").");
     if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ").");
     if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type.");
     app.typ = e0.typ;
   case at@At(e0, e1) =>
     ResolveExpr(e0, context, twoStateContext, false);
     ResolveExpr(e1, context, twoStateContext, false);
     if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ").");
     if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ").");
     if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass;
   case drop@Drop(e0, e1) =>
     ResolveExpr(e0, context, twoStateContext, false);
     ResolveExpr(e1, context, twoStateContext, false);
     if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ").");
     if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ").");
     drop.typ = e0.typ;
   case take@Take(e0, e1) =>
     ResolveExpr(e0, context, twoStateContext, false);
     ResolveExpr(e1, context, twoStateContext, false);
     if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ").");
     if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ").");
     take.typ = e0.typ;
   case contains@Contains(e0, e1) =>
     ResolveExpr(e0, context, twoStateContext, false);
     ResolveExpr(e1, context, twoStateContext, false);
     if(! e1.typ.IsSeq)
       context.Error(contains.pos, "RHS operand of 'in' must be sequence. (found: " + e1.typ.FullName + ").");
     else if(! canAssign(e1.typ.parameters(0), e0.typ))
       context.Error(contains.pos, "LHS operand's type must be element type of sequence. (found: " + e0.typ.FullName + ", expected: " + e1.typ.parameters(0).FullName + ").");
     contains.typ = BoolClass;
   case bin: BinaryExpr =>
     ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])
     ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))
     if (bin.E0.typ != bin.ExpectedLhsType)
       context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" +
                     " (expected " + bin.ExpectedLhsType.FullName + 
                     ", found " + bin.E0.typ.FullName + ")")
     if (bin.E1.typ != bin.ExpectedRhsType)
       context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" +
                     " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")
     bin.typ = bin.ResultType
   case q: Quantification =>
     q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") };
     val typ = q match {
       case q: SeqQuantification =>
         ResolveExpr(q.seq, context, twoStateContext, false);
         if(! q.seq.typ.IsSeq) {
           context.Error(q.seq.pos, "A quantification must range over a sequence. (found: " + q.seq.typ.FullName + ").");
           None;
         } else
           Some(q.seq.typ.parameters(0));
       case q: TypeQuantification =>
         ResolveType(q.t, context);
         if (q.t.typ == null) None else Some(q.t.typ);
     };

     if (typ.isDefined) {
       val vartype = typ.get;
       var bodyContext = context;
       var bvariables = Nil: List[Variable];
       q.Is foreach { i =>
         val variable = new Variable(i, new Type(vartype));
         bodyContext = bodyContext.AddVariable(variable);
         bvariables = bvariables ::: List(variable);
       }
       ResolveExpr(q.E, bodyContext, twoStateContext, true);
       if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " +  q.E.typ.FullName + ").");
       q.variables = bvariables;
     }
     q.typ = BoolClass
   case seq@EmptySeq(t) =>
     ResolveType(t, context)
     seq.typ = SeqClass(t.typ);
   case seq@ExplicitSeq(es) =>
     es foreach { e => ResolveExpr(e, context, twoStateContext, false) }
     es match {
       case Nil => seq.typ = SeqClass(IntClass);
       case h :: t =>
         t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")};
         seq.typ = SeqClass(h.typ);
     }
   case ran@Range(min, max) =>
     ResolveExpr(min, context, twoStateContext, false);
     if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ").");
     ResolveExpr(max, context, twoStateContext, false);
     if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ").");
     ran.typ = SeqClass(IntClass);
   case len@Length(e) =>
     ResolveExpr(e, context, twoStateContext, false);
     if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ").");
     len.typ = IntClass;
   case ev@Eval(h, e) =>
     if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates")
     h match {
       case AcquireState(obj) => 
         ResolveExpr(obj, context, twoStateContext, false)
         if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
       case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false)
         if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");
       case c@CallState(token, obj, id, args) =>
         ResolveExpr(token, context, twoStateContext, false);
         if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");
         ResolveExpr(obj, context, false, false)
         CheckNoGhost(obj, context)
         args foreach { a => a match {
            case VariableExpr("?") => 
            case _ => ResolveExpr(a, context, false, false); CheckNoGhost(a, context)
         }}
         // lookup method
         var typ: Class = IntClass
         obj.typ.LookupMember(id) match {
           case None =>
             context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)
           case Some(m: Method) =>
             c.m = m
             if (args.length != m.ins.length)
               context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +
                         " (" + args.length + " instead of " + m.ins.length + ")")
             else {
               for((actual, formal) <- args zip m.ins){
                 actual match {
                    case VariableExpr("?") =>
                    case _ => if (!canAssign(formal.t.typ, actual.typ))
                        context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
                 }
                 
             }
           }
         case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
     }
           
         
     }
     ResolveExpr(e, context, false, specContext)
     ev.typ = e.typ;
 }

 def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = {
   cl.LookupMember(runMethod) match {
     case None =>
       context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
                     " (found type " + cl.id + ")")
       None
     case Some(m: Method) =>
       m.spec foreach {
         case Precondition(e) => CheckRunSpecification(e, context, true)
         case Postcondition(e) => CheckRunSpecification(e, context, false)
         case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method")
       }
       if(0<m.ins.length || 0<m.outs.length) {
         context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
                     " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None
       } else
         Some(m)
     case _ =>
       context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +
                     " (found non-method member)")
       None
   }
 }

 // assumes that lhs and rhs are resolved
 def canAssign(lhs: Class, rhs: Class): Boolean = {
   (lhs, rhs) match {
     case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2)
     case (TokenClass(c1, m1), _) => false
     case (_, TokenClass(c2, m2)) => false
     case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull)
   }
 }

 def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = {
   AST.visit(expr, e => e match {
     case ve: VariableExpr =>
       if (ve.v != null && ve.v.isGhost) context.Error(ve.pos, "ghost variable not allowed here")
     case fs@ MemberAccess(e, id) =>
       if (!fs.isPredicate && fs.f != null && fs.f.isGhost) context.Error(fs.pos, "ghost fields not allowed here")
     case a: Assigned =>
       if (a.v != null && a.v.isGhost) context.Error(a.pos, "ghost variable not allowed here")
     case _ => // do nothing
   })   
 }

 def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {
   AST.visit(expr, e => e match {
     case ve: VariableExpr =>
       if (ve.v != null && ve.v.isGhost && ve.v.isImmutable) context.Error(ve.pos, "ghost const not allowed here")
     case a: Assigned =>
       if (a.v != null && a.v.isGhost && a.v.isImmutable) context.Error(a.pos, "ghost const not allowed here")
     case _ => // do nothing
   })
 }

 def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: Boolean): Unit = e match {
   case _:MaxLockLiteral =>
     if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention waitlevel here")
   case _:Literal =>
   case _:VariableExpr =>
   case _:ThisExpr =>
   case _:Result =>
   case _:BoogieExpr =>
   case MemberAccess(e, id) =>
     CheckRunSpecification(e, context, false)
   case Frac(perm) => CheckRunSpecification(perm, context, false)
   case Epsilons(perm) => CheckRunSpecification(perm, context, false)
   case PermPlus(p0, p1) =>
     CheckRunSpecification(p0, context, false)
     CheckRunSpecification(p1, context, false)
   case PermMinus(p0, p1) =>
     CheckRunSpecification(p0, context, false)
     CheckRunSpecification(p1, context, false)
   case PermTimes(p0, p1) =>
     CheckRunSpecification(p0, context, false)
     CheckRunSpecification(p1, context, false)
   case IntPermTimes(p0, p1) =>
     CheckRunSpecification(p0, context, false)
     CheckRunSpecification(p1, context, false)
   case Full | Epsilon | Star | MethodEpsilon =>
   case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) =>;
   case ChannelEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
   case PredicateEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
   case MonitorEpsilon(Some(e)) => CheckRunSpecification(e, context, false);
   case ForkEpsilon(tk) => CheckRunSpecification(tk, context, false);
   case Access(e, perm) =>
     CheckRunSpecification(e, context, false);
     CheckRunSpecification(perm, context, false);
   case AccessAll(obj, perm) =>
     CheckRunSpecification(obj, context, false);
     CheckRunSpecification(perm, context, false);
   case AccessSeq(s, f, perm) =>
     CheckRunSpecification(s, context, false);
     CheckRunSpecification(perm, context, false);
   case expr@ Credit(e, n) =>
     CheckRunSpecification(e, context, false)
     CheckRunSpecification(expr.N, context, false)
   case Holds(e) =>
     context.Error(e.pos, "holds is not allowed in specification of run method")
   case RdHolds(e) =>
     context.Error(e.pos, "rd holds is not allowed in specification of run method")
   case _:Assigned =>
   case Old(e) =>
     CheckRunSpecification(e, context, false)  // OLD occurs only in postconditions and monitor invariants, where waitlevel is not allowed anyhow
   case IfThenElse(con, then, els) =>
     CheckRunSpecification(con, context, false);
     CheckRunSpecification(con, context, allowMaxLock); 
     CheckRunSpecification(con, context, allowMaxLock); 
   case Not(e) =>
     CheckRunSpecification(e, context, false)
   case FunctionApplication(obj, id, args) =>
     obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} 
   case Unfolding(pred, e) =>
     CheckRunSpecification(pred, context, true);
     CheckRunSpecification(e, context, allowMaxLock);
   case LockBelow(e0,e1) =>
     CheckRunSpecification(e0, context, allowMaxLock)
     CheckRunSpecification(e1, context, false)
   case And(e0,e1) =>
     CheckRunSpecification(e0, context, allowMaxLock)
     CheckRunSpecification(e1, context, allowMaxLock)
   case Implies(e0,e1) =>
     CheckRunSpecification(e0, context, false)
     CheckRunSpecification(e1, context, allowMaxLock)
   case bin: BinaryExpr =>
     CheckRunSpecification(bin.E0, context, false)
     CheckRunSpecification(bin.E1, context, false)
   case q: SeqQuantification =>
     CheckRunSpecification(q.seq, context, false)
     CheckRunSpecification(q.e, context, true)
   case q: TypeQuantification =>
     CheckRunSpecification(q.e, context, true)
   case Length(e) =>
     CheckRunSpecification(e, context, false);
   case ExplicitSeq(es) =>
     es foreach { e => CheckRunSpecification(e, context, false) }
   case Range(min, max) =>
     CheckRunSpecification(min, context, false)
     CheckRunSpecification(max, context, false)
   case Eval(h, e) =>
     h match {
       case AcquireState(obj) =>  CheckRunSpecification(obj, context, false);
       case ReleaseState(obj) =>  CheckRunSpecification(obj, context, false);
       case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false);  args foreach { a: Expression => CheckRunSpecification(a, context, false)};
     }
     CheckRunSpecification(e, context, allowMaxLock)
 }

 def ResolveTransform(mt: MethodTransform, baseContext: ProgramContext) {
   val context = baseContext.SetClass(mt.Parent).SetMember(mt);

   mt.spec foreach {
     case Precondition(e) =>
       context.Error(e.pos, "Method refinement cannot add a pre-condition")
     case Postcondition(e) =>
       ResolveExpr(e, context, true, true)(false)
     case _ : LockChange => throw new NotSupportedException("not implemented")
   }
   if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have the same input arguments")
   if (! mt.outs.startsWith(mt.refines.Outs)) context.Error(mt.pos, "Refinement must declare all abstract output variables")

   mt.body = AST.refine(mt.refines.Body, mt.trans) match {
     case AST.Matched(ss) => ss
     case AST.Unmatched(t) => context.Error(mt.pos, "Cannot match transform around " + t.pos); Nil
   }
                                
   /**
    * We thread two contexts for the concrete and abstract versions.
    */
   def resolveBody(ss: List[Statement], 
     concreteContext: ProgramContext,
     abstractContext: List[Variable]) {
     var ctx = concreteContext;
     var locals = abstractContext;
     for (s <- ss) { 
       s match {
         case r @ RefinementBlock(c, a) =>
           // abstract globals available at this point in the program
           r.before = locals;

           // resolve concrete version
           ResolveStmt(BlockStmt(c), ctx)

           // compare declared local variables
           val vs = c flatMap {s => s.Declares};
           for (s <- a;
                v <- s.Declares; 
                if (! vs.contains(v)))
             ctx.Error(r.pos, "Refinement block must declare a local variable from the abstract program: " + v.id)
         case w @ WhileStmt(guard, oi, ni, lks, body) =>
           for (inv <- ni) {
             ResolveExpr(inv, ctx, true, true)(false)
             if (!inv.typ.IsBool) ctx.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")
           }
           resolveBody(body.ss, ctx, locals)
           w.LoopTargets = body.Targets.filter(ctx.IsVariablePresent).toList
         case IfStmt(_, thn, None) =>
           resolveBody(thn.ss, ctx, locals)
         case IfStmt(_, thn, Some(els)) =>
           resolveBody(thn.ss, ctx, locals)
           resolveBody(List(els), ctx, locals)
         case BlockStmt(ss) =>
           resolveBody(ss, ctx, locals)
         case _ =>   
       }

       // declare concrete and abstract locals
       for (v <- s.Declares) ctx = ctx.AddVariable(v);
       s match {
         case RefinementBlock(_, a) => locals = locals ++ (a flatMap {s => s.Declares})
         case _ => locals = locals ++ s.Declares 
       }
     }
   }

   resolveBody(mt.body, context, mt.refines.Ins ++ mt.refines.Outs)
 }

 def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {
   assert (cl.IsRefinement)
   for (id <- ci.ids) cl.refines.LookupMember(id) match {
     case Some(f: Field) => ci.fields = f :: ci.fields
     case Some(_) => context.Error(ci.pos, "coupling invariant can only be bound to a field of the abstract program")
     case None => context.Error(ci.pos, "coupling invariant does not refer to a member of the abstract program")
   }
   ResolveExpr(ci.e, context.SetClass(cl).SetMember(ci), false, true)(true)
   if (!ci.e.typ.IsBool) context.Error(ci.pos, "coupling invariant requires a boolean expression (found " + ci.e.typ.FullName + ")")
   // TODO: check coupling invariant may only give permissions to newly declared fields
   // TODO: check concrete body cannot refer to replaced fields
 }
 
 // TODO: this method might need to be replaced at some point. it is not possible
 // to decide what name is used on the source level just by the permission (e.g.,
 // Epsilons can be rd(x,1) or acc(x,rd(1))
 def permExpressionName(perm: Permission): String = {
   perm match {
     case _:Epsilons => "rd";
     case Epsilon => "rd";
     case MethodEpsilon => "rd"
     case Star => "rd";
     case Full => "acc";
     case _:Frac => "acc";
     case _:ArithmeticPermission => "acc";
     case _:ChannelEpsilon | _:ForkEpsilon | _:MonitorEpsilon | _:PredicateEpsilon => "acc";
   }
 }
}