Chalice: added surface syntax for acc(s[*].*) and acc(s[*].f); extended AST, resolver, printer; translation is not yet done

7 files changed, 85 insertions, 26 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index b18e15c5..5f297100 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -271,7 +271,7 @@ sealed abstract class WildCardPermission extends PermissionExpr
 case class Access(e: MemberAccess, perm: Option[Expression]) extends MemberPermission {

   def getMemberAccess = e : MemberAccess;

 }

-// Some(None) is the epsilon

+// perm == Some(None) is the epsilon

 case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends MemberPermission {

   def getMemberAccess = e : MemberAccess;

 }

@@ -279,6 +279,10 @@ case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends M
 case class AccessAll(obj: Expression, perm: Option[Expression]) extends WildCardPermission

 case class RdAccessAll(obj: Expression, perm: Option[Option[Expression]]) extends WildCardPermission

 

+// f == Nil is all fields

+case class AccessSeq(s: Expression, f: Option[String], perm: Option[Expression]) extends WildCardPermission

+case class RdAccessSeq(s: Expression, f: Option[String], perm: Option[Option[Expression]]) extends WildCardPermission

+

 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/Chalice.scala b/Chalice/src/Chalice.scala
index 2f54b71f..49f6b74e 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -10,7 +10,7 @@ import java.io.FileWriter
 import scala.util.parsing.input.Position

 

 object Chalice {

- def main(args: Array[String]): unit = {

+ def main(args: Array[String]): Unit = {

    var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

    // parse command-line arguments

    var inputName: String = null

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 56e0a358..f759831b 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -196,7 +196,8 @@ class ChaliceToCSharp {
         ")"

       case Range(min, max) => "Chalice.ImmutableList.Range(" + convertExpression(min) + ", " + convertExpression(max) + ")"

       case Length(s) => convertExpression(s) + ".Length"

-      case IfThenElse(c, thn, els) => "(" + convertExpression(c) + " ? " + convertExpression(thn) + " : " + convertExpression(els) + ")" 

+      case IfThenElse(c, thn, els) => "(" + convertExpression(c) + " ? " + convertExpression(thn) + " : " + convertExpression(els) + ")"

+      case _ => throw new Exception("Expression not supported yet!");

     }

   }

   

@@ -224,7 +225,7 @@ class ChaliceToCSharp {
   

   // utility methods below

   

-  var uniqueInt: int = 0;

+  var uniqueInt: Int = 0;

   val nl = System.getProperty("line.separator");

   var indentLevel = 0

   

@@ -241,7 +242,7 @@ class ChaliceToCSharp {
   }

   

   def indent: String = {

-    def doIndent(i: int): String = {

+    def doIndent(i: Int): String = {

       if(i==0) { "" } else { "  " + doIndent(i-1) }

     }

     doIndent(indentLevel);

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 68c1c848..3cdc19d4 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -394,22 +394,25 @@ class Parser extends StandardTokenParsers {
   def exprBody =

     "{" ~> expression <~ "}"

 

+  // what is "FerSure"?

   def selectExprFerSure: Parser[MemberAccess] =

     positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ {

       case e ~ _ ~ field ~ moreFields =>

         (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>

           val result = MemberAccess(target, f); result.pos = target.pos; result }})

   def selectExprFerSureX: Parser[MemberAccess] =

-    positioned(atom ~ "." ~ identOrSpecial ~ ("." ~> ident *) ^^ {

-      case e ~ _ ~ field ~ moreFields =>

+    positioned(atom ~ identOrSpecial ~ ("." ~> ident *) ^^ {

+      case e ~ field ~ moreFields =>

         (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>

           val result = MemberAccess(target, f); result.pos = target.pos; result }})

   def identOrSpecial: Parser[String] =

-    (  ident ^^ { case s => s }

-    | "acquire" ^^^ "acquire"

-    | "release" ^^^ "release"

-    | "fork" ^^^ "fork"

-    | "*" ^^^ "*"

+    ( "." ~> ident ^^ { case s => s }

+    | "." ~> "acquire" ^^^ "acquire"

+    | "." ~> "release" ^^^ "release"

+    | "." ~> "fork" ^^^ "fork"

+    | "." ~> "*" ^^^ "*"

+    | "["~"*"~"]"~"."~"*" ^^^ "[*].*"

+    | "["~"*"~"]" ^^^ "[*]"

     )

 

   def atom : Parser[Expression] =

@@ -442,14 +445,18 @@ class Parser extends StandardTokenParsers {
       | selectExprFerSureX ~ rdPermArg <~ ")"

       ) ^^ {

         case MemberAccess(obj, "*") ~ p => RdAccessAll(obj, p);

+        case MemberAccess(obj, "[*].*") ~ p => RdAccessSeq(obj, None, p);

+        case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => RdAccessSeq(obj, Some(f), p);

         case e ~ p => RdAccess(e,p)

       }

     | "acc" ~> "(" ~>

       ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ ("," ~> expression ?) <~ ")"

       | selectExprFerSureX ~ ("," ~> expression ?) <~ ")"

       ) ^^ {

-        case MemberAccess(obj, "*") ~ perm => AccessAll(obj, perm);

-        case e ~ perm => Access(e, perm)

+        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 e ~ p => Access(e, p)

       }

     | "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ {

         case ch ~ n => Credit(ch, n) }

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index ef775b2a..00545103 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -221,7 +221,20 @@ object PrintProgram {
       perm match { case None => case Some(perm) => print(", "); Expr(perm) }

       print(")")

     case RdAccessAll(obj, p) =>

-     print("rd("); Expr(e); print(".*");

+      print("rd("); Expr(e); print(".*");

+      p match {

+        case None =>          print(")")

+        case Some(None) =>    print(", *)")

+        case Some(Some(e)) => print(", "); Expr(e); print(")")

+      }

+    case AccessSeq(s, f, perm) =>

+      print("acc("); Expr(s); print("[*].");

+      f match { case None => print("*"); case Some(x) => print(x)}

+      perm match { case None => case Some(perm) => print(", "); Expr(perm) }

+      print(")")

+    case RdAccessSeq(s, f, p) =>

+      print("rd("); Expr(s); print("[*].*");

+      f match { case None => print("*"); case Some(x) => print(x)}

       p match {

         case None =>          print(")")

         case Some(None) =>    print(", *)")

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index d2f4d0f2..7cf40bd7 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -661,6 +661,28 @@ object Resolver {
        case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

        case _ => }

      expr.typ = BoolClass

+   case expr @ AccessSeq(s, f, perm) =>

+     if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")

+     ResolveExpr(s, context, twoStateContext, false)

+     if(!s.typ.IsSeq) context.Error(expr.pos, "Target of [*] must be sequence")

+     perm match {

+       case None =>

+       case Some(perm) => 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);

+       case _ => }

+     expr.typ = BoolClass

+   case expr @ RdAccessSeq(s, f, perm) =>

+     if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")

+     ResolveExpr(s, context, twoStateContext, false)

+     if(!s.typ.IsSeq) context.Error(expr.pos, "Target of [*] must be object reference.")

+     perm match {

+       case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

+       case _ => }

+     f match {

+       case Some(x) => var ma = MemberAccess(At(s, IntLiteral(0)), x); ma.pos = expr.pos; ResolveExpr(ma, context, twoStateContext, true);

+       case _ => }

+     expr.typ = BoolClass

    case expr@ Credit(e,n) =>

      if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts")

      ResolveExpr(e, context, twoStateContext, false)

@@ -946,6 +968,12 @@ object Resolver {
    case RdAccessAll(obj, perm) =>

      CheckRunSpecification(obj, context, false)

      perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

+   case AccessSeq(s, f, perm) =>

+     CheckRunSpecification(s, context, false)

+     perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }

+   case RdAccessSeq(s, f, perm) =>

+     CheckRunSpecification(s, context, false)

+     perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

    case expr@ Credit(e, n) =>

      CheckRunSpecification(e, context, false)

      CheckRunSpecification(expr.N, context, false)

@@ -1015,6 +1043,10 @@ object Resolver {
        func(obj); perm match { case Some(p) => func(p); case _ => ; }

      case RdAccessAll(obj, perm) =>

        func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; }

+     case AccessSeq(s, f, perm) =>

+       func(s); perm match { case Some(p) => func(p); case _ => ; }

+     case RdAccessSeq(s, f, perm) =>

+       func(s); perm match { case Some(Some(p)) => func(p); case _ => ; }

      case Credit(e, n) =>

        func(e); n match { case Some(n) => func(n); case _ => }

      case Holds(e) => func(e);

@@ -1044,6 +1076,7 @@ object Resolver {
      case Div(e0,e1) => func(e0); func(e1);

      case Mod(e0,e1) => func(e0); func(e1);

      case Forall(i, seq, e) => func(seq); func(e);

+     case Exists(i, seq, e) => func(seq); func(e);

      case ExplicitSeq(es) =>

        es foreach { e => func(e) }

      case Range(min, max) =>

@@ -1058,6 +1091,7 @@ object Resolver {
        func(e0); func(e1);

      case Length(e) =>

        func(e)

+     case Contains(s, n) => func(s); func(n);

      case Eval(h, e) =>

        h match {

          case AcquireState(obj) => func(obj);

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index aea9311e..70d738e5 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -48,7 +48,7 @@ class Translator {
       modules = cl.module :: modules;

     }

     // add class name

-    declarations = Const(cl.id + "#t", true, TypeName) :: declarations;

+    declarations = Const(className(cl).id, true, TypeName) :: declarations;

     // translate monitor invariant

     declarations = declarations ::: translateMonitorInvariant(cl.Invariants, cl.pos);

     // translate each member

@@ -1153,10 +1153,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         isDefined(e) ::: 

         prove(nonNull(Tr(e)), e.pos, "Receiver might be null.") ::

         prove(CanRead(Tr(e), fs.f.FullName), fs.pos, "Location might not be readable.")

-      case _:Access => throw new Exception("acc expression unexpected here")

-      case _:RdAccess => throw new Exception("rd expression unexpected here")

-      case _:AccessAll => throw new Exception("acc expression unexpected here")

-      case _:RdAccessAll => throw new Exception("rd expression unexpected here")

+      case _:PermissionExpr => throw new Exception("permission expression unexpected here: " + e.pos)

       case c@Credit(e, n) =>

         isDefined(e);

         isDefined(c.N)

@@ -1328,10 +1325,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         r !=@ 0 // joinable is encoded as an integer

       else

         r

-    case _:Access => throw new Exception("acc expression unexpected here")

-    case _:RdAccess => throw new Exception("rd expression unexpected here")

-    case _:AccessAll => throw new Exception("acc expression unexpected here")

-    case _:RdAccessAll => throw new Exception("rd expression unexpected here")

+    case _:PermissionExpr => throw new Exception("permission expression unexpected here: " + e.pos)

     case _:Credit => throw new Exception("credit expression unexpected here")

     case Holds(e) =>

       (0 < Heap.select(Tr(e), "held")) &&

@@ -2356,13 +2350,19 @@ object TranslationHelper {
              perm match { case None => perm case Some(perm) => Some(func(perm)) })

       case RdAccess(e, perm) =>

         RdAccess(func(e).asInstanceOf[MemberAccess],

-               perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })

+             perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })

       case AccessAll(obj, perm) =>

         AccessAll(func(obj),

              perm match { case None => perm case Some(perm) => Some(func(perm)) })

       case RdAccessAll(obj, perm) =>

         RdAccessAll(func(obj),

-               perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })

+             perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })

+      case AccessSeq(s, f, perm) =>

+        AccessSeq(func(s), f,

+             perm match { case None => perm case Some(perm) => Some(func(perm)) })

+      case RdAccessSeq(s, f, perm) =>

+        RdAccessSeq(func(s), f,

+             perm match { case Some(Some(p)) => Some(Some(func(p))) case _ => perm })

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