diff options
-rw-r--r-- | Chalice/examples/SchorrWaite.chalice | 144 | ||||
-rw-r--r-- | Chalice/src/Ast.scala | 4 | ||||
-rw-r--r-- | Chalice/src/Parser.scala | 21 | ||||
-rw-r--r-- | Chalice/src/PrettyPrinter.scala | 8 | ||||
-rw-r--r-- | Chalice/src/Resolver.scala | 7 | ||||
-rw-r--r-- | Chalice/src/Translator.scala | 19 |
6 files changed, 172 insertions, 31 deletions
diff --git a/Chalice/examples/SchorrWaite.chalice b/Chalice/examples/SchorrWaite.chalice new file mode 100644 index 00000000..8fbfed0e --- /dev/null +++ b/Chalice/examples/SchorrWaite.chalice @@ -0,0 +1,144 @@ +// Schorr-Waite algorithm in Chalice +// (see Test/dafny1/SchorrWaite.dfy) + +class Node { + var left: Node; + var right: Node; + var marked: bool; + var l: bool; + var r: bool; +} + +class Main { + method RecursiveMark(root: Node, S: seq<Node>) + requires acc(S[*].marked, 50) && acc(S[*].*, 50); + requires root != null && root in S; + // S is closed under 'left' and 'right': + requires forall n in S :: n != null && + ((n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S)); + requires forall n in S :: ! n.marked; + ensures acc(S[*].marked, 50) && acc(S[*].*, 50); + ensures root.marked; + // nodes reachable from 'root' are marked: + ensures forall n in S :: n.marked ==> + ((n.left != null ==> n.left in S && n.left.marked) && + (n.right != null ==> n.right in S && n.right.marked)); + { + var stack: seq<Node> := []; + call RecursiveMarkWorker(root, S, stack); + } + + method RecursiveMarkWorker(root: Node, S: seq<Node>, stack: seq<Node>) + requires acc(S[*].marked, 50) && acc(S[*].*, 50); + requires root != null && root in S; + requires forall n in S :: n != null && + ((n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S)) + requires forall n in S :: n.marked ==> + (n in stack || + ((n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked))); + requires forall n in stack :: n != null && n in S && n.marked; + ensures acc(S[*].marked, 50) && acc(S[*].*, 50); + ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right); + ensures forall n in S :: n.marked ==> + (n in stack || + ((n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked))); + ensures forall n in S :: old(n.marked) ==> n.marked; + ensures root.marked; + { + if (! root.marked) { + root.marked := true; + var next:seq<Node> := [root] ++ stack; + assert next[0] == root; + if (root.left != null) { + call RecursiveMarkWorker(root.left, S, next); + } + + if (root.right != null) { + call RecursiveMarkWorker(root.right, S, next); + } + } + } + + method IterativeMark(root: Node, S: seq<Node>) + requires acc(S[*].*); + requires root in S; + requires forall n in S :: n != null && + (n.left != null ==> n.left in S) && + (n.right != null ==> n.right in S); + requires forall n in S :: ! n.marked; + requires forall n in S :: ! n.l && ! n.r; + ensures acc(S[*].*); + ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right); + ensures root.marked; + ensures forall n in S :: n.marked ==> + (n.left != null ==> n.left.marked) && + (n.right != null ==> n.right.marked); + ensures forall n in S :: ! n.l && ! n.r; + { + var t:Node := root; + t.marked := true; + var stack: seq<Node> := []; + + var stop := false; + while(!stop) + invariant acc(S[*].*); + invariant root.marked && t in S && t !in stack; + invariant forall n in stack :: n in S; + invariant forall i in [0:|stack|] :: forall j in [i+1:|stack|] :: stack[i] != stack[j]; + invariant forall n in S :: (n in stack || n == t) ==> + n.marked && + (n.r ==> n.l) && + (n.l && n.left != null ==> n.left in S && n.left.marked) && + (n.r && n.right != null ==> n.right in S && n.right.marked) + // stack is linked + invariant forall i in [1:|stack|] :: stack[i-1] == (stack[i].l ? stack[i].right : stack[i].left); + invariant 0 < |stack| ==> t == (stack[0].l ? stack[0].right : stack[0].left); + // goal + invariant forall n in S :: n.marked && n !in stack && n != t ==> + (n.left != null ==> n.left in S && n.left.marked) && + (n.right != null ==> n.right in S && n.right.marked); + // preservation + invariant forall n in S :: n !in stack && n != t ==> ! n.l && ! n.r; + invariant forall n in S :: n.left == old(n.left) && n.right == old(n.right); + invariant stop ==> |stack| == 0 && ! t.l && ! t.r && + (t.left != null ==> t.left.marked) && + (t.right != null ==> t.right.marked); + { + if (! t.l && (t.left == null || t.left.marked)) { + // advance + t.l := true; + } else if (t.l && ! t.r && (t.right == null || t.right.marked)) { + // advance + t.r := true; + } else if (t.r) { + // pop + t.l := false; + t.r := false; + if (|stack| == 0) { + stop := true; + } else { + t := stack[0]; + stack := stack[1..]; + if (t.l) {t.r := true} else {t.l := true} + } + } else if (!t.l) { + // push + stack := [t] ++ stack; + assert stack[0] == t; + t := t.left; + t.marked := true; + } else if (!t.r) { + // push + assert t.l; + stack := [t] ++ stack; + assert stack[0] == t; + t := t.right; + t.marked := true; + } + } + } +} diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 8f617e7d..25bfb975 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -277,9 +277,7 @@ case class Access(e: MemberAccess, perm: Permission) extends PermissionExpr(perm def getMemberAccess = e : MemberAccess;
}
case class AccessAll(obj: Expression, perm: Permission) extends WildCardPermission(perm)
-case class AccessSeq(s: Expression, f: Option[String], perm: Permission) extends WildCardPermission(perm) {
- var memberAccess: Option[MemberAccess] = None; // resolved (for s[0] to make type checker happy) -- f == Nil is all fields
-}
+case class AccessSeq(s: Expression, f: Option[MemberAccess], perm: Permission) extends WildCardPermission(perm)
case class Credit(e: Expression, n: Option[Expression]) extends Expression {
def N = n match { case None => IntLiteral(1) case Some(n) => n }
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index d584a483..69c011a8 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -100,14 +100,17 @@ class Parser extends StandardTokenParsers { case None => Nil
case Some(ids) => ids }
def formalList(immutable: Boolean) = {
- def MVar(id: String, t: Type) = {
- currentLocalVariables = currentLocalVariables + id
- if (immutable) new ImmutableVariable(id,t) else new Variable(id,t)
- }
- ( idType ^^ { case (id,t) => MVar(id,t)} ) ~
- (("," ~> idType ^^ { case (id,t) => MVar(id,t)} ) *) ^^ {
- case e ~ ee => e::ee }
+ repsep(formal(immutable), ",")
}
+ def formal(immutable: Boolean): Parser[Variable] =
+ idType ^^ {case (id,t) =>
+ currentLocalVariables = currentLocalVariables + id;
+ if (immutable)
+ new ImmutableVariable(id,t)
+ else
+ new Variable(id,t)
+ }
+
def methodSpec =
positioned( "requires" ~> expression <~ Semi ^^ Precondition
| "ensures" ~> expression <~ Semi ^^ Postcondition
@@ -446,7 +449,7 @@ class Parser extends StandardTokenParsers { ) ^^ {
case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
- case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(f), p);
+ case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
case e ~ p => Access(e, p)
}
| "acc" ~> "(" ~>
@@ -455,7 +458,7 @@ class Parser extends StandardTokenParsers { ) ^^ {
case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
- case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(f), p);
+ case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
case e ~ p => Access(e, p)
}
| "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ {
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala index 0dec5ba2..af068b23 100644 --- a/Chalice/src/PrettyPrinter.scala +++ b/Chalice/src/PrettyPrinter.scala @@ -19,7 +19,7 @@ object PrintProgram { case MonitorInvariant(e) =>
print(" invariant "); Expr(e); println(Semi)
case f@ Field(id, t) =>
- println(" " + (if (f.IsGhost) "ghost " else "") + "var " + id + ": " + t.id + Semi)
+ println(" " + (if (f.IsGhost) "ghost " else "") + "var " + id + ": " + t.FullName + Semi)
case m: Method =>
print(" method " + m.id)
print("("); VarList(m.ins); print(")")
@@ -87,7 +87,7 @@ object PrintProgram { case LocalVar(id,t,c,g,rhs) =>
if (g) print("ghost ")
if (c) print("const ") else print("var ")
- print(id + ": " + t.id)
+ print(id + ": " + t.FullName)
rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
println(Semi)
case Call(_, outs, obj, id, args) =>
@@ -176,8 +176,8 @@ object PrintProgram { def VarList(vv: List[Variable]) = vv match {
case Nil =>
case v :: rest =>
- print(v.id + ": " + v.t.id)
- rest foreach { v => print(", " + v.id + ": " + v.t.id) }
+ print(v.id + ": " + v.t.FullName)
+ rest foreach { v => print(", " + v.id + ": " + v.t.FullName) }
}
def ExprList(ee: List[Expression]) = ee match {
case Nil =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index ae9db65c..91bc1ede 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -652,10 +652,7 @@ object Resolver { ResolveExpr(perm, context, twoStateContext, false);
f match {
case Some(x) =>
- var ma = MemberAccess(At(s, IntLiteral(0)), x);
- ma.pos = expr.pos;
- ResolveExpr(ma, context, twoStateContext, true);
- expr.memberAccess = Some(ma);
+ ResolveExpr(x, context, twoStateContext, true);
case _ => }
expr.typ = BoolClass
case expr@ Credit(e,n) =>
@@ -767,7 +764,7 @@ object Resolver { ResolveExpr(e0, context, twoStateContext, false);
ResolveExpr(e1, context, twoStateContext, false);
if(! e1.typ.IsSeq) context.Error(contains.pos, "RHS operand of 'in' must be sequence. (found: " + e1.typ.FullName + ").");
- if(e0.typ ne e1.typ.parameters(0)) context.Error(contains.pos, "LHS operand's type must be element type of sequence. (found: " + e0.typ.FullName + ", expected: " + e1.typ.parameters(0).FullName + ").");
+ else if(e0.typ ne e1.typ.parameters(0)) context.Error(contains.pos, "LHS operand's type must be element type of sequence. (found: " + e0.typ.FullName + ", expected: " + e1.typ.parameters(0).FullName + ").");
contains.typ = BoolClass;
case bin: BinaryExpr =>
ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 0e6e4590..e5a59385 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1515,7 +1515,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case AccessSeq(s, None, perm) =>
s.typ.parameters(0).Fields flatMap { f =>
val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
- val inhalee = AccessSeq(s, Some(f.id), perm); inhalee.memberAccess = Some(ma); inhalee.pos = p.pos;
+ val inhalee = AccessSeq(s, Some(ma), perm); inhalee.pos = p.pos;
Inhale(inhalee, ih, check) }
case acc@Access(e,perm) =>
val trE = Tr(e.e)
@@ -1541,10 +1541,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodState(new Boogie.MapSelect(ih, trE, memberName))) ::
bassume(wf(Heap, Mask)) ::
bassume(wf(ih, Mask))
- case acc @ AccessSeq(s, Some(_), perm) =>
- if (acc.memberAccess.get.isPredicate) throw new Exception("not yet implemented");
+ case acc @ AccessSeq(s, Some(member), perm) =>
+ if (member.isPredicate) throw new Exception("not yet implemented");
val e = Tr(s);
- val member = acc.memberAccess.get;
val memberName = member.f.FullName;
val (r, n) = perm match {
case Full => (100, 0) : (Expr, Expr)
@@ -1665,7 +1664,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case AccessSeq(s, None, perm) =>
s.typ.parameters(0).Fields flatMap { f =>
val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
- val exhalee = AccessSeq(s, Some(f.id), perm); exhalee.memberAccess = Some(ma); exhalee.pos = p.pos;
+ val exhalee = AccessSeq(s, Some(ma), perm); exhalee.pos = p.pos;
Exhale(exhalee, em, eh, error, check) }
case acc@Access(e,perm:Write) =>
val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
@@ -1731,10 +1730,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E bassume(IsGoodMask(Mask)) :: // TODO: is this necessary?
bassume(wf(Heap, Mask)) ::
bassume(wf(Heap, em))
- case acc @ AccessSeq(s, Some(_), perm) =>
- if (acc.memberAccess.get.isPredicate) throw new Exception("not yet implemented");
+ case acc @ AccessSeq(s, Some(member), perm) =>
+ if (member.isPredicate) throw new Exception("not yet implemented");
val e = Tr(s);
- val member = acc.memberAccess.get;
val memberName = member.f.FullName;
val (r, n) = perm match {
case Full => (100, 0) : (Expr, Expr)
@@ -2345,7 +2343,7 @@ object TranslationHelper { // TODO: this will update the value of x's position many times -- better than none
for ((v,x) <- sub if v == e.v) { x.pos = v.pos; x.typ = e.typ; return x }
e
- case q : Quantification =>
+ case q: Quantification =>
// would be better if this is a part of manipulate method
val newSub = sub filter { xv => q.Is forall { variable => ! variable.id.equals(xv._1)}};
val result = q match {
@@ -2396,7 +2394,8 @@ object TranslationHelper { case Epsilons(perm) => Epsilons(func(perm))
case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], manipulate(perm, func).asInstanceOf[Permission]);
case AccessAll(obj, perm) => AccessAll(func(obj), manipulate(perm, func).asInstanceOf[Permission]);
- case AccessSeq(s, f, perm) => AccessSeq(func(s), f, manipulate(perm, func).asInstanceOf[Permission]);
+ case AccessSeq(s, None, perm) => AccessSeq(func(s), None, manipulate(perm, func).asInstanceOf[Permission])
+ case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), manipulate(perm, func).asInstanceOf[Permission])
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))
|