diff options
Diffstat (limited to 'Chalice/src/Translator.scala')
| -rw-r--r-- | Chalice/src/Translator.scala | 48 |
1 files changed, 36 insertions, 12 deletions
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index ccfdefe6..5580b3f3 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -23,8 +23,9 @@ 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 */
+ case ch: Channel =>
+ translateClass(ChannelClass(ch)) :::
+ translateWhereClause(ch)
/* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */
}
}
@@ -52,7 +53,7 @@ class Translator { /**********************************************************************
***************** MEMBERS *****************
**********************************************************************/
-
+
def translateMember(member: Member): List[Decl] = {
member match {
case f: Field =>
@@ -73,6 +74,29 @@ class Translator { Nil
}
}
+
+ def translateWhereClause(ch: Channel): List[Decl] = {
+
+ // pick new k
+ val (whereKV, whereK) = Boogie.NewBVar("whereK", tint, true)
+ val whereKStmts = BLocal(whereKV) :: bassume(0 < whereK && 1000*whereK < permissionOnePercent)
+
+ // check definedness of where clause
+ Proc(ch.channelId + "$whereClause$checkDefinedness",
+ NewBVarWhere("this", new Type(currentClass)) :: (ch.parameters map {i => Variable2BVarWhere(i)}),
+ Nil,
+ GlobalNames,
+ DefaultPrecondition(),
+ whereKStmts :::
+ DefinePreInitialState :::
+ InhaleWithChecking(List(ch.where), "channel where clause", whereK) :::
+ // smoke test: is the where clause equivalent to false?
+ (if (Chalice.smoke) {
+ val a = SmokeTest.initSmokeAssert(ch.pos, "Where clause of channel " + ch.channelId + " is equivalent to false.")
+ translateStatement(a.chaliceAssert, whereK)
+ } else Nil)
+ )
+ }
def translateMonitorInvariant(invs: List[MonitorInvariant], pos: Position): List[Decl] = {
val (h0V, h0) = NewBVar("h0", theap, true); val (m0V, m0) = NewBVar("m0", tmask, true);
@@ -148,6 +172,7 @@ class Translator { GlobalNames,
DefaultPrecondition(),
functionKStmts :::
+ //bassume(CanAssumeFunctionDefs) ::
DefinePreInitialState :::
// check definedness of the precondition
InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", functionK) :::
@@ -628,7 +653,7 @@ class Translator { // pick new k
val (foldKV, foldK) = Boogie.NewBVar("foldK", tint, true)
Comment("fold") ::
- BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < permissionFull) ::
+ BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < percentPermission(1) && 1000*foldK < methodK) ::
isDefined(e) :::
isDefined(perm) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
@@ -644,7 +669,7 @@ class Translator { // pick new k
val (unfoldKV, unfoldK) = Boogie.NewBVar("unfoldK", tint, true)
Comment("unfold") ::
- BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < permissionFull) ::
+ BLocal(unfoldKV) :: bassume(0 < unfoldK && unfoldK < percentPermission(1) && 1000*unfoldK < methodK) ::
isDefined(e) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
isDefined(perm) :::
@@ -667,7 +692,7 @@ class Translator { // pick new k for this fork
val (asyncMethodCallKV, asyncMethodCallK) = Boogie.NewBVar("asyncMethodCallK", tint, true)
BLocal(asyncMethodCallKV) ::
- bassume(0 < asyncMethodCallK) :: // upper bounds are later provided by the exhale
+ bassume(0 < asyncMethodCallK && 1000*asyncMethodCallK < percentPermission(1) && 1000*asyncMethodCallK < methodK) ::
Comment("call " + id) ::
// declare the local variable, if needed
{ if (c.local == null)
@@ -971,7 +996,7 @@ class Translator { // pick new k for this method call
val (methodCallKV, methodCallK) = Boogie.NewBVar("methodCallK", tint, true)
BLocal(methodCallKV) ::
- bassume(0 < methodCallK) :: // upper bounds are later provided by the exhale
+ bassume(0 < methodCallK && 1000*methodCallK < percentPermission(1) && 1000*methodCallK < methodK) ::
Comment("call " + id) ::
// introduce formal parameters and pre-state globals
(for (v <- formalThisV :: formalInsV ::: formalOutsV) yield BLocal(Variable2BVarWhere(v))) :::
@@ -1024,7 +1049,7 @@ class Translator { Comment("while") ::
// pick new k for this method call
BLocal(whileKV) ::
- bassume(0 < whileK) :: // upper bounds are later provided by the exhale
+ bassume(0 < whileK && 1000*whileK < percentPermission(1) && 1000*whileK < methodK) ::
// save globals
(for (v <- preLoopGlobals) yield BLocal(v)) :::
(loopEtran.oldEtran.Heap := loopEtran.Heap) ::
@@ -1483,7 +1508,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E List(prove(nonNull(Tr(obj)), obj.pos, "Receiver might be null.")) :::
// check precondition of the function by exhaling the precondition in tmpHeap/tmpMask/tmpCredits
Comment("check precondition of call") ::
- BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < permissionFull) ::
+ BLocal(funcappKV) :: bassume(0 < funcappK && 1000*funcappK < percentPermission(1)) ::
bassume(assumption) ::
BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
BLocal(tmpMaskV) :: (tmpMask := Mask) :::
@@ -1507,7 +1532,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E val (unfoldingKV, unfoldingK) = Boogie.NewBVar("unfoldingK", tint, true)
Comment("unfolding") ::
- BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < permissionFull) ::
+ BLocal(unfoldingKV) :: bassume(0 < unfoldingK && 1000*unfoldingK < percentPermission(1)) ::
// check definedness
receiverOk ::: isDefined(perm) :::
// copy state into temporary variables
@@ -1907,7 +1932,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean, currentK: Expr, exactchecking: Boolean): List[Boogie.Stmt] = {
if (predicates.size == 0) return Nil;
-
val (emV, em) = NewBVar("exhaleMask", tmask, true)
Comment("begin exhale (" + occasion + ")") ::
BLocal(emV) :: (em := Mask) ::
@@ -2103,7 +2127,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case MethodEpsilon => (currentK, Nil)
case ForkEpsilon(token) =>
val fk = etran.Heap.select(Tr(token), forkK)
- (fk, bassume(0 < fk && fk < permissionFull) /* this is always true for forkK */)
+ (fk, bassume(0 < fk && fk < percentPermission(1)) /* this is always true for forkK */)
case Star =>
val (starKV, starK) = NewBVar("starK", tint, true);
(starK, BLocal(starKV) :: bassume(starK > 0 /* an upper bound is provided later by DecPermission */) :: Nil)
|