diff options
Diffstat (limited to 'Chalice/src')
| -rw-r--r-- | Chalice/src/Ast.scala | 4 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 21 | ||||
| -rw-r--r-- | Chalice/src/PrettyPrinter.scala | 8 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 7 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 19 |
5 files changed, 28 insertions, 31 deletions
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))
|