summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Chalice/examples/SchorrWaite.chalice144
-rw-r--r--Chalice/src/Ast.scala4
-rw-r--r--Chalice/src/Parser.scala21
-rw-r--r--Chalice/src/PrettyPrinter.scala8
-rw-r--r--Chalice/src/Resolver.scala7
-rw-r--r--Chalice/src/Translator.scala19
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))