Chalice:

* fix a compilation problem (scalac relied on old binaries)
* combinator parser and state don't work well together -- added higher-order parser for method transform

5 files changed, 41 insertions, 160 deletions

diff --git a/Chalice/refinements/original/Counter.chalice b/Chalice/refinements/original/Counter.chalice
deleted file mode 100644
index 310a9d78..00000000
--- a/Chalice/refinements/original/Counter.chalice
+++ /dev/null
@@ -1,128 +0,0 @@
-class Cell {var n: int;}
-
-class Counter0 {
-  var x: int;
-  
-  method init() 
-    requires acc(this.*);
-    ensures acc(x);
-  {
-    x := 0;  
-  }
-
-  method inc()
-    requires acc(x);
-    ensures acc(x);
-  {
-    x := x + 1;
-  } 
-
-  method dec()
-    requires acc(x);
-    ensures acc(x);
-  {    
-    x := x - 1;  
-  }
-
-  method magic1() returns (c: Cell) 
-    requires acc(x)
-    ensures acc(c.n);
-  {
-    c := new Cell;
-  }
-
-  method magic2() returns (c: Cell)
-    requires acc(x);
-    ensures acc(x) && acc(c.n);
-  {
-    c := new Cell;
-  }
-}
-
-class Counter1 {
-  ghost var x: int;
-  var y: int;
-  var z: int;  
-  // replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  
-  method init()
-    requires acc(this.*);
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  {
-    x := 0;
-    y := 0;
-    z := 0;    
-  }
-
-  method inc()
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  {
-    x := x + 1;
-    y := y + 1;
-  }
-
-  method dec() 
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  {
-    x := x - 1;
-    z := z + 1;
-  }       
-}
-
-class Counter2 {
-  ghost var x: int;
-  ghost var y: int;
-  ghost var z: int;
-  var a: Cell;
-  var b: Cell;
-  // replace y || z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-  
-  method init() 
-    requires acc(this.*);
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-  {
-    x := 0;
-    y := 0;
-    z := 0;
-    a := new Cell;
-    b := new Cell;
-    a.n := 0;
-    b.n := 0;
-  }
-
-  method inc() 
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-  {
-    x := x + 1;
-    y := y + 1;
-    a.n := a.n + 1;
-  }
-
-  method dec()
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-  {
-    x := x - 1;
-    z := z + 1;
-    b.n := b.n + 1;
-  }
-
-  method magic1() returns (c: Cell)
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-    ensures acc(c.n);
-  {
-    c := a;
-  }
-
-  method magic2() returns (c: Cell)
-    requires acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
-    ensures acc(x) && acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0 && acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n && acc(c.n);
-  {
-    c := a;
-  }
-}
-
-  
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 82391a9c..4e30c621 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -38,6 +38,8 @@ sealed case class Class(classId: String, parameters: List[Class], module: String
   def LookupMember(id: String): Option[NamedMember] = {

     if (id2member contains id)

       Some(id2member(id))

+    else if (IsRefinement)

+      refines.LookupMember(id)         

     else if (IsRef && this != RootClass) {

       // check with root class

       RootClass LookupMember id match {

@@ -187,7 +189,7 @@ case class LockChange(ee: List[Expression]) extends Specification
 

 case class CouplingInvariant(ids: List[String], e: Expression) extends Member {

   assert(ids.size > 0)

-  var fields = null:List[Field]

+  var fields = Nil:List[Field]

 }

 case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Callable(id) {

   var refines = null: Callable

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 0aaef3f0..36f0e22b 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -71,14 +71,14 @@ class Parser extends StandardTokenParsers {
    */

 

   def memberDecl = {

-    currentLocalVariables = Set[String](); assumeAllLocals = false; 

-    positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | transformDecl | couplingDecl)

+    currentLocalVariables = Set[String]();

+    positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | couplingDecl | transformDecl) // important that last one is transformDecl

   }

   def fieldDecl =

         ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }

         | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }

         )

-  def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)

+  def invariantDecl = "invariant" ~> expression <~ Semi ^^ MonitorInvariant

   def methodDecl =

     "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~

     (methodSpec*) ~ blockStatement ^^ {

@@ -96,16 +96,16 @@ class Parser extends StandardTokenParsers {
     "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {

       case id ~ optE => Condition(id, optE) }

   def transformDecl = {

-    assumeAllLocals = true;

-    "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~

-    (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ {

-      case id ~ ins ~ outs ~ spec ~ trans =>

-        MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))

+    "transforms" ~> ident into {id =>

+      assumeAllLocals = true;            

+      formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ ("{" ~> transform <~ "}") ^^ {

+        case ins ~ outs ~ spec ~ trans =>

+          assumeAllLocals = false;

+          MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))

+      }

     }

   }

-  def couplingDecl = positioned(

-    ("replaces" ~> rep1(ident) <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)} 

-  )

