diff options
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Ast.scala | 10 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 2 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 16 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 20 |
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
|