From 96b51321e63a424bf0f8ae87a4440402bd3e8f1b Mon Sep 17 00:00:00 2001 From: kyessenov Date: Tue, 17 Aug 2010 00:55:40 +0000 Subject: Chalice: refactored AST code for class hierarchy (no need for caches since Scala uses structural equality for case classes); landed first piece of refinement code --- Chalice/src/Ast.scala | 96 ++++++++++++++++----------- Chalice/src/Graph.scala | 21 +++++- Chalice/src/Parser.scala | 52 +++++++++++++-- Chalice/src/PrettyPrinter.scala | 6 +- Chalice/src/Resolver.scala | 143 ++++++++++++++++++++++++++-------------- Chalice/src/Translator.scala | 34 ++++------ 6 files changed, 234 insertions(+), 118 deletions(-) (limited to 'Chalice/src') diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 5ca0f98a..aaaf7fc9 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -16,18 +16,7 @@ trait ASTNode extends Positional case class TopLevelDecl(id: String) extends ASTNode -// this is in fact root of type hierarchy (confusingly, called "class") sealed case class Class(classId: String, parameters: List[Class], module: String, members: List[Member]) extends TopLevelDecl(classId) { - var mm = Map[String,Member]() - def LookupMember(id: String): Option[Member] = { - if (mm.keys exists { i => i.equals(id)}) - Some(mm(id)) - else if (IsRef && (RootClass.mm contains id)) { - val m = RootClass.mm(id) - if (m.Hidden) None else Some(m) - } else - None - } def IsInt: Boolean = false def IsBool: Boolean = false def IsRef: Boolean = true @@ -38,22 +27,41 @@ sealed case class Class(classId: String, parameters: List[Class], module: String def IsChannel: Boolean = false def IsState: Boolean = false def IsNormalClass = true; - var IsExternal = false; // says whether or not to compile the class (compilation ignores external classes) - def Fields: List[Field] = { - members flatMap (m => m match { case f:Field => List(f) case _ => List() }) + lazy val Fields: List[Field] = members flatMap {case x: Field => List(x); case _ => Nil} + lazy val MentionableFields = Fields filter {x => ! x.Hidden} + lazy val Invariants: List[MonitorInvariant] = members flatMap {case x: MonitorInvariant => List(x); case _ => Nil} + lazy val id2member:Map[String,NamedMember] = Map() ++ { + val named = members flatMap {case x: NamedMember => List(x); case _ => Nil}; + (named map {x => x.Id}) zip named } - def Invariants: List[MonitorInvariant] = { - (members :\ List[MonitorInvariant]()) { (m,list) => m match { - case m:MonitorInvariant => m :: list - case _ => list }} + def LookupMember(id: String): Option[NamedMember] = { + if (id2member contains id) + Some(id2member(id)) + else if (IsRef && this != RootClass) { + // check with root class + RootClass LookupMember id match { + case Some(m) if (! m.Hidden) => Some(m) + case _ => None + } + } else + None } def FullName: String = if(parameters.isEmpty) id else id + "<" + parameters.tail.foldLeft(parameters.head.FullName){(a, b) => a + ", " + b.FullName} + ">" + override def toString = FullName + + // Says whether or not to compile the class (compilation ignores external classes) + var IsExternal = false; + + // Refinement extension + var IsRefinement = false; + var refinesId: String = null; + var refines: Class = null; } sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId) -case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) { +sealed case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) { override def IsRef = false; override def IsSeq = true; override def IsNormalClass = false; @@ -85,8 +93,7 @@ case class TokenClass(c: Type, m: String) extends Class("token", Nil, "default", override def IsRef = true; override def IsToken = true; override def IsNormalClass = false; - override def FullName: String = "token<" + c.FullName + "." + m + ">" - mm = mm.+(("joinable", Fields(0))); + override def FullName: String = "token<" + c.FullName + "." + m + ">" } case class ChannelClass(ch: Channel) extends Class(ch.id, Nil, "default", Nil) { override def IsRef = true; @@ -99,9 +106,6 @@ object RootClass extends Class("$root", Nil, "default", List( new SpecialField("held", new Type(BoolClass)){ override val Hidden = true }, new SpecialField("rdheld", new Type(BoolClass)){ override val Hidden = true } )) // joinable and held are bool in Chalice, but translated into an int in Boogie -{ - def MentionableFields = Fields filter {fld => fld.id != "held" && fld.id != "rdheld"} -} sealed case class Type(id: String, params: List[Type]) extends ASTNode { // denotes the use of a type var typ: Class = null @@ -147,21 +151,17 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci var SCC: List[Function] = Nil; } case class Condition(id: String, where: Option[Expression]) extends NamedMember(id) -class Variable(name: String, typ: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode { - val id = name - val t = typ - val IsGhost = isGhost - val IsImmutable = isImmutable +case class Variable(id: String, t: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode { val UniqueName = { val n = Variable.VariableCount Variable.VariableCount = Variable.VariableCount + 1 - name + "#" + n + id + "#" + n } def this(name: String, typ: Type) = this(name,typ,false,false); - override def toString = (if (IsGhost) "ghost " else "") + (if (IsImmutable) "const " else "var ") + id; + override def toString = (if (isGhost) "ghost " else "") + (if (isImmutable) "const " else "var ") + id; } object Variable { var VariableCount = 0 } -class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) { +case class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) { override val UniqueName = name } sealed abstract class Specification extends ASTNode @@ -169,6 +169,23 @@ case class Precondition(e: Expression) extends Specification case class Postcondition(e: Expression) extends Specification case class LockChange(ee: List[Expression]) extends Specification +/** + * Refinement members + */ + +sealed abstract class Refinement(id: String) extends NamedMember(id) { + var refines = null: NamedMember; +} +case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Refinement(id) + +sealed abstract class Transform extends ASTNode +case class BlockPattern() extends Transform // pattern within a block (*) +case class ProgramPattern() extends Transform // can match entire block (*) +case class IfPattern(thn: Transform, els: Option[Transform]) extends Transform +case class NonDetPattern(code: BlockStmt) extends Transform // matches var or spec +case class InsertPattern(code: Statement) extends Transform +case class SequencePattern(pats: List[Transform]) extends Transform + /** * Statements */ @@ -256,14 +273,15 @@ case class VariableExpr(id: String) extends Expression { def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ } } case class Result() extends Expression -sealed abstract class ThisExpr extends Expression { - override def equals(other: Any): Boolean = { - // needed in autoMagic, which checks for syntactic equality using equals - other.isInstanceOf[ThisExpr] - } +sealed abstract class ThisExpr extends Expression +case class ExplicitThisExpr() extends ThisExpr { + override def hashCode = 0; + override def equals(other: Any) = other.isInstanceOf[ThisExpr] +} +case class ImplicitThisExpr() extends ThisExpr { + override def hashCode = 0; + override def equals(other: Any) = other.isInstanceOf[ThisExpr] } -case class ExplicitThisExpr() extends ThisExpr -case class ImplicitThisExpr() extends ThisExpr case class MemberAccess(e: Expression, id: String) extends Expression { var isPredicate: Boolean = false; var f: Field = null diff --git a/Chalice/src/Graph.scala b/Chalice/src/Graph.scala index bcf44bea..e61e482c 100644 --- a/Chalice/src/Graph.scala +++ b/Chalice/src/Graph.scala @@ -54,10 +54,29 @@ class DiGraph[T] { assert (rep contains t); immutable.Set() ++ (rep(t).children map {x => x.data}) } + + // Compute topological sort (edges point in forward direction in the list) + // Terminates but incorrect if not a DAG. + def computeTopologicalSort: List[T] = { + rep.values foreach {v => assert(!v.onstack)} + var l: List[T] = Nil; + + def tarjan(v: Node[T]) { + if (! v.onstack) { + v.onstack = true; + for (w <- v.children) tarjan(w) + l = v.data :: l; + } + } + + rep.values foreach {v => tarjan(v)} + rep.values foreach {v => assert(v.onstack); v.onstack = false;} + l + } // Compute condensation of the digraph. // The resulting digraph has no self loops - def computeSCC(): (DiGraph[List[T]],mutable.Map[T,List[T]]) = { + def computeSCC: (DiGraph[List[T]],mutable.Map[T,List[T]]) = { // Tarjan's algorithm for finding strongly connected components // http://algowiki.net/wiki/index.php/Tarjan%27s_algorithm rep.values foreach {x => assert(x.index == -1 && x.lowlink == -1 && !x.onstack)}; diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 101d6eb0..15b0e33f 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -13,6 +13,8 @@ import scala.util.parsing.input.NoPosition import java.io.File class Parser extends StandardTokenParsers { + + def parseStdin = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in))) def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file))) @@ -30,13 +32,17 @@ class Parser extends StandardTokenParsers { "predicate", "function", "free", "send", "receive", "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", "seq", "nil", "result", "eval", "token", - "wait", "signal") + "wait", "signal", + "refines", "transforms" + ) // todo: can we remove "nil"? lexical.delimiters += ("(", ")", "{", "}", "[[", "]]", "<==>", "==>", "&&", "||", "==", "!=", "<", "<=", ">=", ">", "<<", "in", "!in", "+", "-", "*", "/", "%", "!", ".", "..", - ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::") + ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::", + "_" + ) def programUnit = (classDecl | channelDecl)* def Semi = ";" ? @@ -47,10 +53,12 @@ class Parser extends StandardTokenParsers { */ def classDecl = - positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ { - case ext ~ id ~ module ~ _ ~ members => + positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ opt("refines" ~> ident) ~ + ("{" ~> (memberDecl*) <~ "}") ^^ { + case ext ~ id ~ module ~ refines ~ members => val cl = Class(id, Nil, module.getOrElse("default"), members) - ext match { case None => case Some(t) => cl.IsExternal = true } + if (ext.isDefined) cl.IsExternal = true + if (refines.isDefined) {cl.IsRefinement = true; cl.refinesId = refines.get} cl }) def channelDecl = @@ -63,7 +71,7 @@ class Parser extends StandardTokenParsers { * Member declarations */ - def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl) + def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | transformDecl) def fieldDecl = ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) } | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) } @@ -87,6 +95,15 @@ class Parser extends StandardTokenParsers { def conditionDecl = "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ { case id ~ optE => Condition(id, optE) } + def transformDecl = { + currentLocalVariables = Set[String]() + "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ + (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ { + case id ~ ins ~ outs ~ spec ~ trans => + MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, trans) + } + } + def formalParameters(immutable: Boolean) = "(" ~> (formalList(immutable) ?) <~ ")" ^^ { @@ -222,6 +239,7 @@ class Parser extends StandardTokenParsers { val lhs = ExtractList(outs) Receive(declareImplicitLocals(lhs), e, lhs) } ) + // this could be slightly changed to make it LL(1) def localVarStmt(const: Boolean, ghost: Boolean) = ( (rep1sep(idType, ",") into {decls:List[(PositionedString,Type)] => { val locals = for ((id, t) <- decls; if (! currentLocalVariables.contains(id.v))) yield { @@ -536,4 +554,26 @@ class Parser extends StandardTokenParsers { def accPermArg : Parser[Write] = opt( "," ~> expression ^^ { case e => Frac(e) }) ^^ { case None => Full; case Some(p) => p} + + /** + * Transforms + */ + + def transform: Parser[Transform] = positioned( + "if" ~> ifTransform + | transformAtom ~ rep(transform) ^^ {case atom ~ t => SequencePattern(atom :: t)} + ) + def transformAtom: Parser[Transform] = positioned( + "_" ~ Semi ^^^ BlockPattern() + | statement ^^ {case s => InsertPattern(s)} + ) + def ifTransform: Parser[IfPattern] = + ("{" ~> transform <~ "}") ~ ("else" ~> ifTransformElse ?) ^^ { + case thn ~ els => IfPattern(thn, els) + } + def ifTransformElse = ( + "if" ~> ifTransform + | "{" ~> transform <~ "}" + ) + } diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 5ec898c5..c10aa9ea 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -9,7 +9,7 @@ object PrintProgram { for (decl <- prog) decl match { case cl: Class => if (cl.IsExternal) print("external ") - println("class " + cl.id + " module " + cl.module + " {") + println("class " + cl.id + " module " + cl.module + (if (cl.IsRefinement) " refines " + cl.refinesId else "") + " {") cl.members foreach Member println("}") case ch: Channel => @@ -97,8 +97,8 @@ object PrintProgram { println(Semi) case SpecStmt(lhs, locals, pre, post) => if (locals.size > 0) { - if (locals(0).IsGhost) print("ghost "); - if (locals(0).IsImmutable) print("const ") else print("var ") + if (locals(0).isGhost) print("ghost "); + if (locals(0).isImmutable) print("const ") else print("var ") } else print("var "); VarList(locals); diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index 360146f5..80cabe62 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -13,7 +13,7 @@ object Resolver { case class Success() extends ResolverOutcome case class Errors(ss: List[(Position,String)]) extends ResolverOutcome - var seqClasses = Map[String, SeqClass](); + val runMethod = "run"; class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) { val Decls = decls @@ -53,14 +53,15 @@ object Resolver { } else { decl match { case cl: Class => + val ids = scala.collection.mutable.Set.empty[String] for (m <- cl.members) m match { case _:MonitorInvariant => case m: NamedMember => m.Parent = cl - if (cl.mm contains m.Id) { + if (ids contains m.Id) { return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id))) } else { - cl.mm = cl.mm + (m.Id -> m) + ids + m.Id } } case ch: Channel => @@ -68,6 +69,52 @@ object Resolver { 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 (! decls(cl.refinesId).isInstanceOf[Class]) { + return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class"))) + } else if (cl.refinesId == cl.id) { + return Errors(List((cl.pos, "class cannot refine itself"))) + } else { + cl.refines = decls(cl.refinesId).asInstanceOf[Class]; + refinesRel.addNode(cl); + refinesRel.addNode(cl.refines); + refinesRel.addEdge(cl, cl.refines); + } + 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 + for (List(cl) <- dag.computeTopologicalSort.reverse) { + if (! cl.IsRefinement) { + // check has no refinement members + if (cl.members.exists{case _: Refinement => true; case _ => false}) + return Errors(List((cl.pos, "non-refinement class cannot have refinement members"))) + } else for (member <- cl.members) member match { + case r: Refinement => + if (! cl.refines.LookupMember(r.Id).isDefined) + return Errors(List((r.pos, "abstract class has no member with name " + r.Id))) + r.refines = cl.refines.LookupMember(r.Id).get + case m: NamedMember => + if (cl.refines.LookupMember(m.Id).isDefined) + return Errors(List((m.pos, "member needs to be a refinement since abstract class has a member with the same name"))) + case _ => + } + } + + // collect errors var errors = List[(Position,String)]() // resolve types of members @@ -78,21 +125,19 @@ object Resolver { ResolveType(v.t, contextNoCurrentClass) } case cl: Class => - for (m <- cl.asInstanceOf[Class].members) m match { - case _:MonitorInvariant => + for (m <- cl.members) m match { + case _: MonitorInvariant => case Field(_, t, _) => ResolveType(t, contextNoCurrentClass) case Method(_, ins, outs, _, _) => - for (v <- ins ++ outs) { - ResolveType(v.t, contextNoCurrentClass) - } - case _:Condition => - case _:Predicate => + for (v <- ins ++ outs) ResolveType(v.t, contextNoCurrentClass) + case _: Condition => + case _: Predicate => case Function(id, ins, out, specs, _) => - for (v <- ins) { - ResolveType(v.t, contextNoCurrentClass) - } + for (v <- ins) ResolveType(v.t, contextNoCurrentClass) ResolveType(out, contextNoCurrentClass) + case mt: MethodTransform => + for (v <- mt.ins ++ mt.outs) ResolveType(v.t, contextNoCurrentClass) } } errors = errors ++ contextNoCurrentClass.errors; @@ -130,7 +175,7 @@ object Resolver { case Precondition(e) => ResolveExpr(e, ctx, false, true)(false) case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false) case lc@LockChange(ee) => - if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") + if(m.id == runMethod) context.Error(lc.pos, "lockchange not allowed on method run") ee foreach (e => ResolveExpr(e, ctx, true, false)(false)) } ResolveStmt(BlockStmt(body), ctx) @@ -170,12 +215,14 @@ object Resolver { } case None => } + case mt: MethodTransform => + ResolveTransform(mt, context) } } errors = errors ++ context.errors } - // fill in SCC + // fill in SCC for recursive functions val (_, h) = calls.computeSCC; h.keys foreach {f:Function => f.SCC = h(f); @@ -214,12 +261,8 @@ object Resolver { t.typ = IntClass } } else { - if(seqClasses.contains(t.FullName)) { - t.typ = seqClasses(t.FullName) - } else if(t.id.equals("seq") && t.params.length == 1) { - val seqt = new SeqClass(t.params(0).typ); - seqClasses = seqClasses + ((seqt.FullName, seqt)); - t.typ = seqt; + 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 @@ -227,16 +270,6 @@ object Resolver { } } - def getSeqType(param: Class, context: ProgramContext): Class = { - if(seqClasses.contains("seq<" + param.FullName + ">")) { - seqClasses("seq<" + param.FullName + ">") - } else { - val seqt = new SeqClass(param); - seqClasses = seqClasses + ((seqt.FullName, seqt)); - seqt - } - } - def ResolveStmt(s: Statement, context: ProgramContext): Unit = s match { case Assert(e) => ResolveExpr(e, context, true, true)(false) @@ -274,7 +307,7 @@ object Resolver { 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) + 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) @@ -305,8 +338,8 @@ object Resolver { 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) + 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) @@ -444,7 +477,7 @@ object Resolver { 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 (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 { @@ -548,7 +581,7 @@ object Resolver { 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) + else if (actual.v.isImmutable) ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter") vars = vars + actual.v } @@ -589,7 +622,7 @@ object Resolver { } 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) + if (lhs.v != null && !lhs.v.isGhost) CheckNoGhost(rhs, context) } // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field @@ -711,7 +744,7 @@ object Resolver { case None => context.Error(expr.pos, "undefined local variable " + id) case Some(v) => expr.v = v - if (!(v.IsImmutable && v.IsGhost)) + if (!(v.isImmutable && v.isGhost)) context.Error(expr.pos, "assigned can only be used with ghost consts") } expr.typ = BoolClass @@ -847,21 +880,21 @@ object Resolver { q.typ = BoolClass case seq@EmptySeq(t) => ResolveType(t, context) - seq.typ = getSeqType(t.typ, context); + seq.typ = SeqClass(t.typ); case seq@ExplicitSeq(es) => es foreach { e => ResolveExpr(e, context, twoStateContext, false) } es match { - case Nil => seq.typ = getSeqType(IntClass, context); + 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 = getSeqType(h.typ, context); + 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 = getSeqType(IntClass, context); + 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 + ")."); @@ -906,7 +939,7 @@ object Resolver { } def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = { - cl.LookupMember("run") match { + 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 + ")") @@ -943,11 +976,11 @@ object Resolver { def specOk(e: RValue): Unit = { e match { case ve: VariableExpr => - if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here") + 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") + if (a.v != null && a.v.isGhost) context.Error(a.pos, "ghost variable not allowed here") case _ => // do nothing } } @@ -958,9 +991,9 @@ object Resolver { def specOk(e: RValue): Unit = { e match { case ve: VariableExpr => - if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here") + 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") + if (a.v != null && a.v.isGhost && a.v.isImmutable) context.Error(a.pos, "ghost const not allowed here") case _ => // do nothing } } @@ -1023,9 +1056,9 @@ object Resolver { CheckRunSpecification(bin.E1, context, false) case q: SeqQuantification => CheckRunSpecification(q.seq, context, false) - CheckRunSpecification(q.E, context, true) + CheckRunSpecification(q.e, context, true) case q: TypeQuantification => - CheckRunSpecification(q.E, context, true) + CheckRunSpecification(q.e, context, true) case Length(e) => CheckRunSpecification(e, context, false); case ExplicitSeq(es) => @@ -1041,4 +1074,16 @@ object Resolver { } CheckRunSpecification(e, context, allowMaxLock) } + + def ResolveTransform(mt: MethodTransform, context: ProgramContext) { + mt.refines match { + case m: Method => + if (mt.ins != m.ins) context.Error(mt.pos, "Refinement must have same input arguments") + if (! mt.outs.startsWith(m.outs)) context.Error(mt.pos, "Refinement must declare all concrete output variables") + case r: MethodTransform => + if (mt.ins != r.ins) context.Error(mt.pos, "Refinement must have same input arguments") + if (! mt.outs.startsWith(r.outs)) context.Error(mt.pos, "Refinement must declare all concrete output variables") + case _ => context.Error(mt.pos, "Method can only refine another method or a transform") + } + } } diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index db79df64..eeaf8f72 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -390,7 +390,7 @@ class Translator { translateWhile(w) case Assign(lhs, rhs) => def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = { - if (lhs.v.IsImmutable) { + if (lhs.v.isImmutable) { // this must be a "ghost const" val name = lhs.v.UniqueName bassert(! VarExpr("assigned$" + name), lhs.pos, "Const variable can be assigned to only once.") :: @@ -751,7 +751,7 @@ class Translator { val bv = Variable2BVarWhere(v) Comment("local " + v) :: BLocal(bv) :: - { if (v.IsImmutable) { + { if (v.isImmutable) { val isAssignedVar = new Boogie.BVar("assigned$" + bv.id, BoolClass) // havoc x; var assigned$x: bool; assigned$x := false; Havoc(new Boogie.VarExpr(bv)) :: @@ -955,7 +955,7 @@ class Translator { (new VariableExpr(sv) := new VariableExpr(v))) ::: // havoc local-variable loop targets (w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match { - case v: Variable if v.IsImmutable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id)) + case v: Variable if v.isImmutable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id)) case _ => Boogie.Havoc(Boogie.VarExpr(v.UniqueName)) }) :: vars) ::: Boogie.If(null, // 1. CHECK DEFINEDNESS OF INVARIANT @@ -2381,29 +2381,23 @@ object TranslationHelper { def SubstVars(expr: Expression, vs:List[Variable], es:List[Expression]): Expression = SubstVars(expr, None, Map() ++ (vs zip es)); def SubstVars(expr: Expression, t: Option[Expression], vs: Map[Variable, Expression]): Expression = expr.transform { - _ match { - case _: ThisExpr if t.isDefined => t - case e: VariableExpr => - if (vs.contains(e.v)) Some(vs(e.v)) else None; - case q: Quantification => - q.variables foreach { (v) => if (vs.contains(v)) throw new Exception("cannot substitute a variable bound in the quantifier")} - None; - case _ => None; - } + case _: ThisExpr if t.isDefined => t + case e: VariableExpr => + if (vs.contains(e.v)) Some(vs(e.v)) else None; + case q: Quantification => + q.variables foreach { (v) => if (vs.contains(v)) throw new Exception("cannot substitute a variable bound in the quantifier")} + None; + case _ => None; } def SubstThis(expr: Expression, x: Expression): Expression = expr.transform { - _ match { - case _: ThisExpr => Some(x) - case _ => None - } + case _: ThisExpr => Some(x) + case _ => None } def SubstResult(expr: Expression, x: Expression): Expression = expr.transform { - _ match { - case _: Result => Some(x) - case _ => None - } + case _: Result => Some(x) + case _ => None } // De-sugar expression (idempotent) -- cgit v1.2.3