summaryrefslogtreecommitdiff
path: root/Chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice')
-rw-r--r--Chalice/src/Ast.scala19
-rw-r--r--Chalice/src/Parser.scala6
-rw-r--r--Chalice/src/Translator.scala97
3 files changed, 63 insertions, 59 deletions
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 48990ce9..b18e15c5 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -222,8 +222,8 @@ case class Send(ch: Expression, args: List[Expression]) extends Statement {
case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[VariableExpr]) extends Statement {
var locals = List[Variable]()
}
-case class Fold(pred: PermissionExpr) extends Statement
-case class Unfold(pred: PermissionExpr) extends Statement
+case class Fold(pred: MemberPermission) extends Statement
+case class Unfold(pred: MemberPermission) extends Statement
// expressions
@@ -262,19 +262,22 @@ case class MemberAccess(e: Expression, id: String) extends Expression {
}
case class IfThenElse(con: Expression, then: Expression, els: Expression) extends Expression
-sealed abstract class PermissionExpr extends Expression {
+sealed abstract class PermissionExpr extends Expression
+sealed abstract class MemberPermission extends PermissionExpr {
def getMemberAccess : MemberAccess
}
+sealed abstract class WildCardPermission extends PermissionExpr
-case class Access(e: MemberAccess, perm: Option[Expression]) extends PermissionExpr {
+case class Access(e: MemberAccess, perm: Option[Expression]) extends MemberPermission {
def getMemberAccess = e : MemberAccess;
}
-case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends PermissionExpr {
+// Some(None) is the epsilon
+case class RdAccess(e: MemberAccess, perm: Option[Option[Expression]]) extends MemberPermission {
def getMemberAccess = e : MemberAccess;
}
-case class AccessAll(obj: Expression, perm: Option[Expression]) extends Expression
-case class RdAccessAll(obj: Expression, perm: Option[Option[Expression]]) extends Expression
+case class AccessAll(obj: Expression, perm: Option[Expression]) extends WildCardPermission
+case class RdAccessAll(obj: Expression, 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 }
@@ -290,7 +293,7 @@ case class Not(e: Expression) extends Expression
case class FunctionApplication(obj: Expression, id: String, args: List[Expression]) extends Expression {
var f: Function = null
}
-case class Unfolding(pred: PermissionExpr, in: Expression) extends Expression
+case class Unfolding(pred: MemberPermission, in: Expression) extends Expression
sealed abstract class BinaryExpr(e0: Expression, e1: Expression) extends Expression {
def E0 = e0
def E1 = e1
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index cc82cacf..68c1c848 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -177,11 +177,11 @@ class Parser extends StandardTokenParsers {
case lhs ~ _ ~ rhs => FieldUpdate(lhs, rhs) }
| ("fold" ~> expression <~ Semi) ^? {
case pred: MemberAccess => Fold(Access(pred, None))
- case perm: PermissionExpr => Fold(perm)
+ case perm: MemberPermission => Fold(perm)
}
| ("unfold" ~> expression <~ Semi) ^? {
case pred: MemberAccess => Unfold(Access(pred, None))
- case perm: PermissionExpr => Unfold(perm)
+ case perm: MemberPermission => Unfold(perm)
}
| ("fork") ~> callSignature ^? ({
case None ~ target ~ args =>
@@ -459,7 +459,7 @@ class Parser extends StandardTokenParsers {
| "old" ~> "(" ~> expression <~ ")" ^^ Old
| ("unfolding" ~> suffixExpr <~ "in") ~ expression ^? {
case (pred: MemberAccess) ~ e => val acc = Access(pred, None); acc.pos = pred.pos; Unfolding(acc, e)
- case (perm: PermissionExpr) ~ e => Unfolding(perm, e)
+ case (perm: MemberPermission) ~ e => Unfolding(perm, e)
}
| "|" ~> expression <~ "|" ^^ Length
| ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 740aff47..aea9311e 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -690,7 +690,7 @@ class Translator {
(nw,
Comment("new") ::
BLocal(nw) :: Havoc(nwe) ::
- bassume(nonNull(nwe) && (dtype(nwe) ==@ TrType(cl))) ::
+ bassume(nonNull(nwe) && (dtype(nwe) ==@ className(cl))) ::
bassume(new Boogie.Forall(ttV, f, etran.HasNoPermission(nwe, f.id))) ::
// initial values of fields:
(if (cl.IsChannel)
@@ -1836,7 +1836,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
(new Boogie.MapSelect(mask, obj, field, "perm$N") ==@ Boogie.VarExpr("Permission$PlusInfinity")), error.pos, error.message + " Insufficient epsilons at " + pos + " for " + field + ".") ::
Boogie.If(g, MapUpdate3(mask, obj, field, "perm$N", Boogie.VarExpr("Permission$MinusInfinity")), Nil)
}
- var uniqueInt = 0;
def MapUpdate3(m: Boogie.Expr, arg0: Boogie.Expr, arg1: String, arg2: String, rhs: Boogie.Expr) = {
// m[a,b,c] := rhs
@@ -1918,6 +1917,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
bassert(Tr(expr) <= 100, expr.pos, "Fraction might exceed 100.")
}
}
+
+ // implicit (uses etran)
+
+ implicit def expression2Expr(e: Expression) = etran.Tr(e);
+
+ // prelude (uses etran)
+ def isHeld(e: Expr): Expr = (0 < etran.Heap.select(e, "held"))
+ def isRdHeld(e: Expr): Expr = etran.Heap.select(e, "rdheld")
+ def isShared(e: Expr): Expr = etran.Heap.select(e, "mu") !=@ bLockBottom
+
object S_ExpressionTranslator {
val Globals = {
("Heap", theap) ::
@@ -1927,13 +1936,39 @@ object S_ExpressionTranslator {
}
}
- // implicit
+object TranslationHelper {
+ // implicit conversions
implicit def string2VarExpr(s: String) = VarExpr(s);
- implicit def expression2Expr(e: Expression) = etran.Tr(e);
implicit def field2Expr(f: Field) = VarExpr(f.FullName);
+ implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b)
+ implicit def int2Int(n: Int): Boogie.IntLiteral = Boogie.IntLiteral(n)
+ implicit def lift(s: Boogie.Stmt): List[Boogie.Stmt] = List(s)
+ implicit def type2BType(cl: Class): BType = {
+ if(cl.IsRef) {
+ tref
+ } else if(cl.IsBool) {
+ tbool
+ } else if(cl.IsMu) {
+ tmu
+ } else if(cl.IsInt) {
+ tint
+ } else if(cl.IsSeq) {
+ tseq(type2BType(cl.asInstanceOf[SeqClass].parameter))
+ } else {
+ assert(false, "unexpectected type: " + cl.FullName); null
+ }
+ }
+ implicit def decl2DeclList(decl: Decl): List[Decl] = List(decl)
+ implicit def function2RichFunction(f: Function) = RichFunction(f);
- // prelude
+ case class RichFunction(f: Function) {
+ def apply(args: List[Expr]) = {
+ FunctionApp(functionName(f), args)
+ }
+ }
+
+ // prelude definitions
def ModuleType = NamedType("ModuleName");
def ModuleName(cl: Class) = "module#" + cl.module.id;
@@ -1965,12 +2000,10 @@ object S_ExpressionTranslator {
def IsGoodState(e: Expr) = FunctionApp("IsGoodState", List(e));
def dtype(e: Expr) = FunctionApp("dtype", List(e))
def functionName(f: Function) = "#" + f.FullName;
+ def className(cl: Class) = Boogie.VarExpr(cl.id + "#t")
def bnull = Boogie.Null();
def bLockBottom = VarExpr("$LockBottom")
def nonNull(e: Expr): Expr = e !=@ bnull
- def isHeld(e: Expr): Expr = (0 < etran.Heap.select(e, "held"))
- def isRdHeld(e: Expr): Expr = etran.Heap.select(e, "rdheld")
- def isShared(e: Expr): Expr = etran.Heap.select(e, "mu") !=@ bLockBottom
def LastSeenHeap(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Heap", List(sharedBit, heldBit))
def LastSeenMask(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Mask", List(sharedBit, heldBit))
def LastSeenCredits(sharedBit: Expr, heldBit: Expr) = FunctionApp("LastSeen$Credits", List(sharedBit, heldBit))
@@ -1983,7 +2016,6 @@ object S_ExpressionTranslator {
def CallArgs(joinableBit: Expr) = FunctionApp("Call$Args", List(joinableBit))
def submask(m0: Expr, m1: Expr) = FunctionApp("submask", List(m0, m1))
-object TranslationHelper {
def wf(h: Expr, m: Expr) = FunctionApp("wf", List(h, m));
def IsGoodMask(m: Expr) = FunctionApp("IsGoodMask", List(m))
def IsGoodInhaleState(a: Expr, b: Expr, c: Expr) = FunctionApp("IsGoodInhaleState", List(a, b, c))
@@ -1998,34 +2030,6 @@ object TranslationHelper {
def createRange(min: Expr, max: Expr) = FunctionApp("Seq#Range", List(min, max))
def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
- // implicit conversions
- implicit def bool2Bool(b: Boolean): Boogie.BoolLiteral = Boogie.BoolLiteral(b)
- implicit def int2Int(n: Int): Boogie.IntLiteral = Boogie.IntLiteral(n)
- implicit def lift(s: Boogie.Stmt): List[Boogie.Stmt] = List(s)
- implicit def type2BType(cl: Class): BType = {
- if(cl.IsRef) {
- tref
- } else if(cl.IsBool) {
- tbool
- } else if(cl.IsMu) {
- tmu
- } else if(cl.IsInt) {
- tint
- } else if(cl.IsSeq) {
- tseq(type2BType(cl.asInstanceOf[SeqClass].parameter))
- } else {
- assert(false, "unexpectected type: " + cl.FullName); null
- }
- }
- implicit def decl2DeclList(decl: Decl): List[Decl] = List(decl)
- implicit def function2RichFunction(f: Function) = RichFunction(f);
-
- case class RichFunction(f: Function) {
- def apply(args: List[Expr]) = {
- FunctionApp(functionName(f), args)
- }
- }
-
def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, v.t.typ)
def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)
def NewBVarWhere(id: String, tp: Type) = {
@@ -2075,11 +2079,9 @@ object TranslationHelper {
}
}
- def TrType(cl: Class) = Boogie.VarExpr(cl.id + "#t")
-
def TypeInformation(e: Boogie.Expr, cl: Class): Boogie.Expr = {
if (cl.IsRef) {
- (e ==@ Boogie.Null()) || (new Boogie.FunctionApp("dtype", e) ==@ TrType(cl))
+ (e ==@ Boogie.Null()) || (dtype(e) ==@ className(cl))
} else if (cl.IsSeq && cl.parameters(0).IsRef) {
val (v,ve) = Boogie.NewBVar("$i", tint, true);
new Boogie.Forall(List(v), Nil,
@@ -2090,8 +2092,8 @@ object TranslationHelper {
}
}
- def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =
- {
+ def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =
+ {
expr match{
case pred@MemberAccess(e, p) if pred.isPredicate =>
Version(Access(pred, None), etran)
@@ -2110,7 +2112,7 @@ object TranslationHelper {
case e => Boogie.VarExpr("nostate")
}
}
- /* Unused code that would fail for a nontrivial class
+ /* Unused code that would fail for a nontrivial class
def FieldTp(f: Field): String = {
f match {
case SpecialField("mu", _) => "Mu"
@@ -2264,8 +2266,7 @@ object TranslationHelper {
case And(e0,e1) =>
val r = And(SubstRd(e0), SubstRd(e1)); r.typ = BoolClass; r
case e => e
- }
- }
+ }
def UnfoldPredicatesWithReceiverThis(expr: Expression): Expression = {
def unfoldPred(e: Expression): Expression = {
@@ -2301,7 +2302,7 @@ object TranslationHelper {
case None => e;
}
case e: VariableExpr =>
- // TODO: this will update the value of x many times
+ // TODO: this will update the value of x's position many times
for ((v,x) <- sub if v == e.v) { x.pos = v.pos; return x }
e
case q : Quantification =>
@@ -2373,7 +2374,7 @@ object TranslationHelper {
case funapp@FunctionApplication(obj, id, args) =>
val appl = FunctionApplication(func(obj), id, args map { arg => func(arg)}); appl.f = funapp.f; appl
case Unfolding(pred, e) =>
- Unfolding(func(pred).asInstanceOf[PermissionExpr], func(e))
+ Unfolding(func(pred).asInstanceOf[MemberPermission], func(e))
case Iff(e0,e1) => Iff(func(e0), func(e1))
case Implies(e0,e1) => Implies(func(e0), func(e1))
case And(e0,e1) => And(func(e0), func(e1))
@@ -2421,5 +2422,5 @@ object TranslationHelper {
result.pos = expr.pos
result
}
-
+}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 22:40:05 +0000