diff options
| -rw-r--r-- | Chalice/src/Ast.scala | 14 | ||||
| -rw-r--r-- | Chalice/src/Chalice.scala | 2 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 10 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 37 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 32 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 209 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 12 | ||||
| -rw-r--r-- | Chalice/test.bat | 12 |
8 files changed, 215 insertions, 113 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 44d97290..47bd7de9 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -10,7 +10,9 @@ trait ASTNode extends Positional // classes and types
-sealed case class Class(id: String, parameters: List[Class], module: String, members: List[Member]) extends ASTNode {
+case class TopLevelDecl(id: String) extends ASTNode
+
+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)})
@@ -43,6 +45,8 @@ sealed case class Class(id: String, parameters: List[Class], module: String, mem def FullName: String = if(parameters.isEmpty) id else id + "<" + parameters.tail.foldLeft(parameters.head.FullName){(a, b) => a + ", " + b.FullName} + ">"
}
+sealed case class Channel(channelId: String, parameters: List[Variable], where: Expression) extends TopLevelDecl(channelId)
+
case class SeqClass(parameter: Class) extends Class("seq", List(parameter), "default", Nil) {
override def IsRef = false;
override def IsSeq = true;
@@ -128,6 +132,7 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci result
}
}
+case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)
class Variable(name: String, typ: Type) extends ASTNode {
val id = name
val t = typ
@@ -198,7 +203,12 @@ case class CallAsync(declaresLocal: boolean, lhs: VariableExpr, obj: Expression, case class JoinAsync(lhs: List[VariableExpr], token: Expression) extends Statement {
var m: Method = null
}
-
+case class Wait(obj: Expression, id: String) extends Statement {
+ var c: Condition = null
+}
+case class Signal(obj: Expression, id: String, all: boolean) extends Statement {
+ var c: Condition = null
+}
case class Fold(pred: PermissionExpr) extends Statement
case class Unfold(pred: PermissionExpr) extends Statement
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 439805d4..11481741 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -10,7 +10,7 @@ import java.io.FileWriter object Chalice {
def main(args: Array[String]): unit = {
- var boogiePath = "C:\\Boogie\\2\\Binaries\\Boogie.exe"
+ var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
// parse command-line arguments
var inputName: String = null
var printProgram = false
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index 75135e38..234d4e52 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -5,9 +5,15 @@ //-----------------------------------------------------------------------------
class ChaliceToCSharp {
- def convertProgram(classes: List[Class]): String = {
+ def convertProgram(decls: List[TopLevelDecl]): String = {
"using Chalice;" + nl + nl +
- rep(classes map convertClass)
+ rep(decls map convertTopLevelDecl)
+ }
+
+ def convertTopLevelDecl(decl: TopLevelDecl): String = {
+ decl match {
+ case cl: Class => convertClass(cl)
+ }
}
def convertClass(cl: Class): String = if (cl.IsExternal) "" else {
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 5063cc92..ec085f3c 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -12,21 +12,25 @@ import scala.util.parsing.input.NoPosition class Parser extends StandardTokenParsers {
- def parseFile(path: String): this.ParseResult[List[Class]] = {
+ def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = {
val tokens = new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));
phrase(programUnit)(tokens)
}
case class PositionedString(v: String) extends Positional
- lexical.reserved += ("class", "ghost", "var", "const", "method", "assert", "assume", "new", "this", "reorder",
+ lexical.reserved += ("class", "ghost", "var", "const", "method", "channel", "condition",
+ "assert", "assume", "new", "this", "reorder",
"between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
"lock", "fork", "join", "rd", "acc", "holds", "old", "assigned",
"call", "if", "else", "while", "invariant", "lockchange",
- "returns", "requires", "ensures", "int", "bool", "false", "true", "null", "maxlock", "lockbottom",
+ "returns", "requires", "ensures", "where",
+ "int", "bool", "false", "true", "null", "maxlock", "lockbottom",
"module", "external",
- "predicate", "function", "free", "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
- "seq", "nil", "result", "eval", "token")
+ "predicate", "function", "free", "send", "receive",
+ "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
+ "seq", "nil", "result", "eval", "token",
+ "wait", "signal")
// todo: can we remove "nil"?
lexical.delimiters += ("(", ")", "{", "}",
"<==>", "==>", "&&", "||",
@@ -34,7 +38,7 @@ class Parser extends StandardTokenParsers { "+", "-", "*", "/", "%", "!", ".", "..",
";", ":", ":=", ",", "?", "|", "@", "[", "]", "++")
- def programUnit = classDecl*
+ def programUnit = (classDecl | channelDecl)*
// class and members
@@ -45,7 +49,8 @@ class Parser extends StandardTokenParsers { ext match { case None => case Some(t) => cl.IsExternal = true }
cl
})
- def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | predicateDecl | functionDecl)
+ def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl |
+ predicateDecl | functionDecl)
def fieldDecl =
( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id,t) }
@@ -75,6 +80,11 @@ class Parser extends StandardTokenParsers { outs match {
case None => Method(id, ins, Nil, spec, body)
case Some(outs) => Method(id, ins, outs, spec, body) }}
+ def channelDecl =
+ "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
+ case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
+ case id ~ ins ~ Some(e) => Channel(id, ins, e)
+ }
def predicateDecl: Parser[Predicate] =
("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
def functionDecl =
@@ -103,6 +113,10 @@ class Parser extends StandardTokenParsers { case x => currentLocalVariables = prev; x }
}
+ def conditionDecl =
+ "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
+ case id ~ optE => Condition(id, optE) }
+
// statements
def statement =
@@ -179,6 +193,11 @@ class Parser extends StandardTokenParsers { }, t => "fork statement cannot take more than 1 left-hand side")
| (("join") ~> ( identList <~ ":=" ?)) ~ expression <~ Semi ^^
{ case results ~ token => JoinAsync(ExtractList(results), token) }
+ | "wait" ~> memberAccess <~ Semi ^^ {
+ case MemberAccess(obj, id) => Wait(obj, id) }
+ | "signal" ~> ("forall" ?) ~ memberAccess <~ Semi ^^ {
+ case None ~ MemberAccess(obj, id) => Signal(obj, id, false)
+ case _ ~ MemberAccess(obj, id) => Signal(obj, id, true) }
)
def localVarStmt(const: boolean, ghost: boolean) =
idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
@@ -227,6 +246,10 @@ class Parser extends StandardTokenParsers { ( ident <~ "(" ^^ VariableExpr
| selectExprFerSure <~ "("
)
+ def memberAccess = // returns a MemberAccess
+ ( selectExprFerSure
+ | ident ^^ { case id => MemberAccess(ImplicitThisExpr(), id) }
+ )
def ExtractList[T](a: Option[List[T]]): List[T] = a match {
case None => Nil
case Some(list) => list }
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index b93c23bd..32cf0e15 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -4,12 +4,15 @@ //
//-----------------------------------------------------------------------------
object PrintProgram {
- def P(prog: List[Class]) =
- for (cl <- prog) {
- if (cl.IsExternal) print("external ")
- println("class " + cl.id + " module " + cl.module + " {")
- cl.members foreach Member
- println("}")
+ def P(prog: List[TopLevelDecl]) =
+ for (decl <- prog) decl match {
+ case cl: Class =>
+ if (cl.IsExternal) print("external ")
+ println("class " + cl.id + " module " + cl.module + " {")
+ cl.members foreach Member
+ println("}")
+ case ch: Channel =>
+ println("channel " + ch.id + " where " + Expr(ch.where) + Semi)
}
def Semi = ";"
def Member(m: Member) = m match {
@@ -34,8 +37,15 @@ object PrintProgram { print(" "); Stmt(s, 4)
}
println(" }")
+ case Condition(id, optE) =>
+ print(" condition " + id)
+ optE match {
+ case None =>
+ case Some(e) => print(" where " + Expr(e))
+ }
+ println(Semi)
case Predicate(id, definition) =>
- print(" predicate " + id + " { " + Expr(definition) + "}")
+ println(" predicate " + id + " { " + Expr(definition) + "}")
case Function(id, ins, out, specs, e) =>
print(" function " + id + "(" + VarList(ins) + ")" + ": " + out.id);
specs foreach {
@@ -130,6 +140,14 @@ object PrintProgram { Expr(obj); print("."); print(name); print("("); ExprList(args); print(")");
case JoinAsync(lhs, token) =>
print("join async "); ExprList(lhs); print(" := "); Expr(token);
+ case Wait(obj, id) =>
+ print("wait ")
+ MemberSelect(obj, id, 0, false)
+ println(Semi)
+ case Signal(obj, id, all) =>
+ print("signal "); if (all) { print(" forall") }
+ MemberSelect(obj, id, 0, false)
+ println(Semi)
}
def PrintBounds(lower: List[Expression], upper: List[Expression]) = {
if (lower == Nil && upper == Nil) {
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index c7bdfd15..b0b7df68 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -14,8 +14,8 @@ object Resolver { var seqClasses = Map[String, SeqClass]();
- class ProgramContext(classes: Map[String,Class], currentClass: Class) {
- val Classes = classes
+ class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) {
+ val Decls = decls
val CurrentClass = currentClass
var currentMember = null: Member;
def CurrentMember = currentMember: Member;
@@ -29,7 +29,7 @@ object Resolver { def LookupVariable(id: String): Option[Variable] = None
def IsVariablePresent(vr: Variable): boolean = false
- private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Classes, parent.CurrentClass) {
+ private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, parent.CurrentClass) {
override def Error(pos: Position, msg: String) = parent.Error(pos, msg)
override def LookupVariable(id: String): Option[Variable] = {
if (id == v.id) Some(v) else parent.LookupVariable(id)
@@ -43,31 +43,35 @@ object Resolver { }
}
- def Resolve(prog: List[Class]): ResolverOutcome = {
- // register the classes and their members
- var classes = Map[String,Class]()
- for (cl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {
- if (classes contains cl.id) {
- return Error(cl.pos, "duplicate class name: " + cl.id)
+ def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = {
+ // register the channels as well as the classes and their members
+ var decls = Map[String,TopLevelDecl]()
+ for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {
+ if (decls contains decl.id) {
+ return Error(decl.pos, "duplicate class/channel name: " + decl.id)
} else {
- for (m <- cl.members) m match {
- case _:MonitorInvariant =>
- case m: NamedMember =>
- m.Parent = cl
- if (cl.mm contains m.Id) {
- return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)
- } else {
- cl.mm = cl.mm + (m.Id -> m)
+ decl match {
+ case cl: Class =>
+ for (m <- cl.members) m match {
+ case _:MonitorInvariant =>
+ case m: NamedMember =>
+ m.Parent = cl
+ if (cl.mm contains m.Id) {
+ return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)
+ } else {
+ cl.mm = cl.mm + (m.Id -> m)
+ }
}
+ case _ =>
}
- classes = classes + (cl.id -> cl)
+ decls = decls + (decl.id -> decl)
}
}
var errors = List[String]()
- // resolve types of fields and methods
- val contextNoCurrentClass = new ProgramContext(classes, null)
- for (cl <- prog; m <- cl.members) m match {
+ // resolve types of members
+ val contextNoCurrentClass = new ProgramContext(decls, null)
+ for (decl <- prog; if decl.isInstanceOf[Class]; m <- decl.asInstanceOf[Class].members) m match {
case _:MonitorInvariant =>
case Field(id,t) =>
ResolveType(t, contextNoCurrentClass)
@@ -75,7 +79,8 @@ object Resolver { for (v <- ins ++ outs) {
ResolveType(v.t, contextNoCurrentClass)
}
- case Predicate(id, definition) =>
+ case _:Condition =>
+ case _:Predicate =>
case Function(id, ins, out, specs, definition) =>
for (v <- ins) {
ResolveType(v.t, contextNoCurrentClass)
@@ -88,47 +93,53 @@ object Resolver { // * Field types and Method formal-parameter types
// * Assign, FieldUpdate, and Call statements
// * VariableExpr and FieldSelect expressions
- for (cl <- prog) {
- val context = new ProgramContext(classes, cl)
- for (m <- cl.members) {
- context.currentMember = 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) =>
- var ctx = context
- for (v <- ins ++ outs) {
- ctx = ctx.AddVariable(v)
- }
- spec foreach {
- 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")
- ee foreach (e => ResolveExpr(e, ctx, true, false)(false))
- }
- ResolveStmt(BlockStmt(body), ctx)
- case p@Predicate(id, e) =>
- var ctx = context;
- 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, e) =>
- var ctx = context
- for (v <- ins) {
- ctx = ctx.AddVariable(v)
- }
- spec foreach {
- case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
- case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)
- case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function")
- }
- ResolveExpr(e, ctx, 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 + ")")
+ for (decl <- prog) decl match {
+ case _: Channel =>
+ case cl: Class =>
+ val context = new ProgramContext(decls, cl)
+ for (m <- cl.members) {
+ context.currentMember = 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) =>
+ var ctx = context
+ for (v <- ins ++ outs) {
+ ctx = ctx.AddVariable(v)
+ }
+ spec foreach {
+ 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")
+ ee foreach (e => ResolveExpr(e, ctx, true, false)(false))
+ }
+ ResolveStmt(BlockStmt(body), ctx)
+ 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;
+ 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, e) =>
+ var ctx = context
+ for (v <- ins) {
+ ctx = ctx.AddVariable(v)
+ }
+ spec foreach {
+ case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)
+ case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)
+ case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function")
+ }
+ ResolveExpr(e, ctx, 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 + ")")
+ }
}
- }
- errors = errors ++ context.errors
+ errors = errors ++ context.errors
}
if (errors.length == 0) {
@@ -152,8 +163,13 @@ object Resolver { }
return;
}
- if (context.Classes contains t.FullName) {
- t.typ = context.Classes(t.FullName)
+ if (context.Decls contains t.FullName) {
+ context.Decls(t.FullName) match {
+ case cl: Class => t.typ = cl
+ case _ =>
+ context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class")
+ t.typ = IntClass
+ }
} else {
if(seqClasses.contains(t.FullName)) {
t.typ = seqClasses(t.FullName)
@@ -356,7 +372,7 @@ object Resolver { CheckNoGhost(e, context);
if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
case c@CallAsync(declaresLocal, token, obj, id, args) =>
- // resolve receiver
+ // resolve receiver
ResolveExpr(obj, context, false, false)(false)
CheckNoGhost(obj, context)
// resolve arguments
@@ -418,7 +434,31 @@ object Resolver { }
}
- }
+ }
+ 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)
+ }
}
def ComputeLoopTargets(s: Statement): Set[Variable] = s match { // local variables
@@ -453,24 +493,27 @@ object Resolver { def ResolveExpr(e: RValue, context: ProgramContext,
twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match {
case e @ NewRhs(id, initialization) =>
- if (context.Classes contains id) {
- e.typ = context.Classes(id)
- 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 + ".");
+ if (context.Decls contains id) {
+ context.Decls(id) match {
+ case cl: Class =>
+ e.typ = cl
+ 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 + ".");
+ }
+ }
}
- }
}
} else {
context.Error(e.pos, "undefined class " + id + " used in new expression")
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 9ec41448..1e38a8ee 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -29,8 +29,10 @@ class Translator { var modules = Nil: List[String]
var etran = new ExpressionTranslator(null);
- def translateProgram(classes: List[Class]): List[Decl] = {
- classes flatMap { translateClass(_) }
+ def translateProgram(decls: List[TopLevelDecl]): List[Decl] = {
+ decls flatMap {
+ case cl: Class => translateClass(cl)
+ }
}
def translateClass(cl: Class): List[Decl] = {
@@ -152,7 +154,7 @@ class Translator { wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))
*/
val args = VarExpr("this") :: inArgs;
- val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+ val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args);
Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
List(applyF),
@@ -172,7 +174,7 @@ class Translator { val frameFunctionName = "##" + f.FullName;
val args = VarExpr("this") :: inArgs;
- val applyF = f.apply(List(etran.Heap, etran.Mask) ::: args);
+ val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args);
val applyFrameFunction = FunctionApp(frameFunctionName, version :: args);
Boogie.Function("##" + f.FullName, Boogie.BVar("state", theap) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new BVar("$myresult", f.out)) ::
Axiom(new Boogie.Forall(
@@ -193,7 +195,7 @@ class Translator { val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});
val myresult = Boogie.BVar("result", Boogie.ClassType(f.out.typ));
val args = VarExpr("this") :: inArgs;
- val applyF = f.apply(List(Heap, Mask) ::: args)
+ val applyF = FunctionApp(functionName(f), List(Heap, Mask) ::: args)
//postcondition axioms
(Postconditions(f.spec) map { post : Expression =>
Axiom(new Boogie.Forall(
diff --git a/Chalice/test.bat b/Chalice/test.bat index 480a7bf7..66fd9853 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -3,9 +3,13 @@ echo start > Output set CHALICE=call scala -cp bin Chalice -nologo
-for %%f in (AssociationList cell counter dining-philosophers ForkJoin HandOverHand
+REM to do: AssociationList
+REM to do: GhostConst
+REM to do: Leaks -checkLeaks
+
+for %%f in (cell counter dining-philosophers ForkJoin HandOverHand
iterator iterator2 producer-consumer
- prog0 prog1 prog2 prog3 prog4 RockBand swap GhostConst OwickiGries) do (
+ prog0 prog1 prog2 prog3 prog4 RockBand swap OwickiGries) do (
echo Testing %%f.chalice ...
echo ------ Running regression test %%f.chalice >> Output
%CHALICE% %* examples\%%f.chalice >> Output 2>&1
@@ -19,10 +23,6 @@ echo Testing RockBand-automagic.chalice ... echo ------ Running regression test RockBand-automagic.chalice >> Output
%CHALICE% %* -defaults -autoMagic -checkLeaks -autoFold examples\RockBand-automagic.chalice >> Output 2>&1
-echo Testing Leaks.chalice ...
-echo ------ Running regression test Leaks.chalice >> Output
-%CHALICE% %* -checkLeaks examples\Leaks.chalice >> Output 2>&1
-
fc examples\Answer Output > nul
if not errorlevel 1 goto passTest
|