diff options
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/examples/Answer | 41 | ||||
| -rw-r--r-- | Chalice/examples/ImplicitLocals.chalice | 27 | ||||
| -rw-r--r-- | Chalice/examples/prog0.chalice | 44 | ||||
| -rw-r--r-- | Chalice/src/Ast.scala | 7 | ||||
| -rw-r--r-- | Chalice/src/ChaliceToCSharp.scala | 15 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 20 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 4 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 98 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 6 | ||||
| -rw-r--r-- | Chalice/test.bat | 2 |
10 files changed, 182 insertions, 82 deletions
diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer index e40b7287..438a9dd6 100644 --- a/Chalice/examples/Answer +++ b/Chalice/examples/Answer @@ -1,7 +1,4 @@ start
------- Running regression test AssociationList.chalice
-
-Boogie program verifier finished with 12 verified, 0 errors
------ Running regression test cell.chalice
142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
@@ -152,9 +149,6 @@ The program did not typecheck. 31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
33.19: undeclared member o in class C
-33.10: undefined local variable a
-33.12: undefined local variable b
-33.14: undefined local variable c
33.5: call of undeclared member m in class int
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)
@@ -163,8 +157,24 @@ The program did not typecheck. 58.17: undeclared member sqrt2 in class C
58.25: undeclared member sqrt2 in class C
62.17: undeclared member s in class C
-62.10: undefined local variable v
62.5: call of undeclared member M in class int
+82.5: call of undeclared member MyMethodX in class ImplicitC
+83.12: undefined local variable a
+83.16: undefined local variable b
+83.16: undeclared member k in class int
+88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+88.13: duplicate actual out-parameter: a
+89.16: undeclared member b in class ImplicitC
+89.16: undeclared member k in class int
+96.21: undeclared member chX in class ImplicitC
+96.5: receive expression (which has type int) does not denote a channel
+97.12: undefined local variable a
+97.16: undefined local variable b
+97.16: undeclared member k in class int
+104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+104.16: duplicate actual out-parameter: a
+105.16: undeclared member b in class ImplicitC
+105.16: undeclared member k in class int
------ Running regression test prog1.chalice
9.10: Location might not be readable.
25.5: Location might not be writable
@@ -195,6 +205,9 @@ Boogie program verifier finished with 51 verified, 4 errors 27.7: The held field of the target of the release statement might not be writable.
Boogie program verifier finished with 6 verified, 3 errors
+------ Running regression test ImplicitLocals.chalice
+
+Boogie program verifier finished with 8 verified, 0 errors
------ Running regression test RockBand.chalice
27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
41.10: Location might not be readable.
@@ -207,12 +220,6 @@ Boogie program verifier finished with 29 verified, 6 errors ------ Running regression test swap.chalice
Boogie program verifier finished with 5 verified, 0 errors
------- Running regression test GhostConst.chalice
-The program did not typecheck.
-7.27: undeclared member c in class C
-13.10: ghost variable not allowed here
-21.10: ghost variable not allowed here
-29.10: ghost fields not allowed here
------ Running regression test OwickiGries.chalice
Boogie program verifier finished with 5 verified, 0 errors
@@ -232,11 +239,3 @@ Boogie program verifier finished with 29 verified, 3 errors ------ Running regression test RockBand-automagic.chalice
Boogie program verifier finished with 35 verified, 0 errors
------- Running regression test Leaks.chalice
- 6.3: Monitor invariant is not allowed to hold write permission to this.mu
- 11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
- 16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
- 29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
- 62.3: Monitor invariant is not allowed to hold write permission to this.mu
-
-Boogie program verifier finished with 7 verified, 5 errors
diff --git a/Chalice/examples/ImplicitLocals.chalice b/Chalice/examples/ImplicitLocals.chalice new file mode 100644 index 00000000..15ebe8e0 --- /dev/null +++ b/Chalice/examples/ImplicitLocals.chalice @@ -0,0 +1,27 @@ +class C {
+ var k: int;
+
+ method MyMethod() returns (x: int, y: C)
+ requires acc(k)
+ ensures acc(y.k) && x < y.k
+ {
+ x := k - 15;
+ y := this;
+ }
+
+ method B() {
+ var c := new C;
+ call a, b := c.MyMethod();
+ assert a < b.k;
+ }
+
+ method D() {
+ var ch := new Ch;
+ var c := new C;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, b := ch;
+ assert a < b.k;
+ }
+}
+
+channel Ch(x: int, y: C) where acc(y.k) && x < y.k;
diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice index da351c85..7bcb1505 100644 --- a/Chalice/examples/prog0.chalice +++ b/Chalice/examples/prog0.chalice @@ -63,3 +63,47 @@ class C { }
}
class D { }
+
+// ----- tests specifically of implicit locals in CALL and RECEIVE statements
+
+class ImplicitC {
+ var k: int;
+
+ method MyMethod() returns (x: int, y: ImplicitC)
+ requires acc(k)
+ ensures acc(y.k) && x < y.k
+ {
+ x := k - 15;
+ y := this;
+ }
+
+ method B0() {
+ var c := new ImplicitC;
+ call a, b := c.MyMethodX(); // error: method not found (so what is done with a,b?)
+ assert a < b.k;
+ }
+
+ method B1() {
+ var c := new ImplicitC;
+ call a, a := c.MyMethod(); // error: a occurs twice
+ assert a < b.k;
+ }
+
+ method D0() {
+ var ch := new Ch;
+ var c := new ImplicitC;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, b := chX; // error: channel not found (so what is done with a,b?)
+ assert a < b.k;
+ }
+
+ method D1() {
+ var ch := new Ch;
+ var c := new ImplicitC;
+ send ch(c.k - 15, c); // give ourselves some credit
+ receive a, a := ch; // error: a occurs twice
+ assert a < b.k;
+ }
+}
+
+channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 7ad95899..61d7a0f3 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -189,7 +189,8 @@ case class LocalVar(id: String, t: Type, const: boolean, ghost: boolean, rhs: Op else
new Variable(id, t){override val IsGhost = ghost}
}
-case class Call(lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
+case class Call(declaresLocal: List[boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {
+ var locals = List[Variable]()
var m: Method = null
}
case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement
@@ -217,7 +218,8 @@ case class Signal(obj: Expression, id: String, all: boolean) extends Statement { }
case class Send(ch: Expression, args: List[Expression]) extends Statement {
}
-case class Receive(ch: Expression, outs: List[VariableExpr]) extends Statement {
+case class Receive(declaresLocal: List[boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {
+ var locals = List[Variable]()
}
case class Fold(pred: PermissionExpr) extends Statement
case class Unfold(pred: PermissionExpr) extends Statement
@@ -241,6 +243,7 @@ case class LockBottomLiteral extends Literal case class VariableExpr(id: String) extends Expression {
var v: Variable = null
def this(vr: Variable) = { this(vr.id); v = vr; typ = vr.t.typ }
+ def Resolve(vr: Variable) = { v = vr; typ = vr.t.typ }
}
case class Result extends Expression
sealed abstract class ThisExpr extends Expression {
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala index 18c1f849..110f7a2a 100644 --- a/Chalice/src/ChaliceToCSharp.scala +++ b/Chalice/src/ChaliceToCSharp.scala @@ -94,7 +94,7 @@ class ChaliceToCSharp { case Predicate(_, _) => indent + "//predicate" + nl
}
}
-
+
def convertStatement(statement: Statement): String = {
statement match {
case Assert(e) => indent + "// assert" + nl
@@ -112,7 +112,8 @@ class ChaliceToCSharp { indent + x + " = " + convertExpression(rhs) + ";" + nl
case WhileStmt(guard, _, _, body) =>
indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl
- case Call(lhs, target, id, args) =>
+ case c@Call(_, lhs, target, id, args) =>
+ declareLocals(c.locals) +
indent + convertExpression(target) + "." + id + "(" +
repsep(args map convertExpression, ", ") +
(if(args.length > 0 && lhs.length > 0) ", " else "") +
@@ -148,11 +149,19 @@ class ChaliceToCSharp { (if(lhs.length > 0) ", " else "") + convertExpression(token) + "." + "async" + ");" + nl
case s@Send(ch, args) =>
indent + convertExpression(ch) + ".Send(" + repsep(args map convertExpression, ", ") + ")" + ";" + nl
- case r@Receive(ch, outs) =>
+ case r@Receive(_, ch, outs) =>
+ declareLocals(r.locals) +
indent + convertExpression(ch) + ".Receive(" + repsep(outs map { out => "out " + convertExpression(out)}, ", ") + ")" + ";" + nl
}
}
+ def declareLocals(locals: List[Variable]) = {
+ var s = ""
+ for (v <- locals)
+ s = s + indent + convertType(v.t) + " " + v.id + ";" + nl
+ s
+ }
+
def convertExpression(expression: RValue): String = {
expression match {
case IntLiteral(n) => "" + n
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index f9d21f76..a92e5b40 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -207,7 +207,9 @@ class Parser extends StandardTokenParsers { case fa@FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ {val va = VariableExpr(name); va.pos = fa.pos; Send(va, args)}
case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})
| "receive" ~> (identList <~ ":=" ?) ~ expression <~ Semi ^^ {
- case outs ~ e => Receive(e, ExtractList(outs)) }
+ case outs ~ e =>
+ val lhs = ExtractList(outs)
+ Receive(declareImplicitLocals(lhs), e, lhs) }
)
def localVarStmt(const: boolean, ghost: boolean) =
idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
@@ -245,10 +247,22 @@ class Parser extends StandardTokenParsers { ( "invariant" ~> expression <~ Semi ^^ { case e => (e,Nil) }
| "lockchange" ~> expressionList <~ Semi ^^ { case ee => (null,ee) }
)
+ def declareImplicitLocals(lhs: List[VariableExpr]) =
+ for (v <- lhs) yield
+ if (currentLocalVariables contains v.id)
+ false
+ else {
+ currentLocalVariables = currentLocalVariables + v.id
+ true
+ }
def callStmt =
callSignature ^? ({
- case outs ~ VariableExpr(id) ~ args => Call(ExtractList(outs), new ImplicitThisExpr, id, args)
- case outs ~ MemberAccess(obj,id) ~ args => Call(ExtractList(outs), obj, id, args)
+ case outs ~ VariableExpr(id) ~ args =>
+ val lhs = ExtractList(outs)
+ Call(declareImplicitLocals(lhs), lhs, new ImplicitThisExpr, id, args)
+ case outs ~ MemberAccess(obj,id) ~ args =>
+ val lhs = ExtractList(outs)
+ Call(declareImplicitLocals(lhs), lhs, obj, id, args)
}, t => "bad call statement")
def callSignature =
(identList <~ ":=" ?) ~ callTarget ~ expressionList <~ ")" <~ Semi
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index fb94f711..a97a04f9 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -90,7 +90,7 @@ object PrintProgram { print(id + ": " + t.id)
rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
println(Semi)
- case Call(outs, obj, id, args) =>
+ case Call(_, outs, obj, id, args) =>
print("call ")
outs match {
case Nil =>
@@ -150,7 +150,7 @@ object PrintProgram { println(Semi)
case Send(ch, args) =>
print("send "); Expr(ch); print("("); ExprList(args); print(")"); println(Semi)
- case Receive(ch, outs) =>
+ case Receive(_, ch, outs) =>
print("receive ")
outs match {
case Nil =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index f592740d..00daaa92 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -233,14 +233,17 @@ object Resolver { ResolveExpr(lhs, ctx, false, false)(false)
ResolveAssign(lhs, rhs, oldCtx)
}
- case c@CallAsync(declaresLocal, token, obj, id, args) =>
+ case c: CallAsync =>
ResolveStmt(c, ctx)
- if (declaresLocal) {
- c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))
- ResolveType(c.local.t, ctx)
+ if (c.local != null) {
ctx = ctx.AddVariable(c.local)
- ResolveExpr(token, ctx, false, false)(false)
}
+ case c: Call =>
+ ResolveStmt(c, ctx)
+ for (v <- c.locals) { ctx = ctx.AddVariable(v) }
+ case r: Receive =>
+ ResolveStmt(r, ctx)
+ for (v <- r.locals) { ctx = ctx.AddVariable(v) }
case s =>
ResolveStmt(s, ctx)
}
@@ -281,22 +284,10 @@ object Resolver { if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)
case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
- case c @ Call(lhs, obj, id, args) =>
+ case c @ Call(declaresLocal, lhs, obj, id, args) =>
ResolveExpr(obj, context, false, false)(false)
CheckNoGhost(obj, context)
args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }
- var vars = Set[Variable]()
- for (v <- lhs) {
- ResolveExpr(v, context, false, false)(false)
- if (v.v != null) {
- if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")
- if (vars contains v.v) {
- context.Error(v.pos, "duplicate actual out-parameter: " + v.id)
- } else {
- vars = vars + v.v
- }
- }
- }
// lookup method
var typ: Class = IntClass
obj.typ.LookupMember(id) match {
@@ -316,13 +307,8 @@ object Resolver { if (lhs.length != m.outs.length)
context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +
" (" + lhs.length + " instead of " + m.outs.length + ")")
- else {
- for((out, l) <- m.outs zip lhs){
- if(! canAssign(l.typ, out.t.typ))
- context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")
- }
- }
-
+ else
+ c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context)
case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)
}
case Install(obj, lowerBounds, upperBounds) =>
@@ -408,7 +394,9 @@ object Resolver { }
// resolve the token
if (declaresLocal) {
- // this is taken care of in the caller that handles the enclosing block statement
+ c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))
+ ResolveType(c.local.t, context)
+ token.Resolve(c.local)
} else if (token != null) {
ResolveExpr(token, context, false, false)(false)
if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))
@@ -488,39 +476,51 @@ object Resolver { }
case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel")
}
- case r@Receive(ch, outs) =>
+ case r@Receive(declaresLocal, 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 + ")")
- }
- }
+ else
+ r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context)
case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")
}
}
+ def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {
+ var locals = List[Variable]()
+ var vars = Set[Variable]()
+ var ctx = context
+ for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {
+ if (declareLocal) {
+ val local = new Variable(actual.id, new Type(formal.t.typ))
+ locals = locals + local
+ ResolveType(local.t, ctx)
+ actual.Resolve(local)
+ vars = vars + actual.v
+ ctx = ctx.AddVariable(local)
+ } else {
+ ResolveExpr(actual, ctx, false, false)(false)
+ CheckNoGhost(actual, ctx)
+ if (actual.v != null) {
+ if (! canAssign(actual.typ, formal.t.typ))
+ ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " +
+ formal.t.FullName + ", found: " + actual.typ.FullName + ")")
+ if (vars contains actual.v)
+ ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id)
+ else if (actual.v.IsImmutable)
+ ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter")
+ vars = vars + actual.v
+ }
+ }
+ }
+ locals
+ }
+
def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) =
for (b <- lowerBounds ++ upperBounds) {
ResolveExpr(b, context, true, false)(false)
@@ -541,7 +541,7 @@ object Resolver { if (lhs.v != null) Set(lhs.v) else Set() // don't assume resolution was successful
case lv: LocalVar =>
lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }
- case Call(lhs, obj, id, args) =>
+ case Call(_, lhs, obj, id, args) =>
(lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }
case _ => Set()
}
@@ -614,7 +614,7 @@ object Resolver { case ve @ VariableExpr(id) =>
context.LookupVariable(id) match {
case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass
- case Some(v) => ve.v = v; ve.typ = v.t.typ }
+ case Some(v) => ve.Resolve(v) }
case v:ThisExpr => v.typ = context.CurrentClass
case sel @ MemberAccess(e, id) =>
ResolveExpr(e, context, twoStateContext, false)
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 46805d59..b89fd91a 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -656,7 +656,7 @@ class Translator { (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) =>
+ 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)
@@ -678,6 +678,8 @@ class Translator { (for (v <- formalParams) yield Havoc(v)) :::
// inhale where clause
Inhale(List(SubstThisAndVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::
+ // declare any new local variables among the actual outs
+ (for (v <- r.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
(for ((v,e) <- outs zip formalParams) yield (v := e)) :::
// decrease credits
@@ -822,6 +824,8 @@ class Translator { // inhale postconditions (using the state before the call as the "old" state)
postEtran.Inhale(Postconditions(c.m.spec) map
(p => SubstThisAndVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+ // declare any new local variables among the actual outs
+ (for (v <- c.locals) yield BLocal(Variable2BVarWhere(v))) :::
// assign formal outs to actual outs
(for ((v,e) <- lhs zip formalOuts) yield (v :=e))
}
diff --git a/Chalice/test.bat b/Chalice/test.bat index fde3cc60..42124855 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -9,7 +9,7 @@ REM to do: Leaks -checkLeaks for %%f in (cell counter dining-philosophers ForkJoin HandOverHand
iterator iterator2 producer-consumer
- prog0 prog1 prog2 prog3 prog4
+ prog0 prog1 prog2 prog3 prog4 ImplicitLocals
RockBand swap OwickiGries ProdConsChannel) do (
echo Testing %%f.chalice ...
echo ------ Running regression test %%f.chalice >> Output
|