Chalice: pretty printer now prints element type for sequences; fixed a bug in copying resolved member in sequence accesses; added graph closure (DSW) verification example

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))