diff options
| -rw-r--r-- | Chalice/src/Ast.scala | 96 | ||||
| -rw-r--r-- | Chalice/src/Graph.scala | 21 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 52 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 6 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 143 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 34 |
6 files changed, 234 insertions, 118 deletions
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
@@ -170,6 +170,23 @@ 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)
|