+  def couplingDecl = ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}

 

   def formalParameters(immutable: Boolean) =

     "(" ~> (formalList(immutable) ?) <~ ")" ^^ {

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 19ae2bbd..bdcc7108 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -86,15 +86,16 @@ object Resolver {
      case cl: Class if cl.IsRefinement =>

        if (! (decls contains cl.refinesId)) {

          return Errors(List((cl.pos, "refined class " + cl.refinesId + " does not exist")))

-       } else if (! decls(cl.refinesId).isInstanceOf[Class]) {

-         return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class")))

        } else if (cl.refinesId == cl.id) {

          return Errors(List((cl.pos, "class cannot refine itself")))

-       } else {

-         cl.refines = decls(cl.refinesId).asInstanceOf[Class];

-         refinesRel.addNode(cl);

-         refinesRel.addNode(cl.refines);

-         refinesRel.addEdge(cl, cl.refines);

+       } else decls(cl.refinesId) match {

+         case abs: Class =>

+           cl.refines = abs;

+           refinesRel.addNode(cl);

+           refinesRel.addNode(cl.refines);

+           refinesRel.addEdge(cl, cl.refines);

+         case _ =>

+           return Errors(List((cl.pos, "refined declaration " + cl.refinesId + " is not a class")))

        }

      case _ =>

    }

@@ -224,7 +225,8 @@ object Resolver {
                  }

                case None =>

              }

-           case mt: MethodTransform =>

+           case mt: MethodTransform => // need to resolve them in reverse refinement order

+           case ci: CouplingInvariant => ResolveCouplingInvariant(ci, cl, baseContext)

          }

        }

    }

@@ -242,7 +244,6 @@ object Resolver {
    for (List(cl) <- dag.computeTopologicalSort.reverse) {

      for (m <- cl.members) m match {

        case mt: MethodTransform => ResolveTransform(mt, baseContext)

-       case ci: CouplingInvariant => ResolveCouplingInvariant(ci, cl, baseContext) 

        case _ =>

      }

    }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 75d23e53..915049b2 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -23,7 +23,8 @@ 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))

+        /* TODO: admissibility check of where clause */

         /* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */

     }

   }

@@ -68,6 +69,8 @@ class Translator {
         throw new Exception("not yet implemented")

       case mt: MethodTransform =>

         translateMethodTransform(mt)

+      case ci: CouplingInvariant =>

+        Nil

     }

   }

 

@@ -139,15 +142,17 @@ class Translator {
       ExhaleWithChecking(Postconditions(f.spec) map { post => ((if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(post) else post),

               ErrorMessage(f.pos, "Postcondition at " + post.pos + " might not hold."))}, "function postcondition")) ::

     // definition axiom

-    (if (f.definition.isDefined) definitionAxiom(f) else Nil) :::

+    (f.definition match {

+      case Some(definition) => definitionAxiom(f, definition);

+      case None => Nil

+    }) :::

     // framing axiom (+ frame function)

     framingAxiom(f) :::

     // postcondition axiom(s)

     postconditionAxiom(f)

   }

 

-  def definitionAxiom(f: Function): List[Decl] = {

-    assert(f.definition.isDefined)

+  def definitionAxiom(f: Function, definition: Expression): List[Decl] = {

     val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

     val args = VarExpr("this") :: inArgs;

     val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar);

@@ -157,7 +162,7 @@ class Translator {
     val body = etran.Tr(

       if (f.isRecursive && ! f.isUnlimited) {

         val limited = Map() ++ (f.SCC zip (f.SCC map {f =>

-          val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition);

+          val result = Function(f.id + "#limited", f.ins, f.out, f.spec, None);

           result.Parent = f.Parent;

           result;

         }));

@@ -168,9 +173,9 @@ class Translator {
             Some(result)

           case _ => None

         }

-        f.definition.get transform limit;

+        definition transform limit;

       } else {

-        f.definition.get

+        definition

       }

     );

 

@@ -221,7 +226,7 @@ class Translator {
           (applyF ==@ applyFrameFunction))

       )

     } else {

-      // Encoding with two heap quantification

+      // Encoding with universal quantification over two heaps

       /* axiom (forall h1, h2: HeapType, m1, m2: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

             wf(h1,m1) && wf(h2,m2) && version(h1, h2, #C.f) ==>

               #C.f(h1, m1, this, x_1, ..., x_n) == #C.f(h2, m2, this, x_1, ..., x_n)

@@ -247,8 +252,7 @@ class Translator {
   }

 

   def postconditionAxiom(f: Function): List[Decl] = {

-    /* function ##C.f(state, ref, t_1, ..., t_n) returns (t);       

-       axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

+    /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

           wf(h, m) && CanAssumeFunctionDefs ==> Q[#C.f(h, m, this, x_1, ..., x_n)/result]

     */

     val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

@@ -2459,7 +2463,7 @@ object TranslationHelper {
             case Star => throw new Exception("not supported yet")

             case Epsilons(p) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)

           })

-        case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=TranslationOptions.defaults && func.f.definition.isDefined =>

+        case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=Chalice.defaults && func.f.definition.isDefined =>

           Some(SubstVars(func.f.definition.get, obj, func.f.ins, args))

         case _ => None

       }

@@ -2563,7 +2567,9 @@ object TranslationHelper {
     }

   }

 

+  // tags statements to be preserved

   val keepTag = Boogie.Tag("keep")

+  

   // Assume the only composite statement in Boogie is If

   def tag(l: List[Stmt], t: Boogie.Tag):List[Stmt] =

     for (s <- l) yield {