Chalice: fixed typos in strings; trying out committing with TFS

4 files changed, 41 insertions, 7 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 5f297100..2452f0e1 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -262,6 +262,7 @@ case class MemberAccess(e: Expression, id: String) extends Expression {
 }

 case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression

 

+// TODO: perm should really be a separate abstract case class with Write and Read cases; this can simplify resolving/translation

 sealed abstract class PermissionExpr extends Expression

 sealed abstract class MemberPermission extends PermissionExpr {

   def getMemberAccess : MemberAccess

@@ -280,8 +281,13 @@ case class AccessAll(obj: Expression, perm: Option[Expression]) extends WildCard
 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 AccessSeq(s: Expression, f: Option[String], perm: Option[Expression]) extends WildCardPermission {

+  var memberAccess: Option[MemberAccess] = None; // resolved (for s[0] to make type checker happy)

+}

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

+  var memberAccess: Option[MemberAccess] = None; // resolved (for s[0] to make type checker happy)

+}

+

 

 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/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 00545103..038e5b49 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -233,7 +233,7 @@ object PrintProgram {
       perm match { case None => case Some(perm) => print(", "); Expr(perm) }

       print(")")

     case RdAccessSeq(s, f, p) =>

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

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

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

       p match {

         case None =>          print(")")

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 7cf40bd7..af01ab9d 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -664,23 +664,31 @@ object Resolver {
    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")

+     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 Some(x) =>

+         var ma = MemberAccess(At(s, IntLiteral(0)), x);

+         ma.pos = expr.pos;

+         ResolveExpr(ma, context, twoStateContext, true);

+         expr.memberAccess = Some(ma);

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

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

      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 Some(x) =>

+         var ma = MemberAccess(At(s, IntLiteral(0)), x);

+         ma.pos = expr.pos;

+         ResolveExpr(ma, context, twoStateContext, true);

+         expr.memberAccess = Some(ma);

        case _ => }

      expr.typ = BoolClass

    case expr@ Credit(e,n) =>

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 70d738e5..19bcdd74 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1511,6 +1511,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val inhalee = RdAccess(ma, perm);

         inhalee.pos = acc.pos;

         Inhale(inhalee, ih, check) }

+    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;

+        Inhale(inhalee, ih, check) }

+    case RdAccessSeq(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 = RdAccessSeq(s, Some(f.id), perm); inhalee.memberAccess = Some(ma); inhalee.pos = p.pos;

+        Inhale(inhalee, ih, check) }

     case acc@Access(e,perm) =>

       val trE = Tr(e.e)

       val module = currentClass.module;

@@ -1649,6 +1659,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val exhalee = RdAccess(ma, perm);

         exhalee.pos = acc.pos;

         Exhale(exhalee, em, eh, error, check) }

+    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;

+        Exhale(exhalee, em, eh, error, check) }

+    case RdAccessSeq(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 = RdAccessSeq(s, Some(f.id), perm); exhalee.memberAccess = Some(ma); exhalee.pos = p.pos;

+        Exhale(exhalee, em, eh, error, check) }

     case acc@Access(e,perm) =>

       val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;

       // look up the fraction