diff options
Diffstat (limited to 'Chalice/src/main/scala/Resolver.scala')
| -rw-r--r-- | Chalice/src/main/scala/Resolver.scala | 1494 |
1 files changed, 0 insertions, 1494 deletions
diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala deleted file mode 100644 index 5dc24662..00000000 --- a/Chalice/src/main/scala/Resolver.scala +++ /dev/null @@ -1,1494 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// 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";
- }
- }
-}
|