diff options
| -rw-r--r-- | Chalice/examples/Answer | 17 | ||||
| -rw-r--r-- | Chalice/examples/ProdConsChannel.chalice | 126 | ||||
| -rw-r--r-- | Chalice/src/Ast.scala | 16 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 2 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 225 | ||||
| -rw-r--r-- | Chalice/src/Prelude.scala | 11 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 16 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 171 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 357 | ||||
| -rw-r--r-- | Chalice/test.bat | 3 | ||||
| -rw-r--r-- | Util/Emacs/chalice-mode.el | 7 |
11 files changed, 685 insertions, 266 deletions
diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer index b81e3893..e40b7287 100644 --- a/Chalice/examples/Answer +++ b/Chalice/examples/Answer @@ -96,12 +96,12 @@ The program did not typecheck. 15.6: undeclared member a in class C
15.10: undeclared member b in class C
15.5: undeclared member y in class int
-15.18: undefined class T used in new expression
+15.18: undefined class or channel T used in new expression
16.19: undeclared member O in class C
16.14: == requires operands of the same type, found int and bool
16.31: undeclared member O in class C
16.13: != requires operands of the same type, found bool and int
-16.13: object in install statement must be of a reference type (found bool)
+16.13: object in reorder statement must be of a reference type (found bool)
16.41: undeclared member a in class C
16.41: install bound must be of a reference type or Mu type (found int)
16.43: undeclared member b in class C
@@ -114,11 +114,11 @@ The program did not typecheck. 17.19: undeclared member Y in class C
17.13: incorrect type of ==> LHS (expected bool, found int)
17.19: incorrect type of ==> RHS (expected bool, found int)
-17.13: object in install statement must be of a reference type (found bool)
+17.13: object in reorder statement must be of a reference type (found bool)
17.27: install bound must be of a reference type or Mu type (found int)
18.13: undeclared member o in class C
18.13: undeclared member f in class int
-18.13: object in install statement must be of a reference type (found int)
+18.13: object in reorder statement must be of a reference type (found int)
19.11: undeclared member o in class C
19.11: object in share statement must be of a reference type (found int)
20.13: undeclared member o in class C
@@ -159,7 +159,7 @@ The program did not typecheck. 34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
35.13: undeclared member o in class C
-35.13: object in install statement must be of a reference type (found int)
+35.13: object in reorder statement must be of a reference type (found int)
58.17: undeclared member sqrt2 in class C
58.25: undeclared member sqrt2 in class C
62.17: undeclared member s in class C
@@ -216,6 +216,13 @@ The program did not typecheck. ------ Running regression test OwickiGries.chalice
Boogie program verifier finished with 5 verified, 0 errors
+------ Running regression test ProdConsChannel.chalice
+ 47.3: Method body is not allowed to leave any debt.
+ 61.3: Method body is not allowed to leave any debt.
+ 85.20: Location might not be readable.
+ 123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
+
+Boogie program verifier finished with 19 verified, 4 errors
------ Running regression test cell-defaults.chalice
96.5: The heap of the callee might not be strictly smaller than the heap of the caller.
102.5: The heap of the callee might not be strictly smaller than the heap of the caller.
diff --git a/Chalice/examples/ProdConsChannel.chalice b/Chalice/examples/ProdConsChannel.chalice new file mode 100644 index 00000000..e8ab1a60 --- /dev/null +++ b/Chalice/examples/ProdConsChannel.chalice @@ -0,0 +1,126 @@ +class Cell {
+ var val: int
+}
+
+channel Ch(c: Cell) where
+ c != null ==> acc(c.val) && 0 <= c.val && credit(this)
+
+class Program {
+ method Main() {
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ join tk0
+ join tk1
+ }
+ method Producer(ch: Ch)
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1
+ }
+ send ch(null)
+ }
+ method Consumer(ch: Ch)
+ requires rd(ch.mu) && maxlock << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ while (c != null)
+ invariant rd(ch.mu) && maxlock << ch.mu
+ invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
+ {
+ var i := c.val
+ receive c := ch
+ }
+ }
+
+ // variations
+ method Main0() { // error: debt remains after body
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ // join tk0
+ join tk1
+ }
+ method Main1() {
+ var ch := new Ch
+ fork tk0 := Producer(ch)
+ fork tk1 := Consumer(ch)
+ join tk0
+ // join tk1
+ } // no problem
+ method Producer0(ch: Ch) // error: debt remains after body
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1
+ }
+ // send ch(null)
+ }
+ method Producer1(ch: Ch)
+ requires ch != null
+ ensures credit(ch)
+ {
+ var i := 0
+ while (i < 25)
+ {
+ var x := i*i
+ var c := new Cell { val := x }
+ send ch(c)
+ i := i + 1 + c.val // error: can no longer read c.val
+ }
+ send ch(null)
+ }
+ method Consumer0(ch: Ch)
+ requires rd(ch.mu) && maxlock << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ while (c != null && c.val == 7) // this consumer may end early, but that's allowed
+ invariant rd(ch.mu) && maxlock << ch.mu
+ invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
+ {
+ var i := c.val
+ receive c := ch
+ }
+ }
+ method Consumer1(ch: Ch)
+ requires rd(ch.mu) && maxlock << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert 0 <= c.val // follows from where clause
+ }
+ }
+ method Consumer2(ch: Ch)
+ requires rd(ch.mu) && maxlock << ch.mu
+ requires credit(ch)
+ ensures rd(ch.mu)
+ {
+ var c: Cell
+ receive c := ch
+ if (c != null) {
+ assert c.val < 2 // error: does not follow from where clause
+ }
+ }
+}
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 47bd7de9..7ad95899 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -30,6 +30,7 @@ sealed case class Class(classId: String, parameters: List[Class], module: String def IsMu: boolean = false
def IsSeq: boolean = false
def IsToken: boolean = false
+ 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)
@@ -82,6 +83,11 @@ case class TokenClass(c: Type, m: String) extends Class("token", Nil, "default", override def FullName: String = "token<" + c.FullName + "." + m + ">"
mm = mm.+(("joinable", Fields(0)));
}
+case class ChannelClass(ch: Channel) extends Class(ch.id, Nil, "default", Nil) {
+ override def IsRef = true;
+ override def IsChannel = true;
+ override def IsNormalClass = false;
+}
object RootClass extends Class("$root", Nil, "default", List(
new SpecialField("mu", new Type(MuClass)),
@@ -209,6 +215,10 @@ case class Wait(obj: Expression, id: String) extends Statement { case class Signal(obj: Expression, id: String, all: boolean) extends Statement {
var c: Condition = null
}
+case class Send(ch: Expression, args: List[Expression]) extends Statement {
+}
+case class Receive(ch: Expression, outs: List[VariableExpr]) extends Statement {
+}
case class Fold(pred: PermissionExpr) extends Statement
case class Unfold(pred: PermissionExpr) extends Statement
@@ -217,7 +227,7 @@ case class Unfold(pred: PermissionExpr) extends Statement sealed abstract class RValue extends ASTNode {
var typ: Class = null
}
-case class NewRhs(id: String, initialization: List[Init]) extends RValue
+case class NewRhs(id: String, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression]) extends RValue
case class Init(id: String, e: Expression) extends ASTNode {
var f: Field = null;
}
@@ -262,6 +272,10 @@ case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends P case class AccessAll(obj: Expression, perm: Option[Expression]) extends Expression
case class RdAccessAll(obj: Expression, perm: Option[Option[Expression]]) extends Expression
+case class Credit(e: Expression, n: Option[Expression]) extends Expression {
+ def N = n match { case None => IntLiteral(1) case Some(n) => n }
+}
+
case class Holds(e: Expression) extends Expression
case class RdHolds(e: Expression) extends Expression
case class Assigned(id: String) extends Expression {
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index 234d4e52..feef3195 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -131,7 +131,7 @@ class ChaliceToCSharp { case th: ThisExpr => "this"
case VariableExpr(id) => id
case MemberAccess(target, f) => convertExpression(target) + "." + f
- case newrhs@NewRhs(c, initialization) =>
+ case newrhs@NewRhs(c, initialization, lower, upper) =>
if(initialization.length == 0) { "new " + c + "()" } else {
val init = repsep(newrhs.typ.Fields map { f => (initialization.find { i => i.f == f}) match {
case None => defaultValue(f.typ)
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index ec085f3c..4667f0e7 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -22,7 +22,7 @@ class Parser extends StandardTokenParsers { 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",
+ "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned",
"call", "if", "else", "while", "invariant", "lockchange",
"returns", "requires", "ensures", "where",
"int", "bool", "false", "true", "null", "maxlock", "lockbottom",
@@ -70,6 +70,8 @@ class Parser extends StandardTokenParsers { )
def Semi = ";" ?
+ var currentLocalVariables = Set[String]()
+
def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
def methodDecl =
@@ -178,17 +180,17 @@ class Parser extends StandardTokenParsers { case VariableExpr(id) => (new ImplicitThisExpr, id)
case MemberAccess(obj, id) => (obj, id)
}
- CallAsync(false, null, receiver, name, ExtractList(args))
+ CallAsync(false, null, receiver, name, args)
case Some(List(tok)) ~ target ~ args =>
val (receiver, name) = target match {
case VariableExpr(id) => (new ImplicitThisExpr, id)
case MemberAccess(obj, id) => (obj, id)
}
if (currentLocalVariables contains tok.id) {
- CallAsync(false, tok, receiver, name, ExtractList(args))
+ CallAsync(false, tok, receiver, name, args)
} else {
currentLocalVariables = currentLocalVariables + tok.id;
- CallAsync(true, tok, receiver, name, ExtractList(args))
+ CallAsync(true, tok, receiver, name, args)
}
}, t => "fork statement cannot take more than 1 left-hand side")
| (("join") ~> ( identList <~ ":=" ?)) ~ expression <~ Semi ^^
@@ -198,6 +200,14 @@ class Parser extends StandardTokenParsers { | "signal" ~> ("forall" ?) ~ memberAccess <~ Semi ^^ {
case None ~ MemberAccess(obj, id) => Signal(obj, id, false)
case _ ~ MemberAccess(obj, id) => Signal(obj, id, true) }
+ | ("send" ~> suffixPlusExpr into { e => e match {
+ case FunctionApplication(obj, name, args) => Semi ^^^ Send(MemberAccess(obj,name), args)
+ case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})
+ | ("send" ~> atom into { e => e match {
+ case FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ Send(VariableExpr(name), args)
+ case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})
+ | "receive" ~> (identList <~ ":=" ?) ~ expression <~ Semi ^^ {
+ case outs ~ e => Receive(e, ExtractList(outs)) }
)
def localVarStmt(const: boolean, ghost: boolean) =
idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
@@ -209,7 +219,7 @@ class Parser extends StandardTokenParsers { case None =>
// do a cheap (and hokey) type inference of the RHS
rhs match {
- case Some(NewRhs(tid, _)) => Type(tid, Nil)
+ case Some(NewRhs(tid, _, _, _)) => Type(tid, Nil)
case Some(BoolLiteral(b)) => Type("bool", Nil)
case _ => Type("int", Nil)
}
@@ -237,11 +247,11 @@ class Parser extends StandardTokenParsers { )
def callStmt =
callSignature ^? ({
- case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, ExtractList(args))
- case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, ExtractList(args))
+ case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, args)
+ case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, args)
}, t => "bad call statement")
def callSignature =
- (identList <~ ":=" ?) ~ callTarget ~ (expressionList?) <~ ")" <~ Semi
+ (identList <~ ":=" ?) ~ callTarget ~ expressionList <~ ")" <~ Semi
def callTarget = // returns a VariableExpr or a FieldSelect
( ident <~ "(" ^^ VariableExpr
| selectExprFerSure <~ "("
@@ -257,21 +267,31 @@ class Parser extends StandardTokenParsers { ( Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) ~
(("," ~> Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) *) ^^ { case e ~ ee => e::ee }
def Rhs : Parser[RValue] =
- positioned( "new" ~> ident ~ opt("{" ~> repsep(FieldInit, ",") <~ "}") ^^ { case id ~ None => NewRhs(id, Nil)
- case id ~ Some(inits) => NewRhs(id, inits)
- }
+ positioned(
+ "new" ~> ident ~ opt("{" ~> repsep(FieldInit, ",") <~ "}") ~ opt(installBounds) ^^ {
+ case id ~ None ~ None => NewRhs(id, Nil, Nil, Nil)
+ case id ~ Some(inits) ~ None => NewRhs(id, inits, Nil, Nil)
+ case id ~ None ~ Some(bounds) => NewRhs(id, Nil, bounds._1, bounds._2)
+ case id ~ Some(inits) ~ Some(bounds) => NewRhs(id, inits, bounds._1, bounds._2)
+ }
| expression
)
def FieldInit: Parser[Init] =
positioned( (ident <~ ":=") ~ expression ^^ { case id ~ e => Init(id, e) } )
def installBounds: Parser[(List[Expression], List[Expression])] =
( "between" ~> expressionList ~ "and" ~ expressionList ^^ { case l ~ _ ~ u => (l,u) }
- | "below" ~> expressionList ^^ { (Nil,_) }
- | "above" ~> expressionList ^^ { (_,Nil) }
+ | "below" ~> expressionList ~ ("above" ~> expressionList ?) ^^ {
+ case u ~ None => (Nil,u)
+ case u ~ Some(l) => (l,u) }
+ | "above" ~> expressionList ~ ("below" ~> expressionList ?) ^^ {
+ case l ~ None => (l,Nil)
+ case l ~ Some(u) => (l,u) }
)
// expressions
+ def expressionList =
+ repsep(expression, ",")
def expression = positioned(iteExpr)
def iteExpr: Parser[Expression] =
@@ -293,7 +313,7 @@ class Parser extends StandardTokenParsers { case (a, "&&" ~ b) => And(a,b)
case (a, "||" ~ b) => Or(a,b) }})
def cmpExpr =
- positioned(seqExpr ~ ((CompareOp ~ seqExpr)?) ^^ {
+ positioned(concatExpr ~ ((CompareOp ~ concatExpr)?) ^^ {
case e ~ None => e
case e0 ~ Some("==" ~ e1) => Eq(e0,e1)
case e0 ~ Some("!=" ~ e1) => Neq(e0,e1)
@@ -304,16 +324,10 @@ class Parser extends StandardTokenParsers { case e0 ~ Some("<<" ~ e1) => LockBelow(e0,e1)
})
def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<"
- def seqExpr =
- positioned(addExpr ~ (seqAccess *) ^^ { case e ~ as => as.foldLeft(e: Expression)({ (t, a) => val result = a(t); result.pos = t.pos; result }) })
-
- def seqAccess : Parser[(Expression => SeqAccess)] =
- ( ("[" ~> expression) <~ "]" ^^ { case e1 => { e0: Expression => At(e0, e1) }}
- | "[" ~> expression <~ (".." ~ "]") ^^ { case e1 => { e0: Expression => Drop(e0, e1)}}
- | ("[" ~ "..") ~> expression <~ "]" ^^ { case e1 => { e0: Expression => Take(e0, e1)}}
- | "++" ~> expression ^^ { case e1 => { e0: Expression => Append(e0, e1) }}
- | ("[" ~> expression <~ "..") ~ (expression <~ "]") ^^ { case e1 ~ e2 => {e0: Expression => val tak = Take(e0, e2); tak.pos = e0.pos; Drop(tak, e1)} })
-
+ def concatExpr =
+ positioned(addExpr ~ ("++" ~> addExpr *) ^^ {
+ case e0 ~ rest => (rest foldLeft e0) {
+ case (a, b) => Append(a, b) }})
def addExpr =
positioned(multExpr ~ (AddOp ~ multExpr *) ^^ {
case e0 ~ rest => (rest foldLeft e0) {
@@ -330,22 +344,41 @@ class Parser extends StandardTokenParsers { def unaryExpr: Parser[Expression] =
( "!" ~> unaryExpr ^^ Not
| "-" ~> unaryExpr ^^ { Minus(IntLiteral(0),_) }
- | functionApplication
- | selectExpr
+ | suffixExpr
)
- def selectExpr: Parser[Expression] =
- atom ~ ("." ~> identOrSpecial *) ^^ {
- case e ~ fields => (fields foldLeft e) { case (e, f) => val result = MemberAccess(e, f); result.pos = e.pos; result }
- }
+ def suffixExpr =
+ atom ~ (suffixThing *) ^^ {
+ case e ~ sfxs => sfxs.foldLeft(e) { (t, a) => val result = a(t); result.pos = t.pos; result } }
+ def suffixPlusExpr =
+ atom ~ (suffixThing +) ^^ {
+ case e ~ sfxs => sfxs.foldLeft(e) { (t, a) => val result = a(t); result.pos = t.pos; result } }
+ def suffixThing: Parser[(Expression => Expression)] =
+ ( "[" ~> expression <~ "]" ^^ { case e1 => { e0: Expression => At(e0, e1) }}
+ | "[" ~> expression <~ (".." ~ "]") ^^ { case e1 => { e0: Expression => Drop(e0, e1)}}
+ | "[" ~> ".." ~> expression <~ "]" ^^ { case e1 => { e0: Expression => Take(e0, e1)}}
+ | "[" ~> (expression <~ "..") ~ expression <~ "]" ^^ {
+ case e1 ~ e2 => {e0: Expression => val tak = Take(e0, e2); tak.pos = e0.pos; Drop(tak, e1)} }
+ | "." ~> ident ~ opt("(" ~> expressionList <~ ")") ^^ {
+ case name ~ None => { e0: Expression => MemberAccess(e0, name) }
+ case name ~ Some(es) => { e0: Expression => FunctionApplication(e0, name, es) } }
+ | "." ~> "acquire" ~> exprBody ^^ { case eb => { e0: Expression => Eval(AcquireState(e0), eb) }}
+ | "." ~> "release" ~> exprBody ^^ { case eb => { e0: Expression => Eval(ReleaseState(e0), eb) }}
+ | "." ~> "fork" ~> (callTarget ~ expressionList <~ ")") ~ exprBody ^^ {
+ case MemberAccess(obj,id) ~ args ~ eb => { e0: Expression => Eval(CallState(e0, obj, id, args), eb) }}
+ )
+ def exprBody =
+ "{" ~> expression <~ "}"
+
def selectExprFerSure: Parser[MemberAccess] =
+ positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ {
+ case e ~ _ ~ field ~ moreFields =>
+ (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>
+ val result = MemberAccess(target, f); result.pos = target.pos; result }})
+ def selectExprFerSureX: Parser[MemberAccess] =
positioned(atom ~ "." ~ identOrSpecial ~ ("." ~> ident *) ^^ {
- case e ~ _ ~ field ~ moreFields => (moreFields foldLeft MemberAccess(e,field)) { (target, f) => val result = MemberAccess(target, f); result.pos = target.pos; result }})
- def functionApplication: Parser[Expression] =
- atom ~ rep("." ~> identOrSpecial ~ opt("(" ~> repsep(expression, ",") <~ ")")) ^^ {
- case target ~ members =>
- members.foldLeft(target)({ case (e, name ~ args) => val result = if(! args.isDefined) MemberAccess(e, name) else FunctionApplication(e, name, args.get); result.pos = e.pos; result })
- }
-
+ case e ~ _ ~ field ~ moreFields =>
+ (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>
+ val result = MemberAccess(target, f); result.pos = target.pos; result }})
def identOrSpecial: Parser[String] =
( ident ^^ { case s => s }
| "acquire" ^^^ "acquire"
@@ -353,60 +386,62 @@ class Parser extends StandardTokenParsers { | "fork" ^^^ "fork"
| "*" ^^^ "*")
- var currentLocalVariables = Set[String]()
-
- def expressionList =
- expression ~ ("," ~> expression *) ^^ { case e ~ ee => e::ee }
-
def atom : Parser[Expression] =
- positioned( numericLit ^^ { case n => IntLiteral(n.toInt) }
- | "false" ^^^ BoolLiteral(false)
- | "true" ^^^ BoolLiteral(true)
- | "null" ^^^ NullLiteral()
- | "maxlock" ^^^ MaxLockLiteral()
- | "lockbottom" ^^^ LockBottomLiteral()
- | "this" ^^^ ExplicitThisExpr()
- | ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
- | "(" ~> expression <~ ")"
- | ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
- | ("ite(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ { case con ~ then ~ els => IfThenElse (con, then, els) }
- | "rd" ~>
- ( "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
- | "(" ~>
- ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
- | selectExprFerSure ~ rdPermArg <~ ")"
- ) ^^ { case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p) case e ~ p => RdAccess(e,p) }
- )
- | "acc" ~> "(" ~>
- ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ ("," ~> expression ?) <~ ")"
- | selectExprFerSure ~ ("," ~> expression ?) <~ ")"
- ) ^^ { case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm) case e ~ perm => Access(e, perm) }
- | "holds" ~> "(" ~> expression <~ ")" ^^ Holds
- | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
- | "old" ~> "(" ~> expression <~ ")" ^^ Old
- | positioned(Ident) ~ opt("(" ~> repsep(expression, ",") <~ ")") ^^
- { case id ~ args => val result =
- if(args.isDefined){
- val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos;
- FunctionApplication(implicitThis, id.v, args.get)
- } else {
- if (currentLocalVariables contains id.v)
- VariableExpr(id.v)
- else {
- val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos; MemberAccess(implicitThis, id.v)
- }
- }; result.pos = id.pos; result }
- | ("unfolding" ~> expression <~ "in") ~ expression ^? {
- case (pred: MemberAccess) ~ e => val acc = Access(pred, None); acc.pos = pred.pos; Unfolding(acc, e)
- case (perm: PermissionExpr) ~ e => Unfolding(perm, e)
+ positioned(
+ numericLit ^^ { case n => IntLiteral(n.toInt) }
+ | "false" ^^^ BoolLiteral(false)
+ | "true" ^^^ BoolLiteral(true)
+ | "null" ^^^ NullLiteral()
+ | "maxlock" ^^^ MaxLockLiteral()
+ | "lockbottom" ^^^ LockBottomLiteral()
+ | "this" ^^^ ExplicitThisExpr()
+ | "result" ^^^ Result()
+ | positioned(Ident) ~ opt("(" ~> expressionList <~ ")") ^^ {
+ case id ~ None =>
+ val r =
+ if (currentLocalVariables contains id.v) {
+ VariableExpr(id.v)
+ } else {
+ val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos
+ MemberAccess(implicitThis, id.v)
+ }
+ r.pos = id.pos; r
+ case id ~ Some(args) =>
+ val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos
+ val r = FunctionApplication(implicitThis, id.v, args)
+ r.pos = id.pos; r
}
- | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
- | ("[" ~> repsep(expression, ",") <~ "]") ^^ { case es => ExplicitSeq(es) }
- | "|" ~> expression <~ "|" ^^ Length
- | forall
- | "result" ^^^ Result()
+ | "rd" ~>
+ ( "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
+ | "(" ~>
+ ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
+ | selectExprFerSureX ~ rdPermArg <~ ")"
+ ) ^^ { case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p) case e ~ p => RdAccess(e,p) }
)
- def forall: Parser[Forall] =
+ | "acc" ~> "(" ~>
+ ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ ("," ~> expression ?) <~ ")"
+ | selectExprFerSureX ~ ("," ~> expression ?) <~ ")"
+ ) ^^ { case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm) case e ~ perm => Access(e, perm) }
+ | "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ {
+ case ch ~ n => Credit(ch, n) }
+ | "holds" ~> "(" ~> expression <~ ")" ^^ Holds
+ | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
+ | "old" ~> "(" ~> expression <~ ")" ^^ Old
+ | ("unfolding" ~> expression <~ "in") ~ expression ^? {
+ case (pred: MemberAccess) ~ e => val acc = Access(pred, None); acc.pos = pred.pos; Unfolding(acc, e)
+ case (perm: PermissionExpr) ~ e => Unfolding(perm, e)
+ }
+ | "|" ~> expression <~ "|" ^^ Length
+ | ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
+ | ("ite(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
+ case con ~ then ~ els => IfThenElse (con, then, els) }
+ | "(" ~> expression <~ ")"
+ | forall
+ | ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
+ | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
+ | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }
+ )
+ def forall: Parser[Forall] =
(("forall" ~ "{") ~> repsep(ident, ",") <~ "in") into { is => (expression <~ ";") ~ (exprWithLocals(is) <~ "}") ^^
{ case seq ~ e => val result = Forall(is, seq, e); currentLocalVariables = currentLocalVariables -- is; result } }
def exprWithLocals(i: List[String]) : Parser[Expression] = {
@@ -416,13 +451,13 @@ class Parser extends StandardTokenParsers { result
}
- def evalstate: Parser[EvalState] = {
- functionApplication ~ opt(callTarget ~ (repsep(expression, ",") <~ ")")) ^?
- { case MemberAccess(e, "acquire") ~ None => AcquireState(e)
- case MemberAccess(e, "release") ~ None => ReleaseState(e)
- case MemberAccess(e, "fork") ~ Some((MemberAccess(obj, id) ~ args)) => CallState(e, obj, id, args)
- }
- }
+ def evalstate: Parser[EvalState] =
+ (suffixExpr <~ ".") into { e =>
+ ( "acquire" ^^^ AcquireState(e)
+ | "release" ^^^ ReleaseState(e)
+ | "fork" ~> callTarget ~ expressionList <~ ")" ^^ {
+ case MemberAccess(obj,id) ~ args => CallState(e, obj, id, args) }
+ )}
def rdPermArg : Parser[Option[Option[Expression]]] =
(("," ~> ( "*" ^^^ None
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala index 876a5abe..44080daa 100644 --- a/Chalice/src/Prelude.scala +++ b/Chalice/src/Prelude.scala @@ -10,6 +10,7 @@ object TranslatorPrelude { type Field a;
type HeapType = <a>[ref,Field a]a;
type MaskType = <a>[ref,Field a][PermissionComponent]int;
+type CreditsType = [ref]int;
type ref;
const null: ref;
@@ -48,6 +49,8 @@ function {:expand true} IsGoodMask(m: MaskType) returns (bool) (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
}
+var Credits: CreditsType;
+
function IsGoodState<T>(T) returns (bool);
function combine<T,U>(T, U) returns (T);
const nostate: HeapType;
@@ -77,10 +80,12 @@ axiom (forall m, n: Mu :: MuBelow(m, n) ==> n != $LockBottom); const unique held: Field int;
function Acquire$Heap(int) returns (HeapType);
function Acquire$Mask(int) returns (MaskType);
+function Acquire$Credits(int) returns (CreditsType);
axiom NonPredicateField(held);
function LastSeen$Heap(Mu, int) returns (HeapType);
function LastSeen$Mask(Mu, int) returns (MaskType);
+function LastSeen$Credits(Mu, int) returns (CreditsType);
const unique rdheld: Field bool;
axiom NonPredicateField(rdheld);
@@ -230,12 +235,18 @@ const unique token#t: TypeName; function Call$Heap(int) returns (HeapType);
function Call$Mask(int) returns (MaskType);
+function Call$Credits(int) returns (CreditsType);
function Call$Args(int) returns (ArgSeq);
type ArgSeq = <T>[int]T;
function EmptyMask(m: MaskType) returns (bool);
axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
+const ZeroCredits: CreditsType;
+axiom (forall o: ref :: ZeroCredits[o] == 0);
+function EmptyCredits(c: CreditsType) returns (bool);
+axiom (forall c: CreditsType :: {EmptyCredits(c)} EmptyCredits(c) <==> (forall o: ref :: o != null ==> c[o] == 0));
+
function NonPredicateField<T>(f: Field T) returns (bool);
function PredicateField<T>(f: Field T) returns (bool);
axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 32cf0e15..fb94f711 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -148,6 +148,15 @@ object PrintProgram { print("signal "); if (all) { print(" forall") }
MemberSelect(obj, id, 0, false)
println(Semi)
+ case Send(ch, args) =>
+ print("send "); Expr(ch); print("("); ExprList(args); print(")"); println(Semi)
+ case Receive(ch, outs) =>
+ print("receive ")
+ outs match {
+ case Nil =>
+ case x :: xs => Expr(x); xs foreach { x => print(", "); Expr(x) }; print(" := ")
+ }
+ Expr(ch); println(Semi)
}
def PrintBounds(lower: List[Expression], upper: List[Expression]) = {
if (lower == Nil && upper == Nil) {
@@ -177,11 +186,12 @@ object PrintProgram { rest foreach { e => print(", "); Expr(e) }
}
def Rhs(e: RValue) = e match {
- case NewRhs(id, initialization) =>
+ case NewRhs(id, initialization, lower, upper) =>
print("new " + id);
if(0 < initialization.length) {
print(" {"); print(initialization(0).id); print(":="); Expr(initialization(0).e); initialization.foreach({ init => print(", "); print(init.id); print(":="); Expr(init.e); }); print("}");
}
+ PrintBounds(lower, upper)
case e: Expression => Expr(e)
}
def Expr(e: Expression): Unit = Expr(e, 0, false)
@@ -217,6 +227,10 @@ object PrintProgram { case Some(None) => print(", *)")
case Some(Some(e)) => print(", "); Expr(e); print(")")
}
+ case Credit(e, n) =>
+ print("credit("); Expr(e)
+ n match { case None => case Some(n) => print(", "); Expr(n) }
+ print(")")
case Holds(e) =>
print("holds("); Expr(e); print(")")
case RdHolds(e) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index b0b7df68..15ed531e 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -62,7 +62,7 @@ object Resolver { cl.mm = cl.mm + (m.Id -> m)
}
}
- case _ =>
+ case ch: Channel =>
}
decls = decls + (decl.id -> decl)
}
@@ -71,21 +71,28 @@ object Resolver { // 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)
- case Method(id, ins, outs, spec, body) =>
- for (v <- ins ++ outs) {
- ResolveType(v.t, contextNoCurrentClass)
- }
- case _:Condition =>
- case _:Predicate =>
- case Function(id, ins, out, specs, definition) =>
- for (v <- ins) {
+ for (decl <- prog) decl match {
+ case ch: Channel =>
+ for (v <- ch.parameters) {
ResolveType(v.t, contextNoCurrentClass)
+ }
+ case cl: Class =>
+ for (m <- cl.asInstanceOf[Class].members) m match {
+ case _:MonitorInvariant =>
+ case Field(id,t) =>
+ ResolveType(t, contextNoCurrentClass)
+ case Method(id, ins, outs, spec, body) =>
+ for (v <- ins ++ outs) {
+ ResolveType(v.t, contextNoCurrentClass)
+ }
+ case _:Condition =>
+ case _:Predicate =>
+ case Function(id, ins, out, specs, definition) =>
+ for (v <- ins) {
+ ResolveType(v.t, contextNoCurrentClass)
+ }
+ ResolveType(out, contextNoCurrentClass)
}
- ResolveType(out, contextNoCurrentClass)
}
errors = errors ++ contextNoCurrentClass.errors;
@@ -94,7 +101,12 @@ object Resolver { // * Assign, FieldUpdate, and Call statements
// * VariableExpr and FieldSelect expressions
for (decl <- prog) decl match {
- case _: Channel =>
+ case ch: Channel =>
+ var ctx = new ProgramContext(decls, ChannelClass(ch))
+ for (v <- ch.parameters) {
+ ctx = ctx.AddVariable(v)
+ }
+ ResolveExpr(ch.where, ctx, false, true)(false)
case cl: Class =>
val context = new ProgramContext(decls, cl)
for (m <- cl.members) {
@@ -130,6 +142,7 @@ object Resolver { for (v <- ins) {
ctx = ctx.AddVariable(v)
}
+ // TODO: disallow credit(...) expressions in function specifications
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)
@@ -166,6 +179,7 @@ object Resolver { 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
@@ -311,25 +325,20 @@ object Resolver { }
case Install(obj, lowerBounds, upperBounds) =>
ResolveExpr(obj, context, false, false)(false)
- if (!obj.typ.IsRef) context.Error(obj.pos, "object in install statement must be of a reference type (found " + obj.typ.FullName + ")")
- for (b <- lowerBounds ++ upperBounds) {
- ResolveExpr(b, context, true, false)(false)
- if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "install bound must be of a reference type or Mu type" +
- " (found " + b.typ.FullName + ")")
- }
+ 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 + ")")
- for (b <- lowerBounds ++ upperBounds) {
- ResolveExpr(b, context, true, false)(false)
- if (!b.typ.IsRef && !b.typ.IsMu) context.Error(b.pos, "share bound must be of a reference type or Mu type" +
- " (found " + b.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)
@@ -459,8 +468,64 @@ object Resolver { 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(ch, outs) =>
+ ResolveExpr(ch, context, false, false)(false)
+ CheckNoGhost(ch, context)
+ outs foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
+ // check the outs to be appropriate actually out parameters
+ var vars = Set[Variable]()
+ for (v <- outs) {
+ 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 of receive")
+ if (vars contains v.v) {
+ context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
+ } else {
+ vars = vars + v.v
+ }
+ }
+ }
+ // 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 {
+ for ((actual, formal) <- outs zip channel.parameters) {
+ if (! canAssign(actual.typ, formal.t.typ))
+ context.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ }
+ }
+ case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")
+ }
}
+ 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 ComputeLoopTargets(s: Statement): Set[Variable] = s match { // local variables
case BlockStmt(ss) =>
(ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) }
@@ -492,31 +557,38 @@ object Resolver { // 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) =>
+ 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
- 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 (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 " + id + " used in new expression")
+ context.Error(e.pos, "undefined class or channel " + id + " used in new expression")
e.typ = IntClass
}
case i:IntLiteral =>
@@ -588,6 +660,12 @@ object Resolver { case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)
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")
if(! specContext)
@@ -864,6 +942,9 @@ object Resolver { case RdAccessAll(obj, perm) =>
CheckRunSpecification(obj, context, false)
perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }
+ 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) =>
@@ -930,6 +1011,8 @@ object Resolver { func(obj); perm match { case Some(p) => func(p); case _ => ; }
case RdAccessAll(obj, perm) =>
func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; }
+ case Credit(e, n) =>
+ func(e); n match { case Some(n) => func(n); case _ => }
case Holds(e) => func(e);
case RdHolds(e) => func(e);
case e: Assigned => e
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 1e38a8ee..95f46dc3 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -32,6 +32,8 @@ class Translator { def translateProgram(decls: List[TopLevelDecl]): List[Decl] = {
decls flatMap {
case cl: Class => translateClass(cl)
+ case ch: Channel => translateClass(ChannelClass(ch)) /* TODO: admissibility check of where clause */
+ /* TODO: maxlock not allowed in postcondition of things forked (or, rather, joined) */
}
}
@@ -47,7 +49,7 @@ class Translator { // add class name
declarations = declarations + Const(cl.id + "#t", true, TypeName);
// translate monitor invariant
- declarations = declarations ::: translateMonitorInvariant(cl.Invariants);
+ declarations = declarations ::: translateMonitorInvariant(cl.Invariants, cl.pos);
// translate each member
for(member <- cl.members) {
declarations = declarations ::: translateMember(member);
@@ -74,24 +76,26 @@ class Translator { }
}
- def translateMonitorInvariant(invs: List[MonitorInvariant]): List[Decl] = {
- val (m1V, m1) = NewBVar("m1", tmask, true); val (h1V, h1) = NewBVar("h1", theap, true);
- val (m2V, m2) = NewBVar("m2", tmask, true); val (h2V, h2) = NewBVar("h2", theap, true);
+ def translateMonitorInvariant(invs: List[MonitorInvariant], pos: Position): List[Decl] = {
+ val (h0V, h0) = NewBVar("h0", theap, true); val (m0V, m0) = NewBVar("m0", tmask, true);
+ val (c0V, c0) = NewBVar("c0", tcredits, true);
+ val (h1V, h1) = NewBVar("h1", theap, true); val (m1V, m1) = NewBVar("m1", tmask, true);
+ val (c1V, c1) = NewBVar("c1", tcredits, true);
val (lkV, lk) = NewBVar("lk", tref, true);
- val oldTranslator = new ExpressionTranslator(List(h2, m2), List(h1, m1), currentClass);
+ val oldTranslator = new ExpressionTranslator(List(h1, m1, c1), List(h0, m0, c0), currentClass);
Proc(currentClass.id + "$monitorinvariant$checkDefinedness",
List(NewBVarWhere("this", new Type(currentClass))),
Nil,
GlobalNames,
DefaultPrecondition(),
- BLocal(h1V) :: BLocal(m1V) ::BLocal(h2V) :: BLocal(m2V) :: BLocal(lkV) ::
- bassume(wf(h1, m1)) :: bassume(wf(h2, m2)) ::
- (oldTranslator.Mask := ZeroMask) ::
+ BLocal(h0V) :: BLocal(m0V) :: BLocal(c0V) :: BLocal(h1V) :: BLocal(m1V) :: BLocal(c1V) :: BLocal(lkV) ::
+ bassume(wf(h0, m0)) :: bassume(wf(h1, m1)) ::
+ (oldTranslator.Mask := ZeroMask) :: (oldTranslator.Credits := ZeroCredits) ::
oldTranslator.Inhale(invs map { mi => mi.e}, "monitor invariant", false) :::
- (etran.Mask := ZeroMask) ::
+ (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Havoc(etran.Heap) ::
// check that invariant is well-defined
- etran.WhereOldIs(h2, m2).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
+ etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true) :::
(if (!checkLeaks || invs.length == 0) Nil else
// check that there are no loops among .mu permissions in monitors
// !CanWrite[this,mu]
@@ -106,7 +110,9 @@ class Translator { "Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu")
) :::
//check that invariant is reflexive
- etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false))
+ etran.UseCurrentAsOld().Exhale(invs map {mi => (mi.e, ErrorMessage(mi.pos, "Monitor invariant might not be reflexive."))}, "invariant reflexive?", false) :::
+ bassert(DebtCheck(), pos, "Monitor invariant is not allowed to contain debt.")
+ )
}
def translateField(f: Field): List[Decl] = {
@@ -119,7 +125,7 @@ class Translator { etran.checkTermination = true;
val checkBody = isDefined(f.definition);
etran.checkTermination = false;
- // BoogiePL function that represents the dafny function
+ // Boogie function that represents the Chalice function
Boogie.Function(functionName(f), BVar("heap", theap) :: Boogie.BVar("mask", tmask) :: Boogie.BVar("this", tref) :: (f.ins map Variable2BVar), new Boogie.BVar("$myresult", Boogie.ClassType(f.out.typ))) ::
// check definedness of the function's precondition and body
Proc(f.FullName + "$checkDefinedness",
@@ -158,7 +164,7 @@ class Translator { Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
List(applyF),
- (wf(Heap, Mask) && (CurrentModule ==@ ModuleName(currentClass)))
+ (wf(VarExpr(HeapName), VarExpr(MaskName)) && (CurrentModule ==@ ModuleName(currentClass)))
==>
(applyF ==@ etran.Tr(f.definition)))
)
@@ -180,7 +186,7 @@ class Translator { Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
List(applyF),
- (wf(Heap, Mask) && IsGoodState(version) && CanAssumeFunctionDefs)
+ (wf(VarExpr(HeapName), VarExpr(MaskName)) && IsGoodState(version) && CanAssumeFunctionDefs)
==>
(applyF ==@ applyFrameFunction))
)
@@ -195,13 +201,13 @@ 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 = FunctionApp(functionName(f), List(Heap, Mask) ::: args)
+ val applyF = FunctionApp(functionName(f), List(VarExpr(HeapName), VarExpr(MaskName)) ::: args)
//postcondition axioms
(Postconditions(f.spec) map { post : Expression =>
Axiom(new Boogie.Forall(
BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar),
List(applyF),
- (wf(Heap, Mask) && CanAssumeFunctionDefs)
+ (wf(VarExpr(HeapName), VarExpr(MaskName)) && CanAssumeFunctionDefs)
==>
etran.Tr(SubstResult(post, f.apply(ExplicitThisExpr(), f.ins map { arg => new VariableExpr(arg) })))
))
@@ -235,7 +241,7 @@ class Translator { // check precondition
InhaleWithChecking(Preconditions(method.spec), "precondition") :::
DefineInitialState :::
- (Mask := ZeroMask) ::
+ (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Havoc(etran.Heap) ::
// check postcondition
InhaleWithChecking(Postconditions(method.spec), "postcondition") :::
@@ -255,7 +261,14 @@ class Translator { translateStatements(method.body) :::
Exhale(Postconditions(method.spec) map { p => ((if(0<defaults) UnfoldPredicatesWithReceiverThis(p) else p), ErrorMessage(method.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::
(if(checkLeaks) isLeaking(method.pos, "Method " + method.FullName + " might leak refereces.") else Nil) :::
- bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.")) :: Nil
+ bassert(LockFrame(LockChanges(method.spec), etran), method.pos, "Method might lock/unlock more than allowed.") :::
+ bassert(DebtCheck, method.pos, "Method body is not allowed to leave any debt."))
+ }
+
+ def DebtCheck() = {
+ // (forall ch :: ch == null || 0 <= Credits[ch])
+ val (chV, ch) = NewBVar("ch", tref, false)
+ new Boogie.Forall(chV, (ch ==@ bnull) || (0 <= new MapSelect(etran.Credits, ch)))
}
def DefaultPrecondition() : List[String] =
@@ -264,12 +277,13 @@ class Translator { }
def DefinePreInitialState = {
Comment("define pre-initial state") ::
- (etran.Mask := ZeroMask)
+ (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits)
}
def DefineInitialState = {
Comment("define initial state") ::
bassume(etran.Heap ==@ Boogie.Old(etran.Heap)) ::
- bassume(etran.Mask ==@ Boogie.Old(etran.Mask))
+ bassume(etran.Mask ==@ Boogie.Old(etran.Mask)) ::
+ bassume(etran.Credits ==@ Boogie.Old(etran.Credits))
}
/**********************************************************************
@@ -285,11 +299,13 @@ class Translator { val newGlobals = etran.FreshGlobals("assert");
val tmpHeap = Boogie.NewBVar(HeapName, theap, true);
val tmpMask = Boogie.NewBVar(MaskName, tmask, true);
- val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id), currentClass);
+ val tmpCredits = Boogie.NewBVar(CreditsName, tcredits, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), currentClass);
Comment("assert") ::
- // exhale e in a copy of the heap/mask
- BLocal(tmpHeap._1) :: (tmpHeap._2 := Heap) ::
- BLocal(tmpMask._1) :: (tmpMask._2 := Mask) ::
+ // exhale e in a copy of the heap/mask/credits
+ BLocal(tmpHeap._1) :: (tmpHeap._2 := VarExpr(HeapName)) ::
+ BLocal(tmpMask._1) :: (tmpMask._2 := VarExpr(MaskName)) ::
+ BLocal(tmpCredits._1) :: (tmpCredits._2 := VarExpr(CreditsName)) ::
tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true)
case Assume(e) =>
Comment("assume") ::
@@ -321,8 +337,8 @@ class Translator { }
Comment("assigment to " + lhs.id) ::
(rhs match {
- case rhs@NewRhs(c, initialization) => // x := new C;
- val (nw, ss) = translateAllocation(rhs.typ, initialization);
+ case rhs@NewRhs(c, initialization, lower, upper) => // x := new C;
+ val (nw, ss) = translateAllocation(rhs.typ, initialization, lower, upper, rhs.pos);
ss ::: assignOrAssumeEqual(new VarExpr(nw))
case rhs: Expression => // x := E;
isDefined(rhs) ::: assignOrAssumeEqual(rhs)
@@ -330,9 +346,9 @@ class Translator { case FieldUpdate(lhs@MemberAccess(target, f), rhs) =>
val (statements, toStore : Expr) =
(rhs match {
- case rhs @ NewRhs(c, initialization) =>
+ case rhs @ NewRhs(c, initialization, lower, upper) =>
// e.f := new C;
- val (nw,ss) = translateAllocation(rhs.typ, initialization)
+ val (nw,ss) = translateAllocation(rhs.typ, initialization, lower, upper, rhs.pos)
(ss, new VarExpr(nw))
case rhs : Expression =>
// e.f := E;
@@ -341,7 +357,7 @@ class Translator { Comment("update field " + f) ::
isDefined(target) :::
bassert(CanWrite(target, lhs.f), s.pos, "Location might not be writable") ::
- statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(Heap, Mask))
+ statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(VarExpr(HeapName), VarExpr(MaskName)))
case lv @ LocalVar(id, t, const, ghost, rhs) =>
val bv = Variable2BVarWhere(lv.v)
val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, Boogie.ClassType(BoolClass)) else null
@@ -365,7 +381,7 @@ class Translator { bassert(nonNull(obj), s.pos, "The target of the install statement might be null.") ::
bassert(isHeld(obj), s.pos, "The lock of the target of the install statement might not be held.") ::
// assert CanWrite(obj.mu); assume lowerbounds < obj.mu < upperBounds;
- UpdateMu(obj, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Install might fail."))
+ UpdateMu(obj, false, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Install might fail."))
case Share(obj, lowerBounds, upperBounds) =>
val (preShareMaskV, preShareMask) = Boogie.NewBVar("preShareMask", tmask, true)
Comment("share") ::
@@ -373,7 +389,7 @@ class Translator { BLocal(preShareMaskV) :: Boogie.Assign(preShareMask, etran.Mask) ::
isDefined(obj) :::
bassert(nonNull(obj), s.pos, "The target of the share statement might be null.") ::
- UpdateMu(obj, true, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
+ UpdateMu(obj, true, false, lowerBounds, upperBounds, ErrorMessage(s.pos, "Share might fail.")) :::
bassume(!isHeld(obj) && ! isRdHeld(obj)) :: // follows from o.mu==lockbottom
// no permission to o.held
etran.SetNoPermission(etran.Tr(obj), "held", etran.Mask) ::
@@ -381,7 +397,8 @@ class Translator { ExhaleInvariants(obj, false, ErrorMessage(s.pos, "Monitor invariant might not hold."), etran.UseCurrentAsOld()) :::
// assume a seen state is the one right before the share
bassume(LastSeenHeap(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ etran.Heap) ::
- bassume(LastSeenMask(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ preShareMask)
+ bassume(LastSeenMask(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ preShareMask) ::
+ bassume(LastSeenCredits(etran.Heap.select(obj, "mu"), etran.Heap.select(obj, "held")) ==@ etran.Credits)
case Unshare(obj) =>
val (heldV, held) = Boogie.NewBVar("held", Boogie.NamedType("int"), true)
val o = TrExpr(obj)
@@ -522,8 +539,9 @@ class Translator { val (tokenV,tokenId) = NewBVar("token", tref, true)
val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true)
- val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true)
val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true)
+ val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true)
+ val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true)
val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
val argsSeqLength = 1 + args.length;
Comment("call " + id) ::
@@ -532,9 +550,10 @@ class Translator { List[Stmt]()
else
List(BLocal(Variable2BVarWhere(c.local))) } :::
- // remember the value of the heap and mask
- BLocal(preCallMaskV) :: (preCallMask := etran.Mask) ::
+ // remember the value of the heap/mask/credits
BLocal(preCallHeapV) :: (preCallHeap := etran.Heap) ::
+ BLocal(preCallMaskV) :: (preCallMask := etran.Mask) ::
+ BLocal(preCallCreditsV) :: (preCallCredits := etran.Credits) ::
BLocal(argsSeqV) ::
// introduce formal parameters and pre-state globals
(for (v <- formalThisV :: formalInsV) yield BLocal(Variable2BVarWhere(v))) :::
@@ -556,9 +575,9 @@ class Translator { // create a new token
BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
// the following assumes help in proving that the token is fresh
- bassume(Heap.select(tokenId, "joinable") ==@ 0) ::
- bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$N")==@ 0) ::
- bassume(new Boogie.MapSelect(Mask, tokenId, "joinable", "perm$R")==@ 0) ::
+ bassume(etran.Heap.select(tokenId, "joinable") ==@ 0) ::
+ bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$N")==@ 0) ::
+ bassume(new Boogie.MapSelect(etran.Mask, tokenId, "joinable", "perm$R")==@ 0) ::
etran.IncPermission(tokenId, "joinable", 100) ::
// create a fresh value for the joinable field
BLocal(asyncStateV) :: Boogie.Havoc(asyncState) :: bassume(asyncState !=@ 0) ::
@@ -566,6 +585,7 @@ class Translator { // assume the pre call state for the token is the state before inhaling the precondition
bassume(CallHeap(asyncState) ==@ preCallHeap) ::
bassume(CallMask(asyncState) ==@ preCallMask) ::
+ bassume(CallCredits(asyncState) ==@ preCallCredits) ::
bassume(CallArgs(asyncState) ==@ argsSeq) ::
// assign the returned token to the variable
{ if (token != null) List(token := tokenId) else List() }
@@ -580,19 +600,21 @@ class Translator { val (argsSeqV, argsSeq) = NewBVar("argsSeq", tArgSeq, true)
val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true);
val (preCallMaskV, preCallMask) = NewBVar("preCallMask", tmask, true);
- val preGlobals = List(preCallHeap, preCallMask);
- val postEtran = new ExpressionTranslator(List(etran.Heap, etran.Mask), preGlobals, currentClass);
+ val (preCallCreditsV, preCallCredits) = NewBVar("preCallCredits", tcredits, true);
+ val preGlobals = List(preCallHeap, preCallMask, preCallCredits);
+ val postEtran = new ExpressionTranslator(List(etran.Heap, etran.Mask, etran.Credits), preGlobals, currentClass);
Comment("join async") ::
+ // check that token is well-defined
+ isDefined(token) :::
// check that we did not join yet
bassert(CanWrite(token, "joinable"), jn.pos, "The joinable field might not be writable.") ::
bassert(etran.Heap.select(token, "joinable") !=@ 0, jn.pos, "The joinable field might not be true.") ::
// lookup token.joinable
BLocal(argsSeqV) :: (argsSeq := CallArgs(etran.Heap.select(token, "joinable"))) ::
- // check that token is well-defined
- isDefined(token) :::
// retrieve the call's pre-state from token.joinable
BLocal(preCallHeapV) :: (preCallHeap := CallHeap(etran.Heap.select(token, "joinable"))) ::
BLocal(preCallMaskV) :: (preCallMask := CallMask(etran.Heap.select(token, "joinable"))) ::
+ BLocal(preCallCreditsV) :: (preCallCredits := CallCredits(etran.Heap.select(token, "joinable"))) ::
// introduce locals for the out parameters
(for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
// initialize the in parameters
@@ -609,11 +631,60 @@ class Translator { postEtran.Inhale(Postconditions(jn.m.spec) map
{ p => SubstThisAndVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
// assign formal outs to actual outs
- (for ((v,e) <- lhs zip formalOuts) yield (v :=e))
+ (for ((v,e) <- lhs zip formalOuts) yield (v := e))
+ case s@Send(ch, args) =>
+ val channel = ch.typ.asInstanceOf[ChannelClass].ch
+ val formalThisV = new Variable("this", new Type(ch.typ))
+ val formalThis = new VariableExpr(formalThisV)
+ val formalParamsV = for (p <- channel.parameters) yield new Variable(p.id, p.t)
+ val formalParams = for (v <- formalParamsV) yield new VariableExpr(v)
+ Comment("send") ::
+ // introduce formal parameters
+ (for (v <- formalThisV :: formalParamsV) yield BLocal(Variable2BVarWhere(v))) :::
+ // check definedness of arguments
+ isDefined(ch) :::
+ bassert(nonNull(ch), ch.pos, "The channel might be null.") ::
+ (args flatMap { e: Expression => isDefined(e)}) :::
+ // assign actual ins to formal parameters
+ (formalThis := ch) ::
+ (for ((v,e) <- formalParams zip args) yield (v := e)) :::
+ // increase credits
+ new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) + 1) ::
+ // exhale where clause
+ Exhale(List(
+ (SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams),
+ ErrorMessage(s.pos, "The where clause at " + channel.where.pos + " might not hold."))),
+ "channel where clause")
+ case r@Receive(ch, outs) =>
+ val channel = ch.typ.asInstanceOf[ChannelClass].ch
+ val formalThisV = new Variable("this", new Type(ch.typ))
+ val formalThis = new VariableExpr(formalThisV)
+ val formalParamsV = for (p <- channel.parameters) yield new Variable(p.id, p.t)
+ val formalParams = for (v <- formalParamsV) yield new VariableExpr(v)
+ Comment("receive") ::
+ // check definedness of arguments
+ isDefined(ch) :::
+ bassert(nonNull(ch), ch.pos, "The channel might be null.") ::
+ // check that credits are positive
+ bassert(0 < new Boogie.MapSelect(etran.Credits, TrExpr(ch)), r.pos, "receive operation requires a credit") ::
+ // ...and check: maxlock << ch.mu
+ bassert(CanRead(ch, "mu"), r.pos, "The mu field of the channel in the receive statement might not be readable.") ::
+ bassert(etran.MaxLockIsBelowX(etran.Heap.select(ch, "mu")), r.pos, "The channel must lie above maxlock in the wait order") ::
+ // introduce locals for the parameters
+ (for (v <- formalThisV :: formalParamsV) yield BLocal(Variable2BVarWhere(v))) :::
+ // initialize the parameters; that is, set "this" to the channel and havoc the other formal parameters
+ (formalThis := ch) ::
+ (for (v <- formalParams) yield Havoc(v)) :::
+ // inhale where clause
+ Inhale(List(SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::
+ // assign formal outs to actual outs
+ (for ((v,e) <- outs zip formalParams) yield (v := e)) :::
+ // decrease credits
+ new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1)
}
}
- def translateAllocation(cl: Class, initialization: List[Init]): (Boogie.BVar, List[Boogie.Stmt]) = {
+ def translateAllocation(cl: Class, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression], pos: Position): (Boogie.BVar, List[Boogie.Stmt]) = {
val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true)
val (ttV,tt) = Boogie.NewTVar("T")
val f = new Boogie.BVar("f", FieldType(tt))
@@ -623,7 +694,10 @@ class Translator { bassume(nonNull(nwe) && (dtype(nwe) ==@ TrType(cl))) ::
bassume(new Boogie.Forall(ttV, f, etran.HasNoPermission(nwe, f.id))) ::
// initial values of fields:
- bassume(etran.Heap.select(nwe, "mu") ==@ bLockBottom) ::
+ (if (cl.IsChannel)
+ UpdateMu(nwe, false, true, lowerBounds, upperBounds, ErrorMessage(pos, "new might fail."))
+ else
+ List(bassume(etran.Heap.select(nwe, "mu") ==@ bLockBottom))) :::
bassume(etran.Heap.select(nwe, "held") <= 0) ::
bassume(etran.Heap.select(nwe, "rdheld") ==@ false) ::
// give access to user-defined fields and special fields:
@@ -650,30 +724,40 @@ class Translator { BLocal(lastAcquireVar) :: Havoc(lastAcquire) :: bassume(0 < lastAcquire) ::
etran.SetFullPermission(o, "held") ::
etran.Heap.store(o, "held", lastAcquire) ::
- InhaleInvariants(nonNullObj, false, etran.WhereOldIs(LastSeenHeap(lastSeenMu, lastSeenHeld), LastSeenMask(lastSeenMu, lastSeenHeld))) :::
- // remember values of Heap/Mask globals (for proving history constraint at release)
+ InhaleInvariants(nonNullObj, false, etran.WhereOldIs(
+ LastSeenHeap(lastSeenMu, lastSeenHeld),
+ LastSeenMask(lastSeenMu, lastSeenHeld),
+ LastSeenCredits(lastSeenMu, lastSeenHeld))) :::
+ // remember values of Heap/Mask/Credits globals (for proving history constraint at release)
bassume(AcquireHeap(lastAcquire) ==@ etran.Heap) ::
- bassume(AcquireMask(lastAcquire) ==@ etran.Mask)
+ bassume(AcquireMask(lastAcquire) ==@ etran.Mask) ::
+ bassume(AcquireCredits(lastAcquire) ==@ etran.Credits)
}
def TrRelease(s: Statement, nonNullObj: Expression) = {
val (heldV, held) = Boogie.NewBVar("held", tint, true)
val (prevLmV, prevLm) = Boogie.NewBVar("prevLM", tref, true)
- val (preReleaseMaskV, preReleaseMask) = NewBVar("preReleaseMask", tmask, true)
val (preReleaseHeapV, preReleaseHeap) = NewBVar("preReleaseHeap", theap, true)
+ val (preReleaseMaskV, preReleaseMask) = NewBVar("preReleaseMask", tmask, true)
+ val (preReleaseCreditsV, preReleaseCredits) = NewBVar("preReleaseCredits", tcredits, true)
val o = TrExpr(nonNullObj);
- BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::
BLocal(preReleaseHeapV) :: (preReleaseHeap := etran.Heap) ::
+ BLocal(preReleaseMaskV) :: (preReleaseMask := etran.Mask) ::
+ BLocal(preReleaseCreditsV) :: (preReleaseCredits := etran.Credits) ::
bassert(CanWrite(o, "held"), s.pos, "The held field of the target of the release statement might not be writable.") ::
bassert(isHeld(o), s.pos, "The target of the release statement might be not be locked by the current thread.") ::
bassert(!isRdHeld(o), s.pos, "Release might fail because the current thread might hold the read lock.") ::
- ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(AcquireHeap(etran.Heap.select(o, "held")), AcquireMask(etran.Heap.select(o, "held")))) :::
+ ExhaleInvariants(nonNullObj, false, ErrorMessage(s.pos, "Monitor invariant might hot hold."), etran.WhereOldIs(
+ AcquireHeap(etran.Heap.select(o, "held")),
+ AcquireMask(etran.Heap.select(o, "held")),
+ AcquireCredits(etran.Heap.select(o, "held")))) :::
// havoc o.held where 0<=o.held
BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::
etran.Heap.store(o, "held", held) ::
etran.SetNoPermission(o, "held", etran.Mask) ::
// assume a seen state is the one right before the share
bassume(LastSeenHeap(etran.Heap.select(o, "mu"), held) ==@ preReleaseHeap) ::
- bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask)
+ bassume(LastSeenMask(etran.Heap.select(o, "mu"), held) ==@ preReleaseMask) ::
+ bassume(LastSeenCredits(etran.Heap.select(o, "mu"), held) ==@ preReleaseCredits)
}
def TrRdAcquire(s: Statement, nonNullObj: Expression) = {
val (heldV, held) = Boogie.NewBVar("held", tint, true)
@@ -761,6 +845,7 @@ class Translator { (for (v <- preLoopGlobals) yield BLocal(v)) :::
(loopEtran.oldEtran.Heap := loopEtran.Heap) ::
(loopEtran.oldEtran.Mask := loopEtran.Mask) :: // oldMask is not actually used below
+ (loopEtran.oldEtran.Credits := loopEtran.Credits) :: // is oldCredits?
// check invariant on entry to the loop
Exhale(invs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::
// save values of local-variable loop targets
@@ -775,19 +860,20 @@ class Translator { // 1. CHECK DEFINEDNESS OF INVARIANT
Comment("check loop invariant definedness") ::
//(w.LoopTargets.toList map { v: Variable => Boogie.Havoc(Boogie.VarExpr(v.id)) }) :::
- Boogie.Havoc(etran.Heap) :: Boogie.Assign(etran.Mask, ZeroMask) ::
+ Boogie.Havoc(etran.Heap) :: Boogie.Assign(etran.Mask, ZeroMask) :: Boogie.Assign(etran.Credits, ZeroCredits) ::
InhaleWithChecking(invs, "loop invariant definedness") :::
bassume(false)
, Boogie.If(null,
// 2. CHECK LOOP BODY
- // Renew Heap and Mask: set Mask to ZeroMask, and havoc Heap everywhere except
+ // Renew state: set Mask to ZeroMask and Credits to ZeroCredits, and havoc Heap everywhere except
// at {old(local),local}.{held,rdheld}
- Havoc(etran.Heap) :: (etran.Mask := ZeroMask) ::
+ Havoc(etran.Heap) :: (etran.Mask := ZeroMask) :: (etran.Credits := ZeroCredits) ::
Inhale(invs, "loop invariant, body") :::
// this is the state at the beginning of the loop iteration; save these values
(for (v <- iterStartGlobals) yield BLocal(v)) :::
(iterStartEtran.oldEtran.Heap := iterStartEtran.Heap) ::
(iterStartEtran.oldEtran.Mask := iterStartEtran.Mask) :: // oldMask is not actually used below
+ (iterStartEtran.oldEtran.Credits := iterStartEtran.Credits) :: // is oldCredits?
(for (isv <- iterStartLocalsV) yield BLocal(Variable2BVarWhere(isv))) :::
(for ((v,isv) <- w.LoopTargetsList zip iterStartLocalsV) yield
(new VariableExpr(isv) := new VariableExpr(v))) :::
@@ -799,6 +885,8 @@ class Translator { isLeaking(w.pos, "The loop might leak refereces.") :::
// enforce lockchange
(NumberOfLocksHeldIsInvariant(iterStartLocks, newLocks, iterStartEtran) map { e: Boogie.Expr => bassert(e, w.pos, "The loop might lock/unlock more than the changelock clause allows.") }) :::
+ // perform debt check
+ bassert(DebtCheck, w.pos, "Loop body is not allowed to leave any debt.") :::
bassume(false),
// 3. AFTER LOOP
LockHavoc(oldLocks ++ newLocks, loopEtran) :::
@@ -807,7 +895,7 @@ class Translator { bassume(!guard)))
}
- def UpdateMu(o: Expr, allowOnlyFromBottom: boolean,
+ def UpdateMu(o: Expr, allowOnlyFromBottom: boolean, justAssumeValue: boolean,
lowerBounds: List[Expression], upperBounds: List[Expression], error: ErrorMessage): List[Stmt] = {
def BoundIsNullObject(b: Expression): Boogie.Expr = {
if (b.typ.IsMu) false else b ==@ bnull
@@ -821,9 +909,12 @@ class Translator { val (muV, mu) = Boogie.NewBVar("mu", Boogie.NamedType("Mu"), true)
// check that bounds are well-defined
((lowerBounds ++ upperBounds) flatMap { bound => isDefined(bound)}) :::
- // check that we have full access to mu
- bassert(CanWrite(o, "mu"), error.pos, error.message + " The mu field of the target might not be writable.") ::
- // ...and that mu starts off as lockbottom, if desired
+ // check that we have full access to o.mu
+ (if (!justAssumeValue)
+ List(bassert(CanWrite(o, "mu"), error.pos, error.message + " The mu field of the target might not be writable."))
+ else
+ List()) :::
+ // ...and that o.mu starts off as lockbottom, if desired
(if (allowOnlyFromBottom)
List(bassert(etran.Heap.select(o,"mu") ==@ bLockBottom,
error.pos, error.message + " The object may already be shared (i.e., mu may not be LockBottom)"))
@@ -845,15 +936,15 @@ class Translator { case _ => BoundIsNullObject(lb) ||
BoundIsNullObject(ub) ||
Below(MuValue(lb), MuValue(ub)) }, lb.pos, "The lower bound at " + lb.pos + " might not be smaller than the upper bound at " + ub.pos + ".")) :::
- // havoc o.mu
+ // havoc mu
BLocal(muV) :: Havoc(mu) :: bassume(mu !=@ bLockBottom) ::
- // assume that o.mu is between the given bounds (or above maxlock if no bounds are given)
+ // assume that mu is between the given bounds (or above maxlock if no bounds are given)
(if (lowerBounds == Nil && upperBounds == Nil) {
- // assume maxlock << o.mu
+ // assume maxlock << mu
List(bassume(etran.MaxLockIsBelowX(mu)))
} else {
(for (lb <- lowerBounds) yield
- // assume lb << o.mu
+ // assume lb << mu
bassume(
if (etran.IsMaxLockLit(lb)) {
val (f,o) = etran.ShaveOffOld(lb)
@@ -861,7 +952,7 @@ class Translator { } else
(BoundIsNullObject(lb) || Below(MuValue(lb), mu)))) :::
(for (ub <- upperBounds) yield
- // assume o.mu << ub
+ // assume mu << ub
bassume(
if (etran.IsMaxLockLit(ub)) {
val (f,o) = etran.ShaveOffOld(ub)
@@ -870,7 +961,7 @@ class Translator { (BoundIsNullObject(ub) || Below(mu, MuValue(ub)))))
}) :::
// store the mu field
- etran.Heap.store(o, "mu", mu)
+ (if (justAssumeValue) bassume(etran.Heap.select(o, "mu") ==@ mu) else etran.Heap.store(o, "mu", mu))
}
def isLeaking(pos: Position, msg: String): List[Boogie.Stmt] = {
@@ -992,18 +1083,20 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val Heap = globals(0);
val Mask = globals(1);
+ val Credits = globals(2);
lazy val oldEtran = new ExpressionTranslator(preGlobals, preGlobals, currentClass)
var checkTermination = false; // check that heap required by callee is strictly smaller than heap required by caller
def this(globals: List[Boogie.Expr], cl: Class) = this(globals, globals map (g => Boogie.Old(g)), cl)
def this(cl: Class) = this(for ((id,t) <- S_ExpressionTranslator.Globals) yield Boogie.VarExpr(id), cl)
- def Globals = List(Heap, Mask)
+ def Globals = List(Heap, Mask, Credits)
def ChooseEtran(chooseOld: boolean) = if (chooseOld) oldEtran else this
// Create a list of fresh global variables
def FreshGlobals(prefix: String) = {
- new Boogie.BVar(prefix + "Heap", theap, true) ::
- new Boogie.BVar(prefix + "Mask", tmask, true) ::
+ new Boogie.BVar(prefix + HeapName, theap, true) ::
+ new Boogie.BVar(prefix + MaskName, tmask, true) ::
+ new Boogie.BVar(prefix + CreditsName, tcredits, true) ::
Nil
}
@@ -1019,8 +1112,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E new ExpressionTranslator(globals, globals, currentClass);
}
- def WhereOldIs(h: Boogie.Expr, m: Boogie.Expr) = {
- new ExpressionTranslator(globals, List(h, m), currentClass);
+ def WhereOldIs(h: Boogie.Expr, m: Boogie.Expr, c: Boogie.Expr) = {
+ new ExpressionTranslator(globals, List(h, m, c), currentClass);
}
/**********************************************************************
@@ -1049,6 +1142,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case _:RdAccess => throw new Exception("rd expression unexpected here")
case _:AccessAll => throw new Exception("acc expression unexpected here")
case _:RdAccessAll => throw new Exception("rd expression unexpected here")
+ case c@Credit(e, n) =>
+ isDefined(e);
+ isDefined(c.N)
case Holds(e) =>
isDefined(e)
case RdHolds(e) =>
@@ -1064,16 +1160,18 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val newGlobals = FreshGlobals("checkPre");
val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
- val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask), currentClass);
+ val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap,tmpMask,tmpCredits), currentClass);
// check definedness of receiver + arguments
(obj :: args flatMap { arg => isDefined(arg) }) :::
// check that receiver is not null
List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
- // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask
+ // check precondition of the function by exhaling the precondition in tmpHeap/tmpMask/tmpCredits
Comment("check precondition of call") ::
bassume(assumption) ::
BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
BLocal(tmpMaskV) :: (tmpMask := Mask) :::
+ BLocal(tmpCreditsV) :: (tmpCredits := Credits) :::
tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstThisAndVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
"function call",
false) :::
@@ -1099,14 +1197,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E }
val newGlobals = FreshGlobals("checkPre");
val (tmpHeapV, tmpHeap) = Boogie.NewBVar("Heap", theap, true);
- val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
- val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask), currentClass);
+ val (tmpMaskV, tmpMask) = Boogie.NewBVar("Mask", tmask, true);
+ val (tmpCreditsV, tmpCredits) = Boogie.NewBVar("Credits", tcredits, true);
+ val tmpTranslator = new ExpressionTranslator(List(tmpHeap, tmpMask, tmpCredits), currentClass);
Comment("unfolding") ::
// check definedness
checks :::
// copy state into temporary variables
BLocal(tmpHeapV) :: Boogie.Assign(tmpHeap, Heap) ::
BLocal(tmpMaskV) :: Boogie.Assign(tmpMask, Mask) ::
+ BLocal(tmpCreditsV) :: Boogie.Assign(tmpCredits, Credits) ::
// exhale the predicate
tmpTranslator.Exhale(List((predicate, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false) :::
// inhale the definition of the predicate
@@ -1164,8 +1264,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Length(e) =>
isDefined(e)
case Eval(h, e) =>
- val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
- val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+ val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
+ val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.isDefined(e)
}
}
@@ -1208,6 +1308,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case _:RdAccess => throw new Exception("rd expression unexpected here")
case _:AccessAll => throw new Exception("acc expression unexpected here")
case _:RdAccessAll => throw new Exception("rd expression unexpected here")
+ case _:Credit => throw new Exception("credit expression unexpected here")
case Holds(e) =>
(0 < Heap.select(Tr(e), "held")) &&
!Heap.select(Tr(e), "rdheld")
@@ -1240,9 +1341,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E true
else
MaxLockPreserved
- case ((MaxLockLiteral(),o), (fs@MemberAccess(q, "mu"), useOld)) => isHeldInHeap(Tr(q), ChooseEtran(useOld).Heap) && ChooseEtran(o).MaxLockEqualsX(Tr(fs))
- case ((MaxLockLiteral(),o), _) => ChooseEtran(o).MaxLockEqualsX(Tr(e1))
- case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).MaxLockEqualsX(Tr(e0))
+ case ((MaxLockLiteral(),o), _) => ChooseEtran(o).IsHighestLock(Tr(e1))
+ case (_, (MaxLockLiteral(),o)) => ChooseEtran(o).IsHighestLock(Tr(e0))
case _ => if(e0.typ.IsSeq) FunctionApp("Seq#Equal", List(Tr(e0), Tr(e1))) else (Tr(e0) ==@ Tr(e1))
}
case Neq(e0,e1) =>
@@ -1311,8 +1411,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Length(e) =>
Boogie.FunctionApp("Seq#Length", List(Tr(e)))
case Eval(h, e) =>
- val (evalHeap, evalMask, checks, assumptions) = fromEvalState(h);
- val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask), currentClass);
+ val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
+ val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
evalEtran.Tr(e)
}
@@ -1344,7 +1444,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E Comment("inhale (" + occasion + ")") ::
BLocal(ihV) :: Boogie.Havoc(ih) ::
bassume(IsGoodInhaleState(ih, Heap, Mask)) ::
- List.flatten (for (p <- predicates) yield Inhale(p,ih, check)) :::
+ List.flatten (for (p <- predicates) yield Inhale(p, ih, check)) :::
bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
Comment("end inhale")
@@ -1430,6 +1530,15 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodState(Boogie.MapSelect(ih, trE, memberName))) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(ih, Mask))
+ case cr@Credit(ch, n) =>
+ val trCh = Tr(ch)
+ (if (check)
+ isDefined(ch)(true) :::
+ bassert(nonNull(trCh), ch.pos, "The target of the credit predicate might be null.") :::
+ isDefined(cr.N)(true)
+ else
+ Nil) :::
+ new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) + Tr(cr.N))
case Implies(e0,e1) =>
(if(check) isDefined(e0)(true) else Nil) :::
Boogie.If(Tr(e0), Inhale(e1, ih, check), Nil)
@@ -1440,8 +1549,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E Inhale(e0, ih, check) ::: Inhale(e1, ih, check)
case holds@Holds(e) =>
val trE = Tr(e);
- (if(check) isDefined(e)(true) :::
- List(bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")) else Nil) :::
+ (if(check)
+ isDefined(e)(true) :::
+ bassert(nonNull(trE), holds.pos, "The target of the holds predicate might be null.")
+ else Nil) :::
IncPermission(trE, "held", 100) :::
bassume(IsGoodMask(Mask)) ::
bassume(IsGoodState(Boogie.MapSelect(ih, trE, "held"))) ::
@@ -1457,10 +1568,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(wf(Heap, Mask)) ::
bassume(wf(ih, Mask))
case Eval(h, e) =>
- val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+ val (evalHeap, evalMask, evalCredits, checks, proofOrAssume) = fromEvalState(h);
val preGlobals = etran.FreshGlobals("eval")
val preEtran = new ExpressionTranslator(preGlobals map (v => new Boogie.VarExpr(v)), currentClass)
- BLocal(preGlobals(0)) :: BLocal(preGlobals(1)) ::
+ BLocal(preGlobals(0)) :: BLocal(preGlobals(1)) :: BLocal(preGlobals(2)) ::
(new VarExpr(preGlobals(1)) := ZeroMask) ::
// Should we start from ZeroMask instead of an arbitrary mask? In that case, assume submask(preEtran.Mask, evalMask); at the end!
(if(check) checks else Nil) :::
@@ -1525,7 +1636,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E BLocal(fractionV) :: (frac := Tr(fraction)) ::
// if the mask does not contain sufficient permissions, try folding acc(e, fraction)
(if(e.isPredicate && autoFold && (!perm.isDefined || canTakeFractionOf(DefinitionOf(e.predicate)))) {
- val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+ val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);
val sourceVar = new Variable("fraction", new Type(IntClass));
val bplVar = Variable2BVar(sourceVar);
BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := frac) ::
@@ -1554,7 +1665,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E BLocal(epsilonsV) :: (if(epsilons!=null) (eps := Tr(epsilons)) :: Nil else Nil) :::
// if the mask does not contain sufficient permissions, try folding rdacc(e, epsilons)
(if(e.isPredicate && autoFold && canTakeEpsilonsOf(DefinitionOf(e.predicate)) && epsilons!=null) {
- val inhaleTran = new ExpressionTranslator(List(Heap, em), currentClass);
+ val inhaleTran = new ExpressionTranslator(List(Heap, em, Credits), currentClass);
val sourceVar = new Variable("epsilons", new Type(IntClass));
val bplVar = Variable2BVar(sourceVar);
BLocal(bplVar) :: (VarExpr(sourceVar.UniqueName) := eps) ::
@@ -1568,6 +1679,15 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodMask(Mask)) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(Heap, em))
+ case cr@Credit(ch, n) =>
+ val trCh = Tr(ch)
+ (if (check)
+ isDefined(ch)(true) :::
+ bassert(nonNull(trCh), ch.pos, "The target of the credit predicate might be null.") :::
+ isDefined(cr.N)(true)
+ else
+ Nil) :::
+ new Boogie.MapUpdate(Credits, trCh, new Boogie.MapSelect(Credits, trCh) - Tr(cr.N))
case Implies(e0,e1) =>
(if(check) isDefined(e0)(true) else Nil) :::
Boogie.If(Tr(e0), Exhale(e1, em, eh, error, check), Nil)
@@ -1587,11 +1707,12 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(wf(Heap, Mask)) ::
bassume(wf(Heap, em))
case Eval(h, e) =>
- val (evalHeap, evalMask, checks, proofOrAssume) = fromEvalState(h);
+ val (evalHeap, evalMask, evalCredits, checks, proofOrAssume) = fromEvalState(h);
val preGlobals = etran.FreshGlobals("eval")
- val preEtran = new ExpressionTranslator(List(Boogie.VarExpr(preGlobals(0).id), Boogie.VarExpr(preGlobals(1).id)), currentClass);
+ val preEtran = new ExpressionTranslator(List(Boogie.VarExpr(preGlobals(0).id), Boogie.VarExpr(preGlobals(1).id), Boogie.VarExpr(preGlobals(2).id)), currentClass);
BLocal(preGlobals(0)) :: (VarExpr(preGlobals(0).id) := evalHeap) ::
BLocal(preGlobals(1)) :: (VarExpr(preGlobals(1).id) := evalMask) ::
+ BLocal(preGlobals(2)) :: (VarExpr(preGlobals(2).id) := evalCredits) ::
(if(check) checks else Nil) :::
bassume(IsGoodMask(preEtran.Mask)) ::
bassume(wf(preEtran.Heap, preEtran.Mask)) ::
@@ -1600,18 +1721,25 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case e => (if(check) isDefined(e)(true) else Nil) ::: List(bassert(Tr(e), error.pos, error.message + " The expression at " + e.pos + " might not evaluate to true."))
}
- def fromEvalState(h: EvalState): (Expr, Expr, List[Stmt], Expr) = {
+ def fromEvalState(h: EvalState): (Expr, Expr, Expr, List[Stmt], Expr) = {
h match {
- case AcquireState(obj) =>
- (AcquireHeap(Heap.select(Tr(obj), "held")), AcquireMask(Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
- case ReleaseState(obj) =>
- (LastSeenHeap(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), LastSeenMask(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")), isDefined(obj)(true), true)
+ case AcquireState(obj) =>
+ (AcquireHeap(Heap.select(Tr(obj), "held")),
+ AcquireMask(Heap.select(Tr(obj), "held")),
+ AcquireCredits(Heap.select(Tr(obj), "held")),
+ isDefined(obj)(true), true)
+ case ReleaseState(obj) =>
+ (LastSeenHeap(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")),
+ LastSeenMask(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")),
+ LastSeenCredits(Heap.select(Tr(obj), "mu"), Heap.select(Tr(obj), "held")),
+ isDefined(obj)(true), true)
case CallState(token, obj, id, args) =>
val argsSeq = CallArgs(Heap.select(Tr(token), "joinable"));
var i : int = 0;
(CallHeap(Heap.select(Tr(token), "joinable")),
CallMask(Heap.select(Tr(token), "joinable")),
+ CallCredits(Heap.select(Tr(token), "joinable")),
isDefined(token)(true) :::
isDefined(obj)(true) :::
(args flatMap { a => isDefined(a)(true)}) :::
@@ -1695,31 +1823,22 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E def MaxLockIsBelowX(x: Boogie.Expr) = { // maxlock << x
val (oV, o) = Boogie.NewBVar("o", tref, false)
new Boogie.Forall(oV,
- (isHeldInHeap(o, Heap)) ==>
+ (contributesToWaitLevel(o, Heap, Credits)) ==>
new Boogie.FunctionApp("MuBelow", Boogie.MapSelect(Heap, o, "mu"), x))
}
def MaxLockIsAboveX(x: Boogie.Expr) = { // x << maxlock
val (oV, o) = Boogie.NewBVar("o", tref, false)
new Boogie.Exists(oV,
- (isHeldInHeap(o, Heap)) &&
+ (contributesToWaitLevel(o, Heap, Credits)) &&
new Boogie.FunctionApp("MuBelow", x, Boogie.MapSelect(Heap, o, "mu")))
}
- def MaxLockEqualsX(x: Boogie.Expr) = { // maxlock == o.mu
- // Note: Instead of the existential below, we could generate a nicer expression if we knew that
- // x has the form y.mu--then, we'd replace the existential with y.held. Another possibility
- // would be if we had an inverse of .mu (such an inverse exists, but we're not encoding it).
-// val (oV, o) = Boogie.NewBVar("o", tref, false)
- //new Boogie.Exists(oV,
- // (isHeldInHeap(o, Heap)) && (Boogie.MapSelect(Heap, o, "mu") ==@ x)) &&
- /*isHeldInHeap(x, Heap) &&*/ IsHighestLock(x)
- }
def IsHighestLock(x: Boogie.Expr) = {
// (forall r :: r.held ==> r.mu << x || r.mu == x)
val (rV, r) = Boogie.NewBVar("r", tref, false)
new Boogie.Forall(rV,
- (isHeldInHeap(r, Heap)) ==>
- (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) ||
- (Boogie.MapSelect(Heap, r, "mu") ==@ x)))
+ contributesToWaitLevel(r, Heap, Credits) ==>
+ (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) ||
+ (Boogie.MapSelect(Heap, r, "mu") ==@ x)))
}
def MaxLockPreserved = { // old(maxlock) == maxlock
// I don't know what the best encoding of this conding is, so I'll try a disjunction.
@@ -1758,7 +1877,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E // (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu)))
val (oV, o) = Boogie.NewBVar("o", tref, false)
new Boogie.Exists(oV,
- (0 < Boogie.MapSelect(e0.Heap, o, "held")) &&
+ (0 < Boogie.MapSelect(e1.Heap, o, "held")) &&
e0.MaxLockIsBelowX(Boogie.MapSelect(e1.Heap, o, "mu")))
}
@@ -1771,6 +1890,7 @@ object S_ExpressionTranslator { val Globals = {
("Heap", theap) ::
("Mask", tmask) ::
+ ("Credits", tcredits) ::
Nil
}
}
@@ -1801,12 +1921,13 @@ object S_ExpressionTranslator { def tseq(arg: BType) = IndexedType("Seq", arg)
def theap = NamedType("HeapType");
def tmask = NamedType("MaskType");
+ def tcredits = NamedType("CreditsType");
def ZeroMask = VarExpr("ZeroMask");
+ def ZeroCredits = VarExpr("ZeroCredits");
def HeapName = "Heap";
def MaskName = "Mask";
- def Heap = VarExpr(HeapName);
- def Mask = VarExpr(MaskName);
- def GlobalNames = List(HeapName, MaskName);
+ def CreditsName = "Credits";
+ def GlobalNames = List(HeapName, MaskName, CreditsName);
def CanAssumeFunctionDefs = VarExpr("CanAssumeFunctionDefs");
def CurrentModule = VarExpr("CurrentModule");
def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));
@@ -1820,18 +1941,22 @@ object S_ExpressionTranslator { def isShared(e: Expr): Expr = etran.Heap.select(e, "mu") !=@ bLockBottom
def LastSeenHeap(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Heap", List(sharedBit, heldBit))
def LastSeenMask(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Mask", List(sharedBit, heldBit))
+ def LastSeenCredits(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Credits", List(sharedBit, heldBit))
def AcquireHeap(heldBit: Expr) = FunctionApp("Acquire$Heap", List(heldBit))
def AcquireMask(heldBit: Expr) = FunctionApp("Acquire$Mask", List(heldBit))
+ def AcquireCredits(heldBit: Expr) = FunctionApp("Acquire$Credits", List(heldBit))
def CallHeap(joinableBit: Expr) = FunctionApp("Call$Heap", List(joinableBit))
def CallMask(joinableBit: Expr) = FunctionApp("Call$Mask", List(joinableBit))
+ def CallCredits(joinableBit: Expr) = FunctionApp("Call$Credits", List(joinableBit))
def CallArgs(joinableBit: Expr) = FunctionApp("Call$Args", List(joinableBit))
- def submask(m1: Expr, m2: Expr) = FunctionApp("submask", List(m1, m2))
+ def submask(m0: Expr, m1: Expr) = FunctionApp("submask", List(m0, m1))
object TranslationHelper {
def wf(h: Expr, m: Expr) = FunctionApp("wf", List(h, m));
def IsGoodMask(m: Expr) = FunctionApp("IsGoodMask", List(m))
def IsGoodInhaleState(a: Expr, b: Expr, c: Expr) = FunctionApp("IsGoodInhaleState", List(a, b, c))
- def isHeldInHeap(e: Expr, h: Expr) = 0 < h.select(e, "held")
+ def contributesToWaitLevel(e: Expr, h: Expr, c: Expr) =
+ (0 < h.select(e, "held")) || (new Boogie.MapSelect(c, e) < 0)
def NonEmptyMask(m: Expr) = ! FunctionApp("EmptyMask", List(m))
def NonPredicateField(f: String) = FunctionApp("NonPredicateField", List(VarExpr(f)))
def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))
@@ -2204,6 +2329,8 @@ object TranslationHelper { case RdAccessAll(obj, perm) =>
RdAccessAll(func(obj),
perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })
+ case Credit(e, None) => Credit(func(e), None)
+ case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
case Holds(e) => Holds(func(e))
case RdHolds(e) => RdHolds(func(e))
case e: Assigned => e
diff --git a/Chalice/test.bat b/Chalice/test.bat index 66fd9853..fde3cc60 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -9,7 +9,8 @@ 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 OwickiGries) do (
+ prog0 prog1 prog2 prog3 prog4
+ RockBand swap OwickiGries ProdConsChannel) do (
echo Testing %%f.chalice ...
echo ------ Running regression test %%f.chalice >> Output
%CHALICE% %* examples\%%f.chalice >> Output 2>&1
diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el index 91c69120..7a6b6d4c 100644 --- a/Util/Emacs/chalice-mode.el +++ b/Util/Emacs/chalice-mode.el @@ -32,14 +32,15 @@ `(,(chalice-regexp-opt '(
"class" "ghost" "var" "const" "external" "function" "method"
"predicate" "returns" "requires" "ensures" "lockchange"
- "invariant"
+ "invariant" "channel" "condition" "where"
)) . font-lock-builtin-face)
`(,(chalice-regexp-opt '(
"above" "acc" "acquire" "and" "assert" "assigned" "assume"
- "below" "between" "call"
+ "below" "between" "call" "credit"
"downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"
"if" "in" "install" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"
- "old" "rd" "release" "result" "share" "this" "unfold" "unfolding" "unshare" "while"
+ "old" "rd" "receive" "release" "result" "send" "share"
+ "this" "unfold" "unfolding" "unshare" "while"
"false" "true" "null")) . font-lock-keyword-face)
`(,(chalice-regexp-opt '("bool" "int" "seq" "token")) . font-lock-type-face)
)
|